simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-27 20:04:49 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Add assertion to check theory conflict clauses

Browse source
This commit is contained in:
Guillaume Bury 2018-07-24 21:51:04 +02:00
parent 1722730e26
commit 354f2013b1
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/core/internal.ml
View file

@ -1007,8 +1007,13 @@ module Make
| Plugin_intf.Unsat (l, p) -> | Plugin_intf.Unsat (l, p) ->
(* conflict *) (* conflict *)
let l = List.rev_map create_atom l in let l = List.rev_map create_atom l in
(* Assert that the conflcit is indeeed a conflict *)
if not @@ List.for_all (fun a -> a.neg.is_true) l then
raise (Invalid_argument "msat:core/internal: invalid conflict");
(* Insert elements for decision (and ensure the heap is big enough) *)
Iheap.grow_to_at_least env.order (St.nb_elt ()); Iheap.grow_to_at_least env.order (St.nb_elt ());
List.iter (fun a -> insert_var_order (elt_of_var a.var)) l; List.iter (fun a -> insert_var_order (elt_of_var a.var)) l;
(* Create the clause and return it. *)
let c = St.make_clause (St.fresh_tname ()) l (Lemma p) in let c = St.make_clause (St.fresh_tname ()) l (Lemma p) in
Some c Some c
end end