From d415f8ed2032fa50f460892832ddaddd47244a69 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 29 Dec 2017 18:29:56 +0100 Subject: [PATCH] do not expose `St` in solver, but only expose a restricted API. --- src/backend/Coq.ml | 48 +++++++------ src/backend/Coq.mli | 4 +- src/backend/Dedukti.ml | 12 ++-- src/backend/Dedukti.mli | 2 +- src/backend/Dot.ml | 22 +++--- src/backend/Dot.mli | 6 +- src/core/Internal.ml | 4 +- src/core/Internal.mli | 122 ---------------------------------- src/core/Res.ml | 22 +++--- src/core/Res.mli | 4 +- src/core/Res_intf.ml | 60 +++++++++++------ src/core/Solver.ml | 21 +++++- src/core/Solver.mli | 5 +- src/core/Solver_intf.ml | 60 ++++++++++++----- src/core/Solver_types.ml | 9 +++ src/core/Solver_types_intf.ml | 5 ++ src/main/main.ml | 2 +- src/mcsat/Minismt_mcsat.mli | 2 +- src/sat/Minismt_sat.mli | 2 +- src/smt/Minismt_smt.mli | 2 +- src/solver/mcsolver.mli | 6 +- src/solver/solver.mli | 4 +- 22 files changed, 196 insertions(+), 228 deletions(-) delete mode 100644 src/core/Internal.mli diff --git a/src/backend/Coq.ml b/src/backend/Coq.ml index f33f0a2c..adde1c05 100644 --- a/src/backend/Coq.ml +++ b/src/backend/Coq.ml @@ -22,11 +22,12 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause and type lemma := S.clause and type assumption := S.clause) = struct - module Atom = S.St.Atom - module Clause = S.St.Clause - module M = Map.Make(S.St.Atom) + module Atom = S.Atom + module Clause = S.Clause + module M = Map.Make(S.Atom) + module C_tbl = S.Clause.Tbl - let name = S.St.Clause.name + let name = Clause.name let clause_map c = let rec aux acc a i = @@ -36,11 +37,11 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause aux (M.add a.(i) name acc) a (i + 1) end in - aux M.empty c.S.St.atoms 0 + aux M.empty (Clause.atoms c) 0 let clause_iter m format fmt clause = let aux atom = Format.fprintf fmt format (M.find atom m) in - Array.iter aux clause.S.St.atoms + Array.iter aux (Clause.atoms clause) let elim_duplicate fmt goal hyp _ = (** Printing info comment in coq *) @@ -59,27 +60,30 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause if b == a then begin Format.fprintf fmt "@ (fun p =>@ %s%a)" (name h2) (fun fmt -> (Array.iter (fun c -> - if c == a.S.St.neg then + if Atom.equal c (Atom.neg a) then Format.fprintf fmt "@ (fun np => np p)" else Format.fprintf fmt "@ %s" (M.find c m))) - ) h2.S.St.atoms + ) (Clause.atoms h2) end else Format.fprintf fmt "@ %s" (M.find b m) - )) h1.S.St.atoms + )) (Clause.atoms h1) let resolution fmt goal hyp1 hyp2 atom = let a = Atom.abs atom in let h1, h2 = - if Array.exists (Atom.equal a) hyp1.S.St.atoms then hyp1, hyp2 - else (assert (Array.exists (Atom.equal a) hyp2.S.St.atoms); hyp2, hyp1) + if Array.exists (Atom.equal a) (Clause.atoms hyp1) then hyp1, hyp2 + else ( + assert (Array.exists (Atom.equal a) (Clause.atoms hyp2)); + hyp2, hyp1 + ) in (** Print some debug info *) Format.fprintf fmt "(* Clausal resolution. Goal : %s ; Hyps : %s, %s *)@\n" (name goal) (name h1) (name h2); (** Prove the goal: intro the axioms, then perform resolution *) - if Array.length goal.S.St.atoms = 0 then ( + if Array.length (Clause.atoms goal) = 0 then ( let m = M.empty in Format.fprintf fmt "exact @[(%a)@].@\n" (resolution_aux m a h1 h2) (); false @@ -92,13 +96,13 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause (* Count uses of hypotheses *) let incr_use h c = - let i = try S.H.find h c with Not_found -> 0 in - S.H.add h c (i + 1) + let i = try C_tbl.find h c with Not_found -> 0 in + C_tbl.add h c (i + 1) let decr_use h c = - let i = S.H.find h c - 1 in + let i = C_tbl.find h c - 1 in assert (i >= 0); - let () = S.H.add h c i in + let () = C_tbl.add h c i in i <= 0 let clear fmt c = @@ -136,7 +140,7 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause if resolution fmt clause c1 c2 a then clean t fmt [c1; c2] let count_uses p = - let h = S.H.create 4013 in + let h = C_tbl.create 128 in let aux () node = List.iter (fun p' -> incr_use h S.(conclusion p')) (S.parents node.S.step) in @@ -157,13 +161,13 @@ end module Simple(S : Res.S) - (A : Arg with type hyp = S.St.formula list + (A : Arg with type hyp = S.formula list and type lemma := S.lemma - and type assumption := S.St.formula) = + and type assumption := S.formula) = Make(S)(struct (* Some helpers *) - let lit a = a.S.St.lit + let lit = S.Atom.lit let get_assumption c = match S.to_list c with @@ -171,8 +175,8 @@ module Simple(S : Res.S) | _ -> assert false let get_lemma c = - match c.S.St.cpremise with - | S.St.Lemma p -> p + match S.expand (S.prove c) with + | {S.step=S.Lemma p; _} -> p | _ -> assert false let prove_hyp fmt name c = diff --git a/src/backend/Coq.mli b/src/backend/Coq.mli index 205319b6..ec743ff2 100644 --- a/src/backend/Coq.mli +++ b/src/backend/Coq.mli @@ -40,8 +40,8 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause (** Base functor to output Coq proofs *) -module Simple(S : Res.S)(A : Arg with type hyp = S.St.formula list +module Simple(S : Res.S)(A : Arg with type hyp = S.formula list and type lemma := S.lemma - and type assumption := S.St.formula) : S with type t := S.proof + and type assumption := S.formula) : S with type t := S.proof (** Simple functo to output Coq proofs *) diff --git a/src/backend/Dedukti.ml b/src/backend/Dedukti.ml index a4a842d1..1a13cb08 100644 --- a/src/backend/Dedukti.ml +++ b/src/backend/Dedukti.ml @@ -18,22 +18,24 @@ module type Arg = sig val context : Format.formatter -> proof -> unit end -module Make(S : Res.S)(A : Arg with type formula := S.St.formula and type lemma := S.lemma and type proof := S.proof) = struct +module Make(S : Res.S)(A : Arg with type formula := S.formula + and type lemma := S.lemma + and type proof := S.proof) = struct let pp_nl fmt = Format.fprintf fmt "@\n" let fprintf fmt format = Format.kfprintf pp_nl fmt format - let _clause_name c = S.St.(c.name) + let _clause_name = S.Clause.name let _pp_clause fmt c = let rec aux fmt = function | [] -> () | a :: r -> let f, pos = - if S.St.(a.var.pa == a) then - S.St.(a.lit), true + if S.Atom.is_pos a then + S.Atom.lit a, true else - S.St.(a.neg.lit), false + S.Atom.lit (S.Atom.neg a), false in fprintf fmt "%s _b %a ->@ %a" (if pos then "_pos" else "_neg") A.print f aux r diff --git a/src/backend/Dedukti.mli b/src/backend/Dedukti.mli index e24deb9a..826c8031 100644 --- a/src/backend/Dedukti.mli +++ b/src/backend/Dedukti.mli @@ -27,7 +27,7 @@ end module Make : functor(S : Res.S) -> functor(A : Arg - with type formula := S.St.formula + with type formula := S.formula and type lemma := S.lemma and type proof := S.proof) -> S with type t := S.proof diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml index 2fde8287..067046e7 100644 --- a/src/backend/Dot.ml +++ b/src/backend/Dot.ml @@ -31,8 +31,8 @@ module type Arg = sig end module Default(S : Res.S) = struct - module Atom = S.St.Atom - module Clause = S.St.Clause + module Atom = S.Atom + module Clause = S.Clause let print_atom = Atom.pp @@ -55,8 +55,8 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type hyp := S.clause and type lemma := S.clause and type assumption := S.clause) = struct - module Atom = S.St.Atom - module Clause = S.St.Clause + module Atom = S.Atom + module Clause = S.Clause let node_id n = Clause.name n.S.conclusion @@ -148,13 +148,13 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom end module Simple(S : Res.S) - (A : Arg with type atom := S.St.formula - and type hyp = S.St.formula list + (A : Arg with type atom := S.formula + and type hyp = S.formula list and type lemma := S.lemma - and type assumption = S.St.formula) = + and type assumption = S.formula) = Make(S)(struct - module Atom = S.St.Atom - module Clause = S.St.Clause + module Atom = S.Atom + module Clause = S.Clause (* Some helpers *) let lit = Atom.lit @@ -165,8 +165,8 @@ module Simple(S : Res.S) | _ -> assert false let get_lemma c = - match Clause.premise c with - | S.St.Lemma p -> p + match S.expand (S.prove c) with + | {S.step=S.Lemma p;_} -> p | _ -> assert false (* Actual functions *) diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli index 84cf048b..a3c9c787 100644 --- a/src/backend/Dot.mli +++ b/src/backend/Dot.mli @@ -61,10 +61,10 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom and type assumption := S.clause) : S with type t := S.proof (** Functor for making a module to export proofs to the DOT format. *) -module Simple(S : Res.S)(A : Arg with type atom := S.St.formula - and type hyp = S.St.formula list +module Simple(S : Res.S)(A : Arg with type atom := S.formula + and type hyp = S.formula list and type lemma := S.lemma - and type assumption = S.St.formula) : S with type t := S.proof + and type assumption = S.formula) : S with type t := S.proof (** Functor for making a module to export proofs to the DOT format. The substitution of the hyp type is non-destructive due to a restriction of destructive substitutions on earlier versions of ocaml. *) diff --git a/src/core/Internal.ml b/src/core/Internal.ml index dc8afd11..8b5e730b 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -228,7 +228,7 @@ module Make let l = Lit.make st.st t in insert_var_order st (E_lit l) - let new_atom st p = + let new_atom st (p:formula) : unit = let a = mk_atom st p in insert_var_order st (E_var a.var) @@ -294,7 +294,7 @@ module Make literals (which are the first two lits of the clause) are appropriate. Indeed, it is better to watch true literals, and then unassigned literals. Watching false literals should be a last resort, and come with constraints - (see add_clause). + (see {!add_clause}). *) exception Trivial diff --git a/src/core/Internal.mli b/src/core/Internal.mli deleted file mode 100644 index 6082470e..00000000 --- a/src/core/Internal.mli +++ /dev/null @@ -1,122 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** mSAT core - - This is the core of msat, containing the code doing the actual solving. - This module is based on mini-sat, and as such the solver heavily uses mutation, - which makes using it direclty kinda tricky (some exceptions can be raised - at surprising times, mutating is dangerous for maintaining invariants, etc...). -*) - -module Make - (St : Solver_types.S) - (Th : Plugin_intf.S with type term = St.term - and type formula = St.formula and type proof = St.proof) -: sig - (** Functor to create a solver parametrised by the atomic formulas and a theory. *) - - (** {2 Solving facilities} *) - - exception Unsat - exception UndecidedLit - - type t - (** Solver *) - - val create : ?size:[`Tiny|`Small|`Big] -> ?st:St.t -> unit -> t - - val st : t -> St.t - (** Underlying state *) - - val solve : t -> unit - (** Try and solves the current set of assumptions. - @return () if the current set of clauses is satisfiable - @raise Unsat if a toplevel conflict is found *) - - val assume : t -> ?tag:int -> St.formula list list -> unit - (** Add the list of clauses to the current set of assumptions. - Modifies the sat solver state in place. *) - - val new_lit : t -> St.term -> unit - (** Add a new litteral (i.e term) to the solver. This term will - be decided on at some point during solving, wether it appears - in clauses or not. *) - - val new_atom : t -> St.formula -> unit - (** Add a new atom (i.e propositional formula) to the solver. - This formula will be decided on at some point during solving, - wether it appears in clauses or not. *) - - val push : t -> unit - (** Create a decision level for local assumptions. - @raise Unsat if a conflict is detected in the current state. *) - - val pop : t -> unit - (** Pop a decision level for local assumptions. *) - - val local : t -> St.formula list -> unit - (** Add local assumptions - @param assumptions list of additional local assumptions to make, - removed after the callback returns a value *) - - (** {2 Propositional models} *) - - val eval : t -> St.formula -> bool - (** Returns the valuation of a formula in the current state - of the sat solver. - @raise UndecidedLit if the literal is not decided *) - - val eval_level : t -> 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. - @raise UndecidedLit if the literal is not decided *) - - val model : t -> (St.term * St.term) list - (** Returns the model found if the formula is satisfiable. *) - - val check : t -> bool - (** Check the satisfiability of the current model. Only has meaning - if the solver finished proof search and has returned [Sat]. *) - - (** {2 Proofs and Models} *) - - module Proof : Res.S with module St = St - - val unsat_conflict : t -> St.clause option - (** Returns the unsat clause found at the toplevel, if it exists (i.e if - [solve] has raised [Unsat]) *) - - val full_slice : t -> (St.term, St.formula, St.proof) Plugin_intf.slice - (** View the current state of the trail as a slice. Mainly useful when the - solver has reached a SAT conclusion. *) - - (** {2 Internal data} - These functions expose some internal data stored by the solver, as such - great care should be taken to ensure not to mess with the values returned. *) - - val trail : t -> St.trail_elt Vec.t - (** Returns the current trail. - *DO NOT MUTATE* *) - - val hyps : t -> St.clause Vec.t - (** Returns the vector of assumptions used by the solver. May be slightly different - from the clauses assumed because of top-level simplification of clauses. - *DO NOT MUTATE* *) - - val temp : t -> St.clause Vec.t - (** Returns the clauses coreesponding to the local assumptions. - All clauses in this vec are assured to be unit clauses. - *DO NOT MUTATE* *) - - val history : t -> St.clause Vec.t - (** Returns the history of learnt clauses, with no guarantees on order. - *DO NOT MUTATE* *) - -end - diff --git a/src/core/Res.ml b/src/core/Res.ml index 4fbde74c..0114dbb7 100644 --- a/src/core/Res.ml +++ b/src/core/Res.ml @@ -5,12 +5,13 @@ Copyright 2014 Simon Cruanes *) module type S = Res_intf.S +module type FULL = Res_intf.FULL module Make(St : Solver_types.S) = struct module St = St - (* Type definitions *) + type formula = St.formula type lemma = St.proof type clause = St.clause type atom = St.atom @@ -27,7 +28,8 @@ module Make(St : Solver_types.S) = struct let equal_atoms a b = St.(a.aid) = St.(b.aid) let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) - let print_clause = St.Clause.pp + module Clause = St.Clause + module Atom = St.Atom let merge = List.merge compare_atoms @@ -105,7 +107,7 @@ module Make(St : Solver_types.S) = struct in aux (c, d) - let prove conclusion = + let[@inline] prove conclusion = assert St.(conclusion.cpremise <> History []); conclusion @@ -259,13 +261,7 @@ module Make(St : Solver_types.S) = struct List.iter (fun c -> c.St.visited <- false) tmp; res - (* Iter on proofs *) - module H = Hashtbl.Make(struct - type t = clause - let hash cl = - Array.fold_left (fun i a -> Hashtbl.hash St.(a.aid, i)) 0 cl.St.atoms - let equal = (==) - end) + module Tbl = Clause.Tbl type task = | Enter of proof @@ -277,10 +273,10 @@ module Make(St : Solver_types.S) = struct match spop s with | None -> acc | Some (Leaving c) -> - H.add h c true; + Tbl.add h c true; fold_aux s h f (f acc (expand c)) | Some (Enter c) -> - if not (H.mem h c) then begin + if not (Tbl.mem h c) then begin Stack.push (Leaving c) s; let node = expand c in begin match node.step with @@ -295,7 +291,7 @@ module Make(St : Solver_types.S) = struct fold_aux s h f acc let fold f acc p = - let h = H.create 42 in + let h = Tbl.create 42 in let s = Stack.create () in Stack.push (Enter p) s; fold_aux s h f acc diff --git a/src/core/Res.mli b/src/core/Res.mli index a2c8bdc9..06b9c647 100644 --- a/src/core/Res.mli +++ b/src/core/Res.mli @@ -12,6 +12,8 @@ Copyright 2014 Simon Cruanes module type S = Res_intf.S (** Interface for a module manipulating resolution proofs. *) -module Make : functor (St : Solver_types.S) -> S with module St = St +module type FULL = Res_intf.FULL + +module Make : functor (St : Solver_types.S) -> FULL with module St = St (** Functor to create a module building proofs from a sat-solver unsat trace. *) diff --git a/src/core/Res_intf.ml b/src/core/Res_intf.ml index 772829e6..cdebd00b 100644 --- a/src/core/Res_intf.ml +++ b/src/core/Res_intf.ml @@ -6,25 +6,26 @@ Copyright 2014 Simon Cruanes (** Interface for proofs *) +type 'a printer = Format.formatter -> 'a -> unit + module type S = sig (** Signature for a module handling proof by resolution from sat solving traces *) - module St : Solver_types.S - (** Module defining atom and clauses *) - (** {3 Type declarations} *) exception Insuficient_hyps (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) - type atom = St.atom - type lemma = St.proof - type clause = St.clause + type formula + type atom + type lemma + type clause (** Abstract types for atoms, clauses and theory-specific lemmas *) type proof (** Lazy type for proof trees. Proofs are persistent objects, and can be extended to proof nodes using functions defined later. *) + and proof_node = { conclusion : clause; (** The conclusion of the proof *) step : step; (** The reasoning step used to prove the conclusion *) @@ -45,7 +46,6 @@ module type S = sig of the two given proofs. The atom on which to perform the resolution is also given. *) (** The type of reasoning steps allowed in a proof. *) - (** {3 Resolution helpers} *) val to_list : clause -> atom list @@ -73,7 +73,6 @@ module type S = sig val prove_atom : atom -> proof option (** Given an atom [a], returns a proof of the clause [\[a\]] if [a] is true at level 0 *) - (** {3 Proof Nodes} *) val is_leaf : step -> bool @@ -103,25 +102,46 @@ module type S = sig [f] on a proof node happens after the execution on the parents of the nodes. *) val unsat_core : proof -> clause list - (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof. - More efficient than using the [fold] function since it has access to the internal representation of proofs *) - + (** Returns the unsat_core of the given proof, i.e the lists of conclusions + of all leafs of the proof. + More efficient than using the [fold] function since it has + access to the internal representation of proofs *) (** {3 Misc} *) val check : proof -> unit (** Check the contents of a proof. Mainly for internal use *) - val print_clause : Format.formatter -> clause -> unit - (** A nice looking printer for clauses, which sort the atoms before printing. *) + module Clause : sig + type t = clause + val name : t -> string + val atoms : t -> atom array + val pp : t printer + (** A nice looking printer for clauses, which sort the atoms before printing. *) + module Tbl : Hashtbl.S with type key = t + end - (** {3 Unsafe} *) - - module H : Hashtbl.S with type key = clause - (** Hashtable over proofs. Uses the details of the internal representation - to achieve the best performances, however hashtables from this module - become invalid when solving is restarted, so they should only be live - during inspection of a single proof. *) + module Atom : sig + type t = atom + val is_pos : t -> bool + val neg : t -> t + val abs : t -> t + val compare : t -> t -> int + val equal : t -> t -> bool + val lit : t -> formula + val pp : t printer + end + module Tbl : Hashtbl.S with type key = proof +end + +module type FULL = sig + module St : Solver_types.S + (** Module defining atom and clauses *) + + include S with type atom = St.atom + and type lemma = St.proof + and type clause = St.clause + and type formula = St.formula end diff --git a/src/core/Solver.ml b/src/core/Solver.ml index 1a633694..cc64cfaf 100644 --- a/src/core/Solver.ml +++ b/src/core/Solver.ml @@ -23,11 +23,15 @@ module Make exception UndecidedLit = S.UndecidedLit + type formula = St.formula + type term = St.term type atom = St.formula + type clause = St.clause type t = S.t + type solver = t - let create = S.create + let[@inline] create ?size () = S.create ?size () (* Result type *) type res = @@ -78,6 +82,8 @@ module Make (* Wrappers around internal functions*) let assume = S.assume + let add_clause = S.add_clause + let solve (st:t) ?(assumptions=[]) () = try S.pop st; (* FIXME: what?! *) @@ -106,4 +112,17 @@ module Make let history = S.history st in let local = S.temp st in {hyps; history; local} + + module Clause = struct + include St.Clause + + let atoms c = St.Clause.atoms c |> Array.map (fun a -> a.St.lit) + + let make st ?tag l = + let l = List.map (S.mk_atom st) l in + St.Clause.make ?tag l St.Hyp + end + + module Formula = St.Formula + module Term = St.Term end diff --git a/src/core/Solver.mli b/src/core/Solver.mli index c46dc61c..3272a62b 100644 --- a/src/core/Solver.mli +++ b/src/core/Solver.mli @@ -18,7 +18,10 @@ module Make (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof) - : S with module St = St + : S with type term = St.term + and type formula = St.formula + and type clause = St.clause + and type Proof.lemma = St.proof (** Functor to make a safe external interface. *) diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index 21e2612e..ae98b8d0 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -45,6 +45,8 @@ type 'clause export = { } (** Export internal state *) +type 'a printer = Format.formatter -> 'a -> unit + (** The external interface implemented by safe solvers, such as the one created by the {!Solver.Make} and {!Mcsolver.Make} functors. *) module type S = sig @@ -52,30 +54,29 @@ module type S = sig These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT. *) - (* TODO: replace {!St} with explicit modules (Expr, Var, Lit, Elt,...) - with carefully picked interfaces *) - module St : Solver_types.S - (** WARNING: Very dangerous module that expose the internal representation used - by the solver. *) + type term (** user terms *) - module Proof : Res.S with module St = St + type formula (** user formulas *) + + type clause + + module Proof : Res.S with type clause = clause (** A module to manipulate proofs. *) type t (** Main solver type, containing all state *) - val create : ?size:[`Tiny|`Small|`Big] -> ?st:St.t -> unit -> t + val create : ?size:[`Tiny|`Small|`Big] -> unit -> t (** Create new solver *) - (* TODO: add size hint, callbacks, etc. *) (** {2 Types} *) - type atom = St.formula + type atom = formula (** The type of atoms given by the module argument for formulas *) type res = - | Sat of (St.term,St.formula) sat_state (** Returned when the solver reaches SAT *) - | Unsat of (St.clause,Proof.proof) unsat_state (** Returned when the solver reaches UNSAT *) + | Sat of (term,formula) sat_state (** Returned when the solver reaches SAT *) + | Unsat of (clause,Proof.proof) unsat_state (** Returned when the solver reaches UNSAT *) (** Result type for the solver *) exception UndecidedLit @@ -88,10 +89,13 @@ module type S = sig (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. *) + val add_clause : t -> clause -> unit + (** Lower level addition of clauses *) + val solve : t -> ?assumptions:atom list -> unit -> res (** Try and solves the current set of assumptions. *) - val new_lit : t -> St.term -> unit + val new_lit : t -> term -> unit (** Add a new litteral (i.e term) to the solver. This term will be decided on at some point during solving, wether it appears in clauses or not. *) @@ -101,16 +105,42 @@ module type S = sig This formula will be decided on at some point during solving, wether it appears in clauses or not. *) - val unsat_core : Proof.proof -> St.clause list + val unsat_core : Proof.proof -> clause list (** Returns the unsat core of a given proof. *) val true_at_level0 : t -> atom -> bool (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e. it must hold in all models *) - val get_tag : St.clause -> int option + val get_tag : clause -> int option (** Recover tag from a clause, if any *) - val export : t -> St.clause export + val export : t -> clause export + + (** {2 Re-export some functions} *) + + type solver = t + + module Clause : sig + type t = clause + + val atoms : t -> atom array + val tag : t -> int option + val equal : t -> t -> bool + + val make : solver -> ?tag:int -> atom list -> t + + val pp : t printer + end + + module Formula : sig + type t = formula + val pp : t printer + end + + module Term : sig + type t = term + val pp : t printer + end end diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml index 40f62928..a5663bcb 100644 --- a/src/core/Solver_types.ml +++ b/src/core/Solver_types.ml @@ -283,6 +283,7 @@ module McMake (E : Expr_intf.S) = struct let[@inline] abs a = a.var.pa let[@inline] lit a = a.lit let[@inline] equal a b = a == b + let[@inline] is_pos a = a == abs a let[@inline] compare a b = Pervasives.compare a.aid b.aid let[@inline] reason a = Var.reason a.var let[@inline] id a = a.aid @@ -408,8 +409,10 @@ module McMake (E : Expr_intf.S) = struct let empty = make [] (History []) let name = name_of_clause + let[@inline] equal c1 c2 = c1==c2 let[@inline] atoms c = c.atoms let[@inline] tag c = c.tag + let hash cl = Array.fold_left (fun i a -> Hashtbl.hash (a.aid, i)) 0 cl.atoms let[@inline] premise c = c.cpremise let[@inline] set_premise c p = c.cpremise <- p @@ -423,6 +426,12 @@ module McMake (E : Expr_intf.S) = struct let[@inline] activity c = c.activity let[@inline] set_activity c w = c.activity <- w + module Tbl = Hashtbl.Make(struct + type t = clause + let hash = hash + let equal = equal + end) + let pp fmt c = Format.fprintf fmt "%s : %a" (name c) Atom.pp_a c.atoms diff --git a/src/core/Solver_types_intf.ml b/src/core/Solver_types_intf.ml index 485316df..643bc06d 100644 --- a/src/core/Solver_types_intf.ml +++ b/src/core/Solver_types_intf.ml @@ -210,6 +210,7 @@ module type S = sig val abs : t -> t (** positive atom *) val neg : t -> t val id : t -> int + val is_pos : t -> bool (* positive atom? *) val is_true : t -> bool val is_false : t -> bool @@ -249,6 +250,8 @@ module type S = sig val dummy : t val name : t -> string + val equal : t -> t -> bool + val hash : t -> int val atoms : t -> Atom.t array val tag : t -> int option val premise : t -> premise @@ -270,6 +273,8 @@ module type S = sig val pp : t printer val pp_dimacs : t printer val debug : t printer + + module Tbl : Hashtbl.S with type key = t end module Trail_elt : sig diff --git a/src/main/main.ml b/src/main/main.ml index a8b2e18e..ed177afa 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -43,7 +43,7 @@ module Make let check_clause c = let l = List.map (function a -> Log.debugf 99 - (fun k -> k "Checking value of %a" S.St.Formula.pp a); + (fun k -> k "Checking value of %a" S.Formula.pp a); sat.Msat.eval a) c in List.exists (fun x -> x) l in diff --git a/src/mcsat/Minismt_mcsat.mli b/src/mcsat/Minismt_mcsat.mli index 1499f361..a6de15ae 100644 --- a/src/mcsat/Minismt_mcsat.mli +++ b/src/mcsat/Minismt_mcsat.mli @@ -4,5 +4,5 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -include Minismt.Solver.S with type St.formula = Minismt_smt.Expr.atom +include Minismt.Solver.S with type formula = Minismt_smt.Expr.atom diff --git a/src/sat/Minismt_sat.mli b/src/sat/Minismt_sat.mli index ffc5034f..9dbd63f1 100644 --- a/src/sat/Minismt_sat.mli +++ b/src/sat/Minismt_sat.mli @@ -12,6 +12,6 @@ Copyright 2016 Guillaume Bury module Expr = Expr_sat module Type = Type_sat -include Minismt.Solver.S with type St.formula = Expr.t +include Minismt.Solver.S with type formula = Expr.t (** A functor that can generate as many solvers as needed. *) diff --git a/src/smt/Minismt_smt.mli b/src/smt/Minismt_smt.mli index 4850929d..f81b5277 100644 --- a/src/smt/Minismt_smt.mli +++ b/src/smt/Minismt_smt.mli @@ -7,5 +7,5 @@ Copyright 2014 Simon Cruanes module Expr = Expr_smt module Type = Type_smt -include Minismt.Solver.S with type St.formula = Expr_smt.atom +include Minismt.Solver.S with type formula = Expr_smt.atom diff --git a/src/solver/mcsolver.mli b/src/solver/mcsolver.mli index 04727d35..51f05b8a 100644 --- a/src/solver/mcsolver.mli +++ b/src/solver/mcsolver.mli @@ -16,8 +16,8 @@ module Make (E : Expr_intf.S) (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) - : S with type St.term = E.Term.t - and type St.formula = E.Formula.t - and type St.proof = E.proof + : S with type term = E.Term.t + and type formula = E.Formula.t + and type Proof.lemma = E.proof (** Functor to create a solver parametrised by the atomic formulas and a theory. *) diff --git a/src/solver/solver.mli b/src/solver/solver.mli index fef0160e..77efd675 100644 --- a/src/solver/solver.mli +++ b/src/solver/solver.mli @@ -23,8 +23,8 @@ module DummyTheory(F : Formula_intf.S) : module Make (F : Formula_intf.S) (Th : Theory_intf.S with type formula = F.t and type proof = F.proof) - : S with type St.formula = F.t - and type St.proof = F.proof + : S with type formula = F.t + and type Proof.lemma = F.proof (** Functor to create a SMT Solver parametrised by the atomic formulas and a theory. *)