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 8c8209c08c
58 changed files with 777 additions and 2721 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
Makefile
View file

@ -12,7 +12,8 @@ OPTS= -j $(J)
LIB=$(addprefix $(NAME), .cma .cmxa .cmxs)
all: build-dev test
all: build test
all-dev: build-dev test
build:
jbuilder build $(OPTS) @install
@ -20,12 +21,15 @@ build:
build-dev:
jbuilder build $(OPTS) @install --dev
test: build
build-test: build
jbuilder build $(OPTS) src/main_test/msat_test.exe
test: build-test
@echo "run API tests…"
jbuilder runtest
@echo "run benchmarks…"
# @/usr/bin/time -f "%e" ./tests/run smt
@/usr/bin/time -f "%e" ./tests/run mcsat
@/usr/bin/time -f "%e" ./tests/run smt
# @/usr/bin/time -f "%e" ./tests/run mcsat
enable_log:
cd src/core; ln -sf log_real.ml log.ml

2
msat.exe
View file

@ -1 +1 @@
_build/default/src/main/main.exe
_build/default/src/main_test/msat_test.exe

6
minismt.opam → msat_test.opam
View file

@ -1,15 +1,12 @@
opam-version: "1.2"
name: "minismt"
name: "msat_test"
license: "Apache"
version: "dev"
author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"]
maintainer: ["guillaume.bury@gmail.com" "simon.cruanes.2007@m4x.org"]
build: ["jbuilder" "build" "@install" "-p" name]
build-doc: ["jbuilder" "build" "@doc" "-p" name]
install: ["jbuilder" "install" name]
remove: ["jbuilder" "uninstall" name]
depends: [
"ocamlfind" {build}
"jbuilder" {build}
"dolmen"
"msat"
@ -22,3 +19,4 @@ homepage: "https://github.com/Gbury/mSAT"
dev-repo: "https://github.com/Gbury/mSAT.git"
bug-reports: "https://github.com/Gbury/mSAT/issues/"

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

401
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 lazy_t;
(* Clauses are simplified for eficiency purposes. In the following
vectors, the comments actually refer to the original non-simplified
clause. *)
@ -73,16 +74,20 @@ module Make
mutable next_decision : atom option;
(* When the last conflict was a semantic one, this stores the next decision to make *)
trail : trail_elt Vec.t;
trail : atom Vec.t;
(* decision stack + propagated elements (atoms or assignments). *)
elt_levels : int Vec.t;
(* decision levels in [trail] *)
th_levels : Plugin.level Vec.t;
(* theory states corresponding to elt_levels *)
user_levels : int Vec.t;
(* user levels in [clauses_temp] *)
(* user levels in [clause_tmp] *)
backtrack_levels : int Vec.t;
(* user levels in [backtrack] *)
backtrack : (unit -> unit) Vec.t;
(** Actions to call when backtracking *)
mutable th_head : int;
(* Start offset in the queue {!trail} of
@ -122,8 +127,9 @@ module Make
}
(* Starting environment. *)
let create_ ~st ~size_trail ~size_lvl () : t = {
let create_ ~st ~size_trail ~size_lvl th : t = {
st;
th;
unsat_conflict = None;
next_decision = None;
@ -137,9 +143,10 @@ module Make
th_head = 0;
elt_head = 0;
trail = Vec.make size_trail (Trail_elt.of_atom Atom.dummy);
trail = Vec.make size_trail Atom.dummy;
elt_levels = Vec.make size_lvl (-1);
th_levels = Vec.make size_lvl Plugin.dummy;
backtrack_levels = Vec.make size_lvl (-1);
backtrack = Vec.make size_lvl (fun () -> ());
user_levels = Vec.make 0 (-1);
order = H.create();
@ -153,13 +160,7 @@ module Make
dirty=false;
}
let create ?(size=`Big) ?st () : t =
let st = match st with Some s -> s | None -> St.create ~size () in
let size_trail, size_lvl = match size with
| `Tiny -> 0, 0
| `Small -> 32, 16
| `Big -> 600, 50
in create_ ~st ~size_trail ~size_lvl ()
let[@inline] theory st = Lazy.force st.th
(* Misc functions *)
let to_float = float_of_int
@ -178,35 +179,9 @@ module Make
| Some _ -> true
| None -> false
(* Iteration over subterms.
When incrementing activity, we want to be able to iterate over
all subterms of a formula. However, the function provided by the theory
may be costly (if it walks a tree-like structure, and does some processing
to ignore some subterms for instance), so we want to 'cache' the list
of subterms of each formula, so we have a field [v_assignable]
directly in variables to do so. *)
let iter_sub f v =
if St.mcsat then
match v.v_assignable with
| Some l -> List.iter f l
| None -> assert false
(* When we have a new literal,
we need to first create the list of its subterms. *)
let mk_atom st (f:St.formula) : atom =
let res = Atom.make st.st f in
if St.mcsat then (
begin match res.var.v_assignable with
| Some _ -> ()
| None ->
let l = ref [] in
Plugin.iter_assignable
(fun t -> l := Lit.make st.st t :: !l)
res.var.pa.lit;
res.var.v_assignable <- Some !l;
end;
);
res
let[@inline] mk_atom st (f:St.formula) : atom = Atom.make st.st f
(* Variable and literal activity.
Activity is used to decide on which variable to decide when propagation
@ -215,27 +190,11 @@ module Make
When we add a variable (which wraps a formula), we also need to add all
its subterms.
*)
let rec insert_var_order st (elt:elt) : unit =
H.insert st.order elt;
begin match elt with
| E_lit _ -> ()
| E_var v -> insert_subterms_order st v
end
and insert_subterms_order st (v:St.var) : unit =
iter_sub (fun t -> insert_var_order st (Elt.of_lit t)) v
(* Add new litterals/atoms on which to decide on, even if there is no
clause that constrains it.
We could maybe check if they have already has been decided before
inserting them into the heap, if it appears that it helps performance. *)
let new_lit st t =
let l = Lit.make st.st t in
insert_var_order st (E_lit l)
let[@inline] insert_var_order st (v:var) : unit = H.insert st.order v
let new_atom st (p:formula) : unit =
let a = mk_atom st p in
insert_var_order st (E_var a.var)
insert_var_order st a.var
(* Rather than iterate over all the heap when we want to decrease all the
variables/literals activity, we instead increase the value by which
@ -247,38 +206,18 @@ module Make
st.clause_incr <- st.clause_incr *. clause_decay
(* increase activity of [v] *)
let var_bump_activity_aux st v =
let var_bump_activity st v =
v.v_weight <- v.v_weight +. st.var_incr;
if v.v_weight > 1e100 then (
for i = 0 to St.nb_elt st.st - 1 do
Elt.set_weight (St.get_elt st.st i) ((Elt.weight (St.get_elt st.st i)) *. 1e-100)
Var.set_weight (St.get_elt st.st i) ((Var.weight (St.get_elt st.st i)) *. 1e-100)
done;
st.var_incr <- st.var_incr *. 1e-100;
);
let elt = Elt.of_var v in
if H.in_heap elt then (
H.decrease st.order elt
if H.in_heap v then (
H.decrease st.order v
)
(* increase activity of literal [l] *)
let lit_bump_activity_aux st (l:lit): unit =
l.l_weight <- l.l_weight +. st.var_incr;
if l.l_weight > 1e100 then (
for i = 0 to St.nb_elt st.st - 1 do
Elt.set_weight (St.get_elt st.st i) ((Elt.weight (St.get_elt st.st i)) *. 1e-100)
done;
st.var_incr <- st.var_incr *. 1e-100;
);
let elt = Elt.of_lit l in
if H.in_heap elt then (
H.decrease st.order elt
)
(* increase activity of var [v] *)
let var_bump_activity st (v:var): unit =
var_bump_activity_aux st v;
iter_sub (lit_bump_activity_aux st) v
(* increase activity of clause [c] *)
let clause_bump_activity st (c:clause) : unit =
c.activity <- c.activity +. st.clause_incr;
@ -391,7 +330,7 @@ module Make
assert (st.th_head = Vec.size st.trail);
assert (st.elt_head = Vec.size st.trail);
Vec.push st.elt_levels (Vec.size st.trail);
Vec.push st.th_levels (Plugin.current_level ()); (* save the current theory state *)
Vec.push st.backtrack_levels (Vec.size st.backtrack); (* save the current theory state *)
()
(* Attach/Detach a clause.
@ -408,6 +347,15 @@ module Make
c.attached <- true;
()
let backtrack_down_to (st:t) (l:int): unit =
Log.debugf 2
(fun k->k "@{<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 +374,35 @@ module Make
(* Now we need to cleanup the vars that are not valid anymore
(i.e to the right of elt_head in the queue. *)
for c = st.elt_head to Vec.size st.trail - 1 do
match (Vec.get st.trail c) with
let a = Vec.get st.trail c in
(* A literal is unassigned, we nedd to add it back to
the heap of potentially assignable literals, unless it has
a level lower than [lvl], in which case we just move it back. *)
| Lit l ->
if l.l_level <= lvl then (
Vec.set st.trail !head (Trail_elt.of_lit l);
head := !head + 1
) else (
l.assigned <- None;
l.l_level <- -1;
insert_var_order st (Elt.of_lit l)
)
(* A variable is not true/false anymore, one of two things can happen: *)
| Atom a ->
if a.var.v_level <= lvl then (
(* It is a late propagation, which has a level
lower than where we backtrack, so we just move it to the head
of the queue, to be propagated again. *)
Vec.set st.trail !head (Trail_elt.of_atom a);
head := !head + 1
) else (
(* it is a result of bolean propagation, or a semantic propagation
with a level higher than the level to which we backtrack,
in that case, we simply unset its value and reinsert it into the heap. *)
a.is_true <- false;
a.neg.is_true <- false;
a.var.v_level <- -1;
a.var.reason <- None;
insert_var_order st (Elt.of_var a.var)
)
if a.var.v_level <= lvl then (
(* It is a late propagation, which has a level
lower than where we backtrack, so we just move it to the head
of the queue, to be propagated again. *)
Vec.set st.trail !head a;
head := !head + 1
) else (
(* it is a result of bolean propagation, or a semantic propagation
with a level higher than the level to which we backtrack,
in that case, we simply unset its value and reinsert it into the heap. *)
a.is_true <- false;
a.neg.is_true <- false;
a.var.v_level <- -1;
a.var.reason <- None;
insert_var_order st a.var
)
done;
(* Recover the right theory state. *)
Plugin.backtrack (Vec.get st.th_levels lvl);
backtrack_down_to st (Vec.get st.backtrack_levels lvl);
(* Resize the vectors according to their new size. *)
Vec.shrink st.trail !head;
Vec.shrink st.elt_levels lvl;
Vec.shrink st.th_levels lvl;
Vec.shrink st.backtrack_levels lvl;
);
assert (Vec.size st.elt_levels = Vec.size st.th_levels);
assert (Vec.size st.elt_levels = Vec.size st.backtrack_levels);
()
(* Unsatisfiability is signaled through an exception, since it can happen
@ -527,36 +464,11 @@ module Make
a.is_true <- true;
a.var.v_level <- lvl;
a.var.reason <- Some reason;
Vec.push st.trail (Trail_elt.of_atom a);
Vec.push st.trail a;
Log.debugf debug
(fun k->k "Enqueue (%d): %a" (Vec.size st.trail) Atom.debug a);
()
let enqueue_semantic st a terms =
if not a.is_true then (
let l = List.map (Lit.make st.st) terms in
let lvl = List.fold_left (fun acc {l_level; _} ->
assert (l_level > 0); max acc l_level) 0 l in
H.grow_to_at_least st.order (St.nb_elt st.st);
enqueue_bool st a ~level:lvl Semantic
)
(* MCsat semantic assignment *)
let enqueue_assign st l value lvl =
match l.assigned with
| Some _ ->
Log.debugf error
(fun k -> k "Trying to assign an already assigned literal: %a" Lit.debug l);
assert false
| None ->
assert (l.l_level < 0);
l.assigned <- Some value;
l.l_level <- lvl;
Vec.push st.trail (Trail_elt.of_lit l);
Log.debugf debug
(fun k -> k "Enqueue (%d): %a" (Vec.size st.trail) Lit.debug l);
()
(* swap elements of array *)
let[@inline] swap_arr a i j =
if i<>j then (
@ -584,17 +496,6 @@ module Make
))
arr
(* evaluate an atom for MCsat, if it's not assigned
by boolean propagation/decision *)
let th_eval st a : bool option =
if a.is_true || a.neg.is_true then None
else match Plugin.eval a.lit with
| Plugin_intf.Unknown -> None
| Plugin_intf.Valued (b, l) ->
let atom = if b then a else a.neg in
enqueue_semantic st atom l;
Some b
(* find which level to backtrack to, given a conflict clause
and a boolean stating whether it is
a UIP ("Unique Implication Point")
@ -626,9 +527,7 @@ module Make
cr_is_uip: bool; (* conflict is UIP? *)
}
let get_atom st i =
match Vec.get st.trail i with
| Lit _ -> assert false | Atom x -> x
let[@inline] get_atom st i = Vec.get st.trail i
(* conflict analysis for SAT
Same idea as the mcsat analyze function (without semantic propagations),
@ -690,12 +589,8 @@ module Make
(* look for the next node to expand *)
while
let a = Vec.get st.trail !tr_ind in
Log.debugf debug (fun k -> k " looking at: %a" Trail_elt.debug a);
match a with
| Atom q ->
(not (Var.seen_both q.var)) ||
(q.var.v_level < conflict_level)
| Lit _ -> true
Log.debugf debug (fun k -> k " looking at: %a" St.Atom.debug a);
(not (Var.seen_both a.var)) || (a.var.v_level < conflict_level)
do
decr tr_ind;
done;
@ -792,7 +687,7 @@ module Make
Log.debugf debug (fun k -> k "Adding clause: @[<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 +804,7 @@ module Make
st.elt_head <- Vec.size st.trail;
raise (Conflict c)
) else (
match th_eval st first with
| None -> (* clause is unit, keep the same watches, but propagate *)
enqueue_bool st first ~level:(decision_level st) (Bcp c)
| Some true -> ()
| Some false ->
st.elt_head <- Vec.size st.trail;
raise (Conflict c)
enqueue_bool st first ~level:(decision_level st) (Bcp c)
);
Watch_kept
with Exit ->
@ -950,18 +839,14 @@ module Make
()
(* Propagation (boolean and theory) *)
let create_atom st f =
let a = mk_atom st f in
ignore (th_eval st a);
a
let[@inline] create_atom st f = mk_atom st f
let slice_get st i =
match Vec.get st.trail i with
| Atom a ->
Plugin_intf.Lit a.lit
| Lit {term; assigned = Some v; _} ->
Plugin_intf.Assign (term, v)
| Lit _ -> assert false
let slice_iter st (f:_ -> unit) : unit =
let n = Vec.size st.trail in
for i = st.th_head to n-1 do
let a = Vec.get st.trail i in
f a.lit
done
let slice_push st (l:formula list) (lemma:proof): unit =
let atoms = List.rev_map (create_atom st) l in
@ -969,45 +854,61 @@ module Make
Log.debugf info (fun k->k "Pushing clause %a" Clause.debug c);
Stack.push c st.clauses_to_add
let slice_propagate (st:t) f = function
| Plugin_intf.Eval l ->
let a = mk_atom st f in
enqueue_semantic st a l
| Plugin_intf.Consequence (causes, proof) ->
let l = List.rev_map (mk_atom st) causes in
if List.for_all (fun a -> a.is_true) l then (
let p = mk_atom st f in
let c = Clause.make (p :: List.map Atom.neg l) (Lemma proof) in
if p.is_true then ()
else if p.neg.is_true then (
Stack.push c st.clauses_to_add
) else (
H.grow_to_at_least st.order (St.nb_elt st.st);
insert_subterms_order st p.var;
enqueue_bool st p ~level:(decision_level st) (Bcp c)
)
let slice_propagate (st:t) f causes proof : unit =
let l = List.rev_map (mk_atom st) causes in
if List.for_all (fun a -> a.is_true) l then (
let p = mk_atom st f in
let c = Clause.make (p :: List.map Atom.neg l) (Lemma proof) in
if p.is_true then ()
else if p.neg.is_true then (
Stack.push c st.clauses_to_add
) else (
invalid_arg "Msat.Internal.slice_propagate"
H.grow_to_at_least st.order (St.nb_elt st.st);
insert_var_order st p.var;
enqueue_bool st p ~level:(decision_level st) (Bcp c)
)
) else (
invalid_arg "the solver.Internal.slice_propagate"
)
let current_slice st : (_,_,_) Plugin_intf.slice = {
Plugin_intf.start = st.th_head;
length = Vec.size st.trail - st.th_head;
get = slice_get st;
push = slice_push st;
propagate = slice_propagate st;
let slice_on_backtrack st f : unit =
Vec.push st.backtrack f
let slice_at_level_0 st () : bool =
Vec.is_empty st.backtrack_levels
let current_slice st = Theory_intf.Slice_acts {
slice_iter = slice_iter st;
slice_propagate = slice_propagate st;
}
(* full slice, for [if_sat] final check *)
let full_slice st : (_,_,_) Plugin_intf.slice = {
Plugin_intf.start = 0;
length = Vec.size st.trail;
get = slice_get st;
push = slice_push st;
propagate = (fun _ -> assert false);
let full_slice st = Theory_intf.Slice_acts {
slice_iter = slice_iter st;
slice_propagate = slice_propagate st;
}
(* some boolean literals were decided/propagated within Msat. Now we
let actions st = Theory_intf.Actions {
push = slice_push st;
on_backtrack = slice_on_backtrack st;
at_level_0 = slice_at_level_0 st;
}
let create ?(size=`Big) ?st () : t =
let st = match st with Some s -> s | None -> St.create ~size () in
let size_trail, size_lvl = match size with
| `Tiny -> 0, 0
| `Small -> 32, 16
| `Big -> 600, 50
in
let rec solver = lazy (
create_ ~st ~size_trail ~size_lvl th
) and th = lazy (
Th.create (actions (Lazy.force solver))
) in
Lazy.force solver
(* some boolean literals were decided/propagated within the solver. Now we
need to inform the theory of those assumptions, so it can do its job.
@return the conflict clause, if the theory detects unsatisfiability *)
let rec theory_propagate st : clause option =
@ -1018,14 +919,14 @@ module Make
) else (
let slice = current_slice st in
st.th_head <- st.elt_head; (* catch up *)
match Plugin.assume slice with
| Plugin_intf.Sat ->
match Th.assume (theory st) slice with
| Theory_intf.Sat ->
propagate st
| Plugin_intf.Unsat (l, p) ->
| Theory_intf.Unsat (l, p) ->
(* conflict *)
let l = List.rev_map (create_atom st) l in
H.grow_to_at_least st.order (St.nb_elt st.st);
List.iter (fun a -> insert_var_order st (Elt.of_var a.var)) l;
List.iter (fun a -> insert_var_order st a.var) l;
let c = St.Clause.make l (Lemma p) in
Some c
)
@ -1043,12 +944,9 @@ module Make
let num_props = ref 0 in
let res = ref None in
while st.elt_head < Vec.size st.trail do
begin match Vec.get st.trail st.elt_head with
| Lit _ -> ()
| Atom a ->
incr num_props;
propagate_atom st a res
end;
let a = Vec.get st.trail st.elt_head in
incr num_props;
propagate_atom st a res;
st.elt_head <- st.elt_head + 1;
done;
match !res with
@ -1067,14 +965,11 @@ module Make
if v.v_level >= 0 then (
assert (v.pa.is_true || v.na.is_true);
pick_branch_lit st
) else match Plugin.eval atom.lit with
| Plugin_intf.Unknown ->
new_decision_level st;
let current_level = decision_level st in
enqueue_bool st atom ~level:current_level Decision
| Plugin_intf.Valued (b, l) ->
let a = if b then atom else atom.neg in
enqueue_semantic st a l
) else (
new_decision_level st;
let current_level = decision_level st in
enqueue_bool st atom ~level:current_level Decision
)
and pick_branch_lit st =
match st.next_decision with
@ -1083,17 +978,7 @@ module Make
pick_branch_aux st atom
| None ->
begin match H.remove_min st.order with
| E_lit l ->
if Lit.level l >= 0 then
pick_branch_lit st
else (
let value = Plugin.assign l.term in
new_decision_level st;
let current_level = decision_level st in
enqueue_assign st l value current_level
)
| E_var v ->
pick_branch_aux st v.pa
| v -> pick_branch_aux st v.pa
| exception Not_found -> raise Sat
end
@ -1140,8 +1025,8 @@ module Make
else assert (var.v_level >= 0);
let truth = var.pa.is_true in
let value = match negated with
| Formula_intf.Negated -> not truth
| Formula_intf.Same_sign -> truth
| Theory_intf.Negated -> not truth
| Theory_intf.Same_sign -> truth
in
value, var.v_level
@ -1149,14 +1034,6 @@ module Make
let[@inline] unsat_conflict st = st.unsat_conflict
let model (st:t) : (term * term) list =
let opt = function Some a -> a | None -> assert false in
Vec.fold
(fun acc e -> match e with
| Lit v -> (v.term, opt v.assigned) :: acc
| Atom _ -> acc)
[] st.trail
(* fixpoint of propagation and decisions until a model is found, or a
conflict is reached *)
let solve (st:t) : unit =
@ -1174,9 +1051,9 @@ module Make
n_of_learnts := !n_of_learnts *. learntsize_inc
| Sat ->
assert (st.elt_head = Vec.size st.trail);
begin match Plugin.if_sat (full_slice st) with
| Plugin_intf.Sat -> ()
| Plugin_intf.Unsat (l, p) ->
begin match Th.if_sat (theory st) (full_slice st) with
| Theory_intf.Sat -> ()
| Theory_intf.Unsat (l, p) ->
let atoms = List.rev_map (create_atom st) l in
let c = Clause.make atoms (Lemma p) in
Log.debugf info (fun k -> k "Theory conflict clause: %a" Clause.debug c);
@ -1202,14 +1079,14 @@ module Make
cancel_until st (base_level st);
Log.debugf debug
(fun k -> k "@[<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);

40
src/core/Msat.ml
View file

@ -1,37 +1,57 @@
(** Main API *)
module Formula_intf = Formula_intf
module Plugin_intf = Plugin_intf
module Theory_intf = Theory_intf
module Expr_intf = Expr_intf
module Solver_types_intf = Solver_types_intf
module Config = Config
module Res = Res
module type S = Solver_intf.S
type ('term, 'form) sat_state = ('term, 'form) Solver_intf.sat_state = {
type negated = Theory_intf.negated =
| Negated
| Same_sign
type ('formula, 'proof) res = ('formula, 'proof) Theory_intf.res =
| Sat
(** The current set of assumptions is satisfiable. *)
| Unsat of 'formula list * 'proof
(** The current set of assumptions is *NOT* satisfiable, and here is a
theory tautology (with its proof), for which every litteral is false
under the current assumptions. *)
(** Type returned by the theory. Formulas in the unsat clause must come from the
current set of assumptions, i.e must have been encountered in a slice. *)
type 'form sat_state = 'form Solver_intf.sat_state = Sat_state of {
eval : 'form -> bool;
eval_level : 'form -> bool * int;
iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
model : unit -> ('term * 'term) list;
iter_trail : ('form -> unit) -> unit;
}
type ('clause, 'proof) unsat_state = ('clause, 'proof) Solver_intf.unsat_state = {
type ('clause, 'proof) unsat_state = ('clause, 'proof) Solver_intf.unsat_state = Unsat_state of {
unsat_conflict : unit -> 'clause;
get_proof : unit -> 'proof;
}
type 'clause export = 'clause Solver_intf.export = {
hyps : 'clause Vec.t;
history : 'clause Vec.t;
local : 'clause Vec.t;
}
module Make_smt_expr(E : Formula_intf.S) = Solver_types.SatMake(E)
module Make_mcsat_expr(E : Expr_intf.S) = Solver_types.McMake(E)
type ('form, 'proof) actions = ('form,'proof) Theory_intf.actions = Actions of {
push : 'form list -> 'proof -> unit;
on_backtrack: (unit -> unit) -> unit;
at_level_0 : unit -> bool;
}
module Make = Solver.Make
type ('form, 'proof) slice_actions = ('form, 'proof) Theory_intf.slice_actions = Slice_acts of {
slice_iter : ('form -> unit) -> unit;
slice_propagate : 'form -> 'form list -> 'proof -> unit;
}
module Make(E : Theory_intf.S) = Solver.Make(Solver_types.Make(E))(E)
(**/**)
module Vec = Vec

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

35
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 () : t = S.create ?size ()
(* Result type *)
type res =
| Sat of (St.term,St.formula) sat_state
| Sat of St.formula sat_state
| Unsat of (St.clause,Proof.proof) unsat_state
let pp_all st lvl status =
@ -44,26 +43,19 @@ module Make
"@[<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
Sat_state {
eval = S.eval st;
eval_level = S.eval_level st;
iter_trail = iter;
model = (fun () -> S.model st);
}
let mk_unsat (st:S.t) : (_,_) unsat_state =
@ -77,7 +69,7 @@ module Make
let c = unsat_conflict () in
S.Proof.prove_unsat c
in
{ unsat_conflict; get_proof; }
Unsat_state { unsat_conflict; get_proof; }
(* clean local state *)
let[@inline] cleanup_ (st:t) : unit =
@ -86,6 +78,8 @@ module Make
st.S.dirty <- false;
)
let theory = S.theory
(* Wrappers around internal functions*)
let[@inline] assume st ?tag cls : unit =
cleanup_ st;
@ -124,14 +118,12 @@ module Make
let get_tag cl = St.(cl.tag)
let[@inline] new_lit st t =
cleanup_ st;
S.new_lit st t
let[@inline] new_atom st a =
cleanup_ st;
S.new_atom st a
let actions = S.actions
let export (st:t) : St.clause export =
let hyps = S.hyps st in
let history = S.history st in
@ -150,5 +142,4 @@ module Make
end
module Formula = St.Formula
module Term = St.Term
end

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

37
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 = Sat_state of {
eval: 'form -> bool;
(** Returns the valuation of a formula in the current state
of the sat solver.
@ -22,15 +16,13 @@ type ('term, 'form) sat_state = {
the atom to have this value; otherwise it is due to choices
that can potentially be backtracked.
@raise UndecidedLit if the literal is not decided *)
iter_trail : ('form -> unit) -> ('term -> unit) -> unit;
(** Iter thorugh the formulas and terms in order of decision/propagation
iter_trail : ('form -> unit) -> unit;
(** Iter through the formulas and terms in order of decision/propagation
(starting from the first propagation, to the last propagation). *)
model: unit -> ('term * 'term) list;
(** Returns the model found if the formula is satisfiable. *)
}
(** The type of values returned when the solver reaches a SAT state. *)
type ('clause, 'proof) unsat_state = {
type ('clause, 'proof) unsat_state = Unsat_state of {
unsat_conflict : unit -> 'clause;
(** Returns the unsat clause found at the toplevel *)
get_proof : unit -> 'proof;
@ -54,12 +46,12 @@ module type S = sig
These are the internal modules used, you should probably not use them
if you're not familiar with the internals of mSAT. *)
type term (** user terms *)
type formula (** user formulas *)
type clause
type theory (** user theory *)
module Proof : Res.S with type clause = clause
(** A module to manipulate proofs. *)
@ -80,7 +72,7 @@ module type S = sig
(** Result type for the solver *)
type res =
| Sat of (term,formula) sat_state (** Returned when the solver reaches SAT, with a model *)
| Sat of formula sat_state (** Returned when the solver reaches SAT, with a model *)
| Unsat of (clause,Proof.proof) unsat_state (** Returned when the solver reaches UNSAT, with a proof *)
exception UndecidedLit
@ -89,6 +81,8 @@ module type S = sig
(** {2 Base operations} *)
val theory : t -> theory
val assume : t -> ?tag:int -> atom list list -> unit
(** Add the list of clauses to the current set of assumptions.
Modifies the sat solver state in place. *)
@ -102,11 +96,6 @@ module type S = sig
The assumptions are just used for this call to [solve], they are
not saved in the solver's state. *)
val new_lit : t -> term -> unit
(** Add a new litteral (i.e term) to the solver. This term will
be decided on at some point during solving, wether it appears
in clauses or not. *)
val new_atom : t -> atom -> unit
(** Add a new atom (i.e propositional formula) to the solver.
This formula will be decided on at some point during solving,
@ -132,6 +121,9 @@ module type S = sig
(** Return to last save point, discarding clauses added since last
call to [push] *)
val actions : t -> (formula,Proof.lemma) Theory_intf.actions
(** Obtain actions *)
val export : t -> clause export
(** {2 Re-export some functions} *)
@ -155,10 +147,5 @@ module type S = sig
type t = formula
val pp : t printer
end
module Term : sig
type t = term
val pp : t printer
end
end

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

87
src/core/Theory_intf.ml
View file

@ -23,24 +23,40 @@ Copyright 2016 Simon Cruanes
be used in an SMT solver.
*)
type ('formula, 'proof) res = ('formula, 'proof) Plugin_intf.res =
(** This type is used during the normalisation of formulas.
See {!val:Expr_intf.S.norm} for more details. *)
type negated =
| Negated (** changed sign *)
| Same_sign (** kept sign *)
(** Type returned by the theory. Formulas in the unsat clause must come from the
current set of assumptions, i.e must have been encountered in a slice. *)
type ('formula, 'proof) res =
| Sat
(** The current set of assumptions is satisfiable. *)
| Unsat of 'formula list * 'proof
(** The current set of assumptions is *NOT* satisfiable, and here is a
theory tautology (with its proof), for which every litteral is false
under the current assumptions. *)
(** Type returned by the theory. Formulas in the unsat clause must come from the
current set of assumptions, i.e must have been encountered in a slice. *)
type ('form, 'proof) slice = {
start : int; (** Start of the slice *)
length : int; (** Length of the slice *)
get : int -> 'form; (** Accesor for the formuals in the slice.
Should only be called on integers [i] s.t.
[start <= i < start + length] *)
push : 'form list -> 'proof -> unit; (** Allows to add to the solver a clause. *)
propagate : 'form -> 'form list -> 'proof -> unit;
(** Actions given to the theory during initialization, to be used
at any time *)
type ('form, 'proof) actions = Actions of {
push : 'form list -> 'proof -> unit;
(** Allows to add a clause to the solver. *)
on_backtrack: (unit -> unit) -> unit;
(** [on_backtrack f] calls [f] when the main solver backtracks *)
at_level_0 : unit -> bool;
(** Are we at level 0? *)
}
type ('form, 'proof) slice_actions = Slice_acts of {
slice_iter : ('form -> unit) -> unit;
(** iterate on the slice of the trail *)
slice_propagate : 'form -> 'form list -> 'proof -> unit;
(** [propagate lit causes proof] informs the solver to propagate [lit], with the reason
that the clause [causes => lit] is a theory tautology. It is faster than pushing
the associated clause but the clause will not be remembered by the sat solver,
@ -50,8 +66,10 @@ type ('form, 'proof) slice = {
propagation queue. They allow to look at the propagated literals,
and to add new clauses to the solver. *)
(** {2 Signature for theories to be given to the Solver.} *)
module type S = sig
(** Signature for theories to be given to the Solver. *)
type t
(** State of the theory *)
type formula
(** The type of formulas. Should be compatble with Formula_intf.S *)
@ -59,27 +77,44 @@ module type S = sig
type proof
(** A custom type for the proofs of lemmas produced by the theory. *)
type level
(** The type for levels to allow backtracking. *)
module Form : sig
type t = formula
(** The type of atomic formulas. *)
val dummy : level
(** A dummy level. *)
val equal : t -> t -> bool
(** Equality over formulas. *)
val current_level : unit -> level
(** Return the current level of the theory (either the empty/beginning state, or the
last level returned by the [assume] function). *)
val hash : t -> int
(** Hashing function for formulas. Should be such that two formulas equal according
to {!val:Expr_intf.S.equal} have the same hash. *)
val assume : (formula, proof) slice -> (formula, proof) res
val print : Format.formatter -> t -> unit
(** Printing function used among other thing for debugging. *)
val dummy : t
(** Formula constant. A valid formula should never be physically equal to [dummy] *)
val neg : t -> t
(** Formula negation. Should be an involution, i.e. [equal a (neg neg a)] should
always hold. *)
val norm : t -> t * negated
(** Returns a 'normalized' form of the formula, possibly negated
(in which case return [Negated]). This function is used to recognize
the link between a formula [a] and its negation [neg a], so the goal is
that [a] and [neg a] normalise to the same formula,
but one returns [Same_sign] and the other one returns [Negated] *)
end
val create : (formula, proof) actions -> t
(** Create a new instance of the theory *)
val assume : t -> (formula, proof) slice_actions -> (formula, proof) res
(** Assume the formulas in the slice, possibly pushing new formulas to be propagated,
and returns the result of the new assumptions. *)
val if_sat : (formula, proof) slice -> (formula, proof) res
val if_sat : t -> (formula, proof) slice_actions -> (formula, proof) res
(** Called at the end of the search in case a model has been found. If no new clause is
pushed, then 'sat' is returned, else search is resumed. *)
val backtrack : level -> unit
(** Backtrack to the given level. After a call to [backtrack l], the theory should be in the
same state as when it returned the value [l], *)
end

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

0
src/mcsat/README.md → src/main_test/README.md
View file

8
src/solver/jbuild → src/main_test/jbuild
View file

@ -1,10 +1,8 @@
; vim:ft=lisp:
(library
((name minismt)
(public_name minismt)
(libraries (msat dolmen))
(synopsis "minismt")
(executable
((name msat_test)
(libraries (msat msat.backend msat.tseitin msat.sat dolmen))
(flags (:standard -w +a-4-42-44-48-50-58-32-60@8 -color always -safe-string -open Msat))
(ocamlopt_flags (:standard -O3 -bin-annot
-unbox-closures -unbox-closures-factor 20))

50
src/main/main.ml → src/main_test/msat_test.ml
View file

@ -4,8 +4,6 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
open Msat
exception Incorrect_model
exception Out_of_time
exception Out_of_space
@ -28,7 +26,13 @@ end
module Make
(S : Msat.S)
(T : Minismt.Type.S with type atom := S.atom)
(Th : sig
include Msat.Theory_intf.S with type t = S.theory
end)
(T : sig
include Type.S with type atom := S.atom
val create : Th.t -> t
end)
: sig
val do_task : Dolmen.Statement.t -> unit
end = struct
@ -38,13 +42,15 @@ module Make
let hyps = ref []
let st = S.create ~size:`Big ()
let th = S.theory st
let t_st = T.create th
let check_model sat =
let check_model (Msat.Sat_state sat) =
let check_clause c =
let l = List.map (function a ->
Log.debugf 99
(fun k -> k "Checking value of %a" S.Formula.pp a);
sat.Msat.eval a) c in
sat.eval a) c in
List.exists (fun x -> x) l
in
let l = List.map check_clause !hyps in
@ -60,9 +66,9 @@ module Make
raise Incorrect_model;
let t' = Sys.time () -. t in
Format.printf "Sat (%f/%f)@." t t'
| S.Unsat state ->
| S.Unsat (Msat.Unsat_state us) ->
if !p_check then begin
let p = state.Msat.get_proof () in
let p = us.get_proof () in
S.Proof.check p;
if !p_dot_proof <> "" then begin
let fmt = Format.formatter_of_out_channel (open_out !p_dot_proof) in
@ -73,20 +79,20 @@ module Make
Format.printf "Unsat (%f/%f)@." t t'
end
let do_task s =
let do_task s : unit =
match s.Dolmen.Statement.descr with
| Dolmen.Statement.Def (id, t) -> T.def id t
| Dolmen.Statement.Decl (id, t) -> T.decl id t
| Dolmen.Statement.Def (id, t) -> T.def t_st id t
| Dolmen.Statement.Decl (id, t) -> T.decl t_st id t
| Dolmen.Statement.Clause l ->
let cnf = T.antecedent (Dolmen.Term.or_ l) in
let cnf = T.antecedent t_st (Dolmen.Term.or_ l) in
hyps := cnf @ !hyps;
S.assume st cnf
| Dolmen.Statement.Consequent t ->
let cnf = T.consequent t in
let cnf = T.consequent t_st t in
hyps := cnf @ !hyps;
S.assume st cnf
| Dolmen.Statement.Antecedent t ->
let cnf = T.antecedent t in
let cnf = T.antecedent t_st t in
hyps := cnf @ !hyps;
S.assume st cnf
| Dolmen.Statement.Pack [
@ -95,7 +101,7 @@ module Make
{ Dolmen.Statement.descr = Dolmen.Statement.Prove;_ };
{ Dolmen.Statement.descr = Dolmen.Statement.Pop 1;_ };
] ->
let assumptions = T.assumptions f in
let assumptions = T.assumptions t_st f in
prove ~assumptions ()
| Dolmen.Statement.Prove ->
prove ~assumptions:[] ()
@ -107,15 +113,17 @@ module Make
Dolmen.Statement.print s
end
module Sat = Make(Minismt_sat)(Minismt_sat.Type)
module Smt = Make(Minismt_smt)(Minismt_smt.Type)
module Mcsat = Make(Minismt_mcsat)(Minismt_smt.Type)
module Sat = Make(Msat_sat)(Msat_sat.Th)(Type_sat)
(*
module Smt = Make(Minismt_smt)(Msat_sat.Th)(Minismt_smt.Type)
*)
let solver = ref (module Sat : S)
let solver_list = [
"sat", (module Sat : S);
(* FIXME
"smt", (module Smt : S);
"mcsat", (module Mcsat : S);
*)
]
let error_msg opt arg l =
@ -228,8 +236,10 @@ let () =
| Incorrect_model ->
Format.printf "Internal error : incorrect *sat* model@.";
exit 4
| Minismt_sat.Type.Typing_error (msg, t)
| Minismt_smt.Type.Typing_error (msg, t) ->
(* FIXME
| Minismt_smt.Type.Typing_error (msg, t)
*)
| Type_sat.Typing_error (msg, t) ->
let b = Printexc.get_backtrace () in
let loc = match t.Dolmen.Term.loc with
| Some l -> l | None -> Dolmen.ParseLocation.mk "<>" 0 0 0 0

18
src/main_test/solver.ml Normal file
View file

@ -0,0 +1,18 @@
(**************************************************************************)
(* *)
(* Alt-Ergo Zero *)
(* *)
(* Sylvain Conchon and Alain Mebsout *)
(* Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
module type S = Msat.S
module Make (Th : Theory_intf.S) = Msat.Make(Th)

15
src/solver/solver.mli → src/main_test/solver.mli
View file

@ -14,17 +14,10 @@ Copyright 2014 Simon Cruanes
module type S = Msat.S
(** The interface of instantiated solvers. *)
module DummyTheory(F : Formula_intf.S) :
Theory_intf.S with type formula = F.t
and type proof = F.proof
(** Simple case where the theory is empty and
the proof type is the one given in the formula interface *)
module Make (F : Formula_intf.S)
(Th : Theory_intf.S with type formula = F.t
and type proof = F.proof)
: S with type formula = F.t
and type Proof.lemma = F.proof
module Make (Th : Theory_intf.S)
: S with type formula = Th.formula
and type Proof.lemma = Th.proof
and type theory = Th.t
(** Functor to create a SMT Solver parametrised by the atomic
formulas and a theory. *)

198
src/smt/expr_smt.ml → src/main_test/theory_smt.ml
View file

@ -499,10 +499,6 @@ module Atom = struct
else
mk_formula (Pred t)
let fresh () =
let id = Id.ty "fresh" Ty.prop in
pred (Term.of_id id)
let neg f =
{ f with sign = not f.sign }
@ -516,10 +512,198 @@ module Atom = struct
let norm f =
{ f with sign = true },
if f.sign then Formula_intf.Same_sign
else Formula_intf.Negated
if f.sign then Msat.Same_sign
else Msat.Negated
end
module Formula = Msat_tseitin.Make(Atom)
module Ts_arg = struct
module Form = Atom
type t = unit
let fresh () : Form.t =
let id = Id.ty "fresh" Ty.prop in
Form.pred (Term.of_id id)
end
module Formula = Msat_tseitin.Make(Ts_arg)
(** {2 Theory} *)
module E = Eclosure.Make(Term)
module H = Backtrack.Hashtbl(Term)
module M = Hashtbl.Make(Term)
let uf acts = E.create acts
let assign t =
match E.find_tag uf t with
| _, None -> t
| _, Some (_, v) -> v
(* Propositional constants *)
let true_ = Theory_smt.(Term.of_id (Id.ty "true" Ty.prop))
let false_ = Theory_smt.(Term.of_id (Id.ty "false" Ty.prop))
(* Uninterpreted functions and predicates *)
let map : Theory_smt.term H.t = H.create stack
let watch = M.create 4096
let interpretation = H.create stack
let pop_watches t =
try
let l = M.find watch t in
M.remove watch t;
l
with Not_found ->
[]
let add_job j x =
let l = try M.find watch x with Not_found -> [] in
M.add watch x (j :: l)
let update_job x ((t, watchees) as job) =
try
let y = List.find (fun y -> not (H.mem map y)) watchees in
add_job job y
with Not_found ->
add_job job x;
begin match t with
| { Theory_smt.term = Theory_smt.App (f, tys, l);_ } ->
let is_prop = Theory_smt.(Ty.equal t.t_type Ty.prop) in
let t_v = H.find map t in
let l' = List.map (H.find map) l in
let u = Theory_smt.Term.apply f tys l' in
begin try
let t', u_v = H.find interpretation u in
if not (Theory_smt.Term.equal t_v u_v) then begin
match t' with
| { Theory_smt.term = Theory_smt.App (_, _, r); _ } when is_prop ->
let eqs = List.map2 (fun a b -> Theory_smt.Atom.neg (Theory_smt.Atom.eq a b)) l r in
if Theory_smt.(Term.equal u_v true_) then begin
let res = Theory_smt.Atom.pred t ::
Theory_smt.Atom.neg (Theory_smt.Atom.pred t') :: eqs in
raise (Absurd res)
end else begin
let res = Theory_smt.Atom.pred t' ::
Theory_smt.Atom.neg (Theory_smt.Atom.pred t) :: eqs in
raise (Absurd res)
end
| { Theory_smt.term = Theory_smt.App (_, _, r); _ } ->
let eqs = List.map2 (fun a b -> Theory_smt.Atom.neg (Theory_smt.Atom.eq a b)) l r in
let res = Theory_smt.Atom.eq t t' :: eqs in
raise (Absurd res)
| _ -> assert false
end
with Not_found ->
H.add interpretation u (t, t_v);
end
| _ -> assert false
end
let rec update_watches x = function
| [] -> ()
| job :: r ->
begin
try
update_job x job;
with exn ->
List.iter (fun j -> add_job j x) r;
raise exn
end;
update_watches x r
let add_watch t l =
update_job t (t, l)
let add_assign t v =
H.add map t v;
update_watches t (pop_watches t)
(* Assignemnts *)
let rec iter_aux f = function
| { Theory_smt.term = Theory_smt.Var _; _ } as t ->
Log.debugf 10 (fun k -> k "Adding %a as assignable" Theory_smt.Term.print t);
f t
| { Theory_smt.term = Theory_smt.App (_, _, l); _ } as t ->
if l <> [] then add_watch t (t :: l);
List.iter (iter_aux f) l;
Log.debugf 10 (fun k -> k "Adding %a as assignable" Theory_smt.Term.print t);
f t
let iter_assignable f = function
| { Theory_smt.atom = Theory_smt.Pred { Theory_smt.term = Theory_smt.Var _;_ }; _ } -> ()
| { Theory_smt.atom = Theory_smt.Pred ({ Theory_smt.term = Theory_smt.App (_, _, l);_} as t); _ } ->
if l <> [] then add_watch t (t :: l);
List.iter (iter_aux f) l;
| { Theory_smt.atom = Theory_smt.Equal (a, b);_ } ->
iter_aux f a; iter_aux f b
let eval = function
| { Theory_smt.atom = Theory_smt.Pred t; _ } ->
begin try
let v = H.find map t in
if Theory_smt.Term.equal v true_ then
Plugin_intf.Valued (true, [t])
else if Theory_smt.Term.equal v false_ then
Plugin_intf.Valued (false, [t])
else
Plugin_intf.Unknown
with Not_found ->
Plugin_intf.Unknown
end
| { Theory_smt.atom = Theory_smt.Equal (a, b); sign; _ } ->
begin try
let v_a = H.find map a in
let v_b = H.find map b in
if Theory_smt.Term.equal v_a v_b then
Plugin_intf.Valued(sign, [a; b])
else
Plugin_intf.Valued(not sign, [a; b])
with Not_found ->
Plugin_intf.Unknown
end
(* Theory propagation *)
let rec chain_eq = function
| [] | [_] -> []
| a :: ((b :: _) as l) -> (Theory_smt.Atom.eq a b) :: chain_eq l
let assume s =
let open Plugin_intf in
try
for i = s.start to s.start + s.length - 1 do
match s.get i with
| Assign (t, v) ->
add_assign t v;
E.add_tag uf t v
| Lit f ->
begin match f with
| { Theory_smt.atom = Theory_smt.Equal (u, v); sign = true;_ } ->
E.add_eq uf u v
| { Theory_smt.atom = Theory_smt.Equal (u, v); sign = false;_ } ->
E.add_neq uf u v
| { Theory_smt.atom = Theory_smt.Pred p; sign;_ } ->
let v = if sign then true_ else false_ in
add_assign p v
end
done;
Plugin_intf.Sat
with
| Absurd l ->
Plugin_intf.Unsat (l, ())
| E.Unsat (a, b, l) ->
let c = Theory_smt.Atom.eq a b :: List.map Theory_smt.Atom.neg (chain_eq l) in
Plugin_intf.Unsat (c, ())
let if_sat _ =
Plugin_intf.Sat

5
src/smt/expr_smt.mli → src/main_test/theory_smt.mli
View file

@ -304,9 +304,6 @@ module Atom : sig
val dummy : atom
(** A dummy atom, different from any other atom. *)
val fresh : unit -> atom
(** Create a fresh propositional atom. *)
val eq : term -> term -> atom
(** Create an equality over two terms. The two given terms
must have the same type [t], which must be different from {!Ty.prop} *)
@ -317,7 +314,7 @@ module Atom : sig
val neg : atom -> atom
(** Returns the negation of the given atom *)
val norm : atom -> atom * Formula_intf.negated
val norm : atom -> atom * Msat.negated
(** Normalization functions as required by msat. *)
end

11
src/solver/type.ml → src/main_test/type.ml
View file

@ -3,6 +3,7 @@
This module defines the requirements for typing expre'ssions from dolmen. *)
module type S = sig
type t
type atom
(** The type of atoms that will be fed to tha sovler. *)
@ -10,17 +11,17 @@ module type S = sig
exception Typing_error of string * Dolmen.Term.t
(** Exception raised during typechecking. *)
val decl : Dolmen.Id.t -> Dolmen.Term.t -> unit
val decl : t -> Dolmen.Id.t -> Dolmen.Term.t -> unit
(** New declaration, i.e an identifier and its type. *)
val def : Dolmen.Id.t -> Dolmen.Term.t -> unit
val def : t -> Dolmen.Id.t -> Dolmen.Term.t -> unit
(** New definition, i.e an identifier and the term it is equal to. *)
val assumptions : Dolmen.Term.t -> atom list
val assumptions : t -> Dolmen.Term.t -> atom list
(** Parse a list of local assumptions. *)
val consequent : Dolmen.Term.t -> atom list list
val antecedent : Dolmen.Term.t -> atom list list
val consequent : t -> Dolmen.Term.t -> atom list list
val antecedent : t -> Dolmen.Term.t -> atom list list
(** Parse a formula, and return a cnf ready to be given to the solver.
Consequent is for hypotheses (left of the sequent), while antecedent
is for goals (i.e formulas on the right of a sequent). *)

60
src/sat/type_sat.ml → src/main_test/type_sat.ml
View file

@ -10,7 +10,7 @@ Copyright 2014 Simon Cruanes
module Id = Dolmen.Id
module Ast = Dolmen.Term
module H = Hashtbl.Make(Id)
module Formula = Msat_tseitin.Make(Expr_sat)
module Formula = Msat_tseitin.Make(Msat_sat.Th)
(* Exceptions *)
(* ************************************************************************ *)
@ -20,14 +20,24 @@ exception Typing_error of string * Dolmen.Term.t
(* Identifiers *)
(* ************************************************************************ *)
let symbols = H.create 42
type t = {
symbols: Formula.atom H.t;
fresh: Formula.fresh_state;
st: Formula.state;
}
let find_id id =
let create th : t = {
symbols = H.create 42;
fresh=th;
st=Formula.create th;
}
let find_id st id =
try
H.find symbols id
H.find st.symbols id
with Not_found ->
let res = Expr_sat.fresh () in
H.add symbols id res;
let res = Msat_sat.Th.fresh st.fresh in
H.add st.symbols id res;
res
(* Actual parsing *)
@ -35,29 +45,29 @@ let find_id id =
[@@@ocaml.warning "-9"]
let rec parse = function
let rec parse st = function
| { Ast.term = Ast.Builtin Ast.True } ->
Formula.f_true
| { Ast.term = Ast.Builtin Ast.False } ->
Formula.f_false
| { Ast.term = Ast.Symbol id } ->
let s = find_id id in
let s = find_id st id in
Formula.make_atom s
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Not }, [p]) }
| { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "not" } }, [p]) } ->
Formula.make_not (parse p)
Formula.make_not (parse st p)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.And }, l) }
| { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "and" } }, l) } ->
Formula.make_and (List.map parse l)
Formula.make_and (List.map (parse st) l)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Or }, l) }
| { Ast.term = Ast.App ({Ast.term = Ast.Symbol { Id.name = "or" } }, l) } ->
Formula.make_or (List.map parse l)
Formula.make_or (List.map (parse st) l)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Imply }, [p; q]) } ->
Formula.make_imply (parse p) (parse q)
Formula.make_imply (parse st p) (parse st q)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Equiv }, [p; q]) } ->
Formula.make_equiv (parse p) (parse q)
Formula.make_equiv (parse st p) (parse st q)
| { Ast.term = Ast.App ({Ast.term = Ast.Builtin Ast.Xor }, [p; q]) } ->
Formula.make_xor (parse p) (parse q)
Formula.make_xor (parse st p) (parse st q)
| t ->
raise (Typing_error ("Term is not a pure proposition", t))
@ -66,25 +76,25 @@ let rec parse = function
(* Exported functions *)
(* ************************************************************************ *)
let decl _ t =
let decl _ _ t =
raise (Typing_error ("Declarations are not allowed in pure sat", t))
let def _ t =
let def _ _ t =
raise (Typing_error ("Definitions are not allowed in pure sat", t))
let assumptions t =
let f = parse t in
let cnf = Formula.make_cnf f in
let assumptions st t =
let f = parse st t in
let cnf = Formula.make_cnf st.st f in
List.map (function
| [ x ] -> x
| _ -> assert false
) cnf
let antecedent t =
let f = parse t in
Formula.make_cnf f
let antecedent st t =
let f = parse st t in
Formula.make_cnf st.st f
let consequent t =
let f = parse t in
Formula.make_cnf @@ Formula.make_not f
let consequent st t =
let f = parse st t in
Formula.make_cnf st.st @@ Formula.make_not f

4
src/sat/type_sat.mli → src/main_test/type_sat.mli
View file

@ -8,5 +8,7 @@ Copyright 2014 Simon Cruanes
This module provides functions to parse terms from the untyped syntax tree
defined in Dolmen, and generate formulas as defined in the Expr_sat module. *)
include Minismt.Type.S with type atom := Expr_sat.t
include Type.S with type atom := Msat_sat.Th.formula
val create : Msat_sat.Th.t -> t

0
src/smt/unionfind.ml → src/main_test/unionfind.ml
View file

0
src/smt/unionfind.mli → src/main_test/unionfind.mli
View file

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

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

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

@ -0,0 +1,87 @@
exception Bad_atom
(** Exception raised if an atom cannot be created *)
type proof = unit
(** A empty type for proofs *)
type formula = int
type t = {
actions: (formula, proof) Msat.actions;
mutable max_index: int;
mutable max_fresh: int;
}
let create actions : t = {
actions;
max_index = 0;
max_fresh= (-1);
}
module Form = struct
type t = formula
(** Atoms are represented as integers. [-i] begin the negation of [i].
Additionally, since we nee dot be able to create fresh atoms, we
use even integers for user-created atoms, and odd integers for the
fresh atoms. *)
let max_lit = max_int
let hash (a:int) = a land max_int
let equal (a:int) b = a=b
let compare (a:int) b = Pervasives.compare a b
(** Internal function for creating atoms.
Updates the internal counters *)
let make_ st i =
if i <> 0 && (abs i) < max_lit then (
st.max_index <- max st.max_index (abs i);
i
) else (
raise Bad_atom
)
(** A dummy atom *)
let dummy = 0
let neg a = - a
let norm a =
abs a, if a < 0 then
Msat.Negated
else
Msat.Same_sign
let print fmt a =
Format.fprintf fmt "%s%s%d"
(if a < 0 then "~" else "")
(if a mod 2 = 0 then "v" else "f")
((abs a) / 2)
end
let abs = abs
let sign i = i > 0
let apply_sign b i = if b then i else Form.neg i
let set_sign b i = if b then abs i else Form.neg (abs i)
let make st i = Form.make_ st (2 * i)
let fresh st =
st.max_fresh <- 1 + st.max_fresh;
Form.make_ st (2 * st.max_fresh + 1)
(*
let iter: (t -> unit) -> unit = fun f ->
for j = 1 to !max_index do
f j
done
*)
let assume _ _ = Msat.Theory_intf.Sat
let if_sat _ _ = Msat.Theory_intf.Sat

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

@ -4,28 +4,28 @@
(** SAT Formulas
This modules implements formuals adequate for use in a pure SAT Solver.
Atomic formuals are represented using integers, that should allow
Atomic formulas are represented using integers, that should allow
near optimal efficiency (both in terms of space and time).
*)
include Formula_intf.S
open Msat
include Theory_intf.S with type formula = int and type proof = unit
(** This modules implements the requirements for implementing an SAT Solver. *)
val make : int -> t
val make : t -> int -> formula
(** Make a proposition from an integer. *)
val fresh : unit -> t
val fresh : t -> formula
(** Make a fresh atom *)
val compare : t -> t -> int
(** Compare atoms *)
val sign : t -> bool
val sign : formula -> bool
(** Is the given atom positive ? *)
val apply_sign : bool -> t -> t
val apply_sign : bool -> formula -> formula
(** [apply_sign b] is the identity if [b] is [true], and the negation
function if [b] is [false]. *)
val set_sign : bool -> t -> t
val set_sign : bool -> formula -> formula
(** Return the atom with the sign set. *)

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

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

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

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

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,20 +42,20 @@ exception Incorrect_model
module type BASIC_SOLVER = sig
type t
val create : unit -> t
val solve : t -> ?assumptions:F.t list -> unit -> solver_res
val assume : t -> ?tag:int -> F.t list list -> unit
val solve : t -> ?assumptions:F.atom list -> unit -> solver_res
val assume : t -> ?tag:int -> F.atom list list -> unit
end
let mk_solver (): (module BASIC_SOLVER) =
let module S = struct
include Minismt_sat
include Msat_sat
let create() = create()
let solve st ?assumptions () =
match solve st ?assumptions() with
| Sat _ ->
R_sat
| Unsat us ->
let p = us.Msat.get_proof () in
| Unsat (Unsat_state us) ->
let p = us.get_proof () in
Proof.check p;
R_unsat
end
@ -68,8 +68,8 @@ let errorf msg = Format.ksprintf error msg
module Test = struct
type action =
| A_assume of F.t list list
| A_solve of F.t list * [`Expect_sat | `Expect_unsat]
| A_assume of F.atom list list
| A_solve of F.atom list * [`Expect_sat | `Expect_unsat]
type t = {
name: string;
@ -77,11 +77,9 @@ module Test = struct
}
let mk_test name l = {name; actions=l}
let assume l = A_assume (List.map (List.map F.make) l)
let assume l = A_assume l
let assume1 c = assume [c]
let solve ?(assumptions=[]) e =
let assumptions = List.map F.make assumptions in
A_solve (assumptions, e)
let solve ?(assumptions=[]) e = A_solve (assumptions, e)
type result =
| Pass