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

update conflict resolution for better proofs, improve code

Browse source
This commit is contained in:
Simon Cruanes 2021-11-27 15:30:45 -05:00
parent c5c5426ead
commit 2e4fd5e1c1
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
3 changed files with 11 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/core/Sidekick_core.ml
View file

@ -1276,7 +1276,7 @@ end = struct
else None else None
let on_new_term self cc n (t:T.t) : unit = let on_new_term self cc n (t:T.t) : unit =
Log.debugf 50 (fun k->k "@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n); (*Log.debugf 50 (fun k->k "(@[monoid[%s].on-new-term.try@ %a@])" M.name N.pp n);*)
let maybe_m, l = M.of_term cc n t in let maybe_m, l = M.of_term cc n t in
begin match maybe_m with begin match maybe_m with
| Some v -> | Some v ->

2
src/lra/sidekick_arith_lra.ml
View file

@ -627,7 +627,7 @@ module Make(A : ARG) : S with module A = A = struct
(* look for subterms of type Real, for they will need theory combination *) (* look for subterms of type Real, for they will need theory combination *)
let on_subterm (self:state) _ (t:T.t) : unit = let on_subterm (self:state) _ (t:T.t) : unit =
Log.debugf 50 (fun k->k "lra: cc-on-subterm %a" T.pp t); Log.debugf 50 (fun k->k "(@[lra.cc-on-subterm@ %a@])" T.pp t);
if A.has_ty_real t && if A.has_ty_real t &&
not (T.Tbl.mem self.needs_th_combination t) then ( not (T.Tbl.mem self.needs_th_combination t) then (
Log.debugf 5 (fun k->k "(@[lra.needs-th-combination@ %a@])" T.pp t); Log.debugf 5 (fun k->k "(@[lra.needs-th-combination@ %a@])" T.pp t);

19
src/sat/Solver.ml
View file

@ -1329,6 +1329,7 @@ module Make(Plugin : PLUGIN)
AVec.clear learnt; AVec.clear learnt;
let steps = self.temp_step_vec in (* for proof *) let steps = self.temp_step_vec in (* for proof *)
assert (Step_vec.is_empty steps);
(* loop variables *) (* loop variables *)
let pathC = ref 0 in let pathC = ref 0 in
@ -1371,16 +1372,14 @@ module Make(Plugin : PLUGIN)
let atoms = Clause.atoms_a store clause in let atoms = Clause.atoms_a store clause in
for j = 0 to Array.length atoms - 1 do for j = 0 to Array.length atoms - 1 do
let q = atoms.(j) in let q = atoms.(j) in
assert (Atom.is_true store q || assert (Atom.has_value store q);
Atom.is_false store q && assert (Atom.level store q >= 0);
Atom.level store q >= 0); (* unsure? *) if Atom.level store q = 0 then (
if Atom.level store q <= 0 then (
assert (Atom.is_false store q); assert (Atom.is_false store q);
begin match Atom.reason store q with if Proof.enabled self.proof then (
| Some (Bcp cl | Bcp_lazy (lazy cl)) when Proof.enabled self.proof -> let step = proof_of_atom_lvl0_ self (Atom.neg q) in
Step_vec.push steps (Clause.proof_step self.store cl); Step_vec.push steps step;
| _ -> () )
end
); );
if not (Var.marked store (Atom.var q)) then ( if not (Var.marked store (Atom.var q)) then (
Var.mark store (Atom.var q); Var.mark store (Atom.var q);
@ -1549,7 +1548,7 @@ module Make(Plugin : PLUGIN)
(* cannot recover from this *) (* cannot recover from this *)
report_unsat self @@ US_false clause report_unsat self @@ US_false clause
) else if Atom.is_true store a then ( ) else if Atom.is_true store a then (
() (* atom is already true, nothing to do *) () (* atom is already true, (at level 0) nothing to do *)
) else ( ) else (
Log.debugf 40 Log.debugf 40
(fun k->k "(@[sat.add-clause.unit-clause@ :propagating %a@])" (Atom.debug store) a); (fun k->k "(@[sat.add-clause.unit-clause@ :propagating %a@])" (Atom.debug store) a);