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

fix: bad sign in SAT solver

Browse source
This commit is contained in:
Simon Cruanes 2021-08-21 13:41:30 -04:00
parent 0e77c9ef33
commit 075e251aed
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
2 changed files with 13 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/sat/Solver.ml
View file

@ -466,12 +466,12 @@ module Make(Plugin : PLUGIN)
v v
(* create new variable *) (* create new variable *)
let alloc_var (self:t) ?default_pol (lit:lit) : var * Solver_intf.negated = let alloc_var (self:t) ?default_pol (lit:lit) : var * Solver_intf.same_sign =
let lit, negated = Lit.norm_sign lit in let lit, same_sign = Lit.norm_sign lit in
try Lit_tbl.find self.v_of_lit lit, negated try Lit_tbl.find self.v_of_lit lit, same_sign
with Not_found -> with Not_found ->
let v = alloc_var_uncached_ ?default_pol self lit in let v = alloc_var_uncached_ ?default_pol self lit in
v, negated v, same_sign
let clear_var (self:t) (v:var) : unit = let clear_var (self:t) (v:var) : unit =
Var.unmark self v; Var.unmark self v;
@ -479,17 +479,17 @@ module Make(Plugin : PLUGIN)
Atom.unmark self (Atom.na v); Atom.unmark self (Atom.na v);
() ()
let atom_of_var_ v negated : atom = let atom_of_var_ v same_sign : atom =
if negated then Atom.na v else Atom.pa v if same_sign then Atom.pa v else Atom.na v
let alloc_atom (self:t) ?default_pol lit : atom = let alloc_atom (self:t) ?default_pol lit : atom =
let var, negated = alloc_var self ?default_pol lit in let var, same_sign = alloc_var self ?default_pol lit in
atom_of_var_ var negated atom_of_var_ var same_sign
let find_atom (self:t) lit : atom option = let find_atom (self:t) lit : atom option =
let lit, negated = Lit.norm_sign lit in let lit, same_sign = Lit.norm_sign lit in
match Lit_tbl.find self.v_of_lit lit with match Lit_tbl.find self.v_of_lit lit with
| v -> Some (atom_of_var_ v negated) | v -> Some (atom_of_var_ v same_sign)
| exception Not_found -> None | exception Not_found -> None
end end
type store = Store.t type store = Store.t

6
src/sat/Solver_intf.ml
View file

@ -53,7 +53,7 @@ type ('lit, 'clause) unsat_state =
and type clause = 'clause) and type clause = 'clause)
(** The type of values returned when the solver reaches an UNSAT state. *) (** The type of values returned when the solver reaches an UNSAT state. *)
type negated = bool type same_sign = bool
(** This type is used during the normalisation of lits. (** This type is used during the normalisation of lits.
[true] means the literal stayed the same, [false] that its sign was flipped. *) [true] means the literal stayed the same, [false] that its sign was flipped. *)
@ -145,8 +145,8 @@ module type LIT = sig
val neg : t -> t val neg : t -> t
(** Formula negation *) (** Formula negation *)
val norm_sign : t -> t * negated val norm_sign : t -> t * same_sign
(** Returns a 'normalized' form of the lit, possibly negated (** Returns a 'normalized' form of the lit, possibly same_sign
(in which case return [false]). (in which case return [false]).
[norm] must be so that [a] and [neg a] normalise to the same lit, [norm] must be so that [a] and [neg a] normalise to the same lit,
but one returns [false] and the other [true]. *) but one returns [false] and the other [true]. *)