From d9bf16dfde85ba6ba34ae6032e47922011cdb718 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 28 Dec 2019 08:07:22 -0600 Subject: [PATCH] feat: allow to set the default polarity of variables at creation time --- src/core/Internal.ml | 25 +++++++++++++++---------- src/core/Msat.ml | 2 +- src/core/Solver_intf.ml | 2 +- 3 files changed, 17 insertions(+), 12 deletions(-) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index e0be3c08..bda30191 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -168,6 +168,7 @@ module Make(Plugin : PLUGIN) let seen_var = 0b1 let seen_pos = 0b10 let seen_neg = 0b100 + let default_pol_true = 0b1000 module Var = struct type t = var @@ -180,8 +181,11 @@ module Make(Plugin : PLUGIN) let[@inline] mark v = v.v_fields <- v.v_fields lor seen_var let[@inline] unmark v = v.v_fields <- v.v_fields land (lnot seen_var) let[@inline] marked v = (v.v_fields land seen_var) <> 0 + let[@inline] set_default_pol_true v = v.v_fields <- v.v_fields lor default_pol_true + let[@inline] set_default_pol_false v = v.v_fields <- v.v_fields land (lnot default_pol_true) + let[@inline] default_pol v = (v.v_fields land default_pol_true) <> 0 - let make (st:st) (t:formula) : var * Solver_intf.negated = + let make ?(default_pol=true) (st:st) (t:formula) : var * Solver_intf.negated = let lit, negated = Formula.norm t in try MF.find st.f_map lit, negated @@ -214,6 +218,7 @@ module Make(Plugin : PLUGIN) aid = cpt_double + 1 (* aid = vid*2+1 *) } in MF.add st.f_map lit var; st.cpt_mk_var <- st.cpt_mk_var + 1; + if default_pol then set_default_pol_true var; Vec.push st.vars (E_var var); var, negated @@ -255,8 +260,8 @@ module Make(Plugin : PLUGIN) a.var.v_fields <- seen_neg lor a.var.v_fields ) - let[@inline] make st lit = - let var, negated = Var.make st lit in + let[@inline] make ?default_pol st lit = + let var, negated = Var.make ?default_pol st lit in match negated with | Solver_intf.Negated -> var.na | Solver_intf.Same_sign -> var.pa @@ -899,8 +904,8 @@ module Make(Plugin : PLUGIN) (* When we have a new literal, we need to first create the list of its subterms. *) - let mk_atom st (f:formula) : atom = - let res = Atom.make st.st f in + let mk_atom ?default_pol st (f:formula) : atom = + let res = Atom.make ?default_pol st.st f in if Plugin.mcsat then ( mk_atom_mcsat_ st res; ); @@ -1668,8 +1673,8 @@ module Make(Plugin : PLUGIN) aux 0 (* Propagation (boolean and theory) *) - let create_atom st f = - let a = mk_atom st f in + let create_atom ?default_pol st f = + let a = mk_atom ?default_pol st f in ignore (th_eval st a); a @@ -1757,8 +1762,8 @@ module Make(Plugin : PLUGIN) let a = create_atom st f in eval_atom_ a - let[@inline] acts_mk_lit st f : unit = - ignore (create_atom st f : atom) + let[@inline] acts_mk_lit st ?default_pol f : unit = + ignore (create_atom ?default_pol st f : atom) let[@inline] acts_mk_term st t : unit = make_term st t @@ -1939,7 +1944,7 @@ module Make(Plugin : PLUGIN) enqueue_assign st l value current_level ) | E_var v -> - pick_branch_aux st v.pa + pick_branch_aux st (if Var.default_pol v then v.pa else v.na) | exception Not_found -> raise_notrace E_sat end diff --git a/src/core/Msat.ml b/src/core/Msat.ml index 0aee8e57..6de87bec 100644 --- a/src/core/Msat.ml +++ b/src/core/Msat.ml @@ -44,7 +44,7 @@ type ('term, 'formula, 'proof) reason = ('term, 'formula, 'proof) Solver_intf.re type ('term, 'formula, 'value, 'proof) acts = ('term, 'formula, 'value, 'proof) Solver_intf.acts = { acts_iter_assumptions: (('term,'formula,'value) assumption -> unit) -> unit; acts_eval_lit: 'formula -> lbool; - acts_mk_lit: 'formula -> unit; + acts_mk_lit: ?default_pol:bool -> 'formula -> unit; acts_mk_term: 'term -> unit; acts_add_clause : ?keep:bool -> 'formula list -> 'proof -> unit; acts_raise_conflict: 'b. 'formula list -> 'proof -> 'b; diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index 5815e659..351850c7 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -108,7 +108,7 @@ type ('term, 'formula, 'value, 'proof) acts = { acts_eval_lit: 'formula -> lbool; (** Obtain current value of the given literal *) - acts_mk_lit: 'formula -> unit; + acts_mk_lit: ?default_pol:bool -> 'formula -> unit; (** Map the given formula to a literal, which will be decided by the SAT solver. *)