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

wip: make SMT great again

Browse source
This commit is contained in:
Simon Cruanes 2016-08-16 17:20:48 +02:00
parent 7d57b3f1b5
commit 41557a1509
42 changed files with 1968 additions and 198 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
.merlin
View file

@ -1,6 +1,7 @@
S src/core
S src/solver
S src/example
S src/sat
S src/smt
S src/backend
S src/util
S src/util/smtlib
@ -9,7 +10,8 @@ S tests
B _build/src/
B _build/src/core
B _build/src/solver
B _build/src/example
B _build/src/sat
B _build/src/smt
B _build/src/util
B _build/src/util/smtlib
B _build/src/backend

23
META
View file

@ -1,3 +1,4 @@
# meta
name="msat"
version="dev"
description="MSAT is a modular SAT solver, plus extensions"
@ -6,3 +7,25 @@ archive(byte) = "msat.cma"
archive(byte, plugin) = "msat.cma"
archive(native) = "msat.cmxa"
archive(native, plugin) = "msat.cmxs"
package "sat" (
version = "dev"
description = "SAT solver instance"
requires = "msat"
archive(byte) = "msat_sat.cma"
archive(byte, plugin) = "msat_sat.cma"
archive(native) = "msat_sat.cmxa"
archive(native, plugin) = "msat_sat.cmxs"
exists_if = "msat_sat.cma"
)
package "smt" (
version = "dev"
description = "SMT solver instance"
requires = "msat"
archive(byte) = "msat_smt.cma"
archive(byte, plugin) = "msat_smt.cma"
archive(native) = "msat_smt.cmxa"
archive(native, plugin) = "msat_smt.cmxs"
exists_if = "msat_smt.cma"
)

36
Makefile
View file

@ -3,12 +3,20 @@
LOG=build.log
COMP=ocamlbuild -log $(LOG) -use-ocamlfind
FLAGS=
DOC=msat.docdir/index.html
DOC=msat.docdir/index.html msat_smt.docdir/index.html
BIN=main.native
TEST_BIN=tests/test_api.native
NAME=msat
LIB=$(addprefix $(NAME), .cma .cmxa .cmxs)
NAME_OCAMLFIND=msat
NAME_BIN=msat
NAME_CORE=msat
NAME_SAT=msat_sat
NAME_SMT=msat_smt
LIB_CORE=$(addprefix $(NAME_CORE), .cma .cmxa .cmxs)
LIB_SAT=$(addprefix $(NAME_SAT), .cma .cmxa .cmxs)
LIB_SMT=$(addprefix $(NAME_SMT), .cma .cmxa .cmxs)
LIB=$(LIB_CORE) $(LIB_SAT) $(LIB_SMT)
all: lib test
@ -20,7 +28,7 @@ doc:
bin:
$(COMP) $(FLAGS) $(BIN)
cp $(BIN) $(NAME) && rm $(BIN)
cp $(BIN) $(NAME_BIN) && rm $(BIN)
test_bin:
$(COMP) $(FLAGS) $(TEST_BIN)
@ -44,16 +52,26 @@ log:
clean:
$(COMP) -clean
TO_INSTALL=META $(addprefix _build/src/,$(LIB) $(NAME).a $(NAME).cmi)
ALL_NAMES = $(NAME_CORE) $(NAME_SAT) $(NAME_SMT)
TO_INSTALL_LIB=$(addsuffix .a, $(ALL_NAMES)) \
$(addsuffix .cmi, $(ALL_NAMES))
TO_INSTALL=META $(addprefix _build/src/,$(LIB) $(TO_INSTALL_LIB))
install: lib
ocamlfind install msat $(TO_INSTALL)
ocamlfind install $(NAME_OCAMLFIND) $(TO_INSTALL)
uninstall:
ocamlfind remove msat
ocamlfind remove $(NAME_OCAMLFIND)
reinstall: all
ocamlfind remove msat || true
ocamlfind install msat $(TO_INSTALL)
ocamlfind remove $(NAME_OCAMLFIND) || true
ocamlfind install $(NAME_OCAMLFIND) $(TO_INSTALL)
watch:
while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \
echo "============ at `date` ==========" ; \
sleep 0.1; \
make all; \
done
.PHONY: clean doc all bench install uninstall reinstall enable_log disable_log bin test

6
_tags
View file

@ -9,7 +9,8 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
<src/core>: include
<src/solver>: include
<src/backend>: include
<src/example>: include
<src/smt>: include
<src/sat>: include
<src/util>: include
<src/util/smtlib>: include
@ -18,7 +19,8 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
<src/solver/*.cmx>: for-pack(Msat)
<src/backend/*.cmx>: for-pack(Msat)
<src/util/*.cmx>: for-pack(Msat)
<src/example/*.cmx>: for-pack(Msat)
<src/sat/*.cmx>: for-pack(Msat_sat)
<src/smt/*.cmx>: for-pack(Msat_smt)
# more warnings
<src/**/*.ml>: warn_K, warn_Y, warn_X

99
src/example/cc.ml
View file

