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

fix: allow conflicts below decision level in Make_cdcl_t

Browse source
This commit is contained in:
Simon Cruanes 2020-01-14 22:56:01 -06:00
parent 88550716d8
commit 407a7e83f7
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/core/Internal.ml
View file

@ -8,6 +8,10 @@ module type PLUGIN = sig
val mcsat : bool
(** Is this a mcsat plugin? *)
val has_theory : bool
(** Is this a CDCL(T) plugin or mcsat plugin?
i.e does it have theories *)
include Solver_intf.PLUGIN_MCSAT
end
@ -1366,7 +1370,7 @@ module Make(Plugin : PLUGIN)
assert (decision_level st > 0);
Vec.clear to_unmark;
let conflict_level =
if Plugin.mcsat
if Plugin.mcsat || Plugin.has_theory
then Array.fold_left (fun acc p -> max acc p.var.v_level) 0 c_clause.atoms
else decision_level st
in
@ -2194,6 +2198,7 @@ module Make_cdcl_t(Plugin : Solver_intf.PLUGIN_CDCL_T) =
let eval _ _ = Solver_intf.Unknown
let assign _ t = t
let mcsat = false
let has_theory = true
let iter_assignable _ _ _ = ()
end)
[@@inline][@@specialise]
@ -2202,6 +2207,7 @@ module Make_mcsat(Plugin : Solver_intf.PLUGIN_MCSAT) =
Make(struct
include Plugin
let mcsat = true
let has_theory = false
end)
[@@inline][@@specialise]
@ -2219,6 +2225,7 @@ module Make_pure_sat(Plugin : Solver_intf.PLUGIN_SAT) =
let eval () _ = Solver_intf.Unknown
let assign () t = t
let mcsat = false
let has_theory = false
let iter_assignable () _ _ = ()
let mcsat = false
end)