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

Removed some old, unused legacy code

Browse source
This commit is contained in:
Guillaume Bury 2015-06-25 15:45:18 +02:00
parent 6f384fb80b
commit 898cfee53e
33 changed files with 0 additions and 5905 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
TODO.md
View file

@ -9,7 +9,6 @@
* react upon propagation (possibly by propagating more, or side-effect)
* more advanced/specific propagation (2-clauses)?
* implement 'constraints' (see https://www.lri.fr/~conchon/TER/2013/3/minisat.pdf )
- Adapt old code for theories, in order to plug it into new Solver Functor
## Long term goals

8
old/.merlin
View file

@ -1,8 +0,0 @@
S ./
S ../sat/
S ../common/
B ../_build/
B ../_build/sat/
B ../_build/smt/
B ../_build/common/

435
old/arith.ml
View file

@ -1,435 +0,0 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon, Alain Mebsout *)
(* Francois Bobot, Mohamed Iguernelala *)
(* Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
open Format
open Sig
open Num
module A = Literal
module Sy = Symbols
module T = Term
let ale = Hstring.make "<="
let alt = Hstring.make "<"
let is_le n = Hstring.compare n ale = 0
let is_lt n = Hstring.compare n alt = 0
let is_mult h = Sy.equal (Sy.Op Sy.Mult) h
let mod_symb = Sy.name (Hstring.make "@mod")
module Type (X:Sig.X) : Polynome.T with type r = X.r = struct
let mult _ _ = assert false
include Polynome.Make(struct include X let mult = mult end)
end
module Make
(X : Sig.X)
(P : Polynome.T with type r = X.r)
(C : Sig.C with type t = P.t and type r = X.r) = struct
type t = P.t
type r = P.r
let name = "arith"
let is_mine_a a =
match A.LT.view a with
| A.Builtin (_,p,_) -> is_le p || is_lt p
| _ -> false
let is_mine_symb = function
| Sy.Int _ | Sy.Real _
| Sy.Op (Sy.Plus | Sy.Minus | Sy.Mult | Sy.Div | Sy.Modulo) -> true
| _ -> false
let is_mine_type p =
let ty = P.type_info p in
ty = Ty.Tint || ty = Ty.Treal
let unsolvable _ = false
let empty_polynome ty = P.create [] (Int 0) ty
let is_mine p = match P.is_monomial p with
| Some (a,x,b) when a =/ (Int 1) && b =/ (Int 0) -> x
| _ -> C.embed p
let embed r = match C.extract r with
| Some p -> p
| _ -> P.create [Int 1, r] (Int 0) (X.type_info r)
let check_int exn p =
if P.type_info p = Ty.Tint then
let _, c = P.to_list p in
let ppmc = P.ppmc_denominators p in
if not (is_integer_num (ppmc */ c)) then raise exn
let fresh_string =
let cpt = ref 0 in
fun () ->
incr cpt;
"!k" ^ (string_of_int !cpt)
let fresh_name () =
T.make (Sy.name (Hstring.make (fresh_string()))) [] Ty.Tint
(* t1 % t2 = md <->
c1. 0 <= md ;
c2. md < t2 ;
c3. exists k. t1 = t2 * k + t ;
c4. t2 <> 0 (already checked) *)
let mk_modulo md t1 t2 ctx =
let zero = T.int "0" in
let c1 = A.LT.make (A.Builtin(true, ale, [zero; md])) in
let c2 = A.LT.make (A.Builtin(true, alt, [md; t2])) in
let k = fresh_name () in
let t3 = T.make (Sy.Op Sy.Mult) [t2;k] Ty.Tint in
let t3 = T.make (Sy.Op Sy.Plus) [t3;md] Ty.Tint in
let c3 = A.LT.make (A.Eq (t1, t3)) in
c3 :: c2 :: c1 :: ctx
let mk_euc_division p p2 t1 t2 ctx =
match P.to_list p2 with
| [], coef_p2 ->
let md = T.make (Sy.Op Sy.Modulo) [t1;t2] Ty.Tint in
let r, ctx' = X.make md in
let rp = P.mult (P.create [] ((Int 1) //coef_p2) Ty.Tint) (embed r) in
P.sub p rp, ctx' @ ctx
| _ -> assert false
let rec mke coef p t ctx =
let {T.f = sb ; xs = xs; ty = ty} = T.view t in
match sb, xs with
| (Sy.Int n | Sy.Real n), _ ->
let c = coef */ (num_of_string (Hstring.view n)) in
P.add (P.create [] c ty) p, ctx
| Sy.Op Sy.Mult, [t1;t2] ->
let p1, ctx = mke coef (empty_polynome ty) t1 ctx in
let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in
P.add p (P.mult p1 p2), ctx
| Sy.Op Sy.Div, [t1;t2] ->
let p1, ctx = mke coef (empty_polynome ty) t1 ctx in
let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in
let p3, ctx =
try
let p, approx = P.div p1 p2 in
if approx then mk_euc_division p p2 t1 t2 ctx
else p, ctx
with Division_by_zero | Polynome.Maybe_zero ->
P.create [coef, X.term_embed t] (Int 0) ty, ctx
in
P.add p p3, ctx
| Sy.Op Sy.Plus , [t1;t2] ->
let p2, ctx = mke coef p t2 ctx in
mke coef p2 t1 ctx
| Sy.Op Sy.Minus , [t1;t2] ->
let p2, ctx = mke (minus_num coef) p t2 ctx in
mke coef p2 t1 ctx
| Sy.Op Sy.Modulo , [t1;t2] ->
let p1, ctx = mke coef (empty_polynome ty) t1 ctx in
let p2, ctx = mke (Int 1) (empty_polynome ty) t2 ctx in
let p3, ctx =
try P.modulo p1 p2, ctx
with e ->
let t = T.make mod_symb [t1; t2] Ty.Tint in
let ctx = match e with
| Division_by_zero | Polynome.Maybe_zero -> ctx
| Polynome.Not_a_num -> mk_modulo t t1 t2 ctx
| _ -> assert false
in
P.create [coef, X.term_embed t] (Int 0) ty, ctx
in
P.add p p3, ctx
| _ ->
let a, ctx' = X.make t in
let ctx = ctx' @ ctx in
match C.extract a with
| Some p' -> P.add p (P.mult (P.create [] coef ty) p'), ctx
| _ -> P.add p (P.create [coef, a] (Int 0) ty), ctx
let arith_to_ac p = p
(*
match P.to_list p with
| [] , c -> p
| [Int 1, x] , Int 0 -> p
| l , c ->
let ty = P.type_info p in
let l =
List.fold_left
(fun acc (coef,x) ->
if coef =/ Int 0 then acc
else if coef =/ Int 1 || coef =/ Int (-1) then (coef,x)::acc
else match X.ac_extract x with
| Some ac when is_mult ac.h ->
let unit_coef, abs_coef =
if coef > Int 0 then Int 1, coef
else Int (-1), minus_num coef
in
let p_cst = is_mine (P.create [] abs_coef ty) in
let ac = {ac with l = Ac.add ac.h (p_cst, 1) ac.l} in
(unit_coef, X.ac_embed ac)::acc
| _ -> (coef,x)::acc
)[] l
in
P.create l c ty
*)
let make t =
let {T.ty = ty} = T.view t in
let p, ctx = mke (Int 1) (empty_polynome ty) t [] in
is_mine (arith_to_ac p), ctx
let rec expand p n acc =
assert (n >=0);
if n = 0 then acc else expand p (n-1) (p::acc)
let rec number_of_vars l =
List.fold_left (fun acc (r, n) -> acc + n * nb_vars_in_alien r) 0 l
and nb_vars_in_alien r =
match C.extract r with
| Some p ->
let l, _ = P.to_list p in
List.fold_left (fun acc (a, x) -> max acc (nb_vars_in_alien x)) 0 l
| None -> 1
let max_list_ = function
| [] -> 0
| [ _, x ] -> nb_vars_in_alien x
| (_, x) :: l ->
let acc = nb_vars_in_alien x in
List.fold_left (fun acc (_, x) -> max acc (nb_vars_in_alien x)) acc l
let type_info p = P.type_info p
let is_int r = X.type_info r = Ty.Tint
module XS = Set.Make(struct type t = X.r let compare = X.compare end)
let xs_of_list =
List.fold_left (fun s x -> XS.add x s) XS.empty
let rec leaves p =
let s =
List.fold_left
(fun s (_, a) -> XS.union (xs_of_list (X.leaves a)) s)
XS.empty (fst (P.to_list p))
in
XS.elements s
let subst x t p =
let p = P.subst x (embed t) p in
let ty = P.type_info p in
let l, c = P.to_list p in
let p =
List.fold_left
(fun p (ai, xi) ->
let xi' = X.subst x t xi in
let p' = match C.extract xi' with
| Some p' -> P.mult (P.create [] ai ty) p'
| _ -> P.create [ai, xi'] (Int 0) ty
in
P.add p p')
(P.create [] c ty) l
in
check_int (Exception.Unsolvable) p;
is_mine p
let compare = P.compare
let hash = P.hash
(* symmetric modulo p 131 *)
let mod_sym a b =
let m = mod_num a b in
let m =
if m </ Int 0 then
if m >=/ minus_num b then m +/ b else assert false
else
if m <=/ b then m else assert false
in
if m </ b // (Int 2) then m else m -/ b
let mult_const p c =
P.mult p (P.create [] c (P.type_info p))
let map_monomes f l ax =
List.fold_left
(fun acc (a,x) ->
let a = f a in if a =/ Int 0 then acc else (a, x) :: acc)
[ax] l
let apply_subst sb v =
is_mine (List.fold_left (fun v (x, p) -> embed (subst x p v)) v sb)
(* substituer toutes variables plus grandes que x *)
let subst_bigger x l =
List.fold_left
(fun (l, sb) (b, y) ->
if X.compare y x > 0 then
let k = X.term_embed (fresh_name ()) in
(b, k) :: l, (y, embed k)::sb
else (b, y) :: l, sb)
([], []) l
let is_mine_p = List.map (fun (x,p) -> x, is_mine p)
let extract_min = function
| [] -> assert false
| [c] -> c, []
| (a, x) :: s ->
List.fold_left
(fun ((a, x), l) (b, y) ->
if abs_num a <=/ abs_num b then
(a, x), ((b, y) :: l)
else (b, y), ((a, x):: l)) ((a, x),[]) s
(* Decision Procedures. Page 131 *)
let rec omega l b =
(* 1. choix d'une variable donc le |coef| est minimal *)
let (a, x), l = extract_min l in
(* 2. substituer les aliens plus grand que x pour
assurer l'invariant sur l'ordre AC *)
let l, sbs = subst_bigger x l in
let p = P.create l b Ty.Tint in
match a with
| Int 0 -> assert false
| Int 1 ->
(* 3.1. si a = 1 alors on a une substitution entiere pour x *)
let p = mult_const p (Int (-1)) in
(x, is_mine p) :: (is_mine_p sbs)
| Int (-1) ->
(* 3.2. si a = -1 alors on a une subst entiere pour x*)
(x,is_mine p) :: (is_mine_p sbs)
| _ ->
(* 4. sinon, (|a| <> 1) et a <> 0 *)
(* 4.1. on rend le coef a positif s'il ne l'est pas deja *)
let a, l, b =
if compare_num a (Int 0) < 0 then
(minus_num a,
List.map (fun (a,x) -> minus_num a,x) l, (minus_num b))
else (a, l, b)
in
(* 4.2. on reduit le systeme *)
omega_sigma sbs a x l b
and omega_sigma sbs a x l b =
(* 1. on definie m qui vaut a + 1 *)
let m = a +/ Int 1 in
(* 2. on introduit une variable fraiche *)
let sigma = X.term_embed (fresh_name ()) in
(* 3. l'application de la formule (5.63) nous donne la valeur du pivot x*)
let mm_sigma = (minus_num m, sigma) in
let l_mod = map_monomes (fun a -> mod_sym a m) l mm_sigma in
(* 3.1. Attention au signe de b :
on le passe a droite avant de faire mod_sym, d'ou minus_num *)
let b_mod = minus_num (mod_sym (minus_num b) m) in
let p = P.create l_mod b_mod Ty.Tint in
let sbs = (x, p) :: sbs in
(* 4. on substitue x par sa valeur dans l'equation de depart.
Voir la formule (5.64) *)
let p' = P.add (P.mult_const a p) (P.create l b Ty.Tint) in
(* 5. on resoud sur l'equation simplifiee *)
let sbs2 = solve_int p' in
(* 6. on normalise sbs par sbs2 *)
let sbs = List.map (fun (x, v) -> x, apply_subst sbs2 v) sbs in
(* 7. on supprime les liaisons inutiles de sbs2 et on merge avec sbs *)
let sbs2 = List.filter (fun (y, _) -> y <> sigma) sbs2 in
List.rev_append sbs sbs2
and solve_int p =
if P.is_empty p then raise Not_found;
let pgcd = P.pgcd_numerators p in
let ppmc = P.ppmc_denominators p in
let p = mult_const p (ppmc // pgcd) in
let l, b = P.to_list p in
if not (is_integer_num b) then raise Exception.Unsolvable;
omega l b
let is_null p =
if snd (P.to_list p) <>/ (Int 0) then raise Exception.Unsolvable;
[]
let solve_int p =
try solve_int p with Not_found -> is_null p
let solve_real p =
try
let a, x = P.choose p in
let p =
P.mult
(P.create [] ((Int (-1)) // a) (P.type_info p))
(P.remove x p)
in
[x, is_mine p]
with Not_found -> is_null p
let safe_distribution p =
let l, c = P.to_list p in
let ty = P.type_info p in
List.fold_left
(fun p (coef, x) -> P.add p (P.create [coef,x] (Int 0) ty))
(P.create [] c ty) l
let solve_aux r1 r2 =
let p1 = embed r1 in
let p2 = embed r2 in
let ty = P.type_info p2 in
let p = P.add p1 (P.mult (P.create [] (Int (-1)) ty) p2) in
let pp = safe_distribution p in
if ty = Ty.Treal then solve_real pp else solve_int pp
let solve r1 r2 =
let sbs = solve_aux r1 r2 in
List.fast_sort (fun (a,_) (x,y) -> X.compare x a) sbs
let print = P.print
let fully_interpreted sb =
match sb with
| Sy.Op (Sy.Plus | Sy.Minus) -> true
| _ -> false
let term_extract _ = None
module Rel = Fm.Make (X)
(struct
include P
let poly_of = embed
let alien_of = is_mine
end)
end

21
old/arith.mli
View file

@ -1,21 +0,0 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon, Alain Mebsout *)
(* Francois Bobot, 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 (X : Sig.X ): Polynome.T with type r = X.r
module Make
(X : Sig.X)
(P : Polynome.T with type r = X.r)
(C : Sig.C with type t = P.t and type r = X.r) : Sig.THEORY
with type r = X.r and type t = P.t

524
old/cc.ml
View file

@ -1,524 +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 Format
open Sig
open Exception
let max_split = Num.Int 1000000
let cc_active = ref true
module type S = sig
type t
module TimerCC : Timer.S
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 (X : Sig.X) = struct
module TimerCC = Timer.Make(struct end)
module Ex = Explanation
module SetA = Use.SA
module Use = Use.Make(X)
module Uf = Uf.Make(X)
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 = {
use : Use.t;
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 (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

29
old/cc.mli
View file

@ -1,29 +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 *)
(* *)
(**************************************************************************)
val cc_active : bool ref
module type S = sig
type t
module TimerCC : Timer.S
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 -> Sig.answer
val class_of : t -> Term.t -> Term.t list
end
module Make (X:Sig.X) : S

253
old/combine.ml
View file

@ -1,253 +0,0 @@
(**************************************************************************)
(* *)
(* 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 Format
open Sig
module rec CX : sig
include Sig.X
val extract1 : r -> X1.t option
val embed1 : X1.t -> r
val extract5 : r -> X5.t option
val embed5 : X5.t -> r
end =
struct
type r =
| Term of Term.t
| X1 of X1.t
| X5 of X5.t
let extract1 = function X1 r -> Some r | _ -> None
let extract5 = function X5 r -> Some r | _ -> None
let embed1 x = X1 x
let embed5 x = X5 x
let is_int v =
let ty = match v with
| X1 x -> X1.type_info x
| X5 x -> X5.type_info x
| Term t -> (Term.view t).Term.ty
in
ty = Ty.Tint
let rec compare a b =
let c = compare_tag a b in
if c = 0 then comparei a b else c
and compare_tag a b =
Pervasives.compare (theory_num a) (theory_num b)
and comparei a b =
match a, b with
| X1 x, X1 y -> X1.compare x y
| X5 x, X5 y -> X5.compare x y
| Term x , Term y -> Term.compare x y
| _ -> assert false
and theory_num x = Obj.tag (Obj.repr x)
let equal a b = compare a b = 0
let hash = function
| Term t -> Term.hash t
| X1 x -> X1.hash x
| X5 x -> X5.hash x
module MR = Map.Make(struct type t = r let compare = compare end)
let print fmt r =
match r with
| X1 t -> fprintf fmt "%a" X1.print t
| X5 t -> fprintf fmt "%a" X5.print t
| Term t -> fprintf fmt "%a" Term.print t
let leaves r =
match r with
| X1 t -> X1.leaves t
| X5 t -> X5.leaves t
| Term _ -> [r]
let term_embed t = Term t
let term_extract r =
match r with
| X1 _ -> X1.term_extract r
| X5 _ -> X5.term_extract r
| Term t -> Some t
let subst p v r =
if equal p v then r
else match r with
| X1 t -> X1.subst p v t
| X5 t -> X5.subst p v t
| Term _ -> if equal p r then v else r
let make t =
let {Term.f=sb} = Term.view t in
match X1.is_mine_symb sb, X5.is_mine_symb sb with
| true, false -> X1.make t
| false, true -> X5.make t
| false, false -> Term t, []
| _ -> assert false
let fully_interpreted sb =
match X1.is_mine_symb sb, X5.is_mine_symb sb with
| true, false -> X1.fully_interpreted sb
| false, true -> X5.fully_interpreted sb
| false, false -> false
| _ -> assert false
let add_mr =
List.fold_left
(fun solved (p,v) ->
MR.add p (v::(try MR.find p solved with Not_found -> [])) solved)
let unsolvable = function
| X1 x -> X1.unsolvable x
| X5 x -> X5.unsolvable x
| Term _ -> true
let partition tag =
List.partition
(fun (u,t) ->
(theory_num u = tag || unsolvable u) &&
(theory_num t = tag || unsolvable t))
let rec solve_list solved l =
List.fold_left
(fun solved (a,b) ->
let cmp = compare a b in
if cmp = 0 then solved else
match a , b with
(* both sides are empty *)
| Term _ , Term _ ->
add_mr solved (unsolvable_values cmp a b)
(* only one side is empty *)
| (a, b)
when unsolvable a || unsolvable b || compare_tag a b = 0 ->
let a,b = if unsolvable a then b,a else a,b in
let cp , sol = partition (theory_num a) (solvei b a) in
solve_list (add_mr solved cp) sol
(* both sides are not empty *)
| a , b -> solve_theoryj solved a b
) solved l
and unsolvable_values cmp a b =
match a, b with
(* Clash entre theories: On peut avoir ces pbs ? *)
| X1 _, X5 _
| X5 _, X1 _
-> assert false
(* theorie d'un cote, vide de l'autre *)
| X1 _, _ | _, X1 _ -> X1.solve a b
| X5 _, _ | _, X5 _ -> X5.solve a b
| Term _, Term _ -> [if cmp > 0 then a,b else b,a]
and solve_theoryj solved xi xj =
let cp , sol = partition (theory_num xj) (solvei xi xj) in
solve_list (add_mr solved cp) (List.rev_map (fun (x,y) -> y,x) sol)
and solvei a b =
match b with
| X1 _ -> X1.solve a b
| X5 _ -> X5.solve a b
| Term _ -> assert false
let rec solve_rec mt ab =
let mr = solve_list mt ab in
let mr , ab =
MR.fold
(fun p lr ((mt,ab) as acc) -> match lr with
[] -> assert false
| [_] -> acc
| x::lx ->
MR.add p [x] mr , List.rev_map (fun y-> (x,y)) lx)
mr (mr,[])
in
if ab = [] then mr else solve_rec mr ab
let solve a b =
MR.fold
(fun p lr ret ->
match lr with [r] -> (p ,r)::ret | _ -> assert false)
(solve_rec MR.empty [a,b]) []
let rec type_info = function
| X1 t -> X1.type_info t
| X5 t -> X5.type_info t
| Term t -> let {Term.ty = ty} = Term.view t in ty
module Rel = struct
type elt = r
type r = elt
type t = {
r1: X1.Rel.t;
r5: X5.Rel.t;
}
let empty _ = {
r1=X1.Rel.empty ();
r5=X5.Rel.empty ();
}
let assume env sa =
let env1, { assume = a1; remove = rm1} = X1.Rel.assume env.r1 sa in
let env5, { assume = a5; remove = rm5} = X5.Rel.assume env.r5 sa in
{r1=env1; r5=env5},
{ assume = a1@a5; remove = rm1@rm5;}
let query env a =
match X1.Rel.query env.r1 a with
| Yes _ as ans -> ans
| No -> X5.Rel.query env.r5 a
let case_split env =
let seq1 = X1.Rel.case_split env.r1 in
let seq5 = X5.Rel.case_split env.r5 in
seq1 @ seq5
let add env r =
{r1=X1.Rel.add env.r1 r;
r5=X5.Rel.add env.r5 r }
end
end
and TX1 : Polynome.T with type r = CX.r = Arith.Type(CX)
and X1 : Sig.THEORY with type t = TX1.t and type r = CX.r =
Arith.Make(CX)(TX1)
(struct
type t = TX1.t
type r = CX.r
let extract = CX.extract1
let embed = CX.embed1
let assume env _ _ = env, {Sig.assume = []; remove = []}
end)
and X5 : Sig.THEORY with type r = CX.r and type t = CX.r Sum.abstract =
Sum.Make
(struct
include CX
let extract = extract5
let embed = embed5
end)

14
old/combine.mli
View file

@ -1,14 +0,0 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
module CX : Sig.X

19
old/exception.ml
View file

@ -1,19 +0,0 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
exception Unsolvable
exception Inconsistent of Explanation.t
exception Progress
exception NotCongruent
exception Trivial
exception Interpreted_Symbol

19
old/exception.mli
View file

@ -1,19 +0,0 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
exception Unsolvable
exception Inconsistent of Explanation.t
exception Progress
exception NotCongruent
exception Trivial
exception Interpreted_Symbol

806
old/fm.ml
View file

@ -1,806 +0,0 @@
(**************************************************************************)
(* *)
(* 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 Num
open Format
open Sig
let ale = Hstring.make "<="
let alt = Hstring.make "<"
let is_le n = Hstring.compare n ale = 0
let is_lt n = Hstring.compare n alt = 0
let (-@) l1 l2 = List.rev_append l1 l2
module L = Literal
module Sy = Symbols
exception NotConsistent of Literal.LT.Set.t
module type EXTENDED_Polynome = sig
include Polynome.T
val poly_of : r -> t
val alien_of : t -> r
end
module Make
(X : Sig.X)
(P : EXTENDED_Polynome with type r = X.r) = struct
module MP = Map.Make(P)
module SP = Set.Make(P)
module SX = Set.Make(struct type t = X.r include X end)
module MX = Map.Make(struct type t = X.r include X end)
type r = P.r
module LR = Literal.Make(struct type t = X.r include X end)
module Seq =
Set.Make
(struct
type t = r L.view * L.LT.t option * Explanation.t
let compare (a, _, _) (b, _, _) =
LR.compare (LR.make a) (LR.make b)
end)
module Inequation = struct
type t = {
ple0 : P.t;
is_le : bool;
dep : (Literal.LT.t * num * P.t * bool) list;
expl : Explanation.t
}
let print fmt ineq = fprintf fmt "%a %s 0" P.print ineq.ple0
(if ineq.is_le then "<=" else "<")
let create p1 p2 is_le a expl =
let p = P.add p1 (P.mult (P.create [] (Int (-1)) (P.type_info p1)) p2) in
{ ple0 = p; is_le = is_le; dep = [a, Int 1, p, is_le]; expl = expl }
let choose ineq = snd (P.choose ineq.ple0)
let find x ineq = P.find x ineq.ple0
let is_monomial ineq = P.is_monomial ineq.ple0
let pos_neg mx { ple0 = p } =
List.fold_left (fun m (c,x) ->
let cmp = compare_num c (Int 0) in
if cmp = 0 then m
else
let (pos, neg) = try MX.find x m with Not_found -> (0,0) in
if cmp > 0 then MX.add x (pos+1, neg) m
else MX.add x (pos, neg+1) m ) mx (fst (P.to_list p))
end
type t = {
inequations : (Literal.LT.t * Inequation.t) list ;
monomes: (Intervals.t * SX.t) MX.t;
polynomes : Intervals.t MP.t;
known_eqs : SX.t;
improved : SP.t;
}
module Debug = struct
let list_of_ineqs fmt = List.iter (fprintf fmt "%a " Inequation.print)
let assume a = ()
let cross x cpos cneg others ninqs = ()
let print_use fmt use =
SX.iter (fprintf fmt "%a, " X.print) use
let env env = ()
let implied_equalities l = ()
end
let empty _ = {
inequations = [] ;
monomes = MX.empty ;
polynomes = MP.empty ;
known_eqs = SX.empty ;
improved = SP.empty ;
}
let replace_inequation env x ineq =
{ env with
inequations = (x, ineq)::(List.remove_assoc x env.inequations) }
let up_improved env p oldi newi =
if Intervals.is_strict_smaller newi oldi then
{ env with improved = SP.add p env.improved }
else env
(*
let oldify_inequations env =
{ env with
inequations = env.inequations@env.new_inequations;
new_inequations = [] } *)
let mult_bornes_vars vars monomes ty=
List.fold_left
(fun ui (y,n) ->
let ui' = try
fst (MX.find y monomes)
with Not_found -> Intervals.undefined ty
in
Intervals.mult ui (Intervals.power n ui')
) (Intervals.point (Int 1) ty Explanation.empty) vars
let intervals_from_monomes env p =
let pl, v = P.to_list p in
List.fold_left
(fun i (a, x) ->
let i_x, _ = MX.find x env.monomes in
Intervals.add (Intervals.scale a i_x) i
) (Intervals.point v (P.type_info p) Explanation.empty) pl
let rec add_monome expl use_x env x =
try
let u, old_use_x = MX.find x env.monomes in
{ env with monomes = MX.add x (u, SX.union old_use_x use_x) env.monomes }
with Not_found ->
update_monome expl use_x env x
and init_monomes env p use_p expl =
List.fold_left
(fun env (_, x) -> add_monome expl use_p env x)
env (fst (P.to_list p))
and init_alien expl p (normal_p, c, d) ty use_x env =
let env = init_monomes env p use_x expl in
let i = intervals_from_monomes env p in
let i =
try
let old_i = MP.find normal_p env.polynomes in
let old_i = Intervals.scale d
(Intervals.add old_i (Intervals.point c ty Explanation.empty)) in
Intervals.intersect i old_i
with Not_found -> i
in
env, i
and update_monome expl use_x env x =
let ty = X.type_info x in
let ui, env =
match X.term_extract x with
| Some t ->
let use_x = SX.singleton x in
begin
match Term.view t with
| {Term.f = (Sy.Op Sy.Div); xs = [a; b]} ->
let pa = P.poly_of (fst (X.make a)) in
let pb = P.poly_of (fst (X.make b)) in
let (pa', ca, da) as npa = P.normal_form_pos pa in
let (pb', cb, db) as npb = P.normal_form_pos pb in
let env, ia = init_alien expl pa npa ty use_x env in
let env, ib = init_alien expl pb npb ty use_x env in
let ia, ib = match Intervals.doesnt_contain_0 ib with
| Yes ex when Num.compare_num ca cb = 0
&& P.compare pa' pb' = 0 ->
let expl = Explanation.union ex expl in
Intervals.point da ty expl, Intervals.point db ty expl
| _ -> ia, ib
in
Intervals.div ia ib, env
| _ -> Intervals.undefined ty, env
end
| _ -> Intervals.undefined ty, env
in
let u, use_x' =
try MX.find x env.monomes
with Not_found -> Intervals.undefined (X.type_info x), use_x in
let ui = Intervals.intersect ui u in
{ env with monomes = MX.add x (ui, (SX.union use_x use_x')) env.monomes }
and tighten_div x env expl = env
and tighten_non_lin x use_x env expl =
let env = tighten_div x env expl in
SX.fold
(fun x acc ->
let _, use = MX.find x acc.monomes in
update_monome expl use acc x)
use_x env
let update_monomes_from_poly p i polynomes monomes =
let lp, _ = P.to_list p in
let ty = P.type_info p in
List.fold_left (fun monomes (a,x) ->
let np = P.remove x p in
let (np,c,d) = P.normal_form_pos np in
try
let inp = MP.find np polynomes in
let new_ix =
Intervals.scale
((Int 1) // a)
(Intervals.add i
(Intervals.scale (minus_num d)
(Intervals.add inp
(Intervals.point c ty Explanation.empty)))) in
let old_ix, ux = MX.find x monomes in
let ix = Intervals.intersect old_ix new_ix in
MX.add x (ix, ux) monomes
with Not_found -> monomes)
monomes lp
let update_polynomes env expl =
let polynomes, monomes, improved = MP.fold
(fun p ip (polynomes, monomes, improved) ->
let new_i = intervals_from_monomes env p in
let i = Intervals.intersect new_i ip in
if Intervals.is_strict_smaller i ip then
let monomes = update_monomes_from_poly p i polynomes monomes in
let improved = SP.add p improved in
MP.add p i polynomes, monomes, improved
else polynomes, monomes, improved
) env.polynomes (env.polynomes, env.monomes, env.improved) in
{env with polynomes = polynomes; monomes = monomes ; improved = improved}
let find_one_eq x u =
match Intervals.is_point u with
| Some (v, ex) when X.type_info x <> Ty.Tint || is_integer_num v ->
let eq =
L.Eq (x,(P.alien_of (P.create [] v (X.type_info x)))) in
Some (eq, None, ex)
| _ -> None
let find_eq eqs x u env =
match find_one_eq x u with
| None -> eqs
| Some eq1 -> eq1::eqs
type ineq_status =
| Trivial_eq
| Trivial_ineq of num
| Bottom
| Monome of num * P.r * num
| Other
let ineq_status ({Inequation.ple0 = p ; is_le = is_le} as ineq) =
match Inequation.is_monomial ineq with
Some (a, x, v) -> Monome (a, x, v)
| None ->
if P.is_empty p then
let _, v = P.to_list p in
let c = compare_num v (Int 0) in
if c > 0 || (c >=0 && not is_le) then Bottom
else
if c = 0 && is_le then Trivial_eq
else Trivial_ineq v
else Other
(*let ineqs_from_dep dep borne_inf is_le =
List.map
(fun {poly_orig = p; coef = c} ->
let (m,v,ty) = P.mult_const minusone p in
(* quelle valeur pour le ?????? *)
{ ple0 = {poly = (m, v +/ (borne_inf // c), ty); le = is_le} ;
dep = []}
)dep*)
let mk_equality p =
let r1 = P.alien_of p in
let r2 = P.alien_of (P.create [] (Int 0) (P.type_info p)) in
L.Eq (r1, r2)
let fm_equalities env eqs { Inequation.ple0 = p; dep = dep; expl = ex } =
let inqs, eqs =
List.fold_left
(fun (inqs, eqs) (a, _, p, _) ->
List.remove_assoc a inqs, (mk_equality p, Some a, ex) :: eqs
) (env.inequations, eqs) dep
in
{ env with inequations = inqs }, eqs
let update_intervals env eqs expl (a, x, v) is_le =
let uints, use_x = MX.find x env.monomes in
let b = ((Int (-1)) */ v) // a in
let u =
if a >/ (Int 0) then
Intervals.new_borne_sup expl b is_le uints
else
Intervals.new_borne_inf expl b is_le uints in
let env = { env with monomes = MX.add x (u, use_x) env.monomes } in
let env = tighten_non_lin x use_x env expl in
env, (find_eq eqs x u env)
let update_ple0 env p0 is_le expl =
if P.is_empty p0 then env
else
let ty = P.type_info p0 in
let a, _ = P.choose p0 in
let p, change =
if a </ Int 0 then
P.mult (P.create [] (Int (-1)) ty) p0, true
else p0, false in
let p, c, _ = P.normal_form p in
let c = minus_num c in
let u =
if change then
Intervals.new_borne_inf expl c is_le (Intervals.undefined ty)
else
Intervals.new_borne_sup expl c is_le (Intervals.undefined ty) in
let u, pu =
try
let pu = MP.find p env.polynomes in
let i = Intervals.intersect u pu in
i, pu
with Not_found -> u, Intervals.undefined ty
in
let env =
if Intervals.is_strict_smaller u pu then
let polynomes = MP.add p u env.polynomes in
let monomes = update_monomes_from_poly p u polynomes env.monomes in
let improved = SP.add p env.improved in
{ env with
polynomes = polynomes;
monomes = monomes;
improved = improved }
else env
in
match P.to_list p0 with
| [a,x], v -> fst(update_intervals env [] expl (a, x, v) is_le)
| _ -> env
let add_inequations acc lin expl =
List.fold_left
(fun (env, eqs) ineq ->
(* let expl = List.fold_left
(fun expl (l,_,_,_) ->
Explanation.union (*Explanation.everything*)
(Explanation.singleton (Formula.mk_lit l))
expl
) expl ineq.Inequation.dep
in *)
let expl = Explanation.union ineq.Inequation.expl expl in
match ineq_status ineq with
| Bottom ->
raise (Exception.Inconsistent expl)
| Trivial_eq ->
fm_equalities env eqs ineq
| Trivial_ineq c ->
let n, pp =
List.fold_left
(fun ((n, pp) as acc) (_, _, p, is_le) ->
if is_le then acc else
match pp with
| Some _ -> n+1, None
| None when n=0 -> 1, Some p
| _ -> n+1, None) (0,None) ineq.Inequation.dep
in
let env =
List.fold_left
(fun env (_, coef, p, is_le) ->
let ty = P.type_info p in
let is_le =
match pp with
Some x -> P.compare x p = 0 | _ -> is_le && n=0
in
let p' = P.sub (P.create [] (c // coef) ty) p in
update_ple0 env p' is_le expl
) env ineq.Inequation.dep
in
env, eqs
| Monome (a, x, v) ->
let env, eqs =
update_intervals env eqs expl (a, x, v) ineq.Inequation.is_le
in
(*let env,eqs = update_bornes env eqs ((a,x),c) ineq.ple0.le in
let env,eqs = update_polynomes env eqs ineq in
env, pers_ineqs, eqs*)
env, eqs
| Other ->
env, eqs
(*t env,eqs = update_polynomes env eqs ineq in
env, pers_ineqs, eqs*)
) acc lin
let mult_list c =
List.map (fun (a, coef, p, is_le) -> (a, coef */ c, p, is_le))
let div_by_pgcd (a, b) ty =
try
if ty = Ty.Tint then
let p = Big_int.gcd_big_int (big_int_of_num a) (big_int_of_num b) in
let p = num_of_big_int p in
a // p, b // p
else a, b
with Failure "big_int_of_ratio" -> a, b
let cross x cpos cneg =
let rec cross_rec acc = function
| [] -> acc
| { Inequation.ple0 = p1; is_le = k1; dep = d1; expl = ex1 } :: l ->
let n1 = abs_num (P.find x p1) in
(* let ty = P.type_info p1 in *)
let acc =
List.fold_left
(fun acc {Inequation.ple0 = p2; is_le = k2; dep=d2; expl = ex2} ->
let n2 = abs_num (P.find x p2) in
(* let n1, n2 = div_by_pgcd (n1, n2) ty in *)
let p = P.add
(P.mult (P.create [] n2 (P.type_info p2)) p1)
(P.mult (P.create [] n1 (P.type_info p1)) p2) in
let d1 = mult_list n2 d1 in
let d2 = mult_list n1 d2 in
let ni =
{ Inequation.ple0 = p; is_le = k1&&k2; dep = d1 -@ d2;
expl = Explanation.union ex1 ex2 }
in
ni::acc
) acc cpos
in
cross_rec acc l
in
cross_rec [] cneg
let split x l =
let rec split_rec (cp, cn, co) ineq =
try
let a = Inequation.find x ineq in
if a >/ (Int 0) then ineq::cp, cn, co
else cp, ineq::cn, co
with Not_found -> cp, cn, ineq::co
in
List.fold_left split_rec ([], [], []) l
let length s = SX.fold (fun _ acc -> acc+1) s 0
let choose_var l =
let pos_neg = List.fold_left Inequation.pos_neg MX.empty l in
let xopt = MX.fold (fun x (pos, neg) acc ->
match acc with
| None -> Some (x, pos * neg)
| Some (y, c') ->
let c = pos * neg in
if c < c' then Some (x, c) else acc
) pos_neg None in
match xopt with
| Some (x, _) -> x
| None -> raise Not_found
let rec fourier ( (env, eqs) as acc) l expl =
match l with
| [] -> acc
| ineq :: l' ->
try
(* let x = Inequation.choose ineq in *)
let x = choose_var l in
let cpos, cneg, others = split x l in
let ninqs = cross x cpos cneg in
Debug.cross x cpos cneg others ninqs;
let acc = add_inequations acc cpos expl in
let acc = add_inequations acc cneg expl in
fourier acc (ninqs -@ others) expl
with Not_found -> add_inequations acc l expl
(*
let fm env eqs expl =
fourier (env, eqs)
(List.map snd env.inequations)
(List.map snd env.new_inequations) expl
*)
let fm env eqs expl =
fourier (env, eqs) (List.map snd env.inequations) expl
let is_num r =
let ty = X.type_info r in ty = Ty.Tint || ty = Ty.Treal
let add_disequality env eqs p expl =
let ty = P.type_info p in
match P.to_list p with
| ([], (Int 0)) ->
raise (Exception.Inconsistent expl)
| ([], v) ->
env, eqs
| ([a, x], v) ->
let b = (minus_num v) // a in
let i1 = Intervals.point b ty expl in
let i2, use2 =
try
MX.find x env.monomes
with Not_found -> Intervals.undefined ty, SX.empty
in
let i = Intervals.exclude i1 i2 in
let env ={ env with monomes = MX.add x (i,use2) env.monomes } in
let env = tighten_non_lin x use2 env expl in
env, find_eq eqs x i env
| _ ->
let a, _ = P.choose p in
let p = if a >=/ Int 0 then p
else P.mult (P.create [] (Int (-1)) ty) p in
let p, c, _ = P.normal_form p in
let i1 = Intervals.point (minus_num c) ty expl in
let i2 =
try
MP.find p env.polynomes
with Not_found -> Intervals.undefined ty
in
let i = Intervals.exclude i1 i2 in
let env =
if Intervals.is_strict_smaller i i2 then
let polynomes = MP.add p i env.polynomes in
let monomes = update_monomes_from_poly p i polynomes env.monomes
in
let improved = SP.add p env.improved in
{ env with
polynomes = polynomes;
monomes = monomes;
improved = improved}
else env
in
env, eqs
let add_equality env eqs p expl =
let ty = P.type_info p in
match P.to_list p with
| ([], Int 0) -> env, eqs
| ([], v) ->
raise (Exception.Inconsistent expl)
| ([a, x], v) ->
let b = (minus_num v) // a in
let i = Intervals.point b ty expl in
let i, use =
try
let i', use' = MX.find x env.monomes in
Intervals.intersect i i', use'
with Not_found -> i, SX.empty
in
let env = { env with monomes = MX.add x (i, use) env.monomes} in
let env = tighten_non_lin x use env expl in
env, find_eq eqs x i env
| _ ->
let a, _ = P.choose p in
let p = if a >=/ Int 0 then p
else P.mult (P.create [] (Int (-1)) ty) p in
let p, c, _ = P.normal_form p in
let i = Intervals.point (minus_num c) ty expl in
let i, ip =
try
let ip = MP.find p env.polynomes in
Intervals.intersect i ip, ip
with Not_found -> i, Intervals.undefined ty
in
let env =
if Intervals.is_strict_smaller i ip then
let polynomes = MP.add p i env.polynomes in
let monomes = update_monomes_from_poly p i polynomes env.monomes
in
let improved = SP.add p env.improved in
{ env with
polynomes = polynomes;
monomes = monomes;
improved = improved }
else env
in
let env =
{ env with
known_eqs = SX.add (P.alien_of p) env.known_eqs
} in
env, eqs
let normal_form a = match a with
| L.Builtin (false, n, [r1; r2]) when is_le n && X.type_info r1 = Ty.Tint ->
let pred_r1 = P.sub (P.poly_of r1) (P.create [] (Int 1) Ty.Tint) in
L.Builtin (true, n, [r2; P.alien_of pred_r1])
| L.Builtin (true, n, [r1; r2]) when
not (is_le n) && X.type_info r1 = Ty.Tint ->
let pred_r2 = P.sub (P.poly_of r2) (P.create [] (Int 1) Ty.Tint) in
L.Builtin (true, ale, [r1; P.alien_of pred_r2])
| L.Builtin (false, n, [r1; r2]) when is_le n ->
L.Builtin (true, alt, [r2; r1])
| L.Builtin (false, n, [r1; r2]) when is_lt n ->
L.Builtin (true, ale, [r2; r1])
| _ -> a
let remove_trivial_eqs eqs la =
let set_of l =
List.fold_left (fun s e -> Seq.add e s) Seq.empty l
in
Seq.elements (Seq.diff (set_of eqs) (set_of la))
let equalities_from_polynomes env eqs =
let known, eqs =
MP.fold
(fun p i (knw, eqs) ->
let xp = P.alien_of p in
if SX.mem xp knw then knw, eqs
else
match Intervals.is_point i with
| Some (num, ex) ->
let r2 = P.alien_of (P.create [] num (P.type_info p)) in
SX.add xp knw, (L.Eq(xp, r2), None, ex) :: eqs
| None -> knw, eqs
) env.polynomes (env.known_eqs, eqs)
in {env with known_eqs= known}, eqs
let equalities_from_monomes env eqs =
let known, eqs =
MX.fold
(fun x (i,_) (knw, eqs) ->
if SX.mem x knw then knw, eqs
else
match Intervals.is_point i with
| Some (num, ex) ->
let r2 = P.alien_of (P.create [] num (X.type_info x)) in
SX.add x knw, (L.Eq(x, r2), None, ex) :: eqs
| None -> knw, eqs
) env.monomes (env.known_eqs, eqs)
in {env with known_eqs= known}, eqs
let equalities_from_intervals env eqs =
let env, eqs = equalities_from_polynomes env eqs in
equalities_from_monomes env eqs
let assume env la =
let env = {env with improved = SP.empty} in
Debug.env env;
let env, eqs, new_ineqs, expl =
List.fold_left
(fun (env, eqs, new_ineqs, expl) (a, root, e) ->
let a = normal_form a in
let expl = Explanation.union e expl in
try
match a with
| L.Builtin(_, n, [r1;r2]) when is_le n || is_lt n ->
let root = match root with
| Some a -> a | None -> assert false in
let p1 = P.poly_of r1 in
let p2 = P.poly_of r2 in
let ineq = Inequation.create p1 p2 (is_le n) root expl in
let env =
init_monomes env ineq.Inequation.ple0 SX.empty expl in
let env =
update_ple0 env ineq.Inequation.ple0 (is_le n) expl in
let env = replace_inequation env root ineq in
env, eqs, true, expl
| L.Distinct (false, [r1; r2]) when is_num r1 && is_num r2 ->
let p = P.sub (P.poly_of r1) (P.poly_of r2) in
let env = init_monomes env p SX.empty expl in
let env, eqs = add_disequality env eqs p expl in
env, eqs, new_ineqs, expl
| L.Eq(r1, r2) when is_num r1 && is_num r2 ->
let p = P.sub (P.poly_of r1) (P.poly_of r2) in
let env = init_monomes env p SX.empty expl in
let env, eqs = add_equality env eqs p expl in
env, eqs, new_ineqs, expl
| _ -> (env, eqs, new_ineqs, expl)
with Intervals.NotConsistent expl ->
raise (Exception.Inconsistent expl)
)
(env, [], false, Explanation.empty) la
in
if new_ineqs then
if false then
();
try
(* we only call fm when new ineqs are assumed *)
let env, eqs = if new_ineqs then fm env eqs expl else env, eqs in
(* let env = oldify_inequations env in *)
let env = update_polynomes env expl in
let env, eqs = equalities_from_intervals env eqs in
Debug.env env;
let eqs = remove_trivial_eqs eqs la in
Debug.implied_equalities eqs;
let result =
List.fold_left
(fun r (a_sem, a_term, ex) ->
{ assume = (LSem(a_sem), ex) :: r.assume;
remove =
match a_term with
| None -> r.remove
| Some t -> (LTerm(t), ex)::r.remove
} ) { assume = []; remove = [] } eqs
in
env, result
with Intervals.NotConsistent expl ->
raise (Exception.Inconsistent expl)
let query env a_ex =
try
ignore(assume env [a_ex]);
No
with Exception.Inconsistent expl -> Yes expl
let case_split_polynomes env =
let o = MP.fold
(fun p i o ->
match Intervals.finite_size i with
| Some s when s >/ (Int 1) ->
begin
match o with
| Some (s', _, _, _) when s' <=/ s -> o
| _ ->
let n, ex = Intervals.borne_inf i in
Some (s, p, n, ex)
end
| _ -> o
) env.polynomes None in
match o with
| Some (s, p, n, ex) ->
let r1 = P.alien_of p in
let r2 = P.alien_of (P.create [] n (P.type_info p)) in
[L.Eq(r1, r2), ex, s]
| None ->
[]
let case_split_monomes env =
let o = MX.fold
(fun x (i,_) o ->
match Intervals.finite_size i with
| Some s when s >/ (Int 1) ->
begin
match o with
| Some (s', _, _, _) when s' <=/ s -> o
| _ ->
let n, ex = Intervals.borne_inf i in
Some (s, x, n, ex)
end
| _ -> o
) env.monomes None in
match o with
| Some (s,x,n,ex) ->
let ty = X.type_info x in
let r1 = x in
let r2 = P.alien_of (P.create [] n ty) in
[L.Eq(r1, r2), ex, s]
| None ->
[]
let case_split env =
match case_split_polynomes env with
| [] -> case_split_monomes env
| choices -> choices
let add env _ = env
let extract_improved env =
SP.fold
(fun p acc ->
MP.add p (MP.find p env.polynomes) acc)
env.improved MP.empty
end

23
old/fm.mli
View file

@ -1,23 +0,0 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
module type EXTENDED_Polynome = sig
include Polynome.T
val poly_of : r -> t
val alien_of : t -> r
end
module Make
(X : Sig.X)
(P : EXTENDED_Polynome with type r = X.r)
: Sig.RELATION with type r = X.r

703
old/intervals.ml
View file

@ -1,703 +0,0 @@
(**************************************************************************)
(* *)
(* 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 Num
open Format
module Ex = Explanation
type borne =
| Strict of (num * Ex.t)
| Large of (num * Ex.t)
| Pinfty | Minfty
let compare_bornes b1 b2 =
match b1, b2 with
| Minfty, Minfty | Pinfty, Pinfty -> 0
| Minfty, _ | _, Pinfty -> -1
| Pinfty, _ | _, Minfty -> 1
| Strict (v1, _), Strict (v2, _) | Large (v1, _), Large (v2, _)
| Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) ->
compare_num v1 v2
let compare_bu_bl b1 b2 =
match b1, b2 with
| (Minfty | Pinfty), _ | _,(Minfty | Pinfty)
| Strict _, Strict _ | Large _, Large _ ->
compare_bornes b1 b2
| Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) ->
let c = compare_num v1 v2 in
if c = 0 then -1 else c
let compare_bl_bu b1 b2 =
match b1, b2 with
| (Minfty | Pinfty), _ | _,(Minfty | Pinfty)
| Strict _, Strict _ | Large _, Large _ ->
compare_bornes b1 b2
| Strict (v1, _), Large (v2, _) | Large (v1, _), Strict (v2, _) ->
let c = compare_num v1 v2 in
if c = 0 then 1 else c
let compare_bl_bl b1 b2 =
match b1, b2 with
| (Minfty | Pinfty), _ | _,(Minfty | Pinfty)
| Strict _, Strict _ | Large _, Large _ ->
compare_bornes b1 b2
| Strict (v1, _), Large (v2, _) ->
let c = compare_num v1 v2 in
if c = 0 then 1 else c
| Large (v1, _), Strict (v2, _) ->
let c = compare_num v1 v2 in
if c = 0 then -1 else c
let compare_bu_bu b1 b2 =
match b1, b2 with
| (Minfty | Pinfty), _ | _,(Minfty | Pinfty)
| Strict _, Strict _ | Large _, Large _ ->
compare_bornes b1 b2
| Strict (v1, _), Large (v2, _) ->
let c = compare_num v1 v2 in
if c = 0 then -1 else c
| Large (v1, _), Strict (v2, _) ->
let c = compare_num v1 v2 in
if c = 0 then 1 else c
type t = {
ints : (borne * borne) list;
is_int : bool;
expl: Ex.t
}
exception EmptyInterval of Ex.t
exception NotConsistent of Ex.t
exception Not_a_float
let print_borne fmt = function
| Minfty -> fprintf fmt "-inf"
| Pinfty -> fprintf fmt "+inf"
| Strict (v, e) | Large (v, e) ->
fprintf fmt "%s" (string_of_num v)
let print_interval fmt (b1,b2) =
let c1, c2 = match b1, b2 with
| Large _, Large _ -> '[', ']'
| Large _, _ -> '[', '['
| _, Large _ -> ']', ']'
| _, _ -> ']', '['
in
fprintf fmt "%c%a;%a%c" c1 print_borne b1 print_borne b2 c2
let print fmt {ints = ints; is_int = b; expl = e } =
List.iter (fun i -> fprintf fmt "%a" print_interval i) ints
let undefined ty = {
ints = [Minfty, Pinfty];
is_int = ty = Ty.Tint;
expl = Ex.empty
}
let point b ty e = {
ints = [Large (b, e), Large (b, e)];
is_int = ty = Ty.Tint;
expl = Ex.empty
}
let explain_borne = function
| Large (_, e) | Strict (_, e) -> e
| _ -> Ex.empty
let add_expl_to_borne b e =
match b with
| Large (n, e') -> Large (n, Ex.union e e')
| Strict (n, e') -> Strict (n, Ex.union e e')
| Pinfty | Minfty -> b
let borne_of k e n = if k then Large (n, e) else Strict (n, e)
let is_point { ints = l; expl = e } =
match l with
| [Large (v1, e1) , Large (v2, e2)] when v1 =/ v2 ->
Some (v1, Ex.union e2 (Ex.union e1 e))
| _ -> None
let add_expl_zero i expl =
let res = List.map (fun x ->
match x with
| (Large ((Num.Int 0), e1) , Large ((Num.Int 0), e2)) ->
(Large ((Num.Int 0), Ex.union e1 expl),
Large ((Num.Int 0), Ex.union e2 expl))
| _ -> x) i.ints in
{ i with ints = res }
let check_one_interval b1 b2 is_int =
match b1, b2 with
| Pinfty, _ | _, Minfty -> raise (EmptyInterval Ex.empty)
| (Strict (v1, e1) | Large (v1,e1)),
(Strict (v2, e2) | Large (v2, e2)) ->
let c = compare_num v1 v2 in
if c > 0 then raise
(EmptyInterval (Ex.union e2 e1));
if c = 0 then begin
match b1, b2 with
| Large _, Large _ when not is_int || is_integer_num v1 ->
()
| _ -> raise (EmptyInterval (Ex.union e2 e1))
end
| _ -> ()
let min_borne b1 b2 =
match b1, b2 with
| Minfty , _ | _ , Minfty -> Minfty
| b , Pinfty | Pinfty, b -> b
| (Strict (v1, _) | Large (v1, _)) , (Strict (v2, _) | Large (v2, _)) ->
let c = compare_num v1 v2 in
if c < 0 then b1
else if c > 0 then b2
else match b1, b2 with
| (Strict _ as b) , _ | _, (Strict _ as b) -> b
| _, _ -> b1
let max_borne b1 b2 =
match b1, b2 with
| Pinfty , _ | _ , Pinfty -> Pinfty
| b , Minfty | Minfty, b -> b
| (Strict (v1, _) | Large (v1, _)) , (Strict (v2, _) | Large (v2, _)) ->
let c = compare_num v1 v2 in
if c > 0 then b1
else if c < 0 then b2
else match b1, b2 with
| (Strict _ as b) , _ | _, (Strict _ as b) -> b
| _, _ -> b1
let pos_borne b1 =
compare_bornes b1 (borne_of true Ex.empty (Int 0)) >= 0
let pos_borne_strict b1 =
compare_bornes b1 (borne_of true Ex.empty (Int 0)) > 0
let neg_borne b1 =
compare_bornes b1 (borne_of true Ex.empty (Int 0)) <= 0
let neg_borne_strict b1 =
compare_bornes b1 (borne_of true Ex.empty (Int 0)) < 0
let zero_borne b1 =
compare_bornes b1 (borne_of true Ex.empty (Int 0)) = 0
exception Found of Sig.answer
let doesnt_contain_0 {ints=l} =
try
let max = List.fold_left
(fun old_u (l, u) ->
if neg_borne l && pos_borne u then raise (Found Sig.No);
if neg_borne_strict old_u && pos_borne_strict l then
raise (Found
(Sig.Yes
(Ex.union
(explain_borne old_u) (explain_borne l))));
u) Minfty l in
if neg_borne_strict max then Sig.Yes (explain_borne max)
else Sig.No
with Found ans -> ans
let is_strict_smaller i1 i2 =
match i1, i2 with
| _, [] -> false
| [], _ -> true
| _ ->
try
List.iter2 (fun (l1, u1) (l2, u2) ->
if compare_bornes l1 l2 > 0 || compare_bornes u1 u2 < 0
then raise Exit
) i1 i2;
false
with
| Exit -> true
| Invalid_argument _ -> List.length i1 > List.length i2
let is_strict_smaller {ints=i1} {ints=i2} =
is_strict_smaller i1 i2
let rec union_bornes l =
match l with
| [] | [_] -> l
| (l1, u1)::((l2, u2)::r as r2) ->
if compare_bornes u1 l2 < 0 then
(l1, u1)::(union_bornes r2)
else if compare_bornes u1 u2 > 0 then
union_bornes ((l1, u1)::r)
else
union_bornes ((l1, u2)::r)
let union ({ints = l} as uints) =
let l = List.sort (fun (l1, _) (l2, _) -> compare_bornes l1 l2) l in
{ uints with ints = union_bornes l }
let add_borne b1 b2 =
match b1,b2 with
| Minfty, Pinfty | Pinfty, Minfty -> assert false
| Minfty, _ | _, Minfty -> Minfty
| Pinfty, _ | _, Pinfty -> Pinfty
| Large (v1, e1), Large (v2, e2) ->
Large (v1 +/ v2, Ex.union e1 e2)
| (Large (v1, e1) | Strict (v1, e1)), (Large (v2, e2) | Strict (v2, e2)) ->
Strict (v1 +/ v2, Ex.union e1 e2)
let add_interval l (b1,b2) =
List.fold_right
(fun (b1', b2') l ->
let l1 = ((add_borne b1 b1'),(add_borne b2 b2'))::l in
union_bornes (l1)
) l []
let add {ints = l1; is_int = is_int; expl = e1} {ints = l2; expl = e2}=
let l =
List.fold_left
(fun l bs -> let i = add_interval l1 bs in i@l) [] l2
in
union { ints = l ; is_int = is_int; expl = Ex.union e1 e2 }
let minus_borne = function
| Minfty -> Pinfty
| Pinfty -> Minfty
| Large (v, e) -> Large (minus_num v, e)
| Strict (v, e) -> Strict (minus_num v, e)
let scale_borne n b =
assert (n >=/ Int 0);
if n =/ Int 0 then
match b with
| Pinfty | Minfty -> Large (Int 0, Ex.empty)
| Large (_, e) | Strict (_, e) -> Large (Int 0, e)
else match b with
| Pinfty | Minfty -> b
| Large (v, e) -> Large (n */ v, e)
| Strict (v, e) -> Strict (n */ v, e)
let scale_interval n (b1,b2) =
if n </ Int 0 then
(minus_borne (scale_borne (minus_num n) b2),
minus_borne (scale_borne (minus_num n) b1))
else (scale_borne n b1, scale_borne n b2)
let scale n uints =
let l = List.map (scale_interval n) uints.ints in
union { uints with ints = l; expl = uints.expl }
let mult_borne b1 b2 =
match b1,b2 with
| Minfty, Pinfty | Pinfty, Minfty -> assert false
| Minfty, b | b, Minfty ->
if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0
then b
else if pos_borne b then Minfty
else Pinfty
| Pinfty, b | b, Pinfty ->
if compare_bornes b (borne_of true Ex.empty (Int 0)) = 0
then b
else if pos_borne b then Pinfty
else Minfty
| Strict (v1, e1), Strict (v2, e2) | Strict (v1, e1), Large (v2, e2)
| Large (v1, e1), Strict (v2, e2) ->
Strict (v1 */ v2, Ex.union e1 e2)
| Large (v1, e1), Large (v2, e2) ->
Large (v1 */ v2, Ex.union e1 e2)
let mult_borne_inf b1 b2 =
match b1,b2 with
| Minfty, Pinfty | Pinfty, Minfty -> Minfty
| _, _ -> mult_borne b1 b2
let mult_borne_sup b1 b2 =
match b1,b2 with
| Minfty, Pinfty | Pinfty, Minfty -> Pinfty
| _, _ -> mult_borne b1 b2
type interval_class =
| P of Ex.t
| M of Ex.t
| N of Ex.t
| Z
let class_of (l,u) =
if zero_borne l && zero_borne u then Z
else if pos_borne l && pos_borne u then P (explain_borne l)
else if neg_borne l && neg_borne u then N (explain_borne u)
else M (Ex.union (explain_borne l) (explain_borne u))
let mult_bornes (a,b) (c,d) =
(* see util/intervals_mult.png *)
match class_of (a,b), class_of (c,d) with
| P e1, P e2 ->
mult_borne_inf a c, mult_borne_sup b d, Ex.union e1 e2
| P e1, M e2 ->
mult_borne_inf b c, mult_borne_sup b d, Ex.union e1 e2
| P e1, N e2 ->
mult_borne_inf b c, mult_borne_sup a d, Ex.union e1 e2
| M e1, P e2 ->
mult_borne_inf a d, mult_borne_sup b d, Ex.union e1 e2
| M e1, M e2 ->
min_borne (mult_borne_inf a d) (mult_borne_inf b c),
max_borne (mult_borne_sup a c) (mult_borne_sup b d),
Ex.union e1 e2
| M e1, N e2 ->
mult_borne_inf b c, mult_borne_sup a c, Ex.union e1 e2
| N e1, P e2 ->
mult_borne_inf a d, mult_borne_sup b c, Ex.union e1 e2
| N e1, M e2 ->
mult_borne_inf a d, mult_borne_sup a c, Ex.union e1 e2
| N e1, N e2 ->
mult_borne_inf b d, mult_borne_sup a c, Ex.union e1 e2
| Z, (P _ | M _ | N _ | Z) -> (a, b, Ex.empty)
| (P _ | M _ | N _ ), Z -> (c, d, Ex.empty)
let rec power_borne_inf p b =
match p with
| 1 -> b
| p -> mult_borne_inf b (power_borne_inf (p-1) b)
let rec power_borne_sup p b =
match p with
| 1 -> b
| p -> mult_borne_sup b (power_borne_sup (p-1) b)
let max_merge b1 b2 =
let ex = Ex.union (explain_borne b1) (explain_borne b2) in
let max = max_borne b1 b2 in
match max with
| Minfty | Pinfty -> max
| Large (v, e) -> Large (v, ex)
| Strict (v, e) -> Strict (v, ex)
let power_bornes p (b1,b2) =
if neg_borne b1 && pos_borne b2 then
match p with
| 0 -> assert false
| p when p mod 2 = 0 ->
(* max_merge to have explanations !!! *)
let m = max_merge (power_borne_sup p b1) (power_borne_sup p b2) in
(Large (Int 0, Ex.empty), m)
| _ -> (power_borne_inf p b1, power_borne_sup p b2)
else if pos_borne b1 && pos_borne b2 then
(power_borne_inf p b1, power_borne_sup p b2)
else if neg_borne b1 && neg_borne b2 then
match p with
| 0 -> assert false
| p when p mod 2 = 0 -> (power_borne_inf p b2, power_borne_sup p b1)
| _ -> (power_borne_inf p b1, power_borne_sup p b2)
else assert false
let int_of_borne_inf b =
match b with
| Minfty | Pinfty -> b
| Large (v, e) -> Large (ceiling_num v, e)
| Strict (v, e) ->
let v' = ceiling_num v in
if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e)
let int_of_borne_sup b =
match b with
| Minfty | Pinfty -> b
| Large (v, e) -> Large (floor_num v, e)
| Strict (v, e) ->
let v' = floor_num v in
if v' </ v then Large (v', e) else Large (v -/ (Int 1), e)
let int_div_of_borne_inf b =
match b with
| Minfty | Pinfty -> b
| Large (v, e) -> Large (floor_num v, e)
| Strict (v, e) ->
let v' = floor_num v in
if v' >/ v then Large (v', e) else Large (v +/ (Int 1), e)
let int_div_of_borne_sup b =
match b with
| Minfty | Pinfty -> b
| Large (v, e) -> Large (floor_num v, e)
| Strict (v, e) ->
let v' = floor_num v in
if v' </ v then Large (v', e) else Large (v -/ (Int 1), e)
let int_bornes l u =
int_of_borne_inf l, int_of_borne_sup u
let int_div_bornes l u =
int_div_of_borne_inf l, int_div_of_borne_sup u
let intersect ({ints=l1; expl=e1; is_int=is_int} as uints1)
{ints=l2; expl=e2} =
(* fprintf fmt "intersect %a inter %a@." print uints1 print uints2; *)
let rec step (l1,l2) acc expl =
match l1, l2 with
| (lo1,up1)::r1, (lo2,up2)::r2 ->
let (lo1,up1), (lo2,up2) =
if is_int then (int_bornes lo1 up1), (int_bornes lo2 up2)
else (lo1,up1), (lo2,up2) in
let cll = compare_bl_bl lo1 lo2 in
let cuu = compare_bu_bu up1 up2 in
let clu = compare_bl_bu lo1 up2 in
let cul = compare_bu_bl up1 lo2 in
if cul < 0 then
let nexpl = Ex.union (explain_borne up1) (explain_borne lo2) in
match r1 with
| [] -> step (r1, l2) acc (Ex.union nexpl expl)
| (lor1,upr1)::rr1 ->
let lor1 = add_expl_to_borne lor1 nexpl in
let r1 = (lor1,upr1)::rr1 in
step (r1, l2) acc expl
else if clu > 0 then
let nexpl = Ex.union (explain_borne up2) (explain_borne lo1) in
match r2 with
| [] -> step (l1, r2) acc (Ex.union nexpl expl)
| (lor2,upr2)::rr2 ->
let lor2 = add_expl_to_borne lor2 nexpl in
let r2 = (lor2,upr2)::rr2 in
step (l1, r2) acc expl
else if cll = 0 && cuu = 0 then
step (r1, r2) ((lo1,up1)::acc) expl
else if cll <= 0 && cuu >= 0 then
step (l1, r2) ((lo2,up2)::acc) expl
else if cll >= 0 && cuu <= 0 then
step (r1, l2) ((lo1,up1)::acc) expl
else if cll <= 0 && cuu <= 0 && cul >= 0 then
step (r1, l2) ((lo2,up1)::acc) expl
else if cll >= 0 && cuu >= 0 && clu <= 0 then
step (l1, r2) ((lo1,up2)::acc) expl
else assert false
| [], _ | _, [] -> List.rev acc, expl
in
let l, expl = step (l1,l2) [] (Ex.union e1 e2) in
if l = [] then raise (NotConsistent expl)
else { uints1 with ints = l; expl = expl }
let new_borne_sup expl b ~is_le uints =
intersect
{ ints = [Minfty, (borne_of is_le expl b)];
is_int = uints.is_int;
expl = Ex.empty } uints
let new_borne_inf expl b ~is_le uints =
intersect
{ ints = [(borne_of is_le expl b), Pinfty];
is_int = uints.is_int;
expl = Ex.empty } uints
let complement ({ints=l; expl=e} as uints) =
let rec step l prev acc =
match l with
| (b1,b2)::r ->
let bu = match b1 with
| Strict v -> Large v
| Large v -> Strict v
| _ -> b1 in
let bl = match b2 with
| Strict v -> Large v
| Large v -> Strict v
| _ -> b2 in
if bu = Minfty then step r bl acc
else step r bl ((prev, bu)::acc)
| [] ->
if prev = Pinfty then List.rev acc
else List.rev ((prev, Pinfty)::acc)
in
{ uints with ints = step l Minfty [] }
let exclude uints1 uints2 =
intersect (complement uints1) uints2
let mult u1 u2 =
let resl, expl =
List.fold_left
(fun (l', expl) b1 ->
List.fold_left
(fun (l, ex) b2 ->
let bl, bu, ex' = mult_bornes b1 b2 in
(bl, bu)::l, Ex.union ex ex') (l', expl) u2.ints)
([], Ex.empty) u1.ints
in
union { ints=resl; is_int = u1.is_int;
expl = Ex.union expl
(Ex.union u1.expl u2.expl) }
let power n u =
let l = List.map (power_bornes n) u.ints in
union { u with ints = l }
let num_of_float x =
if x = infinity || x = neg_infinity then raise Not_a_float;
let (f, n) = frexp x in
let z =
Big_int.big_int_of_string
(Int64.to_string (Int64.of_float (f *. 2. ** 52.))) in
(*
Si on a ocaml >= 3.11 on peut mettre (mieux) :
let z =
Big_int.big_int_of_int64
(Int64.of_float (f *. 2. ** 52.)) in
*)
let factor = (Int 2) **/ (Int (n - 52)) in
(Big_int z) */ factor
let root_num a n =
if a </ (Int 0) then assert false
else if a =/ (Int 0) then (Int 0)
else if n = 2 then num_of_float (sqrt (float_of_num a))
else num_of_float ((float_of_num a) ** (1./. (float n)))
let root_default_num a n =
let s = root_num a n in
let d = a -/ (s **/ (Int n)) in
if d >=/ (Int 0) then s else a // (s **/ ((Int n) -/ (Int 1)))
let root_exces_num a n =
let s = root_num a n in
let d = a -/ (s **/ (Int n)) in
if d <=/ (Int 0) then s else a // (s **/ ((Int n) -/ (Int 1)))
let root_default_borne is_int x n =
match x with
| Pinfty -> Pinfty
| Minfty -> Minfty
| Large (v, e) | Strict (v, e) ->
let s = if v >=/ (Int 0) then root_default_num v n
else (minus_num (root_exces_num (minus_num v) n)) in
if is_int then
let cs = ceiling_num s in
let cs2 = cs **/ (Int n) in
if v <=/ cs2 then Large (cs, e)
else Large (cs +/ (Int 1), e)
else Large (s, e)
let root_exces_borne is_int x n =
match x with
| Pinfty -> Pinfty
| Minfty -> Minfty
| Large (v, e) | Strict (v, e) ->
let s = if v >=/ (Int 0) then root_exces_num v n
else (minus_num (root_default_num (minus_num v) n)) in
if is_int then
let cs = floor_num s in
let cs2 = cs **/ (Int n) in
if v >=/ cs2 then Large (cs, e)
else Large (cs -/ (Int 1), e)
else Large (s, e)
let sqrt_interval is_int (b1,b2) =
let l1, u1 = (minus_borne (root_exces_borne is_int b2 2),
minus_borne (root_default_borne is_int b1 2)) in
let l2, u2 = (root_default_borne is_int b1 2,
root_exces_borne is_int b2 2) in
if compare_bornes l1 u1 > 0 then
if compare_bornes l2 u2 > 0 then []
else [l2,u2]
else if compare_bornes l2 u2 > 0 then [l1, u1]
else union_bornes [(l1,u1); (l2, u2)]
let root_interval is_int (b1,b2) n =
let u,l = (root_default_borne is_int b1 n, root_exces_borne is_int b2 n) in
if compare_bornes u l > 0 then [] else [u,l]
let sqrt {ints = l; is_int = is_int; expl = e } =
let l =
List.fold_left
(fun l' bs ->
(sqrt_interval is_int bs)@l'
) [] l in
union { ints = l; is_int = is_int; expl = e }
let rec root n ({ints = l; is_int = is_int; expl = e} as u) =
if n mod 2 = 0 then root (n/2) (sqrt u)
else
let l =
List.fold_left
(fun l' bs ->
(root_interval is_int bs n)@l'
) [] l in
union { ints = l; is_int = is_int; expl = e }
let finite_size {ints = l; is_int = is_int} =
if (not is_int) then None
else
try
let n =
List.fold_left
(fun n (b1,b2) ->
match b1, b2 with
| Minfty, _ | _, Pinfty -> raise Exit
| Large (v1, _) , Large (v2, _) -> n +/ (v2 -/ v1 +/ (Int 1))
| _, _ -> assert false
) (Int 0) l in
Some n
with Exit -> None
let borne_inf = function
| {ints = (Large (v, ex), _)::_} -> v, ex
| _ -> invalid_arg "Intervals.borne_inf : No finite lower bound"
let inv_borne_inf b is_int ~other =
match b with
| Pinfty -> assert false
| Minfty ->
if is_int then Large (Int 0, explain_borne other)
else Strict (Int 0, explain_borne other)
| Strict (Int 0, e) | Large (Int 0, e) -> Pinfty
| Strict (v, e) -> Strict (Int 1 // v, e)
| Large (v, e) -> Large (Int 1 // v, e)
let inv_borne_sup b is_int ~other =
match b with
| Minfty -> assert false
| Pinfty ->
if is_int then Large (Int 0, explain_borne other)
else Strict (Int 0, explain_borne other)
| Strict (Int 0, e) | Large (Int 0, e) -> Minfty
| Strict (v, e) -> Strict (Int 1 // v, e)
| Large (v, e) -> Large (Int 1 // v, e)
let inv_bornes (l, u) is_int =
inv_borne_sup u is_int ~other:l, inv_borne_inf l is_int ~other:u
let inv ({ints=l; is_int=is_int} as u) =
try
let l' = List.fold_left
(fun acc (l,u) ->
if (pos_borne_strict l && pos_borne_strict u)
|| (neg_borne_strict l && neg_borne_strict u) then
(inv_bornes (l, u) is_int) :: acc
else raise Exit
) [] l in
union { u with ints=l' }
with Exit -> { u with ints = [Minfty, Pinfty] }
let div i1 i2 =
let inv_i2 = inv i2 in
if inv_i2.ints = [Minfty, Pinfty] then inv_i2
else
let i1 = match doesnt_contain_0 i2 with
| Sig.Yes ex -> add_expl_zero i1 ex
| Sig.No -> i1
in
let ({ints=l; is_int=is_int} as i) = mult i1 inv_i2 in
let l =
if is_int then
List.map (fun (l,u) -> int_div_bornes l u) l
else l in
{ i with ints = l }

57
old/intervals.mli
View file

@ -1,57 +0,0 @@
(**************************************************************************)
(* *)
(* 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 Num
type t
exception NotConsistent of Explanation.t
exception Not_a_float
val undefined : Ty.t -> t
val point : num -> Ty.t -> Explanation.t -> t
val doesnt_contain_0 : t -> Sig.answer
val is_strict_smaller : t -> t -> bool
val new_borne_sup : Explanation.t -> num -> is_le : bool -> t -> t
val new_borne_inf : Explanation.t -> num -> is_le : bool -> t -> t
val is_point : t -> (num * Explanation.t) option
val intersect : t -> t -> t
val exclude : t -> t -> t
val mult : t -> t -> t
val power : int -> t -> t
val sqrt : t -> t
val root : int -> t -> t
val add : t -> t -> t
val scale : num -> t -> t
val print : Format.formatter -> t -> unit
val finite_size : t -> num option
val borne_inf : t -> num * Explanation.t
val div : t -> t -> t

210
old/literal.ml
View file

@ -1,210 +0,0 @@
(**************************************************************************)
(* *)
(* 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 Hashcons
type 'a view =
| Eq of 'a * 'a
| Distinct of bool * 'a list
| Builtin of bool * Hstring.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 add_label : Hstring.t -> t -> unit
val label : t -> Hstring.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 = (X.t view) hash_consed
module V = struct
type t = X.t view
let equal a1 a2 =
match a1, a2 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 && Hstring.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 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) (Hstring.hash n+x) l)
end
module H = Make_consed(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
let equal = equal
let hash = hash
end
let make t = H.hashcons t
let view a = a.node
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))
module Labels = Hashtbl.Make(T)
let labels = Labels.create 100007
let add_label lbl t = Labels.replace labels t lbl
let label t = try Labels.find labels t with Not_found -> Hstring.empty
let print_list fmt = function
| [] -> ()
| z :: l ->
Format.fprintf fmt "%a" X.print z;
List.iter (Format.fprintf fmt ", %a" X.print) l
let ale = Hstring.make "<="
let alt = Hstring.make "<"
let print fmt a =
let lbl = Hstring.view (label a) in
let lbl = if lbl = "" then lbl else lbl^":" in
match view a with
| Eq (z1, z2) ->
if equal z1 z2 then Format.fprintf fmt "True"
else Format.fprintf fmt "%s%a=%a" lbl X.print z1 X.print z2
| Distinct (b,(z::l)) ->
let b = if b then "~" else "" in
Format.fprintf fmt "%s%s%a" lbl b X.print z;
List.iter (fun x -> Format.fprintf fmt "<>%a" X.print x) l
| Builtin (true, n, [v1;v2]) when Hstring.equal n ale ->
Format.fprintf fmt "%s %a <= %a" lbl X.print v1 X.print v2
| Builtin (true, n, [v1;v2]) when Hstring.equal n alt ->
Format.fprintf fmt "%s %a < %a" lbl X.print v1 X.print v2
| Builtin (false, n, [v1;v2]) when Hstring.equal n ale ->
Format.fprintf fmt "%s %a > %a" lbl X.print v1 X.print v2
| Builtin (false, n, [v1;v2]) when Hstring.equal n alt ->
Format.fprintf fmt "%s %a >= %a" lbl X.print v1 X.print v2
| Builtin (b, n, l) ->
let b = if b then "" else "~" in
Format.fprintf fmt "%s%s%s(%a)" lbl b (Hstring.view 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

63
old/literal.mli
View file

@ -1,63 +0,0 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
(**************************************************************************)
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 * Hstring.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 add_label : Hstring.t -> t -> unit
val label : t -> Hstring.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

257
old/polynome.ml
View file

@ -1,257 +0,0 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon, Alain Mebsout *)
(* Mohamed Iguernelala *)
(* Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
open Format
open Num
exception Not_a_num
exception Maybe_zero
module type S = sig
type r
val compare : r -> r -> int
val term_embed : Term.t -> r
val mult : r -> r -> r
val print : Format.formatter -> r -> unit
end
module type T = sig
type r
type t
val compare : t -> t -> int
val hash : t -> int
val create : (num * r) list -> num -> Ty.t-> t
val add : t -> t -> t
val sub : t -> t -> t
val mult : t -> t -> t
val mult_const : num -> t -> t
val div : t -> t -> t * bool
val modulo : t -> t -> t
val is_empty : t -> bool
val find : r -> t -> num
val choose : t -> num * r
val subst : r -> t -> t -> t
val remove : r -> t -> t
val to_list : t -> (num * r) list * num
val print : Format.formatter -> t -> unit
val type_info : t -> Ty.t
val is_monomial : t -> (num * r * num) option
val ppmc_denominators : t -> num
val pgcd_numerators : t -> num
val normal_form : t -> t * num * num
val normal_form_pos : t -> t * num * num
end
module Make (X : S) = struct
type r = X.r
module M : Map.S with type key = r =
Map.Make(struct type t = r let compare x y = X.compare y x end)
type t = { m : num M.t; c : num; ty : Ty.t }
let compare p1 p2 =
let c = Ty.compare p1.ty p2.ty in
if c <> 0 then c
else
let c = compare_num p1.c p2.c in
if c = 0 then M.compare compare_num p1.m p2.m else c
let hash p =
abs (Hashtbl.hash p.m + 19*Hashtbl.hash p.c + 17 * Ty.hash p.ty)
let pprint fmt p =
M.iter
(fun x n ->
let s, n, op = match n with
| Int 1 -> "+", "", ""
| Int -1 -> "-", "", ""
| n ->
if n >/ Int 0 then "+", string_of_num n, "*"
else "-", string_of_num (minus_num n), "*"
in
fprintf fmt "%s%s%s%a" s n op X.print x
)p.m;
let s, n = if p.c >=/ Int 0 then "+", string_of_num p.c
else "-", string_of_num (minus_num p.c) in
fprintf fmt "%s%s" s n
let print fmt p =
M.iter
(fun t n -> fprintf fmt "%s*%a " (string_of_num n) X.print t) p.m;
fprintf fmt "%s" (string_of_num p.c);
fprintf fmt " [%a]" Ty.print p.ty
let is_num p = M.is_empty p.m
let find x m = try M.find x m with Not_found -> Int 0
let create l c ty =
let m =
List.fold_left
(fun m (n, x) ->
let n' = n +/ (find x m) in
if n' =/ (Int 0) then M.remove x m else M.add x n' m) M.empty l
in
{ m = m; c = c; ty = ty }
let add p1 p2 =
let m =
M.fold
(fun x a m ->
let a' = (find x m) +/ a in
if a' =/ (Int 0) then M.remove x m else M.add x a' m)
p2.m p1.m
in
{ m = m; c = p1.c +/ p2.c; ty = p1.ty }
let mult_const n p =
if n =/ (Int 0) then { m = M.empty; c = Int 0; ty = p.ty }
else { p with m = M.map (mult_num n) p.m; c = n */ p.c }
let mult_monome a x p =
let ax = { m = M.add x a M.empty; c = (Int 0); ty = p.ty} in
let acx = mult_const p.c ax in
let m =
M.fold
(fun xi ai m -> M.add (X.mult x xi) (a */ ai) m) p.m acx.m
in
{ acx with m = m}
let mult p1 p2 =
let p = mult_const p1.c p2 in
M.fold (fun x a p -> add (mult_monome a x p2) p) p1.m p
let sub p1 p2 =
add p1 (mult (create [] (Int (-1)) p1.ty) p2)
let div p1 p2 =
if M.is_empty p2.m then
if p2.c =/ Int 0 then raise Division_by_zero
else
let p = mult_const ((Int 1) // p2.c) p1 in
match M.is_empty p.m, p.ty with
| true, Ty.Tint -> {p with c = floor_num p.c}, false
| true, Ty.Treal -> p, false
| false, Ty.Tint -> p, true
| false, Ty.Treal -> p, false
| _ -> assert false
else raise Maybe_zero
let modulo p1 p2 =
if M.is_empty p2.m then
if p2.c =/ Int 0 then raise Division_by_zero
else
if M.is_empty p1.m then { p1 with c = mod_num p1.c p2.c }
else raise Not_a_num
else raise Maybe_zero
let find x p = M.find x p.m
let is_empty p = M.is_empty p.m
let choose p =
let tn= ref None in
(*version I : prend le premier element de la table*)
(try M.iter
(fun x a -> tn := Some (a, x); raise Exit) p.m with Exit -> ());
(*version II : prend le dernier element de la table i.e. le plus grand
M.iter (fun x a -> tn := Some (a, x)) p.m;*)
match !tn with Some p -> p | _ -> raise Not_found
let subst x p1 p2 =
try
let a = M.find x p2.m in
add (mult_const a p1) { p2 with m = M.remove x p2.m}
with Not_found -> p2
let remove x p = { p with m = M.remove x p.m }
let to_list p =
let l = M.fold (fun x a aliens -> (a, x)::aliens ) p.m [] in
List.rev l, p.c
let type_info p = p.ty
let is_monomial p =
try
M.fold
(fun x a r ->
match r with
| None -> Some (a, x, p.c)
| _ -> raise Exit)
p.m None
with Exit -> None
let denominator = function
| Num.Int _ | Num.Big_int _ -> Big_int.unit_big_int
| Num.Ratio rat -> Ratio.denominator_ratio rat
let numerator = function
| Num.Int i -> Big_int.big_int_of_int i
| Num.Big_int b -> b
| Num.Ratio rat -> Ratio.numerator_ratio rat
let pgcd_bi a b = Big_int.gcd_big_int a b
let ppmc_bi a b = Big_int.div_big_int (Big_int.mult_big_int a b) (pgcd_bi a b)
let abs_big_int_to_num b =
let b =
try Int (Big_int.int_of_big_int b)
with Failure "int_of_big_int" -> Big_int b
in
abs_num b
let ppmc_denominators {m=m} =
let res =
M.fold
(fun k c acc -> ppmc_bi (denominator c) acc)
m Big_int.unit_big_int in
abs_num (num_of_big_int res)
let pgcd_numerators {m=m} =
let res =
M.fold
(fun k c acc -> pgcd_bi (numerator c) acc)
m Big_int.zero_big_int in
abs_num (num_of_big_int res)
let normal_form ({ m = m; c = c } as p) =
if M.is_empty m then
{ p with c = Int 0 }, p.c, (Int 1)
else
let ppcm = ppmc_denominators p in
let pgcd = pgcd_numerators p in
let p = mult_const (ppcm // pgcd) p in
{ p with c = Int 0 }, p.c, (pgcd // ppcm)
let normal_form_pos p =
let p, c, d = normal_form p in
try
let a,x = choose p in
if a >/ (Int 0) then p, c, d
else mult_const (Int (-1)) p, minus_num c, minus_num d
with Not_found -> p, c, d
end

68
old/polynome.mli
View file

@ -1,68 +0,0 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon, Alain Mebsout *)
(* Mohamed Iguernelala *)
(* Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
open Num
exception Not_a_num
exception Maybe_zero
module type S = sig
type r
val compare : r -> r-> int
val term_embed : Term.t -> r
val mult : r -> r -> r
val print : Format.formatter -> r -> unit
end
module type T = sig
type r
type t
val compare : t -> t -> int
val hash : t -> int
val create : (num * r) list -> num -> Ty.t-> t
val add : t -> t -> t
val sub : t -> t -> t
val mult : t -> t -> t
val mult_const : num -> t -> t
val div : t -> t -> t * bool
val modulo : t -> t -> t
val is_empty : t -> bool
val find : r -> t -> num
val choose : t -> num * r
val subst : r -> t -> t -> t
val remove : r -> t -> t
val to_list : t -> (num * r) list * num
val print : Format.formatter -> t -> unit
val type_info : t -> Ty.t
val is_monomial : t -> (num * r * num) option
(* PPMC des denominateurs des coefficients excepte la constante *)
val ppmc_denominators : t -> num
(* PGCD des numerateurs des coefficients excepte la constante *)
val pgcd_numerators : t -> num
(* retourne un polynome sans constante et sa constante
et la constante multiplicative:
normal_form p = (p',c,d) <=> p = (p' + c) * d *)
val normal_form : t -> t * num * num
(* comme normal_form mais le signe est aussi normalise *)
val normal_form_pos : t -> t * num * num
end
module Make (X : S) : T with type r = X.r

146
old/sig.mli
View file

@ -1,146 +0,0 @@
(**************************************************************************)
(* *)
(* 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 answer = Yes of Explanation.t | No
type 'a literal = LSem of 'a Literal.view | LTerm of Literal.LT.t
type 'a input =
'a Literal.view * Literal.LT.t option * Explanation.t
type 'a result = {
assume : ('a literal * Explanation.t) list;
remove: ('a literal * Explanation.t) list;
}
module type RELATION = sig
type t
type r
val empty : unit -> t
val assume : t -> (r input) list -> t * r result
val query : t -> r input -> answer
val case_split : t -> (r Literal.view * Explanation.t * Num.num) list
(** case_split env returns a list of equalities *)
val add : t -> r -> t
(** add a representant to take into account *)
end
module type THEORY = sig
(**Type of terms of the theory*)
type t
(**Type of representants of terms of the theory*)
type r
(** Name of the theory*)
val name : string
(** return true if the symbol is owned by the theory*)
val is_mine_symb : Symbols.t -> bool
(** return true when the argument is an unsolvable function of the theory *)
val unsolvable : t -> bool
(** Give a representant of a term of the theory*)
val make : Term.t -> r * Literal.LT.t list
val term_extract : r -> Term.t option
val type_info : t -> Ty.t
val embed : r -> t
(** Give the leaves of a term of the theory *)
val leaves : t -> r list
val subst : r -> r -> t -> r
val compare : t -> t -> int
val hash : t -> int
(** solve r1 r2, solve the equality r1=r2 and return the substitution *)
val solve : r -> r -> (r * r) list
val print : Format.formatter -> t -> unit
val fully_interpreted : Symbols.t -> bool
module Rel : RELATION with type r = r
end
module type COMBINATOR = sig
type r
type th
val extract : r -> th
val make : Term.t -> r * Literal.LT.t list
val type_info : r -> Ty.t
val compare : r -> r -> int
val leaves : r -> r list
val subst : r -> r -> r -> r
val solve : r -> r -> (r * r) list
val empty_embedding : Term.t -> r
val normal_form : Literal.LT.t -> Literal.LT.t
val print : Format.formatter -> r -> unit
module Rel : RELATION with type r = r
end
module type X = 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
module Rel : RELATION with type r = r
end
module type C = sig
type t
type r
val extract : r -> t option
val embed : t -> r
end

790
old/smt.ml
View file

@ -1,790 +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 *)
(* *)
(**************************************************************************)
open Format
type error =
| DuplicateTypeName of Hstring.t
| DuplicateSymb of Hstring.t
| UnknownType of Hstring.t
| UnknownSymb of Hstring.t
exception Error of error
module AETerm = Term
module H = Hstring.H
module HSet = Hstring.HSet
let decl_types = H.create 17
let decl_symbs = H.create 17
let htrue = Hstring.make "True"
let hfalse = Hstring.make "False"
module Type = struct
type t = Hstring.t
let equal = Hstring.equal
let type_int =
let tint = Hstring.make "int" in
H.add decl_types tint Ty.Tint;
tint
let type_real =
let treal = Hstring.make "real" in
H.add decl_types treal Ty.Treal;
treal
let type_bool =
let tbool = Hstring.make "bool" in
H.add decl_types tbool Ty.Tbool;
tbool
let type_proc =
let tproc = Hstring.make "proc" in
H.add decl_types tproc Ty.Tint;
tproc
let declare_constructor ty c =
if H.mem decl_symbs c then raise (Error (DuplicateSymb c));
H.add decl_symbs c
(Symbols.name ~kind:Symbols.Constructor c, [], ty)
let declare t constrs =
if H.mem decl_types t then raise (Error (DuplicateTypeName t));
match constrs with
| [] ->
H.add decl_types t (Ty.Tabstract t)
| _ ->
let ty = Ty.Tsum (t, constrs) in
H.add decl_types t ty;
List.iter (fun c -> declare_constructor t c) constrs
let all_constructors () =
H.fold (fun _ c acc -> match c with
| Symbols.Name (h, Symbols.Constructor), _, _ -> h :: acc
| _ -> acc
) decl_symbs [htrue; hfalse]
let constructors ty =
if Hstring.equal ty type_bool then [htrue; hfalse]
else match H.find decl_types ty with
| Ty.Tsum (_ , cstrs) -> cstrs
| _ -> raise Not_found
end
module Symbol = struct
type t = Hstring.t
let declare f args ret =
if H.mem decl_symbs f then raise (Error (DuplicateTypeName f));
List.iter
(fun t ->
if not (H.mem decl_types t) then raise (Error (UnknownType t)) )
(ret::args);
H.add decl_symbs f (Symbols.name f, args, ret)
let type_of s = let _, args, ret = H.find decl_symbs s in args, ret
let declared s =
let res = H.mem decl_symbs s in
if not res then begin
eprintf "Not declared : %a in@." Hstring.print s;
H.iter (fun hs (sy, _, _) ->
eprintf "%a (=?%b) -> %a@." Hstring.print hs
(Hstring.compare hs s = 0)
Symbols.print sy)
decl_symbs;
end;
res
let not_builtin ty = Hstring.equal ty Type.type_proc ||
not (Hstring.equal ty Type.type_int || Hstring.equal ty Type.type_real ||
Hstring.equal ty Type.type_bool || Hstring.equal ty Type.type_proc)
let has_abstract_type s =
let _, ret = type_of s in
match H.find decl_types ret with
| Ty.Tabstract _ -> true
| _ -> false
let has_type_proc s =
Hstring.equal (snd (type_of s)) Type.type_proc
let _ =
H.add decl_symbs htrue (Symbols.True, [], Type.type_bool);
H.add decl_symbs hfalse (Symbols.False, [], Type.type_bool);
end
module Variant = struct
let constructors = H.create 17
let assignments = H.create 17
let find t x = try H.find t x with Not_found -> HSet.empty
let add t x v =
let s = find t x in
H.replace t x (HSet.add v s)
let assign_constr = add constructors
let assign_var x y =
if not (Hstring.equal x y) then
add assignments x y
let rec compute () =
let flag = ref false in
let visited = ref HSet.empty in
let rec dfs x s =
if not (HSet.mem x !visited) then
begin
visited := HSet.add x !visited;
HSet.iter
(fun y ->
let c_x = find constructors x in
let c_y = find constructors y in
let c = HSet.union c_x c_y in
if not (HSet.equal c c_x) then
begin
H.replace constructors x c;
flag := true
end;
dfs y (find assignments y)
) s
end
in
H.iter dfs assignments;
if !flag then compute ()
let hset_print fmt s =
HSet.iter (fun c -> Format.eprintf "%a, " Hstring.print c) s
let print () =
H.iter
(fun x c ->
Format.eprintf "%a = {%a}@." Hstring.print x hset_print c)
constructors
let get_variants = H.find constructors
let set_of_list = List.fold_left (fun s x -> HSet.add x s) HSet.empty
let init l =
compute ();
List.iter
(fun (x, nty) ->
if not (H.mem constructors x) then
let ty = H.find decl_types nty in
match ty with
| Ty.Tsum (_, l) ->
H.add constructors x (set_of_list l)
| _ -> ()) l;
H.clear assignments
let update_decl_types s =
let nty = ref "" in
let l = ref [] in
HSet.iter
(fun x ->
l := x :: !l;
let vx = Hstring.view x in
nty := if !nty = "" then vx else !nty ^ "|" ^ vx) s;
let nty = Hstring.make !nty in
let ty = Ty.Tsum (nty, List.rev !l) in
H.replace decl_types nty ty;
nty
let close () =
compute ();
H.iter
(fun x s ->
let nty = update_decl_types s in
let sy, args, _ = H.find decl_symbs x in
H.replace decl_symbs x (sy, args, nty))
constructors
end
module rec Term : sig
type t = T of AETerm.t | Tite of Formula.t * t * t
type operator = Plus | Minus | Mult | Div | Modulo
val first_ite : t list -> t list * (Formula.t * t * t) * t list
val make_int : Num.num -> t
val make_real : Num.num -> t
val make_app : Symbol.t -> t list -> t
val make_arith : operator -> t -> t -> t
val make_ite : Formula.t -> t -> t -> t
val is_int : t -> bool
val is_real : t -> bool
val t_true : t
val t_false : t
end
= struct
type t = T of AETerm.t | Tite of Formula.t * t * t
type operator = Plus | Minus | Mult | Div | Modulo
let make_int i = T (AETerm.int (Num.string_of_num i))
let make_real r = T (AETerm.real (Num.string_of_num r))
let rec first_ite = function
| [] -> raise Not_found
| Tite (c, t1, t2) :: l -> [], (c, t1, t2), l
| x :: l ->
let left, triplet, right = first_ite l in
x::left, triplet, right
let rec lift_ite sb l ty =
try
let left, (c, t1, t2), right = first_ite l in
let l = lift_ite sb (left@(t1::right)) ty in
let r = lift_ite sb (left@(t2::right)) ty in
Tite (c, l, r)
with Not_found ->
let l = List.map (function T x -> x | _ -> assert false) l in
T (AETerm.make sb l ty)
let make_app s l =
try
let (sb, _, nty) = H.find decl_symbs s in
let ty = H.find decl_types nty in
lift_ite sb l ty
with Not_found -> raise (Error (UnknownSymb s))
let t_true = T AETerm.true_
let t_false = T AETerm.false_
let rec is_int = function
| T t -> AETerm.is_int t
| Tite(_, t1, t2) -> is_int t1 && is_int t2
let rec is_real = function
| T t -> AETerm.is_real t
| Tite(_, t1, t2) -> is_real t1 && is_real t2
let make_arith op t1 t2 =
let op =
match op with
| Plus -> Symbols.Plus
| Minus -> Symbols.Minus
| Mult -> Symbols.Mult
| Div -> Symbols.Div
| Modulo -> Symbols.Modulo
in
let ty =
if is_int t1 && is_int t2 then Ty.Tint
else if is_real t1 && is_real t2 then Ty.Treal
else assert false
in
lift_ite (Symbols.Op op) [t1; t2] ty
let make_ite l t1 t2 = Tite (l, t1, t2)
end
and Formula : sig
type comparator = Eq | Neq | Le | Lt
type combinator = And | Or | Imp | Not
type t =
| Lit of Literal.LT.t
| Comb of combinator * t list
val f_true : t
val f_false : t
val make_lit : comparator -> Term.t list -> t
val make : combinator -> t list -> t
val make_cnf : t -> Literal.LT.t list list
val make_pred : ?sign:bool -> Term.t -> t
val make_not : t -> t
val make_and : t list -> t
val make_or : t list -> t
val make_imply : t -> t -> t
val make_equiv : t -> t -> t
val make_xor : t -> t -> t
val make_eq : Term.t -> Term.t -> t
val make_neq : Term.t -> Term.t -> t
val make_le : Term.t -> Term.t -> t
val make_lt : Term.t -> Term.t -> t
val make_ge : Term.t -> Term.t -> t
val make_gt : Term.t -> Term.t -> t
val print_list : string -> Format.formatter -> t list -> unit
val print : Format.formatter -> t -> unit
module Tseitin (Dymmy : sig end) :
sig val make_cnf : t -> Literal.LT.t list list end
end
= struct
type comparator = Eq | Neq | Le | Lt
type combinator = And | Or | Imp | Not
type t =
| Lit of Literal.LT.t
| Comb of combinator * t list
let rec print fmt phi =
match phi with
| Lit a -> Literal.LT.print fmt a
| Comb (Not, [f]) ->
fprintf fmt "not (%a)" print f
| Comb (And, l) -> fprintf fmt "(%a)" (print_list "and") l
| Comb (Or, l) -> fprintf fmt "(%a)" (print_list "or") l
| Comb (Imp, [f1; f2]) ->
fprintf fmt "(%a => %a)" print f1 print f2
| _ -> assert false
and print_list sep fmt = function
| [] -> ()
| [f] -> print fmt f
| f::l -> fprintf fmt "%a %s %a" print f sep (print_list sep) l
let f_true = Lit Literal.LT.true_
let f_false = Lit Literal.LT.false_
let make comb l = Comb (comb, l)
let value env c =
if List.mem c env then Some true
else if List.mem (make Not [c]) env then Some false
else None
let rec lift_ite env op l =
try
let left, (c, t1, t2), right = Term.first_ite l in
begin
match value env c with
| Some true ->
lift_ite (c::env) op (left@(t1::right))
| Some false ->
lift_ite ((make Not [c])::env) op (left@(t2::right))
| None ->
Comb
(And,
[Comb
(Imp, [c; lift_ite (c::env) op (left@(t1::right))]);
Comb (Imp,
[(make Not [c]);
lift_ite
((make Not [c])::env) op (left@(t2::right))])])
end
with Not_found ->
begin
let lit =
match op, l with
| Eq, [Term.T t1; Term.T t2] ->
Literal.Eq (t1, t2)
| Neq, ts ->
let ts =
List.rev_map (function Term.T x -> x | _ -> assert false) ts in
Literal.Distinct (false, ts)
| Le, [Term.T t1; Term.T t2] ->
Literal.Builtin (true, Hstring.make "<=", [t1; t2])
| Lt, [Term.T t1; Term.T t2] ->
Literal.Builtin (true, Hstring.make "<", [t1; t2])
| _ -> assert false
in
Lit (Literal.LT.make lit)
end
let make_lit op l = lift_ite [] op l
let make_pred ?(sign=true) p =
if sign
then make_lit Eq [p; Term.t_true]
else make_lit Eq [p; Term.t_false]
let make_eq t1 t2 = make_lit Eq [t1; t2]
let make_neq t1 t2 = make_lit Neq [t1; t2]
let make_le t1 t2 = make_lit Le [t1; t2]
let make_lt t1 t2 = make_lit Lt [t1; t2]
let make_ge t1 t2 = make_lit Le [t2; t1]
let make_gt t1 t2 = make_lit Lt [t2; t1]
let make_not f = make Not [f]
let make_and l = make And l
let make_imply f1 f2 = make Imp [f1; f2]
let make_equiv f1 f2 = make And [ make_imply f1 f2; make_imply f2 f1]
let make_xor f1 f2 = make Or [ make And [ make Not [f1]; f2 ];
make And [ f1; make Not [f2] ] ]
(* simplify formula *)
let rec sform = function
| Comb (Not, [Lit a]) -> Lit (Literal.LT.neg a)
| Comb (Not, [Comb (Not, [f])]) -> sform f
| Comb (Not, [Comb (Or, l)]) ->
let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in
Comb (And, nl)
| Comb (Not, [Comb (And, l)]) ->
let nl = List.rev_map (fun a -> sform (Comb (Not, [a]))) l in
Comb (Or, nl)
| Comb (Not, [Comb (Imp, [f1; f2])]) ->
Comb (And, [sform f1; sform (Comb (Not, [f2]))])
| Comb (And, l) ->
Comb (And, List.rev_map sform l)
| Comb (Or, l) ->
Comb (Or, List.rev_map sform l)
| Comb (Imp, [f1; f2]) ->
Comb (Or, [sform (Comb (Not, [f1])); sform f2])
| Comb ((Imp | Not), _) -> assert false
| Lit _ as f -> f
let ( @@ ) l1 l2 = List.rev_append l1 l2
let ( @ ) = `Use_rev_append_instead (* prevent use of non-tailrec append *)
let make_or = function
| [] -> f_false
| [a] -> a
| l -> Comb (Or, l)
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)
let rec flatten_or = function
| [] -> []
| Comb (Or, l)::r -> l @@ (flatten_or r)
| Lit a :: r -> (Lit a)::(flatten_or r)
| _ -> assert false
let rec flatten_and = function
| [] -> []
| Comb (And, l)::r -> l @@ (flatten_and r)
| a :: r -> a::(flatten_and r)
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]) -> [[Literal.LT.neg a]]
| _ -> assert false
let rec unfold mono f =
match f with
| Lit a -> a::mono
| Comb (Not, [Lit a]) ->
(Literal.LT.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 =
let cpt = ref 0 in
fun () ->
let t = AETerm.make
(Symbols.name (Hstring.make ("PROXY__"^(string_of_int !cpt))))
[] Ty.Tbool
in
incr cpt;
Literal.LT.make (Literal.Eq (t, AETerm.true_))
module Tseitin (Dummy : sig end)= struct
let acc_or = ref []
let acc_and = ref []
(* 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
| Lit a -> None, [a]
| Comb (Not, [Lit a]) -> None, [Literal.LT.neg a]
| Comb (And, l) ->
List.fold_left
(fun (_, acc) f ->
match cnf f with
| _, [] -> assert false
| cmb, [a] -> Some And, a :: acc
| Some And, l ->
Some And, l @@ acc
(* let proxy = mk_proxy () in *)
(* acc_and := (proxy, l) :: !acc_and; *)
(* proxy :: acc *)
| Some Or, l ->
let proxy = mk_proxy () in
acc_or := (proxy, l) :: !acc_or;
Some And, proxy :: acc
| None, l -> Some And, l @@ acc
| _ -> assert false
) (None, []) l
| Comb (Or, l) ->
List.fold_left
(fun (_, acc) f ->
match cnf f with
| _, [] -> assert false
| cmb, [a] -> Some Or, a :: acc
| Some Or, l ->
Some Or, l @@ acc
(* let proxy = mk_proxy () in *)
(* acc_or := (proxy, l) :: !acc_or; *)
(* proxy :: acc *)
| Some And, l ->
let proxy = mk_proxy () in
acc_and := (proxy, l) :: !acc_and;
Some Or, proxy :: acc
| None, l -> Some Or, l @@ acc
| _ -> assert false
) (None, []) l
| _ -> assert false
let cnf f =
let acc = match f with
| Comb (And, l) -> List.rev_map (fun f -> snd(cnf f)) l
| _ -> [snd (cnf f)]
in
let proxies = ref [] in
(* encore clauses that make proxies in !acc_and equivalent to
their clause *)
let acc =
List.fold_left
(fun acc (p,l) ->
proxies := p :: !proxies;
let np = Literal.LT.neg p in
(* build clause [cl = l1 & l2 & ... & ln => p] where [l = [l1;l2;..]]
also add clauses [p => l1], [p => l2], etc. *)
let cl, acc =
List.fold_left
(fun (cl,acc) a -> (Literal.LT.neg a :: cl), [np; a] :: acc)
([p],acc) l in
cl :: acc
)acc !acc_and
in
(* encore clauses that make proxies in !acc_or equivalent to
their clause *)
let acc =
List.fold_left
(fun acc (p,l) ->
proxies := p :: !proxies;
(* add clause [p => l1 | l2 | ... | ln], and add clauses
[l1 => p], [l2 => p], etc. *)
let acc = List.fold_left (fun acc a -> [p; Literal.LT.neg a]::acc)
acc l in
(Literal.LT.neg p :: l) :: acc
) acc !acc_or
in
acc
let make_cnf f =
acc_or := [];
acc_and := [];
cnf (sform f)
end
(* Naive CNF XXX remove???
let make_cnf f = mk_cnf (sform f)
*)
end
exception Unsat of int list
let set_cc b = Cc.cc_active := b
module type Solver = sig
type state
val get_time : unit -> float
val get_calls : unit -> int
val clear : unit -> unit
val assume : ?profiling:bool -> id:int -> Formula.t -> unit
val check : ?profiling:bool -> unit -> unit
val eval : Term.t -> bool
val save_state : unit -> state
val restore_state : state -> unit
val entails : ?profiling:bool -> id:int -> Formula.t -> bool
end
module Make (Dummy : sig end) = struct
let calls = ref 0
module Time = Timer.Make (Dummy)
let get_time = Time.get
let get_calls () = !calls
module Tseitin = Formula.Tseitin (Dummy)
module CSolver = Solver.Make (Dummy)
let clear () = CSolver.clear ()
let check_unsatcore uc =
eprintf "Unsat Core : @.";
List.iter
(fun c ->
eprintf "%a@." (Formula.print_list "or")
(List.rev_map (fun x -> Formula.Lit x) c)) uc;
eprintf "@.";
try
clear ();
CSolver.assume uc 0;
CSolver.solve ();
eprintf "Not an unsat core !!!@.";
assert false
with
| Solver.Unsat _ -> ();
| Solver.Sat ->
eprintf "Sat: Not an unsat core !!!@.";
assert false
let export_unsatcore cl =
let uc = List.rev_map (fun {Solver_types.atoms=atoms} ->
let l = ref [] in
for i = 0 to Vec.size atoms - 1 do
l := (Vec.get atoms i).Solver_types.lit :: !l
done;
!l) cl
in (* check_unsatcore uc; *)
uc
module SInt =
Set.Make (struct type t = int let compare = Pervasives.compare end)
let export_unsatcore2 cl =
let s =
List.fold_left
(fun s {Solver_types.name = n} ->
try SInt.add (int_of_string n) s with _ -> s) SInt.empty cl
in
SInt.elements s
let assume ?(profiling = false) ~id f =
if profiling then Time.start ();
try
CSolver.assume (Tseitin.make_cnf f) id;
if profiling then Time.pause ()
with Solver.Unsat ex ->
if profiling then Time.pause ();
raise (Unsat (export_unsatcore2 ex))
let check ?(profiling = false) () =
incr calls;
if profiling then Time.start ();
try
CSolver.solve ();
if profiling then Time.pause ()
with
| Solver.Sat -> if profiling then Time.pause ()
| Solver.Unsat ex ->
if profiling then Time.pause ();
raise (Unsat (export_unsatcore2 ex))
type state = CSolver.state
let eval t =
match t with
| Term.T t' ->
let lit = Literal.LT.mk_pred t' in
CSolver.eval lit
| Term.Tite _ ->
failwith "cannot evaluate \"if-then-else\" term"
let save_state = CSolver.save
let restore_state = CSolver.restore
let entails ?(profiling=false) ~id f =
let st = save_state () in
let ans =
try
assume ~profiling ~id (Formula.make Formula.Not [f]) ;
check ~profiling ();
false
with Unsat _ -> true
in
restore_state st;
ans
end

338
old/smt.mli
View file

@ -1,338 +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 *)
(* *)
(**************************************************************************)
(** {b The Alt-Ergo Zero SMT library}
This SMT solver is derived from {{:http://alt-ergo.lri.fr} Alt-Ergo}. It
uses an efficient SAT solver and supports the following quantifier free
theories:
- Equality and uninterpreted functions
- Arithmetic (linear, non-linear, integer, reals)
- Enumerated data-types
This API makes heavy use of hash-consed strings. Please take a moment to
look at {! Hstring}.
*)
(** {2 Error handling } *)
type error =
| DuplicateTypeName of Hstring.t (** raised when a type is already declared *)
| DuplicateSymb of Hstring.t (** raised when a symbol is already declared *)
| UnknownType of Hstring.t (** raised when the given type is not declared *)
| UnknownSymb of Hstring.t (** raised when the given symbol is not declared *)
exception Error of error
(** {2 Typing } *)
(** {3 Typing } *)
module Type : sig
type t = Hstring.t
(** The type of types in Alt-Ergo Zero *)
(** {4 Builtin types } *)
val type_int : t
(** The type of integers *)
val type_real : t
(** The type of reals *)
val type_bool : t
(** The type of booleans *)
val type_proc : t
(** The type processes (identifiers) *)
(** {4 Declaring new types } *)
val declare : Hstring.t -> Hstring.t list -> unit
(** {ul {- [declare n cstrs] declares a new enumerated data-type with
name [n] and constructors [cstrs].}
{- [declare n []] declares a new abstract type with name [n].}}*)
val all_constructors : unit -> Hstring.t list
(** [all_constructors ()] returns a list of all the defined constructors. *)
val constructors : t -> Hstring.t list
(** [constructors ty] returns the list of constructors of [ty] when type is
an enumerated data-type, otherwise returns [[]].*)
end
(** {3 Function symbols} *)
module Symbol : sig
type t = Hstring.t
(** The type of function symbols *)
val declare : Hstring.t -> Type.t list -> Type.t -> unit
(** [declare s [arg_1; ... ; arg_n] out] declares a new function
symbol with type [ (arg_1, ... , arg_n) -> out] *)
val type_of : t -> Type.t list * Type.t
(** [type_of x] returns the type of x. *)
val has_abstract_type : t -> bool
(** [has_abstract_type x] is [true] if the type of x is abstract. *)
val has_type_proc : t -> bool
(** [has_type_proc x] is [true] if x has the type of a process
identifier. *)
val declared : t -> bool
(** [declared x] is [true] if [x] is already declared. *)
end
(** {3 Variants}
The types of symbols (when they are enumerated data types) can be refined
to substypes of their original type (i.e. a subset of their constructors).
*)
module Variant : sig
val init : (Symbol.t * Type.t) list -> unit
(** [init l] where [l] is a list of pairs [(s, ty)] initializes the
type (and associated constructors) of each [s] to its original type [ty].
This function must be called with a list of all symbols before
attempting to refine the types. *)
val close : unit -> unit
(** [close ()] will compute the smallest type possible for each symbol.
This function must be called when all information has been added.*)
val assign_constr : Symbol.t -> Hstring.t -> unit
(** [assign_constr s cstr] will add the constraint that the constructor
[cstr] must be in the type of [s] *)
val assign_var : Symbol.t -> Symbol.t -> unit
(** [assign_var x y] will add the constraint that the type of [y] is a
subtype of [x] (use this function when [x := y] appear in your
program *)
val print : unit -> unit
(** [print ()] will output the computed refined types on std_err. This
function is here only for debugging purposes. Use it afer [close ()].*)
val get_variants : Symbol.t -> Hstring.HSet.t
(** [get_variants s] returns a set of constructors, which is the refined
type of [s].*)
end
(** {2 Building terms} *)
module rec Term : sig
type t
(** The type of terms *)
(** The type of operators *)
type operator =
| Plus (** [+] *)
| Minus (** [-] *)
| Mult (** [*] *)
| Div (** [/] *)
| Modulo (** [mod] *)
val make_int : Num.num -> t
(** [make_int n] creates an integer constant of value [n]. *)
val make_real : Num.num -> t
(** [make_real n] creates an real constant of value [n]. *)
val make_app : Symbol.t -> t list -> t
(** [make_app f l] creates the application of function symbol [f] to a list
of terms [l]. *)
val make_arith : operator -> t -> t -> t
(** [make_arith op t1 t2] creates the term [t1 <op> t2]. *)
val make_ite : Formula.t -> t -> t -> t
(** [make_ite f t1 t2] creates the term [if f then t1 else t2]. *)
val is_int : t -> bool
(** [is_int x] is [true] if the term [x] has type int *)
val is_real : t -> bool
(** [is_real x] is [true] if the term [x] has type real *)
val t_true : t
(** [t_true] is the boolean term [true] *)
val t_false : t
(** [t_false] is the boolean term [false] *)
end
(** {2 Building formulas} *)
and Formula : sig
(** The type of comparators: *)
type comparator =
| Eq (** equality ([=]) *)
| Neq (** disequality ([<>]) *)
| Le (** inequality ([<=]) *)
| Lt (** strict inequality ([<]) *)
(** The type of operators *)
type combinator =
| And (** conjunction *)
| Or (** disjunction *)
| Imp (** implication *)
| Not (** negation *)
(** The type of ground formulas *)
type t =
| Lit of Literal.LT.t
| Comb of combinator * t list
val f_true : t
(** The formula which represents [true]*)
val f_false : t
(** The formula which represents [false]*)
val make_lit : comparator -> Term.t list -> t
(** [make_lit cmp [t1; t2]] creates the literal [(t1 <cmp> t2)]. *)
val make : combinator -> t list -> t
(** [make cmb [f_1; ...; f_n]] creates the formula
[(f_1 <cmb> ... <cmb> f_n)].*)
val make_pred : ?sign:bool -> Term.t -> t
(** [make_pred p] builds the atomic formula [p = true].
@param sign the polarity of the atomic formula *)
val make_not : t -> t
val make_and : t list -> t
val make_or : t list -> t
val make_imply : t -> t -> t
val make_equiv : t -> t -> t
val make_xor : t -> t -> t
val make_eq : Term.t -> Term.t -> t
val make_neq : Term.t -> Term.t -> t
val make_le : Term.t -> Term.t -> t
val make_lt : Term.t -> Term.t -> t
val make_ge : Term.t -> Term.t -> t
val make_gt : Term.t -> Term.t -> t
val make_cnf : t -> Literal.LT.t 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
literals. *)
val print : Format.formatter -> t -> unit
(** [print fmt f] prints the formula on the formatter [fmt].*)
end
(** {2 The SMT solver} *)
exception Unsat of int list
(** The exception raised by {! Smt.Solver.check} and {! Smt.Solver.assume} when
the formula is unsatisfiable. *)
val set_cc : bool -> unit
(** set_cc [false] deactivates congruence closure algorithm
([true] by default).*)
module type Solver = sig
(** This SMT solver is imperative in the sense that it maintains a global
context. To create different instances of Alt-Ergo Zero use the
functor {! Smt.Make}.
A typical use of this solver is to do the following :{[
clear ();
assume f_1;
...
assume f_n;
check ();]}
*)
type state
(** The type of the internal state of the solver (see {!save_state} and
{!restore_state}).*)
(** {2 Profiling functions} *)
val get_time : unit -> float
(** [get_time ()] returns the cumulated time spent in the solver in seconds.*)
val get_calls : unit -> int
(** [get_calls ()] returns the cumulated number of calls to {! check}.*)
(** {2 Main API of the solver} *)
val clear : unit -> unit
(** [clear ()] clears the context of the solver. Use this after {! check}
raised {! Unsat} or if you want to restart the solver. *)
val assume : ?profiling:bool -> id:int -> Formula.t -> unit
(** [assume ~profiling:b f id] adds the formula [f] to the context of the
solver with identifier [id].
This function only performs unit propagation.
@param profiling if set to [true] then profiling information (time) will
be computed (expensive because of system calls).
{b Raises} {! Unsat} if the context becomes inconsistent after unit
propagation. *)
val check : ?profiling:bool -> unit -> unit
(** [check ()] runs Alt-Ergo Zero on its context. If [()] is
returned then the context is satifiable.
@param profiling if set to [true] then profiling information (time) will
be computed (expensive because of system calls).
{b Raises} {! Unsat} [[id_1; ...; id_n]] if the context is unsatisfiable.
[id_1, ..., id_n] is the unsat core (returned as the identifiers of the
formulas given to the solver). *)
val eval : Term.t -> bool
(** [eval lit] returns the current truth value for the literal. The term
must be a boolean proposition that occurred in the problem,
because the only information returned by [eval] is its boolean
truth value in the current model (no theories!).
@raise Invalid_argument if the context is not checked or if it's
unsatisfiable.
@raise Error if the term isn't a known propositional atom. *)
val save_state : unit -> state
(** [save_state ()] returns a {b copy} of the current state of the solver.*)
val restore_state : state -> unit
(** [restore_state s] restores a previously saved state [s].*)
val entails : ?profiling:bool -> id:int -> Formula.t -> bool
(** [entails ~id f] returns [true] if the context of the solver entails
the formula [f]. It doesn't modify the context of the solver (the state
is saved when this function is called and restored on exit).*)
end
(** Functor to create several instances of the solver *)
module Make (Dummy : sig end) : Solver

240
old/sum.ml
View file

@ -1,240 +0,0 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon, Alain Mebsout *)
(* Mohamed Iguernelala *)
(* Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
open Format
open Sig
open Exception
module Sy = Symbols
module T = Term
module A = Literal
module L = List
module Hs = Hstring
module Ex = Explanation
type 'a abstract = Cons of Hs.t * Ty.t | Alien of 'a
module type ALIEN = sig
include Sig.X
val embed : r abstract -> r
val extract : r -> (r abstract) option
end
module Make(X : ALIEN) = struct
type t = X.r abstract
type r = X.r
let name = "Sum"
let unsolvable _ = false
let is_mine_a _ = false
let is_mine_symb = function
| Sy.Name(_, Sy.Constructor) -> true
| _ -> false
let fully_interpreted sb = true
let type_info = function
| Cons (_, ty) -> ty
| Alien x -> X.type_info x
let is_mine_type c = match type_info c with
| Ty.Tsum _ -> true
| _ -> false
let color _ = assert false
let print fmt = function
| Cons (hs,ty) -> fprintf fmt "%s" (Hs.view hs)
| Alien x -> fprintf fmt "%a" X.print x
let embed r =
match X.extract r with
| Some c -> c
| None -> Alien r
let is_mine = function
| Alien r -> r
| Cons(hs,ty) as c -> X.embed c
let compare c1 c2 =
match c1 , c2 with
| Cons (h1,ty1) , Cons (h2,ty2) ->
let n = Hs.compare h1 h2 in
if n <> 0 then n else Ty.compare ty1 ty2
| Alien r1, Alien r2 -> X.compare r1 r2
| Alien _ , Cons _ -> 1
| Cons _ , Alien _ -> -1
let hash = function
| Cons (h, ty) -> Hstring.hash h + 19 * Ty.hash ty
| Alien r -> X.hash r
let leaves _ = []
let subst p v c =
let cr = is_mine c in
if X.equal p cr then v
else
match c with
| Cons(hs,t) -> cr
| Alien r -> X.subst p v r
let make t = match T.view t with
| {T.f=Sy.Name(hs, Sy.Constructor); xs=[];ty=ty} ->
is_mine (Cons(hs,ty)), []
| _ -> assert false
let solve a b =
match embed a, embed b with
| Cons(c1,_) , Cons(c2,_) when Hs.equal c1 c2 -> []
| Cons(c1,_) , Cons(c2,_) -> raise Unsolvable
| Cons _ , Alien r2 -> [r2,a]
| Alien r1 , Cons _ -> [r1,b]
| Alien _ , Alien _ -> assert false
let term_extract _ = None
module Rel = struct
type r = X.r
exception Not_Cons
module Ex = Explanation
module MX = Map.Make(struct type t = X.r include X end)
module HSS = Set.Make (struct type t=Hs.t let compare = Hs.compare end)
type t = (HSS.t * Ex.t) MX.t
let empty () = MX.empty
module Debug = struct
let assume bol r1 r2 = ()
let print_env env = ()
end
let values_of r = match X.type_info r with
| Ty.Tsum (_,l) ->
Some (List.fold_left (fun st hs -> HSS.add hs st) HSS.empty l)
| _ -> None
let add_diseq hss sm1 sm2 dep env eqs =
match sm1, sm2 with
| Alien r , Cons(h,ty)
| Cons (h,ty), Alien r ->
let enum, ex = try MX.find r env with Not_found -> hss, Ex.empty in
let enum = HSS.remove h enum in
let ex = Ex.union ex dep in
if HSS.is_empty enum then raise (Inconsistent ex)
else
let env = MX.add r (enum, ex) env in
if HSS.cardinal enum = 1 then
let h' = HSS.choose enum in
env, (LSem (A.Eq(r, is_mine (Cons(h',ty)))), ex)::eqs
else env, eqs
| Alien r1 , Alien r2 -> env, eqs
| _ -> env, eqs
let add_eq hss sm1 sm2 dep env eqs =
match sm1, sm2 with
| Alien r, Cons(h,ty) | Cons (h,ty), Alien r ->
let enum, ex = try MX.find r env with Not_found -> hss, Ex.empty in
let ex = Ex.union ex dep in
if not (HSS.mem h enum) then raise (Inconsistent ex);
MX.add r (HSS.singleton h, ex) env, eqs
| Alien r1, Alien r2 ->
let enum1,ex1 = try MX.find r1 env with Not_found -> hss, Ex.empty in
let enum2,ex2 = try MX.find r2 env with Not_found -> hss, Ex.empty in
let ex = Ex.union dep (Ex.union ex1 ex2) in
let diff = HSS.inter enum1 enum2 in
if HSS.is_empty diff then raise (Inconsistent ex);
let env = MX.add r1 (diff, ex) env in
let env = MX.add r2 (diff, ex) env in
if HSS.cardinal diff = 1 then
let h' = HSS.choose diff in
let ty = X.type_info r1 in
env, (LSem (A.Eq(r1, is_mine (Cons(h',ty)))), ex)::eqs
else env, eqs
| _ -> env, eqs
let assume env la =
let aux bol r1 r2 dep env eqs = function
| None -> env, eqs
| Some hss ->
Debug.assume bol r1 r2;
if bol then
add_eq hss (embed r1) (embed r2) dep env eqs
else
add_diseq hss (embed r1) (embed r2) dep env eqs
in
Debug.print_env env;
let env, eqs =
List.fold_left
(fun (env,eqs) -> function
| A.Eq(r1,r2), _, ex ->
aux true r1 r2 ex env eqs (values_of r1)
| A.Distinct(false, [r1;r2]), _, ex ->
aux false r1 r2 ex env eqs (values_of r1)
| _ -> env, eqs
) (env,[]) la
in
env, { assume = eqs; remove = [] }
(* XXXXXX : TODO -> ajouter les explications dans les choix du
case split *)
let case_split env =
let acc = MX.fold
(fun r (hss, ex) acc ->
let sz = HSS.cardinal hss in
if sz = 1 then acc
else match acc with
| Some (n,r,hs) when n <= sz -> acc
| _ -> Some (sz, r, HSS.choose hss)
) env None
in
match acc with
| Some (n,r,hs) ->
let r' = is_mine (Cons(hs,X.type_info r)) in
[A.Eq(r, r'), Ex.empty, Num.Int n]
| None -> []
let query env a_ex =
try ignore(assume env [a_ex]); Sig.No
with Inconsistent expl -> Sig.Yes expl
let add env r = match embed r, values_of r with
| Alien r, Some hss ->
if MX.mem r env then env else
MX.add r (hss, Ex.empty) env
| _ -> env
end
end

25
old/sum.mli
View file

@ -1,25 +0,0 @@
(**************************************************************************)
(* *)
(* Cubicle *)
(* Combining model checking algorithms and SMT solvers *)
(* *)
(* Sylvain Conchon, Alain Mebsout *)
(* Mohamed Iguernelala *)
(* Universite Paris-Sud 11 *)
(* *)
(* Copyright 2011. This file is distributed under the terms of the *)
(* Apache Software License version 2.0 *)
(* *)
(**************************************************************************)
type 'a abstract
module type ALIEN = sig
include Sig.X
val embed : r abstract -> r
val extract : r -> (r abstract) option
end
module Make
(X : ALIEN) : Sig.THEORY with type r = X.r and type t = X.r abstract

91
old/symbols.ml
View file

@ -1,91 +0,0 @@
(**************************************************************************)
(* *)
(* 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 Hashcons
type operator =
| Plus | Minus | Mult | Div | Modulo
type name_kind = Ac | Constructor | Other
type t =
| True
| False
| Name of Hstring.t * name_kind
| Int of Hstring.t
| Real of Hstring.t
| Op of operator
| Var of Hstring.t
let name ?(kind=Other) s = Name (s, kind)
let var s = Var (Hstring.make s)
let int i = Int (Hstring.make i)
let real r = Real (Hstring.make r)
let is_ac = function
| Name(_, Ac) -> true
| _ -> false
let compare_kind k1 k2 = match k1, k2 with
| Ac , Ac -> 0
| Ac , _ -> 1
| _ , Ac -> -1
| 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 Hstring.compare n1 n2 else c
| Name _, _ -> -1
| _, Name _ -> 1
| Var n1, Var n2 -> Hstring.compare n1 n2
| Var _, _ -> -1
| _ ,Var _ -> 1
| Int i1, Int i2 -> Hstring.compare i1 i2
| Int _, _ -> -1
| _ ,Int _ -> 1
| _ -> Pervasives.compare s1 s2
let equal s1 s2 = compare s1 s2 = 0
let hash = function
| Name (n,Ac) -> Hstring.hash n * 19 + 1
| Name (n,_) -> Hstring.hash n * 19
| Var n (*| Int n*) -> Hstring.hash n * 19 + 1
| s -> Hashtbl.hash s
let to_string = function
| Name (n,_) -> Hstring.view n
| Var x -> "*var* "^(Hstring.view x)
| Int n -> Hstring.view n
| Real n -> Hstring.view n
| Op Plus -> "+"
| Op Minus -> "-"
| Op Mult -> "*"
| Op Div -> "/"
| Op Modulo -> "%"
| 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)

43
old/symbols.mli
View file

@ -1,43 +0,0 @@
(**************************************************************************)
(* *)
(* 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 operator =
| Plus | Minus | Mult | Div | Modulo
type name_kind = Ac | Constructor | Other
type t =
| True
| False
| Name of Hstring.t * name_kind
| Int of Hstring.t
| Real of Hstring.t
| Op of operator
| Var of Hstring.t
val name : ?kind:name_kind -> Hstring.t -> t
val var : string -> t
val int : string -> t
val real : string -> t
val is_ac : t -> bool
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

82
old/term.ml
View file

@ -1,82 +0,0 @@
(**************************************************************************)
(* *)
(* 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 Format
open Hashcons
module Sy = Symbols
type view = {f: Sy.t ; xs: t list; ty: Ty.t; tag: int}
and t = view
module H = struct
type t = view
let equal t1 t2 = try
Sy.equal t1.f t2.f
&& List.for_all2 (==) t1.xs t2.xs
&& Ty.equal t1.ty t2.ty
with Invalid_argument _ -> false
let hash t =
abs (List.fold_left
(fun acc x-> acc*19 +x.tag) (Sy.hash t.f + Ty.hash t.ty)
t.xs)
let tag tag x = {x with tag = tag}
end
module T = Make(H)
let view t = t
let rec print fmt t =
let {f=x; xs=l; ty=ty} = view t in
match x, l with
| Sy.Op op, [e1; e2] ->
fprintf fmt "(%a %a %a)" print e1 Sy.print x print e2
| _, [] -> fprintf fmt "%a" Sy.print x
| _, _ -> 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 (view t1).f, (view t2).f with
| (Sy.True | Sy.False ), (Sy.True | Sy.False ) -> c
| (Sy.True | Sy.False ), _ -> -1
| _, (Sy.True | Sy.False ) -> 1
| _,_ -> c
let make s l ty = T.hashcons {f=s;xs=l;ty=ty;tag=0 (* dumb_value *) }
let true_ = make (Sy.True) [] Ty.Tbool
let false_ = make (Sy.False) [] Ty.Tbool
let int i = make (Sy.int i) [] Ty.Tint
let real r = make (Sy.real r) [] Ty.Treal
let is_int t = (view t).ty= Ty.Tint
let is_real t = (view t).ty= Ty.Treal
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)

36
old/term.mli
View file

@ -1,36 +0,0 @@
(**************************************************************************)
(* *)
(* 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 t
type view = private {f: Symbols.t ; xs: t list; ty: Ty.t; tag : int}
val view : t -> view
val make : Symbols.t -> t list -> Ty.t -> t
val true_ : t
val false_ : t
val int : string -> t
val real : string -> t
val is_int : t -> bool
val is_real : t -> bool
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

58
old/ty.ml
View file

@ -1,58 +0,0 @@
(**************************************************************************)
(* *)
(* 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 Format
type t =
| Tint
| Treal
| Tbool
| Tabstract of Hstring.t
| Tsum of Hstring.t * Hstring.t list
let hash t =
match t with
| Tabstract s -> Hstring.hash s
| Tsum (s, l) ->
let h =
List.fold_left
(fun h x -> 13 * h + Hstring.hash x) (Hstring.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, _) ->
Hstring.equal s1 s2
| Tint, Tint | Treal, Treal | Tbool, Tbool -> true
| _ -> false
let compare t1 t2 =
match t1, t2 with
| Tabstract s1, Tabstract s2 ->
Hstring.compare s1 s2
| Tabstract _, _ -> -1 | _ , Tabstract _ -> 1
| Tsum (s1, _), Tsum(s2, _) ->
Hstring.compare s1 s2
| Tsum _, _ -> -1 | _ , Tsum _ -> 1
| t1, t2 -> Pervasives.compare t1 t2
let print fmt ty =
match ty with
| Tint -> fprintf fmt "int"
| Treal -> fprintf fmt "real"
| Tbool -> fprintf fmt "bool"
| Tabstract s -> fprintf fmt "%s" (Hstring.view s)
| Tsum (s, _) -> fprintf fmt "%s" (Hstring.view s)

24
old/ty.mli
View file

@ -1,24 +0,0 @@
(**************************************************************************)
(* *)
(* 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 t =
| Tint
| Treal
| Tbool
| Tabstract of Hstring.t
| Tsum of Hstring.t * Hstring.t list
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
val print : Format.formatter -> t -> unit

359
old/uf.ml
View file

@ -1,359 +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 Format
open Exception
open Sig
module type S = sig
type t
module R : Sig.X
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 : Sig.X ) = struct
module L = List
module HS = Hstring
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 =
L.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 =
L.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 x_solve env r1 r2 dep =
let rr1, ex_r1 = Env.find_or_normal_form env r1 in
let rr2, ex_r2 = Env.find_or_normal_form env r2 in
let dep = Ex.union dep (Ex.union ex_r1 ex_r2) in
if R.equal rr1 rr2 then begin
[] (* Remove rule *)
end
else
begin
ignore (Env.update_neqs rr1 rr2 dep env);
try R.solve rr1 rr2
with Unsolvable ->
raise (Inconsistent dep)
end
let rec ac_x eqs env tch =
if Queue.is_empty eqs then env, tch
else
let r1, r2, dep = Queue.pop eqs in
let sbs = x_solve env r1 r2 dep in
let env, tch = List.fold_left (ac_solve eqs dep) (env, tch) sbs in
ac_x eqs env tch
let union env r1 r2 dep =
let equations = Queue.create () in
Queue.push (r1,r2, dep) equations;
ac_x equations env []
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

42
old/uf.mli
View file

@ -1,42 +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 *)
(* *)
(**************************************************************************)
module type S = sig
type t
module R : Sig.X
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 : Sig.X ) : S with module R = X

83
old/use.ml
View file

@ -1,83 +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 *)
(* *)
(**************************************************************************)
module F = Format
module L = List
module T = Term
module S = Symbols
module ST = T.Set
(* module SA = Literal.LT.Set *)
module SA = Set.Make(struct
type t = Literal.LT.t * Explanation.t
let compare (s1,_) (s2,_) = Literal.LT.compare s1 s2
end)
type elt = ST.t * SA.t
module Make (X : Sig.X) = struct
let inter_tpl (x1,y1) (x2,y2) = ST.inter x1 x2, SA.inter y1 y2
let union_tpl (x1,y1) (x2,y2) = ST.union x1 x2, SA.union y1 y2
let bottom = Hstring.make "@bottom"
let leaves r =
let one, _ = X.make (T.make (Symbols.name bottom) [] Ty.Tint) in
match X.leaves r with [] -> [one] | l -> l
module G = Map.Make(struct type t = X.r include X end)
open G
type t = elt G.t
let find k m = try find k m with Not_found -> (ST.empty,SA.empty)
let add_term k t mp =
let g_t,g_a = find k mp in add k (ST.add t g_t,g_a) mp
let up_add g t rt lvs =
let g = if mem rt g then g else add rt (ST.empty, SA.empty) g in
L.fold_left (fun g x -> add_term x t g) g lvs
let congr_add g lvs =
match lvs with
[] -> ST.empty
| x::ls ->
L.fold_left
(fun acc y -> ST.inter (fst(find y g)) acc)
(fst(find x g)) ls
let up_close_up g p v =
let lvs = leaves v in
let g_p = find p g in
L.fold_left (fun gg l -> add l (union_tpl g_p (find l g)) gg) g lvs
let congr_close_up g p touched =
let inter = function
[] -> (ST.empty, SA.empty)
| rx::l ->
L.fold_left (fun acc x ->inter_tpl acc (find x g))(find rx g) l
in
L.fold_left
(fun (st,sa) tch -> union_tpl (st,sa)(inter (leaves tch)))
(find p g) touched
let print g = ()
let mem = G.mem
let add = G.add
let empty = G.empty
end

38
old/use.mli
View file

@ -1,38 +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 *)
(* *)
(**************************************************************************)
module T : sig type t = Term.t end
module S : sig type t = Symbols.t end
module ST : sig type elt = T.t type t = Term.Set.t end
module SA : Set.S with type elt = Literal.LT.t * Explanation.t
type elt = ST.t * SA.t
module Make :
functor (X : Sig.X) ->
sig
type t
val empty : t
val find : X.r -> t -> elt
val add : X.r -> elt -> t -> t
val mem : X.r -> t -> bool
val print : t -> unit
val up_add : t -> ST.elt -> X.r -> X.r list -> t
val congr_add : t -> X.r list -> ST.t
val up_close_up :t -> X.r -> X.r -> t
val congr_close_up : t -> X.r -> X.r list -> elt
end