@ -1,99 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module Make(T : Sig.OrderedType) = struct
module M = Map.Make(T)
module U = Unionfind.Make(T)
exception Unsat of (T.t * T.t * (T.t list))
type t = {
repr : U.t;
expl : T.t M.t;
size : int M.t;
}
let empty = {
repr = U.empty;
expl = M.empty;
size = M.empty;
}
let repr t a = U.find t.repr a
let map_find m v default = try M.find v m with Not_found -> default
let find_parent v m = map_find m v v
let rev_root m root =
let rec aux m curr next =
if T.compare curr next = 0 then
m, curr
else
let parent = find_parent next m in
let m' = M.add next curr (M.remove curr m) in
aux m' next parent
in
aux m root (find_parent root m)
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 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 (U.find t.repr i) (U.find t.repr j) = 0 then
t
else
let m, old_root_i = rev_root t.expl i in
let m, old_root_j = rev_root m j in
let nb_i = map_find t.size old_root_i 0 in
let nb_j = map_find t.size old_root_j 0 in
if nb_i < nb_j then {
repr = t.repr;
expl = M.add i j m;
size = M.add j (nb_i + nb_j + 1) t.size; }
else {
repr = t.repr;
expl = M.add j i m;
size = M.add i (nb_i + nb_j + 1) t.size; }
let add_eq t i j =
let t' = add_eq_aux t i j in
try
let u' = U.union t.repr i j in
{ t' with repr = u' }
with U.Unsat (a, b) ->
raise (Unsat (a, b, expl t' a b))
let add_neq t i j =
try
let u' = U.forbid t.repr i j in
{ t with repr = u' }
with U.Unsat (a, b) ->
raise (Unsat (a, b, expl t a b))
let are_neq t a b =
try
ignore (U.union t.repr a b);
false
with U.Unsat _ ->
true
end

18
src/example/cc.mli
View file

@ -1,18 +0,0 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module Make(T : Sig.OrderedType) : sig
type t
exception Unsat of (T.t * T.t * (T.t list))
val empty : t
val add_eq : t -> T.t -> T.t -> t
val add_neq : t -> T.t -> T.t -> t
val repr : t -> T.t -> T.t
val are_neq : t -> T.t -> T.t -> bool
end

13
src/example/sig.mli
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 type OrderedType = sig
(** Signature for ordered types (mainly for use in Map.Make) *)
type t
val compare : t -> t -> int
end

9
src/main.ml
View file

@ -5,9 +5,10 @@ Copyright 2014 Simon Cruanes
*)
module F = Expr
module T = Cnf.S
module Smt = Smt.Make(struct end)
module Mcsat = Mcsat.Make(struct end)
module T = Msat_smt.Cnf.S
module Sat = Msat_sat.Sat.Make(struct end)
module Smt = Msat_smt.Smt.Make(struct end)
module Mcsat = Msat_smt.Mcsat.Make(struct end)
exception Incorrect_model
exception Out_of_time
@ -26,6 +27,7 @@ type sat_output =
| Dot
type solver =
| Sat
| Smt
| Mcsat
@ -43,6 +45,7 @@ let output_list = [
"dk", Dedukti;
]
let solver_list = [
"sat", Sat;
"smt", Smt;
"mcsat", Mcsat;
]

13
src/msat.mlpack
View file

@ -19,20 +19,11 @@ Mcsolver
Solver_types
# Backends
Backend_intf
Dot
Dedukti
# Auxiliary modules
Res
Tseitin
# Sat/Smt modules
Expr
Cnf
Sat
Mcsat
Cc
Sig
Smt
Unionfind
Hashcons

8
src/msat.odocl
View file

@ -13,6 +13,7 @@ solver/Tseitin_intf
# Main modules
core/Res
core/Res_intf
core/Internal
core/External
core/Solver_types
@ -20,13 +21,12 @@ core/Solver_types
solver/Solver
solver/Mcsolver
solver/Tseitin
solver/Tseitin_intf
# Backends
backend/Dot
backend/Dedukti
backend/Backend_intf
# Examples
example/Sat
example/Smt
# Auxiliary
util/Hashcons

2
src/msat_sat.mlpack Normal file
View file

@ -0,0 +1,2 @@
Sat

3
src/msat_sat.odocl Normal file
View file

@ -0,0 +1,3 @@
smt/Sat

12
src/msat_smt.mlpack Normal file
View file

@ -0,0 +1,12 @@
Cc
Cnf
Explanation
Expr
ID
Literal
Mcsat
Smt
Symbols
Term
Ty
Unionfind

17
src/msat_smt.odocl Normal file
View file

@ -0,0 +1,17 @@
smt/Smt
# support
smt/Cc
smt/Cnf
smt/Explanation
smt/Expr
smt/ID
smt/Sat
smt/Literal
smt/Mcsat
smt/Symbols
smt/Term
smt/Ty
smt/Unionfind

2
src/example/sat.ml → src/sat/sat.ml
View file

@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
open Msat
module FI = Formula_intf
module Fsat = struct

2
src/example/sat.mli → src/sat/sat.mli
View file

@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
open Msat
module Fsat : sig
include Formula_intf.S with type t = private int

39
src/smt/ID.ml Normal file
View file

@ -0,0 +1,39 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes
*)
type t = {
id: int;
name: string;
}
let make =
let n = ref 0 in
fun name ->
let x = { id= !n; name; } in
incr n;
x
let copy {name;_} = make name
let to_string id = id.name
let equal a b = a.id=b.id
let compare a b = Pervasives.compare a.id b.id
let hash a = a.id land max_int
let pp out a = Format.fprintf out "%s/%d" a.name a.id
let pp_name out a = Format.pp_print_string out a.name
module AsKey = struct
type t_ = t
type t = t_
let equal = equal
let compare = compare
let hash = hash
end
module Map = Map.Make(AsKey)
module Set = Set.Make(AsKey)
module Tbl = Hashtbl.Make(AsKey)

25
src/smt/ID.mli Normal file
View file

@ -0,0 +1,25 @@
(*
MSAT is free software, using the Apache license, see file LICENSE
Copyright 2016 Guillaume Bury
Copyright 2016 Simon Cruanes
*)
(** {1 Unique Identifiers} *)
type t
val make : string -> t
val copy : t -> t
val to_string : t -> string
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pp_name : Format.formatter -> t -> unit
module Map : Map.S with type key = t
module Set : Set.S with type elt = t
module Tbl : Hashtbl.S with type key = t

517
src/smt/cc.ml Normal file
View file

@ -0,0 +1,517 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
open Msat
let max_split = 1000000
let cc_active = ref true
type answer = Yes of Explanation.t | No
module type S = sig
type t
val empty : unit -> t
val assume : cs:bool ->
Literal.LT.t -> Explanation.t -> t -> t * Term.Set.t * int
val query : Literal.LT.t -> t -> answer
val class_of : t -> Term.t -> Term.t list
end
module Make (Dummy : sig end) = struct
module Ex = Explanation
module Uf = Uf.Make(Term)
module T = Term
module A = Literal
module LR = A.Make(struct type t = X.r include X end)
module SetT = Term.Set
module S = Symbols
module SetX = Set.Make(struct type t = X.r let compare = X.compare end)
(* module Uf = Pptarjan.Uf *)
type env = {
uf : Uf.t ;
relation : X.Rel.t
}
type choice_sign =
| CPos of int (* The explication of this choice *)
| CNeg (* The choice has been already negated *)
type t = {
gamma : env;
gamma_finite : env ;
choices : (X.r A.view * Num.num * choice_sign * Ex.t) list;
(** the choice, the size, choice_sign, the explication set,
the explication for this choice. *)
}
module Print = struct
let begin_case_split () = ()
let end_case_split () = ()
let cc r1 r2 = ()
let make_cst t ctx = ()
let add_to_use t = ()
let lrepr fmt = List.iter (Format.fprintf fmt "%a " X.print)
let leaves t lvs = ()
let contra_congruence a ex = ()
let split_size sz = ()
let split_backtrack neg_c ex_c = ()
let split_assume c ex_c = ()
let split_backjump c dep = ()
let assume_literal sa = ()
let congruent a ex = ()
let query a = ()
end
let bottom = Hstring.make "@bottom"
let one, _ = X.make (Term.make (S.name bottom) [] Ty.Tint)
let concat_leaves uf l =
let rec concat_rec acc t =
match X.leaves (fst (Uf.find uf t)) , acc with
[] , _ -> one::acc
| res, [] -> res
| res , _ -> List.rev_append res acc
in
match List.fold_left concat_rec [] l with
[] -> [one]
| res -> res
let are_equal env ex t1 t2 =
if T.equal t1 t2 then ex
else match Uf.are_equal env.uf t1 t2 with
| Yes dep -> Ex.union ex dep
| No -> raise Exit
let equal_only_by_congruence env ex t1 t2 acc =
if T.equal t1 t2 then acc
else
let {T.f=f1; xs=xs1; ty=ty1} = T.view t1 in
if X.fully_interpreted f1 then acc
else
let {T.f=f2; xs=xs2; ty=ty2} = T.view t2 in
if Symbols.equal f1 f2 && Ty.equal ty1 ty2 then
try
let ex = List.fold_left2 (are_equal env) ex xs1 xs2 in
let a = A.LT.make (A.Eq(t1, t2)) in
Print.congruent a ex;
(LTerm a, ex) :: acc
with Exit -> acc
else acc
let congruents env t1 s acc ex =
SetT.fold (equal_only_by_congruence env ex t1) s acc
let fold_find_with_explanation find ex l =
List.fold_left
(fun (lr, ex) t -> let r, ex_r = find t in r::lr, Ex.union ex_r ex)
([], ex) l
let view find va ex_a =
match va with
| A.Eq (t1, t2) ->
let r1, ex1 = find t1 in
let r2, ex2 = find t2 in
let ex = Ex.union (Ex.union ex1 ex2) ex_a in
A.Eq(r1, r2), ex
| A.Distinct (b, lt) ->
let lr, ex = fold_find_with_explanation find ex_a lt in
A.Distinct (b, lr), ex
| A.Builtin(b, s, l) ->
let lr, ex = fold_find_with_explanation find ex_a l in
A.Builtin(b, s, List.rev lr), ex
let term_canonical_view env a ex_a =
view (Uf.find env.uf) (A.LT.view a) ex_a
let canonical_view env a ex_a = view (Uf.find_r env.uf) a ex_a
let new_facts_by_contra_congruence env r bol ex =
match X.term_extract r with
| None -> []
| Some t1 ->
match T.view t1 with
| {T.f=f1 ; xs=[x]} ->
List.fold_left
(fun acc t2 ->
match T.view t2 with
| {T.f=f2 ; xs=[y]} when S.equal f1 f2 ->
let a = A.LT.make (A.Distinct (false, [x; y])) in
let dist = LTerm a in
begin match Uf.are_distinct env.uf t1 t2 with
| Yes ex' ->
let ex_r = Ex.union ex ex' in
Print.contra_congruence a ex_r;
(dist, ex_r) :: acc
| No -> assert false
end
| _ -> acc
) [] (Uf.class_of env.uf bol)
| _ -> []
let contra_congruence =
let true_,_ = X.make T.true_ in
let false_, _ = X.make T.false_ in
fun env r ex ->
if X.equal (fst (Uf.find_r env.uf r)) true_ then
new_facts_by_contra_congruence env r T.false_ ex
else if X.equal (fst (Uf.find_r env.uf r)) false_ then
new_facts_by_contra_congruence env r T.true_ ex
else []
let clean_use =
List.fold_left
(fun env (a, ex) ->
match a with
| LSem _ -> assert false
| LTerm t ->
begin
match A.LT.view t with
| A.Distinct (_, lt)
| A.Builtin (_, _, lt) ->
let lvs = concat_leaves env.uf lt in
List.fold_left
(fun env rx ->
let st, sa = Use.find rx env.use in
let sa = SetA.remove (t, ex) sa in
{ env with use = Use.add rx (st,sa) env.use }
) env lvs
| _ -> assert false
end)
let rec congruence_closure env r1 r2 ex =
Print.cc r1 r2;
let uf, res = Uf.union env.uf r1 r2 ex in
List.fold_left
(fun (env, l) (p, touched, v) ->
(* we look for use(p) *)
let p_t, p_a = Use.find p env.use in
(* we compute terms and atoms to consider for congruence *)
let repr_touched = List.map (fun (_,a,_) -> a) touched in
let st_others, sa_others = Use.congr_close_up env.use p repr_touched in
(* we update use *)
let nuse = Use.up_close_up env.use p v in
Use.print nuse;
(* we check the congruence of the terms. *)
let env = {env with use=nuse} in
let new_eqs =
SetT.fold (fun t l -> congruents env t st_others l ex) p_t l in
let touched_atoms =
List.map (fun (x,y,e)-> (LSem(A.Eq(x, y)), e)) touched
in
let touched_atoms = SetA.fold (fun (a, ex) acc ->
(LTerm a, ex)::acc) p_a touched_atoms in
let touched_atoms = SetA.fold (fun (a, ex) acc ->
(LTerm a, ex)::acc) sa_others touched_atoms in
env, new_eqs @ touched_atoms
) ({env with uf=uf}, []) res
let replay_atom env sa =
let relation, result = X.Rel.assume env.relation sa in
let env = { env with relation = relation } in
let env = clean_use env result.remove in
env, result.assume
let rec add_term env choices t ex =
(* nothing to do if the term already exists *)
if Uf.mem env.uf t then env, choices
else begin
Print.add_to_use t;
(* we add t's arguments in env *)
let {T.f = f; xs = xs} = T.view t in
let env, choices =
List.fold_left (fun (env, ch) t -> add_term env ch t ex)
(env, choices) xs
in
(* we update uf and use *)
let nuf, ctx = Uf.add env.uf t in
Print.make_cst t ctx;
let rt, _ = Uf.find nuf t in (* XXX : ctx only in terms *)
if !cc_active then
let lvs = concat_leaves nuf xs in
let nuse = Use.up_add env.use t rt lvs in
(* If finitetest is used we add the term to the relation *)
let rel = X.Rel.add env.relation rt in
Use.print nuse;
(* we compute terms to consider for congruence *)
(* we do this only for non-atomic terms with uninterpreted head-symbol *)
let st_uset = Use.congr_add nuse lvs in
(* we check the congruence of each term *)
let env = {uf = nuf; use = nuse; relation = rel} in
let ct = congruents env t st_uset [] ex in
let ct = (List.map (fun lt -> LTerm lt, ex) ctx) @ ct in
assume_literal env choices ct
else
let rel = X.Rel.add env.relation rt in
let env = {env with uf = nuf; relation = rel} in
env, choices
end
and add env choices a ex =
match A.LT.view a with
| A.Eq (t1, t2) ->
let env, choices = add_term env choices t1 ex in
add_term env choices t2 ex
| A.Distinct (_, lt)
| A.Builtin (_, _, lt) ->
let env, choices = List.fold_left
(fun (env, ch) t-> add_term env ch t ex) (env, choices) lt in
let lvs = concat_leaves env.uf lt in (* A verifier *)
let env = List.fold_left
(fun env rx ->
let st, sa = Use.find rx env.use in
{ env with
use = Use.add rx (st,SetA.add (a, ex) sa) env.use }
) env lvs
in
env, choices
and semantic_view env choices la =
List.fold_left
(fun (env, choices, lsa) (a, ex) ->
match a with
| LTerm a ->
let env, choices = add env choices a ex in
let sa, ex = term_canonical_view env a ex in
env, choices, (sa, Some a, ex)::lsa
(* XXX si on fait canonical_view pour
A.Distinct, la theorie des tableaux
part dans les choux *)
| LSem (A.Builtin _ (*| A.Distinct _*) as sa) ->
let sa, ex = canonical_view env sa ex in
env, choices, (sa, None, ex)::lsa
| LSem sa ->
env, choices, (sa, None, ex)::lsa)
(env, choices, []) la
and assume_literal env choices la =
if la = [] then env, choices
else
let env, choices, lsa = semantic_view env choices la in
let env, choices =
List.fold_left
(fun (env, choices) (sa, _, ex) ->
Print.assume_literal sa;
match sa with
| A.Eq(r1, r2) ->
if !cc_active then
let env, l = congruence_closure env r1 r2 ex in
let env, choices = assume_literal env choices l in
let env, choices =
assume_literal env choices (contra_congruence env r1 ex)
in
assume_literal env choices (contra_congruence env r2 ex)
else
{env with uf = fst(Uf.union env.uf r1 r2 ex)}, choices
| A.Distinct (false, lr) ->
if Uf.already_distinct env.uf lr then env, choices
else
{env with uf = Uf.distinct env.uf lr ex}, choices
| A.Distinct (true, _) -> assert false
| A.Builtin _ -> env, choices)
(env, choices) lsa
in
let env, l = replay_atom env lsa in
assume_literal env (choices@l) l
let look_for_sat ?(bad_last=No) ch t base_env l =
let rec aux ch bad_last dl base_env li =
match li, bad_last with
| [], _ ->
begin
match X.Rel.case_split base_env.relation with
| [] ->
{ t with gamma_finite = base_env; choices = List.rev dl }, ch
| l ->
let l =
List.map
(fun (c, ex_c, size) ->
let exp = Ex.fresh_exp () in
let ex_c_exp = Ex.add_fresh exp ex_c in
(* A new explanation in order to track the choice *)
(c, size, CPos exp, ex_c_exp)) l in
let sz =
List.fold_left
(fun acc (a,s,_,_) ->
Num.mult_num acc s) (Num.Int 1) (l@dl) in
Print.split_size sz;
if Num.le_num sz max_split then aux ch No dl base_env l
else
{ t with gamma_finite = base_env; choices = List.rev dl }, ch
end
| ((c, size, CNeg, ex_c) as a)::l, _ ->
let base_env, ch = assume_literal base_env ch [LSem c, ex_c] in
aux ch bad_last (a::dl) base_env l
(** This optimisation is not correct with the current explanation *)
(* | [(c, size, CPos exp, ex_c)], Yes dep -> *)
(* let neg_c = LR.neg (LR.make c) in *)
(* let ex_c = Ex.union ex_c dep in *)
(* Print.split_backtrack neg_c ex_c; *)
(* aux ch No dl base_env [LR.view neg_c, Num.Int 1, CNeg, ex_c] *)
| ((c, size, CPos exp, ex_c_exp) as a)::l, _ ->
try
Print.split_assume (LR.make c) ex_c_exp;
let base_env, ch = assume_literal base_env ch [LSem c, ex_c_exp] in
aux ch bad_last (a::dl) base_env l
with Exception.Inconsistent dep ->
match Ex.remove_fresh exp dep with
| None ->
(* The choice doesn't participate to the inconsistency *)
Print.split_backjump (LR.make c) dep;
raise (Exception.Inconsistent dep)
| Some dep ->
(* The choice participates to the inconsistency *)
let neg_c = LR.neg (LR.make c) in
Print.split_backtrack neg_c dep;
aux ch No dl base_env [LR.view neg_c, Num.Int 1, CNeg, dep]
in
aux ch bad_last (List.rev t.choices) base_env l
let try_it f t =
Print.begin_case_split ();
let r =
try
if t.choices = [] then look_for_sat [] t t.gamma []
else
try
let env, lt = f t.gamma_finite in
look_for_sat lt t env []
with Exception.Inconsistent dep ->
look_for_sat ~bad_last:(Yes dep)
[] { t with choices = []} t.gamma t.choices
with Exception.Inconsistent d ->
Print.end_case_split ();
raise (Exception.Inconsistent d)
in
Print.end_case_split (); r
let extract_from_semvalues =
List.fold_left
(fun acc r ->
match X.term_extract r with Some t -> SetT.add t acc | _ -> acc)
let extract_terms_from_choices =
List.fold_left
(fun acc (a, _, _, _) ->
match a with
| A.Eq(r1, r2) -> extract_from_semvalues acc [r1; r2]
| A.Distinct (_, l) -> extract_from_semvalues acc l
| _ -> acc)
let extract_terms_from_assumed =
List.fold_left
(fun acc (a, _) ->
match a with
| LTerm r -> begin
match Literal.LT.view r with
| Literal.Eq (t1, t2) ->
SetT.add t1 (SetT.add t2 acc)
| Literal.Distinct (_, l) | Literal.Builtin (_, _, l) ->
List.fold_right SetT.add l acc
end
| _ -> acc)
let assume ~cs a ex t =
let a = LTerm a in
let gamma, ch = assume_literal t.gamma [] [a, ex] in
let t = { t with gamma = gamma } in
let t, ch =
if cs then try_it (fun env -> assume_literal env ch [a, ex] ) t
else t, ch
in
let choices = extract_terms_from_choices SetT.empty t.choices in
let all_terms = extract_terms_from_assumed choices ch in
t, all_terms, 1
let class_of t term = Uf.class_of t.gamma.uf term
let add_and_process a t =
let aux a ex env =
let gamma, l = add env [] a ex in assume_literal gamma [] l
in
let gamma, _ = aux a Ex.empty t.gamma in
let t = { t with gamma = gamma } in
let t, _ = try_it (aux a Ex.empty) t in
Use.print t.gamma.use; t
let query a t =
Print.query a;
try
match A.LT.view a with
| A.Eq (t1, t2) ->
let t = add_and_process a t in
Uf.are_equal t.gamma.uf t1 t2
| A.Distinct (false, [t1; t2]) ->
let na = A.LT.neg a in
let t = add_and_process na t in (* na ? *)
Uf.are_distinct t.gamma.uf t1 t2
| A.Distinct _ ->
assert false (* devrait etre capture par une analyse statique *)
| _ ->
let na = A.LT.neg a in
let t = add_and_process na t in
let env = t.gamma in
let rna, ex_rna = term_canonical_view env na Ex.empty in
X.Rel.query env.relation (rna, Some na, ex_rna)
with Exception.Inconsistent d -> Yes d
let empty () =
let env = {
use = Use.empty ;
uf = Uf.empty ;
relation = X.Rel.empty ();
}
in
let t = { gamma = env; gamma_finite = env; choices = [] } in
let t, _, _ =
assume ~cs:false
(A.LT.make (A.Distinct (false, [T.true_; T.false_]))) Ex.empty t
in t
end

37
src/smt/cc.mli Normal file
View file

@ -0,0 +1,37 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
open Msat
val cc_active : bool ref
type answer = Yes of Explanation.t | No
module type S = sig
type t
val empty : unit -> t
val assume :
cs:bool ->
Literal.LT.t ->
Explanation.t ->
t -> t * Term.Set.t * int
val query : Literal.LT.t -> t -> answer
val class_of : t -> Term.t -> Term.t list
end
module Make (Dummy : sig end) : S

2
src/example/cnf.ml → src/smt/cnf.ml
View file

@ -4,4 +4,6 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
open Msat
module S = Tseitin.Make(Expr)

2
src/example/cnf.mli → src/smt/cnf.mli
View file

@ -4,4 +4,6 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
open Msat
module S : Tseitin.S with type atom = Expr.Formula.t

68
src/smt/explanation.ml Normal file
View file

@ -0,0 +1,68 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon and Alain Mebsout *)
(* Stephane Lescuyer *)
(* INRIA, Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
type atom = Literal.LT.t
type exp = Atom of atom | Fresh of int
module S =
Set.Make
(struct
type t = exp
let compare a b = match a,b with
| Atom _, Fresh _ -> -1
| Fresh _, Atom _ -> 1
| Fresh i1, Fresh i2 -> i1 - i2
| Atom a, Atom b -> a.aid - b.aid
end)
type t = S.t
let singleton e = S.singleton (Atom e)
let empty = S.empty
let union s1 s2 = S.union s1 s2
let iter_atoms f s =
S.iter (fun e -> match e with
| Fresh _ -> ()
| Atom a -> f a) s
let fold_atoms f s acc =
S.fold (fun e acc -> match e with
| Fresh _ -> acc
| Atom a -> f a acc) s acc
let merge e1 e2 = e1
let fresh_exp =
let r = ref (-1) in
fun () -> incr r; !r
let remove_fresh i s =
let fi = Fresh i in
if S.mem fi s then Some (S.remove fi s)
else None
let add_fresh i = S.add (Fresh i)
let print fmt ex =
fprintf fmt "{";
S.iter (function
| Atom a -> fprintf fmt "%a, " Debug.atom a
| Fresh i -> fprintf fmt "Fresh%d " i) ex;
fprintf fmt "}"

39
src/smt/explanation.mli Normal file
View file

@ -0,0 +1,39 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon and Alain Mebsout *)
(* Stephane Lescuyer *)
(* INRIA, Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
type t
type exp
type atom = Literal.LT.t
val empty : t
val singleton : atom-> t
val union : t -> t -> t
val merge : t -> t -> t
val iter_atoms : (atom -> unit) -> t -> unit
val fold_atoms : (atom -> 'a -> 'a ) -> t -> 'a -> 'a
val fresh_exp : unit -> int
val remove_fresh : int -> t -> t option
val add_fresh : int -> t -> t
val print : Format.formatter -> t -> unit

57
src/example/expr.ml → src/smt/expr.ml
View file

@ -3,36 +3,56 @@ MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
open Msat
module I = Formula_intf
module Term = Term
exception Invalid_var
exception Invalid_prop
type var = string
type term = Term.t
(* atomic formula
Prop:
- sign of int determines sign of formula
- odd numbers --> fresh atoms (for Tseitin CNF)
- even numbers --> used for regular int-mapping
*)
type formula =
| Prop of int
| Equal of var * var
| Distinct of var * var
| Equal of term * term
| Distinct of term * term
type t = formula
type proof = unit
let dummy = Prop 0
let max_fresh = ref 0
let fresh () =
incr max_fresh;
Prop (2 * !max_fresh + 1)
let mk_prop i =
if i <> 0 && i < max_int / 2 then Prop (2 * i)
else raise Invalid_var
else raise Invalid_prop
let mk_var i =
if i <> "" then i
else raise Invalid_var
let order_ t1 t2 = if Term.compare t1 t2 > 0 then t2,t1 else t1,t2
let mk_eq i j = Equal (mk_var (min i j), mk_var (max i j))
let mk_neq i j = Distinct (mk_var (min i j), mk_var (max i j))
let mk_eq a b =
let a, b = order_ a b in
Equal (a, b)
let mk_neq a b =
let a, b = order_ a b in
Distinct (a, b)
let mk_true = mk_eq Term.true_ Term.true_
let mk_false = mk_eq Term.true_ Term.false_
let mk_atom = mk_eq Term.true_
let mk_atom_neg = mk_eq Term.false_
let neg = function
| Prop i -> Prop (-i)
@ -50,17 +70,12 @@ let equal = (=)
let compare = Pervasives.compare
let print fmt = function
| Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") ((abs i) / 2)
| Equal (a, b) -> Format.fprintf fmt "%s = %s" a b
| Distinct (a, b) -> Format.fprintf fmt "%s ≠ %s" a b
module Term = struct
type t = var
let hash = Hashtbl.hash
let equal = (=)
let compare = Pervasives.compare
let print fmt t = Format.fprintf fmt "%s" t
end
| Prop i ->
Format.fprintf fmt "%s%s%d"
(if i < 0 then "¬ " else "")
(if i mod 2 = 0 then "v" else "f") ((abs i) / 2)
| Equal (a, b) -> Format.fprintf fmt "(@[=@ %a@ %a@])" Term.print a Term.print b
| Distinct (a, b) -> Format.fprintf fmt "(@[!=@ %a@ %a@])" Term.print a Term.print b
module Formula = struct
type t = formula

29
src/example/expr.mli → src/smt/expr.mli
View file

@ -3,12 +3,14 @@ MSAT is free software, using the Apache license, see file LICENSE
Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
open Msat
type term = Term.t
type var = string
type formula = private
| Prop of int
| Equal of var * var
| Distinct of var * var
| Prop of int (* prop or tseitin atom *)
| Equal of term * term
| Distinct of term * term
type t = formula
type proof = unit
@ -20,16 +22,17 @@ val dummy : t
val fresh : unit -> t
val mk_prop : int -> t
val mk_eq : var -> var -> t
val mk_neq : var -> var -> t
(** [mk_prop i] makes a prop literal from [i], whose sign matters.
@raise Invalid_prop if [i=0] or if [i] is too large *)
module Term : sig
type t = var
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val print : Format.formatter -> t -> unit
end
val mk_true : t
val mk_false : t
val mk_atom : term -> t
val mk_atom_neg : term -> t
val mk_eq : term -> term -> t
val mk_neq : term -> term -> t
module Term = Term
module Formula : sig
type t = formula
val hash : t -> int

184
src/smt/literal.ml Normal file
View file

@ -0,0 +1,184 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
open Msat
type 'a view =
| Eq of 'a * 'a
| Distinct of bool * 'a list
| Builtin of bool * ID.t * 'a list
module type OrderedType = sig
type t
val compare : t -> t -> int
val hash : t -> int
val print : Format.formatter -> t -> unit
end
module type S = sig
type elt
type t
val make : elt view -> t
val view : t -> elt view
val neg : t -> t
val print : Format.formatter -> t -> unit
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
module Map : Map.S with type key = t
module Set : Set.S with type elt = t
end
module Make (X : OrderedType) : S with type elt = X.t = struct
type elt = X.t
type t = {
view: X.t view;
mutable tag: int;
}
module V = struct
type t_ = t
type t = t_
let equal a1 a2 =
match a1.view, a2.view with
| Eq(t1, t2), Eq(u1, u2) ->
(X.compare t1 u1 = 0 && X.compare t2 u2 = 0) ||
(X.compare t1 u2 = 0 && X.compare t2 u1 = 0)
| Distinct (b1,lt1), Distinct (b2,lt2) ->
(try
b1 = b2 &&
List.for_all2 (fun x y -> X.compare x y = 0) lt1 lt2
with Invalid_argument _ -> false)
| Builtin(b1, n1, l1), Builtin(b2, n2, l2) ->
(try
b1 = b2 && ID.equal n1 n2
&&
List.for_all2 (fun x y -> X.compare x y = 0) l1 l2
with Invalid_argument _ -> false)
| _ -> false
let hash a = match a.view with
| Eq(t1, t2) -> abs (19 * (X.hash t1 + X.hash t2))
| Distinct (b,lt) ->
let x = if b then 7 else 23 in
abs (17 * List.fold_left (fun acc t -> (X.hash t) + acc ) x lt)
| Builtin(b, n, l) ->
let x = if b then 7 else 23 in
abs
(List.fold_left
(fun acc t-> acc*13 + X.hash t) (ID.hash n+x) l)
let set_id t tag = t.tag <- tag
end
module H = Hashcons.Make(V)
let compare a1 a2 = Pervasives.compare a1.tag a2.tag
let equal a1 a2 = a1 == a2
let hash a1 = a1.tag
module T = struct
type t_ = t
type t = t_
let compare=compare
end
let make t = H.hashcons {view=t; tag= -1}
let view a = a.view
let neg a = match view a with
| Eq(x, y) -> make (Distinct (false,[x; y]))
| Distinct (false, [x; y]) -> make (Eq (x, y))
| Distinct (true, [x; y]) -> make (Distinct (false,[x; y]))
| Distinct (false, l) -> make (Distinct (true,l))
| Distinct _ -> assert false
| Builtin(b, n, l) -> make (Builtin (not b, n, l))
let print_list fmt = function
| [] -> ()
| z :: l ->
Format.fprintf fmt "%a" X.print z;
List.iter (Format.fprintf fmt ", %a" X.print) l
let print fmt a = match view a with
| Eq (z1, z2) ->
if equal z1 z2 then Format.fprintf fmt "True"
else Format.fprintf fmt "%a=%a" X.print z1 X.print z2
| Distinct (b,(z::l)) ->
let b = if b then "~" else "" in
Format.fprintf fmt "%s%a" b X.print z;
List.iter (fun x -> Format.fprintf fmt "<>%a" X.print x) l
| Builtin (b, n, l) ->
let b = if b then "" else "~" in
Format.fprintf fmt "%s%s(%a)" b (ID.to_string n) print_list l
| _ -> assert false
module Set = Set.Make(T)
module Map = Map.Make(T)
end
module type S_Term = sig
include S with type elt = Term.t
val mk_pred : Term.t -> t
val true_ : t
val false_ : t
(* val terms_of : t -> Term.Set.t
val vars_of : t -> Symbols.Set.t
*)
(* module SetEq : Set.S with type elt = t * Term.t * Term.t*)
end
module LT : S_Term = struct
module L = Make(Term)
include L
let mk_pred t = make (Eq (t, Term.true_) )
let true_ = mk_pred Term.true_
let false_ = mk_pred Term.false_
let neg a = match view a with
| Eq(t1, t2) when Term.equal t2 Term.false_ ->
make (Eq (t1, Term.true_))
| Eq(t1, t2) when Term.equal t2 Term.true_ ->
make (Eq (t1, Term.false_))
| _ -> L.neg a
(* let terms_of a =
let l = match view a with
| Eq (t1, t2) -> [t1; t2]
| Distinct (_, l) | Builtin (_, _, l) -> l
in
List.fold_left Term.subterms Term.Set.empty l
*)
module SS = Symbols.Set
(* let vars_of a =
Term.Set.fold (fun t -> SS.union (Term.vars_of t)) (terms_of a) SS.empty
*)
end

62
src/smt/literal.mli Normal file
View file

@ -0,0 +1,62 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
open Msat
module type OrderedType = sig
type t
val compare : t -> t -> int
val hash : t -> int
val print : Format.formatter -> t -> unit
end
type 'a view =
| Eq of 'a * 'a
| Distinct of bool * 'a list
| Builtin of bool * ID.t * 'a list
module type S = sig
type elt
type t
val make : elt view -> t
val view : t -> elt view
val neg : t -> t
val print : Format.formatter -> t -> unit
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
module Map : Map.S with type key = t
module Set : Set.S with type elt = t
end
module Make ( X : OrderedType ) : S with type elt = X.t
module type S_Term = sig
include S with type elt = Term.t
val mk_pred : Term.t -> t
val true_ : t
val false_ : t
end
module LT : S_Term

2
src/example/mcsat.ml → src/smt/mcsat.ml
View file

@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
open Msat
module Fsmt = Expr
module Tsmt = struct

0
src/example/smt.ml → src/smt/smt.ml
View file

0
src/example/smt.mli → src/smt/smt.mli
View file

62
src/smt/symbols.ml Normal file
View file

@ -0,0 +1,62 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
type name_kind = Constructor | Other
type t =
| True
| False
| Name of ID.t * name_kind
| Var of ID.t
let name ?(kind=Other) s = Name (s, kind)
let var s = Var s
let compare_kind k1 k2 = match k1, k2 with
| Other, Other -> 0
| Other, _ -> 1
| _ , Other -> -1
| Constructor, Constructor -> 0
let compare s1 s2 = match s1, s2 with
| Name (n1,k1), Name (n2,k2) ->
let c = compare_kind k1 k2 in
if c = 0 then ID.compare n1 n2 else c
| Name _, _ -> -1
| _, Name _ -> 1
| Var n1, Var n2 -> ID.compare n1 n2
| Var _, _ -> -1
| _ ,Var _ -> 1
| _ -> Pervasives.compare s1 s2
let equal s1 s2 = compare s1 s2 = 0
let hash = function
| Name (n,_) -> ID.hash n * 19
| Var n (*| Int n*) -> ID.hash n * 19 + 1
| s -> Hashtbl.hash s
let to_string = function
| Name (n,_) -> ID.to_string n
| Var x -> "*var* "^(ID.to_string x)
| True -> "true"
| False -> "false"
let print fmt s = Format.fprintf fmt "%s" (to_string s)
module Map =
Map.Make(struct type t' = t type t=t' let compare=compare end)
module Set =
Set.Make(struct type t' = t type t=t' let compare=compare end)

33
src/smt/symbols.mli Normal file
View file

@ -0,0 +1,33 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
type name_kind = Constructor | Other
type t =
| True
| False
| Name of ID.t * name_kind
| Var of ID.t
val name : ?kind:name_kind -> ID.t -> t
val var : ID.t -> t
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val print : Format.formatter -> t -> unit
module Map : Map.S with type key = t
module Set : Set.S with type elt = t

100
src/smt/term.ml Normal file
View file

@ -0,0 +1,100 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
open Msat
module Sy = Symbols
type view = {
head: head;
ty: Ty.t;
mutable tag: int;
}
and head =
| App of Symbols.t * t list
| Ite of t * t * t
and t = view
module H = struct
type t = view
let equal t1 t2 = match t1.head, t2.head with
| App (f1,l1), App (f2,l2) ->
begin try
Sy.equal f1 f2
&& List.for_all2 (==) l1 l2
&& Ty.equal t1.ty t2.ty
with Invalid_argument _ ->
false
end
| Ite (a1,b1,c1), Ite (a2,b2,c2) ->
a1==a2 && b1==b2 && c1==c2
| App _, Ite _
| Ite _, App _ -> false
let hash t = match t.head with
| Ite (a,b,c) ->
abs
(List.fold_left
(fun acc x-> acc*19 +x.tag) 17 [a;b;c])
| App (f,l) ->
abs
(List.fold_left
(fun acc x-> acc*19 +x.tag) (Sy.hash f + Ty.hash t.ty)
l)
let set_id x tag = x.tag <- tag
end
module T = Hashcons.Make(H)
let view t = t
let rec print fmt t = match t.head with
| Ite (a,b,c) ->
Format.fprintf fmt "(@[<2>ite@ %a@ %a@ %a@])" print a print b print c
| App (x, l) ->
match x, l with
| _, [] -> Format.fprintf fmt "%a" Sy.print x
| _, _ -> Format.fprintf fmt "%a(%a)" Sy.print x print_list l
and print_list fmt = function
| [] -> ()
| [t] -> print fmt t
| t::l -> Format.fprintf fmt "%a,%a" print t print_list l
let compare t1 t2 =
let c = Pervasives.compare t2.tag t1.tag in
if c = 0 then c
else match t1.head, t2.head with
| App ((Sy.True | Sy.False), _), App ((Sy.True | Sy.False), _) -> c
| App ((Sy.True | Sy.False), _), _ -> -1
| _, App ((Sy.True | Sy.False), _) -> 1
| _,_ -> c
let app s l ty = T.hashcons {head=App(s,l); ty=ty; tag= -1; }
let const s ty = app s [] ty
let ite a b c = T.hashcons {head=Ite (a,b,c); ty=b.ty; tag= -1; }
let true_ = app (Sy.True) [] Ty.Tbool
let false_ = app (Sy.False) [] Ty.Tbool
let equal t1 t2 = t1 == t2
let hash t = t.tag
module Set =
Set.Make(struct type t' = t type t=t' let compare=compare end)
module Map =
Map.Make(struct type t' = t type t=t' let compare=compare end)

45
src/smt/term.mli Normal file
View file

@ -0,0 +1,45 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
open Msat
type t
type view = private {
head: head;
ty: Ty.t;
mutable tag: int;
}
and head =
| App of Symbols.t * t list
| Ite of t * t * t
val view : t -> view
val app : Symbols.t -> t list -> Ty.t -> t
val const : Symbols.t -> Ty.t -> t
val ite : t -> t -> t -> t
val true_ : t
val false_ : t
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
val print : Format.formatter -> t -> unit
module Map : Map.S with type key = t
module Set : Set.S with type elt = t

60
src/smt/ty.ml Normal file
View file

@ -0,0 +1,60 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
open Msat
type symbol = Symbols.t
type t =
| Tbool
| Tabstract of ID.t
| Tsum of ID.t * symbol list
let bool = Tbool
let abstract i = Tabstract i
let sum i l = Tsum (i, l)
let hash t =
match t with
| Tabstract s -> ID.hash s
| Tsum (s, l) ->
let h =
List.fold_left
(fun h x -> 13 * h + Symbols.hash x) (ID.hash s) l
in
abs h
| _ -> Hashtbl.hash t
let equal t1 t2 =
match t1, t2 with
| Tabstract s1, Tabstract s2
| Tsum (s1, _), Tsum (s2, _) ->
ID.equal s1 s2
| Tbool, Tbool -> true
| _ -> false
let compare t1 t2 =
match t1, t2 with
| Tabstract s1, Tabstract s2 ->
ID.compare s1 s2
| Tabstract _, _ -> -1 | _ , Tabstract _ -> 1
| Tsum (s1, _), Tsum(s2, _) ->
ID.compare s1 s2
| Tsum _, _ -> -1 | _ , Tsum _ -> 1
| t1, t2 -> Pervasives.compare t1 t2
let print fmt ty =
match ty with
| Tbool -> Format.fprintf fmt "bool"
| Tabstract s -> Format.fprintf fmt "%s" (ID.to_string s)
| Tsum (s, _) -> Format.fprintf fmt "%s" (ID.to_string s)

29
src/smt/ty.mli Normal file
View file

@ -0,0 +1,29 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
open Msat
type symbol = Symbols.t
type t =
| Tbool
| Tabstract of ID.t
| Tsum of ID.t * symbol list
val bool : t
val abstract : ID.t -> t
val sum : ID.t -> symbol list -> t
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val print : Format.formatter -> t -> unit

381
src/smt/uf.ml Normal file
View file

@ -0,0 +1,381 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
type answer = Yes of Explanation.t | No
type 'a literal =
| LSem of 'a Literal.view
| LTerm of Literal.LT.t
exception Inconsistent of Explanation.t
exception Unsolvable
module type ELT = sig
type r
val make : Term.t -> r * Literal.LT.t list
val compare : r -> r -> int
val equal : r -> r -> bool
val hash : r -> int
val leaves : r -> r list
val subst : r -> r -> r -> r
val can_be_equal : r -> r -> bool
val term_embed : Term.t -> r
val term_extract : r -> Term.t option
val unsolvable : r -> bool
val fully_interpreted : Symbols.t -> bool
val print : Format.formatter -> r -> unit
end
module type S = sig
type t
module R : ELT
val empty : t
val add : t -> Term.t -> t * Literal.LT.t list
val mem : t -> Term.t -> bool
val find : t -> Term.t -> R.r * Explanation.t
val find_r : t -> R.r -> R.r * Explanation.t
val union :
t -> R.r -> R.r -> Explanation.t ->
t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list
val distinct : t -> R.r list -> Explanation.t -> t
val are_equal : t -> Term.t -> Term.t -> Sig.answer
val are_distinct : t -> Term.t -> Term.t -> Sig.answer
val already_distinct : t -> R.r list -> bool
val class_of : t -> Term.t -> Term.t list
end
module Make ( R : ELT ) = struct
module Ex = Explanation
module R = R
module Sy = Symbols
module T = Term
module MapT = Term.Map
module SetT = Term.Set
module Lit = Literal.Make(struct type t = R.r include R end)
module MapL = Lit.Map
module MapR = Map.Make(struct type t = R.r let compare = R.compare end)
module SetR = Set.Make(struct type t = R.r let compare = R.compare end)
module SetRR = Set.Make(struct
type t = R.r * R.r
let compare (r1, r1') (r2, r2') =
let c = R.compare r1 r2 in
if c <> 0 then c
else R.compare r1' r2'
end)
type t = {
(* term -> [t] *)
make : R.r MapT.t;
(* representative table *)
repr : (R.r * Ex.t) MapR.t;
(* r -> class (of terms) *)
classes : SetT.t MapR.t;
(*associates each value r with the set of semantical values whose
representatives contains r *)
gamma : SetR.t MapR.t;
(* the disequations map *)
neqs: Ex.t MapL.t MapR.t;
}
let empty = {
make = MapT.empty;
repr = MapR.empty;
classes = MapR.empty;
gamma = MapR.empty;
neqs = MapR.empty;
}
module Env = struct
let mem env t = MapT.mem t env.make
let lookup_by_t t env =
try MapR.find (MapT.find t env.make) env.repr
with Not_found ->
assert false (*R.make t, Ex.empty*) (* XXXX *)
let lookup_by_r r env =
try MapR.find r env.repr with Not_found -> r, Ex.empty
let lookup_for_neqs env r =
try MapR.find r env.neqs with Not_found -> MapL.empty
let add_to_classes t r classes =
MapR.add r
(SetT.add t (try MapR.find r classes with Not_found -> SetT.empty))
classes
let update_classes c nc classes =
let s1 = try MapR.find c classes with Not_found -> SetT.empty in
let s2 = try MapR.find nc classes with Not_found -> SetT.empty in
MapR.remove c (MapR.add nc (SetT.union s1 s2) classes)
let add_to_gamma r c gamma =
List.fold_left
(fun gamma x ->
let s = try MapR.find x gamma with Not_found -> SetR.empty in
MapR.add x (SetR.add r s) gamma)
gamma (R.leaves c)
(* r1 = r2 => neqs(r1) \uplus neqs(r2) *)
let update_neqs r1 r2 dep env =
let nq_r1 = lookup_for_neqs env r1 in
let nq_r2 = lookup_for_neqs env r2 in
let mapl =
MapL.fold
(fun l1 ex1 mapl ->
try
let ex2 = MapL.find l1 mapl in
let ex = Ex.union (Ex.union ex1 ex2) dep in (* VERIF *)
raise (Inconsistent ex)
with Not_found ->
MapL.add l1 (Ex.union ex1 dep) mapl)
nq_r1 nq_r2
in
MapR.add r2 mapl (MapR.add r1 mapl env.neqs)
let filter_leaves r =
List.fold_left (fun p r -> SetR.add r p) SetR.empty (R.leaves r)
let canon_empty st env =
SetR.fold
(fun p ((z, ex) as acc) ->
let q, ex_q = lookup_by_r p env in
if R.equal p q then acc else (p,q)::z, Ex.union ex_q ex)
st ([], Ex.empty)
let canon_aux rx = List.fold_left (fun r (p,v) -> R.subst p v r) rx
let rec canon env r ex_r =
let se = filter_leaves r in
let subst, ex_subst = canon_empty se env in
let r2 = canon_aux r subst in
let ex_r2 = Ex.union ex_r ex_subst in
if R.equal r r2 then r2, ex_r2 else canon env r2 ex_r2
let normal_form env r = canon env r Ex.empty
let find_or_normal_form env r =
try MapR.find r env.repr with Not_found -> normal_form env r
let init_leaf env p =
let in_repr = MapR.mem p env.repr in
let in_neqs = MapR.mem p env.neqs in
{ env with
repr =
if in_repr then env.repr
else MapR.add p (p, Ex.empty) env.repr;
classes =
if in_repr then env.classes
else update_classes p p env.classes;
gamma =
if in_repr then env.gamma
else add_to_gamma p p env.gamma ;
neqs =
if in_neqs then env.neqs
else update_neqs p p Ex.empty env }
let init_term env t =
let mkr, ctx = R.make t in
let rp, ex = normal_form env mkr in
{ make = MapT.add t mkr env.make;
repr = MapR.add mkr (rp,ex) env.repr;
classes = add_to_classes t rp env.classes;
gamma = add_to_gamma mkr rp env.gamma;
neqs =
if MapR.mem rp env.neqs then env.neqs (* pourquoi ce test *)
else MapR.add rp MapL.empty env.neqs}, ctx
let update_aux dep set env=
SetRR.fold
(fun (rr, nrr) env ->
{ env with
neqs = update_neqs rr nrr dep env ;
classes = update_classes rr nrr env.classes})
set env
let apply_sigma_uf env (p, v, dep) =
assert (MapR.mem p env.gamma);
let use_p = MapR.find p env.gamma in
try
let env, tch, neqs_to_up = SetR.fold
(fun r (env, touched, neqs_to_up) ->
let rr, ex = MapR.find r env.repr in
let nrr = R.subst p v rr in
if R.equal rr nrr then env, touched, neqs_to_up
else
let ex = Ex.union ex dep in
let env =
{env with
repr = MapR.add r (nrr, ex) env.repr;
gamma = add_to_gamma r nrr env.gamma }
in
env, (r, nrr, ex)::touched, SetRR.add (rr, nrr) neqs_to_up
) use_p (env, [], SetRR.empty) in
(* Correction : Do not update neqs twice for the same r *)
update_aux dep neqs_to_up env, tch
with Not_found -> assert false
let apply_sigma eqs env tch ((p, v, dep) as sigma) =
let env = init_leaf env p in
let env, touched = apply_sigma_uf env sigma in
env, ((p, touched, v) :: tch)
end
let add env t =
if MapT.mem t env.make then env, [] else Env.init_term env t
let ac_solve eqs dep (env, tch) (p, v) =
(* pourquoi recuperer le representant de rv? r = rv d'apres testopt *)
(* assert ( let rp, _ = Env.find_or_normal_form env p in R.equal p rp); *)
let rv, ex_rv = Env.find_or_normal_form env v in
(* let rv = v in *)
(* assert ( let rv, _ = Env.find_or_normal_form env v in R.equal v rv); *)
let dep = Ex.union ex_rv dep in
Env.apply_sigma eqs env tch (p, rv, dep)
let check_consistent env r1 r2 dep : unit =
let rr1, ex_r1 = Env.find_or_normal_form env r1 in
let rr2, ex_r2 = Env.find_or_normal_form env r2 in
if R.equal rr1 rr2
then () (* Remove rule *)
else
let dep = Ex.union dep (Ex.union ex_r1 ex_r2) in
begin
ignore (Env.update_neqs rr1 rr2 dep env);
if R.can_be_equal rr1 rr2
then ()
else raise (Inconsistent dep)
end
let union env r1 r2 dep =
check_consistent env r1 r2 dep;
()
let rec distinct env rl dep =
let d = Lit.make (Literal.Distinct (false,rl)) in
let env, _, newds =
List.fold_left
(fun (env, mapr, newds) r ->
let rr, ex = Env.find_or_normal_form env r in
try
let exr = MapR.find rr mapr in
raise (Inconsistent (Ex.union ex exr))
with Not_found ->
let uex = Ex.union ex dep in
let mdis =
try MapR.find rr env.neqs with Not_found -> MapL.empty in
let mdis =
try
MapL.add d (Ex.merge uex (MapL.find d mdis)) mdis
with Not_found ->
MapL.add d uex mdis
in
let env = Env.init_leaf env rr in
let env = {env with neqs = MapR.add rr mdis env.neqs} in
env, MapR.add rr uex mapr, (rr, ex, mapr)::newds
)
(env, MapR.empty, [])
rl
in
List.fold_left
(fun env (r1, ex1, mapr) ->
MapR.fold (fun r2 ex2 env ->
let ex = Ex.union ex1 (Ex.union ex2 dep) in
try match R.solve r1 r2 with
| [a, b] ->
if (R.equal a r1 && R.equal b r2) ||
(R.equal a r2 && R.equal b r1) then env
else
distinct env [a; b] ex
| [] ->
raise (Inconsistent ex)
| _ -> env
with Unsolvable -> env) mapr env)
env newds
let are_equal env t1 t2 =
let r1, ex_r1 = Env.lookup_by_t t1 env in
let r2, ex_r2 = Env.lookup_by_t t2 env in
if R.equal r1 r2 then Yes(Ex.union ex_r1 ex_r2) else No
let are_distinct env t1 t2 =
let r1, ex_r1 = Env.lookup_by_t t1 env in
let r2, ex_r2 = Env.lookup_by_t t2 env in
try
ignore (union env r1 r2 (Ex.union ex_r1 ex_r2));
No
with Inconsistent ex -> Yes(ex)
let already_distinct env lr =
let d = Lit.make (Literal.Distinct (false,lr)) in
try
List.iter (fun r ->
let mdis = MapR.find r env.neqs in
ignore (MapL.find d mdis)
) lr;
true
with Not_found -> false
let find env t =
Env.lookup_by_t t env
let find_r = Env.find_or_normal_form
let mem = Env.mem
let class_of env t =
try
let rt, _ = MapR.find (MapT.find t env.make) env.repr in
SetT.elements (MapR.find rt env.classes)
with Not_found -> [t]
end

78
src/smt/uf.mli Normal file
View file

@ -0,0 +1,78 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
type answer = Yes of Explanation.t | No
type 'a literal =
| LSem of 'a Literal.view
| LTerm of Literal.LT.t
module type ELT = sig
type r
val make : Term.t -> r * Literal.LT.t list
val type_info : r -> Ty.t
val compare : r -> r -> int
val equal : r -> r -> bool
val hash : r -> int
val leaves : r -> r list
val subst : r -> r -> r -> r
val solve : r -> r -> (r * r) list
val term_embed : Term.t -> r
val term_extract : r -> Term.t option
val unsolvable : r -> bool
val fully_interpreted : Symbols.t -> bool
val print : Format.formatter -> r -> unit
end
module type S = sig
type t
module R : ELT
val empty : t
val add : t -> Term.t -> t * Literal.LT.t list
val mem : t -> Term.t -> bool
val find : t -> Term.t -> R.r * Explanation.t
val find_r : t -> R.r -> R.r * Explanation.t
val union :
t -> R.r -> R.r -> Explanation.t ->
t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list
val distinct : t -> R.r list -> Explanation.t -> t
val are_equal : t -> Term.t -> Term.t -> Sig.answer
val are_distinct : t -> Term.t -> Term.t -> Sig.answer
val already_distinct : t -> R.r list -> bool
val class_of : t -> Term.t -> Term.t list
end
module Make ( X : ELT ) : S with module R = X

11
src/example/unionfind.ml → src/smt/unionfind.ml
View file

@ -4,13 +4,20 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module type OrderedType = sig
type t
val compare : t -> t -> int
end
(* Union-find Module *)
module Make(T : Sig.OrderedType) = struct
module Make(T : OrderedType) = struct
exception Unsat of T.t * T.t
type var = T.t
module M = Map.Make(T)
(* TODO: better treatment of inequalities *)
type t = {
rank : int M.t;
forbid : ((var * var) list);
@ -43,7 +50,7 @@ module Make(T : Sig.OrderedType) = struct
h.parent <- f;
cx
(* Highly ineficient treatment of inequalities *)
(* Highly inefficient treatment of inequalities *)
let possible h =
let aux (a, b) =
let ca = find h a in

7
src/example/unionfind.mli → src/smt/unionfind.mli
View file

@ -4,7 +4,12 @@ Copyright 2014 Guillaume Bury
Copyright 2014 Simon Cruanes
*)
module Make(T : Sig.OrderedType) : sig
module type OrderedType = sig
type t
val compare : t -> t -> int
end
module Make(T : OrderedType) : sig
type t
exception Unsat of T.t * T.t
val empty : t

28
src/util/hashcons.ml Normal file
View file

@ -0,0 +1,28 @@
module type ARG = sig
type t
val equal : t -> t -> bool
val hash : t -> int
val set_id : t -> int -> unit
end
module Make(A : ARG): sig
val hashcons : A.t -> A.t
val iter : (A.t -> unit) -> unit
end = struct
module W = Weak.Make(A)
let tbl_ = W.create 1024
let n_ = ref 0
(* hashcons terms *)
let hashcons t =
let t' = W.merge tbl_ t in
if t == t' then (
incr n_;
A.set_id t' !n_;
);
t'
let iter yield = W.iter yield tbl_
end