simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-21 16:56:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

large refactoring to keep only a simpler, easier CDCL(T) interface

Browse source 
- only one functor to instantiate
- explicit state that is carried around
- remove minismt stuff
This commit is contained in:
Simon Cruanes 2018-01-21 18:46:28 -06:00
parent 7324647fb1
commit d723aee809
55 changed files with 423 additions and 4074 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
minismt.opam
View file

@ -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/"

73
src/core/Expr_intf.ml
View file

@ -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

53
src/core/Formula_intf.ml
View file

@ -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

12
src/core/Heap.ml
View file

@ -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

12
src/core/Heap.mli
View file

@ -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

371
src/core/Internal.ml
View file

@ -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 "@{<Yellow>** 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: @[<hov>%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 "@[<v>Status:@,@[<hov 2>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 "@[<v>Current trail:@,@[<hov>%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);

27
src/core/Msat.ml
View file

@ -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

121
src/core/Plugin_intf.ml
View file

@ -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

29
src/core/Solver.ml
View file

@ -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
"@[<v>%s - Full resume:@,@[<hov 2>Trail:@\n%a@]@,\
@[<hov 2>Temp:@\n%a@]@,@[<hov 2>Hyps:@\n%a@]@,@[<hov 2>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

9
src/core/Solver.mli
View file

@ -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. *)

34
src/core/Solver_intf.ml
View file

@ -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

175
src/core/Solver_types.ml
View file

@ -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 "@[<hov>@@%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:@[<hov>%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:@[<hov>%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]

26
src/core/Solver_types.mli
View file

@ -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. *)

103
src/core/Solver_types_intf.ml
View file

@ -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

61
src/core/Theory_intf.ml
View file

@ -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

13
src/main/jbuild
View file

@ -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))
))

241
src/main/main.ml
View file

@ -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] <file>"
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),
"<s>[kMGT] Sets the size limit for the sat solver";
"-time", Arg.String (int_arg time_limit),
"<t>[smhd] Sets the time limit for the sat solver";
"-v", Arg.Int (fun i -> Log.set_debug i),
"<lvl> 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

13
src/mcsat/Minismt_mcsat.ml
View file

@ -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)

8
src/mcsat/Minismt_mcsat.mli
View file

@ -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

68
src/mcsat/README.md
View file

@ -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)$

99
src/mcsat/backtrack.ml
View file

@ -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

77
src/mcsat/backtrack.mli
View file

@ -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

232
src/mcsat/eclosure.ml
View file

@ -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

60
src/mcsat/eclosure.mli
View file

@ -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

13
src/mcsat/jbuild
View file

@ -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))
))

200
src/mcsat/plugin_mcsat.ml
View file

@ -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

70
src/sat/Expr_sat.ml
View file

@ -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)

10
src/sat/Minismt_sat.ml
View file

@ -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))

9
src/sat/Msat_sat.ml Normal file
View file

@ -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)

5
src/sat/Minismt_sat.mli → src/sat/Msat_sat.mli
View file

@ -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. *)

85
src/sat/Th_sat.ml Normal file
View file

@ -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

22
src/sat/Expr_sat.mli → src/sat/Th_sat.mli
View file

@ -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. *)

6
src/sat/jbuild
View file

@ -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

90
src/sat/type_sat.ml
View file

@ -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

12
src/sat/type_sat.mli
View file

@ -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

13
src/smt/Minismt_smt.ml
View file

@ -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)

11
src/smt/Minismt_smt.mli
View file

@ -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

525
src/smt/expr_smt.ml
View file

@ -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 "@[<hov 0>%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 = "<dummy>"; id_type = Type; }
let ty =
{ ty = TyVar id_ttype; ty_hash = -1; }
let id =
{ index = -2; id_name = "<dummy>"; 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)

326
src/smt/expr_smt.mli
View file

@ -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

13
src/smt/jbuild
View file

@ -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))
))

628
src/smt/type_smt.ml
View file

@ -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))

7
src/smt/type_smt.mli
View file

@ -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

90
src/smt/unionfind.ml
View file

@ -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

20
src/smt/unionfind.mli
View file

@ -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

12
src/solver/jbuild
View file

@ -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))
))

15
src/solver/mcsolver.ml
View file

@ -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)

23
src/solver/mcsolver.mli
View file

@ -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. *)

81
src/solver/solver.ml
View file

@ -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))

30
src/solver/solver.mli
View file

@ -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. *)

28
src/solver/type.ml
View file

@ -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

153
src/tseitin/Msat_tseitin.ml
View file

@ -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)

2
src/tseitin/Msat_tseitin.mli
View file

@ -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. *)

31
src/tseitin/Tseitin_intf.ml
View file

@ -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. *)

2
tests/jbuild
View file

@ -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))

24
tests/test_api.ml
View file

@ -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