From 8c8209c08cacbdd52ca704773b1f1e9915872d57 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 21 Jan 2018 18:46:28 -0600 Subject: [PATCH] large refactoring to keep only a simpler, easier CDCL(T) interface - only one functor to instantiate - explicit state that is carried around - remove minismt stuff --- Makefile | 12 +- msat.exe | 2 +- minismt.opam => msat_test.opam | 6 +- src/core/Expr_intf.ml | 73 -- src/core/Formula_intf.ml | 53 -- src/core/Heap.ml | 12 - src/core/Heap.mli | 12 - src/core/Internal.ml | 401 ++++------- src/core/Msat.ml | 40 +- src/core/Plugin_intf.ml | 121 ---- src/core/Solver.ml | 35 +- src/core/Solver.mli | 9 +- src/core/Solver_intf.ml | 37 +- src/core/Solver_types.ml | 175 +---- src/core/Solver_types.mli | 26 +- src/core/Solver_types_intf.ml | 103 +-- src/core/Theory_intf.ml | 87 ++- src/main/jbuild | 13 - src/{mcsat => main_test}/README.md | 0 src/{solver => main_test}/jbuild | 8 +- src/{main/main.ml => main_test/msat_test.ml} | 50 +- src/main_test/solver.ml | 18 + src/{solver => main_test}/solver.mli | 15 +- .../expr_smt.ml => main_test/theory_smt.ml} | 198 +++++- .../expr_smt.mli => main_test/theory_smt.mli} | 5 +- src/{solver => main_test}/type.ml | 11 +- src/{sat => main_test}/type_sat.ml | 60 +- src/{sat => main_test}/type_sat.mli | 4 +- src/{smt => main_test}/unionfind.ml | 0 src/{smt => main_test}/unionfind.mli | 0 src/mcsat/Minismt_mcsat.ml | 13 - src/mcsat/Minismt_mcsat.mli | 8 - src/mcsat/backtrack.ml | 99 --- src/mcsat/backtrack.mli | 77 --- src/mcsat/eclosure.ml | 232 ------- src/mcsat/eclosure.mli | 60 -- src/mcsat/jbuild | 13 - src/mcsat/plugin_mcsat.ml | 200 ------ src/sat/Expr_sat.ml | 70 -- src/sat/Minismt_sat.ml | 10 - src/sat/Msat_sat.ml | 9 + src/sat/{Minismt_sat.mli => Msat_sat.mli} | 5 +- src/sat/Th_sat.ml | 87 +++ src/sat/{Expr_sat.mli => Th_sat.mli} | 20 +- src/sat/jbuild | 6 +- src/smt/Minismt_smt.ml | 13 - src/smt/Minismt_smt.mli | 11 - src/smt/jbuild | 13 - src/smt/type_smt.ml | 628 ------------------ src/smt/type_smt.mli | 7 - src/solver/mcsolver.ml | 15 - src/solver/mcsolver.mli | 23 - src/solver/solver.ml | 81 --- src/tseitin/Msat_tseitin.ml | 153 +---- src/tseitin/Msat_tseitin.mli | 2 +- src/tseitin/Tseitin_intf.ml | 31 +- tests/jbuild | 2 +- tests/test_api.ml | 24 +- 58 files changed, 777 insertions(+), 2721 deletions(-) rename minismt.opam => msat_test.opam (83%) 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/main/jbuild rename src/{mcsat => main_test}/README.md (100%) rename src/{solver => main_test}/jbuild (67%) rename src/{main/main.ml => main_test/msat_test.ml} (87%) create mode 100644 src/main_test/solver.ml rename src/{solver => main_test}/solver.mli (55%) rename src/{smt/expr_smt.ml => main_test/theory_smt.ml} (70%) rename src/{smt/expr_smt.mli => main_test/theory_smt.mli} (98%) rename src/{solver => main_test}/type.ml (71%) rename src/{sat => main_test}/type_sat.ml (67%) rename src/{sat => main_test}/type_sat.mli (79%) rename src/{smt => main_test}/unionfind.ml (100%) rename src/{smt => main_test}/unionfind.mli (100%) delete mode 100644 src/mcsat/Minismt_mcsat.ml delete mode 100644 src/mcsat/Minismt_mcsat.mli delete mode 100644 src/mcsat/backtrack.ml delete mode 100644 src/mcsat/backtrack.mli delete mode 100644 src/mcsat/eclosure.ml delete mode 100644 src/mcsat/eclosure.mli delete mode 100644 src/mcsat/jbuild delete mode 100644 src/mcsat/plugin_mcsat.ml delete mode 100644 src/sat/Expr_sat.ml delete mode 100644 src/sat/Minismt_sat.ml create mode 100644 src/sat/Msat_sat.ml rename src/sat/{Minismt_sat.mli => Msat_sat.mli} (74%) create mode 100644 src/sat/Th_sat.ml rename src/sat/{Expr_sat.mli => Th_sat.mli} (63%) delete mode 100644 src/smt/Minismt_smt.ml delete mode 100644 src/smt/Minismt_smt.mli delete mode 100644 src/smt/jbuild delete mode 100644 src/smt/type_smt.ml delete mode 100644 src/smt/type_smt.mli delete mode 100644 src/solver/mcsolver.ml delete mode 100644 src/solver/mcsolver.mli delete mode 100644 src/solver/solver.ml diff --git a/Makefile b/Makefile index f789c987..c6bf8a2f 100644 --- a/Makefile +++ b/Makefile @@ -12,7 +12,8 @@ OPTS= -j $(J) LIB=$(addprefix $(NAME), .cma .cmxa .cmxs) -all: build-dev test +all: build test +all-dev: build-dev test build: jbuilder build $(OPTS) @install @@ -20,12 +21,15 @@ build: build-dev: jbuilder build $(OPTS) @install --dev -test: build +build-test: build + jbuilder build $(OPTS) src/main_test/msat_test.exe + +test: build-test @echo "run API tests…" jbuilder runtest @echo "run benchmarks…" - # @/usr/bin/time -f "%e" ./tests/run smt - @/usr/bin/time -f "%e" ./tests/run mcsat + @/usr/bin/time -f "%e" ./tests/run smt + # @/usr/bin/time -f "%e" ./tests/run mcsat enable_log: cd src/core; ln -sf log_real.ml log.ml diff --git a/msat.exe b/msat.exe index cceb9ac3..2d015b30 120000 --- a/msat.exe +++ b/msat.exe @@ -1 +1 @@ -_build/default/src/main/main.exe \ No newline at end of file +_build/default/src/main_test/msat_test.exe \ No newline at end of file diff --git a/minismt.opam b/msat_test.opam similarity index 83% rename from minismt.opam rename to msat_test.opam index a38b471a..29652a80 100644 --- a/minismt.opam +++ b/msat_test.opam @@ -1,15 +1,12 @@ opam-version: "1.2" -name: "minismt" +name: "msat_test" license: "Apache" version: "dev" author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"] maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"] build: ["jbuilder" "build" "@install" "-p" name] build-doc: ["jbuilder" "build" "@doc" "-p" name] -install: ["jbuilder" "install" name] -remove: ["jbuilder" "uninstall" name] depends: [ - "ocamlfind" {build} "jbuilder" {build} "dolmen" "msat" @@ -22,3 +19,4 @@ homepage: "https://github.com/Gbury/mSAT" dev-repo: "https://github.com/Gbury/mSAT.git" bug-reports: "https://github.com/Gbury/mSAT/issues/" + diff --git a/src/core/Expr_intf.ml b/src/core/Expr_intf.ml deleted file mode 100644 index 172ab472..00000000 --- a/src/core/Expr_intf.ml +++ /dev/null @@ -1,73 +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 print : 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 print : Format.formatter -> t -> unit - (** Printing function used among other thing for debugging. *) - - val dummy : t - (** Constant formula. A valid formula should never be physically equal to [dummy] *) - - 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 fe45e908..00000000 --- a/src/core/Formula_intf.ml +++ /dev/null @@ -1,53 +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 print : Format.formatter -> t -> unit - (** Printing function used among other thing for debugging. *) - - val dummy : t - (** Formula constant. A valid formula should never be physically equal to [dummy] *) - - 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/Heap.ml b/src/core/Heap.ml index a8f78d08..1e309ab1 100644 --- a/src/core/Heap.ml +++ b/src/core/Heap.ml @@ -1,15 +1,3 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Mohamed Iguernelala *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) module type RANKED = Heap_intf.RANKED diff --git a/src/core/Heap.mli b/src/core/Heap.mli index 24c47bd6..ef88dbf0 100644 --- a/src/core/Heap.mli +++ b/src/core/Heap.mli @@ -1,15 +1,3 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Mohamed Iguernelala *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) module type RANKED = Heap_intf.RANKED diff --git a/src/core/Internal.ml b/src/core/Internal.ml index 59d41972..cd600c6b 100644 --- a/src/core/Internal.ml +++ b/src/core/Internal.ml @@ -6,8 +6,7 @@ Copyright 2014 Simon Cruanes module Make (St : Solver_types.S) - (Plugin : Plugin_intf.S with type term = St.term - and type formula = St.formula + (Th : Theory_intf.S with type formula = St.formula and type proof = St.proof) = struct module Proof = Res.Make(St) @@ -15,11 +14,11 @@ module Make open St module H = Heap.Make(struct - type t = St.Elt.t - let[@inline] cmp i j = Elt.weight j < Elt.weight i (* comparison by weight *) - let dummy = Elt.of_var St.Var.dummy - let idx = Elt.idx - let set_idx = Elt.set_idx + type t = St.var + let[@inline] cmp i j = Var.weight j < Var.weight i (* comparison by weight *) + let dummy = St.Var.dummy + let idx = St.Var.idx + let set_idx = St.Var.set_idx end) exception Sat @@ -50,6 +49,8 @@ module Make type t = { st : St.t; + th: Th.t lazy_t; + (* Clauses are simplified for eficiency purposes. In the following vectors, the comments actually refer to the original non-simplified clause. *) @@ -73,16 +74,20 @@ module Make mutable next_decision : atom option; (* When the last conflict was a semantic one, this stores the next decision to make *) - trail : trail_elt Vec.t; + trail : atom Vec.t; (* decision stack + propagated elements (atoms or assignments). *) elt_levels : int Vec.t; (* decision levels in [trail] *) - th_levels : Plugin.level Vec.t; - (* theory states corresponding to elt_levels *) user_levels : int Vec.t; - (* user levels in [clauses_temp] *) + (* user levels in [clause_tmp] *) + + backtrack_levels : int Vec.t; + (* user levels in [backtrack] *) + + backtrack : (unit -> unit) Vec.t; + (** Actions to call when backtracking *) mutable th_head : int; (* Start offset in the queue {!trail} of @@ -122,8 +127,9 @@ module Make } (* Starting environment. *) - let create_ ~st ~size_trail ~size_lvl () : t = { + let create_ ~st ~size_trail ~size_lvl th : t = { st; + th; unsat_conflict = None; next_decision = None; @@ -137,9 +143,10 @@ module Make th_head = 0; elt_head = 0; - trail = Vec.make size_trail (Trail_elt.of_atom Atom.dummy); + trail = Vec.make size_trail Atom.dummy; elt_levels = Vec.make size_lvl (-1); - th_levels = Vec.make size_lvl Plugin.dummy; + backtrack_levels = Vec.make size_lvl (-1); + backtrack = Vec.make size_lvl (fun () -> ()); user_levels = Vec.make 0 (-1); order = H.create(); @@ -153,13 +160,7 @@ module Make dirty=false; } - let create ?(size=`Big) ?st () : t = - let st = match st with Some s -> s | None -> St.create ~size () in - let size_trail, size_lvl = match size with - | `Tiny -> 0, 0 - | `Small -> 32, 16 - | `Big -> 600, 50 - in create_ ~st ~size_trail ~size_lvl () + let[@inline] theory st = Lazy.force st.th (* Misc functions *) let to_float = float_of_int @@ -178,35 +179,9 @@ module Make | Some _ -> true | None -> false - (* Iteration over subterms. - When incrementing activity, we want to be able to iterate over - all subterms of a formula. However, the function provided by the theory - may be costly (if it walks a tree-like structure, and does some processing - to ignore some subterms for instance), so we want to 'cache' the list - 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 - 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 res = Atom.make st.st f in - if St.mcsat then ( - begin match res.var.v_assignable with - | Some _ -> () - | None -> - let l = ref [] in - Plugin.iter_assignable - (fun t -> l := Lit.make st.st t :: !l) - res.var.pa.lit; - res.var.v_assignable <- Some !l; - end; - ); - res + let[@inline] mk_atom st (f:St.formula) : atom = Atom.make st.st f (* Variable and literal activity. Activity is used to decide on which variable to decide when propagation @@ -215,27 +190,11 @@ module Make When we add a variable (which wraps a formula), we also need to add all its subterms. *) - let rec insert_var_order st (elt:elt) : unit = - H.insert st.order elt; - begin match elt with - | E_lit _ -> () - | E_var v -> insert_subterms_order st v - end - - and insert_subterms_order st (v:St.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 - clause that constrains it. - We could maybe check if they have already has been decided before - inserting them into the heap, if it appears that it helps performance. *) - let new_lit st t = - let l = Lit.make st.st t in - insert_var_order st (E_lit l) + let[@inline] insert_var_order st (v:var) : unit = H.insert st.order v let new_atom st (p:formula) : unit = let a = mk_atom st p in - insert_var_order st (E_var a.var) + insert_var_order st a.var (* Rather than iterate over all the heap when we want to decrease all the variables/literals activity, we instead increase the value by which @@ -247,38 +206,18 @@ module Make st.clause_incr <- st.clause_incr *. clause_decay (* increase activity of [v] *) - let var_bump_activity_aux st v = + let var_bump_activity 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) + Var.set_weight (St.get_elt st.st i) ((Var.weight (St.get_elt st.st i)) *. 1e-100) done; st.var_incr <- st.var_incr *. 1e-100; ); - let elt = Elt.of_var v in - if H.in_heap elt then ( - H.decrease st.order elt + if H.in_heap v then ( + H.decrease st.order v ) - (* increase activity of literal [l] *) - 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) - done; - st.var_incr <- st.var_incr *. 1e-100; - ); - let elt = Elt.of_lit l in - if H.in_heap elt then ( - H.decrease st.order elt - ) - - (* increase activity of var [v] *) - let var_bump_activity st (v:var): unit = - var_bump_activity_aux st v; - iter_sub (lit_bump_activity_aux st) v - (* increase activity of clause [c] *) let clause_bump_activity st (c:clause) : unit = c.activity <- c.activity +. st.clause_incr; @@ -391,7 +330,7 @@ module Make assert (st.th_head = Vec.size st.trail); assert (st.elt_head = Vec.size st.trail); Vec.push st.elt_levels (Vec.size st.trail); - Vec.push st.th_levels (Plugin.current_level ()); (* save the current theory state *) + Vec.push st.backtrack_levels (Vec.size st.backtrack); (* save the current theory state *) () (* Attach/Detach a clause. @@ -408,6 +347,15 @@ module Make c.attached <- true; () + let backtrack_down_to (st:t) (l:int): unit = + Log.debugf 2 + (fun k->k "@{** now at level %d (backtrack)@}" l); + while Vec.size st.backtrack > l do + let f = Vec.pop_last st.backtrack in + f() + done; + () + (* Backtracking. Used to backtrack, i.e cancel down to [lvl] excluded, i.e we want to go back to the state the solver was in @@ -426,46 +374,35 @@ module Make (* Now we need to cleanup the vars that are not valid anymore (i.e to the right of elt_head in the queue. *) for c = st.elt_head to Vec.size st.trail - 1 do - match (Vec.get st.trail c) with + let a = Vec.get st.trail c in (* A literal is unassigned, we nedd to add it back to the heap of potentially assignable literals, unless it has a level lower than [lvl], in which case we just move it back. *) - | Lit l -> - if l.l_level <= lvl then ( - Vec.set st.trail !head (Trail_elt.of_lit l); - head := !head + 1 - ) else ( - l.assigned <- None; - l.l_level <- -1; - insert_var_order st (Elt.of_lit l) - ) - (* A variable is not true/false anymore, one of two things can happen: *) - | Atom a -> - if a.var.v_level <= lvl then ( - (* It is a late propagation, which has a level - lower than where we backtrack, so we just move it to the head - of the queue, to be propagated again. *) - Vec.set st.trail !head (Trail_elt.of_atom a); - head := !head + 1 - ) else ( - (* it is a result of bolean propagation, or a semantic propagation - with a level higher than the level to which we backtrack, - in that case, we simply unset its value and reinsert it into the heap. *) - a.is_true <- false; - a.neg.is_true <- false; - a.var.v_level <- -1; - a.var.reason <- None; - insert_var_order st (Elt.of_var a.var) - ) + if a.var.v_level <= lvl then ( + (* It is a late propagation, which has a level + lower than where we backtrack, so we just move it to the head + of the queue, to be propagated again. *) + Vec.set st.trail !head a; + head := !head + 1 + ) else ( + (* it is a result of bolean propagation, or a semantic propagation + with a level higher than the level to which we backtrack, + in that case, we simply unset its value and reinsert it into the heap. *) + a.is_true <- false; + a.neg.is_true <- false; + a.var.v_level <- -1; + a.var.reason <- None; + insert_var_order st a.var + ) done; (* Recover the right theory state. *) - Plugin.backtrack (Vec.get st.th_levels lvl); + backtrack_down_to st (Vec.get st.backtrack_levels lvl); (* Resize the vectors according to their new size. *) Vec.shrink st.trail !head; Vec.shrink st.elt_levels lvl; - Vec.shrink st.th_levels lvl; + Vec.shrink st.backtrack_levels lvl; ); - assert (Vec.size st.elt_levels = Vec.size st.th_levels); + assert (Vec.size st.elt_levels = Vec.size st.backtrack_levels); () (* Unsatisfiability is signaled through an exception, since it can happen @@ -527,36 +464,11 @@ module Make a.is_true <- true; a.var.v_level <- lvl; a.var.reason <- Some reason; - Vec.push st.trail (Trail_elt.of_atom a); + Vec.push st.trail a; Log.debugf debug (fun k->k "Enqueue (%d): %a" (Vec.size st.trail) Atom.debug a); () - let enqueue_semantic st a terms = - if not a.is_true then ( - let l = List.map (Lit.make st.st) terms in - let lvl = List.fold_left (fun acc {l_level; _} -> - assert (l_level > 0); max acc l_level) 0 l in - H.grow_to_at_least st.order (St.nb_elt st.st); - enqueue_bool st a ~level:lvl Semantic - ) - - (* MCsat semantic assignment *) - let enqueue_assign st l value lvl = - match l.assigned with - | Some _ -> - Log.debugf error - (fun k -> k "Trying to assign an already assigned literal: %a" Lit.debug l); - assert false - | None -> - assert (l.l_level < 0); - l.assigned <- Some value; - l.l_level <- lvl; - Vec.push st.trail (Trail_elt.of_lit l); - Log.debugf debug - (fun k -> k "Enqueue (%d): %a" (Vec.size st.trail) Lit.debug l); - () - (* swap elements of array *) let[@inline] swap_arr a i j = if i<>j then ( @@ -584,17 +496,6 @@ module Make )) arr - (* evaluate an atom for MCsat, if it's not assigned - by boolean propagation/decision *) - let th_eval st a : bool option = - if a.is_true || a.neg.is_true then None - else match Plugin.eval a.lit with - | Plugin_intf.Unknown -> None - | Plugin_intf.Valued (b, l) -> - let atom = if b then a else a.neg in - enqueue_semantic st atom l; - Some b - (* find which level to backtrack to, given a conflict clause and a boolean stating whether it is a UIP ("Unique Implication Point") @@ -626,9 +527,7 @@ module Make cr_is_uip: bool; (* conflict is UIP? *) } - let get_atom st i = - match Vec.get st.trail i with - | Lit _ -> assert false | Atom x -> x + let[@inline] get_atom st i = Vec.get st.trail i (* conflict analysis for SAT Same idea as the mcsat analyze function (without semantic propagations), @@ -690,12 +589,8 @@ module Make (* look for the next node to expand *) while let a = Vec.get st.trail !tr_ind in - Log.debugf debug (fun k -> k " looking at: %a" Trail_elt.debug a); - match a with - | Atom q -> - (not (Var.seen_both q.var)) || - (q.var.v_level < conflict_level) - | Lit _ -> true + Log.debugf debug (fun k -> k " looking at: %a" St.Atom.debug a); + (not (Var.seen_both a.var)) || (a.var.v_level < conflict_level) do decr tr_ind; done; @@ -792,7 +687,7 @@ module Make Log.debugf debug (fun k -> k "Adding clause: @[%a@]" Clause.debug init); (* Insertion of new lits is done before simplification. Indeed, else a lit in a trivial clause could end up being not decided on, which is a bug. *) - Array.iter (fun x -> insert_var_order st (Elt.of_var x.var)) init.atoms; + Array.iter (fun x -> insert_var_order st x.var) init.atoms; let vec = clause_vector st init in try let c = eliminate_duplicates init in @@ -909,13 +804,7 @@ module Make st.elt_head <- Vec.size st.trail; raise (Conflict c) ) else ( - match th_eval st first with - | None -> (* clause is unit, keep the same watches, but propagate *) - enqueue_bool st first ~level:(decision_level st) (Bcp c) - | Some true -> () - | Some false -> - st.elt_head <- Vec.size st.trail; - raise (Conflict c) + enqueue_bool st first ~level:(decision_level st) (Bcp c) ); Watch_kept with Exit -> @@ -950,18 +839,14 @@ module Make () (* Propagation (boolean and theory) *) - let create_atom st f = - let a = mk_atom st f in - ignore (th_eval st a); - a + let[@inline] create_atom st f = mk_atom st f - let slice_get st i = - match Vec.get st.trail i with - | Atom a -> - Plugin_intf.Lit a.lit - | Lit {term; assigned = Some v; _} -> - Plugin_intf.Assign (term, v) - | Lit _ -> assert false + let slice_iter st (f:_ -> unit) : unit = + let n = Vec.size st.trail in + for i = st.th_head to n-1 do + let a = Vec.get st.trail i in + f a.lit + done let slice_push st (l:formula list) (lemma:proof): unit = let atoms = List.rev_map (create_atom st) l in @@ -969,45 +854,61 @@ module Make 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 -> - let a = mk_atom st f in - enqueue_semantic st a l - | Plugin_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 - let c = Clause.make (p :: List.map Atom.neg l) (Lemma proof) in - if p.is_true then () - else if p.neg.is_true then ( - Stack.push c st.clauses_to_add - ) else ( - H.grow_to_at_least st.order (St.nb_elt st.st); - insert_subterms_order st p.var; - enqueue_bool st p ~level:(decision_level st) (Bcp c) - ) + let slice_propagate (st:t) f causes proof : unit = + 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 + let c = Clause.make (p :: List.map Atom.neg l) (Lemma proof) in + if p.is_true then () + else if p.neg.is_true then ( + Stack.push c st.clauses_to_add ) else ( - invalid_arg "Msat.Internal.slice_propagate" + H.grow_to_at_least st.order (St.nb_elt st.st); + insert_var_order st p.var; + enqueue_bool st p ~level:(decision_level st) (Bcp c) ) + ) else ( + invalid_arg "the solver.Internal.slice_propagate" + ) - let current_slice st : (_,_,_) Plugin_intf.slice = { - Plugin_intf.start = st.th_head; - length = Vec.size st.trail - st.th_head; - get = slice_get st; - push = slice_push st; - propagate = slice_propagate st; + let slice_on_backtrack st f : unit = + Vec.push st.backtrack f + + let slice_at_level_0 st () : bool = + Vec.is_empty st.backtrack_levels + + let current_slice st = Theory_intf.Slice_acts { + slice_iter = slice_iter st; + slice_propagate = slice_propagate st; } (* full slice, for [if_sat] final check *) - let full_slice st : (_,_,_) Plugin_intf.slice = { - Plugin_intf.start = 0; - length = Vec.size st.trail; - get = slice_get st; - push = slice_push st; - propagate = (fun _ -> assert false); + let full_slice st = Theory_intf.Slice_acts { + slice_iter = slice_iter st; + slice_propagate = slice_propagate st; } - (* some boolean literals were decided/propagated within Msat. Now we + let actions st = Theory_intf.Actions { + push = slice_push st; + on_backtrack = slice_on_backtrack st; + at_level_0 = slice_at_level_0 st; + } + + let create ?(size=`Big) ?st () : t = + let st = match st with Some s -> s | None -> St.create ~size () in + let size_trail, size_lvl = match size with + | `Tiny -> 0, 0 + | `Small -> 32, 16 + | `Big -> 600, 50 + in + let rec solver = lazy ( + create_ ~st ~size_trail ~size_lvl th + ) and th = lazy ( + Th.create (actions (Lazy.force solver)) + ) in + Lazy.force solver + + (* some boolean literals were decided/propagated within the solver. Now we need to inform the theory of those assumptions, so it can do its job. @return the conflict clause, if the theory detects unsatisfiability *) let rec theory_propagate st : clause option = @@ -1018,14 +919,14 @@ module Make ) else ( let slice = current_slice st in st.th_head <- st.elt_head; (* catch up *) - match Plugin.assume slice with - | Plugin_intf.Sat -> + match Th.assume (theory st) slice with + | Theory_intf.Sat -> propagate st - | Plugin_intf.Unsat (l, p) -> + | Theory_intf.Unsat (l, p) -> (* conflict *) let l = List.rev_map (create_atom st) l in H.grow_to_at_least st.order (St.nb_elt st.st); - List.iter (fun a -> insert_var_order st (Elt.of_var a.var)) l; + List.iter (fun a -> insert_var_order st a.var) l; let c = St.Clause.make l (Lemma p) in Some c ) @@ -1043,12 +944,9 @@ module Make let num_props = ref 0 in let res = ref None in while st.elt_head < Vec.size st.trail do - begin match Vec.get st.trail st.elt_head with - | Lit _ -> () - | Atom a -> - incr num_props; - propagate_atom st a res - end; + let a = Vec.get st.trail st.elt_head in + incr num_props; + propagate_atom st a res; st.elt_head <- st.elt_head + 1; done; match !res with @@ -1067,14 +965,11 @@ 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 atom.lit with - | Plugin_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) -> - 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 @@ -1083,17 +978,7 @@ module Make pick_branch_aux st atom | None -> begin match H.remove_min st.order with - | E_lit l -> - if Lit.level l >= 0 then - pick_branch_lit st - else ( - let value = Plugin.assign l.term in - new_decision_level st; - let current_level = decision_level st in - enqueue_assign st l value current_level - ) - | E_var v -> - pick_branch_aux st v.pa + | v -> pick_branch_aux st v.pa | exception Not_found -> raise Sat end @@ -1140,8 +1025,8 @@ module Make 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 + | Theory_intf.Negated -> not truth + | Theory_intf.Same_sign -> truth in value, var.v_level @@ -1149,14 +1034,6 @@ module Make let[@inline] unsat_conflict st = st.unsat_conflict - let model (st:t) : (term * term) list = - let opt = function Some a -> a | None -> assert false in - Vec.fold - (fun acc e -> match e with - | Lit v -> (v.term, opt v.assigned) :: acc - | Atom _ -> acc) - [] st.trail - (* fixpoint of propagation and decisions until a model is found, or a conflict is reached *) let solve (st:t) : unit = @@ -1174,9 +1051,9 @@ module Make n_of_learnts := !n_of_learnts *. learntsize_inc | Sat -> assert (st.elt_head = Vec.size st.trail); - begin match Plugin.if_sat (full_slice st) with - | Plugin_intf.Sat -> () - | Plugin_intf.Unsat (l, p) -> + begin match Th.if_sat (theory st) (full_slice st) with + | Theory_intf.Sat -> () + | Theory_intf.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); @@ -1202,14 +1079,14 @@ module Make cancel_until st (base_level st); Log.debugf debug (fun k -> k "@[Status:@,@[trail: %d - %d@,%a@]" - st.elt_head st.th_head (Vec.print ~sep:"" Trail_elt.debug) st.trail); + st.elt_head st.th_head (Vec.print ~sep:"" Atom.debug) st.trail); begin match propagate st with | Some confl -> report_unsat st confl | None -> Log.debugf debug (fun k -> k "@[Current trail:@,@[%a@]@]" - (Vec.print ~sep:"" Trail_elt.debug) st.trail); + (Vec.print ~sep:"" Atom.debug) st.trail); Log.debug info "Creating new user level"; new_decision_level st; Vec.push st.user_levels (Vec.size st.clauses_temp); diff --git a/src/core/Msat.ml b/src/core/Msat.ml index daa470c2..b1ad22c9 100644 --- a/src/core/Msat.ml +++ b/src/core/Msat.ml @@ -1,37 +1,57 @@ (** 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 Config = Config module Res = Res module type S = Solver_intf.S -type ('term, 'form) sat_state = ('term, 'form) Solver_intf.sat_state = { +type negated = Theory_intf.negated = + | Negated + | Same_sign + +type ('formula, 'proof) res = ('formula, 'proof) Theory_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 sat_state = 'form Solver_intf.sat_state = Sat_state of { eval : 'form -> bool; eval_level : 'form -> bool * int; - iter_trail : ('form -> unit) -> ('term -> unit) -> unit; - model : unit -> ('term * 'term) list; + iter_trail : ('form -> unit) -> unit; } -type ('clause, 'proof) unsat_state = ('clause, 'proof) Solver_intf.unsat_state = { +type ('clause, 'proof) unsat_state = ('clause, 'proof) Solver_intf.unsat_state = Unsat_state of { unsat_conflict : unit -> 'clause; get_proof : unit -> 'proof; } + type 'clause export = 'clause Solver_intf.export = { hyps : 'clause Vec.t; history : 'clause Vec.t; local : 'clause Vec.t; } -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 ('form, 'proof) actions = ('form,'proof) Theory_intf.actions = Actions of { + push : 'form list -> 'proof -> unit; + on_backtrack: (unit -> unit) -> unit; + at_level_0 : unit -> bool; +} -module Make = Solver.Make +type ('form, 'proof) slice_actions = ('form, 'proof) Theory_intf.slice_actions = Slice_acts of { + slice_iter : ('form -> unit) -> unit; + slice_propagate : 'form -> 'form list -> 'proof -> unit; +} + +module Make(E : Theory_intf.S) = Solver.Make(Solver_types.Make(E))(E) (**/**) module Vec = Vec diff --git a/src/core/Plugin_intf.ml b/src/core/Plugin_intf.ml deleted file mode 100644 index 92d1b2e4..00000000 --- a/src/core/Plugin_intf.ml +++ /dev/null @@ -1,121 +0,0 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon, Evelyne Contejean *) -(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) -(* CNRS, Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.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. *) - -module type S = sig - (** Signature for theories to be given to the Model Constructing Solver. *) - - 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 dummy : level - (** A dummy level. *) - - val current_level : unit -> level - (** Return the current level of the theory (either the empty/beginning state, or the - last level returned by the [assume] function). *) - - val assume : (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 : (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 : 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 : term -> term - (** Returns an assignment value for the given term. *) - - val iter_assignable : (term -> unit) -> formula -> unit - (** An iterator over the subterms of a formula that should be assigned a value (usually the poure subterms) *) - - val eval : formula -> term eval_res - (** Returns the evaluation of the formula in the current assignment *) - -end - diff --git a/src/core/Solver.ml b/src/core/Solver.ml index 883636f0..b8a87d01 100644 --- a/src/core/Solver.ml +++ b/src/core/Solver.ml @@ -10,8 +10,7 @@ open Solver_intf module Make (St : Solver_types.S) - (Th : Plugin_intf.S with type term = St.term - and type formula = St.formula + (Th : Theory_intf.S with type formula = St.formula and type proof = St.proof) = struct @@ -24,18 +23,18 @@ module Make 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[@inline] create ?size () = S.create ?size () + let[@inline] create ?size () : t = S.create ?size () (* Result type *) type res = - | Sat of (St.term,St.formula) sat_state + | Sat of St.formula sat_state | Unsat of (St.clause,Proof.proof) unsat_state let pp_all st lvl status = @@ -44,26 +43,19 @@ module Make "@[%s - Full resume:@,@[Trail:@\n%a@]@,\ @[Temp:@\n%a@]@,@[Hyps:@\n%a@]@,@[Lemmas:@\n%a@]@,@]@." status - (Vec.print ~sep:"" St.Trail_elt.debug) (S.trail st) + (Vec.print ~sep:"" St.Atom.debug) (S.trail st) (Vec.print ~sep:"" St.Clause.debug) (S.temp st) (Vec.print ~sep:"" St.Clause.debug) (S.hyps st) (Vec.print ~sep:"" St.Clause.debug) (S.history st) ) - let mk_sat (st:S.t) : (_,_) sat_state = + 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 - { + let iter f : unit = Vec.iter (fun a -> f a.St.lit) (S.trail st) in + Sat_state { 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 = @@ -77,7 +69,7 @@ module Make let c = unsat_conflict () in S.Proof.prove_unsat c in - { unsat_conflict; get_proof; } + Unsat_state { unsat_conflict; get_proof; } (* clean local state *) let[@inline] cleanup_ (st:t) : unit = @@ -86,6 +78,8 @@ module Make st.S.dirty <- false; ) + let theory = S.theory + (* Wrappers around internal functions*) let[@inline] assume st ?tag cls : unit = cleanup_ st; @@ -124,14 +118,12 @@ module Make 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 actions = S.actions + let export (st:t) : St.clause export = let hyps = S.hyps st in let history = S.history st in @@ -150,5 +142,4 @@ module Make end module Formula = St.Formula - module Term = St.Term end diff --git a/src/core/Solver.mli b/src/core/Solver.mli index 3272a62b..1a18d7cf 100644 --- a/src/core/Solver.mli +++ b/src/core/Solver.mli @@ -4,7 +4,7 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -(** mSAT safe interface +(** SAT safe interface This module defines a safe interface for the core solver. It is the basis of the {!module:Solver} and {!module:Mcsolver} modules. @@ -15,13 +15,12 @@ module type S = Solver_intf.S module Make (St : Solver_types.S) - (Th : Plugin_intf.S with type term = St.term - and type formula = St.formula + (Th : Theory_intf.S with type formula = St.formula and type proof = St.proof) - : S with type term = St.term - and type formula = St.formula + : S with type formula = St.formula and type clause = St.clause and type Proof.lemma = St.proof + and type theory = Th.t (** Functor to make a safe external interface. *) diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml index aebfe2b2..76db6216 100644 --- a/src/core/Solver_intf.ml +++ b/src/core/Solver_intf.ml @@ -1,9 +1,3 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -Copyright 2016 Simon Cruanes -*) - (** Interface for Solvers This modules defines the safe external interface for solvers. @@ -11,7 +5,7 @@ Copyright 2016 Simon Cruanes functor in {!Solver} or {!Mcsolver}. *) -type ('term, 'form) sat_state = { +type 'form sat_state = Sat_state of { eval: 'form -> bool; (** Returns the valuation of a formula in the current state of the sat solver. @@ -22,15 +16,13 @@ type ('term, 'form) sat_state = { the atom to have this value; otherwise it is due to choices that can potentially be backtracked. @raise UndecidedLit if the literal is not decided *) - iter_trail : ('form -> unit) -> ('term -> unit) -> unit; - (** Iter thorugh the formulas and terms in order of decision/propagation + iter_trail : ('form -> unit) -> unit; + (** Iter through the formulas and terms in order of decision/propagation (starting from the first propagation, to the last propagation). *) - model: unit -> ('term * 'term) list; - (** Returns the model found if the formula is satisfiable. *) } (** The type of values returned when the solver reaches a SAT state. *) -type ('clause, 'proof) unsat_state = { +type ('clause, 'proof) unsat_state = Unsat_state of { unsat_conflict : unit -> 'clause; (** Returns the unsat clause found at the toplevel *) get_proof : unit -> 'proof; @@ -54,12 +46,12 @@ 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 *) - type formula (** user formulas *) type clause + type theory (** user theory *) + module Proof : Res.S with type clause = clause (** A module to manipulate proofs. *) @@ -80,7 +72,7 @@ module type S = sig (** Result type for the solver *) type res = - | Sat of (term,formula) sat_state (** Returned when the solver reaches SAT, with a model *) + | Sat of 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 *) exception UndecidedLit @@ -89,6 +81,8 @@ module type S = sig (** {2 Base operations} *) + val theory : t -> theory + val assume : t -> ?tag:int -> atom list list -> unit (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. *) @@ -102,11 +96,6 @@ module type S = sig The assumptions are just used for this call to [solve], they are not saved in the solver's state. *) - val new_lit : t -> term -> unit - (** Add a new litteral (i.e term) to the solver. This term will - be decided on at some point during solving, wether it appears - in clauses or not. *) - val new_atom : t -> atom -> unit (** Add a new atom (i.e propositional formula) to the solver. This formula will be decided on at some point during solving, @@ -132,6 +121,9 @@ module type S = sig (** Return to last save point, discarding clauses added since last call to [push] *) + val actions : t -> (formula,Proof.lemma) Theory_intf.actions + (** Obtain actions *) + val export : t -> clause export (** {2 Re-export some functions} *) @@ -155,10 +147,5 @@ module type S = sig type t = formula val pp : t printer end - - module Term : sig - type t = term - val pp : t printer - end end diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml index 5e2686ab..a29743e1 100644 --- a/src/core/Solver_types.ml +++ b/src/core/Solver_types.ml @@ -1,21 +1,3 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.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 module Var_fields = Solver_types_intf.Var_fields @@ -27,32 +9,17 @@ let () = Var_fields.freeze() (* Solver types for McSat Solving *) (* ************************************************************************ *) -module McMake (E : Expr_intf.S) = struct +module Make (E : Theory_intf.S) = struct - (* Flag for Mcsat v.s Pure Sat *) - let mcsat = true - - type term = E.Term.t - type formula = E.Formula.t + type formula = E.Form.t type proof = E.proof - let pp_form = E.Formula.dummy - 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; @@ -61,7 +28,6 @@ module McMake (E : Expr_intf.S) = struct 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; } @@ -95,14 +61,6 @@ module McMake (E : Expr_intf.S) = struct | 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 - let rec dummy_var = { vid = -101; pa = dummy_atom; @@ -111,12 +69,11 @@ module McMake (E : Expr_intf.S) = struct v_level = -1; v_weight = -1.; v_idx= -1; - v_assignable = None; reason = None; } and dummy_atom = { var = dummy_var; - lit = E.Formula.dummy; + lit = E.Form.dummy; watched = Obj.magic 0; (* should be [Vec.make_empty dummy_clause] but we have to break the cycle *) @@ -135,13 +92,11 @@ module McMake (E : Expr_intf.S) = struct let () = dummy_atom.watched <- Vec.make_empty dummy_clause (* Constructors *) - module MF = Hashtbl.Make(E.Formula) - module MT = Hashtbl.Make(E.Term) + module MF = Hashtbl.Make(E.Form) type t = { - t_map: lit MT.t; f_map: var MF.t; - vars: elt Vec.t; + vars: var Vec.t; mutable cpt_mk_var: int; mutable cpt_mk_clause: int; } @@ -150,8 +105,7 @@ module McMake (E : Expr_intf.S) = struct let create_ size_map size_vars () : t = { f_map = MF.create size_map; - t_map = MT.create size_map; - vars = Vec.make size_vars (E_var dummy_var); + vars = Vec.make size_vars dummy_var; cpt_mk_var = 0; cpt_mk_clause = 0; } @@ -174,42 +128,6 @@ module McMake (E : Expr_intf.S) = struct | 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.print t - - let pp out v = E.Term.print out v.term - let debug out v = - Format.fprintf out "%d[%a][lit:@[%a@]]" - (v.lid+1) debug_assign v E.Term.print v.term - end - module Var = struct type t = var let dummy = dummy_var @@ -217,11 +135,18 @@ module McMake (E : Expr_intf.S) = struct 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 + let[@inline] id v =v.vid + let[@inline] level v =v.v_level + let[@inline] idx v = v.v_idx + + let[@inline] set_level v lvl = v.v_level <- lvl + let[@inline] set_idx v i = v.v_idx <- i + let[@inline] set_weight v w = v.v_weight <- w + + let make (st:state) (t:formula) : var * Theory_intf.negated = + let lit, negated = E.Form.norm t in try MF.find st.f_map lit, negated with Not_found -> @@ -234,7 +159,6 @@ module McMake (E : Expr_intf.S) = struct v_level = -1; v_idx= -1; v_weight = 0.; - v_assignable = None; reason = None; } and pa = @@ -246,14 +170,14 @@ module McMake (E : Expr_intf.S) = struct aid = cpt_double (* aid = vid*2 *) } and na = { var = var; - lit = E.Formula.neg lit; + lit = E.Form.neg lit; watched = Vec.make 10 dummy_clause; 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); + Vec.push st.vars var; var, negated (* Marking helpers *) @@ -296,10 +220,10 @@ module McMake (E : Expr_intf.S) = struct 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 + | Theory_intf.Negated -> var.na + | Theory_intf.Same_sign -> var.pa - let pp fmt a = E.Formula.print fmt a.lit + let pp fmt a = E.Form.print fmt a.lit let pp_a fmt v = if Array.length v = 0 then ( @@ -341,45 +265,12 @@ module McMake (E : Expr_intf.S) = struct let debug out a = Format.fprintf out "%s%d[%a][atom:@[%a@]]" - (sign a) (a.var.vid+1) debug_value a E.Formula.print a.lit + (sign a) (a.var.vid+1) debug_value a E.Form.print 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 dummy = dummy_clause @@ -449,28 +340,8 @@ module McMake (E : Expr_intf.S) = struct Format.fprintf fmt "%a0" aux atoms end - module Term = struct - include E.Term - let pp = print - end - module Formula = struct - include E.Formula + include E.Form let pp = print end 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 index 4d12d93d..410fe175 100644 --- a/src/core/Solver_types.mli +++ b/src/core/Solver_types.mli @@ -1,20 +1,3 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -Copyright 2016 Simon Cruanes -*) (** Internal types (implementation) @@ -30,11 +13,8 @@ module type S = Solver_types_intf.S module Var_fields = Solver_types_intf.Var_fields -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 +module Make (E : Theory_intf.S): + S with type formula = E.formula + 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 index f5076d30..9f2fc712 100644 --- a/src/core/Solver_types_intf.ml +++ b/src/core/Solver_types_intf.ml @@ -1,21 +1,3 @@ -(**************************************************************************) -(* *) -(* Cubicle *) -(* Combining model checking algorithms and SMT solvers *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.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 @@ -29,9 +11,6 @@ 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 *) @@ -39,10 +18,9 @@ module type S = sig (** {2 Type definitions} *) - type term type formula type proof - (** The types of terms, formulas and proofs. All of these are user-provided. *) + (** The types of formulas and proofs. All of these are user-provided. *) type seen = | Nope @@ -54,16 +32,6 @@ module type S = sig 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 *) @@ -72,8 +40,6 @@ module type S = sig 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 *) } @@ -131,41 +97,18 @@ module type S = sig 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 + val get_elt : t -> int -> var + val iter_elt : t -> (var -> 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 dummy : t @@ -174,11 +117,15 @@ module type S = sig val neg : t -> atom val level : t -> int + val idx : 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 + val set_level : t -> int -> unit + val set_idx : t -> int -> unit + val set_weight : t -> float -> unit + + val make : state -> formula -> t * Theory_intf.negated (** Returns the variable linked with the given formula, and whether the atom associated with the formula is [var.pa] or [var.na] *) @@ -221,22 +168,6 @@ module type S = sig 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 dummy : t @@ -262,22 +193,6 @@ module type S = sig 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 diff --git a/src/core/Theory_intf.ml b/src/core/Theory_intf.ml index b465f4c9..6ab3e9e3 100644 --- a/src/core/Theory_intf.ml +++ b/src/core/Theory_intf.ml @@ -23,24 +23,40 @@ Copyright 2016 Simon Cruanes be used in an SMT solver. *) -type ('formula, 'proof) res = ('formula, 'proof) Plugin_intf.res = +(** This type is used during the normalisation of formulas. + See {!val:Expr_intf.S.norm} for more details. *) +type negated = + | Negated (** changed sign *) + | Same_sign (** kept sign *) + +(** 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 ('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 ('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; +(** Actions given to the theory during initialization, to be used + at any time *) +type ('form, 'proof) actions = Actions of { + push : 'form list -> 'proof -> unit; + (** Allows to add a clause to the solver. *) + + on_backtrack: (unit -> unit) -> unit; + (** [on_backtrack f] calls [f] when the main solver backtracks *) + + at_level_0 : unit -> bool; + (** Are we at level 0? *) +} + +type ('form, 'proof) slice_actions = Slice_acts of { + slice_iter : ('form -> unit) -> unit; + (** iterate on the slice of the trail *) + + slice_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, @@ -50,8 +66,10 @@ type ('form, 'proof) slice = { propagation queue. They allow to look at the propagated literals, and to add new clauses to the solver. *) +(** {2 Signature for theories to be given to the Solver.} *) module type S = sig - (** Signature for theories to be given to the Solver. *) + type t + (** State of the theory *) type formula (** The type of formulas. Should be compatble with Formula_intf.S *) @@ -59,27 +77,44 @@ module type S = sig type proof (** A custom type for the proofs of lemmas produced by the theory. *) - type level - (** The type for levels to allow backtracking. *) + module Form : sig + type t = formula + (** The type of atomic formulas. *) - val dummy : level - (** A dummy level. *) + val equal : t -> t -> bool + (** Equality over formulas. *) - val current_level : unit -> level - (** Return the current level of the theory (either the empty/beginning state, or the - last level returned by the [assume] function). *) + 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 assume : (formula, proof) slice -> (formula, proof) res + val print : Format.formatter -> t -> unit + (** Printing function used among other thing for debugging. *) + + val dummy : t + (** Formula constant. A valid formula should never be physically equal to [dummy] *) + + 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 + + val create : (formula, proof) actions -> t + (** Create a new instance of the theory *) + + val assume : t -> (formula, proof) slice_actions -> (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 : (formula, proof) slice -> (formula, proof) res + val if_sat : t -> (formula, proof) slice_actions -> (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 : 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 diff --git a/src/main/jbuild b/src/main/jbuild deleted file mode 100644 index 8de51a2e..00000000 --- a/src/main/jbuild +++ /dev/null @@ -1,13 +0,0 @@ - -; vim:ft=lisp: - -; main binary -(executable - ((name main) - (public_name msat_solver) - (package minismt) - (libraries (msat msat.backend minismt.sat minismt.smt minismt.mcsat dolmen)) - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) - (ocamlopt_flags (:standard -O3 -color always - -unbox-closures -unbox-closures-factor 20)) - )) diff --git a/src/mcsat/README.md b/src/main_test/README.md similarity index 100% rename from src/mcsat/README.md rename to src/main_test/README.md diff --git a/src/solver/jbuild b/src/main_test/jbuild similarity index 67% rename from src/solver/jbuild rename to src/main_test/jbuild index f3176323..cc91b1f2 100644 --- a/src/solver/jbuild +++ b/src/main_test/jbuild @@ -1,10 +1,8 @@ ; vim:ft=lisp: -(library - ((name minismt) - (public_name minismt) - (libraries (msat dolmen)) - (synopsis "minismt") +(executable + ((name msat_test) + (libraries (msat msat.backend msat.tseitin msat.sat dolmen)) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) (ocamlopt_flags (:standard -O3 -bin-annot -unbox-closures -unbox-closures-factor 20)) diff --git a/src/main/main.ml b/src/main_test/msat_test.ml similarity index 87% rename from src/main/main.ml rename to src/main_test/msat_test.ml index c943952e..6f6228ff 100644 --- a/src/main/main.ml +++ b/src/main_test/msat_test.ml @@ -4,8 +4,6 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -open Msat - exception Incorrect_model exception Out_of_time exception Out_of_space @@ -28,7 +26,13 @@ end module Make (S : Msat.S) - (T : Minismt.Type.S with type atom := S.atom) + (Th : sig + include Msat.Theory_intf.S with type t = S.theory + end) + (T : sig + include Type.S with type atom := S.atom + val create : Th.t -> t + end) : sig val do_task : Dolmen.Statement.t -> unit end = struct @@ -38,13 +42,15 @@ module Make let hyps = ref [] let st = S.create ~size:`Big () + let th = S.theory st + let t_st = T.create th - let check_model sat = + let check_model (Msat.Sat_state sat) = let check_clause c = let l = List.map (function a -> Log.debugf 99 (fun k -> k "Checking value of %a" S.Formula.pp a); - sat.Msat.eval a) c in + sat.eval a) c in List.exists (fun x -> x) l in let l = List.map check_clause !hyps in @@ -60,9 +66,9 @@ module Make raise Incorrect_model; let t' = Sys.time () -. t in Format.printf "Sat (%f/%f)@." t t' - | S.Unsat state -> + | S.Unsat (Msat.Unsat_state us) -> if !p_check then begin - let p = state.Msat.get_proof () in + let p = us.get_proof () in S.Proof.check p; if !p_dot_proof <> "" then begin let fmt = Format.formatter_of_out_channel (open_out !p_dot_proof) in @@ -73,20 +79,20 @@ module Make Format.printf "Unsat (%f/%f)@." t t' end - let do_task s = + let do_task s : unit = match s.Dolmen.Statement.descr with - | Dolmen.Statement.Def (id, t) -> T.def id t - | Dolmen.Statement.Decl (id, t) -> T.decl id t + | Dolmen.Statement.Def (id, t) -> T.def t_st id t + | Dolmen.Statement.Decl (id, t) -> T.decl t_st id t | Dolmen.Statement.Clause l -> - let cnf = T.antecedent (Dolmen.Term.or_ l) in + let cnf = T.antecedent t_st (Dolmen.Term.or_ l) in hyps := cnf @ !hyps; S.assume st cnf | Dolmen.Statement.Consequent t -> - let cnf = T.consequent t in + let cnf = T.consequent t_st t in hyps := cnf @ !hyps; S.assume st cnf | Dolmen.Statement.Antecedent t -> - let cnf = T.antecedent t in + let cnf = T.antecedent t_st t in hyps := cnf @ !hyps; S.assume st cnf | Dolmen.Statement.Pack [ @@ -95,7 +101,7 @@ module Make { Dolmen.Statement.descr = Dolmen.Statement.Prove;_ }; { Dolmen.Statement.descr = Dolmen.Statement.Pop 1;_ }; ] -> - let assumptions = T.assumptions f in + let assumptions = T.assumptions t_st f in prove ~assumptions () | Dolmen.Statement.Prove -> prove ~assumptions:[] () @@ -107,15 +113,17 @@ module Make Dolmen.Statement.print s end -module Sat = Make(Minismt_sat)(Minismt_sat.Type) -module Smt = Make(Minismt_smt)(Minismt_smt.Type) -module Mcsat = Make(Minismt_mcsat)(Minismt_smt.Type) +module Sat = Make(Msat_sat)(Msat_sat.Th)(Type_sat) + (* +module Smt = Make(Minismt_smt)(Msat_sat.Th)(Minismt_smt.Type) + *) let solver = ref (module Sat : S) let solver_list = [ "sat", (module Sat : S); +(* FIXME "smt", (module Smt : S); - "mcsat", (module Mcsat : S); +*) ] let error_msg opt arg l = @@ -228,8 +236,10 @@ let () = | Incorrect_model -> Format.printf "Internal error : incorrect *sat* model@."; exit 4 - | Minismt_sat.Type.Typing_error (msg, t) - | Minismt_smt.Type.Typing_error (msg, t) -> + (* FIXME + | Minismt_smt.Type.Typing_error (msg, t) + *) + | Type_sat.Typing_error (msg, t) -> let b = Printexc.get_backtrace () in let loc = match t.Dolmen.Term.loc with | Some l -> l | None -> Dolmen.ParseLocation.mk "<>" 0 0 0 0 diff --git a/src/main_test/solver.ml b/src/main_test/solver.ml new file mode 100644 index 00000000..70644d58 --- /dev/null +++ b/src/main_test/solver.ml @@ -0,0 +1,18 @@ +(**************************************************************************) +(* *) +(* Alt-Ergo Zero *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +module type S = Msat.S + + +module Make (Th : Theory_intf.S) = Msat.Make(Th) + + diff --git a/src/solver/solver.mli b/src/main_test/solver.mli similarity index 55% rename from src/solver/solver.mli rename to src/main_test/solver.mli index 77efd675..63ee926d 100644 --- a/src/solver/solver.mli +++ b/src/main_test/solver.mli @@ -14,17 +14,10 @@ Copyright 2014 Simon Cruanes module type S = Msat.S (** The interface of instantiated solvers. *) -module DummyTheory(F : Formula_intf.S) : - Theory_intf.S with type formula = F.t - and type proof = F.proof -(** Simple case where the theory is empty and - the proof type is the one given in the formula interface *) - -module Make (F : Formula_intf.S) - (Th : Theory_intf.S with type formula = F.t - and type proof = F.proof) - : S with type formula = F.t - and type Proof.lemma = F.proof +module Make (Th : Theory_intf.S) + : S with type formula = Th.formula + and type Proof.lemma = Th.proof + and type theory = Th.t (** Functor to create a SMT Solver parametrised by the atomic formulas and a theory. *) diff --git a/src/smt/expr_smt.ml b/src/main_test/theory_smt.ml similarity index 70% rename from src/smt/expr_smt.ml rename to src/main_test/theory_smt.ml index f3b8961f..a24fbbcd 100644 --- a/src/smt/expr_smt.ml +++ b/src/main_test/theory_smt.ml @@ -499,10 +499,6 @@ module Atom = struct else mk_formula (Pred t) - let fresh () = - let id = Id.ty "fresh" Ty.prop in - pred (Term.of_id id) - let neg f = { f with sign = not f.sign } @@ -516,10 +512,198 @@ module Atom = struct let norm f = { f with sign = true }, - if f.sign then Formula_intf.Same_sign - else Formula_intf.Negated + if f.sign then Msat.Same_sign + else Msat.Negated end -module Formula = Msat_tseitin.Make(Atom) +module Ts_arg = struct + module Form = Atom + + type t = unit + + let fresh () : Form.t = + let id = Id.ty "fresh" Ty.prop in + Form.pred (Term.of_id id) + +end + + +module Formula = Msat_tseitin.Make(Ts_arg) + +(** {2 Theory} *) + +module E = Eclosure.Make(Term) +module H = Backtrack.Hashtbl(Term) +module M = Hashtbl.Make(Term) + +let uf acts = E.create acts + +let assign t = + match E.find_tag uf t with + | _, None -> t + | _, Some (_, v) -> v + +(* Propositional constants *) + +let true_ = Theory_smt.(Term.of_id (Id.ty "true" Ty.prop)) +let false_ = Theory_smt.(Term.of_id (Id.ty "false" Ty.prop)) + +(* Uninterpreted functions and predicates *) + +let map : Theory_smt.term H.t = H.create stack +let watch = M.create 4096 +let interpretation = H.create stack + +let pop_watches t = + try + let l = M.find watch t in + M.remove watch t; + l + with Not_found -> + [] + +let add_job j x = + let l = try M.find watch x with Not_found -> [] in + M.add watch x (j :: l) + +let update_job x ((t, watchees) as job) = + try + let y = List.find (fun y -> not (H.mem map y)) watchees in + add_job job y + with Not_found -> + add_job job x; + begin match t with + | { Theory_smt.term = Theory_smt.App (f, tys, l);_ } -> + let is_prop = Theory_smt.(Ty.equal t.t_type Ty.prop) in + let t_v = H.find map t in + let l' = List.map (H.find map) l in + let u = Theory_smt.Term.apply f tys l' in + begin try + let t', u_v = H.find interpretation u in + if not (Theory_smt.Term.equal t_v u_v) then begin + match t' with + | { Theory_smt.term = Theory_smt.App (_, _, r); _ } when is_prop -> + let eqs = List.map2 (fun a b -> Theory_smt.Atom.neg (Theory_smt.Atom.eq a b)) l r in + if Theory_smt.(Term.equal u_v true_) then begin + let res = Theory_smt.Atom.pred t :: + Theory_smt.Atom.neg (Theory_smt.Atom.pred t') :: eqs in + raise (Absurd res) + end else begin + let res = Theory_smt.Atom.pred t' :: + Theory_smt.Atom.neg (Theory_smt.Atom.pred t) :: eqs in + raise (Absurd res) + end + | { Theory_smt.term = Theory_smt.App (_, _, r); _ } -> + let eqs = List.map2 (fun a b -> Theory_smt.Atom.neg (Theory_smt.Atom.eq a b)) l r in + let res = Theory_smt.Atom.eq t t' :: eqs in + raise (Absurd res) + | _ -> assert false + end + with Not_found -> + H.add interpretation u (t, t_v); + end + | _ -> assert false + end + +let rec update_watches x = function + | [] -> () + | job :: r -> + begin + try + update_job x job; + with exn -> + List.iter (fun j -> add_job j x) r; + raise exn + end; + update_watches x r + +let add_watch t l = + update_job t (t, l) + +let add_assign t v = + H.add map t v; + update_watches t (pop_watches t) + +(* Assignemnts *) + +let rec iter_aux f = function + | { Theory_smt.term = Theory_smt.Var _; _ } as t -> + Log.debugf 10 (fun k -> k "Adding %a as assignable" Theory_smt.Term.print t); + f t + | { Theory_smt.term = Theory_smt.App (_, _, l); _ } as t -> + if l <> [] then add_watch t (t :: l); + List.iter (iter_aux f) l; + Log.debugf 10 (fun k -> k "Adding %a as assignable" Theory_smt.Term.print t); + f t + +let iter_assignable f = function + | { Theory_smt.atom = Theory_smt.Pred { Theory_smt.term = Theory_smt.Var _;_ }; _ } -> () + | { Theory_smt.atom = Theory_smt.Pred ({ Theory_smt.term = Theory_smt.App (_, _, l);_} as t); _ } -> + if l <> [] then add_watch t (t :: l); + List.iter (iter_aux f) l; + | { Theory_smt.atom = Theory_smt.Equal (a, b);_ } -> + iter_aux f a; iter_aux f b + +let eval = function + | { Theory_smt.atom = Theory_smt.Pred t; _ } -> + begin try + let v = H.find map t in + if Theory_smt.Term.equal v true_ then + Plugin_intf.Valued (true, [t]) + else if Theory_smt.Term.equal v false_ then + Plugin_intf.Valued (false, [t]) + else + Plugin_intf.Unknown + with Not_found -> + Plugin_intf.Unknown + end + | { Theory_smt.atom = Theory_smt.Equal (a, b); sign; _ } -> + begin try + let v_a = H.find map a in + let v_b = H.find map b in + if Theory_smt.Term.equal v_a v_b then + Plugin_intf.Valued(sign, [a; b]) + else + Plugin_intf.Valued(not sign, [a; b]) + with Not_found -> + Plugin_intf.Unknown + end + + +(* Theory propagation *) + +let rec chain_eq = function + | [] | [_] -> [] + | a :: ((b :: _) as l) -> (Theory_smt.Atom.eq a b) :: chain_eq l + +let assume s = + let open Plugin_intf in + try + for i = s.start to s.start + s.length - 1 do + match s.get i with + | Assign (t, v) -> + add_assign t v; + E.add_tag uf t v + | Lit f -> + begin match f with + | { Theory_smt.atom = Theory_smt.Equal (u, v); sign = true;_ } -> + E.add_eq uf u v + | { Theory_smt.atom = Theory_smt.Equal (u, v); sign = false;_ } -> + E.add_neq uf u v + | { Theory_smt.atom = Theory_smt.Pred p; sign;_ } -> + let v = if sign then true_ else false_ in + add_assign p v + end + done; + Plugin_intf.Sat + with + | Absurd l -> + Plugin_intf.Unsat (l, ()) + | E.Unsat (a, b, l) -> + let c = Theory_smt.Atom.eq a b :: List.map Theory_smt.Atom.neg (chain_eq l) in + Plugin_intf.Unsat (c, ()) + +let if_sat _ = + Plugin_intf.Sat diff --git a/src/smt/expr_smt.mli b/src/main_test/theory_smt.mli similarity index 98% rename from src/smt/expr_smt.mli rename to src/main_test/theory_smt.mli index 03f0b07c..dd5028e0 100644 --- a/src/smt/expr_smt.mli +++ b/src/main_test/theory_smt.mli @@ -304,9 +304,6 @@ module Atom : sig val dummy : atom (** A dummy atom, different from any other atom. *) - val fresh : unit -> atom - (** Create a fresh propositional atom. *) - val eq : term -> term -> atom (** Create an equality over two terms. The two given terms must have the same type [t], which must be different from {!Ty.prop} *) @@ -317,7 +314,7 @@ module Atom : sig val neg : atom -> atom (** Returns the negation of the given atom *) - val norm : atom -> atom * Formula_intf.negated + val norm : atom -> atom * Msat.negated (** Normalization functions as required by msat. *) end diff --git a/src/solver/type.ml b/src/main_test/type.ml similarity index 71% rename from src/solver/type.ml rename to src/main_test/type.ml index 693f35ce..d33f98ae 100644 --- a/src/solver/type.ml +++ b/src/main_test/type.ml @@ -3,6 +3,7 @@ This module defines the requirements for typing expre'ssions from dolmen. *) module type S = sig + type t type atom (** The type of atoms that will be fed to tha sovler. *) @@ -10,17 +11,17 @@ module type S = sig exception Typing_error of string * Dolmen.Term.t (** Exception raised during typechecking. *) - val decl : Dolmen.Id.t -> Dolmen.Term.t -> unit + val decl : t -> Dolmen.Id.t -> Dolmen.Term.t -> unit (** New declaration, i.e an identifier and its type. *) - val def : Dolmen.Id.t -> Dolmen.Term.t -> unit + val def : t -> Dolmen.Id.t -> Dolmen.Term.t -> unit (** New definition, i.e an identifier and the term it is equal to. *) - val assumptions : Dolmen.Term.t -> atom list + val assumptions : t -> Dolmen.Term.t -> atom list (** Parse a list of local assumptions. *) - val consequent : Dolmen.Term.t -> atom list list - val antecedent : Dolmen.Term.t -> atom list list + val consequent : t -> Dolmen.Term.t -> atom list list + val antecedent : t -> Dolmen.Term.t -> atom list list (** Parse a formula, and return a cnf ready to be given to the solver. Consequent is for hypotheses (left of the sequent), while antecedent is for goals (i.e formulas on the right of a sequent). *) diff --git a/src/sat/type_sat.ml b/src/main_test/type_sat.ml similarity index 67% rename from src/sat/type_sat.ml rename to src/main_test/type_sat.ml index b809cb4f..b733d31e 100644 --- a/src/sat/type_sat.ml +++ b/src/main_test/type_sat.ml @@ -10,7 +10,7 @@ Copyright 2014 Simon Cruanes module Id = Dolmen.Id module Ast = Dolmen.Term module H = Hashtbl.Make(Id) -module Formula = Msat_tseitin.Make(Expr_sat) +module Formula = Msat_tseitin.Make(Msat_sat.Th) (* Exceptions *) (* ************************************************************************ *) @@ -20,14 +20,24 @@ exception Typing_error of string * Dolmen.Term.t (* Identifiers *) (* ************************************************************************ *) -let symbols = H.create 42 +type t = { + symbols: Formula.atom H.t; + fresh: Formula.fresh_state; + st: Formula.state; +} -let find_id id = +let create th : t = { + symbols = H.create 42; + fresh=th; + st=Formula.create th; +} + +let find_id st id = try - H.find symbols id + H.find st.symbols id with Not_found -> - let res = Expr_sat.fresh () in - H.add symbols id res; + let res = Msat_sat.Th.fresh st.fresh in + H.add st.symbols id res; res (* Actual parsing *) @@ -35,29 +45,29 @@ let find_id id = [@@@ocaml.warning "-9"] -let rec parse = function +let rec parse st = function | { Ast.term = Ast.Builtin Ast.True } -> Formula.f_true | { Ast.term = Ast.Builtin Ast.False } -> Formula.f_false | { Ast.term = Ast.Symbol id } -> - let s = find_id id in + let s = find_id st id in Formula.make_atom s | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not }, [p]) } | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "not" } }, [p]) } -> - Formula.make_not (parse p) + Formula.make_not (parse st p) | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And }, l) } | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "and" } }, l) } -> - Formula.make_and (List.map parse l) + Formula.make_and (List.map (parse st) l) | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or }, l) } | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "or" } }, l) } -> - Formula.make_or (List.map parse l) + Formula.make_or (List.map (parse st) l) | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply }, [p; q]) } -> - Formula.make_imply (parse p) (parse q) + Formula.make_imply (parse st p) (parse st q) | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv }, [p; q]) } -> - Formula.make_equiv (parse p) (parse q) + Formula.make_equiv (parse st p) (parse st q) | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor }, [p; q]) } -> - Formula.make_xor (parse p) (parse q) + Formula.make_xor (parse st p) (parse st q) | t -> raise (Typing_error ("Term is not a pure proposition", t)) @@ -66,25 +76,25 @@ let rec parse = function (* Exported functions *) (* ************************************************************************ *) -let decl _ t = +let decl _ _ t = raise (Typing_error ("Declarations are not allowed in pure sat", t)) -let def _ t = +let def _ _ t = raise (Typing_error ("Definitions are not allowed in pure sat", t)) -let assumptions t = - let f = parse t in - let cnf = Formula.make_cnf f in +let assumptions st t = + let f = parse st t in + let cnf = Formula.make_cnf st.st f in List.map (function | [ x ] -> x | _ -> assert false ) cnf -let antecedent t = - let f = parse t in - Formula.make_cnf f +let antecedent st t = + let f = parse st t in + Formula.make_cnf st.st f -let consequent t = - let f = parse t in - Formula.make_cnf @@ Formula.make_not f +let consequent st t = + let f = parse st t in + Formula.make_cnf st.st @@ Formula.make_not f diff --git a/src/sat/type_sat.mli b/src/main_test/type_sat.mli similarity index 79% rename from src/sat/type_sat.mli rename to src/main_test/type_sat.mli index a088602c..01011b17 100644 --- a/src/sat/type_sat.mli +++ b/src/main_test/type_sat.mli @@ -8,5 +8,7 @@ Copyright 2014 Simon Cruanes This module provides functions to parse terms from the untyped syntax tree defined in Dolmen, and generate formulas as defined in the Expr_sat module. *) -include Minismt.Type.S with type atom := Expr_sat.t +include Type.S with type atom := Msat_sat.Th.formula + +val create : Msat_sat.Th.t -> t diff --git a/src/smt/unionfind.ml b/src/main_test/unionfind.ml similarity index 100% rename from src/smt/unionfind.ml rename to src/main_test/unionfind.ml diff --git a/src/smt/unionfind.mli b/src/main_test/unionfind.mli similarity index 100% rename from src/smt/unionfind.mli rename to src/main_test/unionfind.mli diff --git a/src/mcsat/Minismt_mcsat.ml b/src/mcsat/Minismt_mcsat.ml deleted file mode 100644 index a7f01e92..00000000 --- a/src/mcsat/Minismt_mcsat.ml +++ /dev/null @@ -1,13 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -include - Minismt.Mcsolver.Make(struct - type proof = unit - module Term = Minismt_smt.Expr.Term - module Formula = Minismt_smt.Expr.Atom - end)(Plugin_mcsat) - diff --git a/src/mcsat/Minismt_mcsat.mli b/src/mcsat/Minismt_mcsat.mli deleted file mode 100644 index a6de15ae..00000000 --- a/src/mcsat/Minismt_mcsat.mli +++ /dev/null @@ -1,8 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -include Minismt.Solver.S with type formula = Minismt_smt.Expr.atom - diff --git a/src/mcsat/backtrack.ml b/src/mcsat/backtrack.ml deleted file mode 100644 index aff629cc..00000000 --- a/src/mcsat/backtrack.ml +++ /dev/null @@ -1,99 +0,0 @@ - -module Stack = struct - - type op = - (* Stack structure *) - | Nil : op - | Level : op * int -> op - (* Undo operations *) - | Set : 'a ref * 'a * op -> op - | Call1 : ('a -> unit) * 'a * op -> op - | Call2 : ('a -> 'b -> unit) * 'a * 'b * op -> op - | Call3 : ('a -> 'b -> 'c -> unit) * 'a * 'b * 'c * op -> op - | CallUnit : (unit -> unit) * op -> op - - type t = { - mutable stack : op; - mutable last : int; - } - - type level = int - - let dummy_level = -1 - - let create () = { - stack = Nil; - last = dummy_level; - } - - let register_set t ref value = t.stack <- Set(ref, value, t.stack) - let register_undo t f = t.stack <- CallUnit (f, t.stack) - let register1 t f x = t.stack <- Call1 (f, x, t.stack) - let register2 t f x y = t.stack <- Call2 (f, x, y, t.stack) - let register3 t f x y z = t.stack <- Call3 (f, x, y, z, t.stack) - - let curr = ref 0 - - let push t = - let level = !curr in - t.stack <- Level (t.stack, level); - t.last <- level; - incr curr - - let rec level t = - match t.stack with - | Level (_, lvl) -> lvl - | _ -> push t; level t - - let backtrack t lvl = - let rec pop = function - | Nil -> assert false - | Level (op, level) as current -> - if level = lvl then begin - t.stack <- current; - t.last <- level - end else - pop op - | Set (ref, x, op) -> ref := x; pop op - | CallUnit (f, op) -> f (); pop op - | Call1 (f, x, op) -> f x; pop op - | Call2 (f, x, y, op) -> f x y; pop op - | Call3 (f, x, y, z, op) -> f x y z; pop op - in - pop t.stack - - let pop t = backtrack t (t.last) - -end - -module Hashtbl(K : Hashtbl.HashedType) = struct - - module H = Hashtbl.Make(K) - - type key = K.t - type 'a t = { - tbl : 'a H.t; - stack : Stack.t; - } - - let create ?(size=256) stack = {tbl = H.create size; stack; } - - let mem {tbl; _} x = H.mem tbl x - let find {tbl; _} k = H.find tbl k - - let add t k v = - Stack.register2 t.stack H.remove t.tbl k; - H.add t.tbl k v - - let remove t k = - try - let v = find t k in - Stack.register3 t.stack H.add t.tbl k v; - H.remove t.tbl k - with Not_found -> () - - let fold t f acc = H.fold f t.tbl acc - - let iter f t = H.iter f t.tbl -end - diff --git a/src/mcsat/backtrack.mli b/src/mcsat/backtrack.mli deleted file mode 100644 index 6480cf63..00000000 --- a/src/mcsat/backtrack.mli +++ /dev/null @@ -1,77 +0,0 @@ - -(** Provides helpers for backtracking. - This module defines backtracking stacks, i.e stacks of undo actions - to perform when backtracking to a certain point. This allows for - side-effect backtracking, and so to have backtracking automatically - handled by extensions without the need for explicit synchronisation - between the dispatcher and the extensions. -*) - -module Stack : sig - (** A backtracking stack is a stack of undo actions to perform - in order to revert back to a (mutable) state. *) - - type t - (** The type for a stack. *) - - type level - (** The type of backtracking point. *) - - val create : unit -> t - (** Creates an empty stack. *) - - val dummy_level : level - (** A dummy level. *) - - val push : t -> unit - (** Creates a backtracking point at the top of the stack. *) - - val pop : t -> unit - (** Pop all actions in the undo stack until the first backtracking point. *) - - val level : t -> level - (** Insert a named backtracking point at the top of the stack. *) - - val backtrack : t -> level -> unit - (** Backtrack to the given named backtracking point. *) - - val register_undo : t -> (unit -> unit) -> unit - (** Adds a callback at the top of the stack. *) - - val register1 : t -> ('a -> unit) -> 'a -> unit - val register2 : t -> ('a -> 'b -> unit) -> 'a -> 'b -> unit - val register3 : t -> ('a -> 'b -> 'c -> unit) -> 'a -> 'b -> 'c -> unit - (** Register functions to be called on the given arguments at the top of the stack. - Allows to save some space by not creating too much closure as would be the case if - only [unit -> unit] callbacks were stored. *) - - val register_set : t -> 'a ref -> 'a -> unit - (** Registers a ref to be set to the given value upon backtracking. *) - -end - -module Hashtbl : - functor (K : Hashtbl.HashedType) -> - sig - (** Provides wrappers around hastables in order to have - very simple integration with backtraking stacks. - All actions performed on this table register the corresponding - undo operations so that backtracking is automatic. *) - - type key = K.t - (** The type of keys of the Hashtbl. *) - - type 'a t - (** The type of hastable from keys to values of type ['a]. *) - - val create : ?size:int -> Stack.t -> 'a t - (** Creates an empty hashtable, that registers undo operations on the given stack. *) - - val add : 'a t -> key -> 'a -> unit - val mem : 'a t -> key -> bool - val find : 'a t -> key -> 'a - val remove : 'a t -> key -> unit - val iter : (key -> 'a -> unit) -> 'a t -> unit - val fold : 'a t -> (key -> 'a -> 'b -> 'b) -> 'b -> 'b - (** Usual operations on the hashtabl. For more information see the Hashtbl module of the stdlib. *) - end diff --git a/src/mcsat/eclosure.ml b/src/mcsat/eclosure.ml deleted file mode 100644 index fb53655d..00000000 --- a/src/mcsat/eclosure.ml +++ /dev/null @@ -1,232 +0,0 @@ - -module type Key = sig - type t - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - val print : Format.formatter -> t -> unit -end - -module type S = sig - type t - type var - - exception Unsat of var * var * var list - - val create : Backtrack.Stack.t -> t - - val find : t -> var -> var - - val add_eq : t -> var -> var -> unit - val add_neq : t -> var -> var -> unit - val add_tag : t -> var -> var -> unit - - val find_tag : t -> var -> var * (var * var) option - -end - -module Make(T : Key) = struct - - module M = Map.Make(T) - module H = Backtrack.Hashtbl(T) - - type var = T.t - - exception Equal of var * var - exception Same_tag of var * var - exception Unsat of var * var * var list - - type repr_info = { - rank : int; - tag : (T.t * T.t) option; - forbidden : (var * var) M.t; - } - - type node = - | Follow of var - | Repr of repr_info - - type t = { - size : int H.t; - expl : var H.t; - repr : node H.t; - } - - let create s = { - size = H.create s; - expl = H.create s; - repr = H.create s; - } - - (* Union-find algorithm with path compression *) - let self_repr = Repr { rank = 0; tag = None; forbidden = M.empty } - - let find_hash m i default = - try H.find m i - with Not_found -> default - - let rec find_aux m i = - match find_hash m i self_repr with - | Repr r -> r, i - | Follow j -> - let r, k = find_aux m j in - H.add m i (Follow k); - r, k - - let get_repr h x = - let r, y = find_aux h.repr x in - y, r - - let tag h x v = - let r, y = find_aux h.repr x in - let new_m = - { r with - tag = match r.tag with - | Some (_, v') when not (T.equal v v') -> raise (Equal (x, y)) - | (Some _) as t -> t - | None -> Some (x, v) } - in - H.add h.repr y (Repr new_m) - - let find h x = fst (get_repr h x) - - let find_tag h x = - let r, y = find_aux h.repr x in - y, r.tag - - let forbid_aux m x = - try - let a, b = M.find x m in - raise (Equal (a, b)) - with Not_found -> () - - let link h x mx y my = - let new_m = { - rank = if mx.rank = my.rank then mx.rank + 1 else mx.rank; - tag = (match mx.tag, my.tag with - | Some (z, t1), Some (w, t2) -> - if not (T.equal t1 t2) then begin - Log.debugf 3 - (fun k -> k "Tag shenanigan : %a (%a) <> %a (%a)" - T.print t1 T.print z T.print t2 T.print w); - raise (Equal (z, w)) - end else Some (z, t1) - | Some t, None | None, Some t -> Some t - | None, None -> None); - forbidden = M.merge (fun _ b1 b2 -> match b1, b2 with - | Some r, _ | None, Some r -> Some r | _ -> assert false) - mx.forbidden my.forbidden;} - in - let aux m z eq = - match H.find m z with - | Repr r -> - let r' = { r with - forbidden = M.add x eq (M.remove y r.forbidden) } - in - H.add m z (Repr r') - | _ -> assert false - in - M.iter (aux h.repr) my.forbidden; - H.add h.repr y (Follow x); - H.add h.repr x (Repr new_m) - - let union h x y = - let rx, mx = get_repr h x in - let ry, my = get_repr h y in - if T.compare rx ry <> 0 then begin - forbid_aux mx.forbidden ry; - forbid_aux my.forbidden rx; - if mx.rank > my.rank then begin - link h rx mx ry my - end else begin - link h ry my rx mx - end - end - - let forbid h x y = - let rx, mx = get_repr h x in - let ry, my = get_repr h y in - if T.compare rx ry = 0 then - raise (Equal (x, y)) - else match mx.tag, my.tag with - | Some (a, v), Some (b, v') when T.compare v v' = 0 -> - raise (Same_tag(a, b)) - | _ -> - H.add h.repr ry (Repr { my with forbidden = M.add rx (x, y) my.forbidden }); - H.add h.repr rx (Repr { mx with forbidden = M.add ry (x, y) mx.forbidden }) - - (* Equivalence closure with explanation output *) - let find_parent v m = find_hash m v v - - let rec root m acc curr = - let parent = find_parent curr m in - if T.compare curr parent = 0 then - curr :: acc - else - root m (curr :: acc) parent - - let rec rev_root m curr = - let next = find_parent curr m in - if T.compare curr next = 0 then - curr - else begin - H.remove m curr; - let res = rev_root m next in - H.add m next curr; - res - end - - let expl t a b = - let rec aux last = function - | x :: r, y :: r' when T.compare x y = 0 -> - aux (Some x) (r, r') - | l, l' -> begin match last with - | Some z -> List.rev_append (z :: l) l' - | None -> List.rev_append l l' - end - in - aux None (root t.expl [] a, root t.expl [] b) - - let add_eq_aux t i j = - if T.compare (find t i) (find t j) = 0 then - () - else begin - let old_root_i = rev_root t.expl i in - let old_root_j = rev_root t.expl j in - let nb_i = find_hash t.size old_root_i 0 in - let nb_j = find_hash t.size old_root_j 0 in - if nb_i < nb_j then begin - H.add t.expl i j; - H.add t.size j (nb_i + nb_j + 1) - end else begin - H.add t.expl j i; - H.add t.size i (nb_i + nb_j + 1) - end - end - - (* Functions wrapped to produce explanation in case - * something went wrong *) - let add_tag t x v = - match tag t x v with - | () -> () - | exception Equal (a, b) -> - raise (Unsat (a, b, expl t a b)) - - let add_eq t i j = - add_eq_aux t i j; - match union t i j with - | () -> () - | exception Equal (a, b) -> - raise (Unsat (a, b, expl t a b)) - - let add_neq t i j = - match forbid t i j with - | () -> () - | exception Equal (a, b) -> - raise (Unsat (a, b, expl t a b)) - | exception Same_tag (_, _) -> - add_eq_aux t i j; - let res = expl t i j in - raise (Unsat (i, j, res)) - -end diff --git a/src/mcsat/eclosure.mli b/src/mcsat/eclosure.mli deleted file mode 100644 index d4d5f32c..00000000 --- a/src/mcsat/eclosure.mli +++ /dev/null @@ -1,60 +0,0 @@ - -(** Equality closure using an union-find structure. - This module implements a equality closure algorithm using an union-find structure. - It supports adding of equality as well as inequalities, and raises exceptions - when trying to build an incoherent closure. - Please note that this does not implement congruence closure, as we do not - look inside the terms we are given. *) - -module type Key = sig - (** The type of keys used by the equality closure algorithm *) - - type t - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - val print : Format.formatter -> t -> unit -end - -module type S = sig - (** Type signature for the equality closure algorithm *) - - type t - (** Mutable state of the equality closure algorithm. *) - - type var - (** The type of expressions on which equality closure is built *) - - exception Unsat of var * var * var list - (** Raise when trying to build an incoherent equality closure, with an explanation - of the incoherence. - [Unsat (a, b, l)] is such that: - - [a <> b] has been previously added to the closure. - - [l] start with [a] and ends with [b] - - for each consecutive terms [p] and [q] in [l], - an equality [p = q] has been added to the closure. - *) - - val create : Backtrack.Stack.t -> t - (** Creates an empty state which uses the given backtrack stack *) - - val find : t -> var -> var - (** Returns the representative of the given expression in the current closure state *) - - val add_eq : t -> var -> var -> unit - val add_neq : t -> var -> var -> unit - (** Add an equality of inequality to the closure. *) - - val add_tag : t -> var -> var -> unit - (** Add a tag to an expression. The algorithm ensures that each equality class - only has one tag. If incoherent tags are added, an exception is raised. *) - - val find_tag : t -> var -> var * (var * var) option - (** Returns the tag associated with the equality class of the given term, if any. - More specifically, [find_tag e] returns a pair [(repr, o)] where [repr] is the representant of the equality - class of [e]. If the class has a tag, then [o = Some (e', t)] such that [e'] has been tagged with [t] previously. *) - -end - -module Make(T : Key) : S with type var = T.t - diff --git a/src/mcsat/jbuild b/src/mcsat/jbuild deleted file mode 100644 index 692db5f8..00000000 --- a/src/mcsat/jbuild +++ /dev/null @@ -1,13 +0,0 @@ -; vim:ft=lisp: - -(library - ((name minismt_mcsat) - (public_name minismt.mcsat) - (libraries (msat minismt minismt.smt)) - (synopsis "mcsat interface") - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) - - diff --git a/src/mcsat/plugin_mcsat.ml b/src/mcsat/plugin_mcsat.ml deleted file mode 100644 index d1c588c7..00000000 --- a/src/mcsat/plugin_mcsat.ml +++ /dev/null @@ -1,200 +0,0 @@ - -(* Module initialization *) - -module Expr_smt = Minismt_smt.Expr - -module E = Eclosure.Make(Expr_smt.Term) -module H = Backtrack.Hashtbl(Expr_smt.Term) -module M = Hashtbl.Make(Expr_smt.Term) - -(* Type definitions *) - -type proof = unit -type term = Expr_smt.Term.t -type formula = Expr_smt.Atom.t -type level = Backtrack.Stack.level - -exception Absurd of Expr_smt.Atom.t list - -(* Backtracking *) - -let stack = Backtrack.Stack.create () - -let dummy = Backtrack.Stack.dummy_level - -let current_level () = Backtrack.Stack.level stack - -let backtrack = Backtrack.Stack.backtrack stack - -(* Equality closure *) - -let uf = E.create stack - -let assign t = - match E.find_tag uf t with - | _, None -> t - | _, Some (_, v) -> v - -(* Propositional constants *) - -let true_ = Expr_smt.(Term.of_id (Id.ty "true" Ty.prop)) -let false_ = Expr_smt.(Term.of_id (Id.ty "false" Ty.prop)) - -(* Uninterpreted functions and predicates *) - -let map : Expr_smt.term H.t = H.create stack -let watch = M.create 4096 -let interpretation = H.create stack - -let pop_watches t = - try - let l = M.find watch t in - M.remove watch t; - l - with Not_found -> - [] - -let add_job j x = - let l = try M.find watch x with Not_found -> [] in - M.add watch x (j :: l) - -let update_job x ((t, watchees) as job) = - try - let y = List.find (fun y -> not (H.mem map y)) watchees in - add_job job y - with Not_found -> - add_job job x; - begin match t with - | { Expr_smt.term = Expr_smt.App (f, tys, l);_ } -> - let is_prop = Expr_smt.(Ty.equal t.t_type Ty.prop) in - let t_v = H.find map t in - let l' = List.map (H.find map) l in - let u = Expr_smt.Term.apply f tys l' in - begin try - let t', u_v = H.find interpretation u in - if not (Expr_smt.Term.equal t_v u_v) then begin - match t' with - | { Expr_smt.term = Expr_smt.App (_, _, r); _ } when is_prop -> - let eqs = List.map2 (fun a b -> Expr_smt.Atom.neg (Expr_smt.Atom.eq a b)) l r in - if Expr_smt.(Term.equal u_v true_) then begin - let res = Expr_smt.Atom.pred t :: - Expr_smt.Atom.neg (Expr_smt.Atom.pred t') :: eqs in - raise (Absurd res) - end else begin - let res = Expr_smt.Atom.pred t' :: - Expr_smt.Atom.neg (Expr_smt.Atom.pred t) :: eqs in - raise (Absurd res) - end - | { Expr_smt.term = Expr_smt.App (_, _, r); _ } -> - let eqs = List.map2 (fun a b -> Expr_smt.Atom.neg (Expr_smt.Atom.eq a b)) l r in - let res = Expr_smt.Atom.eq t t' :: eqs in - raise (Absurd res) - | _ -> assert false - end - with Not_found -> - H.add interpretation u (t, t_v); - end - | _ -> assert false - end - -let rec update_watches x = function - | [] -> () - | job :: r -> - begin - try - update_job x job; - with exn -> - List.iter (fun j -> add_job j x) r; - raise exn - end; - update_watches x r - -let add_watch t l = - update_job t (t, l) - -let add_assign t v = - H.add map t v; - update_watches t (pop_watches t) - -(* Assignemnts *) - -let rec iter_aux f = function - | { Expr_smt.term = Expr_smt.Var _; _ } as t -> - Log.debugf 10 (fun k -> k "Adding %a as assignable" Expr_smt.Term.print t); - f t - | { Expr_smt.term = Expr_smt.App (_, _, l); _ } as t -> - if l <> [] then add_watch t (t :: l); - List.iter (iter_aux f) l; - Log.debugf 10 (fun k -> k "Adding %a as assignable" Expr_smt.Term.print t); - f t - -let iter_assignable f = function - | { Expr_smt.atom = Expr_smt.Pred { Expr_smt.term = Expr_smt.Var _;_ }; _ } -> () - | { Expr_smt.atom = Expr_smt.Pred ({ Expr_smt.term = Expr_smt.App (_, _, l);_} as t); _ } -> - if l <> [] then add_watch t (t :: l); - List.iter (iter_aux f) l; - | { Expr_smt.atom = Expr_smt.Equal (a, b);_ } -> - iter_aux f a; iter_aux f b - -let eval = function - | { Expr_smt.atom = Expr_smt.Pred t; _ } -> - begin try - let v = H.find map t in - if Expr_smt.Term.equal v true_ then - Plugin_intf.Valued (true, [t]) - else if Expr_smt.Term.equal v false_ then - Plugin_intf.Valued (false, [t]) - else - Plugin_intf.Unknown - with Not_found -> - Plugin_intf.Unknown - end - | { Expr_smt.atom = Expr_smt.Equal (a, b); sign; _ } -> - begin try - let v_a = H.find map a in - let v_b = H.find map b in - if Expr_smt.Term.equal v_a v_b then - Plugin_intf.Valued(sign, [a; b]) - else - Plugin_intf.Valued(not sign, [a; b]) - with Not_found -> - Plugin_intf.Unknown - end - - -(* Theory propagation *) - -let rec chain_eq = function - | [] | [_] -> [] - | a :: ((b :: _) as l) -> (Expr_smt.Atom.eq a b) :: chain_eq l - -let assume s = - let open Plugin_intf in - try - for i = s.start to s.start + s.length - 1 do - match s.get i with - | Assign (t, v) -> - add_assign t v; - E.add_tag uf t v - | Lit f -> - begin match f with - | { Expr_smt.atom = Expr_smt.Equal (u, v); sign = true;_ } -> - E.add_eq uf u v - | { Expr_smt.atom = Expr_smt.Equal (u, v); sign = false;_ } -> - E.add_neq uf u v - | { Expr_smt.atom = Expr_smt.Pred p; sign;_ } -> - let v = if sign then true_ else false_ in - add_assign p v - end - done; - Plugin_intf.Sat - with - | Absurd l -> - Plugin_intf.Unsat (l, ()) - | E.Unsat (a, b, l) -> - let c = Expr_smt.Atom.eq a b :: List.map Expr_smt.Atom.neg (chain_eq l) in - Plugin_intf.Unsat (c, ()) - -let if_sat _ = - Plugin_intf.Sat - diff --git a/src/sat/Expr_sat.ml b/src/sat/Expr_sat.ml deleted file mode 100644 index efb92778..00000000 --- a/src/sat/Expr_sat.ml +++ /dev/null @@ -1,70 +0,0 @@ - -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 - use even integers for user-created atoms, and odd integers for the - fresh atoms. *) - -let max_lit = max_int - -(* Counters *) -let max_index = ref 0 -let max_fresh = ref (-1) - -(** Internal function for creating atoms. - Updates the internal counters *) -let _make i = - if i <> 0 && (abs i) < max_lit then begin - max_index := max !max_index (abs i); - i - end else - raise Bad_atom - -(** A dummy atom *) -let dummy = 0 - -(** *) -let neg a = - a - -let norm a = - abs a, if a < 0 then - Formula_intf.Negated - else - Formula_intf.Same_sign - -let abs = abs - -let sign i = i > 0 - -let apply_sign b i = if b then i else neg i - -let set_sign b i = if b then abs i else neg (abs i) - -let hash (a:int) = a land max_int -let equal (a:int) b = a=b -let compare (a:int) b = Pervasives.compare a b - -let make i = _make (2 * i) - -let fresh () = - incr max_fresh; - _make (2 * !max_fresh + 1) - -(* -let iter: (t -> unit) -> unit = fun f -> - for j = 1 to !max_index do - f j - done -*) - -let print fmt a = - Format.fprintf fmt "%s%s%d" - (if a < 0 then "~" else "") - (if a mod 2 = 0 then "v" else "f") - ((abs a) / 2) diff --git a/src/sat/Minismt_sat.ml b/src/sat/Minismt_sat.ml deleted file mode 100644 index cbb2b082..00000000 --- a/src/sat/Minismt_sat.ml +++ /dev/null @@ -1,10 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2016 Guillaume Bury -*) - -module Expr = Expr_sat -module Type = Type_sat - -include Minismt.Solver.Make(Expr)(Minismt.Solver.DummyTheory(Expr)) - diff --git a/src/sat/Msat_sat.ml b/src/sat/Msat_sat.ml new file mode 100644 index 00000000..016fa3b2 --- /dev/null +++ b/src/sat/Msat_sat.ml @@ -0,0 +1,9 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +*) + +module Th = Th_sat + +include Msat.Make(Th) + diff --git a/src/sat/Minismt_sat.mli b/src/sat/Msat_sat.mli similarity index 74% rename from src/sat/Minismt_sat.mli rename to src/sat/Msat_sat.mli index 9dbd63f1..d0201e41 100644 --- a/src/sat/Minismt_sat.mli +++ b/src/sat/Msat_sat.mli @@ -9,9 +9,8 @@ Copyright 2016 Guillaume Bury atomic propositions. *) -module Expr = Expr_sat -module Type = Type_sat +module Th = Th_sat -include Minismt.Solver.S with type formula = Expr.t +include module type of Msat.Make(Th) (** A functor that can generate as many solvers as needed. *) diff --git a/src/sat/Th_sat.ml b/src/sat/Th_sat.ml new file mode 100644 index 00000000..07b484d9 --- /dev/null +++ b/src/sat/Th_sat.ml @@ -0,0 +1,87 @@ + +exception Bad_atom +(** Exception raised if an atom cannot be created *) + +type proof = unit +(** A empty type for proofs *) + +type formula = int + +type t = { + actions: (formula, proof) Msat.actions; + mutable max_index: int; + mutable max_fresh: int; +} + +let create actions : t = { + actions; + max_index = 0; + max_fresh= (-1); +} + +module Form = struct + type t = formula + (** Atoms are represented as integers. [-i] begin the negation of [i]. + Additionally, since we nee dot be able to create fresh atoms, we + use even integers for user-created atoms, and odd integers for the + fresh atoms. *) + + let max_lit = max_int + + let hash (a:int) = a land max_int + let equal (a:int) b = a=b + let compare (a:int) b = Pervasives.compare a b + + (** Internal function for creating atoms. + Updates the internal counters *) + let make_ st i = + if i <> 0 && (abs i) < max_lit then ( + st.max_index <- max st.max_index (abs i); + i + ) else ( + raise Bad_atom + ) + + (** A dummy atom *) + let dummy = 0 + + let neg a = - a + + let norm a = + abs a, if a < 0 then + Msat.Negated + else + Msat.Same_sign + + let print fmt a = + Format.fprintf fmt "%s%s%d" + (if a < 0 then "~" else "") + (if a mod 2 = 0 then "v" else "f") + ((abs a) / 2) + +end + +let abs = abs + +let sign i = i > 0 + +let apply_sign b i = if b then i else Form.neg i + +let set_sign b i = if b then abs i else Form.neg (abs i) + +let make st i = Form.make_ st (2 * i) + +let fresh st = + st.max_fresh <- 1 + st.max_fresh; + Form.make_ st (2 * st.max_fresh + 1) + +(* +let iter: (t -> unit) -> unit = fun f -> + for j = 1 to !max_index do + f j + done +*) + +let assume _ _ = Msat.Theory_intf.Sat + +let if_sat _ _ = Msat.Theory_intf.Sat diff --git a/src/sat/Expr_sat.mli b/src/sat/Th_sat.mli similarity index 63% rename from src/sat/Expr_sat.mli rename to src/sat/Th_sat.mli index a48603af..1e30c2e3 100644 --- a/src/sat/Expr_sat.mli +++ b/src/sat/Th_sat.mli @@ -4,28 +4,28 @@ (** SAT Formulas This modules implements formuals adequate for use in a pure SAT Solver. - Atomic formuals are represented using integers, that should allow + Atomic formulas are represented using integers, that should allow near optimal efficiency (both in terms of space and time). *) -include Formula_intf.S +open Msat + +include Theory_intf.S with type formula = int and type proof = unit (** This modules implements the requirements for implementing an SAT Solver. *) -val make : int -> t +val make : t -> int -> formula (** Make a proposition from an integer. *) -val fresh : unit -> t +val fresh : t -> formula (** Make a fresh atom *) -val compare : t -> t -> int -(** Compare atoms *) - -val sign : t -> bool +val sign : formula -> bool (** Is the given atom positive ? *) -val apply_sign : bool -> t -> t +val apply_sign : bool -> formula -> formula (** [apply_sign b] is the identity if [b] is [true], and the negation function if [b] is [false]. *) -val set_sign : bool -> t -> t +val set_sign : bool -> formula -> formula (** Return the atom with the sign set. *) + diff --git a/src/sat/jbuild b/src/sat/jbuild index 82068bfb..cc2424e4 100644 --- a/src/sat/jbuild +++ b/src/sat/jbuild @@ -1,9 +1,9 @@ ; vim:ft=lisp: (library - ((name minismt_sat) - (public_name minismt.sat) - (libraries (msat msat.tseitin minismt dolmen)) + ((name msat_sat) + (public_name msat.sat) + (libraries (msat msat.tseitin)) (synopsis "sat interface") (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) (ocamlopt_flags (:standard -O3 -bin-annot diff --git a/src/smt/Minismt_smt.ml b/src/smt/Minismt_smt.ml deleted file mode 100644 index 473b12de..00000000 --- a/src/smt/Minismt_smt.ml +++ /dev/null @@ -1,13 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module Expr = Expr_smt -module Type = Type_smt - -module Th = Minismt.Solver.DummyTheory(Expr.Atom) - -include Minismt.Solver.Make(Expr.Atom)(Th) - diff --git a/src/smt/Minismt_smt.mli b/src/smt/Minismt_smt.mli deleted file mode 100644 index f81b5277..00000000 --- a/src/smt/Minismt_smt.mli +++ /dev/null @@ -1,11 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module Expr = Expr_smt -module Type = Type_smt - -include Minismt.Solver.S with type formula = Expr_smt.atom - diff --git a/src/smt/jbuild b/src/smt/jbuild deleted file mode 100644 index 9999f849..00000000 --- a/src/smt/jbuild +++ /dev/null @@ -1,13 +0,0 @@ -; vim:ft=lisp: - -(library - ((name minismt_smt) - (public_name minismt.smt) - (libraries (msat minismt msat.tseitin dolmen)) - (synopsis "smt interface") - (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat)) - (ocamlopt_flags (:standard -O3 -bin-annot - -unbox-closures -unbox-closures-factor 20)) - )) - - diff --git a/src/smt/type_smt.ml b/src/smt/type_smt.ml deleted file mode 100644 index 5dbe3837..00000000 --- a/src/smt/type_smt.ml +++ /dev/null @@ -1,628 +0,0 @@ - -(* Log&Module Init *) -(* ************************************************************************ *) - -module Ast = Dolmen.Term -module Id = Dolmen.Id -module M = Map.Make(Id) -module H = Hashtbl.Make(Id) -module Expr = Expr_smt - -(* Types *) -(* ************************************************************************ *) - -(* The type of potentially expected result type for parsing an expression *) -type expect = - | Nothing - | Type - | Typed of Expr.ty - -(* The type returned after parsing an expression. *) -type res = - | Ttype - | Ty of Expr.ty - | Term of Expr.term - | Formula of Expr.Formula.t - - -(* The local environments used for type-checking. *) -type env = { - - (* local variables (mostly quantified variables) *) - type_vars : (Expr.ttype Expr.id) M.t; - term_vars : (Expr.ty Expr.id) M.t; - - (* Bound variables (through let constructions) *) - term_lets : Expr.term M.t; - prop_lets : Expr.Formula.t M.t; - - (* Typing options *) - expect : expect; -} - -(* Exceptions *) -(* ************************************************************************ *) - -(* Internal exception *) -exception Found of Ast.t - -(* Exception for typing errors *) -exception Typing_error of string * Ast.t - -(* Convenience functions *) -let _expected s t = raise (Typing_error ( - Format.asprintf "Expected a %s" s, t)) -let _bad_arity s n t = raise (Typing_error ( - Format.asprintf "Bad arity for operator '%s' (expected %d arguments)" s n, t)) -let _type_mismatch t ty ty' ast = raise (Typing_error ( - Format.asprintf "Type Mismatch: '%a' has type %a, but an expression of type %a was expected" - Expr.Print.term t Expr.Print.ty ty Expr.Print.ty ty', ast)) -let _fo_term s t = raise (Typing_error ( - Format.asprintf "Let-bound variable '%a' is applied to terms" Id.print s, t)) - -(* Global Environment *) -(* ************************************************************************ *) - -(* Global identifier table; stores declared types and aliases. *) -let global_env = H.create 42 - -let find_global name = - try H.find global_env name - with Not_found -> `Not_found - -(* Symbol declarations *) -let decl_ty_cstr id c = - if H.mem global_env id then - Log.debugf 0 - (fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" Id.print id); - H.add global_env id (`Ty c); - Log.debugf 1 (fun k -> k "New type constructor : %a" Expr.Print.const_ttype c) - -let decl_term id c = - if H.mem global_env id then - Log.debugf 0 - (fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" Id.print id); - H.add global_env id (`Term c); - Log.debugf 1 (fun k -> k "New constant : %a" Expr.Print.const_ty c) - -(* Symbol definitions *) -let def_ty id args body = - if H.mem global_env id then - Log.debugf 0 - (fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" Id.print id); - H.add global_env id (`Ty_alias (args, body)) - -let def_term id ty_args args body = - if H.mem global_env id then - Log.debugf 0 - (fun k -> k "Symbol '%a' has already been defined, overwriting previous definition" Id.print id); - H.add global_env id (`Term_alias (ty_args, args, body)) - -(* Local Environment *) -(* ************************************************************************ *) - -(* Make a new empty environment *) -let empty_env ?(expect=Nothing) () = { - type_vars = M.empty; - term_vars = M.empty; - term_lets = M.empty; - prop_lets = M.empty; - expect; -} - -(* Generate new fresh names for shadowed variables *) -let new_name pre = - let i = ref 0 in - (fun () -> incr i; pre ^ (string_of_int !i)) - -let new_ty_name = new_name "ty#" -let new_term_name = new_name "term#" - -(* Add local variables to environment *) -let add_type_var env id v = - let v' = - if M.mem id env.type_vars then - Expr.Id.ttype (new_ty_name ()) - else - v - in - Log.debugf 1 - (fun k -> k "New binding : %a -> %a" Id.print id Expr.Print.id_ttype v'); - v', { env with type_vars = M.add id v' env.type_vars } - -let add_type_vars env l = - let l', env' = List.fold_left (fun (l, acc) (id, v) -> - let v', acc' = add_type_var acc id v in - v' :: l, acc') ([], env) l in - List.rev l', env' - -let add_term_var env id v = - let v' = - if M.mem id env.type_vars then - Expr.Id.ty (new_term_name ()) Expr.(v.id_type) - else - v - in - Log.debugf 1 - (fun k -> k "New binding : %a -> %a" Id.print id Expr.Print.id_ty v'); - v', { env with term_vars = M.add id v' env.term_vars } - -let find_var env name = - try `Ty (M.find name env.type_vars) - with Not_found -> - begin - try - `Term (M.find name env.term_vars) - with Not_found -> - `Not_found - end - -(* Add local bound variables to env *) -let add_let_term env id t = - Log.debugf 1 - (fun k -> k "New let-binding : %s -> %a" id.Id.name Expr.Print.term t); - { env with term_lets = M.add id t env.term_lets } - -let add_let_prop env id t = - Log.debugf 1 - (fun k -> k "New let-binding : %s -> %a" id.Id.name Expr.Formula.print t); - { env with prop_lets = M.add id t env.prop_lets } - -let find_let env name = - try `Term (M.find name env.term_lets) - with Not_found -> - begin - try - `Prop (M.find name env.prop_lets) - with Not_found -> - `Not_found - end - -(* Some helper functions *) -(* ************************************************************************ *) - -let flat_map f l = List.flatten (List.map f l) - -let take_drop n l = - let rec aux acc = function - | 0, res | _, ([] as res) -> List.rev acc, res - | m, x :: r -> aux (x :: acc) (m - 1, r) - in - aux [] (n, l) - -let diagonal l = - let rec single x acc = function - | [] -> acc - | y :: r -> single x ((x, y) :: acc) r - and aux acc = function - | [] -> acc - | x :: r -> aux (single x acc r) r - in - aux [] l - -(* Wrappers for expression building *) -(* ************************************************************************ *) - -let arity f = - List.length Expr.(f.id_type.fun_vars) + - List.length Expr.(f.id_type.fun_args) - -let ty_apply _env ast f args = - try - Expr.Ty.apply f args - with Expr.Bad_ty_arity _ -> - _bad_arity Expr.(f.id_name) (arity f) ast - -let term_apply _env ast f ty_args t_args = - try - Expr.Term.apply f ty_args t_args - with - | Expr.Bad_arity _ -> - _bad_arity Expr.(f.id_name) (arity f) ast - | Expr.Type_mismatch (t, ty, ty') -> - _type_mismatch t ty ty' ast - -let ty_subst ast_term id args f_args body = - let aux s v ty = Expr.Subst.Id.bind v ty s in - match List.fold_left2 aux Expr.Subst.empty f_args args with - | subst -> - Expr.Ty.subst subst body - | exception Invalid_argument _ -> - _bad_arity id.Id.name (List.length f_args) ast_term - -let term_subst ast_term id ty_args t_args f_ty_args f_t_args body = - let aux s v ty = Expr.Subst.Id.bind v ty s in - match List.fold_left2 aux Expr.Subst.empty f_ty_args ty_args with - | ty_subst -> - begin - let aux s v t = Expr.Subst.Id.bind v t s in - match List.fold_left2 aux Expr.Subst.empty f_t_args t_args with - | t_subst -> - Expr.Term.subst ty_subst t_subst body - | exception Invalid_argument _ -> - _bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term - end - | exception Invalid_argument _ -> - _bad_arity id.Id.name (List.length f_ty_args + List.length f_t_args) ast_term - -let make_eq ast_term a b = - try - Expr.Formula.make_atom @@ Expr.Atom.eq a b - with Expr.Type_mismatch (t, ty, ty') -> - _type_mismatch t ty ty' ast_term - -let make_pred ast_term p = - try - Expr.Formula.make_atom @@ Expr.Atom.pred p - with Expr.Type_mismatch (t, ty, ty') -> - _type_mismatch t ty ty' ast_term - -let infer env s args = - match env.expect with - | Nothing -> `Nothing - | Type -> - let n = List.length args in - let res = Expr.Id.ty_fun s.Id.name n in - decl_ty_cstr s res; - `Ty res - | Typed ty -> - let n = List.length args in - let rec replicate acc n = - if n <= 0 then acc else replicate (Expr.Ty.base :: acc) (n - 1) - in - let res = Expr.Id.term_fun s.Id.name [] (replicate [] n) ty in - decl_term s res; - `Term res - -(* Expression parsing *) -(* ************************************************************************ *) - -[@@@ocaml.warning "-9"] - -let rec parse_expr (env : env) t = - match t with - (* Base Types *) - | { Ast.term = Ast.Builtin Ast.Ttype } -> - Ttype - | { Ast.term = Ast.Symbol { Id.name = "Bool" } } -> - Ty (Expr_smt.Ty.prop) - - (* Basic formulas *) - | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.True }, []) } - | { Ast.term = Ast.Builtin Ast.True } -> - Formula Expr.Formula.f_true - - | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.False }, []) } - | { Ast.term = Ast.Builtin Ast.False } -> - Formula Expr.Formula.f_false - - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And}, l) } - | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "and" }}, l) } -> - Formula (Expr.Formula.make_and (List.map (parse_formula env) l)) - - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or}, l) } - | { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "or" }}, l) } -> - Formula (Expr.Formula.make_or (List.map (parse_formula env) l)) - - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor}, l) } as t -> - begin match l with - | [p; q] -> - let f = parse_formula env p in - let g = parse_formula env q in - Formula (Expr.Formula.make_not (Expr.Formula.make_equiv f g)) - | _ -> _bad_arity "xor" 2 t - end - - | ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply}, l) } as t) - | ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "=>" }}, l) } as t) -> - begin match l with - | [p; q] -> - let f = parse_formula env p in - let g = parse_formula env q in - Formula (Expr.Formula.make_imply f g) - | _ -> _bad_arity "=>" 2 t - end - - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, l) } as t -> - begin match l with - | [p; q] -> - let f = parse_formula env p in - let g = parse_formula env q in - Formula (Expr.Formula.make_equiv f g) - | _ -> _bad_arity "<=>" 2 t - end - - | ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not}, l) } as t) - | ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "not" }}, l) } as t) -> - begin match l with - | [p] -> - Formula (Expr.Formula.make_not (parse_formula env p)) - | _ -> _bad_arity "not" 1 t - end - - (* (Dis)Equality *) - | ({ Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, l) } as t) - | ({ Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "=" }}, l) } as t) -> - begin match l with - | [a; b] -> - Formula ( - make_eq t - (parse_term env a) - (parse_term env b) - ) - | _ -> _bad_arity "=" 2 t - end - - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Distinct}, args) } as t -> - let l' = List.map (parse_term env) args in - let l'' = diagonal l' in - Formula ( - Expr.Formula.make_and - (List.map (fun (a, b) -> - Expr.Formula.make_not - (make_eq t a b)) l'') - ) - - (* General case: application *) - | { Ast.term = Ast.Symbol s } as ast -> - parse_app env ast s [] - | { Ast.term = Ast.App ({ Ast.term = Ast.Symbol s }, l) } as ast -> - parse_app env ast s l - - (* Local bindings *) - | { Ast.term = Ast.Binder (Ast.Let, vars, f) } -> - parse_let env f vars - - (* Other cases *) - | ast -> raise (Typing_error ("Couldn't parse the expression", ast)) - -and parse_var env = function - | { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } -> - begin match parse_expr env e with - | Ttype -> `Ty (s, Expr.Id.ttype s.Id.name) - | Ty ty -> `Term (s, Expr.Id.ty s.Id.name ty) - | _ -> _expected "type (or Ttype)" e - end - | { Ast.term = Ast.Symbol s } -> - begin match env.expect with - | Nothing -> assert false - | Type -> `Ty (s, Expr.Id.ttype s.Id.name) - | Typed ty -> `Term (s, Expr.Id.ty s.Id.name ty) - end - | t -> _expected "(typed) variable" t - -and parse_quant_vars env l = - let ttype_vars, typed_vars, env' = List.fold_left ( - fun (l1, l2, acc) v -> - match parse_var acc v with - | `Ty (id, v') -> - let v'', acc' = add_type_var acc id v' in - (v'' :: l1, l2, acc') - | `Term (id, v') -> - let v'', acc' = add_term_var acc id v' in - (l1, v'' :: l2, acc') - ) ([], [], env) l in - List.rev ttype_vars, List.rev typed_vars, env' - -and parse_let env f = function - | [] -> parse_expr env f - | x :: r -> - begin match x with - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Eq}, [ - { Ast.term = Ast.Symbol s }; e]) } -> - let t = parse_term env e in - let env' = add_let_term env s t in - parse_let env' f r - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv}, [ - { Ast.term = Ast.Symbol s }; e]) } -> - let t = parse_formula env e in - let env' = add_let_prop env s t in - parse_let env' f r - | { Ast.term = Ast.Colon ({ Ast.term = Ast.Symbol s }, e) } -> - begin match parse_expr env e with - | Term t -> - let env' = add_let_term env s t in - parse_let env' f r - | Formula t -> - let env' = add_let_prop env s t in - parse_let env' f r - | _ -> _expected "term of formula" e - end - | t -> _expected "let-binding" t - end - -and parse_app env ast s args = - match find_let env s with - | `Term t -> - if args = [] then Term t - else _fo_term s ast - | `Prop p -> - if args = [] then Formula p - else _fo_term s ast - | `Not_found -> - begin match find_var env s with - | `Ty f -> - if args = [] then Ty (Expr.Ty.of_id f) - else _fo_term s ast - | `Term f -> - if args = [] then Term (Expr.Term.of_id f) - else _fo_term s ast - | `Not_found -> - begin match find_global s with - | `Ty f -> - parse_app_ty env ast f args - | `Term f -> - parse_app_term env ast f args - | `Ty_alias (f_args, body) -> - parse_app_subst_ty env ast s args f_args body - | `Term_alias (f_ty_args, f_t_args, body) -> - parse_app_subst_term env ast s args f_ty_args f_t_args body - | `Not_found -> - begin match infer env s args with - | `Ty f -> parse_app_ty env ast f args - | `Term f -> parse_app_term env ast f args - | `Nothing -> - raise (Typing_error ( - Format.asprintf "Scoping error: '%a' not found" Id.print s, ast)) - end - end - end - -and parse_app_ty env ast f args = - let l = List.map (parse_ty env) args in - Ty (ty_apply env ast f l) - -and parse_app_term env ast f args = - let n = List.length Expr.(f.id_type.fun_vars) in - let ty_l, t_l = take_drop n args in - let ty_args = List.map (parse_ty env) ty_l in - let t_args = List.map (parse_term env) t_l in - Term (term_apply env ast f ty_args t_args) - -and parse_app_subst_ty env ast id args f_args body = - let l = List.map (parse_ty env) args in - Ty (ty_subst ast id l f_args body) - -and parse_app_subst_term env ast id args f_ty_args f_t_args body = - let n = List.length f_ty_args in - let ty_l, t_l = take_drop n args in - let ty_args = List.map (parse_ty env) ty_l in - let t_args = List.map (parse_term env) t_l in - Term (term_subst ast id ty_args t_args f_ty_args f_t_args body) - -and parse_ty env ast = - match parse_expr { env with expect = Type } ast with - | Ty ty -> ty - | _ -> _expected "type" ast - -and parse_term env ast = - match parse_expr { env with expect = Typed Expr.Ty.base } ast with - | Term t -> t - | _ -> _expected "term" ast - -and parse_formula env ast = - match parse_expr { env with expect = Typed Expr.Ty.prop } ast with - | Term t when Expr.(Ty.equal Ty.prop t.t_type) -> - make_pred ast t - | Formula p -> p - | _ -> _expected "formula" ast - -let parse_ttype_var env t = - match parse_var env t with - | `Ty (id, v) -> (id, v) - | `Term _ -> _expected "type variable" t - -let rec parse_sig_quant env = function - | { Ast.term = Ast.Binder (Ast.Pi, vars, t) } -> - let ttype_vars = List.map (parse_ttype_var env) vars in - let ttype_vars', env' = add_type_vars env ttype_vars in - let l = List.combine vars ttype_vars' in - parse_sig_arrow l [] env' t - | t -> - parse_sig_arrow [] [] env t - -and parse_sig_arrow ttype_vars (ty_args: (Ast.t * res) list) env = function - | { Ast.term = Ast.Binder (Ast.Arrow, args, ret) } -> - let t_args = parse_sig_args env args in - parse_sig_arrow ttype_vars (ty_args @ t_args) env ret - | t -> - begin match parse_expr env t with - | Ttype -> - begin match ttype_vars with - | (h, _) :: _ -> - raise (Typing_error ( - "Type constructor signatures cannot have quantified type variables", h)) - | [] -> - let aux n = function - | (_, Ttype) -> n + 1 - | (ast, _) -> raise (Found ast) - in - begin - match List.fold_left aux 0 ty_args with - | n -> `Ty_cstr n - | exception Found err -> - raise (Typing_error ( - Format.asprintf - "Type constructor signatures cannot have non-ttype arguments,", err)) - end - end - | Ty ret -> - let aux acc = function - | (_, Ty t) -> t :: acc - | (ast, _) -> raise (Found ast) - in - begin - match List.fold_left aux [] ty_args with - | exception Found err -> _expected "type" err - | l -> `Fun_ty (List.map snd ttype_vars, List.rev l, ret) - end - | _ -> _expected "Ttype of type" t - end - -and parse_sig_args env l = - flat_map (parse_sig_arg env) l - -and parse_sig_arg env = function - | { Ast.term = Ast.App ({ Ast.term = Ast.Builtin Ast.Product}, l) } -> - List.map (fun x -> x, parse_expr env x) l - | t -> - [t, parse_expr env t] - -let parse_sig = parse_sig_quant - -let rec parse_fun ty_args t_args env = function - | { Ast.term = Ast.Binder (Ast.Fun, l, ret) } -> - let ty_args', t_args', env' = parse_quant_vars env l in - parse_fun (ty_args @ ty_args') (t_args @ t_args') env' ret - | ast -> - begin match parse_expr env ast with - | Ttype -> raise (Typing_error ("Cannot redefine Ttype", ast)) - | Ty body -> - if t_args = [] then `Ty (ty_args, body) - else _expected "term" ast - | Term body -> `Term (ty_args, t_args, body) - | Formula _ -> _expected "type or term" ast - end - -[@@@ocaml.warning "+9"] - -(* High-level parsing functions *) -(* ************************************************************************ *) - -let decl id t = - let env = empty_env () in - Log.debugf 5 - (fun k -> k "Typing declaration: %s : %a" id.Id.name Ast.print t); - begin match parse_sig env t with - | `Ty_cstr n -> decl_ty_cstr id (Expr.Id.ty_fun id.Id.name n) - | `Fun_ty (vars, args, ret) -> - decl_term id (Expr.Id.term_fun id.Id.name vars args ret) - end - -let def id t = - let env = empty_env () in - Log.debugf 5 - (fun k -> k "Typing definition: %s = %a" id.Id.name Ast.print t); - begin match parse_fun [] [] env t with - | `Ty (ty_args, body) -> def_ty id ty_args body - | `Term (ty_args, t_args, body) -> def_term id ty_args t_args body - end - -let formula t = - let env = empty_env () in - Log.debugf 5 (fun k -> k "Typing top-level formula: %a" Ast.print t); - parse_formula env t - -let assumptions t = - let cnf = Expr.Formula.make_cnf (formula t) in - List.map (function - | [ x ] -> x - | _ -> assert false - ) cnf - -let antecedent t = - Expr.Formula.make_cnf (formula t) - -let consequent t = - Expr.Formula.make_cnf (Expr.Formula.make_not (formula t)) - diff --git a/src/smt/type_smt.mli b/src/smt/type_smt.mli deleted file mode 100644 index 1613debb..00000000 --- a/src/smt/type_smt.mli +++ /dev/null @@ -1,7 +0,0 @@ - -(** Typechecking of terms from Dolmen.Term.t - This module provides functions to parse terms from the untyped syntax tree - defined in Dolmen, and generate formulas as defined in the Expr_smt module. *) - -include Minismt.Type.S with type atom := Expr_smt.Atom.t - diff --git a/src/solver/mcsolver.ml b/src/solver/mcsolver.ml deleted file mode 100644 index f6eb0c68..00000000 --- a/src/solver/mcsolver.ml +++ /dev/null @@ -1,15 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module type S = Msat.S - -module Make (E : Expr_intf.S) - (Th : Plugin_intf.S with type term = E.Term.t - and type formula = E.Formula.t - and type proof = E.proof) - = Msat.Make (Make_mcsat_expr(E)) (Th) - - diff --git a/src/solver/mcsolver.mli b/src/solver/mcsolver.mli deleted file mode 100644 index 51f05b8a..00000000 --- a/src/solver/mcsolver.mli +++ /dev/null @@ -1,23 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Create McSat solver - - This module provides a functor to create an McSAt solver. -*) - -module type S = Msat.S -(** The interface exposed by the solver. *) - -module Make (E : Expr_intf.S) - (Th : Plugin_intf.S with type term = E.Term.t - and type formula = E.Formula.t - and type proof = E.proof) - : S with type term = E.Term.t - and type formula = E.Formula.t - and type Proof.lemma = E.proof -(** Functor to create a solver parametrised by the atomic formulas and a theory. *) - diff --git a/src/solver/solver.ml b/src/solver/solver.ml deleted file mode 100644 index d06de2e8..00000000 --- a/src/solver/solver.ml +++ /dev/null @@ -1,81 +0,0 @@ -(**************************************************************************) -(* *) -(* Alt-Ergo Zero *) -(* *) -(* Sylvain Conchon and Alain Mebsout *) -(* Universite Paris-Sud 11 *) -(* *) -(* Copyright 2011. This file is distributed under the terms of the *) -(* Apache Software License version 2.0 *) -(* *) -(**************************************************************************) - -module type S = Msat.S - -module DummyTheory(F : Formula_intf.S) = struct - (* We don't have anything to do since the SAT Solver already - * does propagation and conflict detection *) - - type formula = F.t - type proof = F.proof - type level = unit - - let dummy = () - let current_level () = () - let assume _ = Theory_intf.Sat - let backtrack _ = () - let if_sat _ = Theory_intf.Sat -end - -module Plugin(E : Formula_intf.S) - (Th : Theory_intf.S with type formula = E.t and type proof = E.proof) = struct - - type term = E.t - type formula = E.t - type proof = Th.proof - type level = Th.level - - let dummy = Th.dummy - - let current_level = Th.current_level - - let assume_get get = - function i -> - match get i with - | Plugin_intf.Lit f -> f - | _ -> assert false - - let assume_propagate propagate = - fun f l proof -> - propagate f (Plugin_intf.Consequence (l, proof)) - - let mk_slice s = { - Theory_intf.start = s.Plugin_intf.start; - length = s.Plugin_intf.length; - get = assume_get s.Plugin_intf.get; - push = s.Plugin_intf.push; - propagate = assume_propagate s.Plugin_intf.propagate; - } - - let assume s = Th.assume (mk_slice s) - - let backtrack = Th.backtrack - - let if_sat s = Th.if_sat (mk_slice s) - - - (* McSat specific functions *) - let assign _ = assert false - - let iter_assignable _ _ = () - - let eval _ = Plugin_intf.Unknown - -end - - -module Make (E : Formula_intf.S) - (Th : Theory_intf.S with type formula = E.t and type proof = E.proof) - = Msat.Make (Make_smt_expr(E)) (Plugin(E)(Th)) - - diff --git a/src/tseitin/Msat_tseitin.ml b/src/tseitin/Msat_tseitin.ml index e1901aa1..3dff62e8 100644 --- a/src/tseitin/Msat_tseitin.ml +++ b/src/tseitin/Msat_tseitin.ml @@ -14,12 +14,13 @@ module type Arg = Tseitin_intf.Arg module type S = Tseitin_intf.S -module Make (F : Tseitin_intf.Arg) = struct +module Make (A : Tseitin_intf.Arg) = struct + module F = A.Form exception Empty_Or type combinator = And | Or | Imp | Not - type atom = F.t + type atom = A.Form.t type t = | True | Lit of atom @@ -129,118 +130,34 @@ module Make (F : Tseitin_intf.Arg) = struct let ( @@ ) l1 l2 = List.rev_append l1 l2 (* let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *) *) - (* - let distrib l_and l_or = - let l = - if l_or = [] then l_and - else - List.rev_map - (fun x -> - match x with - | Lit _ -> Comb (Or, x::l_or) - | Comb (Or, l) -> Comb (Or, l @@ l_or) - | _ -> assert false - ) l_and - in - Comb (And, l) + type fresh_state = A.t - let rec flatten_or = function - | [] -> [] - | Comb (Or, l)::r -> l @@ (flatten_or r) - | Lit a :: r -> (Lit a)::(flatten_or r) - | _ -> assert false + type state = { + fresh: fresh_state; + mutable acc_or : (atom * atom list) list; + mutable acc_and : (atom * atom list) list; - let rec flatten_and = function - | [] -> [] - | Comb (And, l)::r -> l @@ (flatten_and r) - | a :: r -> a::(flatten_and r) + } + let create fresh : state = { + fresh; + acc_or=[]; + acc_and=[]; + } - let rec cnf f = - match f with - | Comb (Or, l) -> - begin - let l = List.rev_map cnf l in - let l_and, l_or = - List.partition (function Comb(And,_) -> true | _ -> false) l in - match l_and with - | [ Comb(And, l_conj) ] -> - let u = flatten_or l_or in - distrib l_conj u - - | Comb(And, l_conj) :: r -> - let u = flatten_or l_or in - cnf (Comb(Or, (distrib l_conj u)::r)) - - | _ -> - begin - match flatten_or l_or with - | [] -> assert false - | [r] -> r - | v -> Comb (Or, v) - end - end - | Comb (And, l) -> - Comb (And, List.rev_map cnf l) - | f -> f - - let rec mk_cnf = function - | Comb (And, l) -> - List.fold_left (fun acc f -> (mk_cnf f) @@ acc) [] l - - | Comb (Or, [f1;f2]) -> - let ll1 = mk_cnf f1 in - let ll2 = mk_cnf f2 in - List.fold_left - (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 - - | Comb (Or, f1 :: l) -> - let ll1 = mk_cnf f1 in - let ll2 = mk_cnf (Comb (Or, l)) in - List.fold_left - (fun acc l1 -> (List.rev_map (fun l2 -> l1 @@ l2)ll2) @@ acc) [] ll1 - - | Lit a -> [[a]] - | Comb (Not, [Lit a]) -> [[F.neg a]] - | _ -> assert false - - - let rec unfold mono f = - match f with - | Lit a -> a::mono - | Comb (Not, [Lit a]) -> - (F.neg a)::mono - | Comb (Or, l) -> - List.fold_left unfold mono l - | _ -> assert false - - let rec init monos f = - match f with - | Comb (And, l) -> - List.fold_left init monos l - | f -> (unfold [] f)::monos - - let make_cnf f = - let sfnc = cnf (sform f) in - init [] sfnc - *) - - let mk_proxy = F.fresh - - let acc_or = ref [] - let acc_and = ref [] + let mk_proxy st : F.t = A.fresh st.fresh (* build a clause by flattening (if sub-formulas have the same combinator) and proxy-ing sub-formulas that have the opposite operator. *) - let rec cnf f = match f with + let rec cnf st f = match f with | Lit a -> None, [a] | Comb (Not, [Lit a]) -> None, [F.neg a] | Comb (And, l) -> List.fold_left (fun (_, acc) f -> - match cnf f with + match cnf st f with | _, [] -> assert false | _cmb, [a] -> Some And, a :: acc | Some And, l -> @@ -249,8 +166,8 @@ module Make (F : Tseitin_intf.Arg) = struct (* acc_and := (proxy, l) :: !acc_and; *) (* proxy :: acc *) | Some Or, l -> - let proxy = mk_proxy () in - acc_or := (proxy, l) :: !acc_or; + let proxy = mk_proxy st in + st.acc_or <- (proxy, l) :: st.acc_or; Some And, proxy :: acc | None, l -> Some And, l @@ acc | _ -> assert false @@ -259,7 +176,7 @@ module Make (F : Tseitin_intf.Arg) = struct | Comb (Or, l) -> List.fold_left (fun (_, acc) f -> - match cnf f with + match cnf st f with | _, [] -> assert false | _cmb, [a] -> Some Or, a :: acc | Some Or, l -> @@ -268,20 +185,20 @@ module Make (F : Tseitin_intf.Arg) = struct (* acc_or := (proxy, l) :: !acc_or; *) (* proxy :: acc *) | Some And, l -> - let proxy = mk_proxy () in - acc_and := (proxy, l) :: !acc_and; + let proxy = mk_proxy st in + st.acc_and <- (proxy, l) :: st.acc_and; Some Or, proxy :: acc | None, l -> Some Or, l @@ acc - | _ -> assert false - ) (None, []) l + | _ -> assert false) + (None, []) l | _ -> assert false - let cnf f = + let cnf st f = let acc = match f with | True -> [] | Comb(Not, [True]) -> [[]] - | Comb (And, l) -> List.rev_map (fun f -> snd(cnf f)) l - | _ -> [snd (cnf f)] + | Comb (And, l) -> List.rev_map (fun f -> snd(cnf st f)) l + | _ -> [snd (cnf st f)] in let proxies = ref [] in (* encore clauses that make proxies in !acc_and equivalent to @@ -297,8 +214,8 @@ module Make (F : Tseitin_intf.Arg) = struct List.fold_left (fun (cl,acc) a -> (F.neg a :: cl), [np; a] :: acc) ([p],acc) l in - cl :: acc - ) acc !acc_and + cl :: acc) + acc st.acc_and in (* encore clauses that make proxies in !acc_or equivalent to their clause *) @@ -310,15 +227,15 @@ module Make (F : Tseitin_intf.Arg) = struct [l1 => p], [l2 => p], etc. *) let acc = List.fold_left (fun acc a -> [p; F.neg a]::acc) acc l in - (F.neg p :: l) :: acc - ) acc !acc_or + (F.neg p :: l) :: acc) + acc st.acc_or in acc - let make_cnf f = - acc_or := []; - acc_and := []; - cnf (sform f (fun f' -> f')) + let make_cnf st f : _ list list = + st.acc_or <- []; + st.acc_and <- []; + cnf st (sform f (fun f' -> f')) (* Naive CNF XXX remove??? let make_cnf f = mk_cnf (sform f) diff --git a/src/tseitin/Msat_tseitin.mli b/src/tseitin/Msat_tseitin.mli index 498667c5..85220b17 100644 --- a/src/tseitin/Msat_tseitin.mli +++ b/src/tseitin/Msat_tseitin.mli @@ -17,6 +17,6 @@ module type Arg = Tseitin_intf.Arg module type S = Tseitin_intf.S (** The exposed interface of Tseitin's CNF conversion. *) -module Make : functor (F : Arg) -> S with type atom = F.t +module Make(A : Arg) : S with type atom = A.Form.t and type fresh_state = A.t (** This functor provides an implementation of Tseitin's CNF conversion. *) diff --git a/src/tseitin/Tseitin_intf.ml b/src/tseitin/Tseitin_intf.ml index abdfcf63..de596d91 100644 --- a/src/tseitin/Tseitin_intf.ml +++ b/src/tseitin/Tseitin_intf.ml @@ -19,18 +19,23 @@ module type Arg = sig Tseitin's CNF conversion. *) + module Form : sig + type t + (** Type of atomic formulas. *) + + val neg : t -> t + (** Negation of atomic formulas. *) + + val print : Format.formatter -> t -> unit + (** Print the given formula. *) + end + type t - (** Type of atomic formulas. *) + (** State *) - val neg : t -> t - (** Negation of atomic formulas. *) - - val fresh : unit -> t + val fresh : t -> Form.t (** Generate fresh formulas (that are different from any other). *) - val print : Format.formatter -> t -> unit - (** Print the given formula. *) - end module type S = sig @@ -75,7 +80,15 @@ module type S = sig val make_equiv : t -> t -> t (** [make_equiv p q] creates the boolena formula "[p] is equivalent to [q]". *) - val make_cnf : t -> atom list list + type fresh_state + (** State used to produce fresh atoms *) + + type state + (** State used for the Tseitin transformation *) + + val create : fresh_state -> state + + val make_cnf : state -> t -> atom list list (** [make_cnf f] returns a conjunctive normal form of [f] under the form: a list (which is a conjunction) of lists (which are disjunctions) of atomic formulas. *) diff --git a/tests/jbuild b/tests/jbuild index deab296d..879d27cf 100644 --- a/tests/jbuild +++ b/tests/jbuild @@ -2,7 +2,7 @@ (executable ((name test_api) - (libraries (msat msat.tseitin msat.backend minismt.sat minismt.smt minismt.mcsat dolmen)) + (libraries (msat msat.tseitin msat.backend msat.sat)) (flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string)) (ocamlopt_flags (:standard -O3 -color always -unbox-closures -unbox-closures-factor 20)) diff --git a/tests/test_api.ml b/tests/test_api.ml index 838ceed0..be0bba02 100644 --- a/tests/test_api.ml +++ b/tests/test_api.ml @@ -8,8 +8,8 @@ Copyright 2014 Simon Cruanes open Msat -module F = Minismt_sat.Expr -module T = Msat_tseitin.Make(F) +module Th = Msat_sat.Th +module F = Msat_tseitin.Make(Th) let (|>) x f = f x @@ -42,20 +42,20 @@ 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 + val solve : t -> ?assumptions:F.atom list -> unit -> solver_res + val assume : t -> ?tag:int -> F.atom list list -> unit end let mk_solver (): (module BASIC_SOLVER) = let module S = struct - include Minismt_sat + 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 + | Unsat (Unsat_state us) -> + let p = us.get_proof () in Proof.check p; R_unsat end @@ -68,8 +68,8 @@ let errorf msg = Format.ksprintf error msg module Test = struct type action = - | A_assume of F.t list list - | A_solve of F.t list * [`Expect_sat | `Expect_unsat] + | A_assume of F.atom list list + | A_solve of F.atom list * [`Expect_sat | `Expect_unsat] type t = { name: string; @@ -77,11 +77,9 @@ module Test = struct } let mk_test name l = {name; actions=l} - let assume l = A_assume (List.map (List.map F.make) l) + let assume l = A_assume l let assume1 c = assume [c] - let solve ?(assumptions=[]) e = - let assumptions = List.map F.make assumptions in - A_solve (assumptions, e) + let solve ?(assumptions=[]) e = A_solve (assumptions, e) type result = | Pass