From 1655d09035a4f16a6c9ae08c65b3b2e11310b278 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 18 Jan 2019 22:38:15 -0600 Subject: [PATCH] refactor: simpler, cleaner functors --- src/backend/Coq.ml | 40 +- src/backend/Coq.mli | 7 +- src/backend/Dedukti.ml | 11 +- src/backend/Dedukti.mli | 4 +- src/backend/Dimacs.ml | 30 +- src/backend/Dimacs.mli | 8 +- src/backend/Dot.ml | 58 +-- src/backend/Dot.mli | 7 +- src/backend/dune | 2 +- src/core/Expr_intf.ml | 70 --- src/core/Formula_intf.ml | 50 -- src/core/Internal.ml | 944 +++++++++++++++++++++++++++++++--- src/core/Msat.ml | 24 +- src/core/Plugin_intf.ml | 128 ----- src/core/Res.ml | 302 ----------- src/core/Res.mli | 19 - src/core/Res_intf.ml | 136 ----- src/core/Solver.ml | 149 +----- src/core/Solver.mli | 26 +- src/core/Solver_intf.ml | 371 +++++++++++-- src/core/Solver_types.ml | 420 --------------- src/core/Solver_types.mli | 26 - src/core/Solver_types_intf.ml | 271 ---------- src/core/Theory_intf.ml | 83 --- src/main/main.ml | 4 +- src/sat/Expr_sat.ml | 7 +- src/sat/Expr_sat.mli | 2 +- src/sat/Msat_sat.ml | 4 +- src/sat/Msat_sat.mli | 2 +- tests/test_api.ml | 37 +- 30 files changed, 1342 insertions(+), 1900 deletions(-) delete mode 100644 src/core/Expr_intf.ml delete mode 100644 src/core/Formula_intf.ml delete mode 100644 src/core/Plugin_intf.ml delete mode 100644 src/core/Res.ml delete mode 100644 src/core/Res.mli delete mode 100644 src/core/Res_intf.ml delete mode 100644 src/core/Solver_types.ml delete mode 100644 src/core/Solver_types.mli delete mode 100644 src/core/Solver_types_intf.ml delete mode 100644 src/core/Theory_intf.ml diff --git a/src/backend/Coq.ml b/src/backend/Coq.ml index 7f536d67..865c1e72 100644 --- a/src/backend/Coq.ml +++ b/src/backend/Coq.ml @@ -2,7 +2,6 @@ MSAT is free software, using the Apache license, see file LICENSE Copyright 2015 Guillaume Bury *) -open Msat module type S = Backend_intf.S @@ -18,7 +17,7 @@ module type Arg = sig end -module Make(S : Res.S)(A : Arg with type hyp := S.clause +module Make(S : Msat.S)(A : Arg with type hyp := S.clause and type lemma := S.clause and type assumption := S.clause) = struct @@ -26,6 +25,7 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause module Clause = S.Clause module M = Map.Make(S.Atom) module C_tbl = S.Clause.Tbl + module P = S.Proof let name = Clause.name @@ -122,29 +122,29 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause Format.fprintf fmt "(* Clearing unused clauses *)@\n%a" clean_aux l' let prove_node t fmt node = - let clause = node.S.conclusion in - match node.S.step with - | S.Hypothesis -> + let clause = node.P.conclusion in + match node.P.step with + | P.Hypothesis -> A.prove_hyp fmt (name clause) clause - | S.Assumption -> + | P.Assumption -> A.prove_assumption fmt (name clause) clause - | S.Lemma _ -> + | P.Lemma _ -> A.prove_lemma fmt (name clause) clause - | S.Duplicate (p, l) -> - let c = S.conclusion p in + | P.Duplicate (p, l) -> + let c = P.conclusion p in let () = elim_duplicate fmt clause c l in clean t fmt [c] - | S.Resolution (p1, p2, a) -> - let c1 = S.conclusion p1 in - let c2 = S.conclusion p2 in + | P.Resolution (p1, p2, a) -> + let c1 = P.conclusion p1 in + let c2 = P.conclusion p2 in if resolution fmt clause c1 c2 a then clean t fmt [c1; c2] let count_uses p = 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) + List.iter (fun p' -> incr_use h P.(conclusion p')) (P.parents node.P.step) in - let () = S.fold aux () p in + let () = P.fold aux () p in h (* Here the main idea is to always try and have exactly @@ -155,19 +155,19 @@ module Make(S : Res.S)(A : Arg with type hyp := S.clause Format.fprintf fmt "%a" (prove_node h) node in Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n"; - S.fold aux () p - + P.fold aux () p end -module Simple(S : Res.S) +module Simple(S : Msat.S) (A : Arg with type hyp = S.formula list and type lemma := S.lemma and type assumption := S.formula) = Make(S)(struct + module P = S.Proof (* Some helpers *) - let lit = S.Atom.lit + let lit = S.Atom.formula let get_assumption c = match S.Clause.atoms_l c with @@ -175,8 +175,8 @@ module Simple(S : Res.S) | _ -> assert false let get_lemma c = - match S.expand (S.prove c) with - | {S.step=S.Lemma p; _} -> p + match P.expand (P.prove c) with + | {P.step=P.Lemma p; _} -> p | _ -> assert false let prove_hyp fmt name c = diff --git a/src/backend/Coq.mli b/src/backend/Coq.mli index ec743ff2..3d34f549 100644 --- a/src/backend/Coq.mli +++ b/src/backend/Coq.mli @@ -8,7 +8,6 @@ Copyright 2015 Guillaume Bury This module provides an easy way to produce coq scripts corresponding to the resolution proofs output by the sat solver. *) -open Msat module type S = Backend_intf.S (** Interface for exporting proofs. *) @@ -34,14 +33,14 @@ module type Arg = sig end -module Make(S : Res.S)(A : Arg with type hyp := S.clause +module Make(S : Msat.S)(A : Arg with type hyp := S.clause and type lemma := S.clause and type assumption := S.clause) : S with type t := S.proof (** Base functor to output Coq proofs *) -module Simple(S : Res.S)(A : Arg with type hyp = S.formula list +module Simple(S : Msat.S)(A : Arg with type hyp = S.formula list and type lemma := S.lemma and type assumption := S.formula) : S with type t := S.proof -(** Simple functo to output Coq proofs *) +(** Simple functor to output Coq proofs *) diff --git a/src/backend/Dedukti.ml b/src/backend/Dedukti.ml index 46aa96a3..7f8526eb 100644 --- a/src/backend/Dedukti.ml +++ b/src/backend/Dedukti.ml @@ -3,8 +3,6 @@ MSAT is free software, using the Apache license, see file LICENSE Copyright 2015 Guillaume Bury *) -open Msat - module type S = Backend_intf.S module type Arg = sig @@ -18,9 +16,10 @@ module type Arg = sig val context : Format.formatter -> proof -> unit end -module Make(S : Res.S)(A : Arg with type formula := S.formula +module Make(S : Msat.S)(A : Arg with type formula := S.formula and type lemma := S.lemma and type proof := S.proof) = struct + module P = S.Proof let pp_nl fmt = Format.fprintf fmt "@\n" let fprintf fmt format = Format.kfprintf pp_nl fmt format @@ -32,10 +31,10 @@ module Make(S : Res.S)(A : Arg with type formula := S.formula | [] -> () | a :: r -> let f, pos = - if S.Atom.is_pos a then - S.Atom.lit a, true + if S.Atom.sign a then + S.Atom.formula a, true else - S.Atom.lit (S.Atom.neg a), false + S.Atom.formula (S.Atom.neg a), false in fprintf fmt "%s _b %a ->@ %a" (if pos then "_pos" else "_neg") A.pp f aux r diff --git a/src/backend/Dedukti.mli b/src/backend/Dedukti.mli index bb15697c..ef7cc88e 100644 --- a/src/backend/Dedukti.mli +++ b/src/backend/Dedukti.mli @@ -9,8 +9,6 @@ Copyright 2014 Simon Cruanes Work in progress... *) -open Msat - module type S = Backend_intf.S module type Arg = sig @@ -25,7 +23,7 @@ module type Arg = sig end module Make : - functor(S : Res.S) -> + functor(S : Msat.S) -> functor(A : Arg with type formula := S.formula and type lemma := S.lemma diff --git a/src/backend/Dimacs.ml b/src/backend/Dimacs.ml index 3339175d..cb17851d 100644 --- a/src/backend/Dimacs.ml +++ b/src/backend/Dimacs.ml @@ -6,6 +6,11 @@ Copyright 2014 Simon Cruanes open Msat +module type ARG = sig + type clause + val lits : clause -> int list +end + module type S = sig type st @@ -29,15 +34,21 @@ module type S = sig end -module Make(St : Solver_types_intf.S) = struct +module Make(St : Msat.S)(A: ARG with type clause = St.clause) = struct type st = St.t + let pp_dimacs fmt c = + let lits = A.lits c in + List.iter (fun p -> Format.fprintf fmt "%d " p) lits; + Format.fprintf fmt "0" + + (* Dimacs & iCNF export *) let export_vec name fmt vec = - Format.fprintf fmt "c %s@,%a@," name (Vec.pp ~sep:"" St.Clause.pp_dimacs) vec + Format.fprintf fmt "c %s@,%a@," name (Vec.pp ~sep:"" pp_dimacs) vec let export_assumption fmt vec = - Format.fprintf fmt "c Local assumptions@,a %a@," St.Clause.pp_dimacs vec + Format.fprintf fmt "c Local assumptions@,a %a@," pp_dimacs vec let export_icnf_aux r name map_filter fmt vec = let aux fmt _ = @@ -45,14 +56,15 @@ module Make(St : Solver_types_intf.S) = struct let x = Vec.get vec i in match map_filter x with | None -> () - | Some _ -> Format.fprintf fmt "%a@," St.Clause.pp_dimacs (Vec.get vec i) + | Some _ -> Format.fprintf fmt "%a@," pp_dimacs (Vec.get vec i) done; r := Vec.size vec in Format.fprintf fmt "c %s@,%a" name aux vec + (* TODO let map_filter_learnt c = - match St.Clause.premise c with + match P.Clause.premise c with | St.Hyp | St.Local -> assert false | St.Lemma _ -> Some c | St.History l -> @@ -73,13 +85,17 @@ module Make(St : Solver_types_intf.S) = struct | Some d -> Vec.push lemmas d ) learnt; lemmas + *) let export st fmt ~hyps ~history ~local = + assert false + (* FIXME assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps); (* Learnt clauses, then filtered to only keep only the theory lemmas; all other learnt clauses should be logical consequences of the rest. *) let lemmas = filter_vec history in + let lemmas = history in (* Local assertions *) assert (Vec.for_all (fun c -> St.Local = St.Clause.premise c) local); (* Number of atoms and clauses *) @@ -90,12 +106,15 @@ module Make(St : Solver_types_intf.S) = struct (export_vec "Local assumptions") local (export_vec "Hypotheses") hyps (export_vec "Lemmas") lemmas + *) (* Refs to remember what portion of a problem has been printed *) let icnf_hyp = ref 0 let icnf_lemmas = ref 0 let export_icnf fmt ~hyps ~history ~local = + assert false + (* FIXME assert (Vec.for_all (fun c -> St.Clause.premise c = St.Hyp) hyps); let lemmas = history in (* Local assertions *) @@ -113,6 +132,7 @@ module Make(St : Solver_types_intf.S) = struct (export_icnf_aux icnf_hyp "Hypotheses" (fun x -> Some x)) hyps (export_icnf_aux icnf_lemmas "Lemmas" map_filter_learnt) lemmas export_assumption local + *) end diff --git a/src/backend/Dimacs.mli b/src/backend/Dimacs.mli index e829bebd..aada5010 100644 --- a/src/backend/Dimacs.mli +++ b/src/backend/Dimacs.mli @@ -12,6 +12,11 @@ Copyright 2014 Simon Cruanes open Msat +module type ARG = sig + type clause + val lits : clause -> int list +end + module type S = sig type st @@ -44,6 +49,7 @@ module type S = sig end -module Make(St: Solver_types_intf.S) : S with type clause := St.clause and type st = St.t +module Make(St: Msat.S)(A: ARG with type clause = St.clause) + : S with type clause := St.clause and type st = St.t (** Functor to create a module for exporting probems to the dimacs (& iCNF) formats. *) diff --git a/src/backend/Dot.ml b/src/backend/Dot.ml index 5a33f054..b00178a7 100644 --- a/src/backend/Dot.ml +++ b/src/backend/Dot.ml @@ -4,8 +4,6 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -open Msat - (** Output interface for the backend *) module type S = Backend_intf.S @@ -30,7 +28,7 @@ module type Arg = sig end -module Default(S : Res.S) = struct +module Default(S : Msat.S) = struct module Atom = S.Atom module Clause = S.Clause @@ -51,18 +49,19 @@ module Default(S : Res.S) = struct end (** Functor to provide dot printing *) -module Make(S : Res.S)(A : Arg with type atom := S.atom +module Make(S : Msat.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.Atom module Clause = S.Clause + module P = S.Proof - let node_id n = Clause.name n.S.conclusion + let node_id n = Clause.name n.P.conclusion let res_node_id n = (node_id n) ^ "_res" - let proof_id p = node_id (S.expand p) + let proof_id p = node_id (P.expand p) let print_clause fmt c = let v = Clause.atoms c in @@ -80,8 +79,8 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom Format.fprintf fmt "%s -> %s;@\n" j i let print_edges fmt n = - match S.(n.step) with - | S.Resolution (p1, p2, _) -> + match P.(n.step) with + | P.Resolution (p1, p2, _) -> print_edge fmt (res_node_id n) (proof_id p1); print_edge fmt (res_node_id n) (proof_id p2) | _ -> () @@ -109,29 +108,29 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom let ttify f c = fun fmt () -> f fmt c let print_contents fmt n = - match S.(n.step) with + match P.(n.step) with (* Leafs of the proof tree *) - | S.Hypothesis -> - let rule, color, l = A.hyp_info S.(n.conclusion) in + | P.Hypothesis -> + let rule, color, l = A.hyp_info P.(n.conclusion) in let color = match color with None -> "LIGHTBLUE" | Some c -> c in - print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l - | S.Assumption -> - let rule, color, l = A.assumption_info S.(n.conclusion) in + print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l + | P.Assumption -> + let rule, color, l = A.assumption_info P.(n.conclusion) in let color = match color with None -> "LIGHTBLUE" | Some c -> c in - print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l - | S.Lemma _ -> - let rule, color, l = A.lemma_info S.(n.conclusion) in + print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l + | P.Lemma _ -> + let rule, color, l = A.lemma_info P.(n.conclusion) in let color = match color with None -> "YELLOW" | Some c -> c in - print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l + print_dot_node fmt (node_id n) "LIGHTBLUE" P.(n.conclusion) rule color l (* Tree nodes *) - | S.Duplicate (p, l) -> - print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Duplicate" "GREY" + | P.Duplicate (p, l) -> + print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Duplicate" "GREY" ((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) :: List.map (ttify A.print_atom) l); - print_edge fmt (node_id n) (node_id (S.expand p)) - | S.Resolution (_, _, a) -> - print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY" + print_edge fmt (node_id n) (node_id (P.expand p)) + | P.Resolution (_, _, a) -> + print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Resolution" "GREY" [(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))]; print_dot_res_node fmt (res_node_id n) a; print_edge fmt (node_id n) (res_node_id n) @@ -142,12 +141,12 @@ module Make(S : Res.S)(A : Arg with type atom := S.atom let pp fmt p = Format.fprintf fmt "digraph proof {@\n"; - S.fold (fun () -> print_node fmt) () p; + P.fold (fun () -> print_node fmt) () p; Format.fprintf fmt "}@." end -module Simple(S : Res.S) +module Simple(S : Msat.S) (A : Arg with type atom := S.formula and type hyp = S.formula list and type lemma := S.lemma @@ -155,9 +154,10 @@ module Simple(S : Res.S) Make(S)(struct module Atom = S.Atom module Clause = S.Clause + module P = S.Proof (* Some helpers *) - let lit = Atom.lit + let lit = Atom.formula let get_assumption c = match S.Clause.atoms_l c with @@ -165,13 +165,13 @@ module Simple(S : Res.S) | _ -> assert false let get_lemma c = - match S.expand (S.prove c) with - | {S.step=S.Lemma p;_} -> p + match P.expand (P.prove c) with + | {P.step=P.Lemma p;_} -> p | _ -> assert false (* Actual functions *) let print_atom fmt a = - A.print_atom fmt (Atom.lit a) + A.print_atom fmt (lit a) let hyp_info c = A.hyp_info (List.map lit (S.Clause.atoms_l c)) diff --git a/src/backend/Dot.mli b/src/backend/Dot.mli index a3c9c787..70adffa1 100644 --- a/src/backend/Dot.mli +++ b/src/backend/Dot.mli @@ -9,7 +9,6 @@ Copyright 2014 Simon Cruanes This module provides functions to export proofs into the dot graph format. Graphs in dot format can be used to generates images using the graphviz tool. *) -open Msat module type S = Backend_intf.S (** Interface for exporting proofs. *) @@ -48,20 +47,20 @@ module type Arg = sig end -module Default(S : Res.S) : Arg with type atom := S.atom +module Default(S : Msat.S) : Arg with type atom := S.atom and type hyp := S.clause and type lemma := S.clause and type assumption := S.clause (** Provides a reasonnable default to instantiate the [Make] functor, assuming the original printing functions are compatible with DOT html labels. *) -module Make(S : Res.S)(A : Arg with type atom := S.atom +module Make(S : Msat.S)(A : Arg with type atom := S.atom and type hyp := S.clause and type lemma := S.clause 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.formula +module Simple(S : Msat.S)(A : Arg with type atom := S.formula and type hyp = S.formula list and type lemma := S.lemma and type assumption = S.formula) : S with type t := S.proof diff --git a/src/backend/dune b/src/backend/dune index d9a6c6de..7febb3bc 100644 --- a/src/backend/dune +++ b/src/backend/dune @@ -3,7 +3,7 @@ (public_name msat.backend) (synopsis "proof backends for msat") (libraries msat) - (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string) + (flags :standard -w +a-4-42-44-48-50-58-32-60@8 -warn-error -27 -color always -safe-string) (ocamlopt_flags :standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20) ) diff --git a/src/core/Expr_intf.ml b/src/core/Expr_intf.ml deleted file mode 100644 index 15f9fe99..00000000 --- a/src/core/Expr_intf.ml +++ /dev/null @@ -1,70 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Mcsat expressions - - This modules defines the required implementation of expressions for Mcsat. -*) - -type negated = Formula_intf.negated = - | Negated (** changed sign *) - | Same_sign (** kept sign *) -(** This type is used during the normalisation of formulas. - See {!val:Expr_intf.S.norm} for more details. *) - -module type S = sig - (** Signature of formulas that parametrises the Mcsat Solver Module. *) - - type proof - (** An abstract type for proofs *) - - module Term : sig - (** McSat Terms *) - - type t - (** The type of terms *) - - val equal : t -> t -> bool - (** Equality over terms. *) - - val hash : t -> int - (** Hashing function for terms. Should be such that two terms equal according - to {!val:Expr_intf.S.equal} have the same hash. *) - - val pp : Format.formatter -> t -> unit - (** Printing function used among other for debugging. *) - - end - - module Formula : sig - (** McSat formulas *) - - type t - (** The type of atomic formulas over terms. *) - - val equal : t -> t -> bool - (** Equality over formulas. *) - - val hash : t -> int - (** Hashing function for formulas. Should be such that two formulas equal according - to {!val:Expr_intf.S.equal} have the same hash. *) - - val pp : Format.formatter -> t -> unit - (** Printing function used among other thing for debugging. *) - - val neg : t -> t - (** Formula negation *) - - val norm : t -> t * negated - (** Returns a 'normalized' form of the formula, possibly negated - (in which case return [Negated]). - [norm] must be so that [a] and [neg a] normalise to the same formula, - but one returns [Negated] and the other [Same_sign]. *) - end - - -end - diff --git a/src/core/Formula_intf.ml b/src/core/Formula_intf.ml deleted file mode 100644 index 26226c91..00000000 --- a/src/core/Formula_intf.ml +++ /dev/null @@ -1,50 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** SMT formulas - - This module defines the required implementation of formulas for - an SMT solver. -*) - -type negated = - | Negated (** changed sign *) - | Same_sign (** kept sign *) -(** This type is used during the normalisation of formulas. - See {!val:Expr_intf.S.norm} for more details. *) - -module type S = sig - (** SMT formulas *) - - type t - (** The type of atomic formulas. *) - - type proof - (** An abstract type for proofs *) - - val equal : t -> t -> bool - (** Equality over formulas. *) - - val hash : t -> int - (** Hashing function for formulas. Should be such that two formulas equal according - to {!val:Expr_intf.S.equal} have the same hash. *) - - val pp : Format.formatter -> t -> unit - (** Printing function used among other thing for debugging. *) - - val neg : t -> t - (** Formula negation. Should be an involution, i.e. [equal a (neg neg a)] should - always hold. *) - - val norm : t -> t * negated - (** Returns a 'normalized' form of the formula, possibly negated - (in which case return [Negated]). This function is used to recognize - the link between a formula [a] and its negation [neg a], so the goal is - that [a] and [neg a] normalise to the same formula, - but one returns [Same_sign] and the other one returns [Negated] *) - -end - diff --git a/src/core/Internal.ml b/src/core/Internal.ml index e5bbddf9..42dfd0f0 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -4,28 +4,665 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -(* TODO: move solver types here *) +module type PLUGIN = sig + val mcsat : bool + (** Is this a mcsat plugin? *) -module Make - (St : Solver_types.S) - (Plugin : Plugin_intf.S with type term = St.term - and type formula = St.formula - and type proof = St.proof) + include Solver_intf.PLUGIN_MCSAT +end + +module Make(Plugin : PLUGIN) = struct - module Proof = Res.Make(St) + module Term = Plugin.Term + module Formula = Plugin.Formula - open St + type term = Term.t + type formula = Formula.t type theory = Plugin.t + type lemma = Plugin.proof + + (* MCSAT literal *) + type lit = { + lid : int; + term : term; + mutable l_level : int; + mutable l_idx: int; + mutable l_weight : float; + mutable assigned : term option; + } + + type var = { + vid : int; + pa : atom; + na : atom; + mutable v_fields : int; + mutable v_level : int; + mutable v_idx: int; (** position in heap *) + mutable v_weight : float; (** Weight (for the heap), tracking activity *) + mutable v_assignable: lit list option; + mutable reason : reason option; + } + + and atom = { + aid : int; + var : var; + neg : atom; + lit : formula; + mutable is_true : bool; + watched : clause Vec.t; + } + + and clause = { + name : int; + tag : int option; (* TODO remove *) + atoms : atom array; + mutable cpremise : premise; + mutable activity : float; + mutable attached : bool; (* TODO: use an int field *) + mutable visited : bool; + } + + and reason = + | Decision + | Bcp of clause + | Semantic + + (* TODO: remove, replace with user-provided proof trackng device? + for pure SAT, [reason] is sufficient *) + and premise = + | Hyp + | Local + | Lemma of lemma + | History of clause list + + type elt = + | E_lit of lit + | E_var of var + + type trail_elt = + | Lit of lit + | Atom of atom + + (* Constructors *) + module MF = Hashtbl.Make(Formula) + module MT = Hashtbl.Make(Term) + + type st = { + t_map: lit MT.t; + f_map: var MF.t; + vars: elt Vec.t; + mutable cpt_mk_var: int; + mutable cpt_mk_clause: int; + } + + let create_st ?(size=`Big) () : st = + let size_map = match size with + | `Tiny -> 8 + | `Small -> 16 + | `Big -> 4096 + in + { f_map = MF.create size_map; + t_map = MT.create size_map; + vars = Vec.create(); + cpt_mk_var = 0; + cpt_mk_clause = 0; + } + + let nb_elt st = Vec.size st.vars + let get_elt st i = Vec.get st.vars i + let iter_elt st f = Vec.iter f st.vars + + let name_of_clause c = match c.cpremise with + | Hyp -> "H" ^ string_of_int c.name + | Local -> "L" ^ string_of_int c.name + | Lemma _ -> "T" ^ string_of_int c.name + | History _ -> "C" ^ string_of_int c.name + + module Lit = struct + type t = lit + let[@inline] term l = l.term + let[@inline] level l = l.l_level + let[@inline] assigned l = l.assigned + let[@inline] weight l = l.l_weight + + let make (st:st) (t:term) : t = + try MT.find st.t_map t + with Not_found -> + let res = { + lid = st.cpt_mk_var; + term = t; + l_weight = 1.; + l_idx= -1; + l_level = -1; + assigned = None; + } in + st.cpt_mk_var <- st.cpt_mk_var + 1; + MT.add st.t_map t res; + Vec.push st.vars (E_lit res); + res + + let debug_assign fmt v = + match v.assigned with + | None -> + Format.fprintf fmt "" + | Some t -> + Format.fprintf fmt "@[@@%d->@ %a@]" v.l_level Term.pp t + + let pp out v = Term.pp out v.term + let debug out v = + Format.fprintf out "%d[%a][lit:@[%a@]]" + (v.lid+1) debug_assign v Term.pp v.term + end + + let seen_pos = 0b1 + let seen_neg = 0b10 + + module Var = struct + type t = var + let[@inline] level v = v.v_level + let[@inline] pos v = v.pa + let[@inline] neg v = v.na + let[@inline] reason v = v.reason + let[@inline] assignable v = v.v_assignable + let[@inline] weight v = v.v_weight + + let make (st:st) (t:formula) : var * Solver_intf.negated = + let lit, negated = Formula.norm t in + try + MF.find st.f_map lit, negated + with Not_found -> + let cpt_double = st.cpt_mk_var lsl 1 in + let rec var = + { vid = st.cpt_mk_var; + pa = pa; + na = na; + v_fields = 0; + v_level = -1; + v_idx= -1; + v_weight = 0.; + v_assignable = None; + reason = None; + } + and pa = + { var = var; + lit = lit; + watched = Vec.create(); + neg = na; + is_true = false; + aid = cpt_double (* aid = vid*2 *) } + and na = + { var = var; + lit = Formula.neg lit; + watched = Vec.create(); + neg = pa; + is_true = false; + 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; + Vec.push st.vars (E_var var); + var, negated + + (* Marking helpers *) + let[@inline] clear v = + v.v_fields <- 0 + + let[@inline] seen_both v = + (seen_pos land v.v_fields <> 0) && + (seen_neg land v.v_fields <> 0) + end + + module Atom = struct + type t = atom + let[@inline] level a = a.var.v_level + let[@inline] var a = a.var + let[@inline] neg a = a.neg + let[@inline] abs a = a.var.pa + let[@inline] formula a = a.lit + let[@inline] equal a b = a == b + let[@inline] sign a = a == abs a + let[@inline] hash a = Hashtbl.hash a.aid + 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 + let[@inline] is_true a = a.is_true + let[@inline] is_false a = a.neg.is_true + + let[@inline] seen a = + let pos = equal a (abs a) in + if pos + then (seen_pos land a.var.v_fields <> 0) + else (seen_neg land a.var.v_fields <> 0) + + let[@inline] mark a = + let pos = equal a (abs a) in + if pos then ( + a.var.v_fields <- seen_pos lor a.var.v_fields + ) else ( + a.var.v_fields <- seen_neg lor a.var.v_fields + ) + + let[@inline] make st lit = + let var, negated = Var.make st lit in + match negated with + | Solver_intf.Negated -> var.na + | Solver_intf.Same_sign -> var.pa + + let pp fmt a = Formula.pp fmt a.lit + + let pp_a fmt v = + if Array.length v = 0 then ( + Format.fprintf fmt "∅" + ) else ( + pp fmt v.(0); + if (Array.length v) > 1 then begin + for i = 1 to (Array.length v) - 1 do + Format.fprintf fmt " ∨ %a" pp v.(i) + done + end + ) + + (* Complete debug printing *) + let pp_sign a = if a == a.var.pa then "+" else "-" + + let debug_reason fmt = function + | n, _ when n < 0 -> + Format.fprintf fmt "%%" + | n, None -> + Format.fprintf fmt "%d" n + | n, Some Decision -> + Format.fprintf fmt "@@%d" n + | n, Some Bcp c -> + Format.fprintf fmt "->%d/%s" n (name_of_clause c) + | n, Some Semantic -> + Format.fprintf fmt "::%d" n + + let pp_level fmt a = + debug_reason fmt (a.var.v_level, a.var.reason) + + let debug_value fmt a = + if a.is_true then + Format.fprintf fmt "T%a" pp_level a + else if a.neg.is_true then + Format.fprintf fmt "F%a" pp_level a + else + Format.fprintf fmt "" + + let debug out a = + Format.fprintf out "%s%d[%a][atom:@[%a@]]" + (pp_sign a) (a.var.vid+1) debug_value a Formula.pp a.lit + + let debug_a out vec = + Array.iter (fun a -> Format.fprintf out "%a@ " debug a) vec + end + + (* Elements *) + module Elt = struct + type t = elt + let[@inline] of_lit l = E_lit l + let[@inline] of_var v = E_var v + + let[@inline] id = function + | E_lit l -> l.lid | E_var v -> v.vid + let[@inline] level = function + | E_lit l -> l.l_level | E_var v -> v.v_level + let[@inline] idx = function + | E_lit l -> l.l_idx | E_var v -> v.v_idx + let[@inline] weight = function + | E_lit l -> l.l_weight | E_var v -> v.v_weight + + let[@inline] set_level e lvl = match e with + | E_lit l -> l.l_level <- lvl | E_var v -> v.v_level <- lvl + let[@inline] set_idx e i = match e with + | E_lit l -> l.l_idx <- i | E_var v -> v.v_idx <- i + let[@inline] set_weight e w = match e with + | E_lit l -> l.l_weight <- w | E_var v -> v.v_weight <- w + end + + module Trail_elt = struct + type t = trail_elt + let[@inline] of_lit l = Lit l + let[@inline] of_atom a = Atom a + + let debug fmt = function + | Lit l -> Lit.debug fmt l + | Atom a -> Atom.debug fmt a + end + + module Clause = struct + type t = clause + + let make = + let n = ref 0 in + fun ?tag ali premise -> + let atoms = Array.of_list ali in + let name = !n in + incr n; + { name; + tag = tag; + atoms = atoms; + visited = false; + attached = false; + activity = 0.; + cpremise = premise} + + let empty = make [] (History []) + let name = name_of_clause + let[@inline] equal c1 c2 = c1==c2 + let[@inline] atoms c = c.atoms + let[@inline] atoms_l c = Array.to_list 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 + + let[@inline] visited c = c.visited + let[@inline] set_visited c b = c.visited <- b + + let[@inline] attached c = c.attached + let[@inline] set_attached c b = c.attached <- b + + 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 + + let debug_premise out = function + | Hyp -> Format.fprintf out "hyp" + | Local -> Format.fprintf out "local" + | Lemma _ -> Format.fprintf out "th_lemma" + | History v -> + List.iter (fun c -> Format.fprintf out "%s,@ " (name_of_clause c)) v + + let debug out ({atoms=arr; cpremise=cp;_}as c) = + Format.fprintf out "%s@[{@[%a@]}@ cpremise={@[%a@]}@]" + (name c) Atom.debug_a arr debug_premise cp + end + + module Proof = struct + exception Insuficient_hyps + exception Resolution_error of string + + type atom = Atom.t + type clause = Clause.t + type formula = Formula.t + type lemma = Plugin.proof + + let merge = List.merge Atom.compare + + let _c = ref 0 + let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c) + + (* Compute resolution of 2 clauses *) + let resolve l = + let rec aux resolved acc = function + | [] -> resolved, acc + | [a] -> resolved, a :: acc + | a :: b :: r -> + if Atom.equal a b then + aux resolved (a :: acc) r + else if Atom.equal a.neg b then + aux (a.var.pa :: resolved) acc r + else + aux resolved (a :: acc) (b :: r) + in + let resolved, new_clause = aux [] [] l in + resolved, List.rev new_clause + + (* Compute the set of doublons of a clause *) + let list c = List.sort Atom.compare (Array.to_list c.atoms) + + let analyze cl = + let rec aux duplicates free = function + | [] -> duplicates, free + | [ x ] -> duplicates, x :: free + | x :: ((y :: r) as l) -> + if x == y then + count duplicates (x :: free) x [y] r + else + aux duplicates (x :: free) l + and count duplicates free x acc = function + | (y :: r) when x == y -> + count duplicates free x (y :: acc) r + | l -> + aux (acc :: duplicates) free l + in + let doublons, acc = aux [] [] cl in + doublons, List.rev acc + + let to_list c = + let cl = list c in + let doublons, l = analyze cl in + let conflicts, _ = resolve l in + if doublons <> [] then + Log.debug 3 "Input clause has redundancies"; + if conflicts <> [] then + Log.debug 3 "Input clause is a tautology"; + cl + + (* Comparison of clauses *) + let cmp_cl c d = + let rec aux = function + | [], [] -> 0 + | a :: r, a' :: r' -> + begin match Atom.compare a a' with + | 0 -> aux (r, r') + | x -> x + end + | _ :: _ , [] -> -1 + | [], _ :: _ -> 1 + in + aux (c, d) + + let[@inline] prove conclusion = + assert (conclusion.cpremise <> History []); + conclusion + + let rec set_atom_proof a = + let aux acc b = + if Atom.equal a.neg b then acc + else set_atom_proof b :: acc + in + assert (a.var.v_level >= 0); + match (a.var.reason) with + | Some (Bcp c) -> + Log.debugf 5 (fun k->k "Analysing: @[%a@ %a@]" Atom.debug a Clause.debug c); + if Array.length c.atoms = 1 then ( + Log.debugf 5 (fun k -> k "Old reason: @[%a@]" Atom.debug a); + c + ) else ( + assert (a.neg.is_true); + let r = History (c :: (Array.fold_left aux [] c.atoms)) in + let c' = Clause.make [a.neg] r in + a.var.reason <- Some (Bcp c'); + Log.debugf 5 + (fun k -> k "New reason: @[%a@ %a@]" Atom.debug a Clause.debug c'); + c' + ) + | _ -> + Log.debugf 0 (fun k -> k "Error while proving atom %a" Atom.debug a); + raise (Resolution_error "Cannot prove atom") + + let prove_unsat conflict = + if Array.length conflict.atoms = 0 then conflict + else ( + Log.debugf 1 (fun k -> k "Proving unsat from: @[%a@]" Clause.debug conflict); + let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.atoms in + let res = Clause.make [] (History (conflict :: l)) in + Log.debugf 1 (fun k -> k "Proof found: @[%a@]" Clause.debug res); + res + ) + + let prove_atom a = + if (a.is_true && a.var.v_level = 0) then + Some (set_atom_proof a) + else + None + + (* Interface exposed *) + type t = clause + and proof_node = { + conclusion : clause; + step : step; + } + and step = + | Hypothesis + | Assumption + | Lemma of lemma + | Duplicate of t * atom list + | Resolution of t * t * atom + + let rec chain_res (c, cl) = function + | d :: r -> + Log.debugf 5 + (fun k -> k " Resolving clauses : @[%a@\n%a@]" Clause.debug c Clause.debug d); + let dl = to_list d in + begin match resolve (merge cl dl) with + | [ a ], l -> + begin match r with + | [] -> (l, c, d, a) + | _ -> + let new_clause = Clause.make l (History [c; d]) in + chain_res (new_clause, l) r + end + | _ -> + Log.debugf 5 + (fun k -> k "While resolving clauses:@[%a@\n%a@]" + Clause.debug c Clause.debug d); + raise (Resolution_error "Clause mismatch") + end + | _ -> + raise (Resolution_error "Bad history") + + let[@inline] conclusion (p:t) : clause = p + + let expand conclusion = + Log.debugf 5 (fun k -> k "Expanding : @[%a@]" Clause.debug conclusion); + match conclusion.cpremise with + | Lemma l -> + {conclusion; step = Lemma l; } + | Hyp -> + { conclusion; step = Hypothesis; } + | Local -> + { conclusion; step = Assumption; } + | History [] -> + Log.debugf 0 (fun k -> k "Empty history for clause: %a" Clause.debug conclusion); + raise (Resolution_error "Empty history") + | History [ c ] -> + let duplicates, res = analyze (list c) in + assert (cmp_cl res (list conclusion) = 0); + { conclusion; step = Duplicate (c, List.concat duplicates) } + | History ( c :: ([_] as r)) -> + let (l, c', d', a) = chain_res (c, to_list c) r in + assert (cmp_cl l (to_list conclusion) = 0); + { conclusion; step = Resolution (c', d', a); } + | History ( c :: r ) -> + let (l, c', d', a) = chain_res (c, to_list c) r in + conclusion.cpremise <- History [c'; d']; + assert (cmp_cl l (to_list conclusion) = 0); + { conclusion; step = Resolution (c', d', a); } + + (* Proof nodes manipulation *) + let is_leaf = function + | Hypothesis + | Assumption + | Lemma _ -> true + | Duplicate _ + | Resolution _ -> false + + let parents = function + | Hypothesis + | Assumption + | Lemma _ -> [] + | Duplicate (p, _) -> [p] + | Resolution (p, p', _) -> [p; p'] + + let expl = function + | Hypothesis -> "hypothesis" + | Assumption -> "assumption" + | Lemma _ -> "lemma" + | Duplicate _ -> "duplicate" + | Resolution _ -> "resolution" + + (* Compute unsat-core + TODO: replace visited bool by a int unique to each call + of unsat_core, so that the cleanup can be removed ? *) + let unsat_core proof = + let rec aux res acc = function + | [] -> res, acc + | c :: r -> + if not c.visited then ( + c.visited <- true; + match c.cpremise with + | Hyp | Local | Lemma _ -> aux (c :: res) acc r + | History h -> + let l = List.fold_left (fun acc c -> + if not c.visited then c :: acc else acc) r h in + aux res (c :: acc) l + ) else ( + aux res acc r + ) + in + let res, tmp = aux [] [] [proof] in + List.iter (fun c -> c.visited <- false) res; + List.iter (fun c -> c.visited <- false) tmp; + res + + module Tbl = Clause.Tbl + + type task = + | Enter of t + | Leaving of t + + let spop s = try Some (Stack.pop s) with Stack.Empty -> None + + let rec fold_aux s h f acc = + match spop s with + | None -> acc + | Some (Leaving c) -> + Tbl.add h c true; + fold_aux s h f (f acc (expand c)) + | Some (Enter c) -> + if not (Tbl.mem h c) then begin + Stack.push (Leaving c) s; + let node = expand c in + begin match node.step with + | Duplicate (p1, _) -> + Stack.push (Enter p1) s + | Resolution (p1, p2, _) -> + Stack.push (Enter p2) s; + Stack.push (Enter p1) s + | Hypothesis | Assumption | Lemma _ -> () + end + end; + fold_aux s h f acc + + let fold f acc p = + let h = Tbl.create 42 in + let s = Stack.create () in + Stack.push (Enter p) s; + fold_aux s h f acc + + let check p = fold (fun () _ -> ()) () p + end + type proof = Proof.t module H = (Heap.Make [@specialise]) (struct - type t = St.Elt.t + type t = Elt.t let[@inline] cmp i j = Elt.weight j < Elt.weight i (* comparison by weight *) let idx = Elt.idx let set_idx = Elt.set_idx end) - exception Sat - exception Unsat + exception E_sat + exception E_unsat exception UndecidedLit exception Restart exception Conflict of clause @@ -50,9 +687,8 @@ module Make (* Singleton type containing the current state *) type t = { - st : St.t; - - th: Plugin.t; + st : st; + th: theory; (* Clauses are simplified for eficiency purposes. In the following vectors, the comments actually refer to the original non-simplified @@ -62,6 +698,7 @@ module Make (* clauses added by the user *) clauses_learnt : clause Vec.t; (* learnt clauses (tautologies true at any time, whatever the user level) *) + (* TODO: remove, replace by vec of assumptions *) clauses_temp : clause Vec.t; (* Temp clauses, corresponding to the local assumptions. This vec is used only to have an efficient way to access the list of local assumptions. *) @@ -85,6 +722,7 @@ module Make th_levels : Plugin.level Vec.t; (* theory states corresponding to elt_levels *) + (* TODO: remove *) user_levels : int Vec.t; (* user levels in [clauses_temp] *) @@ -120,10 +758,12 @@ module Make (* initial limit for the number of learnt clauses, 1/3 of initial number of clauses by default *) + (* TODO: remove *) mutable dirty: bool; (* is there a [pop()] on top of the stack for examining current model/proof? *) } + type solver = t (* Starting environment. *) let create_ ~st (th:theory) : t = { @@ -158,7 +798,7 @@ module Make } let create ?(size=`Big) (th:theory) : t = - let st = St.create ~size () in + let st = create_st ~size () in create_ ~st th (* Misc functions *) @@ -186,16 +826,16 @@ module Make of subterms of each formula, so we have a field [v_assignable] directly in variables to do so. *) let iter_sub f v = - if St.mcsat then + if Plugin.mcsat then match v.v_assignable with | Some l -> List.iter f l | None -> assert false (* When we have a new literal, we need to first create the list of its subterms. *) - let mk_atom st (f:St.formula) : atom = + let mk_atom st (f:formula) : atom = let res = Atom.make st.st f in - if St.mcsat then ( + if Plugin.mcsat then ( begin match res.var.v_assignable with | Some _ -> () | None -> @@ -217,12 +857,13 @@ module Make *) let rec insert_var_order st (elt:elt) : unit = H.insert st.order elt; - begin match elt with + if Plugin.mcsat then ( + match elt with | E_lit _ -> () | E_var v -> insert_subterms_order st v - end + ) - and insert_subterms_order st (v:St.var) : unit = + and insert_subterms_order st (v:var) : unit = iter_sub (fun t -> insert_var_order st (Elt.of_lit t)) v (* Add new litterals/atoms on which to decide on, even if there is no @@ -233,9 +874,10 @@ module Make let l = Lit.make st.st t in insert_var_order st (E_lit l) - let new_atom st (p:formula) : unit = + let make_atom_ st (p:formula) : atom = let a = mk_atom st p in - insert_var_order st (E_var a.var) + insert_var_order st (E_var a.var); + a (* Rather than iterate over all the heap when we want to decrease all the variables/literals activity, we instead increase the value by which @@ -250,8 +892,8 @@ module Make let var_bump_activity_aux st v = v.v_weight <- v.v_weight +. st.var_incr; if v.v_weight > 1e100 then ( - for i = 0 to St.nb_elt st.st - 1 do - Elt.set_weight (St.get_elt st.st i) ((Elt.weight (St.get_elt st.st i)) *. 1e-100) + for i = 0 to nb_elt st.st - 1 do + Elt.set_weight (get_elt st.st i) ((Elt.weight (get_elt st.st i)) *. 1e-100) done; st.var_incr <- st.var_incr *. 1e-100; ); @@ -264,8 +906,8 @@ module Make let lit_bump_activity_aux st (l:lit): unit = l.l_weight <- l.l_weight +. st.var_incr; if l.l_weight > 1e100 then ( - for i = 0 to St.nb_elt st.st - 1 do - Elt.set_weight (St.get_elt st.st i) ((Elt.weight (St.get_elt st.st i)) *. 1e-100) + for i = 0 to nb_elt st.st - 1 do + Elt.set_weight (get_elt st.st i) ((Elt.weight (get_elt st.st i)) *. 1e-100) done; st.var_incr <- st.var_incr *. 1e-100; ); @@ -473,7 +1115,7 @@ module Make let report_unsat st confl : _ = Log.debugf info (fun k -> k "@[Unsat conflict: %a@]" Clause.debug confl); st.unsat_conflict <- Some confl; - raise Unsat + raise E_unsat (* Simplification of boolean propagation reasons. When doing boolean propagation *at level 0*, it can happen @@ -588,8 +1230,8 @@ module Make let th_eval st a : bool option = if a.is_true || a.neg.is_true then None else match Plugin.eval st.th a.lit with - | Plugin_intf.Unknown -> None - | Plugin_intf.Valued (b, l) -> + | Solver_intf.Unknown -> None + | Solver_intf.Valued (b, l) -> if l = [] then raise (Invalid_argument ( Format.asprintf "msat:core/internal.ml: %s" @@ -731,7 +1373,7 @@ module Make let[@inline] analyze st c_clause : conflict_res = analyze_sat st c_clause (* - if St.mcsat + if mcsat then analyze_mcsat c_clause else analyze_sat c_clause *) @@ -959,22 +1601,22 @@ module Make let slice_get st i = match Vec.get st.trail i with | Atom a -> - Plugin_intf.Lit a.lit + Solver_intf.Lit a.lit | Lit {term; assigned = Some v; _} -> - Plugin_intf.Assign (term, v) + Solver_intf.Assign (term, v) | Lit _ -> assert false - let slice_push st (l:formula list) (lemma:proof): unit = + let slice_push st (l:formula list) (lemma:lemma): unit = let atoms = List.rev_map (create_atom st) l in let c = Clause.make atoms (Lemma lemma) in Log.debugf info (fun k->k "Pushing clause %a" Clause.debug c); Stack.push c st.clauses_to_add let slice_propagate (st:t) f = function - | Plugin_intf.Eval l -> + | Solver_intf.Eval l -> let a = mk_atom st f in enqueue_semantic st a l - | Plugin_intf.Consequence (causes, proof) -> + | Solver_intf.Consequence (causes, proof) -> let l = List.rev_map (mk_atom st) causes in if List.for_all (fun a -> a.is_true) l then ( let p = mk_atom st f in @@ -991,8 +1633,8 @@ module Make invalid_arg "Msat.Internal.slice_propagate" ) - let current_slice st : (_,_,_) Plugin_intf.slice = { - Plugin_intf.start = st.th_head; + let current_slice st : (_,_,_) Solver_intf.slice = { + Solver_intf.start = st.th_head; length = Vec.size st.trail - st.th_head; get = slice_get st; push = slice_push st; @@ -1000,8 +1642,8 @@ module Make } (* full slice, for [if_sat] final check *) - let full_slice st : (_,_,_) Plugin_intf.slice = { - Plugin_intf.start = 0; + let full_slice st : (_,_,_) Solver_intf.slice = { + Solver_intf.start = 0; length = Vec.size st.trail; get = slice_get st; push = slice_push st; @@ -1020,9 +1662,9 @@ module Make let slice = current_slice st in st.th_head <- st.elt_head; (* catch up *) match Plugin.assume st.th slice with - | Plugin_intf.Sat -> + | Solver_intf.Th_sat -> propagate st - | Plugin_intf.Unsat (l, p) -> + | Solver_intf.Th_unsat (l, p) -> (* conflict *) let l = List.rev_map (create_atom st) l in (* Assert that the conflcit is indeeed a conflict *) @@ -1031,7 +1673,7 @@ module Make ); List.iter (fun a -> insert_var_order st (Elt.of_var a.var)) l; (* Create the clause and return it. *) - let c = St.Clause.make l (Lemma p) in + let c = Clause.make l (Lemma p) in Some c ) @@ -1072,14 +1714,20 @@ module Make if v.v_level >= 0 then ( assert (v.pa.is_true || v.na.is_true); pick_branch_lit st - ) else match Plugin.eval st.th atom.lit with - | Plugin_intf.Unknown -> + ) else if Plugin.mcsat then ( + match Plugin.eval st.th atom.lit with + | Solver_intf.Unknown -> new_decision_level st; let current_level = decision_level st in enqueue_bool st atom ~level:current_level Decision - | Plugin_intf.Valued (b, l) -> + | Solver_intf.Valued (b, l) -> let a = if b then atom else atom.neg in enqueue_semantic st a l + ) else ( + new_decision_level st; + let current_level = decision_level st in + enqueue_bool st atom ~level:current_level Decision + ) and pick_branch_lit st = match st.next_decision with @@ -1099,7 +1747,7 @@ module Make ) | E_var v -> pick_branch_aux st v.pa - | exception Not_found -> raise Sat + | exception Not_found -> raise E_sat end (* do some amount of search, until the number of conflicts or clause learnt @@ -1122,8 +1770,7 @@ module Make | None -> (* No Conflict *) assert (st.elt_head = Vec.size st.trail); assert (st.elt_head = st.th_head); - if Vec.size st.trail = St.nb_elt st.st - then raise Sat; + if Vec.size st.trail = nb_elt st.st then raise E_sat; if n_of_conflicts > 0 && !conflictC >= n_of_conflicts then ( Log.debug info "Restarting..."; cancel_until st (base_level st); @@ -1138,19 +1785,18 @@ module Make pick_branch_lit st done - let eval_level (st:t) lit = - let var, negated = Var.make st.st lit in - if not var.pa.is_true && not var.na.is_true - then raise UndecidedLit - else assert (var.v_level >= 0); - let truth = var.pa.is_true in - let value = match negated with - | Formula_intf.Negated -> not truth - | Formula_intf.Same_sign -> truth - in - value, var.v_level + let eval_level (_st:t) (a:atom) = + let lvl = a.var.v_level in + if Atom.is_true a then ( + assert (lvl >= 0); + true, lvl + ) else if Atom.is_false a then ( + false, lvl + ) else ( + raise UndecidedLit + ) - let eval st lit = fst (eval_level st lit) + let[@inline] eval st lit = fst @@ eval_level st lit let[@inline] unsat_conflict st = st.unsat_conflict @@ -1166,7 +1812,7 @@ module Make conflict is reached *) let solve (st:t) : unit = Log.debug 5 "solve"; - if is_unsat st then raise Unsat; + if is_unsat st then raise E_unsat; let n_of_conflicts = ref (to_float st.restart_first) in let n_of_learnts = ref ((to_float (nb_clauses st)) *. st.learntsize_factor) in try @@ -1177,20 +1823,20 @@ module Make | Restart -> n_of_conflicts := !n_of_conflicts *. restart_inc; n_of_learnts := !n_of_learnts *. learntsize_inc - | Sat -> + | E_sat -> assert (st.elt_head = Vec.size st.trail); begin match Plugin.if_sat st.th (full_slice st) with - | Plugin_intf.Sat -> () - | Plugin_intf.Unsat (l, p) -> + | Solver_intf.Th_sat -> () + | Solver_intf.Th_unsat (l, p) -> let atoms = List.rev_map (create_atom st) l in let c = Clause.make atoms (Lemma p) in Log.debugf info (fun k -> k "Theory conflict clause: %a" Clause.debug c); Stack.push c st.clauses_to_add end; - if Stack.is_empty st.clauses_to_add then raise Sat + if Stack.is_empty st.clauses_to_add then raise E_sat end done - with Sat -> () + with E_sat -> () let assume st ?tag cnf = List.iter @@ -1205,7 +1851,7 @@ module Make let push st : unit = Log.debug debug "Pushing a new user level"; match st.unsat_conflict with - | Some _ -> raise Unsat + | Some _ -> raise E_unsat | None -> cancel_until st (base_level st); Log.debugf debug @@ -1244,9 +1890,8 @@ module Make ) (* Add local hyps to the current decision level *) - let local (st:t) (l:_ list) : unit = - let aux lit = - let a = mk_atom st lit in + let local (st:t) (l:atom list) : unit = + let aux a = Log.debugf info (fun k-> k "Local assumption: @[%a@]" Atom.debug a); assert (decision_level st = base_level st); if not a.is_true then ( @@ -1313,6 +1958,159 @@ module Make let trail env = env.trail -end -[@@inline] + (* Result type *) + type res = + | Sat of (term,atom) Solver_intf.sat_state + | Unsat of (clause,Proof.t) Solver_intf.unsat_state + + let pp_all st lvl status = + Log.debugf lvl + (fun k -> k + "@[%s - Full resume:@,@[Trail:@\n%a@]@,\ + @[Temp:@\n%a@]@,@[Hyps:@\n%a@]@,@[Lemmas:@\n%a@]@,@]@." + status + (Vec.pp ~sep:"" Trail_elt.debug) (trail st) + (Vec.pp ~sep:"" Clause.debug) (temp st) + (Vec.pp ~sep:"" Clause.debug) (hyps st) + (Vec.pp ~sep:"" Clause.debug) (history st) + ) + + let mk_sat (st:t) : (_,_) Solver_intf.sat_state = + pp_all st 99 "SAT"; + let t = trail st in + let iter f f' = + Vec.iter (function + | Atom a -> f a + | Lit l -> f' l.term) + t + in + { Solver_intf. + eval = eval st; + eval_level = eval_level st; + iter_trail = iter; + model = (fun () -> model st); + } + + let mk_unsat (st:t) : (_,_) Solver_intf.unsat_state = + pp_all st 99 "UNSAT"; + let unsat_conflict () = + match unsat_conflict st with + | None -> assert false + | Some c -> c + in + let get_proof () = + let c = unsat_conflict () in + Proof.prove_unsat c + in + { Solver_intf.unsat_conflict; get_proof; } + + (* clean local state *) + let[@inline] cleanup_ (st:t) : unit = + if st.dirty then ( + pop st; (* reset *) + st.dirty <- false; + ) + + (* Wrappers around internal functions*) + let[@inline] assume st ?tag cls : unit = + cleanup_ st; + assume st ?tag cls + + let[@inline] add_clause st ?tag c : unit = + cleanup_ st; + let c = Clause.make ?tag c Hyp in + add_clause st c + + let solve (st:t) ?(assumptions=[]) () = + cleanup_ st; + try + push st; + st.dirty <- true; (* to call [pop] before any other action *) + local st assumptions; + solve st; + Sat (mk_sat st) + with E_unsat -> + Unsat (mk_unsat st) + + let[@inline] push st = + cleanup_ st; + push st + + let[@inline] pop st = + cleanup_ st; + pop st + + let unsat_core = Proof.unsat_core + + let true_at_level0 st a = + try + let b, lev = eval_level st a in + b && lev = 0 + with UndecidedLit -> false + + (* TODO: remove *) + let get_tag cl = cl.tag + + let[@inline] new_lit st t = + cleanup_ st; + new_lit st t + + let[@inline] make_atom st a = + cleanup_ st; + make_atom_ st a + + let export (st:t) : clause Solver_intf.export = + let hyps = hyps st in + let history = history st in + let local = temp st in + {Solver_intf.hyps; history; local} +end +[@@inline][@@specialise] + +module Make_cdcl_t(Plugin : Solver_intf.PLUGIN_CDCL_T) = + Make(struct + include Plugin + module Term = struct + type t = Solver_intf.void + let equal _ _ = assert false + let hash _ = assert false + let pp _ _ = assert false + end + let eval _ _ = Solver_intf.Unknown + let assign _ t = t + let mcsat = false + let iter_assignable _ _ _ = () + end) +[@@inline][@@specialise] + +module Make_mcsat(Plugin : Solver_intf.PLUGIN_MCSAT) = + Make(struct + include Plugin + let mcsat = true + end) +[@@inline][@@specialise] + +module Make_pure_sat(F: Solver_intf.FORMULA) = + Make(struct + module Formula = F + module Term = struct + type t = Solver_intf.void + let equal _ _ = true + let hash _ = 1 + let pp out _ = Format.pp_print_string out "()" + end + type t = unit + type proof = Solver_intf.void + type level = unit + let current_level () = () + let assume () _ = Solver_intf.Th_sat + let if_sat () _ = Solver_intf.Th_sat + let backtrack () _ = () + let eval () _ = Solver_intf.Unknown + let assign () t = t + let mcsat = false + let iter_assignable () _ _ = () + let mcsat = false + end) +[@@inline][@@specialise] diff --git a/src/core/Msat.ml b/src/core/Msat.ml index 6b15cf2f..1dd6b961 100644 --- a/src/core/Msat.ml +++ b/src/core/Msat.ml @@ -1,15 +1,15 @@ (** Main API *) -module Formula_intf = Formula_intf -module Plugin_intf = Plugin_intf -module Theory_intf = Theory_intf -module Expr_intf = Expr_intf -module Solver_types_intf = Solver_types_intf -module Res = Res +module Solver_intf = Solver_intf module type S = Solver_intf.S +module type FORMULA = Solver_intf.FORMULA +module type EXPR = Solver_intf.EXPR +module type PLUGIN_CDCL_T = Solver_intf.PLUGIN_CDCL_T +module type PLUGIN_MCSAT = Solver_intf.PLUGIN_MCSAT +module type PROOF = Solver_intf.PROOF type ('term, 'form) sat_state = ('term, 'form) Solver_intf.sat_state = { eval : 'form -> bool; @@ -27,13 +27,15 @@ type 'clause export = 'clause Solver_intf.export = { history : 'clause Vec.t; local : 'clause Vec.t; } +type ('formula, 'proof) th_res = ('formula, 'proof) Solver_intf.th_res = + | Th_sat + | Th_unsat of 'formula list * 'proof -module Make_smt_expr(E : Formula_intf.S) = Solver_types.SatMake(E) -module Make_mcsat_expr(E : Expr_intf.S) = Solver_types.McMake(E) +type negated = Solver_intf.negated = Negated | Same_sign -module Make = Solver.Make - -module Make_dummy = Plugin_intf.Dummy +module Make_mcsat = Solver.Make_mcsat +module Make_cdcl_t = Solver.Make_cdcl_t +module Make_pure_sat = Solver.Make_pure_sat (**/**) module Vec = Vec diff --git a/src/core/Plugin_intf.ml b/src/core/Plugin_intf.ml deleted file mode 100644 index 98e87f53..00000000 --- a/src/core/Plugin_intf.ml +++ /dev/null @@ -1,128 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -Copyright 2016 Simon Cruanes -*) - -(** McSat Theory - - This module defines what a theory must implement in order to - be sued in a McSat solver. -*) - -type 'term eval_res = - | Unknown (** The given formula does not have an evaluation *) - | Valued of bool * ('term list) (** The given formula can be evaluated to the given bool. - The list of terms to give is the list of terms that - were effectively used for the evaluation. *) -(** The type of evaluation results for a given formula. - For instance, let's suppose we want to evaluate the formula [x * y = 0], the - following result are correct: - - [Unknown] if neither [x] nor [y] are assigned to a value - - [Valued (true, [x])] if [x] is assigned to [0] - - [Valued (true, [y])] if [y] is assigned to [0] - - [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number) -*) - -type ('formula, 'proof) res = - | Sat - (** The current set of assumptions is satisfiable. *) - | Unsat of 'formula list * 'proof - (** The current set of assumptions is *NOT* satisfiable, and here is a - theory tautology (with its proof), for which every litteral is false - under the current assumptions. *) -(** Type returned by the theory. Formulas in the unsat clause must come from the - current set of assumptions, i.e must have been encountered in a slice. *) - -type ('term, 'formula) assumption = - | Lit of 'formula (** The given formula is asserted true by the solver *) - | Assign of 'term * 'term (** The first term is assigned to the second *) -(** Asusmptions made by the core SAT solver. *) - -type ('term, 'formula, 'proof) reason = - | Eval of 'term list (** The formula can be evalutaed using the terms in the list *) - | Consequence of 'formula list * 'proof (** [Consequence (l, p)] means that the formulas in [l] imply - the propagated formula [f]. The proof should be a proof of - the clause "[l] implies [f]". *) -(** The type of reasons for propagations of a formula [f]. *) - -type ('term, 'formula, 'proof) slice = { - start : int; (** Start of the slice *) - length : int; (** Length of the slice *) - get : int -> ('term, 'formula) assumption; (** Accessor for the assertions in the slice. - Should only be called on integers [i] s.t. - [start <= i < start + length] *) - push : 'formula list -> 'proof -> unit; (** Add a clause to the solver. *) - propagate : 'formula -> - ('term, 'formula, 'proof) reason -> unit; (** Propagate a formula, i.e. the theory can - evaluate the formula to be true (see the - definition of {!type:eval_res} *) -} -(** The type for a slice of assertions to assume/propagate in the theory. *) - -(** Signature for theories to be given to the Model Constructing Solver. *) -module type S = sig - - type t - (** The plugin state itself *) - - type term - (** The type of terms. Should be compatible with Expr_intf.Term.t*) - - type formula - (** The type of formulas. Should be compatble with Expr_intf.Formula.t *) - - type proof - (** A custom type for the proofs of lemmas produced by the theory. *) - - type level - (** The type for levels to allow backtracking. *) - - val current_level : t -> level - (** Return the current level of the theory (either the empty/beginning state, or the - last level returned by the [assume] function). *) - - val assume : t -> (term, formula, proof) slice -> (formula, proof) res - (** Assume the formulas in the slice, possibly pushing new formulas to be propagated, - and returns the result of the new assumptions. *) - - val if_sat : t -> (term, formula, proof) slice -> (formula, proof) res - (** Called at the end of the search in case a model has been found. If no new clause is - pushed and the function returns [Sat], then proof search ends and 'sat' is returned, - else search is resumed. *) - - val backtrack : t -> level -> unit - (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the - same state as when it returned the value [l], *) - - val assign : t -> term -> term - (** Returns an assignment value for the given term. *) - - val iter_assignable : t -> (term -> unit) -> formula -> unit - (** An iterator over the subterms of a formula that should be assigned a value (usually the poure subterms) *) - - val eval : t -> formula -> term eval_res - (** Returns the evaluation of the formula in the current assignment *) - -end - -module Dummy(F: Solver_types.S) - : S with type formula = F.formula - and type term = F.term - and type proof = F.proof - and type t = unit -= struct - type t = unit - type formula = F.formula - type term = F.term - type proof = F.proof - type level = unit - let current_level () = () - let assume () _ = Sat - let if_sat () _ = Sat - let backtrack () _ = () - let eval () _ = Unknown - let assign () t = t - let mcsat = false - let iter_assignable () _ _ = () -end diff --git a/src/core/Res.ml b/src/core/Res.ml deleted file mode 100644 index 0114dbb7..00000000 --- a/src/core/Res.ml +++ /dev/null @@ -1,302 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -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 formula = St.formula - type lemma = St.proof - type clause = St.clause - type atom = St.atom - - exception Insuficient_hyps - exception Resolution_error of string - - (* Log levels *) - let error = 1 - let warn = 3 - let info = 10 - let debug = 80 - - let equal_atoms a b = St.(a.aid) = St.(b.aid) - let compare_atoms a b = Pervasives.compare St.(a.aid) St.(b.aid) - - module Clause = St.Clause - module Atom = St.Atom - - let merge = List.merge compare_atoms - - let _c = ref 0 - let fresh_pcl_name () = incr _c; "R" ^ (string_of_int !_c) - - (* Compute resolution of 2 clauses *) - let resolve l = - let rec aux resolved acc = function - | [] -> resolved, acc - | [a] -> resolved, a :: acc - | a :: b :: r -> - if equal_atoms a b then - aux resolved (a :: acc) r - else if equal_atoms St.(a.neg) b then - aux (St.(a.var.pa) :: resolved) acc r - else - aux resolved (a :: acc) (b :: r) - in - let resolved, new_clause = aux [] [] l in - resolved, List.rev new_clause - - (* Compute the set of doublons of a clause *) - let list c = List.sort St.Atom.compare (Array.to_list St.(c.atoms)) - - let analyze cl = - let rec aux duplicates free = function - | [] -> duplicates, free - | [ x ] -> duplicates, x :: free - | x :: ((y :: r) as l) -> - if x == y then - count duplicates (x :: free) x [y] r - else - aux duplicates (x :: free) l - and count duplicates free x acc = function - | (y :: r) when x == y -> - count duplicates free x (y :: acc) r - | l -> - aux (acc :: duplicates) free l - in - let doublons, acc = aux [] [] cl in - doublons, List.rev acc - - let to_list c = - let cl = list c in - let doublons, l = analyze cl in - let conflicts, _ = resolve l in - if doublons <> [] then - Log.debug warn "Input clause has redundancies"; - if conflicts <> [] then - Log.debug warn "Input clause is a tautology"; - cl - - (* - let pp_cl fmt l = - let rec aux fmt = function - | [] -> () - | a :: r -> - Format.fprintf fmt "%a@,%a" St.pp_atom a aux r - in - Format.fprintf fmt "@[%a@]" aux l - *) - - (* Comparison of clauses *) - let cmp_cl c d = - let rec aux = function - | [], [] -> 0 - | a :: r, a' :: r' -> - begin match compare_atoms a a' with - | 0 -> aux (r, r') - | x -> x - end - | _ :: _ , [] -> -1 - | [], _ :: _ -> 1 - in - aux (c, d) - - let[@inline] prove conclusion = - assert St.(conclusion.cpremise <> History []); - conclusion - - let rec set_atom_proof a = - let aux acc b = - if equal_atoms a.St.neg b then acc - else set_atom_proof b :: acc - in - assert St.(a.var.v_level >= 0); - match St.(a.var.reason) with - | Some St.Bcp c -> - Log.debugf debug (fun k->k "Analysing: @[%a@ %a@]" St.Atom.debug a St.Clause.debug c); - if Array.length c.St.atoms = 1 then ( - Log.debugf debug (fun k -> k "Old reason: @[%a@]" St.Atom.debug a); - c - ) else ( - assert (a.St.neg.St.is_true); - let r = St.History (c :: (Array.fold_left aux [] c.St.atoms)) in - let c' = St.Clause.make [a.St.neg] r in - a.St.var.St.reason <- Some St.(Bcp c'); - Log.debugf debug - (fun k -> k "New reason: @[%a@ %a@]" St.Atom.debug a St.Clause.debug c'); - c' - ) - | _ -> - Log.debugf error (fun k -> k "Error while proving atom %a" St.Atom.debug a); - raise (Resolution_error "Cannot prove atom") - - let prove_unsat conflict = - if Array.length conflict.St.atoms = 0 then conflict - else ( - Log.debugf info (fun k -> k "Proving unsat from: @[%a@]" St.Clause.debug conflict); - let l = Array.fold_left (fun acc a -> set_atom_proof a :: acc) [] conflict.St.atoms in - let res = St.Clause.make [] (St.History (conflict :: l)) in - Log.debugf info (fun k -> k "Proof found: @[%a@]" St.Clause.debug res); - res - ) - - let prove_atom a = - if St.(a.is_true && a.var.v_level = 0) then - Some (set_atom_proof a) - else - None - - (* Interface exposed *) - type proof = clause - and proof_node = { - conclusion : clause; - step : step; - } - and step = - | Hypothesis - | Assumption - | Lemma of lemma - | Duplicate of proof * atom list - | Resolution of proof * proof * atom - - let rec chain_res (c, cl) = function - | d :: r -> - Log.debugf debug - (fun k -> k " Resolving clauses : @[%a@\n%a@]" St.Clause.debug c St.Clause.debug d); - let dl = to_list d in - begin match resolve (merge cl dl) with - | [ a ], l -> - begin match r with - | [] -> (l, c, d, a) - | _ -> - let new_clause = St.Clause.make l (St.History [c; d]) in - chain_res (new_clause, l) r - end - | _ -> - Log.debugf error - (fun k -> k "While resolving clauses:@[%a@\n%a@]" - St.Clause.debug c St.Clause.debug d); - raise (Resolution_error "Clause mismatch") - end - | _ -> - raise (Resolution_error "Bad history") - - let[@inline] conclusion (p:proof) : clause = p - - let expand conclusion = - Log.debugf debug (fun k -> k "Expanding : @[%a@]" St.Clause.debug conclusion); - match conclusion.St.cpremise with - | St.Lemma l -> - {conclusion; step = Lemma l; } - | St.Hyp -> - { conclusion; step = Hypothesis; } - | St.Local -> - { conclusion; step = Assumption; } - | St.History [] -> - Log.debugf error (fun k -> k "Empty history for clause: %a" St.Clause.debug conclusion); - raise (Resolution_error "Empty history") - | St.History [ c ] -> - let duplicates, res = analyze (list c) in - assert (cmp_cl res (list conclusion) = 0); - { conclusion; step = Duplicate (c, List.concat duplicates) } - | St.History ( c :: ([_] as r)) -> - let (l, c', d', a) = chain_res (c, to_list c) r in - assert (cmp_cl l (to_list conclusion) = 0); - { conclusion; step = Resolution (c', d', a); } - | St.History ( c :: r ) -> - let (l, c', d', a) = chain_res (c, to_list c) r in - conclusion.St.cpremise <- St.History [c'; d']; - assert (cmp_cl l (to_list conclusion) = 0); - { conclusion; step = Resolution (c', d', a); } - - (* Proof nodes manipulation *) - let is_leaf = function - | Hypothesis - | Assumption - | Lemma _ -> true - | Duplicate _ - | Resolution _ -> false - - let parents = function - | Hypothesis - | Assumption - | Lemma _ -> [] - | Duplicate (p, _) -> [p] - | Resolution (p, p', _) -> [p; p'] - - let expl = function - | Hypothesis -> "hypothesis" - | Assumption -> "assumption" - | Lemma _ -> "lemma" - | Duplicate _ -> "duplicate" - | Resolution _ -> "resolution" - - (* Compute unsat-core - TODO: replace visited bool by a int unique to each call - of unsat_core, so that the cleanup can be removed ? *) - let unsat_core proof = - let rec aux res acc = function - | [] -> res, acc - | c :: r -> - if not c.St.visited then ( - c.St.visited <- true; - match c.St.cpremise with - | St.Hyp | St.Local | St.Lemma _ -> aux (c :: res) acc r - | St.History h -> - let l = List.fold_left (fun acc c -> - if not c.St.visited then c :: acc else acc) r h in - aux res (c :: acc) l - ) else ( - aux res acc r - ) - in - let res, tmp = aux [] [] [proof] in - List.iter (fun c -> c.St.visited <- false) res; - List.iter (fun c -> c.St.visited <- false) tmp; - res - - module Tbl = Clause.Tbl - - type task = - | Enter of proof - | Leaving of proof - - let spop s = try Some (Stack.pop s) with Stack.Empty -> None - - let rec fold_aux s h f acc = - match spop s with - | None -> acc - | Some (Leaving c) -> - Tbl.add h c true; - fold_aux s h f (f acc (expand c)) - | Some (Enter c) -> - if not (Tbl.mem h c) then begin - Stack.push (Leaving c) s; - let node = expand c in - begin match node.step with - | Duplicate (p1, _) -> - Stack.push (Enter p1) s - | Resolution (p1, p2, _) -> - Stack.push (Enter p2) s; - Stack.push (Enter p1) s - | Hypothesis | Assumption | Lemma _ -> () - end - end; - fold_aux s h f acc - - let fold f acc p = - let h = Tbl.create 42 in - let s = Stack.create () in - Stack.push (Enter p) s; - fold_aux s h f acc - - let check p = fold (fun () _ -> ()) () p - -end - diff --git a/src/core/Res.mli b/src/core/Res.mli deleted file mode 100644 index 06b9c647..00000000 --- a/src/core/Res.mli +++ /dev/null @@ -1,19 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Resolution proofs - - This modules defines functions to create and manipulate resolution proofs. -*) - -module type S = Res_intf.S -(** Interface for a module manipulating resolution proofs. *) - -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 deleted file mode 100644 index 2106a3bc..00000000 --- a/src/core/Res_intf.ml +++ /dev/null @@ -1,136 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -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 *) - - (** {3 Type declarations} *) - - exception Insuficient_hyps - (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) - - 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 *) - } - (** A proof can be expanded into a proof node, which show the first step of the proof. *) - - (** The type of reasoning steps allowed in a proof. *) - and step = - | Hypothesis - (** The conclusion is a user-provided hypothesis *) - | Assumption - (** The conclusion has been locally assumed by the user *) - | Lemma of lemma - (** The conclusion is a tautology provided by the theory, with associated proof *) - | Duplicate of proof * atom list - (** The conclusion is obtained by eliminating multiple occurences of the atom in - the conclusion of the provided proof. *) - | Resolution of proof * proof * atom - (** The conclusion can be deduced by performing a resolution between the conclusions - of the two given proofs. The atom on which to perform the resolution is also given. *) - - (** {3 Proof building functions} *) - - val prove : clause -> proof - (** Given a clause, return a proof of that clause. - @raise Insuficient_hyps if it does not succeed. *) - - val prove_unsat : clause -> proof - (** Given a conflict clause [c], returns a proof of the empty clause. - @raise Insuficient_hyps if it does not succeed. *) - - 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 parents : step -> proof list - (** Returns the parents of a proof node. *) - - val is_leaf : step -> bool - (** Returns wether the the proof node is a leaf, i.e. an hypothesis, - an assumption, or a lemma. - [true] if and only if {!parents} returns the empty list. *) - - val expl : step -> string - (** Returns a short string description for the proof step; for instance - ["hypothesis"] for a [Hypothesis] - (it currently returns the variant name in lowercase). *) - - - (** {3 Proof Manipulation} *) - - val expand : proof -> proof_node - (** Return the proof step at the root of a given proof. *) - - val conclusion : proof -> clause - (** What is proved at the root of the clause *) - - val fold : ('a -> proof_node -> 'a) -> 'a -> proof -> 'a - (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that - [f] is executed exactly once on each proof node in the tree, and that the execution of - [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 *) - - (** {3 Misc} *) - - val check : proof -> unit - (** Check the contents of a proof. Mainly for internal use *) - - module Clause : sig - type t = clause - val name : t -> string - val atoms : t -> atom array - val atoms_l : t -> atom list - 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 - - 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 6d788347..5863de2a 100644 --- a/src/core/Solver.ml +++ b/src/core/Solver.ml @@ -6,150 +6,7 @@ Copyright 2016 Simon Cruanes module type S = Solver_intf.S -open Solver_intf +module Make_cdcl_t = Internal.Make_cdcl_t +module Make_mcsat = Internal.Make_mcsat +module Make_pure_sat = Internal.Make_pure_sat -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) -= struct - - module St = St - - module S = Internal.Make(St)(Th) - - module Proof = S.Proof - - exception UndecidedLit = S.UndecidedLit - - type formula = St.formula - type term = St.term - type atom = St.formula - type clause = St.clause - type theory = Th.t - - type t = S.t - type solver = t - - let create = S.create - - (* Result type *) - type res = - | Sat of (St.term,St.formula) sat_state - | Unsat of (St.clause,Proof.proof) unsat_state - - let pp_all st lvl status = - Log.debugf lvl - (fun k -> k - "@[%s - Full resume:@,@[Trail:@\n%a@]@,\ - @[Temp:@\n%a@]@,@[Hyps:@\n%a@]@,@[Lemmas:@\n%a@]@,@]@." - status - (Vec.pp ~sep:"" St.Trail_elt.debug) (S.trail st) - (Vec.pp ~sep:"" St.Clause.debug) (S.temp st) - (Vec.pp ~sep:"" St.Clause.debug) (S.hyps st) - (Vec.pp ~sep:"" St.Clause.debug) (S.history st) - ) - - let mk_sat (st:S.t) : (_,_) sat_state = - pp_all st 99 "SAT"; - let t = S.trail st in - let iter f f' = - Vec.iter (function - | St.Atom a -> f a.St.lit - | St.Lit l -> f' l.St.term) - t - in - { - eval = S.eval st; - eval_level = S.eval_level st; - iter_trail = iter; - model = (fun () -> S.model st); - } - - let mk_unsat (st:S.t) : (_,_) unsat_state = - pp_all st 99 "UNSAT"; - let unsat_conflict () = - match S.unsat_conflict st with - | None -> assert false - | Some c -> c - in - let get_proof () = - let c = unsat_conflict () in - S.Proof.prove_unsat c - in - { unsat_conflict; get_proof; } - - (* clean local state *) - let[@inline] cleanup_ (st:t) : unit = - if st.S.dirty then ( - S.pop st; (* reset *) - st.S.dirty <- false; - ) - - (* Wrappers around internal functions*) - let[@inline] assume st ?tag cls : unit = - cleanup_ st; - S.assume st ?tag cls - - let[@inline] add_clause st c : unit = - cleanup_ st; - S.add_clause st c - - let solve (st:t) ?(assumptions=[]) () = - cleanup_ st; - try - S.push st; - st.S.dirty <- true; (* to call [pop] before any other action *) - S.local st assumptions; - S.solve st; - Sat (mk_sat st) - with S.Unsat -> - Unsat (mk_unsat st) - - let[@inline] push st = - cleanup_ st; - S.push st - - let[@inline] pop st = - cleanup_ st; - S.pop st - - let unsat_core = S.Proof.unsat_core - - let true_at_level0 st a = - try - let b, lev = S.eval_level st a in - b && lev = 0 - with S.UndecidedLit -> false - - let get_tag cl = St.(cl.tag) - - let[@inline] new_lit st t = - cleanup_ st; - S.new_lit st t - - let[@inline] new_atom st a = - cleanup_ st; - S.new_atom st a - - let export (st:t) : St.clause export = - let hyps = S.hyps st in - 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 atoms_l c = St.Clause.atoms_l c |> List.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 69441e0d..d50fc2e4 100644 --- a/src/core/Solver.mli +++ b/src/core/Solver.mli @@ -13,16 +13,22 @@ Copyright 2014 Simon Cruanes module type S = Solver_intf.S (** Safe external interface of solvers. *) -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) - : S with type term = St.term - and type formula = St.formula - and type clause = St.clause - and type Proof.lemma = St.proof +module Make_cdcl_t(Th : Solver_intf.PLUGIN_CDCL_T) + : S with type Term.t = Solver_intf.void + and module Formula = Th.Formula + and type lemma = Th.proof and type theory = Th.t -(** Functor to make a safe external interface. *) + +module Make_mcsat(Th : Solver_intf.PLUGIN_MCSAT) + : S with module Term = Th.Term + and module Formula = Th.Formula + and type lemma = Th.proof + and type theory = Th.t + +module Make_pure_sat(F: Solver_intf.FORMULA) + : S with type Term.t = Solver_intf.void + and module Formula = F + and type lemma = Solver_intf.void + and type theory = unit diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index a28cb248..8b17d69f 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -11,6 +11,8 @@ Copyright 2016 Simon Cruanes functor in {!Solver} or {!Mcsolver}. *) +type 'a printer = Format.formatter -> 'a -> unit + type ('term, 'form) sat_state = { eval: 'form -> bool; (** Returns the valuation of a formula in the current state @@ -45,7 +47,279 @@ type 'clause export = { } (** Export internal state *) -type 'a printer = Format.formatter -> 'a -> unit +type negated = + | Negated (** changed sign *) + | Same_sign (** kept sign *) +(** This type is used during the normalisation of formulas. + See {!val:Expr_intf.S.norm} for more details. *) + +type 'term eval_res = + | Unknown (** The given formula does not have an evaluation *) + | Valued of bool * ('term list) (** The given formula can be evaluated to the given bool. + The list of terms to give is the list of terms that + were effectively used for the evaluation. *) +(** The type of evaluation results for a given formula. + For instance, let's suppose we want to evaluate the formula [x * y = 0], the + following result are correct: + - [Unknown] if neither [x] nor [y] are assigned to a value + - [Valued (true, [x])] if [x] is assigned to [0] + - [Valued (true, [y])] if [y] is assigned to [0] + - [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number) +*) + +type ('formula, 'proof) th_res = + | Th_sat + (** The current set of assumptions is satisfiable. *) + | Th_unsat of 'formula list * 'proof + (** The current set of assumptions is *NOT* satisfiable, and here is a + theory tautology (with its proof), for which every litteral is false + under the current assumptions. *) +(** Type returned by the theory. Formulas in the unsat clause must come from the + current set of assumptions, i.e must have been encountered in a slice. *) + +type ('term, 'formula) assumption = + | Lit of 'formula (** The given formula is asserted true by the solver *) + | Assign of 'term * 'term (** The first term is assigned to the second *) +(** Asusmptions made by the core SAT solver. *) + +type ('term, 'formula, 'proof) reason = + | Eval of 'term list (** The formula can be evalutaed using the terms in the list *) + | Consequence of 'formula list * 'proof (** [Consequence (l, p)] means that the formulas in [l] imply + the propagated formula [f]. The proof should be a proof of + the clause "[l] implies [f]". *) +(** The type of reasons for propagations of a formula [f]. *) + +type ('term, 'formula, 'proof) slice = { + start : int; (** Start of the slice *) + length : int; (** Length of the slice *) + get : int -> ('term, 'formula) assumption; (** Accessor for the assertions in the slice. + Should only be called on integers [i] s.t. + [start <= i < start + length] *) + push : 'formula list -> 'proof -> unit; (** Add a clause to the solver. *) + propagate : 'formula -> + ('term, 'formula, 'proof) reason -> unit; (** Propagate a formula, i.e. the theory can + evaluate the formula to be true (see the + definition of {!type:eval_res} *) +} +(** The type for a slice of assertions to assume/propagate in the theory. *) + +type ('a, 'b) gadt_eq = GADT_EQ : ('a, 'a) gadt_eq + +type void = (unit,bool) gadt_eq +(** A provably empty type *) + +module type FORMULA = sig + (** formulas *) + + type t + (** The type of atomic formulas over terms. *) + + val equal : t -> t -> bool + (** Equality over formulas. *) + + val hash : t -> int + (** Hashing function for formulas. Should be such that two formulas equal according + to {!val:Expr_intf.S.equal} have the same hash. *) + + val pp : t printer + (** Printing function used among other thing for debugging. *) + + val neg : t -> t + (** Formula negation *) + + val norm : t -> t * negated + (** Returns a 'normalized' form of the formula, possibly negated + (in which case return [Negated]). + [norm] must be so that [a] and [neg a] normalise to the same formula, + but one returns [Negated] and the other [Same_sign]. *) +end + +(** Formulas and Terms required for mcSAT *) +module type EXPR = sig + type proof + (** An abstract type for proofs *) + + module Term : sig + type t + (** The type of terms *) + + val equal : t -> t -> bool + (** Equality over terms. *) + + val hash : t -> int + (** Hashing function for terms. Should be such that two terms equal according + to {!val:Expr_intf.S.equal} have the same hash. *) + + val pp : t printer + (** Printing function used among other for debugging. *) + end + + module Formula : FORMULA +end + +(** Signature for theories to be given to the CDCL(T) solver *) +module type PLUGIN_CDCL_T = sig + type t + (** The plugin state itself *) + + module Formula : FORMULA + + type proof + + type level + (** The type for levels to allow backtracking. *) + + val current_level : t -> level + (** Return the current level of the theory (either the empty/beginning state, or the + last level returned by the [assume] function). *) + + val assume : t -> (void, Formula.t, proof) slice -> (Formula.t, proof) th_res + (** Assume the formulas in the slice, possibly pushing new formulas to be propagated, + and returns the result of the new assumptions. *) + + val if_sat : t -> (void, Formula.t, proof) slice -> (Formula.t, proof) th_res + (** Called at the end of the search in case a model has been found. If no new clause is + pushed and the function returns [Sat], then proof search ends and 'sat' is returned, + else search is resumed. *) + + val backtrack : t -> level -> unit + (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the + same state as when it returned the value [l], *) + +end + +(** Signature for theories to be given to the Model Constructing Solver. *) +module type PLUGIN_MCSAT = sig + type t + (** The plugin state itself *) + + include EXPR + + type level + (** The type for levels to allow backtracking. *) + + val current_level : t -> level + (** Return the current level of the theory (either the empty/beginning state, or the + last level returned by the [assume] function). *) + + val assume : t -> (Term.t, Formula.t, proof) slice -> (Formula.t, proof) th_res + (** Assume the formulas in the slice, possibly pushing new formulas to be propagated, + and returns the result of the new assumptions. *) + + val if_sat : t -> (Term.t, Formula.t, proof) slice -> (Formula.t, proof) th_res + (** Called at the end of the search in case a model has been found. If no new clause is + pushed and the function returns [Sat], then proof search ends and 'sat' is returned, + else search is resumed. *) + + val backtrack : t -> level -> unit + (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the + same state as when it returned the value [l], *) + + val assign : t -> Term.t -> Term.t + (** Returns an assignment value for the given term. *) + + val iter_assignable : t -> (Term.t -> unit) -> Formula.t -> unit + (** An iterator over the subTerm.ts of a Formula.t that should be assigned a value (usually the poure subTerm.ts) *) + + val eval : t -> Formula.t -> Term.t eval_res + (** Returns the evaluation of the Formula.t in the current assignment *) + +end + +module type PROOF = sig + (** Signature for a module handling proof by resolution from sat solving traces *) + + (** {3 Type declarations} *) + + exception Insuficient_hyps + (** Raised when a complete resolution derivation cannot be found using the current hypotheses. *) + + type formula + type atom + type lemma + type clause + (** Abstract types for atoms, clauses and theory-specific lemmas *) + + type t + (** 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 *) + } + (** A proof can be expanded into a proof node, which show the first step of the proof. *) + + (** The type of reasoning steps allowed in a proof. *) + and step = + | Hypothesis + (** The conclusion is a user-provided hypothesis *) + | Assumption + (** The conclusion has been locally assumed by the user *) + | Lemma of lemma + (** The conclusion is a tautology provided by the theory, with associated proof *) + | Duplicate of t * atom list + (** The conclusion is obtained by eliminating multiple occurences of the atom in + the conclusion of the provided proof. *) + | Resolution of t * t * atom + (** The conclusion can be deduced by performing a resolution between the conclusions + of the two given proofs. The atom on which to perform the resolution is also given. *) + + (** {3 Proof building functions} *) + + val prove : clause -> t + (** Given a clause, return a proof of that clause. + @raise Insuficient_hyps if it does not succeed. *) + + val prove_unsat : clause -> t + (** Given a conflict clause [c], returns a proof of the empty clause. + @raise Insuficient_hyps if it does not succeed. *) + + val prove_atom : atom -> t option + (** Given an atom [a], returns a proof of the clause [[a]] if [a] is true at level 0 *) + + (** {3 Proof Nodes} *) + + val parents : step -> t list + (** Returns the parents of a proof node. *) + + val is_leaf : step -> bool + (** Returns wether the the proof node is a leaf, i.e. an hypothesis, + an assumption, or a lemma. + [true] if and only if {!parents} returns the empty list. *) + + val expl : step -> string + (** Returns a short string description for the proof step; for instance + ["hypothesis"] for a [Hypothesis] + (it currently returns the variant name in lowercase). *) + + + (** {3 Proof Manipulation} *) + + val expand : t -> proof_node + (** Return the proof step at the root of a given proof. *) + + val conclusion : t -> clause + (** What is proved at the root of the clause *) + + val fold : ('a -> proof_node -> 'a) -> 'a -> t -> 'a + (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that + [f] is executed exactly once on each proof node in the tree, and that the execution of + [f] on a proof node happens after the execution on the parents of the nodes. *) + + val unsat_core : t -> 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 *) + + (** {3 Misc} *) + + val check : t -> unit + (** Check the contents of a proof. Mainly for internal use *) + + module Tbl : Hashtbl.S with type key = t +end (** The external interface implemented by safe solvers, such as the one created by the {!Solver.Make} and {!Mcsolver.Make} functors. *) @@ -54,18 +328,61 @@ 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. *) - type term (** user terms *) + include EXPR - type formula (** user formulas *) + type term = Term.t (** user terms *) + + type formula = Formula.t (** user formulas *) + + type atom + (** The type of atoms given by the module argument for formulas. + An atom is a user-defined atomic formula whose truth value is + picked by Msat. *) type clause type theory - module Proof : Res.S with type clause = clause + type lemma + + type solver + + module Atom : sig + type t = atom + + val equal : t -> t -> bool + val compare : t -> t -> int + val hash : t -> int + val neg : t -> t + val sign : t -> bool + val abs : t -> t + val formula : t -> formula + val pp : t printer + end + + module Clause : sig + type t = clause + + val atoms : t -> atom array + val atoms_l : t -> atom list + val tag : t -> int option + val equal : t -> t -> bool + val name : t -> string + + val pp : t printer + + module Tbl : Hashtbl.S with type key = t + end + + module Proof : PROOF + with type clause = clause + and type atom = atom + and type formula = formula + and type lemma = lemma + and type t = proof (** A module to manipulate proofs. *) - type t + type t = solver (** Main solver type, containing all state for solving. *) val create : ?size:[`Tiny|`Small|`Big] -> theory -> t @@ -76,15 +393,10 @@ module type S = sig (** {2 Types} *) - type atom = formula - (** The type of atoms given by the module argument for formulas. - An atom is a user-defined atomic formula whose truth value is - picked by Msat. *) - (** Result type for the solver *) type res = - | Sat of (term,formula) sat_state (** Returned when the solver reaches SAT, with a model *) - | Unsat of (clause,Proof.proof) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) + | Sat of (term,atom) sat_state (** Returned when the solver reaches SAT, with a model *) + | Unsat of (clause,Proof.t) unsat_state (** Returned when the solver reaches UNSAT, with a proof *) exception UndecidedLit (** Exception raised by the evaluating functions when a literal @@ -92,11 +404,11 @@ module type S = sig (** {2 Base operations} *) - val assume : t -> ?tag:int -> atom list list -> unit + val assume : t -> ?tag:int -> formula list list -> unit (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. *) - val add_clause : t -> clause -> unit + val add_clause : t -> ?tag:int -> atom list -> unit (** Lower level addition of clauses *) val solve : t -> ?assumptions:atom list -> unit -> res @@ -110,12 +422,12 @@ module type S = sig be decided on at some point during solving, wether it appears in clauses or not. *) - val new_atom : t -> atom -> unit + val make_atom : t -> formula -> atom (** 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 unsat_core : Proof.proof -> clause list + val unsat_core : Proof.t -> clause list (** Returns the unsat core of a given proof, ie a subset of all the added clauses that is sufficient to establish unsatisfiability. *) @@ -136,32 +448,5 @@ module type S = sig call to [push] *) 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 atoms_l : t -> atom list - 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 deleted file mode 100644 index d585f5dd..00000000 --- a/src/core/Solver_types.ml +++ /dev/null @@ -1,420 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -Copyright 2016 Simon Cruanes -*) - -module type S = Solver_types_intf.S - -(* Solver types for McSat Solving *) -(* ************************************************************************ *) - -module McMake (E : Expr_intf.S) = struct - - (* Flag for Mcsat v.s Pure Sat *) - let mcsat = true - - type term = E.Term.t - type formula = E.Formula.t - type proof = E.proof - - type seen = - | Nope - | Both - | Positive - | Negative - - type lit = { - lid : int; - term : term; - mutable l_level : int; - mutable l_idx: int; - mutable l_weight : float; - mutable assigned : term option; - } - - type var = { - vid : int; - pa : atom; - na : atom; - mutable v_fields : int; - mutable v_level : int; - mutable v_idx: int; (** position in heap *) - mutable v_weight : float; (** Weight (for the heap), tracking activity *) - mutable v_assignable: lit list option; - mutable reason : reason option; - } - - and atom = { - aid : int; - var : var; - neg : atom; - lit : formula; - mutable is_true : bool; - mutable watched : clause Vec.t; - } - - and clause = { - name : int; - tag : int option; - atoms : atom array; - mutable cpremise : premise; - mutable activity : float; - mutable attached : bool; - mutable visited : bool; - } - - and reason = - | Decision - | Bcp of clause - | Semantic - - and premise = - | Hyp - | Local - | Lemma of proof - | History of clause list - - type elt = - | E_lit of lit - | E_var of var - - type trail_elt = - | Lit of lit - | Atom of atom - - (* Constructors *) - module MF = Hashtbl.Make(E.Formula) - module MT = Hashtbl.Make(E.Term) - - type t = { - t_map: lit MT.t; - f_map: var MF.t; - vars: elt Vec.t; - mutable cpt_mk_var: int; - mutable cpt_mk_clause: int; - } - - type state = t - - let create_ size_map () : t = { - f_map = MF.create size_map; - t_map = MT.create size_map; - vars = Vec.create(); - cpt_mk_var = 0; - cpt_mk_clause = 0; - } - - let create ?(size=`Big) () : t = - let size_map = match size with - | `Tiny -> 8 - | `Small -> 16 - | `Big -> 4096 - in - create_ size_map () - - let nb_elt st = Vec.size st.vars - let get_elt st i = Vec.get st.vars i - let iter_elt st f = Vec.iter f st.vars - - let name_of_clause c = match c.cpremise with - | Hyp -> "H" ^ string_of_int c.name - | Local -> "L" ^ string_of_int c.name - | Lemma _ -> "T" ^ string_of_int c.name - | History _ -> "C" ^ string_of_int c.name - - module Lit = struct - type t = lit - let[@inline] term l = l.term - let[@inline] level l = l.l_level - let[@inline] assigned l = l.assigned - let[@inline] weight l = l.l_weight - - let make (st:state) (t:term) : t = - try MT.find st.t_map t - with Not_found -> - let res = { - lid = st.cpt_mk_var; - term = t; - l_weight = 1.; - l_idx= -1; - l_level = -1; - assigned = None; - } in - st.cpt_mk_var <- st.cpt_mk_var + 1; - MT.add st.t_map t res; - Vec.push st.vars (E_lit res); - res - - let debug_assign fmt v = - match v.assigned with - | None -> - Format.fprintf fmt "" - | Some t -> - Format.fprintf fmt "@[@@%d->@ %a@]" v.l_level E.Term.pp t - - let pp out v = E.Term.pp out v.term - let debug out v = - Format.fprintf out "%d[%a][lit:@[%a@]]" - (v.lid+1) debug_assign v E.Term.pp v.term - end - - let seen_pos = 0b1 - let seen_neg = 0b10 - - module Var = struct - type t = var - let[@inline] level v = v.v_level - let[@inline] pos v = v.pa - let[@inline] neg v = v.na - let[@inline] reason v = v.reason - let[@inline] assignable v = v.v_assignable - let[@inline] weight v = v.v_weight - - let make (st:state) (t:formula) : var * Expr_intf.negated = - let lit, negated = E.Formula.norm t in - try - MF.find st.f_map lit, negated - with Not_found -> - let cpt_double = st.cpt_mk_var lsl 1 in - let rec var = - { vid = st.cpt_mk_var; - pa = pa; - na = na; - v_fields = 0; - v_level = -1; - v_idx= -1; - v_weight = 0.; - v_assignable = None; - reason = None; - } - and pa = - { var = var; - lit = lit; - watched = Vec.create(); - neg = na; - is_true = false; - aid = cpt_double (* aid = vid*2 *) } - and na = - { var = var; - lit = E.Formula.neg lit; - watched = Vec.create(); - neg = pa; - is_true = false; - 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; - Vec.push st.vars (E_var var); - var, negated - - (* Marking helpers *) - let[@inline] clear v = - v.v_fields <- 0 - - let[@inline] seen_both v = - (seen_pos land v.v_fields <> 0) && - (seen_neg land v.v_fields <> 0) - end - - module Atom = struct - type t = atom - let[@inline] level a = a.var.v_level - let[@inline] var a = a.var - let[@inline] neg a = a.neg - 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 - let[@inline] is_true a = a.is_true - let[@inline] is_false a = a.neg.is_true - - let[@inline] seen a = - let pos = equal a (abs a) in - if pos - then (seen_pos land a.var.v_fields <> 0) - else (seen_neg land a.var.v_fields <> 0) - - let[@inline] mark a = - let pos = equal a (abs a) in - if pos then ( - a.var.v_fields <- seen_pos lor a.var.v_fields - ) else ( - a.var.v_fields <- seen_neg lor a.var.v_fields - ) - - let[@inline] make st lit = - let var, negated = Var.make st lit in - match negated with - | Formula_intf.Negated -> var.na - | Formula_intf.Same_sign -> var.pa - - let pp fmt a = E.Formula.pp fmt a.lit - - let pp_a fmt v = - if Array.length v = 0 then ( - Format.fprintf fmt "∅" - ) else ( - pp fmt v.(0); - if (Array.length v) > 1 then begin - for i = 1 to (Array.length v) - 1 do - Format.fprintf fmt " ∨ %a" pp v.(i) - done - end - ) - - (* Complete debug printing *) - let sign a = if a == a.var.pa then "+" else "-" - - let debug_reason fmt = function - | n, _ when n < 0 -> - Format.fprintf fmt "%%" - | n, None -> - Format.fprintf fmt "%d" n - | n, Some Decision -> - Format.fprintf fmt "@@%d" n - | n, Some Bcp c -> - Format.fprintf fmt "->%d/%s" n (name_of_clause c) - | n, Some Semantic -> - Format.fprintf fmt "::%d" n - - let pp_level fmt a = - debug_reason fmt (a.var.v_level, a.var.reason) - - let debug_value fmt a = - if a.is_true then - Format.fprintf fmt "T%a" pp_level a - else if a.neg.is_true then - Format.fprintf fmt "F%a" pp_level a - else - Format.fprintf fmt "" - - let debug out a = - Format.fprintf out "%s%d[%a][atom:@[%a@]]" - (sign a) (a.var.vid+1) debug_value a E.Formula.pp a.lit - - let debug_a out vec = - Array.iter (fun a -> Format.fprintf out "%a@ " debug a) vec - end - - (* Elements *) - module Elt = struct - type t = elt - let[@inline] of_lit l = E_lit l - let[@inline] of_var v = E_var v - - let[@inline] id = function - | E_lit l -> l.lid | E_var v -> v.vid - let[@inline] level = function - | E_lit l -> l.l_level | E_var v -> v.v_level - let[@inline] idx = function - | E_lit l -> l.l_idx | E_var v -> v.v_idx - let[@inline] weight = function - | E_lit l -> l.l_weight | E_var v -> v.v_weight - - let[@inline] set_level e lvl = match e with - | E_lit l -> l.l_level <- lvl | E_var v -> v.v_level <- lvl - let[@inline] set_idx e i = match e with - | E_lit l -> l.l_idx <- i | E_var v -> v.v_idx <- i - let[@inline] set_weight e w = match e with - | E_lit l -> l.l_weight <- w | E_var v -> v.v_weight <- w - end - - module Trail_elt = struct - type t = trail_elt - let[@inline] of_lit l = Lit l - let[@inline] of_atom a = Atom a - - let debug fmt = function - | Lit l -> Lit.debug fmt l - | Atom a -> Atom.debug fmt a - end - - module Clause = struct - type t = clause - - let make = - let n = ref 0 in - fun ?tag ali premise -> - let atoms = Array.of_list ali in - let name = !n in - incr n; - { name; - tag = tag; - atoms = atoms; - visited = false; - attached = false; - activity = 0.; - cpremise = premise} - - let empty = make [] (History []) - let name = name_of_clause - let[@inline] equal c1 c2 = c1==c2 - let[@inline] atoms c = c.atoms - let[@inline] atoms_l c = Array.to_list 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 - - let[@inline] visited c = c.visited - let[@inline] set_visited c b = c.visited <- b - - let[@inline] attached c = c.attached - let[@inline] set_attached c b = c.attached <- b - - 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 - - let debug_premise out = function - | Hyp -> Format.fprintf out "hyp" - | Local -> Format.fprintf out "local" - | Lemma _ -> Format.fprintf out "th_lemma" - | History v -> - List.iter (fun c -> Format.fprintf out "%s,@ " (name_of_clause c)) v - - let debug out ({atoms=arr; cpremise=cp;_}as c) = - Format.fprintf out "%s@[{@[%a@]}@ cpremise={@[%a@]}@]" - (name c) Atom.debug_a arr debug_premise cp - - let pp_dimacs fmt {atoms;_} = - let aux fmt a = - Array.iter (fun p -> - Format.fprintf fmt "%s%d " - (if p == p.var.pa then "-" else "") - (p.var.vid+1) - ) a - in - Format.fprintf fmt "%a0" aux atoms - end - - module Term = E.Term - module Formula = E.Formula -end[@@inline] - - -(* Solver types for pure SAT Solving *) -(* ************************************************************************ *) - -module SatMake (E : Formula_intf.S) = struct - include McMake(struct - include E - module Term = E - module Formula = E - end) - - let mcsat = false -end[@@inline] - diff --git a/src/core/Solver_types.mli b/src/core/Solver_types.mli deleted file mode 100644 index fb1e03c3..00000000 --- a/src/core/Solver_types.mli +++ /dev/null @@ -1,26 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -Copyright 2016 Simon Cruanes -*) - -(** Internal types (implementation) - - This modules actually implements the internal types used by the solver. - Since mutation is heavily used in the solver, it is really, really, *really* - discouraged to direclty use the functions in this module if you don't know the - inner working of mSAT perfectly as even the simplest - change can have dramatic effects on the solver. -*) - -module type S = Solver_types_intf.S -(** Interface for the internal types. *) - -module McMake (E : Expr_intf.S): - S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof -(** Functor to instantiate the types of clauses for a solver. *) - -module SatMake (E : Formula_intf.S): - S with type term = E.t and type formula = E.t and type proof = E.proof -(** Functor to instantiate the types of clauses for a solver. *) - diff --git a/src/core/Solver_types_intf.ml b/src/core/Solver_types_intf.ml deleted file mode 100644 index c5d0ff37..00000000 --- a/src/core/Solver_types_intf.ml +++ /dev/null @@ -1,271 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -Copyright 2016 Simon Cruanes -*) - -(** Internal types (interface) - - This modules defines the interface of most of the internal types - used in the core solver. -*) - -type 'a printer = Format.formatter -> 'a -> unit - -module type S = sig - (** The signatures of clauses used in the Solver. *) - - val mcsat : bool - (** TODO:deprecate. *) - - type t - (** State for creating new terms, literals, clauses *) - - val create: ?size:[`Tiny|`Small|`Big] -> unit -> t - - (** {2 Type definitions} *) - - type term - type formula - type proof - (** The types of terms, formulas and proofs. All of these are user-provided. *) - - type seen = - | Nope - | Both - | Positive - | Negative - - (* TODO: hide these types (from the outside of [Msat]); - instead, provide well defined modules [module Lit : sig type t val …] - that define their API in Msat itself (not here) *) - - type lit = { - lid : int; (** Unique identifier *) - term : term; (** Wrapped term *) - mutable l_level : int; (** Decision level of the assignment *) - mutable l_idx: int; (** index in heap *) - mutable l_weight : float; (** Weight (for the heap) *) - mutable assigned : term option; (** Assignment *) - } - (** Wrapper type for literals, i.e. theory terms (for mcsat only). *) - - type var = { - vid : int; (** Unique identifier *) - pa : atom; (** Link for the positive atom *) - na : atom; (** Link for the negative atom *) - mutable v_fields : int; (** bool fields *) - mutable v_level : int; (** Level of decision/propagation *) - mutable v_idx: int; (** rank in variable heap *) - mutable v_weight : float; (** Variable weight (for the heap) *) - mutable v_assignable: lit list option; - (** In mcsat, the list of lits that wraps subterms of the formula wrapped. *) - mutable reason : reason option; - (** The reason for propagation/decision of the literal *) - } - - and atom = { - aid : int; (** Unique identifier *) - var : var; (** Link for the parent variable *) - neg : atom; (** Link for the negation of the atom *) - lit : formula; (** Wrapped formula *) - mutable is_true : bool; (** Is the atom true ? Conversely, the atom - is false iff a.neg.is_true *) - mutable watched : clause Vec.t; (** The vector of clauses that watch this atom *) - } - (** Atoms and variables wrap theory formulas. They exist in the form of - triplet: a variable and two atoms. For a formula [f] in normal form, - the variable v points to the positive atom [a] which wraps [f], while - [a.neg] wraps the theory negation of [f]. *) - - and clause = { - name : int; (** Clause name, mainly for printing, unique. *) - tag : int option; (** User-provided tag for clauses. *) - atoms : atom array; (** The atoms that constitute the clause.*) - mutable cpremise : premise; (** The premise of the clause, i.e. the justification - of why the clause must be satisfied. *) - mutable activity : float; (** Clause activity, used for the heap heuristics. *) - mutable attached : bool; (** Is the clause attached, i.e. does it watch literals. *) - mutable visited : bool; (** Boolean used during propagation and proof generation. *) - } - (** The type of clauses. Each clause generated should be true, i.e. enforced - by the current problem (for more information, see the cpremise field). *) - - and reason = - | Decision (** The atom has been decided by the sat solver *) - | Bcp of clause (** The atom has been propagated by the given clause *) - | Semantic (** The atom has been propagated by the theory at the given level. *) - (** Reasons of propagation/decision of atoms. *) - - and premise = - | Hyp (** The clause is a hypothesis, provided by the user. *) - | Local (** The clause is a 1-atom clause, - where the atom is a local assumption*) - | Lemma of proof (** The clause is a theory-provided tautology, with - the given proof. *) - | History of clause list (** The clause can be obtained by resolution of the clauses - in the list. If the list has a single element [c] , then - the clause can be obtained by simplifying [c] (i.e - eliminating doublons in its atom list). - For a premise [History [a_1 :: ... :: a_n]] ([n > 0]) - the clause is obtained by performing resolution of - [a_1] with [a_2], and then performing a resolution step between - the result and [a_3], etc... - Of course, each of the clause [a_i] also has its own premise. *) - (** Premises for clauses. Indeed each clause generated during a run of the solver - should be satisfied, the premise is the justification of why it should be - satisfied by the solver. *) - - (** {2 Decisions and propagations} *) - type trail_elt = - | Lit of lit - | Atom of atom (**) - (** Either a lit of an atom *) - - (** {2 Elements} *) - - type elt = - | E_lit of lit - | E_var of var (**) - (** Either a lit of a var *) - - val nb_elt : t -> int - val get_elt : t -> int -> elt - val iter_elt : t -> (elt -> unit) -> unit - (** Read access to the vector of variables created *) - - (** {2 Variables, Literals & Clauses } *) - - type state = t - - module Lit : sig - type t = lit - val term : t -> term - val make : state -> term -> t - (** Returns the variable associated with the term *) - - val level : t -> int - val assigned : t -> term option - val weight : t -> float - - val pp : t printer - val debug : t printer - end - - module Var : sig - type t = var - - val pos : t -> atom - val neg : t -> atom - - val level : t -> int - val reason : t -> reason option - val assignable : t -> lit list option - val weight : t -> float - - val make : state -> formula -> t * Formula_intf.negated - (** Returns the variable linked with the given formula, - and whether the atom associated with the formula - is [var.pa] or [var.na] *) - - val seen_both : t -> bool - (** both atoms have been seen? *) - - val clear : t -> unit - (** Clear the 'seen' field of the variable. *) - end - - module Atom : sig - type t = atom - val level : t -> int - val reason : t -> reason option - val lit : t -> formula - val equal : t -> t -> bool - val compare : t -> t -> int - val var : t -> Var.t - 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 - - val make : state -> formula -> t - (** Returns the atom associated with the given formula *) - - val mark : t -> unit - (** Mark the atom as seen, using the 'seen' field in the variable. *) - - val seen : t -> bool - (** Returns wether the atom has been marked as seen. *) - - val pp : t printer - val pp_a : t array printer - val debug : t printer - val debug_a : t array printer - end - - module Elt : sig - type t = elt - - val of_lit : Lit.t -> t - val of_var : Var.t -> t - - val id : t -> int - val level : t -> int - val idx : t -> int - val weight : t -> float - - val set_level : t -> int -> unit - val set_idx : t -> int -> unit - val set_weight : t -> float -> unit - end - - module Clause : sig - type t = clause - - val name : t -> string - val equal : t -> t -> bool - val hash : t -> int - val atoms : t -> Atom.t array - val atoms_l : t -> Atom.t list - val tag : t -> int option - val premise : t -> premise - - val empty : t - (** The empty clause *) - - val make : ?tag:int -> Atom.t list -> premise -> clause - (** [make_clause name atoms size premise] creates a clause with the given attributes. *) - - 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 - type t = trail_elt - - val of_lit : Lit.t -> t - val of_atom : Atom.t -> t - (** Constructors and destructors *) - val debug : t printer - end - - module Term : sig - type t = term - val equal : t -> t -> bool - val hash : t -> int - val pp : t printer - end - - module Formula : sig - type t = formula - val equal : t -> t -> bool - val hash : t -> int - val pp : t printer - end -end - diff --git a/src/core/Theory_intf.ml b/src/core/Theory_intf.ml deleted file mode 100644 index d377509d..00000000 --- a/src/core/Theory_intf.ml +++ /dev/null @@ -1,83 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -Copyright 2016 Simon Cruanes -*) - -(** SMT Theory - - This module defines what a theory must implement in order to - be used in an SMT solver. -*) - -type ('formula, 'proof) res = ('formula, 'proof) Plugin_intf.res = - | Sat - (** The current set of assumptions is satisfiable. *) - | Unsat of 'formula list * 'proof - (** The current set of assumptions is *NOT* satisfiable, and here is a - theory tautology (with its proof), for which every litteral is false - under the current assumptions. *) -(** Type returned by the theory. Formulas in the unsat clause must come from the - current set of assumptions, i.e must have been encountered in a slice. *) - -type ('form, 'proof) slice = { - start : int; (** Start of the slice *) - length : int; (** Length of the slice *) - get : int -> 'form; (** Accesor for the formuals in the slice. - Should only be called on integers [i] s.t. - [start <= i < start + length] *) - push : 'form list -> 'proof -> unit; (** Allows to add to the solver a clause. *) - propagate : 'form -> 'form list -> 'proof -> unit; - (** [propagate lit causes proof] informs the solver to propagate [lit], with the reason - that the clause [causes => lit] is a theory tautology. It is faster than pushing - the associated clause but the clause will not be remembered by the sat solver, - i.e it will not be used by the solver to do boolean propagation. *) -} -(** The type for a slice. Slices are some kind of view of the current - propagation queue. They allow to look at the propagated literals, - and to add new clauses to the solver. *) - -(** Signature for theories to be given to the Solver. *) -module type S = sig - type t - (** The state of the theory itself *) - - type formula - (** The type of formulas. Should be compatble with Formula_intf.S *) - - type proof - (** A custom type for the proofs of lemmas produced by the theory. *) - - type level - (** The type for levels to allow backtracking. *) - - val current_level : t -> level - (** Return the current level of the theory (either the empty/beginning state, or the - last level returned by the [assume] function). *) - - val assume : t -> (formula, proof) slice -> (formula, proof) res - (** Assume the formulas in the slice, possibly pushing new formulas to be propagated, - and returns the result of the new assumptions. *) - - val if_sat : t -> (formula, proof) slice -> (formula, proof) res - (** Called at the end of the search in case a model has been found. If no new clause is - pushed, then 'sat' is returned, else search is resumed. *) - - val backtrack : t -> level -> unit - (** Backtrack to the given level. After a call to [backtrack l], the theory should be in the - same state as when it returned the value [l], *) - -end - -module Dummy(F: Formula_intf.S) - : S with type formula = F.t and type t = unit -= struct - type t = unit - type formula = F.t - type proof = unit - type level = unit - let current_level () = () - let assume () _ = Sat - let if_sat () _ = Sat - let backtrack () _ = () -end diff --git a/src/main/main.ml b/src/main/main.ml index 177b5b32..e2573b4f 100644 --- a/src/main/main.ml +++ b/src/main/main.ml @@ -19,7 +19,7 @@ let size_limit = ref 1000_000_000. module S = Msat_sat module Process = struct - module D = Msat_backend.Dot.Make(S.Proof)(Msat_backend.Dot.Default(S.Proof)) + module D = Msat_backend.Dot.Make(S)(Msat_backend.Dot.Default(S)) let hyps = ref [] @@ -29,7 +29,7 @@ module Process = struct let check_clause c = let l = List.map (function a -> Log.debugf 99 - (fun k -> k "Checking value of %a" S.Formula.pp a); + (fun k -> k "Checking value of %a" S.Atom.pp a); sat.Msat.eval a) c in List.exists (fun x -> x) l in diff --git a/src/sat/Expr_sat.ml b/src/sat/Expr_sat.ml index f41ba5d5..e6de1a13 100644 --- a/src/sat/Expr_sat.ml +++ b/src/sat/Expr_sat.ml @@ -2,9 +2,6 @@ exception Bad_atom (** Exception raised if an atom cannot be created *) -type proof -(** A empty type for proofs *) - type t = int (** Atoms are represented as integers. [-i] begin the negation of [i]. Additionally, since we nee dot be able to create fresh atoms, we @@ -31,9 +28,9 @@ let neg a = - a let norm a = abs a, if a < 0 then - Formula_intf.Negated + Solver_intf.Negated else - Formula_intf.Same_sign + Solver_intf.Same_sign let abs = abs diff --git a/src/sat/Expr_sat.mli b/src/sat/Expr_sat.mli index a48603af..a8be3e3e 100644 --- a/src/sat/Expr_sat.mli +++ b/src/sat/Expr_sat.mli @@ -8,7 +8,7 @@ near optimal efficiency (both in terms of space and time). *) -include Formula_intf.S +include Solver_intf.FORMULA (** This modules implements the requirements for implementing an SAT Solver. *) val make : int -> t diff --git a/src/sat/Msat_sat.ml b/src/sat/Msat_sat.ml index 1fc3d1ee..007f385b 100644 --- a/src/sat/Msat_sat.ml +++ b/src/sat/Msat_sat.ml @@ -4,7 +4,5 @@ Copyright 2016 Guillaume Bury *) module Expr = Expr_sat - -module F = Msat.Make_smt_expr(Expr) -include Msat.Make(F)(Msat.Make_dummy(F)) +include Msat.Make_pure_sat(Expr) diff --git a/src/sat/Msat_sat.mli b/src/sat/Msat_sat.mli index 95695269..b36bda05 100644 --- a/src/sat/Msat_sat.mli +++ b/src/sat/Msat_sat.mli @@ -11,6 +11,6 @@ Copyright 2016 Guillaume Bury module Expr = Expr_sat -include Msat.S with type formula = Expr.t and type theory = unit +include Msat.S with type Formula.t = Expr.t and type theory = unit (** A functor that can generate as many solvers as needed. *) diff --git a/tests/test_api.ml b/tests/test_api.ml index 89e8cafb..bef40497 100644 --- a/tests/test_api.ml +++ b/tests/test_api.ml @@ -7,6 +7,7 @@ Copyright 2014 Simon Cruanes (* Tests that require the API *) module F = Msat_sat.Expr +module S = Msat_sat let (|>) x f = f x @@ -36,27 +37,7 @@ type solver_res = exception Incorrect_model -module type BASIC_SOLVER = sig - type t - val create : unit -> t - val solve : t -> ?assumptions:F.t list -> unit -> solver_res - val assume : t -> ?tag:int -> F.t list list -> unit -end - -let mk_solver (): (module BASIC_SOLVER) = - let module S = struct - include Msat_sat - let create() = create() - let solve st ?assumptions () = - match solve st ?assumptions() with - | Sat _ -> - R_sat - | Unsat us -> - let p = us.Msat.get_proof () in - Proof.check p; - R_unsat - end - in (module S) +let mk_solver () : S.t = S.create ~size:`Big () exception Error of string @@ -86,20 +67,22 @@ module Test = struct let run (t:t): result = (* Interesting stuff happening *) - let (module S: BASIC_SOLVER) = mk_solver () in - let st = S.create() in + let st = mk_solver() in try List.iter (function | A_assume cs -> S.assume st cs | A_solve (assumptions, expect) -> + let assumptions = List.map (S.make_atom st) assumptions in match S.solve st ~assumptions (), expect with - | R_sat, `Expect_sat - | R_unsat, `Expect_unsat -> () - | R_unsat, `Expect_sat -> + | S.Sat _, `Expect_sat -> () + | S.Unsat us, `Expect_unsat -> + let p = us.Msat.get_proof () in + S.Proof.check p; + | S.Unsat _, `Expect_sat -> error "expect sat, got unsat" - | R_sat, `Expect_unsat -> + | S.Sat _, `Expect_unsat -> error "expect unsat, got sat" ) t.actions;