diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index 62762e173b643e93f871b418d9663d621d37ee0d..26a9f958eafe4e1e14b440b38152b48146bf1d47 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -39,6 +39,17 @@ module Subst = struct
include Colibri2_popop_lib.Popop_stdlib.MkDatatype(T)
let empty = { term = Expr.Term.Var.M.empty; ty = Expr.Ty.Var.M.empty}
+
+ let distinct_union subst1 subst2 =
+ {
+ ty =
+ Expr.Ty.Var.M.union (fun _ _ -> assert false) subst1.ty subst2.ty;
+ term =
+ Expr.Term.Var.M.union
+ (fun _ _ -> assert false)
+ subst1.term subst2.term;
+ }
+
end
diff --git a/src_colibri2/core/ground.mli b/src_colibri2/core/ground.mli
index aa66b0730f6780af04b6c2982f4ad8632a082adf..0466e1e3b493b93682f4e0acdfbc3556c900239e 100644
--- a/src_colibri2/core/ground.mli
+++ b/src_colibri2/core/ground.mli
@@ -29,6 +29,8 @@ module Subst: sig
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
val empty: t
+
+ val distinct_union: t -> t -> t
end
module Ty: sig
diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
index 7155d1b705b7442f4ba553530501407ac8e74d09..0c848087852ca710ad7909a1f5467b02ec55f71b 100644
--- a/src_colibri2/tests/generate_tests/generate_dune_tests.ml
+++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -13,7 +13,7 @@ let () =
let files = Sys.readdir dir in
Array.sort String.compare files;
let files = Array.to_list files in
- let files = List.filter (fun f -> Filename.check_suffix f "cnf" || Filename.check_suffix f ".smt2") files in
+ let files = List.filter (fun f -> List.exists (Filename.check_suffix f) ["cnf";".smt2";".psmt2"]) files in
let cout = open_out (Filename.concat dir "dune.inc") in
Printf.fprintf cout
"(rule (action (with-stdout-to oracle (echo %S))))\n"
diff --git a/src_colibri2/tests/solve/all/steplimitreached/bag-BagImpl-addqtvc.psmt2 b/src_colibri2/tests/solve/all/steplimitreached/bag-BagImpl-addqtvc.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..b08480453a0ef400f9563741b34eaddf709247ab
--- /dev/null
+++ b/src_colibri2/tests/solve/all/steplimitreached/bag-BagImpl-addqtvc.psmt2
@@ -0,0 +1,245 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; SMT-LIB2: integer arithmetic
+(declare-sort string 0)
+
+(declare-datatypes ((tuple0 0))
+(((Tuple0))))
+(declare-sort infix_mngt 2)
+
+(declare-fun infix_at (par (a b) ((infix_mngt a b) a) b))
+
+(define-fun infix_eqeq (par (a1) ((b1 (infix_mngt a1 Int)) (b2 (infix_mngt a1
+ Int))) Bool (forall ((x a1)) (= (infix_at b1 x) (infix_at b2 x)))))
+
+(declare-fun add (par (a1) (a1 (infix_mngt a1 Int)) (infix_mngt a1 Int)))
+
+;; add'def
+ (assert (par (a1)
+ (forall ((e a1) (b1 (infix_mngt a1 Int)) (x a1))
+ (= (infix_at (add e b1) x) (ite (= x e) (+ (infix_at b1 x) 1)
+ (infix_at b1 x))))))
+
+(declare-fun remove (par (a1) (a1 (infix_mngt a1 Int)) (infix_mngt a1 Int)))
+
+;; remove'def
+ (assert (par (a1)
+ (forall ((e a1) (b1 (infix_mngt a1 Int)) (x a1))
+ (= (infix_at (remove e b1) x) (ite (= x e) (- (infix_at b1 x) 1)
+ (infix_at b1 x))))))
+
+(declare-fun set (par (a1 b1) ((infix_mngt a1 b1) a1 b1) (infix_mngt a1 b1)))
+
+;; set'def
+ (assert (par (a1 b1)
+ (forall ((f (infix_mngt a1 b1)) (x a1) (v b1) (y a1))
+ (= (infix_at (set f x v) y) (ite (= y x) v (infix_at f y))))))
+
+(declare-fun const1 (par (a1 b1) (b1) (infix_mngt a1 b1)))
+
+;; const'def
+ (assert (par (a1 b1)
+ (forall ((v b1) (us a1)) (= (infix_at (const1 v) us) v))))
+
+(declare-sort rarray 1)
+
+(declare-fun len (par (a1) ((rarray a1)) Int))
+
+(declare-fun data (par (a1) ((rarray a1)) (infix_mngt Int a1)))
+
+;; rarray'invariant
+ (assert (par (a1)
+ (forall ((self (rarray a1))) (! (<= 0 (len self)) :pattern ((len self)) ))))
+
+(define-fun mixfix_lbrb (par (a1) ((r (rarray a1))
+ (i Int)) a1 (infix_at (data r) i)))
+
+(declare-fun mixfix_lblsmnrb (par (a1) ((rarray a1) Int a1) (rarray a1)))
+
+;; mixfix [<-]'spec
+ (assert (par (a1)
+ (forall ((r (rarray a1)) (i Int) (v a1))
+ (and (= (len (mixfix_lblsmnrb r i v)) (len r))
+ (= (data (mixfix_lblsmnrb r i v)) (set (data r) i v))))))
+
+(declare-fun numof ((infix_mngt Int Bool) Int Int) Int)
+
+;; numof'def
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (ite (<= b2 a2) (= (numof p a2 b2) 0)
+ (ite (= (infix_at p (- b2 1)) true)
+ (= (numof p a2 b2) (+ 1 (numof p a2 (- b2 1))))
+ (= (numof p a2 b2) (numof p a2 (- b2 1)))))))
+
+;; Numof_bounds
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (=> (< a2 b2) (and (<= 0 (numof p a2 b2)) (<= (numof p a2 b2) (- b2 a2))))))
+
+;; Numof_append
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int) (c Int))
+ (=> (and (<= a2 b2) (<= b2 c))
+ (= (numof p a2 c) (+ (numof p a2 b2) (numof p b2 c))))))
+
+;; Numof_left_no_add
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (=> (< a2 b2)
+ (=> (not (= (infix_at p a2) true))
+ (= (numof p a2 b2) (numof p (+ a2 1) b2))))))
+
+;; Numof_left_add
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (=> (< a2 b2)
+ (=> (= (infix_at p a2) true)
+ (= (numof p a2 b2) (+ 1 (numof p (+ a2 1) b2)))))))
+
+;; Empty
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (=>
+ (forall ((n Int))
+ (=> (and (<= a2 n) (< n b2)) (not (= (infix_at p n) true))))
+ (= (numof p a2 b2) 0))))
+
+;; Full
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (=> (<= a2 b2)
+ (=>
+ (forall ((n Int)) (=> (and (<= a2 n) (< n b2)) (= (infix_at p n) true)))
+ (= (numof p a2 b2) (- b2 a2))))))
+
+;; numof_increasing
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (i Int) (j Int) (k Int))
+ (=> (and (<= i j) (<= j k)) (<= (numof p i j) (numof p i k)))))
+
+;; numof_strictly_increasing
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (i Int) (j Int) (k Int) (l Int))
+ (=> (and (<= i j) (and (<= j k) (< k l)))
+ (=> (= (infix_at p k) true) (< (numof p i j) (numof p i l))))))
+
+;; numof_change_any
+ (assert
+ (forall ((p1 (infix_mngt Int Bool)) (p2 (infix_mngt Int Bool)) (a2 Int)
+ (b2 Int))
+ (=>
+ (forall ((j Int))
+ (=> (and (<= a2 j) (< j b2))
+ (=> (= (infix_at p1 j) true) (= (infix_at p2 j) true))))
+ (>= (numof p2 a2 b2) (numof p1 a2 b2)))))
+
+;; numof_change_some
+ (assert
+ (forall ((p1 (infix_mngt Int Bool)) (p2 (infix_mngt Int Bool)) (a2 Int)
+ (b2 Int) (i Int))
+ (=> (and (<= a2 i) (< i b2))
+ (=>
+ (forall ((j Int))
+ (=> (and (<= a2 j) (< j b2))
+ (=> (= (infix_at p1 j) true) (= (infix_at p2 j) true))))
+ (=> (not (= (infix_at p1 i) true))
+ (=> (= (infix_at p2 i) true) (> (numof p2 a2 b2) (numof p1 a2 b2))))))))
+
+;; numof_change_equiv
+ (assert
+ (forall ((p1 (infix_mngt Int Bool)) (p2 (infix_mngt Int Bool)) (a2 Int)
+ (b2 Int))
+ (=>
+ (forall ((j Int))
+ (=> (and (<= a2 j) (< j b2))
+ (= (= (infix_at p1 j) true) (= (infix_at p2 j) true))))
+ (= (numof p2 a2 b2) (numof p1 a2 b2)))))
+
+(declare-datatypes ((t_model 1))
+((par (a1) ((Null (Null_proj_1 Int)) (Value (Value_proj_1 a1))))))
+(declare-sort t 1)
+
+(declare-fun v (par (a1) ((t a1)) (t_model a1)))
+
+(define-fun is_null (par (a1)
+ ((t1 (t a1))) Bool (let ((subject (v t1)))
+ (ite ((_ is Null) subject) true false))))
+
+(declare-fun fc (par (a1) ((rarray (t a1)) a1) (infix_mngt Int Bool)))
+
+;; fc'def
+ (assert (par (a1)
+ (forall ((r (rarray (t a1))) (x a1) (i Int))
+ (= (= (infix_at (fc r x) i) true) (= (v (infix_at (data r) i)) (Value x))))))
+
+(define-fun numof1 (par (a1) ((r (rarray (t a1))) (x a1) (l Int)
+ (u Int)) Int (numof (fc r x) l u)))
+
+(declare-sort t1 1)
+
+(declare-fun size (par (a1) ((t1 a1)) Int))
+
+(declare-fun data1 (par (a1) ((t1 a1)) (rarray (t a1))))
+
+(declare-fun contents (par (a1) ((t1 a1)) (infix_mngt a1 Int)))
+
+;; t'invariant
+ (assert (par (a1)
+ (forall ((self (t1 a1)))
+ (! (and (and (<= 0 (size self)) (= (size self) (len (data1 self))))
+ (and
+ (forall ((i Int))
+ (=> (and (<= 0 i) (< i (size self)))
+ (not (is_null (mixfix_lbrb (data1 self) i)))))
+ (forall ((x a1))
+ (= (infix_at (contents self) x) (numof1 (data1 self) x 0 (size self)))))) :pattern (
+ (contents self)) :pattern ((data1 self)) :pattern ((size self)) ))))
+
+(declare-sort a2 0)
+
+(assert
+;; addqtvc
+ ;; File "why3/examples/bag.mlw", line 128, characters 6-9
+ (not
+ (forall ((t2 (t1 a2)) (x a2))
+ (let ((n (size t2)))
+ (let ((o (+ n 1)))
+ (and (<= 0 o)
+ (forall ((t_data (rarray (t a2))))
+ (=>
+ (and (= (len t_data) o)
+ (forall ((i Int))
+ (=> (and (<= 0 i) (< i (len (data1 t2))))
+ (=> (< i o) (= (mixfix_lbrb t_data i) (mixfix_lbrb (data1 t2) i))))))
+ (and
+ (forall ((v1 a2)) (= (infix_at (contents t2) v1) (numof1 t_data v1 0 n)))
+ (forall ((result (t a2)))
+ (=> (= (v result) (Value x))
+ (and (and (<= 0 n) (< n (len t_data)))
+ (=> (= (len (mixfix_lblsmnrb t_data n result)) (len t_data))
+ (=> (= (len (mixfix_lblsmnrb t_data n result)) (len t_data))
+ (and
+ (forall ((v1 a2))
+ (= (infix_at (contents t2) v1) (numof1 (mixfix_lblsmnrb t_data n result) v1
+ 0 n)))
+ (forall ((t3 (t1 a2)))
+ (and
+ (and
+ (and (<= 0 (+ n 1)) (= (+ n 1) (len (mixfix_lblsmnrb t_data n result))))
+ (and
+ (forall ((i Int))
+ (=> (and (<= 0 i) (< i (+ n 1)))
+ (not (is_null (mixfix_lbrb (mixfix_lblsmnrb t_data n result) i)))))
+ (forall ((x1 a2))
+ (= (infix_at (add x (contents t2)) x1) (numof1
+ (mixfix_lblsmnrb t_data n result) x1
+ 0 (+ n 1))))))
+ (=>
+ (and (= (add x (contents t2)) (contents t3))
+ (and (= (mixfix_lblsmnrb t_data n result) (data1 t3))
+ (= (+ n 1) (size t3))))
+ (and (= (size t3) (+ (size t2) 1)) (infix_eqeq (contents t3)
+ (add x (contents t2))))))))))))))))))))))
+(check-sat)
diff --git a/src_colibri2/tests/solve/all/steplimitreached/dune b/src_colibri2/tests/solve/all/steplimitreached/dune
new file mode 100644
index 0000000000000000000000000000000000000000..39efa26de274dd57baab7e1bac879e0503838bd5
--- /dev/null
+++ b/src_colibri2/tests/solve/all/steplimitreached/dune
@@ -0,0 +1,13 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+ (glob_files *.cnf)
+ (glob_files *.smt2)
+ (glob_files *.psmt2))
+ (action
+ (with-stdout-to
+ dune.inc
+ (run %{exe:../../../generate_tests/generate_dune_tests.exe} . steplimitreached)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/all/steplimitreached/dune.inc b/src_colibri2/tests/solve/all/steplimitreached/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..7a7c228cac804f431679042072eb142be13719db
--- /dev/null
+++ b/src_colibri2/tests/solve/all/steplimitreached/dune.inc
@@ -0,0 +1,3 @@
+(rule (action (with-stdout-to oracle (echo "steplimitreached\n"))))
+(rule (action (with-stdout-to bag-BagImpl-addqtvc.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bag-BagImpl-addqtvc.psmt2}))))
+(rule (alias runtest) (action (diff oracle bag-BagImpl-addqtvc.psmt2.res)))
diff --git a/src_colibri2/tests/solve/all/unsat/bag-BagImpl-createqtvc.psmt2 b/src_colibri2/tests/solve/all/unsat/bag-BagImpl-createqtvc.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..cea398b9b343bd2244529c5bc8a78445cc54847a
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/bag-BagImpl-createqtvc.psmt2
@@ -0,0 +1,233 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; SMT-LIB2: integer arithmetic
+(declare-sort string 0)
+
+(declare-datatypes ((tuple0 0))
+(((Tuple0))))
+(declare-sort infix_mngt 2)
+
+(declare-fun infix_at (par (a b) ((infix_mngt a b) a) b))
+
+(define-fun infix_eqeq (par (a1) ((b1 (infix_mngt a1 Int)) (b2 (infix_mngt a1
+ Int))) Bool (forall ((x a1)) (= (infix_at b1 x) (infix_at b2 x)))))
+
+(declare-fun add (par (a1) (a1 (infix_mngt a1 Int)) (infix_mngt a1 Int)))
+
+;; add'def
+ (assert (par (a1)
+ (forall ((e a1) (b1 (infix_mngt a1 Int)) (x a1))
+ (= (infix_at (add e b1) x) (ite (= x e) (+ (infix_at b1 x) 1)
+ (infix_at b1 x))))))
+
+(declare-fun remove (par (a1) (a1 (infix_mngt a1 Int)) (infix_mngt a1 Int)))
+
+;; remove'def
+ (assert (par (a1)
+ (forall ((e a1) (b1 (infix_mngt a1 Int)) (x a1))
+ (= (infix_at (remove e b1) x) (ite (= x e) (- (infix_at b1 x) 1)
+ (infix_at b1 x))))))
+
+(declare-fun set (par (a1 b1) ((infix_mngt a1 b1) a1 b1) (infix_mngt a1 b1)))
+
+;; set'def
+ (assert (par (a1 b1)
+ (forall ((f (infix_mngt a1 b1)) (x a1) (v b1) (y a1))
+ (= (infix_at (set f x v) y) (ite (= y x) v (infix_at f y))))))
+
+(declare-fun const1 (par (a1 b1) (b1) (infix_mngt a1 b1)))
+
+;; const'def
+ (assert (par (a1 b1)
+ (forall ((v b1) (us a1)) (= (infix_at (const1 v) us) v))))
+
+(declare-sort rarray 1)
+
+(declare-fun len (par (a1) ((rarray a1)) Int))
+
+(declare-fun data (par (a1) ((rarray a1)) (infix_mngt Int a1)))
+
+;; rarray'invariant
+ (assert (par (a1)
+ (forall ((self (rarray a1))) (! (<= 0 (len self)) :pattern ((len self)) ))))
+
+(define-fun mixfix_lbrb (par (a1) ((r (rarray a1))
+ (i Int)) a1 (infix_at (data r) i)))
+
+(declare-fun mixfix_lblsmnrb (par (a1) ((rarray a1) Int a1) (rarray a1)))
+
+;; mixfix [<-]'spec
+ (assert (par (a1)
+ (forall ((r (rarray a1)) (i Int) (v a1))
+ (and (= (len (mixfix_lblsmnrb r i v)) (len r))
+ (= (data (mixfix_lblsmnrb r i v)) (set (data r) i v))))))
+
+(declare-fun numof ((infix_mngt Int Bool) Int Int) Int)
+
+;; numof'def
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (ite (<= b2 a2) (= (numof p a2 b2) 0)
+ (ite (= (infix_at p (- b2 1)) true)
+ (= (numof p a2 b2) (+ 1 (numof p a2 (- b2 1))))
+ (= (numof p a2 b2) (numof p a2 (- b2 1)))))))
+
+;; Numof_bounds
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (=> (< a2 b2) (and (<= 0 (numof p a2 b2)) (<= (numof p a2 b2) (- b2 a2))))))
+
+;; Numof_append
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int) (c Int))
+ (=> (and (<= a2 b2) (<= b2 c))
+ (= (numof p a2 c) (+ (numof p a2 b2) (numof p b2 c))))))
+
+;; Numof_left_no_add
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (=> (< a2 b2)
+ (=> (not (= (infix_at p a2) true))
+ (= (numof p a2 b2) (numof p (+ a2 1) b2))))))
+
+;; Numof_left_add
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (=> (< a2 b2)
+ (=> (= (infix_at p a2) true)
+ (= (numof p a2 b2) (+ 1 (numof p (+ a2 1) b2)))))))
+
+;; Empty
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (=>
+ (forall ((n Int))
+ (=> (and (<= a2 n) (< n b2)) (not (= (infix_at p n) true))))
+ (= (numof p a2 b2) 0))))
+
+;; Full
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (a2 Int) (b2 Int))
+ (=> (<= a2 b2)
+ (=>
+ (forall ((n Int)) (=> (and (<= a2 n) (< n b2)) (= (infix_at p n) true)))
+ (= (numof p a2 b2) (- b2 a2))))))
+
+;; numof_increasing
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (i Int) (j Int) (k Int))
+ (=> (and (<= i j) (<= j k)) (<= (numof p i j) (numof p i k)))))
+
+;; numof_strictly_increasing
+ (assert
+ (forall ((p (infix_mngt Int Bool)) (i Int) (j Int) (k Int) (l Int))
+ (=> (and (<= i j) (and (<= j k) (< k l)))
+ (=> (= (infix_at p k) true) (< (numof p i j) (numof p i l))))))
+
+;; numof_change_any
+ (assert
+ (forall ((p1 (infix_mngt Int Bool)) (p2 (infix_mngt Int Bool)) (a2 Int)
+ (b2 Int))
+ (=>
+ (forall ((j Int))
+ (=> (and (<= a2 j) (< j b2))
+ (=> (= (infix_at p1 j) true) (= (infix_at p2 j) true))))
+ (>= (numof p2 a2 b2) (numof p1 a2 b2)))))
+
+;; numof_change_some
+ (assert
+ (forall ((p1 (infix_mngt Int Bool)) (p2 (infix_mngt Int Bool)) (a2 Int)
+ (b2 Int) (i Int))
+ (=> (and (<= a2 i) (< i b2))
+ (=>
+ (forall ((j Int))
+ (=> (and (<= a2 j) (< j b2))
+ (=> (= (infix_at p1 j) true) (= (infix_at p2 j) true))))
+ (=> (not (= (infix_at p1 i) true))
+ (=> (= (infix_at p2 i) true) (> (numof p2 a2 b2) (numof p1 a2 b2))))))))
+
+;; numof_change_equiv
+ (assert
+ (forall ((p1 (infix_mngt Int Bool)) (p2 (infix_mngt Int Bool)) (a2 Int)
+ (b2 Int))
+ (=>
+ (forall ((j Int))
+ (=> (and (<= a2 j) (< j b2))
+ (= (= (infix_at p1 j) true) (= (infix_at p2 j) true))))
+ (= (numof p2 a2 b2) (numof p1 a2 b2)))))
+
+(declare-datatypes ((t_model 1))
+((par (a1) ((Null (Null_proj_1 Int)) (Value (Value_proj_1 a1))))))
+(declare-sort t 1)
+
+(declare-fun v (par (a1) ((t a1)) (t_model a1)))
+
+(define-fun is_null (par (a1)
+ ((t1 (t a1))) Bool (let ((subject (v t1)))
+ (ite ((_ is Null) subject) true false))))
+
+(declare-fun fc (par (a1) ((rarray (t a1)) a1) (infix_mngt Int Bool)))
+
+;; fc'def
+ (assert (par (a1)
+ (forall ((r (rarray (t a1))) (x a1) (i Int))
+ (= (= (infix_at (fc r x) i) true) (= (v (infix_at (data r) i)) (Value x))))))
+
+(define-fun numof1 (par (a1) ((r (rarray (t a1))) (x a1) (l Int)
+ (u Int)) Int (numof (fc r x) l u)))
+
+(declare-sort t1 1)
+
+(declare-fun size (par (a1) ((t1 a1)) Int))
+
+(declare-fun data1 (par (a1) ((t1 a1)) (rarray (t a1))))
+
+(declare-fun contents (par (a1) ((t1 a1)) (infix_mngt a1 Int)))
+
+;; t'invariant
+ (assert (par (a1)
+ (forall ((self (t1 a1)))
+ (! (and (and (<= 0 (size self)) (= (size self) (len (data1 self))))
+ (and
+ (forall ((i Int))
+ (=> (and (<= 0 i) (< i (size self)))
+ (not (is_null (mixfix_lbrb (data1 self) i)))))
+ (forall ((x a1))
+ (= (infix_at (contents self) x) (numof1 (data1 self) x 0 (size self)))))) :pattern (
+ (contents self)) :pattern ((data1 self)) :pattern ((size self)) ))))
+
+(declare-sort a2 0)
+
+(declare-fun fc1 () (infix_mngt a2 Int))
+
+(declare-fun fc2 () (infix_mngt a2 Int))
+
+;; fc'def
+ (assert (forall ((y0 a2)) (= (infix_at fc1 y0) 0)))
+
+;; fc'def
+ (assert (forall ((y0 a2)) (= (infix_at fc2 y0) 0)))
+
+(assert
+;; createqtvc
+ ;; File "why3/examples/bag.mlw", line 113, characters 6-12
+ (not
+ (forall ((null (t a2)))
+ (=> (is_null null)
+ (let ((result fc1))
+ (and (<= 0 0)
+ (forall ((o (rarray (t a2))))
+ (=> (and (= (len o) 0) (= (data o) (const1 null)))
+ (and
+ (and (and (<= 0 0) (= 0 (len o)))
+ (and
+ (forall ((i Int))
+ (=> (and (<= 0 i) (< i 0)) (not (is_null (mixfix_lbrb o i)))))
+ (forall ((x a2)) (= (infix_at result x) (numof1 o x 0 0)))))
+ (forall ((result1 (t1 a2)))
+ (=>
+ (and (= (size result1) 0)
+ (and (= (data1 result1) o) (= (contents result1) result)))
+ (and (= (size result1) 0) (infix_eqeq (contents result1) fc2)))))))))))))
+(check-sat)
diff --git a/src_colibri2/tests/solve/all/unsat/dune b/src_colibri2/tests/solve/all/unsat/dune
new file mode 100644
index 0000000000000000000000000000000000000000..6d9fe5883f08bc15b92dc715d3c58c193023dbb5
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/dune
@@ -0,0 +1,13 @@
+(include dune.inc)
+
+(rule
+ (alias runtest)
+ (deps
+ (glob_files *.cnf)
+ (glob_files *.smt2)
+ (glob_files *.psmt2))
+ (action
+ (with-stdout-to
+ dune.inc
+ (run %{exe:../../../generate_tests/generate_dune_tests.exe} . unsat)))
+ (mode promote))
diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
new file mode 100644
index 0000000000000000000000000000000000000000..5120eabbe923927229d66a7af3975baf6e9dc60c
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -0,0 +1,5 @@
+(rule (action (with-stdout-to oracle (echo "unsat\n"))))
+(rule (action (with-stdout-to bag-BagImpl-createqtvc.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:bag-BagImpl-createqtvc.psmt2}))))
+(rule (alias runtest) (action (diff oracle bag-BagImpl-createqtvc.psmt2.res)))
+(rule (action (with-stdout-to fact-FactRecursive-fact_recqtvc.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:fact-FactRecursive-fact_recqtvc.psmt2}))))
+(rule (alias runtest) (action (diff oracle fact-FactRecursive-fact_recqtvc.psmt2.res)))
diff --git a/src_colibri2/tests/solve/all/unsat/fact-FactRecursive-fact_recqtvc.psmt2 b/src_colibri2/tests/solve/all/unsat/fact-FactRecursive-fact_recqtvc.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..aeb3c6c3d5a21ad84f9b4db2c80e4f95aa5d0dc0
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/fact-FactRecursive-fact_recqtvc.psmt2
@@ -0,0 +1,27 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(declare-fun fact (Int) Int)
+
+;; fact'def
+ (assert
+ (forall ((n Int))
+ (=> (<= 0 n)
+ (ite (= n 0) (= (fact n) 1) (= (fact n) (* n (fact (- n 1))))))))
+
+(assert
+;; fact_recqtvc
+ ;; File "examples/fact.mlw", line 9, characters 10-18
+ (not
+ (forall ((x Int))
+ (=> (<= 0 x)
+ (and
+ (=> (not (= x 0))
+ (let ((o (- x 1))) (and (and (<= 0 x) (< o x)) (<= 0 o))))
+ (forall ((result Int))
+ (=>
+ (ite (= x 0) (= result 1) (= result (* x (fact (- x 1)))))
+ (= result (fact x))))
+ )))))
+(check-sat)
diff --git a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
index 9c4a2ebd51587acbfe31ccf0a461a9757b1d4c06..55451ca3a29b790a96c17ab2251b3c0144b8e89d 100644
--- a/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_adt/unsat/dune.inc
@@ -13,3 +13,5 @@
(rule (alias runtest) (action (diff oracle list3.smt2.res)))
(rule (action (with-stdout-to list4.smt2.res (run %{bin:colibri2} --max-step 3000 %{dep:list4.smt2}))))
(rule (alias runtest) (action (diff oracle list4.smt2.res)))
+(rule (action (with-stdout-to parlist0.psmt2.res (run %{bin:colibri2} --max-step 3000 %{dep:parlist0.psmt2}))))
+(rule (alias runtest) (action (diff oracle parlist0.psmt2.res)))
diff --git a/src_colibri2/tests/solve/smt_adt/unsat/parlist0.psmt2 b/src_colibri2/tests/solve/smt_adt/unsat/parlist0.psmt2
index 66fa9e1701c3446237a0445ec4caba30c10f51f2..9b0f6334bc083def5576b4e975eb99b81815c9d3 100644
--- a/src_colibri2/tests/solve/smt_adt/unsat/parlist0.psmt2
+++ b/src_colibri2/tests/solve/smt_adt/unsat/parlist0.psmt2
@@ -7,6 +7,6 @@
(define-fun singleton (par (a) ((x a)) (list a) (cons x nil)))
-(assert (not (= nil (singleton 1))))
+(assert (= nil (singleton 1)))
(check-sat)
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 23aad9c4b967f78ffbfd4ed8dc850f8297f65edd..f6e37854985117f4c7366e2ff107401ca448ae1e 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -6,6 +6,9 @@ let scheduled = Datastructure.Ref.create Bool.pp "LRA.fourier.scheduled" false
let debug = Debug.register_info_flag ~desc:"Reasoning about <= < in LRA" "fourier"
+let stats_run = Debug.register_stats_int ~name:"Fourier.run" ~init:0
+
+
type eq = { p: Polynome.t; bound: Interval.Bound.t; origins: Ground.S.t }
[@@deriving show]
(** p <= 0 or p < 0 *)
@@ -70,29 +73,65 @@ let delta d eq =
Delta.add d src (Q.neg eq.p.cst) eq.bound dst
| _ -> ()
+let apply d ~f truth g =
+ let aux d bound a b =
+ let bound = if truth then bound else match bound with | Interval.Bound.Large -> Strict | Strict -> Large in
+ let a,b = if truth then a,b else b,a in
+ f d bound a b
+ in
+ match Ground.sem g with
+ | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
+ let a,b = IArray.extract2_exn args in
+ aux d Interval.Bound.Strict a b
+ | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
+ let a,b = IArray.extract2_exn args in
+ aux d Large a b
+ | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
+ let a,b = IArray.extract2_exn args in
+ aux d Large b a
+ | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
+ let a,b = IArray.extract2_exn args in
+ aux d Strict b a
+ | _ -> assert false
+
+
let add_eq d eqs p bound origins =
match Polynome.is_cst p, bound with
| None, _ ->
let eq = { p; bound; origins } in
delta d eq;
eq::eqs
- | Some p, Interval.Bound.Large when Q.sign p <= 0 ->
- Debug.dprintf2 debug "[Fourier] discard %a" Ground.S.pp origins;
+ | Some p, Interval.Bound.Large when Q.sign p = 0 ->
+ Ground.S.iter (fun g ->
+ let truth = Option.get_exn (Boolean.is d (Ground.node g)) in
+ apply d truth g ~f:(fun d bound a b ->
+ match bound with
+ | Strict when Dom_interval.is_integer d a && Dom_interval.is_integer d b ->
+ Dom_polynome.assume_poly_equality d a (Polynome.of_list Q.minus_one [b,Q.one])
+ | Large ->
+ Dom_polynome.assume_poly_equality d a (Polynome.monome Q.one b)
+ | Strict ->
+ assert false
+ )) origins;
eqs
- | Some p, Interval.Bound.Strict when Q.sign p < 0 ->
+ | Some p, _ when Q.sign p < 0 ->
Debug.dprintf2 debug "[Fourier] discard %a" Ground.S.pp origins;
eqs
| _ -> Egraph.contradiction d
-let mk_eq d bound truth a b =
+let mk_eq d bound a b =
let (!) n =
match Egraph.get_dom d Dom_polynome.dom n with
| None -> Polynome.monome Q.one (Egraph.find_def d n)
| Some p -> p in
- let bound = if truth then bound else match bound with | Interval.Bound.Large -> Strict | Strict -> Large in
- let a,b = if truth then a,b else b,a in
- Polynome.sub (!a) (!b), bound,
- Polynome.sub (Polynome.monome Q.one a) (Polynome.monome Q.one b)
+ let p,bound' =
+ match bound with
+ | Interval.Bound.Strict when Dom_interval.is_integer d a && Dom_interval.is_integer d b ->
+ Polynome.add_cst (Polynome.sub (!a) (!b)) Q.one, Interval.Bound.Large
+ | _ -> Polynome.sub (!a) (!b), bound
+ in
+ p,bound',
+ Polynome.sub (Polynome.monome Q.one a) (Polynome.monome Q.one b), bound
let make_equations d (eqs,vars) g =
Debug.dprintf2 debug "[Fourier] %a" Ground.pp g;
@@ -100,23 +139,10 @@ let make_equations d (eqs,vars) g =
| None ->
(eqs,vars)
| Some truth ->
- let p,bound,p_non_norm =
- match Ground.sem g with
- | { app = {builtin = Expr.Lt}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- mk_eq d Strict truth a b
- | { app = {builtin = Expr.Leq}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- mk_eq d Large truth a b
- | { app = {builtin = Expr.Geq}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- mk_eq d Large truth b a
- | { app = {builtin = Expr.Gt}; tyargs = []; args; _ } ->
- let a,b = IArray.extract2_exn args in
- mk_eq d Strict truth b a
- | _ -> assert false
+ let p,bound,p_non_norm,bound_non_norm =
+ apply d ~f:mk_eq truth g
in
- Debug.dprintf5 debug "[Fourier] %b %a(%a)" truth Polynome.pp p Polynome.pp p_non_norm;
+ Debug.dprintf6 debug "[Fourier] %a(%a)%a0" Polynome.pp p Polynome.pp p_non_norm Interval.Bound.pp bound;
let eqs, vars =
(add_eq d eqs p bound (Ground.S.singleton g),
Node.M.union_merge (fun _ _ _ -> Some ()) vars p.Polynome.poly)
@@ -124,12 +150,13 @@ let make_equations d (eqs,vars) g =
match divide d p_non_norm with
| Some (p',_,_) ->
let p' = Dom_polynome.norm d p' in
- (add_eq d eqs p' bound Ground.S.empty,
+ (add_eq d eqs p' bound_non_norm Ground.S.empty,
Node.M.union_merge (fun _ _ _ -> Some ()) vars p'.Polynome.poly)
| None -> eqs, vars
let fm (d:Egraph.t) =
Debug.dprintf0 debug "[Fourier]";
+ Debug.incr stats_run;
Datastructure.Ref.set scheduled d false;
let eqs, vars = Datastructure.Queue.fold comparisons d
~f:(make_equations d) ~init:([],Node.S.empty)
diff --git a/src_colibri2/theories/LRA/integer_sign_domain.ml b/src_colibri2/theories/LRA/integer_sign_domain.ml
index ad8e9a52c18bd06b4322f2cba83578616b3e5b9e..e521eea13acec1a1ce79c4b391ae0a8f2ae6f5ef 100644
--- a/src_colibri2/theories/LRA/integer_sign_domain.ml
+++ b/src_colibri2/theories/LRA/integer_sign_domain.ml
@@ -33,7 +33,7 @@ module T = struct
let pp fmt t =
- let prefix s = if t.noninteger then "â„•"^s else s in
+ let prefix s = if t.noninteger then s else "â„•"^s in
Fmt.string fmt @@
match t.sign.neg, t.sign.zero, t.sign.pos with
| true, true, true -> if t.noninteger then "â„" else "â„•"
diff --git a/src_colibri2/theories/LRA/polynome.ml b/src_colibri2/theories/LRA/polynome.ml
index 88a42251db1009db22ff6390e7eb71e998dfcaf5..8a7900a48fd398cc9f0e3dc200fbda5543a9b46c 100644
--- a/src_colibri2/theories/LRA/polynome.ml
+++ b/src_colibri2/theories/LRA/polynome.ml
@@ -97,6 +97,7 @@ let is_one_node p = (** cst = 0 and one empty monome *)
else None
let sub_cst p q = {p with cst = Q.sub p.cst q}
+let add_cst p q = {p with cst = Q.add p.cst q}
let mult_cst c p1 =
if Q.equal Q.one c then p1
diff --git a/src_colibri2/theories/LRA/polynome.mli b/src_colibri2/theories/LRA/polynome.mli
index 3f5a6f05386cd495818858b207055f75e082d054..bd9ada2d33d7ad18311f08858158832a6b6a9605 100644
--- a/src_colibri2/theories/LRA/polynome.mli
+++ b/src_colibri2/theories/LRA/polynome.mli
@@ -46,6 +46,7 @@ type kind = | ZERO | CST | VAR
val classify : t -> kind
val sub_cst: t -> Q.t -> t
+val add_cst: t -> Q.t -> t
val mult_cst: Q.t -> t -> t
val add: t -> t -> t
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index b3ee59315080ca2e4b318110d7a5a3bf3a55b9b2..7b8ce5a3032c9b12f4cf78d376cf1ccf5c29e9e8 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -189,32 +189,37 @@ module TwoWatchLiteral = struct
let args = (Ground.sem r.ground).args in
if o_from_start = o_from_end then Events.Wait.EnqStopped
else
- let n_end = IArray.get args o_from_end in
- match check_if_equal_or_set d args r.absorbent (+1) o_from_end o_from_start
- n_end with
- | LimitReached ->
- Context.Ref.set r.from_start o_from_end;
- Events.Wait.EnqLast(fun d -> Egraph.merge d n_end (Ground.node r.ground))
- | Absorbent ->
- Events.Wait.EnqLast(fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent)
- | ToWatch from_start ->
- if from_start <> o_from_start then (
- Context.Ref.set r.from_start from_start;
- attach d r from_start;
- );
- let n_start = IArray.get args from_start in
- match check_if_equal_or_set d args r.absorbent (-1) from_start o_from_end n_start with
+ match Egraph.Ro.get_value d (Ground.node r.ground) with
+ | Some v when not (Value.equal v r.absorbent) ->
+ Context.Ref.set r.from_end o_from_start;
+ Events.Wait.EnqLast(fun d -> IArray.iter ~f:(fun a -> Egraph.set_value d a v) args)
+ | _ ->
+ let n_end = IArray.get args o_from_end in
+ match check_if_equal_or_set d args r.absorbent (+1) o_from_end o_from_start
+ n_end with
| LimitReached ->
- Context.Ref.set r.from_end from_start;
- Events.Wait.EnqLast (fun d -> Egraph.merge d n_start (Ground.node r.ground))
+ Context.Ref.set r.from_start o_from_end;
+ Events.Wait.EnqLast(fun d -> Egraph.merge d n_end (Ground.node r.ground))
| Absorbent ->
- Events.Wait.EnqLast (fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent)
- | ToWatch from_end when from_end = o_from_end ->
- Events.Wait.EnqAlready
- | ToWatch from_end ->
- Context.Ref.set r.from_end from_end;
- attach d r from_end;
- Events.Wait.EnqAlready
+ Events.Wait.EnqLast(fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent)
+ | ToWatch from_start ->
+ if from_start <> o_from_start then (
+ Context.Ref.set r.from_start from_start;
+ attach d r from_start;
+ );
+ let n_start = IArray.get args from_start in
+ match check_if_equal_or_set d args r.absorbent (-1) from_start o_from_end n_start with
+ | LimitReached ->
+ Context.Ref.set r.from_end from_start;
+ Events.Wait.EnqLast (fun d -> Egraph.merge d n_start (Ground.node r.ground))
+ | Absorbent ->
+ Events.Wait.EnqLast (fun d -> Egraph.set_value d (Ground.node r.ground) r.absorbent)
+ | ToWatch from_end when from_end = o_from_end ->
+ Events.Wait.EnqAlready
+ | ToWatch from_end ->
+ Context.Ref.set r.from_end from_end;
+ attach d r from_end;
+ Events.Wait.EnqAlready
let enqueue d event =
match event with
@@ -229,34 +234,38 @@ module TwoWatchLiteral = struct
if IArray.length args = 1 then
Egraph.merge d (IArray.get args 0) (Ground.node ground)
else
- let r from_start from_end =
- assert (from_start < from_end);
- Debug.dprintf4 debug "Bool create %a (%i-%i)" Ground.pp ground
- from_start from_end;
- {
- ground; absorbent;
- from_start = Context.Ref.create (Egraph.context d) from_start;
- from_end = Context.Ref.create (Egraph.context d) from_end;
- }
- in
- match check_if_set (d :> Egraph.Ro.t) args absorbent 1 (IArray.length args - 1) 0 with
- | LimitReached ->
- Egraph.merge d (IArray.get args (IArray.length args - 1)) (Ground.node ground)
- | Absorbent ->
- Egraph.set_value d (Ground.node ground) absorbent
- | ToWatch from_start ->
- let n_start = IArray.get args from_start in
- match
- check_if_equal_or_set (d :> Egraph.Ro.t) args absorbent (-1) from_start (IArray.length args - 1) n_start
- with
- | LimitReached ->
- Egraph.merge d n_start (Ground.node ground)
- | Absorbent ->
- Egraph.set_value d (Ground.node ground) absorbent
- | ToWatch from_end ->
- let r = r from_start from_end in
- attach (d :> Egraph.Ro.t) r from_start;
- attach (d :> Egraph.Ro.t) r from_end
+ match Egraph.get_value d (Ground.node ground) with
+ | Some v when not (Value.equal v absorbent) ->
+ IArray.iter ~f:(fun a -> Egraph.set_value d a v) args
+ | _ ->
+ let r from_start from_end =
+ assert (from_start < from_end);
+ Debug.dprintf4 debug "Bool create %a (%i-%i)" Ground.pp ground
+ from_start from_end;
+ {
+ ground; absorbent;
+ from_start = Context.Ref.create (Egraph.context d) from_start;
+ from_end = Context.Ref.create (Egraph.context d) from_end;
+ }
+ in
+ match check_if_set (d :> Egraph.Ro.t) args absorbent 1 (IArray.length args - 1) 0 with
+ | LimitReached ->
+ Egraph.merge d (IArray.get args (IArray.length args - 1)) (Ground.node ground)
+ | Absorbent ->
+ Egraph.set_value d (Ground.node ground) absorbent
+ | ToWatch from_start ->
+ let n_start = IArray.get args from_start in
+ match
+ check_if_equal_or_set (d :> Egraph.Ro.t) args absorbent (-1) from_start (IArray.length args - 1) n_start
+ with
+ | LimitReached ->
+ Egraph.merge d n_start (Ground.node ground)
+ | Absorbent ->
+ Egraph.set_value d (Ground.node ground) absorbent
+ | ToWatch from_end ->
+ let r = r from_start from_end in
+ attach (d :> Egraph.Ro.t) r from_start;
+ attach (d :> Egraph.Ro.t) r from_end
end
let () = Egraph.Wait.register_dem (module Daemon)
@@ -314,6 +323,9 @@ let converter d (f:Ground.t) =
| { app = {builtin = Expr.False}; tyargs = []; args; _ } ->
assert ( IArray.is_empty args);
reg _false
+ | { ty; _ }
+ when Ground.Ty.equal ty Ground.Ty.bool ->
+ Egraph.register_decision d (chobool res)
| _ -> ()
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
index 61c29b4c0cfbb75fe92fc644734344cb0134c3db..7cfbd188b89b626c02b7e1cac3c19b2f12fde9d5 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.ml
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -129,7 +129,7 @@ let insert_pattern d (trigger : Trigger.t) =
let rec aux (fp : F_Pos.t) pp_vars p =
match p with
| Pattern.Var v ->
- let pairs = Expr.Term.Var.M.find_def [] v pp_vars in
+ let pairs = Expr.Term.Var.M.find_def [] v.var pp_vars in
let pairs =
List.filter
(fun pp ->
diff --git a/src_colibri2/theories/quantifier/InvertedPath.mli b/src_colibri2/theories/quantifier/InvertedPath.mli
index c2551744b710523b0c167020b69b9811f1c9994f..9c0eda7e93c61d16d63c13b49ebd8603892dd1d7 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.mli
+++ b/src_colibri2/theories/quantifier/InvertedPath.mli
@@ -31,7 +31,7 @@ val pc_ips : t HPC.t
module HPT : Datastructure.Memo with type key := F_Pos.t
-val pt_ips : (Ty.t * t) Context.Queue.t HPT.t
+val pt_ips : (Expr.Ty.t * t) Context.Queue.t HPT.t
(** The database of inverted path for each parent-type, needed for polymorphic
variables *)
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index 26af230dfaba9d4a79cc8cd93e8a02dc4a1e9bda..3412d3f4e3665d485736a329adc11c464131ca39 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -7,13 +7,15 @@ module T = struct
open Base
type t =
- | Var of Expr.Term.Var.t
+ | Var of { var : Expr.Term.Var.t; ty : Expr.Ty.t }
| App of F.t * Expr.Ty.t list * t IArray.t
| Node of Node.t
[@@deriving eq, ord, hash]
let rec pp fmt = function
- | Var v -> Expr.Term.Var.pp fmt v
+ | Var v ->
+ if Expr.Ty.equal v.var.ty v.ty then Expr.Term.Var.pp fmt v.var
+ else Fmt.pf fmt "(%a:%a)" Expr.Term.Var.pp v.var Expr.Ty.pp v.ty
| App (f, tyl, tl) ->
Fmt.pf fmt "%a[%a](%a)" F.pp f
Fmt.(list ~sep:comma Expr.Ty.pp)
@@ -26,16 +28,29 @@ end
include T
include Popop_stdlib.MkDatatype (T)
+let rec convert_back (ty : Ground.Ty.t) =
+ Expr.Ty.apply ty.app (List.map convert_back ty.args)
+
+let rec subst_ty subst (ty : Expr.Ty.t) =
+ match ty.descr with
+ | Var v -> (
+ match Expr.Ty.Var.M.find_opt v subst with
+ | Some ty -> convert_back ty
+ | None -> ty)
+ | App (f, args) -> Expr.Ty.apply f (List.map (subst_ty subst) args)
+
let rec of_term ~subst (t : Expr.Term.t) =
match t.descr with
| Var v -> (
match Expr.Term.Var.M.find v subst.Ground.Subst.term with
- | exception Not_found -> Var v (* todo type substitution *)
+ | exception Not_found -> Var { var = v; ty = subst_ty subst.ty v.ty }
| n -> Node n)
| App ({ builtin = Expr.Coercion; _ }, _, [ a ]) -> of_term ~subst a
| App (f, tys, tl) ->
- (* todo type substitution *)
- App (f, tys, IArray.of_list_map ~f:(of_term ~subst) tl)
+ App
+ ( f,
+ List.map (subst_ty subst.ty) tys,
+ IArray.of_list_map ~f:(of_term ~subst) tl )
| _ -> (* absurd *) assert false
let init = Ground.Subst.S.singleton Ground.Subst.empty
@@ -76,10 +91,10 @@ let rec match_term d (substs : Ground.Subst.S.t) (n : Node.t) (p : t) :
in
Ground.Subst.S.fold_left
(fun acc subst ->
- match Expr.Term.Var.M.find v subst.term with
+ match Expr.Term.Var.M.find v.var subst.term with
| exception Not_found ->
Ground.Subst.S.add
- { subst with term = Expr.Term.Var.M.add v n subst.term }
+ { subst with term = Expr.Term.Var.M.add v.var n subst.term }
acc
| n' ->
if Egraph.is_equal d n n' then Ground.Subst.S.add subst acc
@@ -123,7 +138,7 @@ let rec check_term d (subst : Ground.Subst.t) (n : Node.t) (p : t) : bool =
| Var v -> (
Ground.Ty.S.exists (fun ty -> check_ty subst ty v.ty) (Ground.tys d n)
&&
- match Expr.Term.Var.M.find v subst.term with
+ match Expr.Term.Var.M.find v.var subst.term with
| exception Not_found -> false
| n' -> Egraph.is_equal d n n')
| App (pf, ptyl, pargs) ->
@@ -150,7 +165,7 @@ exception IncompleteSubstitution
let rec check_term_exists_exn d (subst : Ground.Subst.t) (p : t) : Node.S.t =
match p with
| Var v -> (
- match Expr.Term.Var.M.find v subst.term with
+ match Expr.Term.Var.M.find v.var subst.term with
| exception Not_found -> raise IncompleteSubstitution
| n ->
if
@@ -204,7 +219,8 @@ let check_term_exists d (subst : Ground.Subst.t) (p : t) : Node.S.t =
let get_pps pattern =
let rec aux acc fp p =
match p with
- | Var v -> Expr.Term.Var.M.add_change F_Pos.S.singleton F_Pos.S.add v fp acc
+ | Var v ->
+ Expr.Term.Var.M.add_change F_Pos.S.singleton F_Pos.S.add v.var fp acc
| App (f, _, tl) ->
IArray.foldi
~f:(fun pos acc p -> aux acc F_Pos.{ f; pos } p)
@@ -253,7 +269,10 @@ let match_any_term d (p : t) : Ground.Subst.S.t =
Context.Queue.fold
(fun acc n ->
Ground.Subst.S.add
- { subst with term = Expr.Term.Var.M.add v n subst.term }
+ {
+ subst with
+ term = Expr.Term.Var.M.add v.var n subst.term;
+ }
acc)
acc q)
acc substs)
diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli
index a545681a16217f9c9076b5f07d626883ae2fce6c..b820c35f9c8544e239cdd913d32398f0b3a68c07 100644
--- a/src_colibri2/theories/quantifier/pattern.mli
+++ b/src_colibri2/theories/quantifier/pattern.mli
@@ -1,8 +1,9 @@
open Colibri2_popop_lib
+
(** Pattern *)
type t =
- | Var of Expr.Term.Var.t
+ | Var of { var : Expr.Term.Var.t; ty : Expr.Ty.t }
| App of F.t * Expr.Ty.t list * t IArray.t
| Node of Node.t
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index aab7a0b9df825935ef1d1926fd23270aefe8a0cc..aff0944fd316b4c6e51e3b22add75dba38c18ddf 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -187,14 +187,11 @@ let skolemize d (e : Ground.ClosedQuantifier.t) =
(fun acc v ->
let id = Expr.Term.Const.mk v.Expr.name [] [] v.ty in
let t = Expr.Term.apply id [] [] in
- Expr.Term.Var.M.add v (Ground.convert t) acc)
+ Expr.Term.Var.M.add v (Ground.convert ~subst:e.subst t) acc)
e.subst.term e.term_vars
in
- let n =
- Ground.convert
- ~subst:{ Ground.Subst.ty = e.subst.ty; term = subst_term }
- e.body
- in
+ let subst = { Ground.Subst.ty = e.subst.ty; term = subst_term } in
+ let n = Ground.convert ~subst e.body in
Egraph.register d n;
n
@@ -205,6 +202,8 @@ let init, attach =
match (Ground.ThClosedQuantifier.sem th, b) with
| ({ binder = Exists; _ } as e), true
| ({ binder = Forall; _ } as e), false ->
+ Debug.dprintf2 debug "[Quant] Skolemize %a"
+ Ground.ThClosedQuantifier.pp th;
Egraph.merge d (skolemize d e) n
| { binder = Exists; _ }, false | { binder = Forall; _ }, true ->
let triggers = Trigger.compute_top_triggers th in
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index 4232d43c936ae90e49541f2ac7e3f3a17de3d72b..d8f35bb6fe4f6765172eafe3c049228186a8b3a7 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -7,7 +7,7 @@ module T = struct
type t = {
pat : Pattern.t;
checks : Pattern.t list;
- (* list *) form : Ground.ThClosedQuantifier.t;
+ form : Ground.ThClosedQuantifier.t;
eager : bool;
}
[@@deriving eq, ord, hash]
@@ -120,7 +120,7 @@ let compute_all_triggers (cq : Ground.ThClosedQuantifier.t) =
let pats =
List.filter_map
(fun (c, (sty, st)) ->
- if Expr.Ty.Var.S.equal sty tyvs && Expr.Term.Var.S.equal st tvs then
+ if Expr.Ty.Var.S.subset tyvs sty && Expr.Term.Var.S.subset tvs st then
Some
{
pat = Pattern.of_term ~subst:cq'.subst c;
@@ -148,16 +148,7 @@ let add_trigger d t =
let instantiate_aux d tri subst =
let form = Ground.ThClosedQuantifier.sem tri.form in
Debug.incr nb_instantiation;
- let subst =
- {
- Ground.Subst.ty =
- Expr.Ty.Var.M.union (fun _ _ -> assert false) subst.ty form.subst.ty;
- Ground.Subst.term =
- Expr.Term.Var.M.union
- (fun _ _ -> assert false)
- subst.Ground.Subst.term form.subst.term;
- }
- in
+ let subst = Ground.Subst.distinct_union subst form.subst in
let n = Ground.convert ~subst form.body in
if Debug.test_flag Debug.stats && not (Egraph.is_registered d n) then
Debug.incr nb_new_instantiation;