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

Internal check also checks for undecided lits

Browse source
This commit is contained in:
Guillaume Bury 2017-03-30 19:29:53 +02:00
parent 7f634da201
commit 88eaa03968
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/core/internal.ml
View file

@ -1237,7 +1237,11 @@ module Make
(* Check satisfiability *) (* Check satisfiability *)
let check_clause c = let check_clause c =
let res = Array_util.exists (fun a -> a.is_true) c.atoms in 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_util.exists (fun x -> x) tmp in
if not res then begin if not res then begin
Log.debugf debug "Clause not satisfied: @[<hov>%a@]" Log.debugf debug "Clause not satisfied: @[<hov>%a@]"
(fun k -> k St.pp_clause c); (fun k -> k St.pp_clause c);