diff --git a/minismt.opam b/minismt.opam deleted file mode 100644 index a38b471a..00000000 --- a/minismt.opam +++ /dev/null @@ -1,24 +0,0 @@ -opam-version: "1.2" -name: "minismt" -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" -] -available: [ - ocaml-version >= "4.03.0" -] -tags: [ "sat" "smt" ] -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..35d7d825 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; + (* 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,15 @@ module Make dirty=false; } - let create ?(size=`Big) ?st () : t = + let create ?(size=`Big) ?st th : 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 () + in create_ ~st ~size_trail ~size_lvl th + + let theory st = st.th (* Misc functions *) let to_float = float_of_int @@ -178,35 +187,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 +198,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 +214,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 +338,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 +355,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 +382,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 +472,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 +504,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 +535,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 +597,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 +695,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 +812,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 +847,11 @@ 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[@inline] slice_get st i = + let a = Vec.get st.trail i in + a.lit let slice_push st (l:formula list) (lemma:proof): unit = let atoms = List.rev_map (create_atom st) l in @@ -969,45 +859,52 @@ 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; + 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 = { + Theory_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; + on_backtrack = slice_on_backtrack st; + at_level_0 = slice_at_level_0 st; } (* full slice, for [if_sat] final check *) - let full_slice st : (_,_,_) Plugin_intf.slice = { - Plugin_intf.start = 0; + let full_slice st : (_,_) Theory_intf.slice = { + Theory_intf.start = 0; length = Vec.size st.trail; get = slice_get st; push = slice_push st; propagate = (fun _ -> assert false); + on_backtrack = slice_on_backtrack st; + at_level_0 = slice_at_level_0 st; } - (* some boolean literals were decided/propagated within Msat. Now we + (* 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 +915,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 st.th 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 +940,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 +961,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 +974,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 +1021,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 +1030,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 +1047,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 st.th (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 +1075,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..c15ff935 100644 --- a/src/core/Msat.ml +++ b/src/core/Msat.ml @@ -1,21 +1,31 @@ (** Main API *) -module Formula_intf = Formula_intf -module Plugin_intf = Plugin_intf module Theory_intf = Theory_intf -module Expr_intf = Expr_intf module Solver_types_intf = Solver_types_intf module Res = Res module 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 = { 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 = { @@ -28,10 +38,7 @@ type 'clause export = 'clause Solver_intf.export = { 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) - -module Make = Solver.Make +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..e6594f07 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 th : t = S.create ?size th (* 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 { 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 = @@ -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,10 +118,6 @@ 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 @@ -150,5 +140,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..8078c5ad 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 = { eval: 'form -> bool; (** Returns the valuation of a formula in the current state of the sat solver. @@ -22,11 +16,9 @@ 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. *) @@ -54,19 +46,19 @@ 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. *) type t (** Main solver type, containing all state for solving. *) - val create : ?size:[`Tiny|`Small|`Big] -> unit -> t + val create : ?size:[`Tiny|`Small|`Big] -> theory -> t (** Create new solver @param size the initial size of internal data structures. The bigger, the faster, but also the more RAM it uses. *) @@ -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, @@ -155,10 +144,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..e4016929 100644 --- a/src/core/Theory_intf.ml +++ b/src/core/Theory_intf.ml @@ -23,7 +23,13 @@ Copyright 2016 Simon Cruanes be used in an SMT solver. *) -type ('formula, 'proof) res = ('formula, 'proof) Plugin_intf.res = +type negated = + | Negated (** changed sign *) + | Same_sign (** kept sign *) +(** This type is used during the normalisation of formulas. + See {!val:Expr_intf.S.norm} for more details. *) + +type ('formula, 'proof) res = | Sat (** The current set of assumptions is satisfiable. *) | Unsat of 'formula list * 'proof @@ -45,13 +51,22 @@ type ('form, 'proof) slice = { that the clause [causes => lit] is a theory tautology. It is faster than pushing the associated clause but the clause will not be remembered by the sat solver, i.e it will not be used by the solver to do boolean propagation. *) + 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? *) } (** The type for a slice. Slices are some kind of view of the current propagation queue. They allow to look at the propagated literals, and to add new clauses to the solver. *) +module type FORM = sig +end + +(** {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 +74,41 @@ 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 assume : t -> (formula, proof) slice -> (formula, proof) res (** Assume the formulas in the slice, possibly pushing new formulas to be propagated, and returns the result of the new assumptions. *) - val if_sat : (formula, proof) slice -> (formula, proof) res + val if_sat : t -> (formula, proof) slice -> (formula, proof) res (** Called at the end of the search in case a model has been found. If no new clause is pushed, then 'sat' is returned, else search is resumed. *) - - val backtrack : 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/main/main.ml b/src/main/main.ml deleted file mode 100644 index c943952e..00000000 --- a/src/main/main.ml +++ /dev/null @@ -1,241 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -open Msat - -exception Incorrect_model -exception Out_of_time -exception Out_of_space - -let file = ref "" -let p_cnf = ref false -let p_check = ref false -let p_dot_proof = ref "" -let p_proof_print = ref false -let time_limit = ref 300. -let size_limit = ref 1000_000_000. - -module P = - Dolmen.Logic.Make(Dolmen.ParseLocation) - (Dolmen.Id)(Dolmen.Term)(Dolmen.Statement) - -module type S = sig - val do_task : Dolmen.Statement.t -> unit -end - -module Make - (S : Msat.S) - (T : Minismt.Type.S with type atom := S.atom) - : sig - val do_task : Dolmen.Statement.t -> unit - end = struct - - module D = Msat_backend.Dot.Make(S.Proof)(Msat_backend.Dot.Default(S.Proof)) - - let hyps = ref [] - - let st = S.create ~size:`Big () - - let check_model 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 - List.exists (fun x -> x) l - in - let l = List.map check_clause !hyps in - List.for_all (fun x -> x) l - - let prove ~assumptions () = - let res = S.solve st ~assumptions () in - let t = Sys.time () in - begin match res with - | S.Sat state -> - if !p_check then - if not (check_model state) then - raise Incorrect_model; - let t' = Sys.time () -. t in - Format.printf "Sat (%f/%f)@." t t' - | S.Unsat state -> - if !p_check then begin - let p = state.Msat.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 - D.print fmt p - end - end; - let t' = Sys.time () -. t in - Format.printf "Unsat (%f/%f)@." t t' - end - - let do_task s = - 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.Clause l -> - let cnf = T.antecedent (Dolmen.Term.or_ l) in - hyps := cnf @ !hyps; - S.assume st cnf - | Dolmen.Statement.Consequent t -> - let cnf = T.consequent t in - hyps := cnf @ !hyps; - S.assume st cnf - | Dolmen.Statement.Antecedent t -> - let cnf = T.antecedent t in - hyps := cnf @ !hyps; - S.assume st cnf - | Dolmen.Statement.Pack [ - { Dolmen.Statement.descr = Dolmen.Statement.Push 1;_ }; - { Dolmen.Statement.descr = Dolmen.Statement.Antecedent f;_ }; - { Dolmen.Statement.descr = Dolmen.Statement.Prove;_ }; - { Dolmen.Statement.descr = Dolmen.Statement.Pop 1;_ }; - ] -> - let assumptions = T.assumptions f in - prove ~assumptions () - | Dolmen.Statement.Prove -> - prove ~assumptions:[] () - | Dolmen.Statement.Set_info _ - | Dolmen.Statement.Set_logic _ -> () - | Dolmen.Statement.Exit -> exit 0 - | _ -> - Format.printf "Command not supported:@\n%a@." - 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) - -let solver = ref (module Sat : S) -let solver_list = [ - "sat", (module Sat : S); - "smt", (module Smt : S); - "mcsat", (module Mcsat : S); -] - -let error_msg opt arg l = - Format.fprintf Format.str_formatter "'%s' is not a valid argument for '%s', valid arguments are : %a" - arg opt (fun fmt -> List.iter (fun (s, _) -> Format.fprintf fmt "%s, " s)) l; - Format.flush_str_formatter () - -let set_flag opt arg flag l = - try - flag := List.assoc arg l - with Not_found -> - invalid_arg (error_msg opt arg l) - -let set_solver s = set_flag "Solver" s solver solver_list - -(* Arguments parsing *) -let int_arg r arg = - let l = String.length arg in - let multiplier m = - let arg1 = String.sub arg 0 (l-1) in - r := m *. (float_of_string arg1) - in - if l = 0 then raise (Arg.Bad "bad numeric argument") - else - try - match arg.[l-1] with - | 'k' -> multiplier 1e3 - | 'M' -> multiplier 1e6 - | 'G' -> multiplier 1e9 - | 'T' -> multiplier 1e12 - | 's' -> multiplier 1. - | 'm' -> multiplier 60. - | 'h' -> multiplier 3600. - | 'd' -> multiplier 86400. - | '0'..'9' -> r := float_of_string arg - | _ -> raise (Arg.Bad "bad numeric argument") - with Failure _ -> raise (Arg.Bad "bad numeric argument") - -let setup_gc_stat () = - at_exit (fun () -> - Gc.print_stat stdout; - ) - -let input_file = fun s -> file := s - -let usage = "Usage : main [options] " -let argspec = Arg.align [ - "-bt", Arg.Unit (fun () -> Printexc.record_backtrace true), - " Enable stack traces"; - "-cnf", Arg.Set p_cnf, - " Prints the cnf used."; - "-check", Arg.Set p_check, - " Build, check and print the proof (if output is set), if unsat"; - "-dot", Arg.Set_string p_dot_proof, - " If provided, print the dot proof in the given file"; - "-gc", Arg.Unit setup_gc_stat, - " Outputs statistics about the GC"; - "-s", Arg.String set_solver, - "{sat,smt,mcsat} Sets the solver to use (default smt)"; - "-size", Arg.String (int_arg size_limit), - "[kMGT] Sets the size limit for the sat solver"; - "-time", Arg.String (int_arg time_limit), - "[smhd] Sets the time limit for the sat solver"; - "-v", Arg.Int (fun i -> Log.set_debug i), - " Sets the debug verbose level"; - ] - -(* Limits alarm *) -let check () = - let t = Sys.time () in - let heap_size = (Gc.quick_stat ()).Gc.heap_words in - let s = float heap_size *. float Sys.word_size /. 8. in - if t > !time_limit then - raise Out_of_time - else if s > !size_limit then - raise Out_of_space - - -let main () = - (* Administrative duties *) - Arg.parse argspec input_file usage; - if !file = "" then ( - Arg.usage argspec usage; - exit 2 - ); - let al = Gc.create_alarm check in - - (* Interesting stuff happening *) - let lang, input = P.parse_file !file in - let module S = (val !solver : S) in - List.iter S.do_task input; - (* Small hack for dimacs, which do not output a "Prove" statement *) - begin match lang with - | P.Dimacs -> S.do_task @@ Dolmen.Statement.check_sat () - | _ -> () - end; - Gc.delete_alarm al; - () - -let () = - try - main () - with - | Out_of_time -> - Format.printf "Timeout@."; - exit 2 - | Out_of_space -> - Format.printf "Spaceout@."; - exit 3 - | 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) -> - 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 - in - Format.fprintf Format.std_formatter "While typing:@\n%a@\n%a: typing error\n%s@." - Dolmen.Term.print t Dolmen.ParseLocation.fmt loc msg; - if Printexc.backtrace_status () then - Format.fprintf Format.std_formatter "%s@." b - 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/README.md b/src/mcsat/README.md deleted file mode 100644 index 80ab1a01..00000000 --- a/src/mcsat/README.md +++ /dev/null @@ -1,68 +0,0 @@ - -# Equality in McSat - -## Basics - -McSat theories have different interfaces and requirements than classic SMT theories. -The good point of these additional requirements is that it becomes easier to combine -theories, since the assignments allow theories to exchange information about -the equality of terms. In a context where there are multiple theories, they each have -to handle the following operations: - -- return an assignment value for a given term -- receive a new assignment value for a term (the assignment may, or not, have been - done by another theory) -- receive a new assertion (i.e an atomic formula asserted to be true by the sat solver) - -With assignments, the reason for a theory returning UNSAT now becomes when -some term has no potential assignment value because of past assignments -and assertions, (or in some cases, an assignments decided by a theory A is -incompatible with the possible assignments of the same term according to theory B). - -When returning UNSAT, the theory must, as usual return a conflict clause. -The conflict clause must be a tautology, and such that every atomic proposition -in it must evaluate to false using assignments. - - -## Equality of uninterpreted types - -To handle equality on arbitrary values efficiently, we maintain a simple union-find -of known equalities (*NOT* computing congruence closure, only the reflexive-transitive -closure of the equalities), where each class can be tagged with an optional assignment. - -When receiving a new assertions by the sat, we update the union-find. When the theory is -asked for an assignment value for a term, we lookup its class. If it is tagged, we return -the tagged value. Else, we take an arbitrary representative $x$ of the class and return it. -When a new assignment $t \mapsto v$ is propagated by the sat solver, there are three cases: - -- the class of $t$ if not tagged, we then tag it with $t \mapsto v$ and continue -- the class of $t$ is already tagged with $\_ mapsto v$, we do nothing -- the class of $t$ is tagged with a $t' \mapsto v'$, we raise unsat, - using the explanation of why $t$ and $t'$ are in the same class and the equality - $t' = v'$ - -Additionally, in order to handle disequalities, each class contains the list of classes -it must be distinct from. There are then two possible reasons to raise unsat, when -a disequality $x <> y$ is invalidated by assignemnts or later equalities: - -- when two classes that should be distinct are merged -- when two classes that should be distinct are assigned to the same value - -in both cases, we use the union-find structure to get the explanation of why $x$ and $y$ -must now be equal (since their class have been merged), and use that to create the -conflict clause. - - -## Uninterpreted functions - -The uninterpreted function theory is much simpler, it doesn't return any assignemnt values -(the equality theory does it already), but rather check that the assignemnts so far are -coherent with the semantics of uninterpreted functions. - -So for each function asignment $f(x1,...,xn) \mapsto v$, we wait for all the arguments to -also be assigned to values $x1 \mapsto v1$, etc... $xn \mapsto vn$, and we add the binding -$(f,v1,...,vn) \mapsto (v,x1,...,xn)$ in a map (meaning that in the model $f$ applied to -$v1,...,vn$ is equal to $v$). If a binding $(f,v1,...,vn) \mapsto (v',y1,...,yn)$ already -exists (with $v' <> v$), then we raise UNSAT, with the explanation: -$( x1=y1 /\ ... /\ xn = yn) => f(x1,...,xn) = f(y1,...,yn)$ - 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..4b713c38 --- /dev/null +++ b/src/sat/Th_sat.ml @@ -0,0 +1,85 @@ + +exception Bad_atom +(** Exception raised if an atom cannot be created *) + +type proof = unit +(** A empty type for proofs *) + +type formula = int + +type t = { + mutable max_index: int; + mutable max_fresh: int; +} + +let create () : t = { + 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 61% rename from src/sat/Expr_sat.mli rename to src/sat/Th_sat.mli index a48603af..22035511 100644 --- a/src/sat/Expr_sat.mli +++ b/src/sat/Th_sat.mli @@ -4,28 +4,30 @@ (** 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 create : unit -> 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/sat/type_sat.ml b/src/sat/type_sat.ml deleted file mode 100644 index b809cb4f..00000000 --- a/src/sat/type_sat.ml +++ /dev/null @@ -1,90 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(* Log&Module Init *) -(* ************************************************************************ *) - -module Id = Dolmen.Id -module Ast = Dolmen.Term -module H = Hashtbl.Make(Id) -module Formula = Msat_tseitin.Make(Expr_sat) - -(* Exceptions *) -(* ************************************************************************ *) - -exception Typing_error of string * Dolmen.Term.t - -(* Identifiers *) -(* ************************************************************************ *) - -let symbols = H.create 42 - -let find_id id = - try - H.find symbols id - with Not_found -> - let res = Expr_sat.fresh () in - H.add symbols id res; - res - -(* Actual parsing *) -(* ************************************************************************ *) - -[@@@ocaml.warning "-9"] - -let rec parse = 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 - 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) - | { 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) - | { 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) - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply }, [p; q]) } -> - Formula.make_imply (parse p) (parse q) - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv }, [p; q]) } -> - Formula.make_equiv (parse p) (parse q) - | { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor }, [p; q]) } -> - Formula.make_xor (parse p) (parse q) - | t -> - raise (Typing_error ("Term is not a pure proposition", t)) - -[@@@ocaml.warning "+9"] - -(* Exported functions *) -(* ************************************************************************ *) - -let decl _ t = - raise (Typing_error ("Declarations are not allowed in pure sat", 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 - List.map (function - | [ x ] -> x - | _ -> assert false - ) cnf - -let antecedent t = - let f = parse t in - Formula.make_cnf f - -let consequent t = - let f = parse t in - Formula.make_cnf @@ Formula.make_not f - diff --git a/src/sat/type_sat.mli b/src/sat/type_sat.mli deleted file mode 100644 index a088602c..00000000 --- a/src/sat/type_sat.mli +++ /dev/null @@ -1,12 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** 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_sat module. *) - -include Minismt.Type.S with type atom := Expr_sat.t - 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/expr_smt.ml b/src/smt/expr_smt.ml deleted file mode 100644 index f3b8961f..00000000 --- a/src/smt/expr_smt.ml +++ /dev/null @@ -1,525 +0,0 @@ -(* - Base modules that defines the terms used in the prover. -*) - -(* Type definitions *) -(* ************************************************************************ *) - -(* Private aliases *) -type hash = int -type index = int - -(* Identifiers, parametrized by the kind of the type of the variable *) -type 'ty id = { - id_type : 'ty; - id_name : string; - index : index; (** unique *) -} - -(* Type for first order types *) -type ttype = Type - -(* The type of functions *) -type 'ty function_descr = { - fun_vars : ttype id list; (* prenex forall *) - fun_args : 'ty list; - fun_ret : 'ty; -} - -(* Types *) -type ty_descr = - | TyVar of ttype id (** Bound variables *) - | TyApp of ttype function_descr id * ty list - -and ty = { - ty : ty_descr; - mutable ty_hash : hash; (** lazy hash *) -} - -(* Terms & formulas *) -type term_descr = - | Var of ty id - | App of ty function_descr id * ty list * term list - -and term = { - term : term_descr; - t_type : ty; - mutable t_hash : hash; (* lazy hash *) -} - -type atom_descr = - | Pred of term - | Equal of term * term - -and atom = { - sign : bool; - atom : atom_descr; - mutable f_hash : hash; (* lazy hash *) -} - -(* Utilities *) -(* ************************************************************************ *) - -let rec list_cmp ord l1 l2 = - match l1, l2 with - | [], [] -> 0 - | [], _ -> -1 - | _, [] -> 1 - | x1::l1', x2::l2' -> - let c = ord x1 x2 in - if c = 0 - then list_cmp ord l1' l2' - else c - -(* Exceptions *) -(* ************************************************************************ *) - -exception Type_mismatch of term * ty * ty -exception Bad_arity of ty function_descr id * ty list * term list -exception Bad_ty_arity of ttype function_descr id * ty list - -(* Printing functions *) -(* ************************************************************************ *) - -module Print = struct - let rec list f sep fmt = function - | [] -> () - | [x] -> f fmt x - | x :: ((_ :: _) as r) -> - Format.fprintf fmt "%a%s" f x sep; - list f sep fmt r - - let id fmt v = Format.fprintf fmt "%s" v.id_name - let ttype fmt = function Type -> Format.fprintf fmt "Type" - - let rec ty fmt t = match t.ty with - | TyVar v -> id fmt v - | TyApp (f, []) -> - Format.fprintf fmt "%a" id f - | TyApp (f, l) -> - Format.fprintf fmt "%a(%a)" id f (list ty ", ") l - - let params fmt = function - | [] -> () - | l -> Format.fprintf fmt "∀ %a. " (list id ", ") l - - let signature print fmt f = - match f.fun_args with - | [] -> Format.fprintf fmt "%a%a" params f.fun_vars print f.fun_ret - | l -> Format.fprintf fmt "%a%a -> %a" params f.fun_vars - (list print " -> ") l print f.fun_ret - - let fun_ty = signature ty - let fun_ttype = signature ttype - - let id_type print fmt v = Format.fprintf fmt "%a : %a" id v print v.id_type - - let id_ty = id_type ty - let id_ttype = id_type ttype - let const_ty = id_type fun_ty - let const_ttype = id_type fun_ttype - - let rec term fmt t = match t.term with - | Var v -> id fmt v - | App (f, [], []) -> - Format.fprintf fmt "%a" id f - | App (f, [], args) -> - Format.fprintf fmt "%a(%a)" id f - (list term ", ") args - | App (f, tys, args) -> - Format.fprintf fmt "%a(%a; %a)" id f - (list ty ", ") tys - (list term ", ") args - - let atom_aux fmt f = - match f.atom with - | Equal (a, b) -> - Format.fprintf fmt "%a %s %a" - term a (if f.sign then "=" else "<>") term b - | Pred t -> - Format.fprintf fmt "%s%a" (if f.sign then "" else "¬ ") term t - - let atom fmt f = Format.fprintf fmt "⟦%a⟧" atom_aux f - -end - -(* Substitutions *) -(* ************************************************************************ *) - -module Subst = struct - module Mi = Map.Make(struct - type t = int * int - let compare (a, b) (c, d) = match compare a c with 0 -> compare b d | x -> x - end) - - type ('a, 'b) t = ('a * 'b) Mi.t - - (* Usual functions *) - let empty = Mi.empty - - let is_empty = Mi.is_empty - - let iter f = Mi.iter (fun _ (key, value) -> f key value) - - let fold f = Mi.fold (fun _ (key, value) acc -> f key value acc) - - let bindings s = Mi.fold (fun _ (key, value) acc -> (key, value) :: acc) s [] - - (* Comparisons *) - let equal f = Mi.equal (fun (_, value1) (_, value2) -> f value1 value2) - let compare f = Mi.compare (fun (_, value1) (_, value2) -> f value1 value2) - let hash h s = Mi.fold (fun i (_, value) acc -> Hashtbl.hash (acc, i, h value)) s 1 - - let choose m = snd (Mi.choose m) - - (* Iterators *) - let exists pred s = - try - iter (fun m s -> if pred m s then raise Exit) s; - false - with Exit -> - true - - let for_all pred s = - try - iter (fun m s -> if not (pred m s) then raise Exit) s; - true - with Exit -> - false - - let print print_key print_value fmt map = - let aux _ (key, value) = - Format.fprintf fmt "%a -> %a@ " print_key key print_value value - in - Format.fprintf fmt "@[%a@]" (fun _ -> Mi.iter aux) map - - module type S = sig - type 'a key - val get : 'a key -> ('a key, 'b) t -> 'b - val mem : 'a key -> ('a key, 'b) t -> bool - val bind : 'a key -> 'b -> ('a key, 'b) t -> ('a key, 'b) t - val remove : 'a key -> ('a key, 'b) t -> ('a key, 'b) t - end - - (* Variable substitutions *) - module Id = struct - type 'a key = 'a id - let tok v = (v.index, 0) - let get v s = snd (Mi.find (tok v) s) - let mem v s = Mi.mem (tok v) s - let bind v t s = Mi.add (tok v) (v, t) s - let remove v s = Mi.remove (tok v) s - end - -end - -(* Dummies *) -(* ************************************************************************ *) - -module Dummy = struct - - let id_ttype = - { index = -1; id_name = ""; id_type = Type; } - - let ty = - { ty = TyVar id_ttype; ty_hash = -1; } - - let id = - { index = -2; id_name = ""; id_type = ty; } - - let term = - { term = Var id; t_type = ty; t_hash = -1; } - - let atom = - { atom = Pred term; sign = true; f_hash = -1; } - -end - -(* Variables *) -(* ************************************************************************ *) - -module Id = struct - type 'a t = 'a id - - (* Hash & comparisons *) - let hash v = v.index - - let compare: 'a. 'a id -> 'a id -> int = - fun v1 v2 -> compare v1.index v2.index - - let equal v1 v2 = compare v1 v2 = 0 - - (* Printing functions *) - let print = Print.id - - (* Id count *) - let _count = ref 0 - - (* Constructors *) - let mk_new id_name id_type = - incr _count; - let index = !_count in - { index; id_name; id_type } - - let ttype name = mk_new name Type - let ty name ty = mk_new name ty - - let const name fun_vars fun_args fun_ret = - mk_new name { fun_vars; fun_args; fun_ret; } - - let ty_fun name n = - let rec replicate acc n = - if n <= 0 then acc - else replicate (Type :: acc) (n - 1) - in - const name [] (replicate [] n) Type - - let term_fun = const - - (* Builtin Types *) - let prop = ty_fun "Prop" 0 - let base = ty_fun "$i" 0 - -end - -(* Types *) -(* ************************************************************************ *) - -module Ty = struct - type t = ty - type subst = (ttype id, ty) Subst.t - - (* Hash & Comparisons *) - let rec hash_aux t = match t.ty with - | TyVar v -> Id.hash v - | TyApp (f, args) -> - Hashtbl.hash (Id.hash f, List.map hash args) - - and hash t = - if t.ty_hash = -1 then - t.ty_hash <- hash_aux t; - t.ty_hash - - let discr ty = match ty.ty with - | TyVar _ -> 1 - | TyApp _ -> 2 - - let rec compare u v = - let hu = hash u and hv = hash v in - if hu <> hv then Pervasives.compare hu hv - else match u.ty, v.ty with - | TyVar v1, TyVar v2 -> Id.compare v1 v2 - | TyApp (f1, args1), TyApp (f2, args2) -> - begin match Id.compare f1 f2 with - | 0 -> list_cmp compare args1 args2 - | x -> x - end - | _, _ -> Pervasives.compare (discr u) (discr v) - - let equal u v = - u == v || (hash u = hash v && compare u v = 0) - - (* Printing functions *) - let print = Print.ty - - (* Constructors *) - let mk_ty ty = { ty; ty_hash = -1; } - - let of_id v = mk_ty (TyVar v) - - let apply f args = - assert (f.id_type.fun_vars = []); - if List.length args <> List.length f.id_type.fun_args then - raise (Bad_ty_arity (f, args)) - else - mk_ty (TyApp (f, args)) - - (* Builtin types *) - let prop = apply Id.prop [] - let base = apply Id.base [] - - (* Substitutions *) - let rec subst_aux map t = match t.ty with - | TyVar v -> begin try Subst.Id.get v map with Not_found -> t end - | TyApp (f, args) -> - let new_args = List.map (subst_aux map) args in - if List.for_all2 (==) args new_args then t - else apply f new_args - - let subst map t = if Subst.is_empty map then t else subst_aux map t - - (* Typechecking *) - let instantiate f tys args = - if List.length f.id_type.fun_vars <> List.length tys || - List.length f.id_type.fun_args <> List.length args then - raise (Bad_arity (f, tys, args)) - else - let map = List.fold_left2 (fun acc v ty -> Subst.Id.bind v ty acc) Subst.empty f.id_type.fun_vars tys in - let fun_args = List.map (subst map) f.id_type.fun_args in - List.iter2 (fun t ty -> - if not (equal t.t_type ty) then raise (Type_mismatch (t, t.t_type, ty))) - args fun_args; - subst map f.id_type.fun_ret - -end - -(* Terms *) -(* ************************************************************************ *) - -module Term = struct - type t = term - type subst = (ty id, term) Subst.t - - (* Hash & Comparisons *) - let rec hash_aux t = match t.term with - | Var v -> Id.hash v - | App (f, tys, args) -> - let l = List.map Ty.hash tys in - let l' = List.map hash args in - Hashtbl.hash (Id.hash f, l, l') - - and hash t = - if t.t_hash = -1 then - t.t_hash <- hash_aux t; - t.t_hash - - let discr t = match t.term with - | Var _ -> 1 - | App _ -> 2 - - let rec compare u v = - let hu = hash u and hv = hash v in - if hu <> hv then Pervasives.compare hu hv - else match u.term, v.term with - | Var v1, Var v2 -> Id.compare v1 v2 - | App (f1, tys1, args1), App (f2, tys2, args2) -> - begin match Id.compare f1 f2 with - | 0 -> - begin match list_cmp Ty.compare tys1 tys2 with - | 0 -> list_cmp compare args1 args2 - | x -> x - end - | x -> x - end - | _, _ -> Pervasives.compare (discr u) (discr v) - - let equal u v = - u == v || (hash u = hash v && compare u v = 0) - - (* Printing functions *) - let print = Print.term - - (* Constructors *) - let mk_term term t_type = - { term; t_type; t_hash = -1; } - - let of_id v = - mk_term (Var v) v.id_type - - let apply f ty_args t_args = - mk_term (App (f, ty_args, t_args)) (Ty.instantiate f ty_args t_args) - - (* Substitutions *) - let rec subst_aux ty_map t_map t = match t.term with - | Var v -> begin try Subst.Id.get v t_map with Not_found -> t end - | App (f, tys, args) -> - let new_tys = List.map (Ty.subst ty_map) tys in - let new_args = List.map (subst_aux ty_map t_map) args in - if List.for_all2 (==) new_tys tys && List.for_all2 (==) new_args args then t - else apply f new_tys new_args - - let subst ty_map t_map t = - if Subst.is_empty ty_map && Subst.is_empty t_map then - t - else - subst_aux ty_map t_map t - - let rec replace (t, t') t'' = match t''.term with - | _ when equal t t'' -> t' - | App (f, ty_args, t_args) -> - apply f ty_args (List.map (replace (t, t')) t_args) - | _ -> t'' - -end - -(* Formulas *) -(* ************************************************************************ *) - -module Atom = struct - type t = atom - - type proof = unit - - (* Hash & Comparisons *) - let h_eq = 2 - let h_pred = 3 - - let rec hash_aux f = match f.atom with - | Equal (t1, t2) -> - Hashtbl.hash (h_eq, Term.hash t1, Term.hash t2) - | Pred t -> - Hashtbl.hash (h_pred, Term.hash t) - - and hash f = - if f.f_hash = -1 then - f.f_hash <- hash_aux f; - f.f_hash - - let discr f = match f.atom with - | Equal _ -> 1 - | Pred _ -> 2 - - let compare f g = - let hf = hash f and hg = hash g in - if hf <> hg then Pervasives.compare hf hg - else match f.atom, g.atom with - | Equal (u1, v1), Equal(u2, v2) -> - list_cmp Term.compare [u1; v1] [u2; v2] - | Pred t1, Pred t2 -> Term.compare t1 t2 - | _, _ -> Pervasives.compare (discr f) (discr g) - - let equal u v = - u == v || (hash u = hash v && compare u v = 0) - - (* Printing functions *) - let print = Print.atom - - (* Constructors *) - let mk_formula f = { - sign = true; - atom = f; - f_hash = -1; - } - - let dummy = Dummy.atom - - let pred t = - if not (Ty.equal Ty.prop t.t_type) then - raise (Type_mismatch (t, t.t_type, Ty.prop)) - 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 } - - let eq a b = - if not (Ty.equal a.t_type b.t_type) then - raise (Type_mismatch (b, b.t_type, a.t_type)) - else if Term.compare a b < 0 then - mk_formula (Equal (a, b)) - else - mk_formula (Equal (b, a)) - - let norm f = - { f with sign = true }, - if f.sign then Formula_intf.Same_sign - else Formula_intf.Negated - -end - -module Formula = Msat_tseitin.Make(Atom) - diff --git a/src/smt/expr_smt.mli b/src/smt/expr_smt.mli deleted file mode 100644 index 03f0b07c..00000000 --- a/src/smt/expr_smt.mli +++ /dev/null @@ -1,326 +0,0 @@ - -(** Expressions for TabSat *) - -(** {2 Type definitions} *) - -(** These are custom types used in functions later. *) - -(** {3 Identifiers} *) - -(** Identifiers are the basic building blocks used to build types terms and expressions. *) - -type hash -type index = private int - -(** Private aliases to provide access. You should not have any need - to use these, instead use the functions provided by this module. *) - -type 'ty id = private { - id_type : 'ty; - id_name : string; - index : index; (** unique *) -} - -(** The type of identifiers. An ['a id] is an identifier whose solver-type - is represented by an inhabitant of type ['a]. - All identifier have an unique [index] which is used for comparison, - so that the name of a variable is only there for tracability - and/or pretty-printing. *) - -(** {3 Types} *) - -type ttype = Type - -(** The caml type of solver-types. *) - -type 'ty function_descr = private { - fun_vars : ttype id list; (* prenex forall *) - fun_args : 'ty list; - fun_ret : 'ty; -} - -(** This represents the solver-type of a function. - Functions can be polymorphic in the variables described in the - [fun_vars] field. *) - -type ty_descr = private - | TyVar of ttype id - (** bound variables (i.e should only appear under a quantifier) *) - | TyApp of ttype function_descr id * ty list - (** application of a constant to some arguments *) - -and ty = private { - ty : ty_descr; - mutable ty_hash : hash; (** Use Ty.hash instead *) -} - -(** These types defines solver-types, i.e the representation of the types - of terms in the solver. Record definition for [type ty] is shown in order - to be able to use the [ty.ty] field in patter matches. Other fields shoud not - be accessed directly, but throught the functions provided by the [Ty] module. *) - -(** {3 Terms} *) - -type term_descr = private - | Var of ty id - (** bound variables (i.e should only appear under a quantifier) *) - | App of ty function_descr id * ty list * term list - (** application of a constant to some arguments *) - -and term = private { - term : term_descr; - t_type : ty; - mutable t_hash : hash; (** Do not use this filed, call Term.hash instead *) -} - -(** Types defining terms in the solver. The definition is vary similar to that - of solver-types, except for type arguments of polymorphic functions which - are explicit. This has the advantage that there is a clear and typed distinction - between solver-types and terms, but may lead to some duplication of code - in some places. *) - -(** {3 Formulas} *) - -type atom_descr = private - (** Atoms *) - | Pred of term - | Equal of term * term - -and atom = private { - sign : bool; - atom : atom_descr; - mutable f_hash : hash; (** Use Formula.hash instead *) -} - -(** The type of atoms in the solver. The list of free arguments in quantifiers - is a bit tricky, so you should not touch it (see full doc for further - explanations). *) - -(** {3 Exceptions} *) - -exception Type_mismatch of term * ty * ty -(* Raised when as Type_mismatch(term, actual_type, expected_type) *) - -exception Bad_arity of ty function_descr id * ty list * term list -exception Bad_ty_arity of ttype function_descr id * ty list -(** Raised when trying to build an application with wrong arity *) - -(** {2 Printing} *) - -module Print : sig - (** Pretty printing functions *) - - val id : Format.formatter -> 'a id -> unit - val id_ty : Format.formatter -> ty id -> unit - val id_ttype : Format.formatter -> ttype id -> unit - - val const_ty : Format.formatter -> ty function_descr id -> unit - val const_ttype : Format.formatter -> ttype function_descr id -> unit - - val ty : Format.formatter -> ty -> unit - val fun_ty : Format.formatter -> ty function_descr -> unit - - val ttype : Format.formatter -> ttype -> unit - val fun_ttype : Format.formatter -> ttype function_descr -> unit - - val term : Format.formatter -> term -> unit - val atom : Format.formatter -> atom -> unit -end - -(** {2 Identifiers & Metas} *) - -module Id : sig - type 'a t = 'a id - (* Type alias *) - - val hash : 'a t -> int - val equal : 'a t -> 'a t -> bool - val compare : 'a t -> 'a t -> int - (** Usual functions for hash/comparison *) - - val print : Format.formatter -> 'a t -> unit - (** Printing for variables *) - - val prop : ttype function_descr id - val base : ttype function_descr id - (** Constants representing the type for propositions and a default type - for term, respectively. *) - - val ttype : string -> ttype id - (** Create a fresh type variable with the given name. *) - - val ty : string -> ty -> ty id - (** Create a fresh variable with given name and type *) - - val ty_fun : string -> int -> ttype function_descr id - (** Create a fresh type constructor with given name and arity *) - - val term_fun : string -> ttype id list -> ty list -> ty -> ty function_descr id - (** [ty_fun name type_vars arg_types return_type] returns a fresh constant symbol, - possibly polymorphic with respect to the variables in [type_vars] (which may appear in the - types in [arg_types] and in [return_type]). *) - -end - -(** {2 Substitutions} *) - -module Subst : sig - (** Module to handle substitutions *) - - type ('a, 'b) t - (** The type of substitutions from values of type ['a] to values of type ['b]. *) - - val empty : ('a, 'b) t - (** The empty substitution *) - - val is_empty : ('a, 'b) t -> bool - (** Test wether a substitution is empty *) - - val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit - (** Iterates over the bindings of the substitution. *) - - val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c - (** Fold over the elements *) - - val bindings : ('a, 'b) t -> ('a * 'b) list - (** Returns the list of bindings ofa substitution. *) - - val exists : ('a -> 'b -> bool) -> ('a, 'b) t -> bool - (** Tests wether the predicate holds for at least one binding. *) - - val for_all : ('a -> 'b -> bool) -> ('a, 'b) t -> bool - (** Tests wether the predicate holds for all bindings. *) - - val hash : ('b -> int) -> ('a, 'b) t -> int - val compare : ('b -> 'b -> int) -> ('a, 'b) t -> ('a, 'b) t -> int - val equal : ('b -> 'b -> bool) -> ('a, 'b) t -> ('a, 'b) t -> bool - (** Comparison and hash functions, with a comparison/hash function on values as parameter *) - - val print : - (Format.formatter -> 'a -> unit) -> - (Format.formatter -> 'b -> unit) -> - Format.formatter -> ('a, 'b) t -> unit - (** Prints the substitution, using the given functions to print keys and values. *) - - val choose : ('a, 'b) t -> 'a * 'b - (** Return one binding of the given substitution, or raise Not_found if the substitution is empty.*) - - (** {5 Concrete subtitutions } *) - module type S = sig - type 'a key - val get : 'a key -> ('a key, 'b) t -> 'b - (** [get v subst] returns the value associated with [v] in [subst], if it exists. - @raise Not_found if there is no binding for [v]. *) - val mem : 'a key -> ('a key, 'b) t -> bool - (** [get v subst] returns wether there is a value associated with [v] in [subst]. *) - val bind : 'a key -> 'b -> ('a key, 'b) t -> ('a key, 'b) t - (** [bind v t subst] returns the same substitution as [subst] with the additional binding from [v] to [t]. - Erases the previous binding of [v] if it exists. *) - val remove : 'a key -> ('a key, 'b) t -> ('a key, 'b) t - (** [remove v subst] returns the same substitution as [subst] except for [v] which is unbound in the returned substitution. *) - end - - module Id : S with type 'a key = 'a id -end - -(** {2 Types} *) - -module Ty : sig - type t = ty - (** Type alias *) - - type subst = (ttype id, ty) Subst.t - (** The type of substitutions over types. *) - - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - (** Usual hash/compare functions *) - - val print : Format.formatter -> t -> unit - - val prop : ty - val base : ty - (** The type of propositions and individuals *) - - val of_id : ttype id -> ty - (** Creates a type from a variable *) - - val apply : ttype function_descr id -> ty list -> ty - (** Applies a constant to a list of types *) - - val subst : subst -> ty -> ty - (** Substitution over types. *) - -end - -(** {2 Terms} *) - -module Term : sig - type t = term - (** Type alias *) - - type subst = (ty id, term) Subst.t - (** The type of substitutions in types. *) - - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - (** Usual hash/compare functions *) - - val print : Format.formatter -> t -> unit - (** Printing functions *) - - val of_id : ty id -> term - (** Create a term from a variable *) - - val apply : ty function_descr id -> ty list -> term list -> term - (** Applies a constant function to type arguments, then term arguments *) - - val subst : Ty.subst -> subst -> term -> term - (** Substitution over types. *) - - val replace : term * term -> term -> term - (** [replace (t, t') t''] returns the term [t''] where every occurence of [t] - has been replace by [t']. *) - -end - -(** {2 Formulas} *) - -module Atom : sig - type t = atom - type proof = unit - (** Type alias *) - - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - (** Usual hash/compare functions *) - - val print : Format.formatter -> t -> unit - (** Printing functions *) - - 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} *) - - val pred : term -> atom - (** Create a atom from a term. The given term must have type {!Ty.prop} *) - - val neg : atom -> atom - (** Returns the negation of the given atom *) - - val norm : atom -> atom * Formula_intf.negated - (** Normalization functions as required by msat. *) - -end - -module Formula : Msat_tseitin.S with type atom = 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/smt/unionfind.ml b/src/smt/unionfind.ml deleted file mode 100644 index ab81a1ad..00000000 --- a/src/smt/unionfind.ml +++ /dev/null @@ -1,90 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module type OrderedType = sig - type t - val compare : t -> t -> int -end - -(* Union-find Module *) -module Make(T : OrderedType) = struct - exception Unsat of T.t * T.t - - type var = T.t - module M = Map.Make(T) - - (* TODO: better treatment of inequalities *) - - type t = { - rank : int M.t; - forbid : ((var * var) list); - mutable parent : var M.t; - } - - let empty = { - rank = M.empty; - forbid = []; - parent = M.empty; - } - - let find_map m i default = - try - M.find i m - with Not_found -> - default - - let rec find_aux f i = - let fi = find_map f i i in - if fi = i then - (f, i) - else - let f, r = find_aux f fi in - let f = M.add i r f in - (f, r) - - let find h x = - let f, cx = find_aux h.parent x in - h.parent <- f; - cx - - (* Highly inefficient treatment of inequalities *) - let possible h = - let aux (a, b) = - let ca = find h a in - let cb = find h b in - if T.compare ca cb = 0 then - raise (Unsat (a, b)) - in - List.iter aux h.forbid; - h - - let union_aux h x y = - let cx = find h x in - let cy = find h y in - if cx != cy then begin - let rx = find_map h.rank cx 0 in - let ry = find_map h.rank cy 0 in - if rx > ry then - { h with parent = M.add cy cx h.parent } - else if ry > rx then - { h with parent = M.add cx cy h.parent } - else - { rank = M.add cx (rx + 1) h.rank; - parent = M.add cy cx h.parent; - forbid = h.forbid; } - end else - h - - let union h x y = possible (union_aux h x y) - - let forbid h x y = - let cx = find h x in - let cy = find h y in - if cx = cy then - raise (Unsat (x, y)) - else - { h with forbid = (x, y) :: h.forbid } -end diff --git a/src/smt/unionfind.mli b/src/smt/unionfind.mli deleted file mode 100644 index adf2cd25..00000000 --- a/src/smt/unionfind.mli +++ /dev/null @@ -1,20 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module type OrderedType = sig - type t - val compare : t -> t -> int -end - -module Make(T : OrderedType) : sig - type t - exception Unsat of T.t * T.t - val empty : t - val find : t -> T.t -> T.t - val union : t -> T.t -> T.t -> t - val forbid : t -> T.t -> T.t -> t -end - diff --git a/src/solver/jbuild b/src/solver/jbuild deleted file mode 100644 index f3176323..00000000 --- a/src/solver/jbuild +++ /dev/null @@ -1,12 +0,0 @@ -; vim:ft=lisp: - -(library - ((name minismt) - (public_name minismt) - (libraries (msat dolmen)) - (synopsis "minismt") - (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/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/solver/solver.mli b/src/solver/solver.mli deleted file mode 100644 index 77efd675..00000000 --- a/src/solver/solver.mli +++ /dev/null @@ -1,30 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -(** Create SAT/SMT Solvers - - This module provides a functor to create an SMT solver. Additionally, it also - gives a functor that produce an adequate empty theory that can be given to the [Make] - functor in order to create a pure SAT solver. -*) - -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 -(** Functor to create a SMT Solver parametrised by the atomic - formulas and a theory. *) - diff --git a/src/solver/type.ml b/src/solver/type.ml deleted file mode 100644 index 693f35ce..00000000 --- a/src/solver/type.ml +++ /dev/null @@ -1,28 +0,0 @@ - -(** Typechecking of terms from Dolmen.Term.t - This module defines the requirements for typing expre'ssions from dolmen. *) - -module type S = sig - - type atom - (** The type of atoms that will be fed to tha sovler. *) - - exception Typing_error of string * Dolmen.Term.t - (** Exception raised during typechecking. *) - - val decl : 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 - (** New definition, i.e an identifier and the term it is equal to. *) - - val assumptions : 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 - (** 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). *) - -end 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..16e14d94 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,14 +42,14 @@ 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 - let create() = create() + include Msat_sat + let create() = create (Msat_sat.Th.create()) let solve st ?assumptions () = match solve st ?assumptions() with | Sat _ -> @@ -68,20 +68,20 @@ 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; actions: action list; } + let st = F.create @@ Th.create() + 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