diff --git a/.merlin b/.merlin index beb445b8..d7ed7f73 100644 --- a/.merlin +++ b/.merlin @@ -1,6 +1,7 @@ S src/core S src/solver -S src/example +S src/sat +S src/smt S src/backend S src/util S src/util/smtlib @@ -9,7 +10,8 @@ S tests B _build/src/ B _build/src/core B _build/src/solver -B _build/src/example +B _build/src/sat +B _build/src/smt B _build/src/util B _build/src/util/smtlib B _build/src/backend diff --git a/META b/META index f2ed910c..993b7f01 100644 --- a/META +++ b/META @@ -1,3 +1,4 @@ +# meta name="msat" version="dev" description="MSAT is a modular SAT solver, plus extensions" @@ -6,3 +7,25 @@ archive(byte) = "msat.cma" archive(byte, plugin) = "msat.cma" archive(native) = "msat.cmxa" archive(native, plugin) = "msat.cmxs" + +package "sat" ( + version = "dev" + description = "SAT solver instance" + requires = "msat" + archive(byte) = "msat_sat.cma" + archive(byte, plugin) = "msat_sat.cma" + archive(native) = "msat_sat.cmxa" + archive(native, plugin) = "msat_sat.cmxs" + exists_if = "msat_sat.cma" +) + +package "smt" ( + version = "dev" + description = "SMT solver instance" + requires = "msat" + archive(byte) = "msat_smt.cma" + archive(byte, plugin) = "msat_smt.cma" + archive(native) = "msat_smt.cmxa" + archive(native, plugin) = "msat_smt.cmxs" + exists_if = "msat_smt.cma" +) diff --git a/Makefile b/Makefile index 406b5b38..92f4bc5e 100644 --- a/Makefile +++ b/Makefile @@ -3,12 +3,20 @@ LOG=build.log COMP=ocamlbuild -log $(LOG) -use-ocamlfind FLAGS= -DOC=msat.docdir/index.html +DOC=msat.docdir/index.html msat_smt.docdir/index.html BIN=main.native TEST_BIN=tests/test_api.native -NAME=msat -LIB=$(addprefix $(NAME), .cma .cmxa .cmxs) +NAME_OCAMLFIND=msat +NAME_BIN=msat +NAME_CORE=msat +NAME_SAT=msat_sat +NAME_SMT=msat_smt + +LIB_CORE=$(addprefix $(NAME_CORE), .cma .cmxa .cmxs) +LIB_SAT=$(addprefix $(NAME_SAT), .cma .cmxa .cmxs) +LIB_SMT=$(addprefix $(NAME_SMT), .cma .cmxa .cmxs) +LIB=$(LIB_CORE) $(LIB_SAT) $(LIB_SMT) all: lib test @@ -20,7 +28,7 @@ doc: bin: $(COMP) $(FLAGS) $(BIN) - cp $(BIN) $(NAME) && rm $(BIN) + cp $(BIN) $(NAME_BIN) && rm $(BIN) test_bin: $(COMP) $(FLAGS) $(TEST_BIN) @@ -44,16 +52,26 @@ log: clean: $(COMP) -clean -TO_INSTALL=META $(addprefix _build/src/,$(LIB) $(NAME).a $(NAME).cmi) +ALL_NAMES = $(NAME_CORE) $(NAME_SAT) $(NAME_SMT) +TO_INSTALL_LIB=$(addsuffix .a, $(ALL_NAMES)) \ + $(addsuffix .cmi, $(ALL_NAMES)) +TO_INSTALL=META $(addprefix _build/src/,$(LIB) $(TO_INSTALL_LIB)) install: lib - ocamlfind install msat $(TO_INSTALL) + ocamlfind install $(NAME_OCAMLFIND) $(TO_INSTALL) uninstall: - ocamlfind remove msat + ocamlfind remove $(NAME_OCAMLFIND) reinstall: all - ocamlfind remove msat || true - ocamlfind install msat $(TO_INSTALL) + ocamlfind remove $(NAME_OCAMLFIND) || true + ocamlfind install $(NAME_OCAMLFIND) $(TO_INSTALL) + +watch: + while find src/ -print0 | xargs -0 inotifywait -e delete_self -e modify ; do \ + echo "============ at `date` ==========" ; \ + sleep 0.1; \ + make all; \ + done .PHONY: clean doc all bench install uninstall reinstall enable_log disable_log bin test diff --git a/_tags b/_tags index c918133e..6511633d 100644 --- a/_tags +++ b/_tags @@ -9,7 +9,8 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20) : include : include : include -: include +: include +: include : include : include @@ -18,7 +19,8 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20) : for-pack(Msat) : for-pack(Msat) : for-pack(Msat) -: for-pack(Msat) +: for-pack(Msat_sat) +: for-pack(Msat_smt) # more warnings : warn_K, warn_Y, warn_X diff --git a/src/example/cc.ml b/src/example/cc.ml deleted file mode 100644 index cbfa7d97..00000000 --- a/src/example/cc.ml +++ /dev/null @@ -1,99 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module Make(T : Sig.OrderedType) = struct - - module M = Map.Make(T) - module U = Unionfind.Make(T) - - exception Unsat of (T.t * T.t * (T.t list)) - - type t = { - repr : U.t; - expl : T.t M.t; - size : int M.t; - } - - let empty = { - repr = U.empty; - expl = M.empty; - size = M.empty; - } - - let repr t a = U.find t.repr a - - let map_find m v default = try M.find v m with Not_found -> default - let find_parent v m = map_find m v v - - let rev_root m root = - let rec aux m curr next = - if T.compare curr next = 0 then - m, curr - else - let parent = find_parent next m in - let m' = M.add next curr (M.remove curr m) in - aux m' next parent - in - aux m root (find_parent root m) - - let rec root m acc curr = - let parent = find_parent curr m in - if T.compare curr parent = 0 then - curr :: acc - else - root m (curr :: acc) parent - - let expl t a b = - let rec aux last = function - | x :: r, y :: r' when T.compare x y = 0 -> - aux (Some x) (r, r') - | l, l' -> begin match last with - | Some z -> List.rev_append (z :: l) l' - | None -> List.rev_append l l' - end - in - aux None (root t.expl [] a, root t.expl [] b) - - let add_eq_aux t i j = - if T.compare (U.find t.repr i) (U.find t.repr j) = 0 then - t - else - let m, old_root_i = rev_root t.expl i in - let m, old_root_j = rev_root m j in - let nb_i = map_find t.size old_root_i 0 in - let nb_j = map_find t.size old_root_j 0 in - if nb_i < nb_j then { - repr = t.repr; - expl = M.add i j m; - size = M.add j (nb_i + nb_j + 1) t.size; } - else { - repr = t.repr; - expl = M.add j i m; - size = M.add i (nb_i + nb_j + 1) t.size; } - - let add_eq t i j = - let t' = add_eq_aux t i j in - try - let u' = U.union t.repr i j in - { t' with repr = u' } - with U.Unsat (a, b) -> - raise (Unsat (a, b, expl t' a b)) - - let add_neq t i j = - try - let u' = U.forbid t.repr i j in - { t with repr = u' } - with U.Unsat (a, b) -> - raise (Unsat (a, b, expl t a b)) - - let are_neq t a b = - try - ignore (U.union t.repr a b); - false - with U.Unsat _ -> - true - -end diff --git a/src/example/cc.mli b/src/example/cc.mli deleted file mode 100644 index 005264d8..00000000 --- a/src/example/cc.mli +++ /dev/null @@ -1,18 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - -module Make(T : Sig.OrderedType) : sig - type t - - exception Unsat of (T.t * T.t * (T.t list)) - - val empty : t - val add_eq : t -> T.t -> T.t -> t - val add_neq : t -> T.t -> T.t -> t - - val repr : t -> T.t -> T.t - val are_neq : t -> T.t -> T.t -> bool -end diff --git a/src/example/sig.mli b/src/example/sig.mli deleted file mode 100644 index 1441de22..00000000 --- a/src/example/sig.mli +++ /dev/null @@ -1,13 +0,0 @@ -(* -MSAT is free software, using the Apache license, see file LICENSE -Copyright 2014 Guillaume Bury -Copyright 2014 Simon Cruanes -*) - - -module type OrderedType = sig - (** Signature for ordered types (mainly for use in Map.Make) *) - - type t - val compare : t -> t -> int -end diff --git a/src/main.ml b/src/main.ml index 866c29c0..16a0ed8d 100644 --- a/src/main.ml +++ b/src/main.ml @@ -5,9 +5,10 @@ Copyright 2014 Simon Cruanes *) module F = Expr -module T = Cnf.S -module Smt = Smt.Make(struct end) -module Mcsat = Mcsat.Make(struct end) +module T = Msat_smt.Cnf.S +module Sat = Msat_sat.Sat.Make(struct end) +module Smt = Msat_smt.Smt.Make(struct end) +module Mcsat = Msat_smt.Mcsat.Make(struct end) exception Incorrect_model exception Out_of_time @@ -26,6 +27,7 @@ type sat_output = | Dot type solver = + | Sat | Smt | Mcsat @@ -43,6 +45,7 @@ let output_list = [ "dk", Dedukti; ] let solver_list = [ + "sat", Sat; "smt", Smt; "mcsat", Mcsat; ] diff --git a/src/msat.mlpack b/src/msat.mlpack index bf7c053c..b07295d9 100644 --- a/src/msat.mlpack +++ b/src/msat.mlpack @@ -19,20 +19,11 @@ Mcsolver Solver_types # Backends +Backend_intf Dot Dedukti # Auxiliary modules Res Tseitin - -# Sat/Smt modules -Expr -Cnf -Sat -Mcsat -Cc -Sig -Smt -Unionfind - +Hashcons diff --git a/src/msat.odocl b/src/msat.odocl index 09f5e4ce..ff4f7d94 100644 --- a/src/msat.odocl +++ b/src/msat.odocl @@ -13,6 +13,7 @@ solver/Tseitin_intf # Main modules core/Res +core/Res_intf core/Internal core/External core/Solver_types @@ -20,13 +21,12 @@ core/Solver_types solver/Solver solver/Mcsolver solver/Tseitin +solver/Tseitin_intf # Backends backend/Dot backend/Dedukti backend/Backend_intf -# Examples -example/Sat -example/Smt - +# Auxiliary +util/Hashcons diff --git a/src/msat_sat.mlpack b/src/msat_sat.mlpack new file mode 100644 index 00000000..492570c2 --- /dev/null +++ b/src/msat_sat.mlpack @@ -0,0 +1,2 @@ +Sat + diff --git a/src/msat_sat.odocl b/src/msat_sat.odocl new file mode 100644 index 00000000..1fb3c3bf --- /dev/null +++ b/src/msat_sat.odocl @@ -0,0 +1,3 @@ + +smt/Sat + diff --git a/src/msat_smt.mlpack b/src/msat_smt.mlpack new file mode 100644 index 00000000..cfd8b1ba --- /dev/null +++ b/src/msat_smt.mlpack @@ -0,0 +1,12 @@ +Cc +Cnf +Explanation +Expr +ID +Literal +Mcsat +Smt +Symbols +Term +Ty +Unionfind diff --git a/src/msat_smt.odocl b/src/msat_smt.odocl new file mode 100644 index 00000000..ab9aa609 --- /dev/null +++ b/src/msat_smt.odocl @@ -0,0 +1,17 @@ + +smt/Smt + +# support +smt/Cc +smt/Cnf +smt/Explanation +smt/Expr +smt/ID +smt/Sat +smt/Literal +smt/Mcsat +smt/Symbols +smt/Term +smt/Ty +smt/Unionfind + diff --git a/src/example/sat.ml b/src/sat/sat.ml similarity index 99% rename from src/example/sat.ml rename to src/sat/sat.ml index fcf4ed34..448cecb4 100644 --- a/src/example/sat.ml +++ b/src/sat/sat.ml @@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +open Msat + module FI = Formula_intf module Fsat = struct diff --git a/src/example/sat.mli b/src/sat/sat.mli similarity index 99% rename from src/example/sat.mli rename to src/sat/sat.mli index bcc87f68..06e4185b 100644 --- a/src/example/sat.mli +++ b/src/sat/sat.mli @@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +open Msat + module Fsat : sig include Formula_intf.S with type t = private int diff --git a/src/smt/ID.ml b/src/smt/ID.ml new file mode 100644 index 00000000..fb0f64d4 --- /dev/null +++ b/src/smt/ID.ml @@ -0,0 +1,39 @@ +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) + +type t = { + id: int; + name: string; +} + +let make = + let n = ref 0 in + fun name -> + let x = { id= !n; name; } in + incr n; + x + +let copy {name;_} = make name + +let to_string id = id.name + +let equal a b = a.id=b.id +let compare a b = Pervasives.compare a.id b.id +let hash a = a.id land max_int +let pp out a = Format.fprintf out "%s/%d" a.name a.id +let pp_name out a = Format.pp_print_string out a.name + +module AsKey = struct + type t_ = t + type t = t_ + let equal = equal + let compare = compare + let hash = hash +end + +module Map = Map.Make(AsKey) +module Set = Set.Make(AsKey) +module Tbl = Hashtbl.Make(AsKey) diff --git a/src/smt/ID.mli b/src/smt/ID.mli new file mode 100644 index 00000000..f0ac869d --- /dev/null +++ b/src/smt/ID.mli @@ -0,0 +1,25 @@ + +(* +MSAT is free software, using the Apache license, see file LICENSE +Copyright 2016 Guillaume Bury +Copyright 2016 Simon Cruanes +*) + +(** {1 Unique Identifiers} *) + +type t + +val make : string -> t +val copy : t -> t + +val to_string : t -> string + +val equal : t -> t -> bool +val compare : t -> t -> int +val hash : t -> int + +val pp_name : Format.formatter -> t -> unit + +module Map : Map.S with type key = t +module Set : Set.S with type elt = t +module Tbl : Hashtbl.S with type key = t diff --git a/src/smt/cc.ml b/src/smt/cc.ml new file mode 100644 index 00000000..a4114398 --- /dev/null +++ b/src/smt/cc.ml @@ -0,0 +1,517 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon, Evelyne Contejean *) +(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) +(* CNRS, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +open Msat + +let max_split = 1000000 + +let cc_active = ref true + +type answer = Yes of Explanation.t | No + +module type S = sig + type t + + val empty : unit -> t + val assume : cs:bool -> + Literal.LT.t -> Explanation.t -> t -> t * Term.Set.t * int + val query : Literal.LT.t -> t -> answer + val class_of : t -> Term.t -> Term.t list +end + +module Make (Dummy : sig end) = struct + + module Ex = Explanation + module Uf = Uf.Make(Term) + module T = Term + module A = Literal + module LR = A.Make(struct type t = X.r include X end) + module SetT = Term.Set + module S = Symbols + + module SetX = Set.Make(struct type t = X.r let compare = X.compare end) + + (* module Uf = Pptarjan.Uf *) + + type env = { + uf : Uf.t ; + relation : X.Rel.t + } + + type choice_sign = + | CPos of int (* The explication of this choice *) + | CNeg (* The choice has been already negated *) + + type t = { + gamma : env; + gamma_finite : env ; + choices : (X.r A.view * Num.num * choice_sign * Ex.t) list; + (** the choice, the size, choice_sign, the explication set, + the explication for this choice. *) + } + + module Print = struct + + let begin_case_split () = () + + let end_case_split () = () + + let cc r1 r2 = () + + let make_cst t ctx = () + + let add_to_use t = () + + let lrepr fmt = List.iter (Format.fprintf fmt "%a " X.print) + + let leaves t lvs = () + + let contra_congruence a ex = () + + let split_size sz = () + + let split_backtrack neg_c ex_c = () + + let split_assume c ex_c = () + + let split_backjump c dep = () + + let assume_literal sa = () + + let congruent a ex = () + + let query a = () + + end + + let bottom = Hstring.make "@bottom" + let one, _ = X.make (Term.make (S.name bottom) [] Ty.Tint) + + let concat_leaves uf l = + let rec concat_rec acc t = + match X.leaves (fst (Uf.find uf t)) , acc with + [] , _ -> one::acc + | res, [] -> res + | res , _ -> List.rev_append res acc + in + match List.fold_left concat_rec [] l with + [] -> [one] + | res -> res + + let are_equal env ex t1 t2 = + if T.equal t1 t2 then ex + else match Uf.are_equal env.uf t1 t2 with + | Yes dep -> Ex.union ex dep + | No -> raise Exit + + let equal_only_by_congruence env ex t1 t2 acc = + if T.equal t1 t2 then acc + else + let {T.f=f1; xs=xs1; ty=ty1} = T.view t1 in + if X.fully_interpreted f1 then acc + else + let {T.f=f2; xs=xs2; ty=ty2} = T.view t2 in + if Symbols.equal f1 f2 && Ty.equal ty1 ty2 then + try + let ex = List.fold_left2 (are_equal env) ex xs1 xs2 in + let a = A.LT.make (A.Eq(t1, t2)) in + Print.congruent a ex; + (LTerm a, ex) :: acc + with Exit -> acc + else acc + + let congruents env t1 s acc ex = + SetT.fold (equal_only_by_congruence env ex t1) s acc + + let fold_find_with_explanation find ex l = + List.fold_left + (fun (lr, ex) t -> let r, ex_r = find t in r::lr, Ex.union ex_r ex) + ([], ex) l + + let view find va ex_a = + match va with + | A.Eq (t1, t2) -> + let r1, ex1 = find t1 in + let r2, ex2 = find t2 in + let ex = Ex.union (Ex.union ex1 ex2) ex_a in + A.Eq(r1, r2), ex + | A.Distinct (b, lt) -> + let lr, ex = fold_find_with_explanation find ex_a lt in + A.Distinct (b, lr), ex + | A.Builtin(b, s, l) -> + let lr, ex = fold_find_with_explanation find ex_a l in + A.Builtin(b, s, List.rev lr), ex + + let term_canonical_view env a ex_a = + view (Uf.find env.uf) (A.LT.view a) ex_a + + let canonical_view env a ex_a = view (Uf.find_r env.uf) a ex_a + + let new_facts_by_contra_congruence env r bol ex = + match X.term_extract r with + | None -> [] + | Some t1 -> + match T.view t1 with + | {T.f=f1 ; xs=[x]} -> + List.fold_left + (fun acc t2 -> + match T.view t2 with + | {T.f=f2 ; xs=[y]} when S.equal f1 f2 -> + let a = A.LT.make (A.Distinct (false, [x; y])) in + let dist = LTerm a in + begin match Uf.are_distinct env.uf t1 t2 with + | Yes ex' -> + let ex_r = Ex.union ex ex' in + Print.contra_congruence a ex_r; + (dist, ex_r) :: acc + | No -> assert false + end + | _ -> acc + ) [] (Uf.class_of env.uf bol) + | _ -> [] + + let contra_congruence = + let true_,_ = X.make T.true_ in + let false_, _ = X.make T.false_ in + fun env r ex -> + if X.equal (fst (Uf.find_r env.uf r)) true_ then + new_facts_by_contra_congruence env r T.false_ ex + else if X.equal (fst (Uf.find_r env.uf r)) false_ then + new_facts_by_contra_congruence env r T.true_ ex + else [] + + let clean_use = + List.fold_left + (fun env (a, ex) -> + match a with + | LSem _ -> assert false + | LTerm t -> + begin + match A.LT.view t with + | A.Distinct (_, lt) + | A.Builtin (_, _, lt) -> + let lvs = concat_leaves env.uf lt in + List.fold_left + (fun env rx -> + let st, sa = Use.find rx env.use in + let sa = SetA.remove (t, ex) sa in + { env with use = Use.add rx (st,sa) env.use } + ) env lvs + | _ -> assert false + end) + + let rec congruence_closure env r1 r2 ex = + Print.cc r1 r2; + let uf, res = Uf.union env.uf r1 r2 ex in + List.fold_left + (fun (env, l) (p, touched, v) -> + (* we look for use(p) *) + let p_t, p_a = Use.find p env.use in + + (* we compute terms and atoms to consider for congruence *) + let repr_touched = List.map (fun (_,a,_) -> a) touched in + let st_others, sa_others = Use.congr_close_up env.use p repr_touched in + + (* we update use *) + let nuse = Use.up_close_up env.use p v in + Use.print nuse; + + (* we check the congruence of the terms. *) + let env = {env with use=nuse} in + let new_eqs = + SetT.fold (fun t l -> congruents env t st_others l ex) p_t l in + let touched_atoms = + List.map (fun (x,y,e)-> (LSem(A.Eq(x, y)), e)) touched + in + let touched_atoms = SetA.fold (fun (a, ex) acc -> + (LTerm a, ex)::acc) p_a touched_atoms in + let touched_atoms = SetA.fold (fun (a, ex) acc -> + (LTerm a, ex)::acc) sa_others touched_atoms in + env, new_eqs @ touched_atoms + + ) ({env with uf=uf}, []) res + + let replay_atom env sa = + let relation, result = X.Rel.assume env.relation sa in + let env = { env with relation = relation } in + let env = clean_use env result.remove in + env, result.assume + + let rec add_term env choices t ex = + (* nothing to do if the term already exists *) + if Uf.mem env.uf t then env, choices + else begin + Print.add_to_use t; + (* we add t's arguments in env *) + let {T.f = f; xs = xs} = T.view t in + let env, choices = + List.fold_left (fun (env, ch) t -> add_term env ch t ex) + (env, choices) xs + in + (* we update uf and use *) + let nuf, ctx = Uf.add env.uf t in + Print.make_cst t ctx; + let rt, _ = Uf.find nuf t in (* XXX : ctx only in terms *) + + if !cc_active then + let lvs = concat_leaves nuf xs in + let nuse = Use.up_add env.use t rt lvs in + + (* If finitetest is used we add the term to the relation *) + let rel = X.Rel.add env.relation rt in + Use.print nuse; + + (* we compute terms to consider for congruence *) + (* we do this only for non-atomic terms with uninterpreted head-symbol *) + let st_uset = Use.congr_add nuse lvs in + + (* we check the congruence of each term *) + let env = {uf = nuf; use = nuse; relation = rel} in + let ct = congruents env t st_uset [] ex in + let ct = (List.map (fun lt -> LTerm lt, ex) ctx) @ ct in + assume_literal env choices ct + else + let rel = X.Rel.add env.relation rt in + let env = {env with uf = nuf; relation = rel} in + env, choices + end + + and add env choices a ex = + match A.LT.view a with + | A.Eq (t1, t2) -> + let env, choices = add_term env choices t1 ex in + add_term env choices t2 ex + | A.Distinct (_, lt) + | A.Builtin (_, _, lt) -> + let env, choices = List.fold_left + (fun (env, ch) t-> add_term env ch t ex) (env, choices) lt in + let lvs = concat_leaves env.uf lt in (* A verifier *) + let env = List.fold_left + (fun env rx -> + let st, sa = Use.find rx env.use in + { env with + use = Use.add rx (st,SetA.add (a, ex) sa) env.use } + ) env lvs + in + env, choices + + and semantic_view env choices la = + List.fold_left + (fun (env, choices, lsa) (a, ex) -> + match a with + | LTerm a -> + let env, choices = add env choices a ex in + let sa, ex = term_canonical_view env a ex in + env, choices, (sa, Some a, ex)::lsa + + (* XXX si on fait canonical_view pour + A.Distinct, la theorie des tableaux + part dans les choux *) + | LSem (A.Builtin _ (*| A.Distinct _*) as sa) -> + let sa, ex = canonical_view env sa ex in + env, choices, (sa, None, ex)::lsa + | LSem sa -> + env, choices, (sa, None, ex)::lsa) + (env, choices, []) la + + and assume_literal env choices la = + if la = [] then env, choices + else + let env, choices, lsa = semantic_view env choices la in + let env, choices = + List.fold_left + (fun (env, choices) (sa, _, ex) -> + Print.assume_literal sa; + match sa with + | A.Eq(r1, r2) -> + if !cc_active then + let env, l = congruence_closure env r1 r2 ex in + let env, choices = assume_literal env choices l in + let env, choices = + assume_literal env choices (contra_congruence env r1 ex) + in + assume_literal env choices (contra_congruence env r2 ex) + else + {env with uf = fst(Uf.union env.uf r1 r2 ex)}, choices + | A.Distinct (false, lr) -> + if Uf.already_distinct env.uf lr then env, choices + else + {env with uf = Uf.distinct env.uf lr ex}, choices + | A.Distinct (true, _) -> assert false + | A.Builtin _ -> env, choices) + (env, choices) lsa + in + let env, l = replay_atom env lsa in + assume_literal env (choices@l) l + + let look_for_sat ?(bad_last=No) ch t base_env l = + let rec aux ch bad_last dl base_env li = + match li, bad_last with + | [], _ -> + begin + match X.Rel.case_split base_env.relation with + | [] -> + { t with gamma_finite = base_env; choices = List.rev dl }, ch + | l -> + let l = + List.map + (fun (c, ex_c, size) -> + let exp = Ex.fresh_exp () in + let ex_c_exp = Ex.add_fresh exp ex_c in + (* A new explanation in order to track the choice *) + (c, size, CPos exp, ex_c_exp)) l in + let sz = + List.fold_left + (fun acc (a,s,_,_) -> + Num.mult_num acc s) (Num.Int 1) (l@dl) in + Print.split_size sz; + if Num.le_num sz max_split then aux ch No dl base_env l + else + { t with gamma_finite = base_env; choices = List.rev dl }, ch + end + | ((c, size, CNeg, ex_c) as a)::l, _ -> + let base_env, ch = assume_literal base_env ch [LSem c, ex_c] in + aux ch bad_last (a::dl) base_env l + + (** This optimisation is not correct with the current explanation *) + (* | [(c, size, CPos exp, ex_c)], Yes dep -> *) + (* let neg_c = LR.neg (LR.make c) in *) + (* let ex_c = Ex.union ex_c dep in *) + (* Print.split_backtrack neg_c ex_c; *) + (* aux ch No dl base_env [LR.view neg_c, Num.Int 1, CNeg, ex_c] *) + + | ((c, size, CPos exp, ex_c_exp) as a)::l, _ -> + try + Print.split_assume (LR.make c) ex_c_exp; + let base_env, ch = assume_literal base_env ch [LSem c, ex_c_exp] in + aux ch bad_last (a::dl) base_env l + with Exception.Inconsistent dep -> + match Ex.remove_fresh exp dep with + | None -> + (* The choice doesn't participate to the inconsistency *) + Print.split_backjump (LR.make c) dep; + raise (Exception.Inconsistent dep) + | Some dep -> + (* The choice participates to the inconsistency *) + let neg_c = LR.neg (LR.make c) in + Print.split_backtrack neg_c dep; + aux ch No dl base_env [LR.view neg_c, Num.Int 1, CNeg, dep] + in + aux ch bad_last (List.rev t.choices) base_env l + + let try_it f t = + Print.begin_case_split (); + let r = + try + if t.choices = [] then look_for_sat [] t t.gamma [] + else + try + let env, lt = f t.gamma_finite in + look_for_sat lt t env [] + with Exception.Inconsistent dep -> + look_for_sat ~bad_last:(Yes dep) + [] { t with choices = []} t.gamma t.choices + with Exception.Inconsistent d -> + Print.end_case_split (); + raise (Exception.Inconsistent d) + in + Print.end_case_split (); r + + let extract_from_semvalues = + List.fold_left + (fun acc r -> + match X.term_extract r with Some t -> SetT.add t acc | _ -> acc) + + let extract_terms_from_choices = + List.fold_left + (fun acc (a, _, _, _) -> + match a with + | A.Eq(r1, r2) -> extract_from_semvalues acc [r1; r2] + | A.Distinct (_, l) -> extract_from_semvalues acc l + | _ -> acc) + + let extract_terms_from_assumed = + List.fold_left + (fun acc (a, _) -> + match a with + | LTerm r -> begin + match Literal.LT.view r with + | Literal.Eq (t1, t2) -> + SetT.add t1 (SetT.add t2 acc) + | Literal.Distinct (_, l) | Literal.Builtin (_, _, l) -> + List.fold_right SetT.add l acc + end + | _ -> acc) + + let assume ~cs a ex t = + let a = LTerm a in + let gamma, ch = assume_literal t.gamma [] [a, ex] in + let t = { t with gamma = gamma } in + let t, ch = + if cs then try_it (fun env -> assume_literal env ch [a, ex] ) t + else t, ch + in + let choices = extract_terms_from_choices SetT.empty t.choices in + let all_terms = extract_terms_from_assumed choices ch in + t, all_terms, 1 + + let class_of t term = Uf.class_of t.gamma.uf term + + let add_and_process a t = + let aux a ex env = + let gamma, l = add env [] a ex in assume_literal gamma [] l + in + let gamma, _ = aux a Ex.empty t.gamma in + let t = { t with gamma = gamma } in + let t, _ = try_it (aux a Ex.empty) t in + Use.print t.gamma.use; t + + let query a t = + Print.query a; + try + match A.LT.view a with + | A.Eq (t1, t2) -> + let t = add_and_process a t in + Uf.are_equal t.gamma.uf t1 t2 + + | A.Distinct (false, [t1; t2]) -> + let na = A.LT.neg a in + let t = add_and_process na t in (* na ? *) + Uf.are_distinct t.gamma.uf t1 t2 + + | A.Distinct _ -> + assert false (* devrait etre capture par une analyse statique *) + + | _ -> + let na = A.LT.neg a in + let t = add_and_process na t in + let env = t.gamma in + let rna, ex_rna = term_canonical_view env na Ex.empty in + X.Rel.query env.relation (rna, Some na, ex_rna) + with Exception.Inconsistent d -> Yes d + + let empty () = + let env = { + use = Use.empty ; + uf = Uf.empty ; + relation = X.Rel.empty (); + } + in + let t = { gamma = env; gamma_finite = env; choices = [] } in + let t, _, _ = + assume ~cs:false + (A.LT.make (A.Distinct (false, [T.true_; T.false_]))) Ex.empty t + in t + +end diff --git a/src/smt/cc.mli b/src/smt/cc.mli new file mode 100644 index 00000000..935ed2ea --- /dev/null +++ b/src/smt/cc.mli @@ -0,0 +1,37 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon, Evelyne Contejean *) +(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) +(* CNRS, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +open Msat + +val cc_active : bool ref + +type answer = Yes of Explanation.t | No + +module type S = sig + type t + + val empty : unit -> t + + val assume : + cs:bool -> + Literal.LT.t -> + Explanation.t -> + t -> t * Term.Set.t * int + + val query : Literal.LT.t -> t -> answer + + val class_of : t -> Term.t -> Term.t list +end + +module Make (Dummy : sig end) : S diff --git a/src/example/cnf.ml b/src/smt/cnf.ml similarity index 93% rename from src/example/cnf.ml rename to src/smt/cnf.ml index f778231a..999271ac 100644 --- a/src/example/cnf.ml +++ b/src/smt/cnf.ml @@ -4,4 +4,6 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +open Msat + module S = Tseitin.Make(Expr) diff --git a/src/example/cnf.mli b/src/smt/cnf.mli similarity index 94% rename from src/example/cnf.mli rename to src/smt/cnf.mli index b0eae539..6eb68976 100644 --- a/src/example/cnf.mli +++ b/src/smt/cnf.mli @@ -4,4 +4,6 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +open Msat + module S : Tseitin.S with type atom = Expr.Formula.t diff --git a/src/smt/explanation.ml b/src/smt/explanation.ml new file mode 100644 index 00000000..3646c112 --- /dev/null +++ b/src/smt/explanation.ml @@ -0,0 +1,68 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Stephane Lescuyer *) +(* INRIA, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +type atom = Literal.LT.t + +type exp = Atom of atom | Fresh of int + +module S = + Set.Make + (struct + type t = exp + let compare a b = match a,b with + | Atom _, Fresh _ -> -1 + | Fresh _, Atom _ -> 1 + | Fresh i1, Fresh i2 -> i1 - i2 + | Atom a, Atom b -> a.aid - b.aid + end) + +type t = S.t + +let singleton e = S.singleton (Atom e) + +let empty = S.empty + +let union s1 s2 = S.union s1 s2 + +let iter_atoms f s = + S.iter (fun e -> match e with + | Fresh _ -> () + | Atom a -> f a) s + +let fold_atoms f s acc = + S.fold (fun e acc -> match e with + | Fresh _ -> acc + | Atom a -> f a acc) s acc + +let merge e1 e2 = e1 + + +let fresh_exp = + let r = ref (-1) in + fun () -> incr r; !r + +let remove_fresh i s = + let fi = Fresh i in + if S.mem fi s then Some (S.remove fi s) + else None + +let add_fresh i = S.add (Fresh i) + + +let print fmt ex = + fprintf fmt "{"; + S.iter (function + | Atom a -> fprintf fmt "%a, " Debug.atom a + | Fresh i -> fprintf fmt "Fresh%d " i) ex; + fprintf fmt "}" diff --git a/src/smt/explanation.mli b/src/smt/explanation.mli new file mode 100644 index 00000000..b362b0c3 --- /dev/null +++ b/src/smt/explanation.mli @@ -0,0 +1,39 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Stephane Lescuyer *) +(* INRIA, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +type t + +type exp + +type atom = Literal.LT.t + +val empty : t + +val singleton : atom-> t + +val union : t -> t -> t + +val merge : t -> t -> t + +val iter_atoms : (atom -> unit) -> t -> unit + +val fold_atoms : (atom -> 'a -> 'a ) -> t -> 'a -> 'a + +val fresh_exp : unit -> int + +val remove_fresh : int -> t -> t option + +val add_fresh : int -> t -> t + +val print : Format.formatter -> t -> unit diff --git a/src/example/expr.ml b/src/smt/expr.ml similarity index 50% rename from src/example/expr.ml rename to src/smt/expr.ml index 72eef2e1..dda3d7fc 100644 --- a/src/example/expr.ml +++ b/src/smt/expr.ml @@ -3,36 +3,56 @@ MSAT is free software, using the Apache license, see file LICENSE Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +open Msat module I = Formula_intf +module Term = Term -exception Invalid_var +exception Invalid_prop -type var = string +type term = Term.t + +(* atomic formula + + Prop: + - sign of int determines sign of formula + - odd numbers --> fresh atoms (for Tseitin CNF) + - even numbers --> used for regular int-mapping +*) type formula = | Prop of int - | Equal of var * var - | Distinct of var * var + | Equal of term * term + | Distinct of term * term + type t = formula type proof = unit let dummy = Prop 0 let max_fresh = ref 0 + let fresh () = incr max_fresh; Prop (2 * !max_fresh + 1) let mk_prop i = if i <> 0 && i < max_int / 2 then Prop (2 * i) - else raise Invalid_var + else raise Invalid_prop -let mk_var i = - if i <> "" then i - else raise Invalid_var +let order_ t1 t2 = if Term.compare t1 t2 > 0 then t2,t1 else t1,t2 -let mk_eq i j = Equal (mk_var (min i j), mk_var (max i j)) -let mk_neq i j = Distinct (mk_var (min i j), mk_var (max i j)) +let mk_eq a b = + let a, b = order_ a b in + Equal (a, b) + +let mk_neq a b = + let a, b = order_ a b in + Distinct (a, b) + +let mk_true = mk_eq Term.true_ Term.true_ +let mk_false = mk_eq Term.true_ Term.false_ +let mk_atom = mk_eq Term.true_ +let mk_atom_neg = mk_eq Term.false_ let neg = function | Prop i -> Prop (-i) @@ -50,17 +70,12 @@ let equal = (=) let compare = Pervasives.compare let print fmt = function - | Prop i -> Format.fprintf fmt "%s%s%d" (if i < 0 then "¬ " else "") (if i mod 2 = 0 then "v" else "f") ((abs i) / 2) - | Equal (a, b) -> Format.fprintf fmt "%s = %s" a b - | Distinct (a, b) -> Format.fprintf fmt "%s ≠ %s" a b - -module Term = struct - type t = var - let hash = Hashtbl.hash - let equal = (=) - let compare = Pervasives.compare - let print fmt t = Format.fprintf fmt "%s" t -end + | Prop i -> + Format.fprintf fmt "%s%s%d" + (if i < 0 then "¬ " else "") + (if i mod 2 = 0 then "v" else "f") ((abs i) / 2) + | Equal (a, b) -> Format.fprintf fmt "(@[=@ %a@ %a@])" Term.print a Term.print b + | Distinct (a, b) -> Format.fprintf fmt "(@[!=@ %a@ %a@])" Term.print a Term.print b module Formula = struct type t = formula diff --git a/src/example/expr.mli b/src/smt/expr.mli similarity index 54% rename from src/example/expr.mli rename to src/smt/expr.mli index 8a9f7591..0f01ae83 100644 --- a/src/example/expr.mli +++ b/src/smt/expr.mli @@ -3,12 +3,14 @@ MSAT is free software, using the Apache license, see file LICENSE Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +open Msat + +type term = Term.t -type var = string type formula = private - | Prop of int - | Equal of var * var - | Distinct of var * var + | Prop of int (* prop or tseitin atom *) + | Equal of term * term + | Distinct of term * term type t = formula type proof = unit @@ -20,16 +22,17 @@ val dummy : t val fresh : unit -> t val mk_prop : int -> t -val mk_eq : var -> var -> t -val mk_neq : var -> var -> t +(** [mk_prop i] makes a prop literal from [i], whose sign matters. + @raise Invalid_prop if [i=0] or if [i] is too large *) -module Term : sig - type t = var - val hash : t -> int - val equal : t -> t -> bool - val compare : t -> t -> int - val print : Format.formatter -> t -> unit -end +val mk_true : t +val mk_false : t +val mk_atom : term -> t +val mk_atom_neg : term -> t +val mk_eq : term -> term -> t +val mk_neq : term -> term -> t + +module Term = Term module Formula : sig type t = formula val hash : t -> int diff --git a/src/smt/literal.ml b/src/smt/literal.ml new file mode 100644 index 00000000..0d939be7 --- /dev/null +++ b/src/smt/literal.ml @@ -0,0 +1,184 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +open Msat + +type 'a view = + | Eq of 'a * 'a + | Distinct of bool * 'a list + | Builtin of bool * ID.t * 'a list + +module type OrderedType = sig + type t + val compare : t -> t -> int + val hash : t -> int + val print : Format.formatter -> t -> unit +end + +module type S = sig + type elt + type t + + val make : elt view -> t + val view : t -> elt view + + val neg : t -> t + + val print : Format.formatter -> t -> unit + + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + + module Map : Map.S with type key = t + module Set : Set.S with type elt = t + +end + +module Make (X : OrderedType) : S with type elt = X.t = struct + + type elt = X.t + type t = { + view: X.t view; + mutable tag: int; + } + + module V = struct + type t_ = t + type t = t_ + + let equal a1 a2 = + match a1.view, a2.view with + | Eq(t1, t2), Eq(u1, u2) -> + (X.compare t1 u1 = 0 && X.compare t2 u2 = 0) || + (X.compare t1 u2 = 0 && X.compare t2 u1 = 0) + | Distinct (b1,lt1), Distinct (b2,lt2) -> + (try + b1 = b2 && + List.for_all2 (fun x y -> X.compare x y = 0) lt1 lt2 + with Invalid_argument _ -> false) + | Builtin(b1, n1, l1), Builtin(b2, n2, l2) -> + (try + b1 = b2 && ID.equal n1 n2 + && + List.for_all2 (fun x y -> X.compare x y = 0) l1 l2 + with Invalid_argument _ -> false) + | _ -> false + + let hash a = match a.view with + | Eq(t1, t2) -> abs (19 * (X.hash t1 + X.hash t2)) + | Distinct (b,lt) -> + let x = if b then 7 else 23 in + abs (17 * List.fold_left (fun acc t -> (X.hash t) + acc ) x lt) + | Builtin(b, n, l) -> + let x = if b then 7 else 23 in + abs + (List.fold_left + (fun acc t-> acc*13 + X.hash t) (ID.hash n+x) l) + + let set_id t tag = t.tag <- tag + end + + module H = Hashcons.Make(V) + + let compare a1 a2 = Pervasives.compare a1.tag a2.tag + let equal a1 a2 = a1 == a2 + let hash a1 = a1.tag + + module T = struct + type t_ = t + type t = t_ + let compare=compare + end + + let make t = H.hashcons {view=t; tag= -1} + let view a = a.view + + let neg a = match view a with + | Eq(x, y) -> make (Distinct (false,[x; y])) + | Distinct (false, [x; y]) -> make (Eq (x, y)) + | Distinct (true, [x; y]) -> make (Distinct (false,[x; y])) + | Distinct (false, l) -> make (Distinct (true,l)) + | Distinct _ -> assert false + | Builtin(b, n, l) -> make (Builtin (not b, n, l)) + + let print_list fmt = function + | [] -> () + | z :: l -> + Format.fprintf fmt "%a" X.print z; + List.iter (Format.fprintf fmt ", %a" X.print) l + + let print fmt a = match view a with + | Eq (z1, z2) -> + if equal z1 z2 then Format.fprintf fmt "True" + else Format.fprintf fmt "%a=%a" X.print z1 X.print z2 + | Distinct (b,(z::l)) -> + let b = if b then "~" else "" in + Format.fprintf fmt "%s%a" b X.print z; + List.iter (fun x -> Format.fprintf fmt "<>%a" X.print x) l + | Builtin (b, n, l) -> + let b = if b then "" else "~" in + Format.fprintf fmt "%s%s(%a)" b (ID.to_string n) print_list l + | _ -> assert false + + module Set = Set.Make(T) + module Map = Map.Make(T) + +end + +module type S_Term = sig + + include S with type elt = Term.t + + val mk_pred : Term.t -> t + + val true_ : t + val false_ : t + + (* val terms_of : t -> Term.Set.t + val vars_of : t -> Symbols.Set.t + *) + (* module SetEq : Set.S with type elt = t * Term.t * Term.t*) +end + +module LT : S_Term = struct + + module L = Make(Term) + include L + + let mk_pred t = make (Eq (t, Term.true_) ) + + let true_ = mk_pred Term.true_ + let false_ = mk_pred Term.false_ + + let neg a = match view a with + | Eq(t1, t2) when Term.equal t2 Term.false_ -> + make (Eq (t1, Term.true_)) + | Eq(t1, t2) when Term.equal t2 Term.true_ -> + make (Eq (t1, Term.false_)) + | _ -> L.neg a + + (* let terms_of a = + let l = match view a with + | Eq (t1, t2) -> [t1; t2] + | Distinct (_, l) | Builtin (_, _, l) -> l + in + List.fold_left Term.subterms Term.Set.empty l + *) + + module SS = Symbols.Set + (* let vars_of a = + Term.Set.fold (fun t -> SS.union (Term.vars_of t)) (terms_of a) SS.empty + *) +end + diff --git a/src/smt/literal.mli b/src/smt/literal.mli new file mode 100644 index 00000000..f38963ab --- /dev/null +++ b/src/smt/literal.mli @@ -0,0 +1,62 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +open Msat + +module type OrderedType = sig + type t + val compare : t -> t -> int + val hash : t -> int + val print : Format.formatter -> t -> unit +end + +type 'a view = + | Eq of 'a * 'a + | Distinct of bool * 'a list + | Builtin of bool * ID.t * 'a list + +module type S = sig + type elt + type t + + val make : elt view -> t + val view : t -> elt view + + val neg : t -> t + + val print : Format.formatter -> t -> unit + + val compare : t -> t -> int + val equal : t -> t -> bool + val hash : t -> int + + module Map : Map.S with type key = t + module Set : Set.S with type elt = t + +end + +module Make ( X : OrderedType ) : S with type elt = X.t + +module type S_Term = sig + + include S with type elt = Term.t + + val mk_pred : Term.t -> t + val true_ : t + val false_ : t + +end + +module LT : S_Term + + diff --git a/src/example/mcsat.ml b/src/smt/mcsat.ml similarity index 99% rename from src/example/mcsat.ml rename to src/smt/mcsat.ml index 9be8e7bc..9a5b67fc 100644 --- a/src/example/mcsat.ml +++ b/src/smt/mcsat.ml @@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +open Msat + module Fsmt = Expr module Tsmt = struct diff --git a/src/example/smt.ml b/src/smt/smt.ml similarity index 100% rename from src/example/smt.ml rename to src/smt/smt.ml diff --git a/src/example/smt.mli b/src/smt/smt.mli similarity index 100% rename from src/example/smt.mli rename to src/smt/smt.mli diff --git a/src/smt/symbols.ml b/src/smt/symbols.ml new file mode 100644 index 00000000..c39e60ab --- /dev/null +++ b/src/smt/symbols.ml @@ -0,0 +1,62 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +type name_kind = Constructor | Other + +type t = + | True + | False + | Name of ID.t * name_kind + | Var of ID.t + +let name ?(kind=Other) s = Name (s, kind) +let var s = Var s + +let compare_kind k1 k2 = match k1, k2 with + | Other, Other -> 0 + | Other, _ -> 1 + | _ , Other -> -1 + | Constructor, Constructor -> 0 + +let compare s1 s2 = match s1, s2 with + | Name (n1,k1), Name (n2,k2) -> + let c = compare_kind k1 k2 in + if c = 0 then ID.compare n1 n2 else c + | Name _, _ -> -1 + | _, Name _ -> 1 + | Var n1, Var n2 -> ID.compare n1 n2 + | Var _, _ -> -1 + | _ ,Var _ -> 1 + | _ -> Pervasives.compare s1 s2 + +let equal s1 s2 = compare s1 s2 = 0 + +let hash = function + | Name (n,_) -> ID.hash n * 19 + | Var n (*| Int n*) -> ID.hash n * 19 + 1 + | s -> Hashtbl.hash s + +let to_string = function + | Name (n,_) -> ID.to_string n + | Var x -> "*var* "^(ID.to_string x) + | True -> "true" + | False -> "false" + +let print fmt s = Format.fprintf fmt "%s" (to_string s) + +module Map = + Map.Make(struct type t' = t type t=t' let compare=compare end) + +module Set = + Set.Make(struct type t' = t type t=t' let compare=compare end) + diff --git a/src/smt/symbols.mli b/src/smt/symbols.mli new file mode 100644 index 00000000..17dd3e0b --- /dev/null +++ b/src/smt/symbols.mli @@ -0,0 +1,33 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +type name_kind = Constructor | Other + +type t = + | True + | False + | Name of ID.t * name_kind + | Var of ID.t + +val name : ?kind:name_kind -> ID.t -> t +val var : ID.t -> t + +val equal : t -> t -> bool +val compare : t -> t -> int +val hash : t -> int + +val print : Format.formatter -> t -> unit + +module Map : Map.S with type key = t +module Set : Set.S with type elt = t + diff --git a/src/smt/term.ml b/src/smt/term.ml new file mode 100644 index 00000000..4d0db744 --- /dev/null +++ b/src/smt/term.ml @@ -0,0 +1,100 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +open Msat + +module Sy = Symbols + +type view = { + head: head; + ty: Ty.t; + mutable tag: int; +} + +and head = + | App of Symbols.t * t list + | Ite of t * t * t + +and t = view + +module H = struct + type t = view + let equal t1 t2 = match t1.head, t2.head with + | App (f1,l1), App (f2,l2) -> + begin try + Sy.equal f1 f2 + && List.for_all2 (==) l1 l2 + && Ty.equal t1.ty t2.ty + with Invalid_argument _ -> + false + end + | Ite (a1,b1,c1), Ite (a2,b2,c2) -> + a1==a2 && b1==b2 && c1==c2 + | App _, Ite _ + | Ite _, App _ -> false + + let hash t = match t.head with + | Ite (a,b,c) -> + abs + (List.fold_left + (fun acc x-> acc*19 +x.tag) 17 [a;b;c]) + | App (f,l) -> + abs + (List.fold_left + (fun acc x-> acc*19 +x.tag) (Sy.hash f + Ty.hash t.ty) + l) + let set_id x tag = x.tag <- tag +end + +module T = Hashcons.Make(H) + +let view t = t + +let rec print fmt t = match t.head with + | Ite (a,b,c) -> + Format.fprintf fmt "(@[<2>ite@ %a@ %a@ %a@])" print a print b print c + | App (x, l) -> + match x, l with + | _, [] -> Format.fprintf fmt "%a" Sy.print x + | _, _ -> Format.fprintf fmt "%a(%a)" Sy.print x print_list l + +and print_list fmt = function + | [] -> () + | [t] -> print fmt t + | t::l -> Format.fprintf fmt "%a,%a" print t print_list l + +let compare t1 t2 = + let c = Pervasives.compare t2.tag t1.tag in + if c = 0 then c + else match t1.head, t2.head with + | App ((Sy.True | Sy.False), _), App ((Sy.True | Sy.False), _) -> c + | App ((Sy.True | Sy.False), _), _ -> -1 + | _, App ((Sy.True | Sy.False), _) -> 1 + | _,_ -> c + +let app s l ty = T.hashcons {head=App(s,l); ty=ty; tag= -1; } +let const s ty = app s [] ty +let ite a b c = T.hashcons {head=Ite (a,b,c); ty=b.ty; tag= -1; } + +let true_ = app (Sy.True) [] Ty.Tbool +let false_ = app (Sy.False) [] Ty.Tbool + +let equal t1 t2 = t1 == t2 + +let hash t = t.tag + +module Set = + Set.Make(struct type t' = t type t=t' let compare=compare end) + +module Map = + Map.Make(struct type t' = t type t=t' let compare=compare end) diff --git a/src/smt/term.mli b/src/smt/term.mli new file mode 100644 index 00000000..c9542d3d --- /dev/null +++ b/src/smt/term.mli @@ -0,0 +1,45 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +open Msat + +type t + +type view = private { + head: head; + ty: Ty.t; + mutable tag: int; +} + +and head = + | App of Symbols.t * t list + | Ite of t * t * t + +val view : t -> view + +val app : Symbols.t -> t list -> Ty.t -> t +val const : Symbols.t -> Ty.t -> t +val ite : t -> t -> t -> t + +val true_ : t +val false_ : t + +val compare : t -> t -> int +val equal : t -> t -> bool +val hash : t -> int + +val print : Format.formatter -> t -> unit + +module Map : Map.S with type key = t +module Set : Set.S with type elt = t + diff --git a/src/smt/ty.ml b/src/smt/ty.ml new file mode 100644 index 00000000..a3af5bd7 --- /dev/null +++ b/src/smt/ty.ml @@ -0,0 +1,60 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +open Msat + +type symbol = Symbols.t + +type t = + | Tbool + | Tabstract of ID.t + | Tsum of ID.t * symbol list + +let bool = Tbool +let abstract i = Tabstract i +let sum i l = Tsum (i, l) + +let hash t = + match t with + | Tabstract s -> ID.hash s + | Tsum (s, l) -> + let h = + List.fold_left + (fun h x -> 13 * h + Symbols.hash x) (ID.hash s) l + in + abs h + | _ -> Hashtbl.hash t + +let equal t1 t2 = + match t1, t2 with + | Tabstract s1, Tabstract s2 + | Tsum (s1, _), Tsum (s2, _) -> + ID.equal s1 s2 + | Tbool, Tbool -> true + | _ -> false + +let compare t1 t2 = + match t1, t2 with + | Tabstract s1, Tabstract s2 -> + ID.compare s1 s2 + | Tabstract _, _ -> -1 | _ , Tabstract _ -> 1 + | Tsum (s1, _), Tsum(s2, _) -> + ID.compare s1 s2 + | Tsum _, _ -> -1 | _ , Tsum _ -> 1 + | t1, t2 -> Pervasives.compare t1 t2 + +let print fmt ty = + match ty with + | Tbool -> Format.fprintf fmt "bool" + | Tabstract s -> Format.fprintf fmt "%s" (ID.to_string s) + | Tsum (s, _) -> Format.fprintf fmt "%s" (ID.to_string s) diff --git a/src/smt/ty.mli b/src/smt/ty.mli new file mode 100644 index 00000000..0c94cf71 --- /dev/null +++ b/src/smt/ty.mli @@ -0,0 +1,29 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon and Alain Mebsout *) +(* Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) +open Msat + +type symbol = Symbols.t + +type t = + | Tbool + | Tabstract of ID.t + | Tsum of ID.t * symbol list + +val bool : t +val abstract : ID.t -> t +val sum : ID.t -> symbol list -> t + +val hash : t -> int +val equal : t -> t -> bool +val compare : t -> t -> int +val print : Format.formatter -> t -> unit diff --git a/src/smt/uf.ml b/src/smt/uf.ml new file mode 100644 index 00000000..573189c6 --- /dev/null +++ b/src/smt/uf.ml @@ -0,0 +1,381 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon, Evelyne Contejean *) +(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) +(* CNRS, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +type answer = Yes of Explanation.t | No + +type 'a literal = + | LSem of 'a Literal.view + | LTerm of Literal.LT.t + +exception Inconsistent of Explanation.t +exception Unsolvable + +module type ELT = sig + type r + + val make : Term.t -> r * Literal.LT.t list + + val compare : r -> r -> int + + val equal : r -> r -> bool + + val hash : r -> int + + val leaves : r -> r list + + val subst : r -> r -> r -> r + + val can_be_equal : r -> r -> bool + + val term_embed : Term.t -> r + + val term_extract : r -> Term.t option + + val unsolvable : r -> bool + + val fully_interpreted : Symbols.t -> bool + + val print : Format.formatter -> r -> unit +end + +module type S = sig + type t + + module R : ELT + + val empty : t + val add : t -> Term.t -> t * Literal.LT.t list + + val mem : t -> Term.t -> bool + + val find : t -> Term.t -> R.r * Explanation.t + + val find_r : t -> R.r -> R.r * Explanation.t + + val union : + t -> R.r -> R.r -> Explanation.t -> + t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list + + val distinct : t -> R.r list -> Explanation.t -> t + + val are_equal : t -> Term.t -> Term.t -> Sig.answer + val are_distinct : t -> Term.t -> Term.t -> Sig.answer + val already_distinct : t -> R.r list -> bool + + val class_of : t -> Term.t -> Term.t list +end + +module Make ( R : ELT ) = struct + + module Ex = Explanation + module R = R + module Sy = Symbols + module T = Term + module MapT = Term.Map + module SetT = Term.Set + + module Lit = Literal.Make(struct type t = R.r include R end) + module MapL = Lit.Map + + module MapR = Map.Make(struct type t = R.r let compare = R.compare end) + + module SetR = Set.Make(struct type t = R.r let compare = R.compare end) + + module SetRR = Set.Make(struct + type t = R.r * R.r + let compare (r1, r1') (r2, r2') = + let c = R.compare r1 r2 in + if c <> 0 then c + else R.compare r1' r2' + end) + + + type t = { + + (* term -> [t] *) + make : R.r MapT.t; + + (* representative table *) + repr : (R.r * Ex.t) MapR.t; + + (* r -> class (of terms) *) + classes : SetT.t MapR.t; + + (*associates each value r with the set of semantical values whose + representatives contains r *) + gamma : SetR.t MapR.t; + + (* the disequations map *) + neqs: Ex.t MapL.t MapR.t; + + } + + let empty = { + make = MapT.empty; + repr = MapR.empty; + classes = MapR.empty; + gamma = MapR.empty; + neqs = MapR.empty; + } + + module Env = struct + + let mem env t = MapT.mem t env.make + + let lookup_by_t t env = + try MapR.find (MapT.find t env.make) env.repr + with Not_found -> + assert false (*R.make t, Ex.empty*) (* XXXX *) + + let lookup_by_r r env = + try MapR.find r env.repr with Not_found -> r, Ex.empty + + let lookup_for_neqs env r = + try MapR.find r env.neqs with Not_found -> MapL.empty + + let add_to_classes t r classes = + MapR.add r + (SetT.add t (try MapR.find r classes with Not_found -> SetT.empty)) + classes + + let update_classes c nc classes = + let s1 = try MapR.find c classes with Not_found -> SetT.empty in + let s2 = try MapR.find nc classes with Not_found -> SetT.empty in + MapR.remove c (MapR.add nc (SetT.union s1 s2) classes) + + let add_to_gamma r c gamma = + List.fold_left + (fun gamma x -> + let s = try MapR.find x gamma with Not_found -> SetR.empty in + MapR.add x (SetR.add r s) gamma) + gamma (R.leaves c) + + (* r1 = r2 => neqs(r1) \uplus neqs(r2) *) + let update_neqs r1 r2 dep env = + let nq_r1 = lookup_for_neqs env r1 in + let nq_r2 = lookup_for_neqs env r2 in + let mapl = + MapL.fold + (fun l1 ex1 mapl -> + try + let ex2 = MapL.find l1 mapl in + let ex = Ex.union (Ex.union ex1 ex2) dep in (* VERIF *) + raise (Inconsistent ex) + with Not_found -> + MapL.add l1 (Ex.union ex1 dep) mapl) + nq_r1 nq_r2 + in + MapR.add r2 mapl (MapR.add r1 mapl env.neqs) + + let filter_leaves r = + List.fold_left (fun p r -> SetR.add r p) SetR.empty (R.leaves r) + + let canon_empty st env = + SetR.fold + (fun p ((z, ex) as acc) -> + let q, ex_q = lookup_by_r p env in + if R.equal p q then acc else (p,q)::z, Ex.union ex_q ex) + st ([], Ex.empty) + + let canon_aux rx = List.fold_left (fun r (p,v) -> R.subst p v r) rx + + let rec canon env r ex_r = + let se = filter_leaves r in + let subst, ex_subst = canon_empty se env in + let r2 = canon_aux r subst in + let ex_r2 = Ex.union ex_r ex_subst in + if R.equal r r2 then r2, ex_r2 else canon env r2 ex_r2 + + let normal_form env r = canon env r Ex.empty + + let find_or_normal_form env r = + try MapR.find r env.repr with Not_found -> normal_form env r + + let init_leaf env p = + let in_repr = MapR.mem p env.repr in + let in_neqs = MapR.mem p env.neqs in + { env with + repr = + if in_repr then env.repr + else MapR.add p (p, Ex.empty) env.repr; + classes = + if in_repr then env.classes + else update_classes p p env.classes; + gamma = + if in_repr then env.gamma + else add_to_gamma p p env.gamma ; + neqs = + if in_neqs then env.neqs + else update_neqs p p Ex.empty env } + + let init_term env t = + let mkr, ctx = R.make t in + let rp, ex = normal_form env mkr in + { make = MapT.add t mkr env.make; + repr = MapR.add mkr (rp,ex) env.repr; + classes = add_to_classes t rp env.classes; + gamma = add_to_gamma mkr rp env.gamma; + neqs = + if MapR.mem rp env.neqs then env.neqs (* pourquoi ce test *) + else MapR.add rp MapL.empty env.neqs}, ctx + + + let update_aux dep set env= + SetRR.fold + (fun (rr, nrr) env -> + { env with + neqs = update_neqs rr nrr dep env ; + classes = update_classes rr nrr env.classes}) + set env + + let apply_sigma_uf env (p, v, dep) = + assert (MapR.mem p env.gamma); + let use_p = MapR.find p env.gamma in + try + let env, tch, neqs_to_up = SetR.fold + (fun r (env, touched, neqs_to_up) -> + let rr, ex = MapR.find r env.repr in + let nrr = R.subst p v rr in + if R.equal rr nrr then env, touched, neqs_to_up + else + let ex = Ex.union ex dep in + let env = + {env with + repr = MapR.add r (nrr, ex) env.repr; + gamma = add_to_gamma r nrr env.gamma } + in + env, (r, nrr, ex)::touched, SetRR.add (rr, nrr) neqs_to_up + ) use_p (env, [], SetRR.empty) in + (* Correction : Do not update neqs twice for the same r *) + update_aux dep neqs_to_up env, tch + + with Not_found -> assert false + + let apply_sigma eqs env tch ((p, v, dep) as sigma) = + let env = init_leaf env p in + let env, touched = apply_sigma_uf env sigma in + env, ((p, touched, v) :: tch) + + end + + let add env t = + if MapT.mem t env.make then env, [] else Env.init_term env t + + let ac_solve eqs dep (env, tch) (p, v) = + (* pourquoi recuperer le representant de rv? r = rv d'apres testopt *) + (* assert ( let rp, _ = Env.find_or_normal_form env p in R.equal p rp); *) + let rv, ex_rv = Env.find_or_normal_form env v in + (* let rv = v in *) + (* assert ( let rv, _ = Env.find_or_normal_form env v in R.equal v rv); *) + let dep = Ex.union ex_rv dep in + Env.apply_sigma eqs env tch (p, rv, dep) + + let check_consistent env r1 r2 dep : unit = + let rr1, ex_r1 = Env.find_or_normal_form env r1 in + let rr2, ex_r2 = Env.find_or_normal_form env r2 in + if R.equal rr1 rr2 + then () (* Remove rule *) + else + let dep = Ex.union dep (Ex.union ex_r1 ex_r2) in + begin + ignore (Env.update_neqs rr1 rr2 dep env); + if R.can_be_equal rr1 rr2 + then () + else raise (Inconsistent dep) + end + + let union env r1 r2 dep = + check_consistent env r1 r2 dep; + () + + let rec distinct env rl dep = + let d = Lit.make (Literal.Distinct (false,rl)) in + let env, _, newds = + List.fold_left + (fun (env, mapr, newds) r -> + let rr, ex = Env.find_or_normal_form env r in + try + let exr = MapR.find rr mapr in + raise (Inconsistent (Ex.union ex exr)) + with Not_found -> + let uex = Ex.union ex dep in + let mdis = + try MapR.find rr env.neqs with Not_found -> MapL.empty in + let mdis = + try + MapL.add d (Ex.merge uex (MapL.find d mdis)) mdis + with Not_found -> + MapL.add d uex mdis + in + let env = Env.init_leaf env rr in + let env = {env with neqs = MapR.add rr mdis env.neqs} in + env, MapR.add rr uex mapr, (rr, ex, mapr)::newds + ) + (env, MapR.empty, []) + rl + in + List.fold_left + (fun env (r1, ex1, mapr) -> + MapR.fold (fun r2 ex2 env -> + let ex = Ex.union ex1 (Ex.union ex2 dep) in + try match R.solve r1 r2 with + | [a, b] -> + if (R.equal a r1 && R.equal b r2) || + (R.equal a r2 && R.equal b r1) then env + else + distinct env [a; b] ex + | [] -> + raise (Inconsistent ex) + | _ -> env + with Unsolvable -> env) mapr env) + env newds + + let are_equal env t1 t2 = + let r1, ex_r1 = Env.lookup_by_t t1 env in + let r2, ex_r2 = Env.lookup_by_t t2 env in + if R.equal r1 r2 then Yes(Ex.union ex_r1 ex_r2) else No + + let are_distinct env t1 t2 = + let r1, ex_r1 = Env.lookup_by_t t1 env in + let r2, ex_r2 = Env.lookup_by_t t2 env in + try + ignore (union env r1 r2 (Ex.union ex_r1 ex_r2)); + No + with Inconsistent ex -> Yes(ex) + + let already_distinct env lr = + let d = Lit.make (Literal.Distinct (false,lr)) in + try + List.iter (fun r -> + let mdis = MapR.find r env.neqs in + ignore (MapL.find d mdis) + ) lr; + true + with Not_found -> false + + let find env t = + Env.lookup_by_t t env + + let find_r = Env.find_or_normal_form + + let mem = Env.mem + + let class_of env t = + try + let rt, _ = MapR.find (MapT.find t env.make) env.repr in + SetT.elements (MapR.find rt env.classes) + with Not_found -> [t] + + +end diff --git a/src/smt/uf.mli b/src/smt/uf.mli new file mode 100644 index 00000000..3b30e261 --- /dev/null +++ b/src/smt/uf.mli @@ -0,0 +1,78 @@ +(**************************************************************************) +(* *) +(* Cubicle *) +(* Combining model checking algorithms and SMT solvers *) +(* *) +(* Sylvain Conchon, Evelyne Contejean *) +(* Francois Bobot, Mohamed Iguernelala, Alain Mebsout *) +(* CNRS, Universite Paris-Sud 11 *) +(* *) +(* Copyright 2011. This file is distributed under the terms of the *) +(* Apache Software License version 2.0 *) +(* *) +(**************************************************************************) + +type answer = Yes of Explanation.t | No + +type 'a literal = + | LSem of 'a Literal.view + | LTerm of Literal.LT.t + +module type ELT = sig + type r + + val make : Term.t -> r * Literal.LT.t list + + val type_info : r -> Ty.t + + val compare : r -> r -> int + + val equal : r -> r -> bool + + val hash : r -> int + + val leaves : r -> r list + + val subst : r -> r -> r -> r + + val solve : r -> r -> (r * r) list + + val term_embed : Term.t -> r + + val term_extract : r -> Term.t option + + val unsolvable : r -> bool + + val fully_interpreted : Symbols.t -> bool + + val print : Format.formatter -> r -> unit +end + +module type S = sig + type t + + module R : ELT + + val empty : t + val add : t -> Term.t -> t * Literal.LT.t list + + val mem : t -> Term.t -> bool + + val find : t -> Term.t -> R.r * Explanation.t + + val find_r : t -> R.r -> R.r * Explanation.t + + val union : + t -> R.r -> R.r -> Explanation.t -> + t * (R.r * (R.r * R.r * Explanation.t) list * R.r) list + + val distinct : t -> R.r list -> Explanation.t -> t + + val are_equal : t -> Term.t -> Term.t -> Sig.answer + val are_distinct : t -> Term.t -> Term.t -> Sig.answer + val already_distinct : t -> R.r list -> bool + + val class_of : t -> Term.t -> Term.t list +end + +module Make ( X : ELT ) : S with module R = X diff --git a/src/example/unionfind.ml b/src/smt/unionfind.ml similarity index 88% rename from src/example/unionfind.ml rename to src/smt/unionfind.ml index 7211fbe0..ab81a1ad 100644 --- a/src/example/unionfind.ml +++ b/src/smt/unionfind.ml @@ -4,13 +4,20 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) +module type OrderedType = sig + type t + val compare : t -> t -> int +end + (* Union-find Module *) -module Make(T : Sig.OrderedType) = struct +module Make(T : OrderedType) = struct exception Unsat of T.t * T.t type var = T.t module M = Map.Make(T) + (* TODO: better treatment of inequalities *) + type t = { rank : int M.t; forbid : ((var * var) list); @@ -43,7 +50,7 @@ module Make(T : Sig.OrderedType) = struct h.parent <- f; cx - (* Highly ineficient treatment of inequalities *) + (* Highly inefficient treatment of inequalities *) let possible h = let aux (a, b) = let ca = find h a in diff --git a/src/example/unionfind.mli b/src/smt/unionfind.mli similarity index 72% rename from src/example/unionfind.mli rename to src/smt/unionfind.mli index 4d559ced..adf2cd25 100644 --- a/src/example/unionfind.mli +++ b/src/smt/unionfind.mli @@ -4,7 +4,12 @@ Copyright 2014 Guillaume Bury Copyright 2014 Simon Cruanes *) -module Make(T : Sig.OrderedType) : sig +module type OrderedType = sig + type t + val compare : t -> t -> int +end + +module Make(T : OrderedType) : sig type t exception Unsat of T.t * T.t val empty : t diff --git a/src/util/hashcons.ml b/src/util/hashcons.ml new file mode 100644 index 00000000..2f2fa7e7 --- /dev/null +++ b/src/util/hashcons.ml @@ -0,0 +1,28 @@ + +module type ARG = sig + type t + val equal : t -> t -> bool + val hash : t -> int + val set_id : t -> int -> unit +end + +module Make(A : ARG): sig + val hashcons : A.t -> A.t + val iter : (A.t -> unit) -> unit +end = struct + module W = Weak.Make(A) + + let tbl_ = W.create 1024 + let n_ = ref 0 + + (* hashcons terms *) + let hashcons t = + let t' = W.merge tbl_ t in + if t == t' then ( + incr n_; + A.set_id t' !n_; + ); + t' + + let iter yield = W.iter yield tbl_ +end