diff --git a/colibri2/core/choice_group.ml b/colibri2/core/choice_group.ml
index 77a101da112be0d1c5a7c93d8bdcab9fd951867a..004d705cda42337799d9b45c7d955342c8d4b8e8 100644
--- a/colibri2/core/choice_group.ml
+++ b/colibri2/core/choice_group.ml
@@ -43,6 +43,7 @@ let register_decision d thterm choice =
match HThTerm.find state d thterm with
| Choosable -> Egraph.register_decision d choice
| Init ->
+ (* HThTerm.set state d thterm (Wait { choices = [ choice ]; groups = [] }) *)
HThTerm.set state d thterm Choosable;
Egraph.register_decision d choice
| Wait l ->
diff --git a/colibri2/core/colibri2_core.mli b/colibri2/core/colibri2_core.mli
index 77569584205602394fb8c226c5c9f72b90c9f24e..755416923967b8ce982bd8e8d20bc138c363108b 100644
--- a/colibri2/core/colibri2_core.mli
+++ b/colibri2/core/colibri2_core.mli
@@ -317,6 +317,36 @@ and Ground : sig
val convert_one_binder :
Subst.t -> 'a Egraph.t -> Expr.binder -> Expr.term -> Expr.ty -> Node.t
+ val convert_one_app_and_iter :
+ 'a ->
+ Expr.term ->
+ Expr.ty list ->
+ Node.t Colibri2_popop_lib.IArray.t ->
+ Expr.ty ->
+ Subst.t ->
+ ('a -> t -> unit) ->
+ ('a -> ClosedQuantifier.t -> unit) ->
+ ('a -> NotTotallyApplied.t -> unit) ->
+ Node.t
+
+ val convert_one_cst_and_iter :
+ 'a ->
+ Expr.term_cst ->
+ Subst.t ->
+ ('a -> t -> unit) ->
+ ('a -> NotTotallyApplied.t -> unit) ->
+ Node.t
+
+ val convert_one_binder_and_iter :
+ 'a ->
+ Expr.binder ->
+ Expr.term ->
+ Expr.ty ->
+ Subst.t ->
+ ('a -> ClosedQuantifier.t -> unit) ->
+ ('a -> NotTotallyApplied.t -> unit) ->
+ Node.t
+
val convert_let_seq :
Subst.t ->
'a ->
diff --git a/colibri2/core/ground.mli b/colibri2/core/ground.mli
index c331cda8a3d81f84bd78d25fc1aeab673565cf2a..6bef1d7e22a30a6620149b316c76bc3816d672f6 100644
--- a/colibri2/core/ground.mli
+++ b/colibri2/core/ground.mli
@@ -193,6 +193,36 @@ val convert_one_cst :
val convert_one_binder :
Subst.t -> 'a Egraph.t -> Expr.binder -> Expr.term -> Expr.ty -> Node.t
+val convert_one_app_and_iter :
+ 'a ->
+ Expr.term ->
+ Expr.ty list ->
+ Node.t Colibri2_popop_lib.IArray.t ->
+ Expr.ty ->
+ Subst.t ->
+ ('a -> t -> unit) ->
+ ('a -> ClosedQuantifier.t -> unit) ->
+ ('a -> NotTotallyApplied.t -> unit) ->
+ Node.t
+
+val convert_one_cst_and_iter :
+ 'a ->
+ Dolmen_std.Expr.term_cst ->
+ Subst.t ->
+ ('a -> t -> unit) ->
+ ('a -> NotTotallyApplied.t -> unit) ->
+ Node.t
+
+val convert_one_binder_and_iter :
+ 'a ->
+ Expr.binder ->
+ Expr.term ->
+ Expr.ty ->
+ Subst.t ->
+ ('a -> ClosedQuantifier.t -> unit) ->
+ ('a -> NotTotallyApplied.t -> unit) ->
+ Node.t
+
val convert_let_seq :
Subst.t ->
'a ->
diff --git a/colibri2/solver/scheduler.ml b/colibri2/solver/scheduler.ml
index 6adbd53951cad76c09afdcdeafc6e32e933f571a..5373ac754d47f6f5374e9f986a1132e90cf7fc94 100644
--- a/colibri2/solver/scheduler.ml
+++ b/colibri2/solver/scheduler.ml
@@ -578,13 +578,20 @@ let run_one_step_propagation ~nodec t =
| Some (Steps step_limit) -> step_limit <= t.steps
| _ -> false
in
- Debug.dprintf2 debug_queue "[Scheduler] LastEffort: %i%s"
- (PrioLastEffort.size t.lasteffort)
- (if last_effort_deactivated then " (deactivated)" else "");
- if last_effort_deactivated then false
+ if last_effort_deactivated then (
+ Debug.dprintf1 debug_queue
+ "[Scheduler] LastEffort: %i (deactivated)"
+ (PrioLastEffort.size t.lasteffort);
+ false)
else
match PrioLastEffort.extract_min t.lasteffort with
| Some att as o ->
+ Debug.dprintf3 debug_queue "[Scheduler] LastEffort: %i after %a"
+ (PrioLastEffort.size t.lasteffort)
+ (fun fmt (att : PrioLastEffort.Att.t) ->
+ match att.v with
+ | DaemonKey (k, _, _) -> Events.Dem.pp fmt k)
+ att;
Debug.incr stats_lasteffort;
t.last_effort_made <- o;
protect_against_contradiction ~no_learning:true t
@@ -593,6 +600,7 @@ let run_one_step_propagation ~nodec t =
Backtrackable.run_daemon d att.v)
(fun () -> true)
| None ->
+ Debug.dprintf0 debug_queue "[Scheduler] LastEffort: 0";
t.last_effort_made <- None;
false
(* else false *)))
diff --git a/colibri2/tests/solve/all/unsat/wp_initialize.psmt2 b/colibri2/tests/solve/all/unsat/wp_initialize.psmt2
new file mode 100644
index 0000000000000000000000000000000000000000..ed012f60eaaaf68d9304017d949402769e7996d0
--- /dev/null
+++ b/colibri2/tests/solve/all/unsat/wp_initialize.psmt2
@@ -0,0 +1,1015 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(set-option :max-steps-colibri2 8000)
+;;; SMT-LIB2: integer arithmetic
+;;; SMT-LIB2: real arithmetic
+(declare-sort string 0)
+
+(declare-datatypes ((tuple0 0))
+ (((Tuple0))))
+
+;; "abs"
+(define-fun abs1 ((x Int)) Int
+ (ite (>= x 0) x (- x)))
+
+;; "Abs_le"
+(assert
+ (forall ((x Int) (y Int)) (= (<= (abs1 x) y) (and (<= (- y) x) (<= x y)))))
+
+;; "Abs_pos"
+(assert (forall ((x Int)) (>= (abs1 x) 0)))
+
+;; "div"
+(declare-fun div1 (Int
+ Int) Int)
+
+;; "mod"
+(declare-fun mod1 (Int
+ Int) Int)
+
+;; "Div_mod"
+(assert
+ (forall ((x Int) (y Int))
+ (=> (not (= y 0)) (= x (+ (* y (div1 x y)) (mod1 x y))))))
+
+;; "Div_bound"
+(assert
+ (forall ((x Int) (y Int))
+ (=> (and (>= x 0) (> y 0)) (and (<= 0 (div1 x y)) (<= (div1 x y) x)))))
+
+;; "Mod_bound"
+(assert
+ (forall ((x Int) (y Int))
+ (=>
+ (not (= y 0))
+ (and (< (- (abs1 y)) (mod1 x y)) (< (mod1 x y) (abs1 y))))))
+
+;; "Div_sign_pos"
+(assert
+ (forall ((x Int) (y Int)) (=> (and (>= x 0) (> y 0)) (>= (div1 x y) 0))))
+
+;; "Div_sign_neg"
+(assert
+ (forall ((x Int) (y Int)) (=> (and (<= x 0) (> y 0)) (<= (div1 x y) 0))))
+
+;; "Mod_sign_pos"
+(assert
+ (forall ((x Int) (y Int))
+ (=> (and (>= x 0) (not (= y 0))) (>= (mod1 x y) 0))))
+
+;; "Mod_sign_neg"
+(assert
+ (forall ((x Int) (y Int))
+ (=> (and (<= x 0) (not (= y 0))) (<= (mod1 x y) 0))))
+
+;; "Rounds_toward_zero"
+(assert
+ (forall ((x Int) (y Int))
+ (=> (not (= y 0)) (<= (abs1 (* (div1 x y) y)) (abs1 x)))))
+
+;; "Div_1"
+(assert (forall ((x Int)) (= (div1 x 1) x)))
+
+;; "Mod_1"
+(assert (forall ((x Int)) (= (mod1 x 1) 0)))
+
+;; "Div_inf"
+(assert
+ (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (div1 x y) 0))))
+
+;; "Mod_inf"
+(assert
+ (forall ((x Int) (y Int)) (=> (and (<= 0 x) (< x y)) (= (mod1 x y) x))))
+
+;; "Div_mult"
+(assert
+ (forall ((x Int) (y Int) (z Int))
+ (! (=>
+ (and (> x 0) (and (>= y 0) (>= z 0)))
+ (= (div1 (+ (* x y) z) x) (+ y (div1 z x)))) :pattern ((div1
+ (+ (* x y) z)
+ x)) )))
+
+;; "Mod_mult"
+(assert
+ (forall ((x Int) (y Int) (z Int))
+ (! (=>
+ (and (> x 0) (and (>= y 0) (>= z 0)))
+ (= (mod1 (+ (* x y) z) x) (mod1 z x))) :pattern ((mod1
+ (+ (* x y) z)
+ x)) )))
+
+;; "add_div"
+(assert
+ (forall ((x Real) (y Real) (z Real))
+ (=> (not (= z 0.0)) (= (/ (+ x y) z) (+ (/ x z) (/ y z))))))
+
+;; "sub_div"
+(assert
+ (forall ((x Real) (y Real) (z Real))
+ (=> (not (= z 0.0)) (= (/ (- x y) z) (- (/ x z) (/ y z))))))
+
+;; "neg_div"
+(assert
+ (forall ((x Real) (y Real))
+ (=> (not (= y 0.0)) (= (/ (- x) y) (- (/ x y))))))
+
+;; "assoc_mul_div"
+(assert
+ (forall ((x Real) (y Real) (z Real))
+ (=> (not (= z 0.0)) (= (/ (* x y) z) (* x (/ y z))))))
+
+;; "assoc_div_mul"
+(assert
+ (forall ((x Real) (y Real) (z Real))
+ (=>
+ (and (not (= y 0.0)) (not (= z 0.0)))
+ (= (/ (/ x y) z) (/ x (* y z))))))
+
+;; "assoc_div_div"
+(assert
+ (forall ((x Real) (y Real) (z Real))
+ (=>
+ (and (not (= y 0.0)) (not (= z 0.0)))
+ (= (/ x (/ y z)) (/ (* x z) y)))))
+
+;; "infix +."
+(define-fun infix_pldt ((x Real) (y Real)) Real
+ (+ x y))
+
+;; "infix -."
+(define-fun infix_mndt ((x Real) (y Real)) Real
+ (- x y))
+
+;; "infix *."
+(define-fun infix_asdt ((x Real) (y Real)) Real
+ (* x y))
+
+;; "infix /."
+(define-fun infix_sldt ((x Real) (y Real)) Real
+ (/ x y))
+
+;; "prefix -."
+(define-fun prefix_mndt ((x Real)) Real
+ (- x))
+
+;; "inv"
+(define-fun inv ((x Real)) Real
+ (/ 1.0 x))
+
+;; "infix <=."
+(define-fun infix_lseqdt ((x Real) (y Real)) Bool
+ (<= x y))
+
+;; "infix >=."
+(define-fun infix_gteqdt ((x Real) (y Real)) Bool
+ (>= x y))
+
+;; "infix <."
+(define-fun infix_lsdt ((x Real) (y Real)) Bool
+ (< x y))
+
+;; "infix >."
+(define-fun infix_gtdt ((x Real) (y Real)) Bool
+ (> x y))
+
+;; "Zero"
+(assert (= (to_real 0) 0.0))
+
+;; "One"
+(assert (= (to_real 1) 1.0))
+
+;; "Add"
+(assert
+ (forall ((x Int) (y Int))
+ (= (to_real (+ x y)) (+ (to_real x) (to_real y)))))
+
+;; "Sub"
+(assert
+ (forall ((x Int) (y Int))
+ (= (to_real (- x y)) (- (to_real x) (to_real y)))))
+
+;; "Mul"
+(assert
+ (forall ((x Int) (y Int))
+ (= (to_real (* x y)) (* (to_real x) (to_real y)))))
+
+;; "Neg"
+(assert (forall ((x Int)) (= (to_real (- x)) (- (to_real x)))))
+
+;; "Injective"
+(assert (forall ((x Int) (y Int)) (=> (= (to_real x) (to_real y)) (= x y))))
+
+;; "Monotonic"
+(assert
+ (forall ((x Int) (y Int)) (=> (<= x y) (<= (to_real x) (to_real y)))))
+
+;; "eqb"
+(declare-fun eqb (par (a)
+ (a
+ a) Bool))
+
+;; "eqb"
+(assert (par (a) (forall ((x a) (y a)) (= (= (eqb x y) true) (= x y)))))
+
+;; "neqb"
+(declare-fun neqb (par (a)
+ (a
+ a) Bool))
+
+;; "neqb"
+(assert (par (a)
+ (forall ((x a) (y a)) (= (= (neqb x y) true) (not (= x y))))))
+
+;; "zlt"
+(declare-fun zlt (Int
+ Int) Bool)
+
+;; "zleq"
+(declare-fun zleq (Int
+ Int) Bool)
+
+;; "zlt"
+(assert (forall ((x Int) (y Int)) (= (= (zlt x y) true) (< x y))))
+
+;; "zleq"
+(assert (forall ((x Int) (y Int)) (= (= (zleq x y) true) (<= x y))))
+
+;; "rlt"
+(declare-fun rlt (Real
+ Real) Bool)
+
+;; "rleq"
+(declare-fun rleq (Real
+ Real) Bool)
+
+;; "rlt"
+(assert (forall ((x Real) (y Real)) (= (= (rlt x y) true) (infix_lsdt x y))))
+
+;; "rleq"
+(assert
+ (forall ((x Real) (y Real)) (= (= (rleq x y) true) (infix_lseqdt x y))))
+
+;; "real_of_int"
+(define-fun real_of_int ((x Int)) Real
+ (to_real x))
+
+;; "c_euclidian"
+(assert
+ (forall ((n Int) (d Int))
+ (! (=> (not (= d 0)) (= n (+ (* (div1 n d) d) (mod1 n d)))) :pattern (
+ (div1
+ n
+ d)
+ (mod1 n d)) )))
+
+;; "cmod_remainder"
+(assert
+ (forall ((n Int) (d Int))
+ (! (and
+ (=> (>= n 0) (=> (> d 0) (and (<= 0 (mod1 n d)) (< (mod1 n d) d))))
+ (and
+ (=>
+ (<= n 0)
+ (=> (> d 0) (and (< (- d) (mod1 n d)) (<= (mod1 n d) 0))))
+ (and
+ (=>
+ (>= n 0)
+ (=> (< d 0) (and (<= 0 (mod1 n d)) (< (mod1 n d) (- d)))))
+ (=>
+ (<= n 0)
+ (=> (< d 0) (and (< d (mod1 n d)) (<= (mod1 n d) 0))))))) :pattern (
+ (mod1
+ n
+ d)) )))
+
+;; "cdiv_neutral"
+(assert (forall ((a1 Int)) (! (= (div1 a1 1) a1) :pattern ((div1 a1 1)) )))
+
+;; "cdiv_inv"
+(assert
+ (forall ((a1 Int))
+ (! (=> (not (= a1 0)) (= (div1 a1 a1) 1)) :pattern ((div1 a1 a1)) )))
+
+;; "cdiv_closed_remainder"
+(assert
+ (forall ((a1 Int) (b Int) (n Int))
+ (=>
+ (<= 0 a1)
+ (=>
+ (<= 0 b)
+ (=>
+ (and (<= 0 (- b a1)) (< (- b a1) n))
+ (=> (= (mod1 a1 n) (mod1 b n)) (= a1 b)))))))
+
+(declare-sort infix_mngt 2)
+
+;; "infix @"
+(declare-fun infix_at (par (a1
+ b)
+ ((infix_mngt a1
+ b)
+ a1) b))
+
+;; "get"
+(define-fun get (par (a
+ b1)
+ ((f (infix_mngt a b1)) (x a)) b1
+ (infix_at f x)))
+
+;; "set"
+(declare-fun set (par (a
+ b1)
+ ((infix_mngt a
+ b1)
+ a
+ b1) (infix_mngt a
+ b1)))
+
+;; "set'def"
+(assert (par (a b1)
+ (forall ((f (infix_mngt a b1)) (x a) (v b1) (y a))
+ (= (infix_at (set f x v) y) (ite (= y x) v (infix_at f y))))))
+
+;; "mixfix []"
+(define-fun mixfix_lbrb (par (a
+ b1)
+ ((f (infix_mngt a b1)) (x a)) b1
+ (infix_at f x)))
+
+;; "mixfix [<-]"
+(define-fun mixfix_lblsmnrb (par (a
+ b1)
+ ((f (infix_mngt a b1)) (x a) (v b1)) (infix_mngt a b1)
+ (set f x v)))
+
+(declare-datatypes ((addr 0))
+ (((addrqtmk (base Int)(offset Int)))))
+
+;; "addr_le"
+(declare-fun addr_le (addr
+ addr) Bool)
+
+;; "addr_lt"
+(declare-fun addr_lt (addr
+ addr) Bool)
+
+;; "addr_le_bool"
+(declare-fun addr_le_bool (addr
+ addr) Bool)
+
+;; "addr_lt_bool"
+(declare-fun addr_lt_bool (addr
+ addr) Bool)
+
+;; "addr_le_def"
+(assert
+ (forall ((p addr) (q addr))
+ (! (=>
+ (= (base p) (base q))
+ (= (addr_le p q) (<= (offset p) (offset q)))) :pattern ((addr_le
+ p
+ q)) )))
+
+;; "addr_lt_def"
+(assert
+ (forall ((p addr) (q addr))
+ (! (=> (= (base p) (base q)) (= (addr_lt p q) (< (offset p) (offset q)))) :pattern (
+ (addr_lt
+ p
+ q)) )))
+
+;; "addr_le_bool_def"
+(assert
+ (forall ((p addr) (q addr))
+ (! (= (addr_le p q) (= (addr_le_bool p q) true)) :pattern ((addr_le_bool
+ p
+ q)) )))
+
+;; "addr_lt_bool_def"
+(assert
+ (forall ((p addr) (q addr))
+ (! (= (addr_lt p q) (= (addr_lt_bool p q) true)) :pattern ((addr_lt_bool
+ p
+ q)) )))
+
+;; "null"
+(define-fun null () addr
+ (addrqtmk 0 0))
+
+;; "global"
+(define-fun global ((b2 Int)) addr
+ (addrqtmk b2 0))
+
+;; "shift"
+(define-fun shift ((p addr) (k Int)) addr
+ (addrqtmk (base p) (+ (offset p) k)))
+
+;; "included"
+(define-fun included ((p addr) (a2 Int) (q addr) (b2 Int)) Bool
+ (=>
+ (> a2 0)
+ (and
+ (>= b2 0)
+ (and
+ (= (base p) (base q))
+ (and
+ (<= (offset q) (offset p))
+ (<= (+ (offset p) a2) (+ (offset q) b2)))))))
+
+;; "separated"
+(define-fun separated ((p addr) (a2 Int) (q addr) (b2 Int)) Bool
+ (or
+ (<= a2 0)
+ (or
+ (<= b2 0)
+ (or
+ (not (= (base p) (base q)))
+ (or
+ (<= (+ (offset q) b2) (offset p))
+ (<= (+ (offset p) a2) (offset q)))))))
+
+;; "eqmem"
+(define-fun eqmem (par (a)
+ ((m1 (infix_mngt addr a)) (m2 (infix_mngt addr a)) (p addr) (a2 Int)) Bool
+ (forall ((q addr))
+ (! (=> (included q 1 p a2) (= (mixfix_lbrb m1 q) (mixfix_lbrb m2 q))) :pattern (
+ (mixfix_lbrb
+ m1
+ p)) :pattern ((mixfix_lbrb m2 q)) ))))
+
+;; "havoc"
+(declare-fun havoc (par (a)
+ ((infix_mngt addr
+ a)
+ (infix_mngt addr
+ a)
+ addr
+ Int) (infix_mngt addr
+ a)))
+
+;; "valid_rw"
+(define-fun valid_rw ((m (infix_mngt Int Int)) (p addr) (n Int)) Bool
+ (=>
+ (> n 0)
+ (and
+ (< 0 (base p))
+ (and (<= 0 (offset p)) (<= (+ (offset p) n) (mixfix_lbrb m (base p)))))))
+
+;; "valid_rd"
+(define-fun valid_rd ((m (infix_mngt Int Int)) (p addr) (n Int)) Bool
+ (=>
+ (> n 0)
+ (and
+ (not (= 0 (base p)))
+ (and (<= 0 (offset p)) (<= (+ (offset p) n) (mixfix_lbrb m (base p)))))))
+
+;; "valid_obj"
+(define-fun valid_obj ((m (infix_mngt Int Int)) (p addr) (n Int)) Bool
+ (=>
+ (> n 0)
+ (or
+ (= p null)
+ (and
+ (not (= 0 (base p)))
+ (and
+ (<= 0 (offset p))
+ (<= (+ (offset p) n) (+ 1 (mixfix_lbrb m (base p)))))))))
+
+;; "invalid"
+(define-fun invalid ((m (infix_mngt Int Int)) (p addr) (n Int)) Bool
+ (or
+ (<= n 0)
+ (or
+ (= (base p) 0)
+ (or (<= (mixfix_lbrb m (base p)) (offset p)) (<= (+ (offset p) n) 0)))))
+
+;; "valid_rw_rd"
+(assert
+ (forall ((m (infix_mngt Int Int)))
+ (forall ((p addr))
+ (forall ((n Int)) (=> (valid_rw m p n) (valid_rd m p n))))))
+
+;; "valid_string"
+(assert
+ (forall ((m (infix_mngt Int Int)))
+ (forall ((p addr))
+ (=>
+ (< (base p) 0)
+ (=>
+ (and (<= 0 (offset p)) (< (offset p) (mixfix_lbrb m (base p))))
+ (and (valid_rd m p 1) (not (valid_rw m p 1))))))))
+
+;; "separated_1"
+(assert
+ (forall ((p addr) (q addr))
+ (forall ((a2 Int) (b2 Int) (i Int) (j Int))
+ (! (=>
+ (separated p a2 q b2)
+ (=>
+ (and (<= (offset p) i) (< i (+ (offset p) a2)))
+ (=>
+ (and (<= (offset q) j) (< j (+ (offset q) b2)))
+ (not (= (addrqtmk (base p) i) (addrqtmk (base q) j)))))) :pattern (
+ (separated
+ p
+ a2
+ q
+ b2)
+ (addrqtmk (base p) i)
+ (addrqtmk (base q) j)) ))))
+
+;; "region"
+(declare-fun region (Int) Int)
+
+;; "linked"
+(declare-fun linked ((infix_mngt Int
+ Int)) Bool)
+
+;; "sconst"
+(declare-fun sconst ((infix_mngt addr
+ Int)) Bool)
+
+;; "framed"
+(define-fun framed ((m (infix_mngt addr addr))) Bool
+ (forall ((p addr))
+ (! (=> (<= (region (base p)) 0) (<= (region (base (mixfix_lbrb m p))) 0)) :pattern (
+ (mixfix_lbrb
+ m
+ p)) )))
+
+;; "separated_included"
+(assert
+ (forall ((p addr) (q addr))
+ (forall ((a2 Int) (b2 Int))
+ (! (=>
+ (> a2 0)
+ (=>
+ (> b2 0)
+ (=> (separated p a2 q b2) (not (included p a2 q b2))))) :pattern (
+ (separated
+ p
+ a2
+ q
+ b2)
+ (included p a2 q b2)) ))))
+
+;; "included_trans"
+(assert
+ (forall ((p addr) (q addr) (r addr))
+ (forall ((a2 Int) (b2 Int) (c Int))
+ (! (=>
+ (included p a2 q b2)
+ (=> (included q b2 r c) (included p a2 r c))) :pattern ((included
+ p
+ a2
+ q
+ b2)
+ (included q b2 r c)) ))))
+
+;; "separated_trans"
+(assert
+ (forall ((p addr) (q addr) (r addr))
+ (forall ((a2 Int) (b2 Int) (c Int))
+ (! (=>
+ (included p a2 q b2)
+ (=> (separated q b2 r c) (separated p a2 r c))) :pattern (
+ (included
+ p
+ a2
+ q
+ b2)
+ (separated q b2 r c)) ))))
+
+;; "separated_sym"
+(assert
+ (forall ((p addr) (q addr))
+ (forall ((a2 Int) (b2 Int))
+ (! (= (separated p a2 q b2) (separated q b2 p a2)) :pattern ((separated
+ p
+ a2
+ q
+ b2)) ))))
+
+;; "eqmem_included"
+(assert (par (a)
+ (forall ((m1 (infix_mngt addr a)) (m2 (infix_mngt addr a)))
+ (forall ((p addr) (q addr))
+ (forall ((a2 Int) (b2 Int))
+ (! (=>
+ (included p a2 q b2)
+ (=> (eqmem m1 m2 q b2) (eqmem m1 m2 p a2))) :pattern ((eqmem
+ m1
+ m2
+ p
+ a2)
+ (eqmem m1 m2 q b2)) ))))))
+
+;; "eqmem_sym"
+(assert (par (a)
+ (forall ((m1 (infix_mngt addr a)) (m2 (infix_mngt addr a)))
+ (forall ((p addr))
+ (forall ((a2 Int)) (=> (eqmem m1 m2 p a2) (eqmem m2 m1 p a2)))))))
+
+;; "havoc_access"
+(assert (par (a)
+ (forall ((m0 (infix_mngt addr a)) (m1 (infix_mngt addr a)))
+ (forall ((q addr) (p addr))
+ (forall ((a2 Int))
+ (= (mixfix_lbrb (havoc m0 m1 p a2) q) (ite (separated q 1 p a2)
+ (mixfix_lbrb m1 q)
+ (mixfix_lbrb m0 q))))))))
+
+;; "cinits"
+(declare-fun cinits ((infix_mngt addr
+ Bool)) Bool)
+
+;; "is_init_range"
+(define-fun is_init_range ((m (infix_mngt addr Bool)) (p addr) (l Int)) Bool
+ (forall ((i Int))
+ (=> (and (<= 0 i) (< i l)) (= (mixfix_lbrb m (shift p i)) true))))
+
+;; "set_init"
+(declare-fun set_init ((infix_mngt addr
+ Bool)
+ addr
+ Int) (infix_mngt addr
+ Bool))
+
+;; "set_init_access"
+(assert
+ (forall ((m (infix_mngt addr Bool)))
+ (forall ((q addr) (p addr))
+ (forall ((a2 Int))
+ (= (mixfix_lbrb (set_init m p a2) q) (ite (separated q 1 p a2)
+ (mixfix_lbrb m q)
+ true))))))
+
+;; "monotonic_init"
+(define-fun monotonic_init ((m1 (infix_mngt addr Bool)) (m2 (infix_mngt addr Bool))) Bool
+ (forall ((p addr))
+ (=> (= (mixfix_lbrb m1 p) true) (= (mixfix_lbrb m2 p) true))))
+
+;; "int_of_addr"
+(declare-fun int_of_addr (addr) Int)
+
+;; "addr_of_int"
+(declare-fun addr_of_int (Int) addr)
+
+(declare-sort table 0)
+
+;; "table_of_base"
+(declare-fun table_of_base (Int) table)
+
+;; "table_to_offset"
+(declare-fun table_to_offset (table
+ Int) Int)
+
+;; "table_to_offset_zero"
+(assert (forall ((t table)) (= (table_to_offset t 0) 0)))
+
+;; "table_to_offset_monotonic"
+(assert
+ (forall ((t table))
+ (forall ((o1 Int) (o2 Int))
+ (= (<= o1 o2) (<= (table_to_offset t o1) (table_to_offset t o2))))))
+
+;; "int_of_addr_bijection"
+(assert (forall ((a2 Int)) (= (int_of_addr (addr_of_int a2)) a2)))
+
+;; "addr_of_int_bijection"
+(assert (forall ((p addr)) (= (addr_of_int (int_of_addr p)) p)))
+
+;; "addr_of_null"
+(assert (= (int_of_addr null) 0))
+
+;; "max_uint8"
+(define-fun max_uint8 () Int
+ 256)
+
+;; "max_sint8"
+(define-fun max_sint8 () Int
+ 128)
+
+;; "max_uint16"
+(define-fun max_uint16 () Int
+ 65536)
+
+;; "max_sint16"
+(define-fun max_sint16 () Int
+ 32768)
+
+;; "max_uint32"
+(define-fun max_uint32 () Int
+ 4294967296)
+
+;; "max_sint32"
+(define-fun max_sint32 () Int
+ 2147483648)
+
+;; "max_uint64"
+(define-fun max_uint64 () Int
+ 18446744073709551616)
+
+;; "max_sint64"
+(define-fun max_sint64 () Int
+ 9223372036854775808)
+
+;; "is_bool"
+(define-fun is_bool ((x Int)) Bool
+ (or (= x 0) (= x 1)))
+
+;; "is_uint8"
+(declare-fun is_uint8 (Int) Bool)
+
+;; "is_uint8_def"
+(assert
+ (forall ((x Int))
+ (! (= (is_uint8 x) (and (<= 0 x) (< x max_uint8))) :pattern ((is_uint8 x)) )))
+
+;; "is_sint8"
+(declare-fun is_sint8 (Int) Bool)
+
+;; "is_sint8_def"
+(assert
+ (forall ((x Int))
+ (! (= (is_sint8 x) (and (<= (- max_sint8) x) (< x max_sint8))) :pattern (
+ (is_sint8
+ x)) )))
+
+;; "is_uint16"
+(declare-fun is_uint16 (Int) Bool)
+
+;; "is_uint16_def"
+(assert
+ (forall ((x Int))
+ (! (= (is_uint16 x) (and (<= 0 x) (< x max_uint16))) :pattern ((is_uint16
+ x)) )))
+
+;; "is_sint16"
+(define-fun is_sint16 ((x Int)) Bool
+ (and (<= (- max_sint16) x) (< x max_sint16)))
+
+;; "is_uint32"
+(declare-fun is_uint32 (Int) Bool)
+
+;; "is_uint32_def"
+(assert
+ (forall ((x Int))
+ (! (= (is_uint32 x) (and (<= 0 x) (< x max_uint32))) :pattern ((is_uint32
+ x)) )))
+
+;; "is_sint32"
+(declare-fun is_sint32 (Int) Bool)
+
+;; "is_sint32_def"
+(assert
+ (forall ((x Int))
+ (! (= (is_sint32 x) (and (<= (- max_sint32) x) (< x max_sint32))) :pattern (
+ (is_sint32
+ x)) )))
+
+;; "is_uint64"
+(declare-fun is_uint64 (Int) Bool)
+
+;; "is_uint64_def"
+(assert
+ (forall ((x Int))
+ (! (= (is_uint64 x) (and (<= 0 x) (< x max_uint64))) :pattern ((is_uint64
+ x)) )))
+
+;; "is_sint64"
+(declare-fun is_sint64 (Int) Bool)
+
+;; "is_sint64_def"
+(assert
+ (forall ((x Int))
+ (! (= (is_sint64 x) (and (<= (- max_sint64) x) (< x max_sint64))) :pattern (
+ (is_sint64
+ x)) )))
+
+;; "is_bool0"
+(assert (is_bool 0))
+
+;; "is_bool1"
+(assert (is_bool 1))
+
+;; "to_bool"
+(define-fun to_bool ((x Int)) Int
+ (ite (= x 0) 0 1))
+
+;; "to_uint8"
+(declare-fun to_uint8 (Int) Int)
+
+;; "to_sint8"
+(declare-fun to_sint8 (Int) Int)
+
+;; "to_uint16"
+(declare-fun to_uint16 (Int) Int)
+
+;; "to_sint16"
+(declare-fun to_sint16 (Int) Int)
+
+;; "to_uint32"
+(declare-fun to_uint32 (Int) Int)
+
+;; "to_sint32"
+(declare-fun to_sint32 (Int) Int)
+
+;; "to_uint64"
+(declare-fun to_uint64 (Int) Int)
+
+;; "to_sint64"
+(declare-fun to_sint64 (Int) Int)
+
+;; "two_power_abs"
+(declare-fun two_power_abs (Int) Int)
+
+;; "is_uint"
+(define-fun is_uint ((n Int) (x Int)) Bool
+ (and (<= 0 x) (< x (two_power_abs n))))
+
+;; "is_sint"
+(define-fun is_sint ((n Int) (x Int)) Bool
+ (and (<= (- (two_power_abs n)) x) (< x (two_power_abs n))))
+
+;; "to_uint"
+(declare-fun to_uint (Int
+ Int) Int)
+
+;; "to_sint"
+(declare-fun to_sint (Int
+ Int) Int)
+
+;; "is_to_uint8"
+(assert (forall ((x Int)) (is_uint8 (to_uint8 x))))
+
+;; "is_to_sint8"
+(assert (forall ((x Int)) (is_sint8 (to_sint8 x))))
+
+;; "is_to_uint16"
+(assert (forall ((x Int)) (is_uint16 (to_uint16 x))))
+
+;; "is_to_sint16"
+(assert (forall ((x Int)) (is_sint16 (to_sint16 x))))
+
+;; "is_to_uint32"
+(assert (forall ((x Int)) (is_uint32 (to_uint32 x))))
+
+;; "is_to_sint32"
+(assert (forall ((x Int)) (is_sint32 (to_sint32 x))))
+
+;; "is_to_uint64"
+(assert (forall ((x Int)) (is_uint64 (to_uint64 x))))
+
+;; "is_to_sint64"
+(assert (forall ((x Int)) (is_sint64 (to_sint64 x))))
+
+;; "id_uint8"
+(assert
+ (forall ((x Int))
+ (! (=> (and (<= 0 x) (< x max_uint8)) (= (to_uint8 x) x)) :pattern (
+ (to_uint8
+ x)) )))
+
+;; "id_sint8"
+(assert
+ (forall ((x Int))
+ (! (=> (and (<= (- max_sint8) x) (< x max_sint8)) (= (to_sint8 x) x)) :pattern (
+ (to_sint8
+ x)) )))
+
+;; "id_uint16"
+(assert
+ (forall ((x Int))
+ (! (=> (and (<= 0 x) (< x max_uint16)) (= (to_uint16 x) x)) :pattern (
+ (to_uint16
+ x)) )))
+
+;; "id_sint16"
+(assert
+ (forall ((x Int))
+ (! (=> (and (<= (- max_sint16) x) (< x max_sint16)) (= (to_sint16 x) x)) :pattern (
+ (to_sint16
+ x)) )))
+
+;; "id_uint32"
+(assert
+ (forall ((x Int))
+ (! (=> (and (<= 0 x) (< x max_uint32)) (= (to_uint32 x) x)) :pattern (
+ (to_uint32
+ x)) )))
+
+;; "id_sint32"
+(assert
+ (forall ((x Int))
+ (! (=> (and (<= (- max_sint32) x) (< x max_sint32)) (= (to_sint32 x) x)) :pattern (
+ (to_sint32
+ x)) )))
+
+;; "id_uint64"
+(assert
+ (forall ((x Int))
+ (! (=> (and (<= 0 x) (< x max_uint64)) (= (to_uint64 x) x)) :pattern (
+ (to_uint64
+ x)) )))
+
+;; "id_sint64"
+(assert
+ (forall ((x Int))
+ (! (=> (and (<= (- max_sint64) x) (< x max_sint64)) (= (to_sint64 x) x)) :pattern (
+ (to_sint64
+ x)) )))
+
+;; "proj_int8"
+(assert
+ (forall ((x Int))
+ (! (= (to_sint8 (to_uint8 x)) (to_sint8 x)) :pattern ((to_sint8
+ (to_uint8 x))) )))
+
+;; "proj_int16"
+(assert
+ (forall ((x Int))
+ (! (= (to_sint16 (to_uint16 x)) (to_sint16 x)) :pattern ((to_sint16
+ (to_uint16 x))) )))
+
+;; "proj_int32"
+(assert
+ (forall ((x Int))
+ (! (= (to_sint32 (to_uint32 x)) (to_sint32 x)) :pattern ((to_sint32
+ (to_uint32 x))) )))
+
+;; "proj_int64"
+(assert
+ (forall ((x Int))
+ (! (= (to_sint64 (to_uint64 x)) (to_sint64 x)) :pattern ((to_sint64
+ (to_uint64 x))) )))
+
+;; "shiftfield_F1_S_a"
+(define-fun shiftfield_F1_S_a ((p addr)) addr
+ (shift p 1))
+
+;; "shift_sint32"
+(define-fun shift_sint32 ((p addr) (k Int)) addr
+ (shift p k))
+
+;; "shiftfield_F1_S_i"
+(define-fun shiftfield_F1_S_i ((p addr)) addr
+ (shift p 0))
+
+;; "IsInitArray_sint32"
+(define-fun IsInitArray_sint32 ((p addr) (n Int) (Init (infix_mngt addr Bool))) Bool
+ (forall ((i Int))
+ (=> (<= 0 i) (=> (< i n) (= (get Init (shift_sint32 p i)) true)))))
+
+;; "IsInit_S1_S"
+(define-fun IsInit_S1_S ((p addr) (Init (infix_mngt addr Bool))) Bool
+ (and
+ (IsInitArray_sint32 (shiftfield_F1_S_a p) 10 Init)
+ (= (get Init (shiftfield_F1_S_i p)) true)))
+
+;; "Q_IsInitArray_sint32_range"
+(assert
+ (forall ((p addr) (n Int) (Init (infix_mngt addr Bool)))
+ (= (is_init_range Init p n) (IsInitArray_sint32 p n Init))))
+
+;; "Q_IsInit_S1_S_range"
+(assert
+ (forall ((p addr) (Init (infix_mngt addr Bool)))
+ (= (is_init_range Init p 11) (IsInit_S1_S p Init))))
+
+;; Goal "wp_goal"
+(assert
+ (not
+ (forall ((t (infix_mngt addr Bool)) (t1 (infix_mngt addr Bool)) (i Int) (a2 addr))
+ (let ((a3 (shiftfield_F1_S_a a2)))
+ (let ((a4 (havoc
+ t1
+ (set t (shiftfield_F1_S_i a2) true)
+ (shift_sint32 a3 0)
+ 10)))
+ (=>
+ (<= 0 i)
+ (=>
+ (<= (region (base a2)) 0)
+ (=>
+ (<= 10 i)
+ (=>
+ (<= i 10)
+ (=>
+ (cinits t)
+ (=>
+ (is_sint32 i)
+ (=>
+ (cinits a4)
+ (=>
+ (forall ((i1 Int))
+ (=>
+ (<= 0 i1)
+ (=>
+ (< i1 i)
+ (= (get a4 (shift_sint32 a3 i1)) true))))
+ (IsInit_S1_S a2 a4))))))))))))))
+
+(check-sat)
diff --git a/colibri2/theories/quantifier/subst.ml b/colibri2/theories/quantifier/subst.ml
index 96990e7f243d254013983ad484d697995025afd6..913f47786a48191938b98e1e3e2c421c0b9c3b29 100644
--- a/colibri2/theories/quantifier/subst.ml
+++ b/colibri2/theories/quantifier/subst.ml
@@ -28,6 +28,26 @@ type mode = { context : bool; avoid_new_term : bool }
exception New_term
+let ft choice_group d th =
+ match choice_group with
+ | Some choice_group -> Choice.Group.add_to_group d th choice_group
+ | None -> Choice.Group.make_choosable d th
+
+let fg choice_group d th = ft choice_group d (Ground.thterm th)
+
+let fcq choice_group d th =
+ ft choice_group d (Ground.ClosedQuantifier.thterm th)
+
+let fnt choice_group d th =
+ ft choice_group d (Ground.NotTotallyApplied.thterm th)
+
+(* let fg _ (_ : Ground.t) = () *)
+(* let fcq _ (_ : Ground.ClosedQuantifier.t) = () *)
+(* let fnt _ (_ : Ground.NotTotallyApplied.t) = () *)
+
+let skipped_builtin d builtin =
+ Info.Builtin_skipped_for_trigger.skipped d builtin
+
let of_node mode d n =
if mode.avoid_new_term && not (Egraph.is_registered d n) then raise New_term;
Node.S.singleton n
@@ -39,7 +59,7 @@ let of_node mode d n =
*)
let rec convert_and_iter mode d (subst_old : Ground.Subst.t)
- (subst_new : Ground.Subst.t) subst (t : Expr.Term.t) :
+ (subst_new : Ground.Subst.t) subst choice_group (t : Expr.Term.t) :
Node.S.t * bool (* with freevars *) =
match t.term_descr with
| Var v -> (
@@ -64,7 +84,7 @@ let rec convert_and_iter mode d (subst_old : Ground.Subst.t)
{ term_descr = Cst { builtin = Expr.False; _ }; _ };
] ) ->
(* Why3 generates spurious (if v then true else false) *)
- convert_and_iter mode d subst_old subst_new subst cond
+ convert_and_iter mode d subst_old subst_new subst choice_group cond
| App (({ term_descr = Cst cst; _ } as f), tyargs, args) ->
Debug.dprintf2 debug "ci app cst %a" Expr.Term.pp t;
let with_freevars = ref false in
@@ -72,7 +92,7 @@ let rec convert_and_iter mode d (subst_old : Ground.Subst.t)
IArray.of_list_map
~f:(fun arg ->
let arg', wf =
- convert_and_iter mode d subst_old subst_new subst arg
+ convert_and_iter mode d subst_old subst_new subst choice_group arg
in
Debug.dprintf3 debug "fv %a: %b" Expr.Term.pp arg wf;
with_freevars := !with_freevars || wf;
@@ -84,7 +104,7 @@ let rec convert_and_iter mode d (subst_old : Ground.Subst.t)
(IArray.pp Node.S.pp) args Node.S.pp nodes;
let mode =
if mode.context then
- if Info.Builtin_skipped_for_trigger.skipped d cst.builtin then mode
+ if skipped_builtin d cst.builtin then mode
else { mode with context = false }
else mode
in
@@ -93,7 +113,10 @@ let rec convert_and_iter mode d (subst_old : Ground.Subst.t)
Debug.dprintf2 debug "new term cst: %a" Expr.Term.pp t;
raise New_term);
let args = IArray.map ~f:Node.S.choose args in
- let n = Ground.convert_one_app subst d f tyargs args t.term_ty in
+ let n =
+ Ground.convert_one_app_and_iter d f tyargs args t.term_ty subst
+ (fg choice_group) (fcq choice_group) (fnt choice_group)
+ in
(Node.S.singleton n, !with_freevars))
else (nodes, !with_freevars)
| App (f, tyargs, args) ->
@@ -106,21 +129,29 @@ let rec convert_and_iter mode d (subst_old : Ground.Subst.t)
IArray.of_list_map
~f:(fun arg ->
let arg, wf =
- convert_and_iter mode d subst_old subst_new subst arg
+ convert_and_iter mode d subst_old subst_new subst choice_group arg
in
with_freevars := !with_freevars || wf;
arg)
args
in
let args = IArray.map ~f:Node.S.choose args in
- let n = Ground.convert_one_app subst d f tyargs args t.term_ty in
+ let n =
+ Ground.convert_one_app_and_iter d f tyargs args t.term_ty subst
+ (fg choice_group) (fcq choice_group) (fnt choice_group)
+ in
(Node.S.singleton n, !with_freevars)
| Cst f ->
Debug.dprintf2 debug "ci cst %a" Expr.Term.pp t;
(* even if it could create a new term, it will create it only once (global term) *)
- (Node.S.singleton (Ground.convert_one_cst subst d f), false)
+ ( Node.S.singleton
+ (Ground.convert_one_cst_and_iter d f subst (fg choice_group)
+ (fnt choice_group)),
+ false )
| Expr.Binder (((Exists _ | Forall _ | Lambda _) as b), body) ->
- ( Ground.convert_one_binder subst d b body t.term_ty |> of_node mode d,
+ ( Ground.convert_one_binder_and_iter d b body t.term_ty subst
+ (fcq choice_group) (fnt choice_group)
+ |> of_node mode d,
true )
| Expr.Binder (Let_seq l, body) ->
let subst_old, subst_new, subst =
@@ -129,7 +160,7 @@ let rec convert_and_iter mode d (subst_old : Ground.Subst.t)
let n, fv =
convert_and_iter
{ mode with context = false }
- d subst_old subst_new subst t
+ d subst_old subst_new subst choice_group t
in
let n = Node.S.choose n in
let add (s : Ground.Subst.t) =
@@ -140,7 +171,7 @@ let rec convert_and_iter mode d (subst_old : Ground.Subst.t)
(subst_old, subst_new, subst)
l
in
- convert_and_iter mode d subst_old subst_new subst body
+ convert_and_iter mode d subst_old subst_new subst choice_group body
| Expr.Binder (Let_par l, body) ->
let subst_old, subst_new, subst =
List.fold_left
@@ -148,7 +179,7 @@ let rec convert_and_iter mode d (subst_old : Ground.Subst.t)
let n, fv =
convert_and_iter
{ mode with context = false }
- d subst_old subst_new subst t
+ d subst_old subst_new subst choice_group t
in
let n = Node.S.choose n in
let add (s : Ground.Subst.t) =
@@ -159,13 +190,14 @@ let rec convert_and_iter mode d (subst_old : Ground.Subst.t)
(subst_old, subst_new, subst)
l
in
- convert_and_iter mode d subst_old subst_new subst body
+ convert_and_iter mode d subst_old subst_new subst choice_group body
| Expr.Match (_, _) -> invalid_arg "match from dolmen not implemented"
(* TODO convert to one multitest like
the match of why3 and projection *)
let rec check_context_aux d (subst_old : Ground.Subst.t)
- (subst_new : Ground.Subst.t) (subst : Ground.Subst.t) (t : Expr.Term.t) =
+ (subst_new : Ground.Subst.t) (subst : Ground.Subst.t)
+ (choice_group : Choice.Group.t option) (t : Expr.Term.t) =
match t.term_descr with
| Var _ -> true
| App
@@ -177,15 +209,17 @@ let rec check_context_aux d (subst_old : Ground.Subst.t)
{ term_descr = Cst { builtin = Expr.False; _ }; _ };
] ) ->
(* Why3 generates spurious (if v then true else false) *)
- check_context d subst_old subst_new subst cond
+ check_context d subst_old subst_new subst choice_group cond
| App ({ term_descr = Cst cst; _ }, _, args) ->
- if Info.Builtin_skipped_for_trigger.skipped d cst.builtin then
- List.for_all (check_context d subst_old subst_new subst) args
+ if skipped_builtin d cst.builtin then
+ List.for_all
+ (check_context d subst_old subst_new subst choice_group)
+ args
else
let n, _ =
convert_and_iter
{ context = true; avoid_new_term = true }
- d subst_old subst_new subst t
+ d subst_old subst_new subst choice_group t
in
not (Node.S.is_empty n)
| App _ -> false
@@ -195,7 +229,8 @@ let rec check_context_aux d (subst_old : Ground.Subst.t)
* |> of_node { context = true; avoid_new_term = true } d
* |> Node.S.is_empty |> not *)
| Expr.Binder (((Exists _ | Forall _ | Lambda _) as b), body) ->
- Ground.convert_one_binder subst d b body t.term_ty
+ Ground.convert_one_binder_and_iter d b body t.term_ty subst
+ (fcq choice_group) (fnt choice_group)
|> of_node { context = true; avoid_new_term = true } d
|> Node.S.is_empty |> not
| Expr.Binder (Let_seq l, body) ->
@@ -205,7 +240,7 @@ let rec check_context_aux d (subst_old : Ground.Subst.t)
let n, fv =
convert_and_iter
{ context = false; avoid_new_term = true }
- d subst_old subst_new subst t
+ d subst_old subst_new subst choice_group t
in
let n = Node.S.choose n in
let add (s : Ground.Subst.t) =
@@ -216,7 +251,7 @@ let rec check_context_aux d (subst_old : Ground.Subst.t)
(subst_old, subst_new, subst)
l
in
- check_context d subst_old subst_new subst body
+ check_context d subst_old subst_new subst choice_group body
| Expr.Binder (Let_par l, body) ->
let subst_old, subst_new, subst =
List.fold_left
@@ -224,7 +259,7 @@ let rec check_context_aux d (subst_old : Ground.Subst.t)
let n, fv =
convert_and_iter
{ context = false; avoid_new_term = true }
- d subst_old subst_new subst t
+ d subst_old subst_new subst choice_group t
in
let n = Node.S.choose n in
let add (s : Ground.Subst.t) =
@@ -235,31 +270,31 @@ let rec check_context_aux d (subst_old : Ground.Subst.t)
(subst_old, subst_new, subst)
l
in
- check_context d subst_old subst_new subst body
+ check_context d subst_old subst_new subst choice_group body
| Expr.Match (_, _) -> invalid_arg "match from dolmen not implemented"
(* TODO convert to one multitest like
the match of why3 and projection *)
-and check_context d subst_old subst_new subst t =
- let c = check_context_aux d subst_old subst_new subst t in
+and check_context d subst_old subst_new subst choice_group t =
+ let c = check_context_aux d subst_old subst_new subst choice_group t in
if not c then Debug.dprintf2 debug "check false: %a" Expr.Term.pp t;
c
-let convert ~subst_old ~subst_new d t =
+let convert ~subst_old ~subst_new d choice_group t =
let subst = Ground.Subst.distinct_union subst_old subst_new in
try
let n, _ =
convert_and_iter
{ context = true; avoid_new_term = false }
- d subst_old subst_new subst t
+ d subst_old subst_new subst choice_group t
in
Node.S.choose n
with New_term -> assert false
-let convert_avoid_new_terms ~subst_old ~subst_new d t =
+let convert_avoid_new_terms ~subst_old ~subst_new d choice_group t =
let subst = Ground.Subst.distinct_union subst_old subst_new in
let b =
- try check_context d subst_old subst_new subst t
+ try check_context d subst_old subst_new subst choice_group (* todo *) t
with New_term ->
Debug.dprintf0 debug "check_context";
false
@@ -269,7 +304,7 @@ let convert_avoid_new_terms ~subst_old ~subst_new d t =
let n, _ =
convert_and_iter
{ context = true; avoid_new_term = true }
- d subst_old subst_new subst t
+ d subst_old subst_new subst choice_group t
in
Some (Node.S.choose n)
with New_term -> None
diff --git a/colibri2/theories/quantifier/subst.mli b/colibri2/theories/quantifier/subst.mli
index e9b262c70dd33c5d2057b0408b30b4ccf39e99e5..870e6629aa5d634666ffcddd04af0a09c8c4da03 100644
--- a/colibri2/theories/quantifier/subst.mli
+++ b/colibri2/theories/quantifier/subst.mli
@@ -22,6 +22,7 @@ val convert :
subst_old:Ground.Subst.t ->
subst_new:Ground.Subst.t ->
_ Egraph.t ->
+ Choice.Group.t option ->
Expr.Term.t ->
Node.t
(** Same as {!Ground.convert} but try to reuse terms that are equal and already
@@ -31,6 +32,7 @@ val convert_avoid_new_terms :
subst_old:Ground.Subst.t ->
subst_new:Ground.Subst.t ->
_ Egraph.t ->
+ Choice.Group.t option ->
Expr.Term.t ->
Node.t option
(** Same as {!convert} but doesn't create new terms (except for skipped builtins
diff --git a/colibri2/theories/quantifier/trigger.ml b/colibri2/theories/quantifier/trigger.ml
index 82f77593a271650ef96dd4419a4f11123875a99a..84094540e8b15ad91a4303b41fa725368161c093 100644
--- a/colibri2/theories/quantifier/trigger.ml
+++ b/colibri2/theories/quantifier/trigger.ml
@@ -402,6 +402,11 @@ let no_eager_instantiation =
value & flag
& info [ "no-eager-instantiation" ] ~doc:"Don't do eager instantiation")
+let eager_decision =
+ Options.register ~pp:Fmt.bool "Quant.eager_decision"
+ Cmdliner.Arg.(
+ value & flag & info [ "eager-decision" ] ~doc:"Do decisions with eager")
+
let instantiate' d tri subst =
let show_debug debug =
Debug.dprintf11 debug
@@ -428,7 +433,7 @@ let instantiate' d tri subst =
let no_eager_instantiation = Options.get d no_eager_instantiation in
match level_inst with
| Instantiated -> show_debug debug_full
- | Delayed when no_eager_instantiation -> show_debug debug_full
+ | Delayed -> show_debug debug_full
| NotSeen when no_eager_instantiation -> delayed ()
| _ ->
show_debug debug_instantiation;
@@ -446,12 +451,17 @@ let instantiate' d tri subst =
else delayed ()
else if tri.eager then
let form = Ground.ClosedQuantifier.sem tri.form in
+ let choice_group =
+ if Options.get d eager_decision then None
+ else Some (Choice.Group.create d)
+ in
match
Subst.convert_avoid_new_terms ~subst_old:form.subst ~subst_new:subst d
- form.body
+ choice_group form.body
with
| Some n ->
- SubstTrie.set tri.substs subst Instantiated;
+ if Options.get d eager_decision then
+ SubstTrie.set tri.substs subst Instantiated;
Debug.incr nb_instantiation;
Debug.incr nb_eager_instantiation;
if
@@ -463,6 +473,7 @@ let instantiate' d tri subst =
tri.form Ground.Subst.pp subst Ground.Subst.pp form.subst;
Egraph.register d n;
Egraph.merge d n (Ground.ClosedQuantifier.node tri.form);
+ if not (Options.get d eager_decision) then delayed ();
Debug.dprintf0 debug "[Quant] Done"
| None -> delayed ()
else delayed ()