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

Fix typo in resolution error message

Browse source
This commit is contained in:
Guillaume Bury 2015-01-30 10:28:46 +01:00
parent 0e84c5bfb3
commit cef1cef703
2 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
solver/mcproof.ml
View file

@ -80,7 +80,7 @@ module Make(St : Mcsolver_types.S) = struct
done; done;
let l, res = resolve (List.sort_uniq compare_atoms !l) in let l, res = resolve (List.sort_uniq compare_atoms !l) in
if l <> [] then if l <> [] then
raise (Resolution_error "Input cause is a tautology"); raise (Resolution_error "Input clause is a tautology");
res res
(* Adding hyptoheses *) (* Adding hyptoheses *)

6
solver/mcsolver.ml
View file

@ -436,7 +436,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
| fuip :: _ -> | fuip :: _ ->
let name = fresh_lname () in let name = fresh_lname () in
let lclause = make_clause name learnt (List.length learnt) true history in let lclause = make_clause name learnt (List.length learnt) true history in
L.debug 1 "New clause learnt : %a" St.pp_clause lclause; L.debug 2 "New clause learnt : %a" St.pp_clause lclause;
Vec.push env.learnts lclause; Vec.push env.learnts lclause;
attach_clause lclause; attach_clause lclause;
clause_bump_activity lclause; clause_bump_activity lclause;
@ -632,7 +632,9 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma) add_clause ~cnumber:!_th_cnumber atoms (Lemma lemma)
let slice_propagate f lvl = let slice_propagate f lvl =
enqueue_bool (add_atom f) lvl (Semantic lvl) let a = add_atom f in
Iheap.grow_to_by_double env.order (St.nb_vars ());
enqueue_bool a lvl (Semantic lvl)
let current_slice () = Th.({ let current_slice () = Th.({
start = env.tatoms_qhead; start = env.tatoms_qhead;