simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 20:55:39 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Prevent semantic propagations at level 0

Browse source
This commit is contained in:
Guillaume Bury 2018-07-24 23:42:20 +02:00
parent 8cdfe65048
commit 2bba885266
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/core/internal.ml
View file

@ -568,6 +568,10 @@ module Make
else match Plugin.eval a.lit with else match Plugin.eval a.lit with
| Plugin_intf.Unknown -> None | Plugin_intf.Unknown -> None
| Plugin_intf.Valued (b, l) -> | Plugin_intf.Valued (b, l) ->
if l = [] then
raise (Invalid_argument (
Format.asprintf "msat:core/internal.ml: %s"
"semantic propagation at level 0 are currently forbidden"));
let atom = if b then a else a.neg in let atom = if b then a else a.neg in
enqueue_semantic atom l; enqueue_semantic atom l;
Some b Some b