simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge branch 'master' of github.com:Gbury/mSAT

Browse source
This commit is contained in:
Guillaume Bury 2016-11-21 15:53:08 +01:00
commit 0dc44b1173
12 changed files with 22 additions and 1038 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Makefile
View file

@ -3,7 +3,7 @@
LOG=build.log LOG=build.log
COMP=ocamlbuild -log $(LOG) -use-ocamlfind COMP=ocamlbuild -log $(LOG) -use-ocamlfind
FLAGS= FLAGS=
DOC=msat.docdir/index.html msat_sat.docdir/index.html msat_smt.docdir/index.html DOC=src/msat.docdir/index.html
BIN=main.native BIN=main.native
TEST_BIN=tests/test_api.native TEST_BIN=tests/test_api.native

3
README.md
View file

@ -12,6 +12,9 @@ It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).
This program is distributed under the Apache Software License version This program is distributed under the Apache Software License version
2.0. See the enclosed file `LICENSE`. 2.0. See the enclosed file `LICENSE`.
## Documentation
See https://gbury.github.io/mSAT/
## USAGE ## USAGE

2
src/core/solver_types_intf.ml
View file

@ -140,7 +140,7 @@ module type S = sig
val add_atom : formula -> atom val add_atom : formula -> atom
(** Returns the atom associated with the given formula *) (** Returns the atom associated with the given formula *)
val make_boolean_var : formula -> var * Formula_intf.negated val make_boolean_var : formula -> var * Formula_intf.negated
(** Returns the variable linked with the given formula, and wether the atom associated with the formula (** Returns the variable linked with the given formula, and whether the atom associated with the formula
is [var.pa] or [var.na] *) is [var.pa] or [var.na] *)
val empty_clause : clause val empty_clause : clause

19
src/msat.odocl
View file

@ -13,7 +13,6 @@ solver/Tseitin_intf
# Main modules # Main modules
core/Res core/Res
core/Res_intf
core/Internal core/Internal
core/External core/External
core/Solver_types core/Solver_types
@ -21,7 +20,6 @@ core/Solver_types
solver/Solver solver/Solver
solver/Mcsolver solver/Mcsolver
solver/Tseitin solver/Tseitin
solver/Tseitin_intf
# Backends # Backends
backend/Dot backend/Dot
@ -30,3 +28,20 @@ backend/Backend_intf
# Auxiliary # Auxiliary
util/Hashcons util/Hashcons
# SAT solver frontend
sat/Expr_sat
sat/Sat
sat/Type_sat
# SMT solver frontend
smt/Expr_smt
smt/Smt
smt/Type_smt
smt/Unionfind
# MCsat
mcsat/Eclosure
mcsat/Mcsat
mcsat/Plugin_mcsat

3
src/msat_sat.odocl
View file

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

17
src/msat_smt.odocl
View file

@ -1,17 +0,0 @@
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

515
src/smt/cc.ml
View file

@ -1,515 +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 *)
(* *)
(**************************************************************************)
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
View file

@ -1,37 +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 *)
(* *)
(**************************************************************************)
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

68
src/smt/explanation.ml
View file

@ -1,68 +0,0 @@
(**************************************************************************)
(* *)
(* 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
View file

@ -1,39 +0,0 @@
(**************************************************************************)
(* *)
(* 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

310
src/smt/uf.ml
View file

@ -1,310 +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 *)
(* *)
(**************************************************************************)
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 Ex = Explanation
module Sy = Symbols
module T = Term
module MapT = Term.Map
module SetT = Term.Set
module Lit = Literal.Make(T)
module MapL = Lit.Map
module MapR = MapT
module SetR = SetT
module R = struct
include T
type r = t
let leaves t : r list = match T.head t with
| T.Ite (a, _, _) -> [a]
| T.App (_, l) -> l
end
type r = R.r
module SetRR = Set.Make(struct
type t = r * r
let compare (r1, r1') (r2, r2') =
let c = T.compare r1 r2 in
if c <> 0 then c
else T.compare r1' r2'
end)
type t = {
(* term -> [t] *)
make : r MapT.t;
(* representative table *)
repr : (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 find_or_normal_form env r =
try MapR.find r env.repr with Not_found -> r, Ex.empty
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]

45
src/smt/uf.mli
View file

@ -1,45 +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 *)
(* *)
(**************************************************************************)
type answer = Yes of Explanation.t | No
type 'a literal =
| LSem of 'a Literal.view
| LTerm of Literal.LT.t
type t
type r
(** representative *)
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 * Explanation.t
val find_r : t -> r -> r * Explanation.t
val union :
t -> r -> r -> Explanation.t ->
t * (r * (r * r * Explanation.t) list * r) list
val distinct : t -> 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 list -> bool
val class_of : t -> Term.t -> Term.t list