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

fix(sat): base-level = 1 under assumptions

Browse source
This commit is contained in:
Simon Cruanes 2018-06-11 21:47:37 -05:00
parent 080cde778e
commit 5e380464ce
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/sat/Internal.ml
View file

@ -728,16 +728,17 @@ module Make (Th : Theory_intf.S) = struct
end
let[@inline] theory st = Lazy.force st.th
let[@inline] nb_clauses st = Vec.size st.clauses
let[@inline] decision_level st = Vec.size st.elt_levels
let[@inline] base_level st = if decision_level st > 0 then 1 else 0 (* first level=assumptions *)
let[@inline] at_level_0 st : bool = Vec.is_empty st.backtrack_levels
let[@inline] on_backtrack st f : unit =
if not (at_level_0 st) then (
Vec.push st.backtrack f
)
let[@inline] nb_clauses st = Vec.size st.clauses
let[@inline] decision_level st = Vec.size st.elt_levels
let[@inline] base_level _st = 0
(* [redo_down_to_level_0 f ~undo] performs [f] now. Upon backtracking
before current level, some undo actions scheduled by [f]
might run;