From f088ef73e188e81b47f03d5330d18f332c0fc989 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 29 Jan 2016 14:59:48 +0100 Subject: [PATCH 1/2] expose `tag_clause` in Solver.Make --- sat/sat.ml | 2 +- solver/solver.ml | 1 + solver/solver.mli | 3 +++ 3 files changed, 5 insertions(+), 1 deletion(-) diff --git a/sat/sat.ml b/sat/sat.ml index 6c68d8e0..2a570338 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -71,7 +71,7 @@ module Make(Dummy : sig end) = struct type clause = SatSolver.St.clause type proof = SatSolver.Proof.proof - let tag_clause cl = SatSolver.St.(cl.tag) + let tag_clause = SatSolver.tag_clause type res = | Sat diff --git a/solver/solver.ml b/solver/solver.ml index c71e07c7..0915797d 100644 --- a/solver/solver.ml +++ b/solver/solver.ml @@ -101,5 +101,6 @@ module Make (E : Formula_intf.S) include S + let tag_clause cl = St.(cl.tag) end diff --git a/solver/solver.mli b/solver/solver.mli index 56bd14ad..aec7be1f 100644 --- a/solver/solver.mli +++ b/solver/solver.mli @@ -38,6 +38,9 @@ module Make (F : Formula_intf.S) Modifies the sat solver state in place. @raise Unsat if a conflict is detect when adding the clauses *) + val tag_clause : St.clause -> int option + (** Recover tag from a clause, if any *) + val eval : F.t -> bool (** Returns the valuation of a formula in the current state of the sat solver. *) From 60250f261194c1195315244365143f6ddc45cfc1 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 29 Jan 2016 17:00:05 +0100 Subject: [PATCH 2/2] add `UndecidedLit` for `eval, eval_level` --- sat/sat.ml | 1 + sat/sat.mli | 8 ++++++-- solver/internal.ml | 5 ++++- solver/internal.mli | 7 +++++-- solver/solver.mli | 7 +++++-- 5 files changed, 21 insertions(+), 7 deletions(-) diff --git a/sat/sat.ml b/sat/sat.ml index 2a570338..a8da48ad 100644 --- a/sat/sat.ml +++ b/sat/sat.ml @@ -66,6 +66,7 @@ module Make(Dummy : sig end) = struct module SatSolver = Solver.Make(Fsat)(Tsat) exception Bad_atom + exception UndecidedLit = SatSolver.UndecidedLit type atom = Fsat.t type clause = SatSolver.St.clause diff --git a/sat/sat.mli b/sat/sat.mli index 7f2f0a05..d766a9cc 100644 --- a/sat/sat.mli +++ b/sat/sat.mli @@ -11,6 +11,8 @@ module Tseitin : Tseitin.S with type atom = Fsat.t module Make(Dummy : sig end) : sig (** Fonctor to make a pure SAT Solver module with built-in literals. *) + exception UndecidedLit + exception Bad_atom (** Exception raised when a problem with atomic formula encoding is detected. *) @@ -55,13 +57,15 @@ module Make(Dummy : sig end) : sig (** Returns the satisfiability status of the current set of assumptions. *) val eval : atom -> bool - (** Return the current assignement of the literals. *) + (** Return the current assignement of the literal. + @raise UndecidedLit if the literal is not decided *) val eval_level : atom -> bool * int (** Return the current assignement of the literals, as well as its decision level. If the level is 0, then it is necessary for the atom to have this value; otherwise it is due to choices - that can potentially be backtracked. *) + that can potentially be backtracked. + @raise UndecidedLit if the literal is not decided *) val assume : ?tag:int -> atom list list -> unit (** Add a list of clauses to the set of assumptions. *) diff --git a/solver/internal.ml b/solver/internal.ml index b6a81f6b..4d727504 100644 --- a/solver/internal.ml +++ b/solver/internal.ml @@ -15,6 +15,7 @@ module Make exception Sat exception Unsat + exception UndecidedLit exception Restart exception Conflict of clause @@ -970,7 +971,9 @@ module Make let eval_level lit = let var, negated = make_boolean_var lit in - assert (var.pa.is_true || var.na.is_true); + if not var.pa.is_true && not var.na.is_true + then raise UndecidedLit + else assert (var.level >= 0); let truth = var.pa.is_true in let value = if negated then not truth else truth in value, var.level diff --git a/solver/internal.mli b/solver/internal.mli index ec8c16a7..c00f5eaf 100644 --- a/solver/internal.mli +++ b/solver/internal.mli @@ -13,6 +13,7 @@ module Make (** {2 Solving facilities} *) exception Unsat + exception UndecidedLit module Proof : Res.S with module St = St @@ -28,13 +29,15 @@ module Make val eval : St.formula -> bool (** Returns the valuation of a formula in the current state - of the sat solver. *) + of the sat solver. + @raise UndecidedLit if the literal is not decided *) val eval_level : St.formula -> bool * int (** Return the current assignement of the literals, as well as its decision level. If the level is 0, then it is necessary for the atom to have this value; otherwise it is due to choices - that can potentially be backtracked. *) + that can potentially be backtracked. + @raise UndecidedLit if the literal is not decided *) val hyps : unit -> St.clause Vec.t (** Returns the vector of assumptions used by the solver. May be slightly different diff --git a/solver/solver.mli b/solver/solver.mli index aec7be1f..6594ad63 100644 --- a/solver/solver.mli +++ b/solver/solver.mli @@ -21,6 +21,7 @@ module Make (F : Formula_intf.S) formulas and a theory. *) exception Unsat + exception UndecidedLit module St : Solver_types.S with type formula = F.t @@ -43,13 +44,15 @@ module Make (F : Formula_intf.S) val eval : F.t -> bool (** Returns the valuation of a formula in the current state - of the sat solver. *) + of the sat solver. + @raise UndecidedLit if the literal is not decided *) val eval_level : F.t -> bool * int (** Return the current assignement of the literals, as well as its decision level. If the level is 0, then it is necessary for the atom to have this value; otherwise it is due to choices - that can potentially be backtracked. *) + that can potentially be backtracked. + @raise UndecidedLit if the literal is not decided *) val hyps : unit -> St.clause Vec.t (** Returns the vector of assumptions used by the solver. May be slightly different