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

refactor: account for @gbury's review

Browse source
This commit is contained in:
Simon Cruanes 2019-12-28 07:47:53 -06:00
parent 919c1e6011
commit 4097ed9dc2
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/core/Internal.ml
View file

@ -1493,6 +1493,7 @@ module Make(Plugin : PLUGIN)
enqueue_bool st fuip ~level:cr.cr_backtrack_lvl (Bcp lclause) enqueue_bool st fuip ~level:cr.cr_backtrack_lvl (Bcp lclause)
) else ( ) else (
assert Plugin.mcsat; assert Plugin.mcsat;
assert (st.next_decisions = []);
st.next_decisions <- [fuip.neg]; st.next_decisions <- [fuip.neg];
) )
end; end;
@ -1929,7 +1930,6 @@ module Make(Plugin : PLUGIN)
and pick_branch_lit st = and pick_branch_lit st =
match st.next_decisions with match st.next_decisions with
| atom :: tl -> | atom :: tl ->
assert Plugin.mcsat;
st.next_decisions <- tl; st.next_decisions <- tl;
pick_branch_aux st atom pick_branch_aux st atom
| [] when decision_level st < Vec.size st.assumptions -> | [] when decision_level st < Vec.size st.assumptions ->

2
src/core/Solver_intf.ml
View file

@ -134,7 +134,7 @@ type ('term, 'formula, 'value, 'proof) acts = {
acts_add_decision_lit: 'formula -> unit; acts_add_decision_lit: 'formula -> unit;
(** Ask the SAT solver to decide on the given formula before it can (** Ask the SAT solver to decide on the given formula before it can
answer [SAT]. This will be removed on backtrack. answer [SAT]. The order of decisions is still unspecified.
Useful for theory combination. *) Useful for theory combination. *)
} }
(** The type for a slice of assertions to assume/propagate in the theory. *) (** The type for a slice of assertions to assume/propagate in the theory. *)