From 075e251aed6d397cbe9eaf3d81cbe9c76eb91496 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 21 Aug 2021 13:41:30 -0400 Subject: [PATCH] fix: bad sign in SAT solver --- src/sat/Solver.ml | 20 ++++++++++---------- src/sat/Solver_intf.ml | 6 +++--- 2 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 43c50054..bbe83970 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -466,12 +466,12 @@ module Make(Plugin : PLUGIN) v (* create new variable *) - let alloc_var (self:t) ?default_pol (lit:lit) : var * Solver_intf.negated = - let lit, negated = Lit.norm_sign lit in - try Lit_tbl.find self.v_of_lit lit, negated + let alloc_var (self:t) ?default_pol (lit:lit) : var * Solver_intf.same_sign = + let lit, same_sign = Lit.norm_sign lit in + try Lit_tbl.find self.v_of_lit lit, same_sign with Not_found -> let v = alloc_var_uncached_ ?default_pol self lit in - v, negated + v, same_sign let clear_var (self:t) (v:var) : unit = Var.unmark self v; @@ -479,17 +479,17 @@ module Make(Plugin : PLUGIN) Atom.unmark self (Atom.na v); () - let atom_of_var_ v negated : atom = - if negated then Atom.na v else Atom.pa v + let atom_of_var_ v same_sign : atom = + if same_sign then Atom.pa v else Atom.na v let alloc_atom (self:t) ?default_pol lit : atom = - let var, negated = alloc_var self ?default_pol lit in - atom_of_var_ var negated + let var, same_sign = alloc_var self ?default_pol lit in + atom_of_var_ var same_sign 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 - | v -> Some (atom_of_var_ v negated) + | v -> Some (atom_of_var_ v same_sign) | exception Not_found -> None end type store = Store.t diff --git a/src/sat/Solver_intf.ml b/src/sat/Solver_intf.ml index 41189a01..ab9fc650 100644 --- a/src/sat/Solver_intf.ml +++ b/src/sat/Solver_intf.ml @@ -53,7 +53,7 @@ type ('lit, 'clause) unsat_state = and type clause = 'clause) (** 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. [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 (** Formula negation *) - val norm_sign : t -> t * negated - (** Returns a 'normalized' form of the lit, possibly negated + val norm_sign : t -> t * same_sign + (** Returns a 'normalized' form of the lit, possibly same_sign (in which case return [false]). [norm] must be so that [a] and [neg a] normalise to the same lit, but one returns [false] and the other [true]. *)