From d5c49f4fe47fa682c22f35bbb3d7d654d7cdc23f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 12 Oct 2021 18:58:44 +0200
Subject: [PATCH] [Quantifier] Fix useless application criteria
The consequence was missing congruence closure
---
src_colibri2/core/egraph.ml | 4 +-
src_colibri2/core/ground.ml | 10 +-
src_colibri2/tests/solve/all/unsat/dune.inc | 3 +
.../all/unsat/lost_in_search_union.psmt2 | 2 +-
.../solve/all/unsat/ordered_is_ordered.psmt2 | 2 +-
.../all/unsat/union-Union-interqtvc_5.psmt2 | 740 ++++++++++++++++++
src_colibri2/theories/quantifier/info.ml | 2 -
.../theories/quantifier/quantifier.ml | 32 +-
src_common/union.mlw | 8 +-
src_common/union/why3session.xml | 261 +++---
10 files changed, 861 insertions(+), 203 deletions(-)
create mode 100644 src_colibri2/tests/solve/all/unsat/union-Union-interqtvc_5.psmt2
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index 7f32eb133..6b62164f9 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -542,9 +542,9 @@ module Delayed = struct
if Debug.test_flag debug_few then begin
match Only_for_solver.thterm node with
| None ->
- Debug.dprintf2 debug "[Egraph] @[register %a@]" Node.pp node
+ Debug.dprintf2 debug_few "[Egraph] @[register %a@]" Node.pp node
| Some thterm ->
- Debug.dprintf4 debug "[Egraph] @[register %a: %a@]"
+ Debug.dprintf4 debug_few "[Egraph] @[register %a: %a@]"
Node.pp node ThTerm.pp thterm
end;
(* assert ( check_no_dom t node ); *)
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index f64774bdf..0207576f9 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -487,7 +487,10 @@ module Defs = struct
let levels = ThTermH.create Popop_stdlib.DInt.pp "ground_levels"
(** Maximum level of unfolding *)
- let level_max = 10
+ let level_max = 15
+
+ (** Maximum level of delayed decisions *)
+ let level_dec_delayed = 5
(** Maximum level where the terms can be directly decided *)
let level_dec = 0
@@ -545,8 +548,9 @@ module Defs = struct
group)
fundef.body
in
- Demon.Simple.LastEffort.schedule_immediately d (fun d ->
- Choice_group.activate d group);
+ if level_dec < level && level <= level_dec_delayed then
+ Demon.Simple.LastEffort.schedule_immediately d (fun d ->
+ Choice_group.activate d group);
Debug.incr stats_function_call;
Egraph.register d n;
Egraph.merge d cl n)
diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
index 54cb6af43..15fa7cb3c 100644
--- a/src_colibri2/tests/solve/all/unsat/dune.inc
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -23,6 +23,9 @@
--dont-print-result %{dep:ordered_is_ordered.psmt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:ordered_is_ordered.psmt2})))
(rule (alias runtest) (action (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status unsat
+--dont-print-result %{dep:union-Union-interqtvc_5.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-interqtvc_5.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_1.psmt2})))
(rule (alias runtest) (action (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status unsat
diff --git a/src_colibri2/tests/solve/all/unsat/lost_in_search_union.psmt2 b/src_colibri2/tests/solve/all/unsat/lost_in_search_union.psmt2
index 618aeb15c..3d403ebe2 100644
--- a/src_colibri2/tests/solve/all/unsat/lost_in_search_union.psmt2
+++ b/src_colibri2/tests/solve/all/unsat/lost_in_search_union.psmt2
@@ -3,7 +3,7 @@
(set-info :smt-lib-version 2.6)
;;; SMT-LIB2: integer arithmetic
;;; SMT-LIB2: real arithmetic
-(set-option :max-steps-colibri2 41000)
+(set-option :max-steps-colibri2 30000)
(declare-sort t 0)
;; real
diff --git a/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2 b/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2
index d3c911337..16c96a949 100644
--- a/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2
+++ b/src_colibri2/tests/solve/all/unsat/ordered_is_ordered.psmt2
@@ -1,7 +1,7 @@
;; produced by local colibri2.drv ;;
(set-logic ALL)
(set-info :smt-lib-version 2.6)
-(set-option :max-steps-colibri2 14000)
+(set-option :max-steps-colibri2 10000)
(declare-datatypes ((tuple2 2))
((par (a1 a2) ((Tuple2 (Tuple2_proj_1 a1)(Tuple2_proj_2 a2))))))
diff --git a/src_colibri2/tests/solve/all/unsat/union-Union-interqtvc_5.psmt2 b/src_colibri2/tests/solve/all/unsat/union-Union-interqtvc_5.psmt2
new file mode 100644
index 000000000..3f2bc9b89
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/union-Union-interqtvc_5.psmt2
@@ -0,0 +1,740 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+;;; SMT-LIB2: integer arithmetic
+;;; SMT-LIB2: real arithmetic
+(declare-sort string 0)
+
+(declare-datatypes ((tuple0 0))
+ (((Tuple0))))
+
+(declare-datatypes ((option 1))
+ ((par (a) ((None) (Some (Some_proj_1 a))))))
+
+;; is_none
+(define-fun is_none (par (a)
+ ((o (option a))) Bool
+ (ite ((_ is None) o) true false)))
+
+;; is_none'spec
+(assert (par (a)
+ (forall ((o (option a))) (= (is_none o) (= o (as None (option a)))))))
+
+;; 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)))))
+
+;; 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)))))
+
+;; ddivisible_using
+(define-fun ddivisible_using ((a1 Int) (b Int) (c Int)) Bool
+ (= a1 (* c b)))
+
+;; ddivisible
+(define-fun ddivisible ((a1 Int) (b Int)) Bool
+ (exists ((d Int)) (ddivisible_using a1 b d)))
+
+(declare-datatypes ((tuple2 2))
+ ((par (a1 a2) ((Tuple2 (Tuple2_proj_1 a1)(Tuple2_proj_2 a2))))))
+
+;; gcd
+(declare-fun gcd (Int
+ Int) Int)
+
+(declare-datatypes ((tuple3 3))
+ ((par (a3 a4
+ a5) ((Tuple3 (Tuple3_proj_1 a3)(Tuple3_proj_2 a4)(Tuple3_proj_3 a5))))))
+
+;; lcm
+(declare-fun lcm (Int
+ Int) Int)
+
+(declare-sort infix_mngt 2)
+
+;; infix @
+(declare-fun infix_at (par (a6
+ b)
+ ((infix_mngt a6
+ b)
+ a6) b))
+
+(declare-datatypes ((tuple4 4))
+ ((par (a7 a8 a9
+ a10) ((Tuple4
+ (Tuple4_proj_1 a7)(Tuple4_proj_2 a8)(Tuple4_proj_3 a9)(Tuple4_proj_4 a10))))))
+
+;; prime_to_one_another
+(declare-fun prime_to_one_another (Int
+ Int) Bool)
+
+;; prime_to_one_another_refl
+(assert (forall ((a11 Int)) (prime_to_one_another a11 a11)))
+
+;; GCD1
+(assert
+ (forall ((a11 Int) (b1 Int) (c Int))
+ (=> (prime_to_one_another a11 b1) (prime_to_one_another (gcd a11 c) b1))))
+
+;; GCD2
+(assert
+ (forall ((a11 Int) (b1 Int) (c Int))
+ (=> (prime_to_one_another a11 b1) (prime_to_one_another a11 (gcd b1 c)))))
+
+;; GCD3
+(assert
+ (forall ((a11 Int) (b1 Int) (c Int))
+ (=>
+ (prime_to_one_another a11 b1)
+ (=> (prime_to_one_another a11 c) (prime_to_one_another a11 (lcm b1 c))))))
+
+;; GCD4
+(assert
+ (forall ((a11 Int) (b1 Int) (c Int))
+ (=>
+ (prime_to_one_another a11 b1)
+ (=> (prime_to_one_another c b1) (prime_to_one_another (lcm a11 c) b1)))))
+
+;; GCD_comm
+(assert (forall ((a11 Int) (b1 Int)) (= (gcd a11 b1) (gcd b1 a11))))
+
+(declare-sort t 0)
+
+;; num
+(declare-fun num (t) Int)
+
+;; den
+(declare-fun den (t) Int)
+
+;; t'invariant
+(assert
+ (forall ((self t))
+ (! (and (< 0 (den self)) (prime_to_one_another (num self) (den self))) :pattern (
+ (den
+ self)) :pattern ((num self)) )))
+
+;; real
+(define-fun real ((q t)) Real
+ (/ (to_real (num q)) (to_real (den q))))
+
+;; equal
+(define-fun equal ((a11 t) (b1 t)) Bool
+ (= (real a11) (real b1)))
+
+;; equal_is_eq
+(assert (forall ((a11 t) (b1 t)) (=> (equal a11 b1) (= a11 b1))))
+
+;; infix <=
+(define-fun infix_lseq ((a11 t) (b1 t)) Bool
+ (<= (real a11) (real b1)))
+
+;; infix <
+(define-fun infix_ls ((a11 t) (b1 t)) Bool
+ (< (real a11) (real b1)))
+
+;; abs
+(define-fun abs1 ((x Real)) Real
+ (ite (>= x 0.0) x (- x)))
+
+;; Abs_le
+(assert
+ (forall ((x Real) (y Real))
+ (= (<= (abs1 x) y) (and (<= (- y) x) (<= x y)))))
+
+;; Abs_pos
+(assert (forall ((x Real)) (>= (abs1 x) 0.0)))
+
+;; Abs_sum
+(assert
+ (forall ((x Real) (y Real)) (<= (abs1 (+ x y)) (+ (abs1 x) (abs1 y)))))
+
+;; Abs_prod
+(assert
+ (forall ((x Real) (y Real)) (= (abs1 (* x y)) (* (abs1 x) (abs1 y)))))
+
+;; triangular_inequality
+(assert
+ (forall ((x Real) (y Real) (z Real))
+ (<= (abs1 (- x z)) (+ (abs1 (- x y)) (abs1 (- y z))))))
+
+(declare-datatypes ((t1 0))
+ (((Eq) (Lt) (Gt))))
+
+;; infix +
+(declare-fun infix_pl (t
+ t) t)
+
+;; infix +'spec
+(assert
+ (forall ((a11 t) (b1 t))
+ (= (+ (real a11) (real b1)) (real (infix_pl a11 b1)))))
+
+;; infix -
+(declare-fun infix_mn (t
+ t) t)
+
+;; infix -'spec
+(assert
+ (forall ((a11 t) (b1 t))
+ (= (- (real a11) (real b1)) (real (infix_mn a11 b1)))))
+
+;; infix *
+(declare-fun infix_as (t
+ t) t)
+
+;; infix *'spec
+(assert
+ (forall ((a11 t) (b1 t))
+ (= (* (real a11) (real b1)) (real (infix_as a11 b1)))))
+
+;; infix /
+(declare-fun infix_sl (t
+ t) t)
+
+;; infix /'spec
+(assert
+ (forall ((a11 t) (b1 t))
+ (=>
+ (not (= (real b1) 0.0))
+ (= (/ (real a11) (real b1)) (real (infix_sl a11 b1))))))
+
+;; make
+(declare-fun make (Int
+ Int) t)
+
+;; make_def
+(assert
+ (forall ((num1 Int) (den1 Int))
+ (=>
+ (not (= den1 0))
+ (= (real (make num1 den1)) (/ (to_real num1) (to_real den1))))))
+
+;; truncate
+(declare-fun truncate (Real) Int)
+
+;; Truncate_int
+(assert (forall ((i Int)) (= (truncate (to_real i)) i)))
+
+;; Truncate_down_pos
+(assert
+ (forall ((x Real))
+ (=>
+ (>= x 0.0)
+ (and (<= (to_real (truncate x)) x) (< x (to_real (+ (truncate x) 1)))))))
+
+;; Truncate_up_neg
+(assert
+ (forall ((x Real))
+ (=>
+ (<= x 0.0)
+ (and (< (to_real (- (truncate x) 1)) x) (<= x (to_real (truncate x)))))))
+
+;; Real_of_truncate
+(assert
+ (forall ((x Real))
+ (and
+ (<= (- x 1.0) (to_real (truncate x)))
+ (<= (to_real (truncate x)) (+ x 1.0)))))
+
+;; Truncate_monotonic
+(assert
+ (forall ((x Real) (y Real)) (=> (<= x y) (<= (truncate x) (truncate y)))))
+
+;; Truncate_monotonic_int1
+(assert
+ (forall ((x Real) (i Int)) (=> (<= x (to_real i)) (<= (truncate x) i))))
+
+;; Truncate_monotonic_int2
+(assert
+ (forall ((x Real) (i Int)) (=> (<= (to_real i) x) (<= i (truncate x)))))
+
+;; Floor_int
+(assert (forall ((i Int)) (= (to_int (to_real i)) i)))
+
+;; Ceil_int
+(assert (forall ((i Int)) (= (- (to_int (- (to_real i)))) i)))
+
+;; Floor_down
+(assert
+ (forall ((x Real))
+ (and (<= (to_real (to_int x)) x) (< x (to_real (+ (to_int x) 1))))))
+
+;; Ceil_up
+(assert
+ (forall ((x Real))
+ (and
+ (< (to_real (- (- (to_int (- x))) 1)) x)
+ (<= x (to_real (- (to_int (- x))))))))
+
+;; Floor_monotonic
+(assert
+ (forall ((x Real) (y Real)) (=> (<= x y) (<= (to_int x) (to_int y)))))
+
+;; Ceil_monotonic
+(assert
+ (forall ((x Real) (y Real))
+ (=> (<= x y) (<= (- (to_int (- x))) (- (to_int (- y)))))))
+
+(declare-datatypes ((t2 0))
+ (((Strict) (Large))))
+
+(declare-datatypes ((t0 0))
+ (((Singleton (Singleton_proj_1 t)(Singleton_proj_2 t0))
+ (Inter
+ (Inter_proj_1 t)(Inter_proj_2 t2)(Inter_proj_3 t)(Inter_proj_4 t2)(Inter_proj_5 t0))
+ (FiniteInf (FiniteInf_proj_1 t)(FiniteInf_proj_2 t2)) (End))))
+
+(declare-datatypes ((t3 0))
+ (((InfFinite
+ (InfFinite_proj_1 t)(InfFinite_proj_2 t2)(InfFinite_proj_3 t0))
+ (Finite (Finite_proj_1 t0)) (Inf))))
+
+;; length0
+(define-fun-rec length0 ((l t0)) Int
+ (ite ((_ is Singleton) l) (let (
+ (x (Singleton_proj_2 l))) (+ (length0 x) 1))
+ (ite ((_ is Inter) l) (let (
+
+
+
+ (x1 (Inter_proj_5 l))) (+ (length0 x1) 2))
+ (ite ((_ is FiniteInf) l) 1 0))))
+
+;; length0_positive
+(assert (forall ((l t0)) (>= (length0 l) 0)))
+
+;; nth0
+(define-fun-rec nth0 ((i Int) (l t0)) t
+ (ite ((_ is Singleton) l) (let ((x2 (Singleton_proj_1 l))
+ (x3 (Singleton_proj_2 l))) (ite (= i 0)
+ x2
+ (nth0 (- i 1) x3)))
+ (ite ((_ is Inter) l) (let ((x4 (Inter_proj_1 l))
+
+ (x5 (Inter_proj_3 l))
+
+ (x6 (Inter_proj_5 l))) (ite (= i 0)
+ x4
+ (ite (= i 1)
+ x5
+ (nth0 (- i 2) x6))))
+ (ite ((_ is FiniteInf) l) (let ((x7 (FiniteInf_proj_1 l))
+ ) (ite (= i 0) x7 (make 0 1))) (make 0 1)))))
+
+;; nth0_rewritted
+(assert
+ (forall ((i Int) (l t0))
+ (ite ((_ is Singleton) l) (let (
+ (x8 (Singleton_proj_2 l))) (=>
+ (not
+ (= i (- 1)))
+ (= (nth0
+ (+ i 1)
+ l)
+ (nth0
+ i
+ x8))))
+ (ite ((_ is Inter) l) (let (
+
+
+
+ (x9 (Inter_proj_5 l))) (=>
+ (not (= i (- 2)))
+ (=>
+ (not (= i (- 1)))
+ (= (nth0 (+ i 2) l)
+ (nth0
+ i
+ x9))))) (ite ((_ is FiniteInf) l) true true)))))
+
+;; nth0_singleton
+(assert
+ (forall ((i Int) (q t) (l t0))
+ (ite (= i 0)
+ (= (nth0 i (Singleton q l)) q)
+ (= (nth0 i (Singleton q l)) (nth0 (- i 1) l)))))
+
+;; length
+(define-fun length ((l t3)) Int
+ (ite ((_ is InfFinite) l) (let (
+
+ (x10 (InfFinite_proj_3 l))) (+ (length0 x10) 1))
+ (ite ((_ is Finite) l) (let ((x11 (Finite_proj_1 l))) (length0 x11)) 0)))
+
+;; nth
+(define-fun nth ((i Int) (l t3)) t
+ (ite ((_ is InfFinite) l) (let ((x12 (InfFinite_proj_1 l))
+
+ (x13 (InfFinite_proj_3 l))) (ite (= i 0)
+ x12
+ (nth0
+ (- i 1)
+ x13)))
+ (ite ((_ is Finite) l) (let ((x14 (Finite_proj_1 l))) (nth0 i x14))
+ (make
+ 0
+ 1))))
+
+;; lt_bound0
+(define-fun-rec lt_bound0 ((x15 t) (l t0)) Bool
+ (ite ((_ is Singleton) l) (let ((x16 (Singleton_proj_1 l))
+ (x17 (Singleton_proj_2 l))) (and
+ (< (real x15)
+ (real
+ x16))
+ (lt_bound0
+ x15
+ x17)))
+ (ite ((_ is Inter) l) (let ((x18 (Inter_proj_1 l))
+
+ (x19 (Inter_proj_3 l))
+
+ (x20 (Inter_proj_5 l))) (and
+ (< (real x15) (real
+ x18))
+ (and
+ (< (real x15)
+ (real
+ x19))
+ (lt_bound0 x15 x20))))
+ (ite ((_ is FiniteInf) l) (let ((x21 (FiniteInf_proj_1 l))
+ ) (< (real x15) (real x21))) true))))
+
+;; lt_bound
+(define-fun lt_bound ((x22 t) (l t3)) Bool
+ (ite ((_ is InfFinite) l) (let ((x23 (InfFinite_proj_1 l))
+
+ (x24 (InfFinite_proj_3 l))) (or
+ (< (real x22)
+ (real
+ x23))
+ (lt_bound0
+ x22
+ x24)))
+ (ite ((_ is Finite) l) (let ((x25 (Finite_proj_1 l))) (lt_bound0 x22 x25)) true)))
+
+;; ordered0
+(define-fun-rec ordered0 ((l t0)) Bool
+ (ite ((_ is Singleton) l) (let ((x26 (Singleton_proj_1 l))
+ (x27 (Singleton_proj_2 l))) (and
+ (lt_bound0
+ x26
+ x27)
+ (ordered0 x27)))
+ (ite ((_ is Inter) l) (let ((x28 (Inter_proj_1 l))
+
+ (x29 (Inter_proj_3 l))
+
+ (x30 (Inter_proj_5 l))) (and
+ (infix_ls x28 x29)
+ (and
+ (lt_bound0 x29 x30)
+ (ordered0 x30))))
+ (ite ((_ is FiniteInf) l) true true))))
+
+;; ordered
+(define-fun ordered ((l t3)) Bool
+ (ite ((_ is InfFinite) l) (let ((x31 (InfFinite_proj_1 l))
+
+ (x32 (InfFinite_proj_3 l))) (and
+ (lt_bound0
+ x31
+ x32)
+ (ordered0 x32)))
+ (ite ((_ is Finite) l) (let ((x33 (Finite_proj_1 l))) (ordered0 x33)) true)))
+
+(declare-datatypes ((tuple1 1))
+ ((par (a11) ((Tuple1 (Tuple1_proj_1 a11))))))
+
+(declare-sort tqt 0)
+
+;; a
+(declare-fun a12 (tqt) t3)
+
+;; t''invariant
+(assert
+ (forall ((self tqt))
+ (! (and (ordered (a12 self)) (not (= (a12 self) (Finite End)))) :pattern (
+ (a12
+ self)) )))
+
+;; cmp
+(define-fun cmp ((x34 Real) (b1 t2) (y Real)) Bool
+ (ite ((_ is Large) b1) (<= x34 y) (< x34 y)))
+
+;; mem0
+(define-fun-rec mem0 ((x34 Real) (l t0)) Bool
+ (ite ((_ is Singleton) l) (let ((x35 (Singleton_proj_1 l))
+ (x36 (Singleton_proj_2 l))) (or
+ (= x34 (real x35))
+ (mem0 x34 x36)))
+ (ite ((_ is Inter) l) (let ((x37 (Inter_proj_1 l))
+ (x38 (Inter_proj_2 l))
+ (x39 (Inter_proj_3 l))
+ (x40 (Inter_proj_4 l))
+ (x41 (Inter_proj_5 l))) (or
+ (and
+ (cmp
+ (real x37)
+ x38
+ x34)
+ (cmp
+ x34
+ x40
+ (real x39)))
+ (mem0 x34 x41)))
+ (ite ((_ is FiniteInf) l) (let ((x42 (FiniteInf_proj_1 l))
+ (x43 (FiniteInf_proj_2 l))) (cmp
+ (real x42)
+ x43
+ x34)) false))))
+
+;; lt_bound0_is_not_mem0
+(assert
+ (forall ((q t) (r Real) (l t0))
+ (=> (lt_bound0 q l) (=> (<= r (real q)) (not (mem0 r l))))))
+
+;; mem
+(define-fun mem ((x44 Real) (l t3)) Bool
+ (ite ((_ is InfFinite) l) (let ((x45 (InfFinite_proj_1 l))
+ (x46 (InfFinite_proj_2 l))
+ (x47 (InfFinite_proj_3 l))) (or
+ (cmp
+ x44
+ x46
+ (real x45))
+ (mem0 x44 x47)))
+ (ite ((_ is Finite) l) (let ((x48 (Finite_proj_1 l))) (mem0 x44 x48)) true)))
+
+;; u
+(declare-fun u () tqt)
+
+;; v
+(declare-fun v () tqt)
+
+;; u
+(declare-fun u1 () t0)
+
+;; v
+(declare-fun v1 () t0)
+
+;; Requires
+(assert (ordered0 u1))
+
+;; Requires
+(assert (ordered0 v1))
+
+;; x
+(declare-fun x49 () t)
+
+;; x
+(declare-fun x50 () t2)
+
+;; x
+(declare-fun x51 () t)
+
+;; x
+(declare-fun x52 () t2)
+
+;; x
+(declare-fun x53 () t0)
+
+;; H
+(assert (= v1 (Inter x49 x50 x51 x52 x53)))
+
+;; x
+(declare-fun x54 () t)
+
+;; x
+(declare-fun x55 () t2)
+
+;; x
+(declare-fun x56 () t)
+
+;; x
+(declare-fun x57 () t2)
+
+;; x
+(declare-fun x58 () t0)
+
+;; H
+(assert (= u1 (Inter x54 x55 x56 x57 x58)))
+
+;; qu0
+(declare-fun qu0 () t)
+
+;; bu0
+(declare-fun bu0 () t2)
+
+;; qu1
+(declare-fun qu1 () t)
+
+;; bu1
+(declare-fun bu1 () t2)
+
+;; lu
+(declare-fun lu () t0)
+
+;; u
+(declare-fun u2 () t0)
+
+;; qv0
+(declare-fun qv0 () t)
+
+;; bv0
+(declare-fun bv0 () t2)
+
+;; qv1
+(declare-fun qv1 () t)
+
+;; v
+(declare-fun v2 () t0)
+
+;; Requires
+(assert (ordered0 u2))
+
+;; Requires
+(assert (ordered0 v2))
+
+;; Requires
+(assert (= u2 (Inter qu0 bu0 qu1 bu1 lu)))
+
+;; bv1
+(declare-fun bv1 () t2)
+
+;; lv
+(declare-fun lv () t0)
+
+;; Requires
+(assert (= v2 (Inter qv0 bv0 qv1 bv1 lv)))
+
+;; Requires
+(assert
+ (or
+ (and (= v2 v1) (= (+ (length0 lu) 2) (length0 u1)))
+ (and (= v2 u1) (= (+ (length0 lu) 2) (length0 v1)))))
+
+;; Requires
+(assert (infix_ls qu1 qv1))
+
+;; result
+(declare-fun result () t0)
+
+;; Ensures
+(assert (equal qu1 qv0))
+
+;; o
+(declare-fun o () t0)
+
+;; v3
+(declare-fun v3 () t)
+
+;; b3
+(declare-fun b3 () t2)
+
+;; o
+(declare-fun o1 () t0)
+
+;; H
+(assert (= bv0 Large))
+
+;; H
+(assert (= bu1 Large))
+
+;; Ensures
+(assert (ordered0 o))
+
+;; Ensures
+(assert
+ (forall ((x59 Real)) (= (and (mem0 x59 lu) (mem0 x59 v2)) (mem0 x59 o))))
+
+;; Ensures
+(assert (forall ((q t)) (=> (lt_bound0 q lu) (lt_bound0 q o))))
+
+;; Ensures
+(assert (forall ((q t)) (=> (lt_bound0 q v2) (lt_bound0 q o))))
+
+;; H
+(assert (= result (Singleton qu1 o)))
+
+;; Ensures
+(assert (ordered0 result))
+
+;; Ensures
+(assert
+ (forall ((x59 Real))
+ (= (and (mem0 x59 u2) (mem0 x59 v2)) (mem0 x59 result))))
+
+;; q
+(declare-fun q () t)
+
+;; H
+(assert (lt_bound0 q u2))
+
+;; Hinst
+(assert (=> (lt_bound0 q lu) (lt_bound0 q o)))
+
+;; Goal inter'vc
+;; File "/home/bobot/Sources/colibrics/src_common/union.mlw", line 286, characters 8-13
+(assert
+ (not (lt_bound0 q result)))
+
+(check-sat)
diff --git a/src_colibri2/theories/quantifier/info.ml b/src_colibri2/theories/quantifier/info.ml
index 53755873b..a418ece20 100644
--- a/src_colibri2/theories/quantifier/info.ml
+++ b/src_colibri2/theories/quantifier/info.ml
@@ -29,8 +29,6 @@ type t = {
let _ = pp
-(* let pp fmt _ = Fmt.pf fmt "Info" *)
-
(** because it is currently not hidden and too long *)
let pp = Fmt.nop
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index f61622228..ce157326d 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -250,23 +250,18 @@ let quantifier_registered d th =
let application_useless d thg =
let g = Ground.sem thg in
let n = Ground.node thg in
- if IArray.is_empty g.args then false (* No argument no congruence closure *)
- else
- let find_app pos n =
- Opt.get_def Ground.S.empty
- @@
- let open CCOpt in
- let* info = Egraph.get_dom d Info.dom (Egraph.find_def d n) in
- F_Pos.M.find_opt { f = g.app; pos } info.parents
- in
- let check_arg pos arg =
- Ground.S.exists
- (fun arg ->
- Egraph.is_equal d n (Ground.node arg)
- && List.for_all2 Ground.Ty.equal (Ground.sem arg).tyargs g.tyargs)
- (find_app pos arg)
- in
- IArray.for_alli ~f:check_arg g.args
+ let apps =
+ Opt.get_def Ground.S.empty
+ @@
+ let open CCOpt in
+ let* info = Egraph.get_dom d Info.dom (Egraph.find_def d n) in
+ F.M.find_opt g.app info.apps
+ in
+ Ground.S.exists
+ (fun g' ->
+ List.for_all2 Ground.Ty.equal (Ground.sem g').tyargs g.tyargs
+ && IArray.for_all2_exn ~f:(Egraph.is_equal d) (Ground.sem g').args g.args)
+ apps
let add_info_on_ground_terms d thg =
Debug.dprintf2 debug_full "[Quant] add_info_on_ground_terms %a" Ground.pp thg;
@@ -303,7 +298,8 @@ let th_register d =
(* let delay = Events.Delayed_by 10 in *)
Daemon.attach_reg_sem d Ground.ClosedQuantifier.key quantifier_registered;
Ground.register_converter d (fun d g ->
- if not (application_useless d g) then add_info_on_ground_terms d g);
+ if not (application_useless d g) then add_info_on_ground_terms d g
+ else Debug.dprintf2 debug "[Info] %a is redundant" Ground.pp g);
Interp.Register.check_closed_quantifier d (fun d g ->
let n = Ground.ClosedQuantifier.node g in
let unknown =
diff --git a/src_common/union.mlw b/src_common/union.mlw
index fd6ed106c..4c8645ea4 100644
--- a/src_common/union.mlw
+++ b/src_common/union.mlw
@@ -104,18 +104,18 @@ module Union
predicate lt_bound0 (x:Q.t) (l:t0) =
match l with
| Singleton q l ->
- Q.(x < q) /\ lt_bound0 x l
+ x <. q /\ lt_bound0 x l
| Inter q _ q' _ l ->
- Q.(x < q) /\ Q.(x < q') /\ lt_bound0 x l
+ x <. q /\ x <. q' /\ lt_bound0 x l
| FiniteInf q _ ->
- Q.(x < q)
+ x <. q
| End -> true
end
predicate lt_bound (x:Q.t) (l:t) =
match l with
| InfFinite q _ l ->
- Q.(x < q) \/ lt_bound0 x l
+ x <. q \/ lt_bound0 x l
| Finite l ->
lt_bound0 x l
| Inf ->
diff --git a/src_common/union/why3session.xml b/src_common/union/why3session.xml
index fda794dfa..ed77a419a 100644
--- a/src_common/union/why3session.xml
+++ b/src_common/union/why3session.xml
@@ -26,7 +26,7 @@
</transf>
</goal>
<goal name="lt_bound0_is_not_mem0'vc" expl="VC for lt_bound0_is_not_mem0" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="singleton'vc" expl="VC for singleton" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -37,7 +37,7 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="is_singleton'vc.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.40"/></proof>
+ <proof prover="3"><result status="valid" time="3.18"/></proof>
</goal>
</transf>
</goal>
@@ -171,7 +171,6 @@
</transf>
</goal>
<goal name="inter'vc.35" expl="variant decrease" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" proved="true" >
<goal name="inter'vc.35.0" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -188,15 +187,7 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="inter'vc.38" expl="variant decrease" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.38.0" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.38.1" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="inter'vc.39" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -205,15 +196,7 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="inter'vc.41" expl="variant decrease" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.41.0" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.41.1" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="inter'vc.42" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -222,15 +205,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.44" expl="variant decrease" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.44.0" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.44.1" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="inter'vc.45" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -245,15 +220,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.49" expl="variant decrease" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.49.0" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.49.1" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.06"/></proof>
- </goal>
- </transf>
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="inter'vc.50" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
@@ -276,7 +243,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.52.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.66"/></proof>
+ <proof prover="3"><result status="valid" time="0.45"/></proof>
</goal>
</transf>
</goal>
@@ -286,53 +253,22 @@
<goal name="inter'vc.53.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="inter'vc.53.0.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.42"/></proof>
+ <proof prover="3"><result status="valid" time="0.75"/></proof>
</goal>
<goal name="inter'vc.53.0.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.26"/></proof>
+ <proof prover="3"><result status="valid" time="0.60"/></proof>
</goal>
<goal name="inter'vc.53.0.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.37"/></proof>
+ <proof prover="3"><result status="valid" time="1.24"/></proof>
</goal>
<goal name="inter'vc.53.0.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.99"/></proof>
+ <proof prover="3"><result status="valid" time="1.71"/></proof>
</goal>
<goal name="inter'vc.53.0.4" expl="postcondition" proved="true">
- <proof prover="3" timelimit="100"><undone/></proof>
- <transf name="case" proved="true" arg1="(mem0 x lu)">
- <goal name="inter'vc.53.0.4.0" expl="true case (postcondition)" proved="true">
- <proof prover="3"><result status="valid" time="1.23"/></proof>
- </goal>
- <goal name="inter'vc.53.0.4.1" expl="false case (postcondition)" proved="true">
- <transf name="case" proved="true" arg1="(mem0 x lv)">
- <goal name="inter'vc.53.0.4.1.0" expl="false case (true case. postcondition)" proved="true">
- <proof prover="3"><result status="valid" time="3.38"/></proof>
- </goal>
- <goal name="inter'vc.53.0.4.1.1" expl="false case (postcondition)" proved="true">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- <transf name="cut" proved="true" arg1="(cmp v3 b3 x)">
- <goal name="inter'vc.53.0.4.1.1.0" expl="false case (postcondition)" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="inter'vc.53.0.4.1.1.1" expl="asserted formula" proved="true">
- <proof prover="3"><result status="valid" time="3.04"/></proof>
- </goal>
- </transf>
- <transf name="instantiate" proved="true" arg1="Ensures9" arg2="x">
- <goal name="inter'vc.53.0.4.1.1.0" expl="false case (postcondition)" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- </transf>
- <transf name="case" arg1="(cmp v3 b3 x)">
- <goal name="inter'vc.53.0.4.0" expl="true case (postcondition)" proved="true">
- <proof prover="3"><result status="valid" time="1.16"/></proof>
- </goal>
- <goal name="inter'vc.53.0.4.1" expl="false case (postcondition)">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <proof prover="3" timelimit="30"><result status="valid" time="8.24"/></proof>
+ <transf name="instantiate" proved="true" arg1="Ensures9" arg2="x">
+ <goal name="inter'vc.53.0.4.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.12"/></proof>
</goal>
</transf>
</goal>
@@ -341,65 +277,63 @@
<goal name="inter'vc.53.1" expl="postcondition">
<transf name="split_vc" >
<goal name="inter'vc.53.1.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.38"/></proof>
+ <proof prover="3"><result status="valid" time="2.00"/></proof>
</goal>
<goal name="inter'vc.53.1.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.63"/></proof>
+ <proof prover="3"><result status="valid" time="0.25"/></proof>
</goal>
<goal name="inter'vc.53.1.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.70"/></proof>
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="inter'vc.53.1.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.71"/></proof>
+ <proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="inter'vc.53.1.4" expl="postcondition">
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.53.2" expl="postcondition">
- <transf name="split_vc" >
+ <goal name="inter'vc.53.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
<goal name="inter'vc.53.2.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.64"/></proof>
+ <proof prover="3"><result status="valid" time="1.26"/></proof>
</goal>
<goal name="inter'vc.53.2.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.35"/></proof>
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
</goal>
<goal name="inter'vc.53.2.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.42"/></proof>
+ <proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="inter'vc.53.2.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.44"/></proof>
+ <proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
- <goal name="inter'vc.53.2.4" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.53.2.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.52"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
- <goal name="inter'vc.54" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.54.0" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.54" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.54.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.47"/></proof>
</goal>
- <goal name="inter'vc.54.1" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.54.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.26"/></proof>
</goal>
- <goal name="inter'vc.54.2" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.54.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
- <goal name="inter'vc.54.3" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.54.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
- <goal name="inter'vc.54.4" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.54.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.51"/></proof>
</goal>
</transf>
</goal>
<goal name="inter'vc.55" expl="postcondition" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" proved="true" >
<goal name="inter'vc.55.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.32"/></proof>
@@ -414,7 +348,7 @@
<proof prover="3"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="inter'vc.55.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.42"/></proof>
+ <proof prover="3"><result status="valid" time="0.27"/></proof>
</goal>
</transf>
</goal>
@@ -529,7 +463,7 @@
<goal name="inter'vc.72.9" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="inter'vc.72.9.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.44"/></proof>
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
<goal name="inter'vc.72.9.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -539,12 +473,6 @@
<goal name="inter'vc.72.9.2.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.68.9.0.1" expl="postcondition">
- <proof prover="3"><result status="valid" time="0.35"/></proof>
- </goal>
- <goal name="inter'vc.68.9.0.2" expl="postcondition">
- <proof prover="3"><result status="valid" time="0.38"/></proof>
- </goal>
</transf>
</goal>
</transf>
@@ -567,30 +495,29 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.73.0.3" expl="postcondition" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" proved="true" >
<goal name="inter'vc.73.0.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.69"/></proof>
+ <proof prover="3"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="inter'vc.73.0.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.26"/></proof>
+ <proof prover="3"><result status="valid" time="0.44"/></proof>
</goal>
<goal name="inter'vc.73.0.3.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.27"/></proof>
+ <proof prover="3"><result status="valid" time="0.42"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.73.0.4" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.73.0.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.92"/></proof>
</goal>
<goal name="inter'vc.73.0.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="inter'vc.73.0.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
+ <proof prover="3"><result status="valid" time="0.64"/></proof>
</goal>
- <goal name="inter'vc.73.0.7" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.73.0.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.97"/></proof>
</goal>
<goal name="inter'vc.73.0.8" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -611,9 +538,8 @@
</goal>
</transf>
</goal>
- <goal name="inter'vc.73.1" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
+ <goal name="inter'vc.73.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
<goal name="inter'vc.73.1.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
@@ -624,13 +550,13 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.73.1.3" expl="postcondition" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <proof prover="3"><result status="valid" time="1.47"/></proof>
<transf name="split_vc" proved="true" >
<goal name="inter'vc.73.1.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.72"/></proof>
+ <proof prover="3"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="inter'vc.73.1.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.43"/></proof>
+ <proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
<goal name="inter'vc.73.1.3.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
@@ -638,7 +564,7 @@
</transf>
</goal>
<goal name="inter'vc.73.1.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.69"/></proof>
+ <proof prover="3"><result status="valid" time="1.59"/></proof>
</goal>
<goal name="inter'vc.73.1.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -646,17 +572,16 @@
<goal name="inter'vc.73.1.6" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.29"/></proof>
</goal>
- <goal name="inter'vc.73.1.7" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.73.1.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.63"/></proof>
</goal>
<goal name="inter'vc.73.1.8" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.73.1.9" expl="postcondition" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" proved="true" >
<goal name="inter'vc.73.1.9.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="6.33"/></proof>
+ <proof prover="3"><result status="valid" time="3.31"/></proof>
</goal>
<goal name="inter'vc.73.1.9.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.19"/></proof>
@@ -668,9 +593,8 @@
</goal>
</transf>
</goal>
- <goal name="inter'vc.73.2" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
+ <goal name="inter'vc.73.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
<goal name="inter'vc.73.2.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
@@ -681,10 +605,9 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.73.2.3" expl="postcondition" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" proved="true" >
<goal name="inter'vc.73.2.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.75"/></proof>
+ <proof prover="3"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="inter'vc.73.2.3.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
@@ -694,8 +617,8 @@
</goal>
</transf>
</goal>
- <goal name="inter'vc.73.2.4" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.73.2.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.62"/></proof>
</goal>
<goal name="inter'vc.73.2.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -704,16 +627,15 @@
<proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
<goal name="inter'vc.73.2.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.35"/></proof>
+ <proof prover="3"><result status="valid" time="1.63"/></proof>
</goal>
<goal name="inter'vc.73.2.8" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.73.2.9" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.73.2.9.0" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.73.2.9" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.73.2.9.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.78"/></proof>
</goal>
<goal name="inter'vc.73.2.9.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.23"/></proof>
@@ -727,9 +649,8 @@
</goal>
</transf>
</goal>
- <goal name="inter'vc.74" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
+ <goal name="inter'vc.74" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
<goal name="inter'vc.74.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
@@ -739,11 +660,11 @@
<goal name="inter'vc.74.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.74.3" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.74.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.07"/></proof>
</goal>
<goal name="inter'vc.74.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.72"/></proof>
+ <proof prover="3"><result status="valid" time="1.03"/></proof>
</goal>
<goal name="inter'vc.74.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
@@ -752,19 +673,18 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.74.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.08"/></proof>
+ <proof prover="3"><result status="valid" time="0.98"/></proof>
</goal>
<goal name="inter'vc.74.8" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.74.9" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.74.9" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.17"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.75" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
+ <goal name="inter'vc.75" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
<goal name="inter'vc.75.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
@@ -775,7 +695,6 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="inter'vc.75.3" expl="postcondition" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" proved="true" >
<goal name="inter'vc.75.3.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.26"/></proof>
@@ -789,7 +708,6 @@
</transf>
</goal>
<goal name="inter'vc.75.4" expl="postcondition" proved="true">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" proved="true" >
<goal name="inter'vc.75.4.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.17"/></proof>
@@ -812,16 +730,15 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inter'vc.75.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.77"/></proof>
+ <proof prover="3"><result status="valid" time="1.06"/></proof>
</goal>
<goal name="inter'vc.75.8" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.75.9" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.75.9.0" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.75.9" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.75.9.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="inter'vc.75.9.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.19"/></proof>
@@ -1017,8 +934,8 @@
<goal name="inter'vc.120.1.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.1.3" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.120.1.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.09"/></proof>
</goal>
<goal name="inter'vc.120.1.4" expl="postcondition">
<proof prover="3"><result status="timeout" time="5.00"/></proof>
@@ -1046,8 +963,8 @@
<goal name="inter'vc.120.2.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.2.3" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.120.2.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.84"/></proof>
</goal>
<goal name="inter'vc.120.2.4" expl="postcondition">
<proof prover="3"><result status="timeout" time="5.00"/></proof>
@@ -1075,8 +992,8 @@
<goal name="inter'vc.120.3.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.3.3" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.120.3.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.54"/></proof>
</goal>
<goal name="inter'vc.120.3.4" expl="postcondition">
<proof prover="3"><result status="timeout" time="5.00"/></proof>
--
GitLab