simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 11:45:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

refactor: remove dead code, some basic simplifications

Browse source
This commit is contained in:
Simon Cruanes 2019-01-26 12:57:33 -06:00 • committed by Guillaume Bury
parent fdc042aee3
commit 0a3a3b576a
1 changed files with 4 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/core/Internal.ml
View file

@ -1248,10 +1248,11 @@ module Make(Plugin : PLUGIN)
else match Plugin.eval st.th a.lit with
| Solver_intf.Unknown -> None
| Solver_intf.Valued (b, l) ->
if l = [] then
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
enqueue_semantic st atom l;
Some b
@ -1962,11 +1963,7 @@ module Make(Plugin : PLUGIN)
(* Check satisfiability *)
let check_clause c =
let tmp = Array.map (fun a ->
if a.is_true then true
else if a.neg.is_true then false
else raise UndecidedLit) c.atoms in
let res = Array.exists (fun x -> x) tmp in
let res = Array.exists (fun a -> a.is_true) c.atoms in
if not res then (
Log.debugf debug
(fun k -> k "Clause not satisfied: @[<hov>%a@]" Clause.debug c);
@ -1974,16 +1971,7 @@ module Make(Plugin : PLUGIN)
) else
true
let check_vec v =
Vec.for_all check_clause v
let check_stack s =
try
Stack.iter (fun c -> if not (check_clause c) then raise Exit) s;
true
with Exit ->
false
let check_vec v = Vec.for_all check_clause v
let check st : bool =
Vec.is_empty st.clauses_to_add &&
check_vec st.clauses_hyps &&