From 95a9c70fe37dab57f507172508d82f074768017f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 24 Nov 2021 22:19:44 +0100
Subject: [PATCH] [Simplex] Don't create new terms only add propagations
---
src_colibri2/bin/main.ml | 3 +
src_colibri2/solver/scheduler.ml | 19 +-
src_colibri2/tests/solve/all/unsat/dune.inc | 3 +
.../work_with_fourier_not_simplex2.psmt2 | 634 ++++++++++++++++++
src_colibri2/theories/LRA/LRA.ml | 2 +-
src_colibri2/theories/LRA/LRA_build.ml | 214 +++---
src_colibri2/theories/LRA/dom_interval.ml | 204 +++---
src_colibri2/theories/LRA/dom_interval.mli | 12 +
src_colibri2/theories/LRA/dom_polynome.ml | 25 +-
src_colibri2/theories/LRA/dom_polynome.mli | 2 +-
src_colibri2/theories/LRA/dom_product.ml | 19 +-
src_colibri2/theories/LRA/dom_product.mli | 3 +
src_colibri2/theories/LRA/polynome.ml | 203 +++---
src_colibri2/theories/LRA/simplex.ml | 48 +-
src_colibri2/theories/bool/boolean.ml | 2 +-
src_common/union/why3session.xml | 74 +-
16 files changed, 1083 insertions(+), 384 deletions(-)
create mode 100644 src_colibri2/tests/solve/all/unsat/work_with_fourier_not_simplex2.psmt2
diff --git a/src_colibri2/bin/main.ml b/src_colibri2/bin/main.ml
index 849da6039..b48b60b99 100644
--- a/src_colibri2/bin/main.ml
+++ b/src_colibri2/bin/main.ml
@@ -20,6 +20,8 @@
(* This file is free software, copied from dolmen. See file "LICENSE" for more information *)
+let stat_runtime = Colibri2_core.Debug.register_stats_time "runtime"
+
let () =
let man =
[
@@ -47,6 +49,7 @@ let () =
| `Ok opt -> opt
in
try
+ Colibri2_core.Debug.add_time_during stat_runtime @@ fun () ->
Colibri2_solver.Input.read ~show_steps
~set_true:Colibri2_theories_bool.Boolean.set_true
~handle_exn:Colibri2_solver.Input.handle_exn_with_exit st ~check_status
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index bb681d9dc..08d798506 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -213,6 +213,7 @@ type t = {
(* last before contradiction *)
mutable last_effort_made : PrioLastEffort.Att.t option;
mutable last_decision_made : Prio.Att.t option;
+ position_in_tree : int list Context.Ref.t;
}
(** To treat in the reverse order *)
@@ -262,6 +263,7 @@ let new_solver ~learning ?last_effort_limit
learning_tbl = Array.make 0 0;
last_decision_made = None;
last_effort_made = None;
+ position_in_tree = Context.Ref.create creator [ 0 ];
}
in
let sched_daemon att =
@@ -287,10 +289,14 @@ let new_solver ~learning ?last_effort_limit
Backtrackable.delayed_stop t.solver_state;
t
+let print_position_in_tree fmtt t =
+ Fmt.(list ~sep:comma int fmtt (List.rev (Context.Ref.get t.position_in_tree)))
+
let push kind t =
if Colibri2_popop_lib.Debug.test_flag debug_dotgui then
Backtrackable.draw_graph ~force:true t.solver_state;
- Debug.dprintf2 debug_pushpop "[Scheduler] push from %a" print_level t;
+ Debug.dprintf4 debug_pushpop "[Scheduler] push from %a: %a" print_level t
+ print_position_in_tree t;
let prev =
{
pre_prev_scheduler_state = t.prev_scheduler_state;
@@ -303,16 +309,23 @@ let push kind t =
t.level <- t.level + 1;
t.prev_scheduler_state <- Some prev;
ignore (Context.push t.context);
+ Context.Ref.set t.position_in_tree (0 :: Context.Ref.get t.position_in_tree);
prev
let pop_to t prev =
- Debug.dprintf2 debug_pushpop "[Scheduler] pop from %a" print_level t;
+ Debug.dprintf4 debug_pushpop "[Scheduler] pop from %a : %a" print_level t
+ print_position_in_tree t;
t.prev_scheduler_state <- prev.pre_prev_scheduler_state;
t.level <- prev.pre_level;
Context.pop prev.pre_backtrack_point;
t.last_todo <- prev.last_todo;
+ Context.Ref.set t.position_in_tree
+ (match Context.Ref.get t.position_in_tree with
+ | [] -> [ min_int ]
+ | i :: l -> (i + 1) :: l);
Backtrackable.draw_graph t.solver_state;
- Debug.dprintf2 debug_pushpop "[Scheduler] pop to %a" print_level t
+ Debug.dprintf4 debug_pushpop "[Scheduler] pop to %a: %a" print_level t
+ print_position_in_tree t
(*
let rec apply_learnt llearnt t d =
diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
index 4968e3c0f..b544830cd 100644
--- a/src_colibri2/tests/solve/all/unsat/dune.inc
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -40,3 +40,6 @@
(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:work_with_fourier_not_simplex.psmt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:work_with_fourier_not_simplex.psmt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat
+--dont-print-result %{dep:work_with_fourier_not_simplex2.psmt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:work_with_fourier_not_simplex2.psmt2})))
diff --git a/src_colibri2/tests/solve/all/unsat/work_with_fourier_not_simplex2.psmt2 b/src_colibri2/tests/solve/all/unsat/work_with_fourier_not_simplex2.psmt2
new file mode 100644
index 000000000..33c36448e
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/work_with_fourier_not_simplex2.psmt2
@@ -0,0 +1,634 @@
+;; 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 ((on 0)
+ (off 0))
+ (((OnSin (OnSin_proj_1 t)(OnSin_proj_2 on))
+ (OnEnd (OnEnd_proj_1 t)(OnEnd_proj_2 t2)(OnEnd_proj_3 off)) (OnInf))
+ ((OffSin (OffSin_proj_1 t)(OffSin_proj_2 off))
+ (OffEnd (OffEnd_proj_1 t)(OffEnd_proj_2 t2)(OffEnd_proj_3 on)) (OffInf))))
+
+(declare-datatypes ((t3 0))
+ (((On (On_proj_1 on)) (Off (Off_proj_1 off)))))
+
+(define-funs-rec ((length_on ((l on)) Int)
+
+ (length_off ((l1 off)) Int)
+
+ ) ((ite ((_ is OnSin) l) (let ( (x (OnSin_proj_2 l))) (+ (length_on x) 1))
+ (ite ((_ is OnEnd) l) (let (
+
+ (x1 (OnEnd_proj_3 l))) (+ (length_off x1) 1)) 0))
+ (ite ((_ is OffSin) l1) (let (
+ (x2 (OffSin_proj_2 l1))) (+ (length_off x2) 1))
+ (ite ((_ is OffEnd) l1) (let (
+
+ (x3 (OffEnd_proj_3 l1))) (+ (length_on x3) 1)) 0))))
+
+;; pos_length_on
+(assert (forall ((l on)) (>= (length_on l) 0)))
+
+;; pos_length_off
+(assert (forall ((l off)) (>= (length_off l) 0)))
+
+;; length
+(define-fun length ((l t3)) Int
+ (ite ((_ is On) l) (let ((x4 (On_proj_1 l))) (+ (length_on x4) 1))
+ (let ((x5 (Off_proj_1 l))) (length_off x5))))
+
+(define-funs-rec ((lt_bound_on ((x6 Real) (l on)) Bool)
+
+ (lt_bound_off ((x7 Real) (l1 off)) Bool)
+
+ ) ((ite ((_ is OnSin) l) (let ((x8 (OnSin_proj_1 l))
+ (x9 (OnSin_proj_2 l))) (and
+ (< x6 (real x8))
+ (lt_bound_on x6 x9)))
+ (ite ((_ is OnEnd) l) (let ((x10 (OnEnd_proj_1 l))
+
+ (x11 (OnEnd_proj_3 l))) (and
+ (< x6 (real x10))
+ (lt_bound_off
+ x6
+ x11))) true))
+ (ite ((_ is OffSin) l1) (let ((x12 (OffSin_proj_1 l1))
+ (x13 (OffSin_proj_2 l1))) (and
+ (< x7 (real x12))
+ (lt_bound_off x7 x13)))
+ (ite ((_ is OffEnd) l1) (let ((x14 (OffEnd_proj_1 l1))
+
+ (x15 (OffEnd_proj_3 l1))) (and
+ (< x7 (real x14))
+ (lt_bound_on
+ x7
+ x15))) true))))
+
+;; lt_bound
+(define-fun lt_bound ((x16 t) (l t3)) Bool
+ (ite ((_ is On) l) (let ((x17 (On_proj_1 l))) (lt_bound_on (real x16) x17))
+ (let ((x18 (Off_proj_1 l))) (lt_bound_off (real x16) x18))))
+
+(define-funs-rec ((ordered_on ((l on)) Bool)
+
+ (ordered_off ((l1 off)) Bool)
+
+ ) ((ite ((_ is OnSin) l) (let ((x19 (OnSin_proj_1 l))
+ (x20 (OnSin_proj_2 l))) (and
+ (lt_bound_on
+ (real x19)
+ x20)
+ (ordered_on x20)))
+ (ite ((_ is OnEnd) l) (let ((x21 (OnEnd_proj_1 l))
+
+ (x22 (OnEnd_proj_3 l))) (and
+ (lt_bound_off
+ (real x21)
+ x22)
+ (ordered_off x22))) true))
+ (ite ((_ is OffSin) l1) (let ((x23 (OffSin_proj_1 l1))
+ (x24 (OffSin_proj_2 l1))) (and
+ (lt_bound_off
+ (real x23)
+ x24)
+ (ordered_off x24)))
+ (ite ((_ is OffEnd) l1) (let ((x25 (OffEnd_proj_1 l1))
+
+ (x26 (OffEnd_proj_3 l1))) (and
+ (lt_bound_on
+ (real x25)
+ x26)
+ (ordered_on x26))) true))))
+
+;; ordered
+(define-fun ordered ((l t3)) Bool
+ (ite ((_ is On) l) (let ((x27 (On_proj_1 l))) (ordered_on x27)) (let ((x28 (Off_proj_1 l)))
+ (ordered_off
+ x28))))
+
+(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) (Off OffInf)))) :pattern (
+ (a12
+ self)) )))
+
+;; cmp
+(define-fun cmp ((x29 Real) (b1 t2) (y Real)) Bool
+ (ite ((_ is Large) b1) (<= x29 y) (< x29 y)))
+
+(define-funs-rec ((mem_on ((x29 Real) (l on)) Bool)
+
+ (mem_off ((x30 Real) (l1 off)) Bool)
+
+ ) ((ite ((_ is OnSin) l) (let ((x31 (OnSin_proj_1 l))
+ (x32 (OnSin_proj_2 l))) (or
+ (< x29 (real x31))
+ (and
+ (< (real x31) x29)
+ (mem_on x29 x32))))
+ (ite ((_ is OnEnd) l) (let ((x33 (OnEnd_proj_1 l))
+ (x34 (OnEnd_proj_2 l))
+ (x35 (OnEnd_proj_3 l))) (or
+ (cmp
+ x29
+ x34
+ (real x33))
+ (mem_off x29 x35))) true))
+ (ite ((_ is OffSin) l1) (let ((x36 (OffSin_proj_1 l1))
+ (x37 (OffSin_proj_2 l1))) (or
+ (= x30 (real x36))
+ (mem_off x30 x37)))
+ (ite ((_ is OffEnd) l1) (let ((x38 (OffEnd_proj_1 l1))
+ (x39 (OffEnd_proj_2 l1))
+ (x40 (OffEnd_proj_3 l1))) (and
+ (cmp
+ (real x38)
+ x39
+ x30)
+ (mem_on x30 x40))) false))))
+
+;; mem
+(define-fun mem ((x41 Real) (l t3)) Bool
+ (ite ((_ is On) l) (let ((x42 (On_proj_1 l))) (mem_on x41 x42)) (let ((x43 (Off_proj_1 l)))
+ (mem_off
+ x41
+ x43))))
+
+;; u
+(declare-fun u () off)
+
+;; v
+(declare-fun v () off)
+
+;; Requires
+(assert (ordered_off u))
+
+;; Requires
+(assert (ordered_off v))
+
+;; result
+(declare-fun result () off)
+
+;; o
+(declare-fun o () t1)
+
+;; o
+(declare-fun o1 () off)
+
+;; o
+(declare-fun o2 () off)
+
+;; o
+(declare-fun o3 () off)
+
+;; o
+(declare-fun o4 () t1)
+
+;; o
+(declare-fun o5 () on)
+
+;; o
+(declare-fun o6 () off)
+
+;; o
+(declare-fun o7 () on)
+
+;; o
+(declare-fun o8 () t1)
+
+;; b
+(declare-fun b1 () t2)
+
+;; o
+(declare-fun o9 () on)
+
+;; o
+(declare-fun o10 () on)
+
+;; o
+(declare-fun o11 () on)
+
+;; o
+(declare-fun o12 () t1)
+
+;; o
+(declare-fun o13 () on)
+
+;; o
+(declare-fun o14 () off)
+
+;; o
+(declare-fun o15 () on)
+
+;; x
+(declare-fun x44 () t)
+
+;; x
+(declare-fun x45 () off)
+
+;; H
+(assert (= v (OffSin x44 x45)))
+
+;; x
+(declare-fun x46 () t)
+
+;; x
+(declare-fun x47 () t2)
+
+;; x
+(declare-fun x48 () on)
+
+;; H
+(assert (= u (OffEnd x46 x47 x48)))
+
+;; Ensures
+(assert (forall ((r Real)) (=> (<= r (real x44)) (not (mem_off r x45)))))
+
+;; Ensures
+(assert
+ (let ((subject o4))
+ (ite ((_ is Eq) subject) (equal x44 x46) (ite ((_ is Lt) subject)
+ (infix_ls
+ x44
+ x46) (infix_ls x46 x44)))))
+
+;; H
+(assert (= o4 Eq))
+
+;; H
+(assert (lt_bound_off (real x46) x45))
+
+;; H
+(assert (ordered_on o5))
+
+;; H
+(assert
+ (forall ((x49 Real))
+ (= (or (mem_on x49 x48) (mem_off x49 x45)) (mem_on x49 o5))))
+
+;; H
+(assert
+ (forall ((q Real))
+ (=> (lt_bound_on q x48) (=> (lt_bound_off q x45) (lt_bound_on q o5)))))
+
+;; H
+(assert (= result (OffEnd x46 Large o5)))
+
+;; Ensures
+(assert (ordered_off result))
+
+;; x
+(declare-fun x49 () Real)
+
+;; H
+(assert (or (mem_off x49 u) (mem_off x49 v)))
+
+;; Goal union_off_off'vc
+;; File "/home/bobot/Sources/colibrics/src_common/union.mlw", line 602, characters 11-24
+(assert
+ (not (mem_off x49 result)))
+
+(check-sat)
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index 7aaa3bba2..8bb630719 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -39,4 +39,4 @@ let th_register env =
let () = Init.add_default_theory th_register
-include LRA_build
+include LRA_build.LastEffort
diff --git a/src_colibri2/theories/LRA/LRA_build.ml b/src_colibri2/theories/LRA/LRA_build.ml
index 7f0b7e530..f35108a03 100644
--- a/src_colibri2/theories/LRA/LRA_build.ml
+++ b/src_colibri2/theories/LRA/LRA_build.ml
@@ -22,123 +22,125 @@ open Colibri2_core
(** Helpers to remove *)
-let a = Expr.Term.Var.mk "a" Expr.Ty.real
-
-let b = Expr.Term.Var.mk "b" Expr.Ty.real
-
-let ta = Expr.Term.of_var a
-
-let tb = Expr.Term.of_var b
-
-let c = Expr.Term.Var.mk "c" Expr.Ty.real
-
-let d = Expr.Term.Var.mk "d" Expr.Ty.real
-
-let tc = Expr.Term.of_var c
-
-let td = Expr.Term.of_var d
-
-let tadd = Expr.Term.Real.add ta tb
+module LastEffort = struct
+ let a = Expr.Term.Var.mk "a" Expr.Ty.real
+
+ let b = Expr.Term.Var.mk "b" Expr.Ty.real
+
+ let ta = Expr.Term.of_var a
+
+ let tb = Expr.Term.of_var b
+
+ let c = Expr.Term.Var.mk "c" Expr.Ty.real
+
+ let d = Expr.Term.Var.mk "d" Expr.Ty.real
+
+ let tc = Expr.Term.of_var c
+
+ let td = Expr.Term.of_var d
+
+ let tadd = Expr.Term.Real.add ta tb
-let add d na nb =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
- }
- in
- Ground.convert ~subst d tadd
+ let add d na nb =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
+ }
+ in
+ Ground.convert ~subst d tadd
-let tadd' = Expr.Term.Real.(add (mul tc ta) (mul td tb))
+ let tadd' = Expr.Term.Real.(add (mul tc ta) (mul td tb))
-let add' env qa na qb nb =
- let qa = RealValue.cst qa in
- let qb = RealValue.cst qb in
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, nb); (c, qa); (d, qb) ];
- }
- in
- Ground.convert ~subst env tadd'
+ let add' env qa na qb nb =
+ let qa = RealValue.cst qa in
+ let qb = RealValue.cst qb in
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, nb); (c, qa); (d, qb) ];
+ }
+ in
+ Ground.convert ~subst env tadd'
-let tsub = Expr.Term.Real.sub ta tb
+ let tsub = Expr.Term.Real.sub ta tb
-let sub env na nb =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
- }
- in
- Ground.convert ~subst env tsub
+ let sub env na nb =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
+ }
+ in
+ Ground.convert ~subst env tsub
-let tmult_cst = Expr.Term.Real.(mul tc ta)
+ let tmult_cst = Expr.Term.Real.(mul tc ta)
-let mult_cst env qa na =
- let qa = RealValue.cst qa in
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (c, qa) ];
- }
- in
- Ground.convert ~subst env tmult_cst
+ let mult_cst env qa na =
+ let qa = RealValue.cst qa in
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (c, qa) ];
+ }
+ in
+ Ground.convert ~subst env tmult_cst
-let tmult = Expr.Term.Real.(mul ta tb)
+ let tmult = Expr.Term.Real.(mul ta tb)
-let mult env na nb =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
- }
- in
- Ground.convert ~subst env tmult
+ let mult env na nb =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
+ }
+ in
+ Ground.convert ~subst env tmult
-let tgt_zero = Expr.Term.Real.(gt ta tb)
+ let tgt_zero = Expr.Term.Real.(gt ta tb)
-let gt_zero env na =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, RealValue.zero) ];
- }
- in
- Ground.convert ~subst env tgt_zero
+ let gt_zero env na =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, RealValue.zero) ];
+ }
+ in
+ Ground.convert ~subst env tgt_zero
-let tge_zero = Expr.Term.Real.(ge ta tb)
+ let tge_zero = Expr.Term.Real.(ge ta tb)
-let ge_zero env na =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, RealValue.zero) ];
- }
- in
- Ground.convert ~subst env tge_zero
+ let ge_zero env na =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, RealValue.zero) ];
+ }
+ in
+ Ground.convert ~subst env tge_zero
-let cmp tcmp env na nb =
- let subst =
- {
- Ground.Subst.empty with
- term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
- }
- in
- Ground.convert ~subst env tcmp
-
-let tlt = Expr.Term.Real.lt ta tb
-
-let tle = Expr.Term.Real.le ta tb
-
-let tgt = Expr.Term.Real.gt ta tb
-
-let tge = Expr.Term.Real.ge ta tb
-
-let lt env na nb = cmp tlt env na nb
-
-let le env na nb = cmp tle env na nb
-
-let gt env na nb = cmp tgt env na nb
-
-let ge env na nb = cmp tge env na nb
+ let cmp tcmp env na nb =
+ let subst =
+ {
+ Ground.Subst.empty with
+ term = Expr.Term.Var.M.of_list [ (a, na); (b, nb) ];
+ }
+ in
+ Ground.convert ~subst env tcmp
+
+ let tlt = Expr.Term.Real.lt ta tb
+
+ let tle = Expr.Term.Real.le ta tb
+
+ let tgt = Expr.Term.Real.gt ta tb
+
+ let tge = Expr.Term.Real.ge ta tb
+
+ let lt env na nb = cmp tlt env na nb
+
+ let le env na nb = cmp tle env na nb
+
+ let gt env na nb = cmp tgt env na nb
+
+ let ge env na nb = cmp tge env na nb
+end
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index d64a5a9a0..973dab454 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -126,15 +126,54 @@ let backward = function
| `Ge -> D.ge'
(** {2 Initialization} *)
-let converter d (f : Ground.t) =
- let r = Ground.node f in
- let reg n = Egraph.register d n in
- let open Monad in
- let setb = setv Boolean.dom in
- let getb = getv Boolean.dom in
- let set = updd upd_dom in
- let get = getd dom in
- let cmp test cmp a b =
+module Propagate = struct
+ open Monad
+
+ let setb = setv Boolean.dom
+
+ let getb = getv Boolean.dom
+
+ let set = updd upd_dom
+
+ let get = getd dom
+
+ let sub d ~r ~a ~b =
+ let reg n = Egraph.register d n in
+ reg a;
+ reg b;
+ attach d
+ (set r
+ (let+ va = get a and+ vb = get b in
+ D.minus va vb)
+ && set a
+ (let+ vb = get b and+ vr = get r in
+ D.add vr vb)
+ && set b
+ (let+ va = get a and+ vr = get r in
+ D.minus va vr))
+
+ let cmp d cmp ~r ~a ~b =
+ let reg n = Egraph.register d n in
+ let test c =
+ match c with
+ | D.Uncomparable -> None
+ | Le -> (
+ match cmp with
+ | `Le -> Some true
+ | `Gt -> Some false
+ | `Lt | `Ge -> None)
+ | Lt -> (
+ match cmp with `Le | `Lt -> Some true | `Ge | `Gt -> Some false)
+ | Eq -> (
+ match cmp with `Le | `Ge -> Some true | `Lt | `Gt -> Some false)
+ | Ge -> (
+ match cmp with
+ | `Ge -> Some true
+ | `Lt -> Some false
+ | `Gt | `Le -> None)
+ | Gt -> (
+ match cmp with `Gt | `Ge -> Some true | `Lt | `Le -> Some false)
+ in
reg a;
reg b;
attach d
@@ -147,103 +186,76 @@ let converter d (f : Ground.t) =
&& set a
(let+ vb = get b and+ vr = getb r in
backward (if vr then cmp else neg_cmp cmp) vb))
- in
- match Ground.sem f with
- | { app = { builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
- when Ground.Ty.equal ty Ground.Ty.real ->
- (* Egraph.register_decision d (ChoLRA.choice r) *)
- (* not useful for now *)
- ()
- | { app = { builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
- when Ground.Ty.equal ty Ground.Ty.int ->
- upd_dom d r D.integers
- | { app = { builtin = Expr.Add }; tyargs = []; args; _ } ->
- let a, b = IArray.extract2_exn args in
- reg a;
- reg b;
- attach d
- (set r
- (let+ va = get a and+ vb = get b in
- D.add va vb)
- && set a
- (let+ vb = get b and+ vr = get r in
- D.minus vr vb)
- && set b
- (let+ va = get a and+ vr = get r in
- D.minus vr va))
- | { app = { builtin = Expr.Sub }; tyargs = []; args; _ } ->
- let a, b = IArray.extract2_exn args in
- reg a;
- reg b;
- attach d
- (set r
- (let+ va = get a and+ vb = get b in
- D.minus va vb)
- && set a
- (let+ vb = get b and+ vr = get r in
- D.add vr vb)
- && set b
- (let+ va = get a and+ vr = get r in
- D.minus va vr))
- | { app = { builtin = Expr.Minus }; tyargs = []; args; _ } ->
- let a = IArray.extract1_exn args in
- reg a;
- attach d
- (set r
- (let+ va = get a in
- D.mult_cst Q.minus_one va)
- && set a
- (let+ vr = get r in
- D.mult_cst Q.minus_one vr))
- | { app = { builtin = Expr.Lt }; tyargs = []; args; _ } ->
- let a, b = IArray.extract2_exn args in
- cmp
- (function
- | Uncomparable | Le -> None
- | Lt -> Some true
- | Eq | Ge | Gt -> Some false)
- `Lt a b
- | { app = { builtin = Expr.Leq }; tyargs = []; args; _ } ->
- let a, b = IArray.extract2_exn args in
- cmp
- (function
- | Uncomparable | Ge -> None
- | Eq | Lt | Le -> Some true
- | Gt -> Some false)
- `Le a b
- | { app = { builtin = Expr.Geq }; tyargs = []; args; _ } ->
- let a, b = IArray.extract2_exn args in
- cmp
- (function
- | Uncomparable | Le -> None
- | Lt -> Some false
- | Eq | Ge | Gt -> Some true)
- `Ge a b
- | { app = { builtin = Expr.Gt }; tyargs = []; args; _ } ->
- let a, b = IArray.extract2_exn args in
- cmp
- (function
- | Uncomparable | Ge -> None
- | Eq | Lt | Le -> Some false
- | Gt -> Some true)
- `Gt a b
- | { app = { builtin = Expr.Equal }; tyargs = _; args; _ } ->
- if IArray.length args = 2 then (
+
+ let converter d (f : Ground.t) =
+ let r = Ground.node f in
+ let reg n = Egraph.register d n in
+ match Ground.sem f with
+ | { app = { builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
+ when Ground.Ty.equal ty Ground.Ty.real ->
+ (* Egraph.register_decision d (ChoLRA.choice r) *)
+ (* not useful for now *)
+ ()
+ | { app = { builtin = Expr.Base; _ }; tyargs = _; args = _; ty }
+ when Ground.Ty.equal ty Ground.Ty.int ->
+ upd_dom d r D.integers
+ | { app = { builtin = Expr.Add }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
reg a;
reg b;
attach d
- (setb r
- (let* va = get a and+ vb = get b in
- if D.is_distinct va vb then Some false else None)))
- | _ -> ()
+ (set r
+ (let+ va = get a and+ vb = get b in
+ D.add va vb)
+ && set a
+ (let+ vb = get b and+ vr = get r in
+ D.minus vr vb)
+ && set b
+ (let+ va = get a and+ vr = get r in
+ D.minus vr va))
+ | { app = { builtin = Expr.Sub }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ sub d ~r ~a ~b
+ | { app = { builtin = Expr.Minus }; tyargs = []; args; _ } ->
+ let a = IArray.extract1_exn args in
+ reg a;
+ attach d
+ (set r
+ (let+ va = get a in
+ D.mult_cst Q.minus_one va)
+ && set a
+ (let+ vr = get r in
+ D.mult_cst Q.minus_one vr))
+ | { app = { builtin = Expr.Lt }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp d `Lt ~r ~a ~b
+ | { app = { builtin = Expr.Leq }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp d `Le ~r ~a ~b
+ | { app = { builtin = Expr.Geq }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp d `Ge ~r ~a ~b
+ | { app = { builtin = Expr.Gt }; tyargs = []; args; _ } ->
+ let a, b = IArray.extract2_exn args in
+ cmp d `Gt ~r ~a ~b
+ | { app = { builtin = Expr.Equal }; tyargs = _; args; _ } ->
+ if IArray.length args = 2 then (
+ let a, b = IArray.extract2_exn args in
+ reg a;
+ reg b;
+ attach d
+ (setb r
+ (let* va = get a and+ vb = get b in
+ if D.is_distinct va vb then Some false else None)))
+ | _ -> ()
+end
let init env =
Daemon.attach_reg_value env RealValue.key (fun d value ->
let v = RealValue.value value in
let s = D.singleton v in
upd_dom d (RealValue.node value) s);
- Ground.register_converter env converter;
+ Ground.register_converter env Propagate.converter;
Interp.Register.node env (fun _ d n ->
match Egraph.get_dom d dom n with
| None -> None
diff --git a/src_colibri2/theories/LRA/dom_interval.mli b/src_colibri2/theories/LRA/dom_interval.mli
index b5391c834..108d1a063 100644
--- a/src_colibri2/theories/LRA/dom_interval.mli
+++ b/src_colibri2/theories/LRA/dom_interval.mli
@@ -49,3 +49,15 @@ val zero_is : _ Egraph.t -> Node.t -> D.is_comparable
val assume_positive : Egraph.wt -> Node.t -> unit
val assume_negative : Egraph.wt -> Node.t -> unit
+
+module Propagate : sig
+ val sub : 'a Egraph.t -> r:Node.t -> a:Node.t -> b:Node.t -> unit
+
+ val cmp :
+ 'a Egraph.t ->
+ [ `Ge | `Gt | `Le | `Lt ] ->
+ r:Node.t ->
+ a:Node.t ->
+ b:Node.t ->
+ unit
+end
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index f1e7db95b..db5b7dfdf 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -53,21 +53,8 @@ module Table = struct
Egraph.merge d n n';
s)
h d new_
-
- let new_ d p =
- match H.find_opt h d p with
- | Some n -> n
- | None ->
- let n = ThE.node (ThE.index p) in
- H.set h d p n;
- n
end
-let node_of_polynome d p =
- match Polynome.is_cst p with
- | None -> Table.new_ d p
- | Some q -> RealValue.node (RealValue.index q)
-
include Pivot.Total (struct
include Polynome
@@ -111,6 +98,18 @@ include Pivot.Total (struct
Subst (x, Polynome.mult_cst (Q.div Q.one (Q.neg q)) p')
end)
+let node_of_polynome d p =
+ match Polynome.is_cst p with
+ | None -> (
+ match Table.H.find_opt Table.h d p with
+ | Some n -> n
+ | None ->
+ let n = ThE.node (ThE.index p) in
+ Egraph.register d n;
+ assume_equality d n p;
+ n)
+ | Some q -> RealValue.node (RealValue.index q)
+
(** {2 Initialization} *)
let converter d (f : Ground.t) =
let res = Ground.node f in
diff --git a/src_colibri2/theories/LRA/dom_polynome.mli b/src_colibri2/theories/LRA/dom_polynome.mli
index f9051653d..b63f44e9c 100644
--- a/src_colibri2/theories/LRA/dom_polynome.mli
+++ b/src_colibri2/theories/LRA/dom_polynome.mli
@@ -30,6 +30,6 @@ val events_repr_change :
val init : Egraph.wt -> unit
-val node_of_polynome : _ Egraph.t -> Polynome.t -> Node.t
+val node_of_polynome : Egraph.wt -> Polynome.t -> Node.t
val normalize : _ Egraph.t -> Polynome.t -> Polynome.t
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index c726fd0dd..0d6af37fa 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -288,6 +288,13 @@ let factorize res a coef b d _ =
| _ -> ()
(** {2 Initialization} *)
+let propagate_a_cb d ~res ~a ~c ~b =
+ List.iter
+ (fun node ->
+ SolveAbs.attach_repr_change d ~node (factorize res a c b);
+ SolveSign.attach_repr_change d ~node (factorize res a c b))
+ [ a; b ]
+
let converter d (f : Ground.t) =
let res = Ground.node f in
let reg n = Egraph.register d n in
@@ -319,20 +326,12 @@ let converter d (f : Ground.t) =
let a, b = IArray.extract2_exn args in
reg a;
reg b;
- List.iter
- (fun node ->
- SolveAbs.attach_repr_change d ~node (factorize res a Q.one b);
- SolveSign.attach_repr_change d ~node (factorize res a Q.one b))
- [ a; b ]
+ propagate_a_cb d ~res ~a ~b ~c:Q.one
| { app = { builtin = Expr.Sub }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
reg a;
reg b;
- List.iter
- (fun node ->
- SolveAbs.attach_repr_change d ~node (factorize res a Q.minus_one b);
- SolveSign.attach_repr_change d ~node (factorize res a Q.minus_one b))
- [ a; b ]
+ propagate_a_cb d ~res ~a ~b ~c:Q.minus_one
| {
app = { builtin = Expr.Abs | RealValue.Builtin.Abs_real };
tyargs = [];
diff --git a/src_colibri2/theories/LRA/dom_product.mli b/src_colibri2/theories/LRA/dom_product.mli
index df0dd22e7..ae452721d 100644
--- a/src_colibri2/theories/LRA/dom_product.mli
+++ b/src_colibri2/theories/LRA/dom_product.mli
@@ -31,3 +31,6 @@ module SolveSign : sig
end
val init : Egraph.wt -> unit
+
+val propagate_a_cb :
+ _ Egraph.t -> res:Node.t -> a:Node.t -> c:Q.t -> b:Node.t -> unit
diff --git a/src_colibri2/theories/LRA/polynome.ml b/src_colibri2/theories/LRA/polynome.ml
index d80e81848..d9aca9efd 100644
--- a/src_colibri2/theories/LRA/polynome.ml
+++ b/src_colibri2/theories/LRA/polynome.ml
@@ -23,94 +23,90 @@ open Colibri2_core
let print_poly fmt poly =
let print_not_1 first fmt q =
- if not first && Q.compare q Q.zero >= 0
- then Format.pp_print_string fmt "+";
- if Q.equal q Q.zero then Format.pp_print_string fmt "!0!"
+ if (not first) && Q.compare q Q.zero >= 0 then
+ Format.pp_print_string fmt "+";
+ if Q.equal q Q.zero then Format.pp_print_string fmt "!0!"
else if Q.equal Q.minus_one q then Format.pp_print_string fmt "-"
else if not (Q.equal Q.one q) then Q.pp fmt q
in
- let print_mono k v (fmt,first) =
- Format.fprintf fmt "@[%a%a@]@," (print_not_1 first) v Node.pp k;
- (fmt,false)
- in
- let _,first = Node.M.fold print_mono poly (fmt,true) in
+ let print_mono k v (fmt, first) =
+ Format.fprintf fmt "@[%a%a@]@," (print_not_1 first) v Node.pp k;
+ (fmt, false)
+ in
+ let _, first = Node.M.fold print_mono poly (fmt, true) in
first
module T = struct
- type t = { cst : Q.t; poly : Q.t Node.M.t}
- [@@deriving eq,ord,hash]
+ type t = { cst : Q.t; poly : Q.t Node.M.t } [@@deriving eq, ord, hash]
let pp fmt v =
- let print_not_0 first fmt q =
- if first
- then Q.pp fmt q
- else
- if not (Q.equal Q.zero q) then begin
- if Q.compare q Q.zero > 0 then Format.pp_print_string fmt "+";
- Q.pp fmt q
- end
- in
+ let print_not_0 first fmt q =
+ if first then Q.pp fmt q
+ else if not (Q.equal Q.zero q) then (
+ if Q.compare q Q.zero > 0 then Format.pp_print_string fmt "+";
+ Q.pp fmt q)
+ in
Format.fprintf fmt "@[";
let first = print_poly fmt v.poly in
Format.fprintf fmt "%a@]" (print_not_0 first) v.cst
-
end
include T
-include Popop_stdlib.MkDatatype(T)
+include Popop_stdlib.MkDatatype (T)
(** different invariant *)
-let invariant p =
- Node.M.for_all (fun _ q -> not (Q.equal q Q.zero)) p.poly
+let invariant p = Node.M.for_all (fun _ q -> not (Q.equal q Q.zero)) p.poly
(** constructor *)
-let cst q = {cst = q; poly = Node.M.empty}
+let cst q = { cst = q; poly = Node.M.empty }
+
let zero = cst Q.zero
+
let is_cst p = if Node.M.is_empty p.poly then Some p.cst else None
+
let is_zero p = Q.equal p.cst Q.zero && Node.M.is_empty p.poly
type extract = Zero | Cst of Q.t | Var of Q.t * Node.t * t
+
let extract p =
if Node.M.is_empty p.poly then
- if Q.equal p.cst Q.zero then Zero
- else Cst p.cst
+ if Q.equal p.cst Q.zero then Zero else Cst p.cst
else
- let x,q = Shuffle.chooseb Node.M.choose Node.M.choose_rnd p.poly in
- let p' = {p with poly = Node.M.remove x p.poly} in
- Var(q,x,p')
+ (* max binding is more interesting than choose (min binding) because it
+ force results to be choosen as pivot*)
+ let x, q = Node.M.max_binding p.poly in
+ let p' = { p with poly = Node.M.remove x p.poly } in
+ Var (q, x, p')
type kind = ZERO | CST | VAR
-let classify p =
- if Node.M.is_empty p.poly then
- if Q.equal p.cst Q.zero then ZERO
- else CST
- else
- VAR
+let classify p =
+ if Node.M.is_empty p.poly then if Q.equal p.cst Q.zero then ZERO else CST
+ else VAR
let monome c x =
if Q.equal Q.zero c then cst Q.zero
- else {cst = Q.zero; poly = Node.M.singleton x c}
+ else { cst = Q.zero; poly = Node.M.singleton x c }
-let is_one_node p = (** cst = 0 and one empty monome *)
+let is_one_node p =
+ (* cst = 0 and one empty monome *)
if Q.equal Q.zero p.cst && Node.M.is_num_elt 1 p.poly then
- let node,k = Node.M.choose p.poly in
- if Q.equal Q.one k then Some node
- else None
+ let node, k = Node.M.choose p.poly in
+ if Q.equal Q.one k then Some node else None
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 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
else
- let poly_mult c m = Node.M.map (fun c1 -> Q.mul c c1) m in
- if Q.equal Q.zero c then cst Q.zero
- else {cst = Q.mul c p1.cst; poly = poly_mult c p1.poly}
-
+ let poly_mult c m = Node.M.map (fun c1 -> Q.mul c c1) m in
+ if Q.equal Q.zero c then cst Q.zero
+ else { cst = Q.mul c p1.cst; poly = poly_mult c p1.poly }
let none_zero c = if Q.equal Q.zero c then None else Some c
@@ -120,100 +116,111 @@ let add p1 p2 =
let poly_add m1 m2 =
Node.M.union (fun _ c1 c2 -> none_zero (Q.add c1 c2)) m1 m2
in
- {cst = Q.add p1.cst p2.cst; poly = poly_add p1.poly p2.poly}
+ { cst = Q.add p1.cst p2.cst; poly = poly_add p1.poly p2.poly }
let sub p1 p2 =
let poly_sub m1 m2 =
- Node.M.union_merge (fun _ c1 c2 ->
- match c1 with
- | None -> Some (Q.neg c2)
- | Some c1 -> none_zero (Q.sub c1 c2))
- m1 m2 in
- {cst = Q.sub p1.cst p2.cst; poly = poly_sub p1.poly p2.poly}
+ Node.M.union_merge
+ (fun _ c1 c2 ->
+ match c1 with
+ | None -> Some (Q.neg c2)
+ | Some c1 -> none_zero (Q.sub c1 c2))
+ m1 m2
+ in
+ { cst = Q.sub p1.cst p2.cst; poly = poly_sub p1.poly p2.poly }
let x_p_cy p1 c p2 =
assert (not (Q.equal c Q.zero));
let f a b = Q.add a (Q.mul c b) in
let poly m1 m2 =
- Node.M.union_merge (fun _ c1 c2 ->
- match c1 with
- | None -> Some (Q.mul c c2)
- | Some c1 -> none_zero (f c1 c2))
- m1 m2 in
- {cst = f p1.cst p2.cst; poly = poly p1.poly p2.poly}
-
+ Node.M.union_merge
+ (fun _ c1 c2 ->
+ match c1 with
+ | None -> Some (Q.mul c c2)
+ | Some c1 -> none_zero (f c1 c2))
+ m1 m2
+ in
+ { cst = f p1.cst p2.cst; poly = poly p1.poly p2.poly }
let cx_p_cy c1 p1 c2 p2 =
let c1_iszero = Q.equal c1 Q.zero in
let c2_iszero = Q.equal c2 Q.zero in
if c1_iszero && c2_iszero then zero
- else if c1_iszero
- then p2
- else if c2_iszero
- then p1
+ else if c1_iszero then p2
+ else if c2_iszero then p1
else
let f e1 e2 = Q.add (Q.mul c1 e1) (Q.mul c2 e2) in
let poly m1 m2 =
- Node.M.merge (fun _ e1 e2 ->
- match e1, e2 with
+ Node.M.merge
+ (fun _ e1 e2 ->
+ match (e1, e2) with
| None, None -> assert false
| None, Some e2 -> Some (Q.mul c2 e2)
| Some e1, None -> Some (Q.mul c1 e1)
- | Some e1, Some e2 ->
- none_zero (f e1 e2))
- m1 m2 in
- {cst = f p1.cst p2.cst; poly = poly p1.poly p2.poly}
+ | Some e1, Some e2 -> none_zero (f e1 e2))
+ m1 m2
+ in
+ { cst = f p1.cst p2.cst; poly = poly p1.poly p2.poly }
let subst_node p x y =
- let poly,qo = Node.M.find_remove x p.poly in
+ let poly, qo = Node.M.find_remove x p.poly in
match qo with
- | None -> p, Q.zero
+ | None -> (p, Q.zero)
| Some q ->
- let poly = Node.M.change (function
- | None -> qo
- | Some q' -> none_zero (Q.add q q')
- ) y poly in
- {p with poly}, q
+ let poly =
+ Node.M.change
+ (function None -> qo | Some q' -> none_zero (Q.add q q'))
+ y poly
+ in
+ ({ p with poly }, q)
let subst p x s =
- let poly,q = Node.M.find_remove x p.poly in
- match q with
- | None -> p, Q.zero
- | Some q -> x_p_cy {p with poly} q s, q
+ let poly, q = Node.M.find_remove x p.poly in
+ match q with None -> (p, Q.zero) | Some q -> (x_p_cy { p with poly } q s, q)
let fold f acc p = Node.M.fold_left f acc p.poly
+
let iter f p = Node.M.iter f p.poly
let of_list cst l =
- let fold acc (node,q) = Node.M.change (function
- | None -> Some q
- | Some q' -> none_zero (Q.add q q')) node acc in
- {cst;poly= List.fold_left fold Node.M.empty l}
+ let fold acc (node, q) =
+ Node.M.change
+ (function None -> Some q | Some q' -> none_zero (Q.add q q'))
+ node acc
+ in
+ { cst; poly = List.fold_left fold Node.M.empty l }
let of_map cst poly =
- assert ( Node.M.for_all (fun _ q -> not (Q.equal Q.zero q)) poly );
- {cst;poly}
+ assert (Node.M.for_all (fun _ q -> not (Q.equal Q.zero q)) poly);
+ { cst; poly }
-module ClM = Extmap.Make(Node)
+module ClM = Extmap.Make (Node)
type 'a tree = 'a ClM.view =
| Empty
| Node of 'a tree * Node.t * 'a * 'a tree * int
let get_tree p =
- (ClM.view
- (Node.M.fold_left (fun acc node q -> ClM.add node q acc) ClM.empty p.poly))
-, p.cst
+ ( ClM.view
+ (Node.M.fold_left (fun acc node q -> ClM.add node q acc) ClM.empty p.poly),
+ p.cst )
let normalize p =
- if Node.M.is_empty p.poly then cst (Q.of_int (Q.sign p.cst)) else
- let init = if Q.equal Q.zero p.cst then snd (Node.M.choose p.poly) else p.cst in
- let (num,den) = Node.M.fold_left (fun (num,den) _ q -> Z.gcd num q.Q.num, Z.gcd den q.Q.den)
- (init.Q.num,init.Q.den) p.poly in
+ if Node.M.is_empty p.poly then cst (Q.of_int (Q.sign p.cst))
+ else
+ let init =
+ if Q.equal Q.zero p.cst then snd (Node.M.choose p.poly) else p.cst
+ in
+ let num, den =
+ Node.M.fold_left
+ (fun (num, den) _ q -> (Z.gcd num q.Q.num, Z.gcd den q.Q.den))
+ (init.Q.num, init.Q.den) p.poly
+ in
if Z.equal Z.one num && Z.equal Z.one den then p
else
let conv q = Q.make (Z.divexact q.Q.num num) (Z.divexact q.Q.den den) in
- { poly = Node.M.map conv p.poly;
- cst = conv p.cst }
+ { poly = Node.M.map conv p.poly; cst = conv p.cst }
-let print_poly fmt poly = let _ = print_poly fmt poly in ()
+let print_poly fmt poly =
+ let _ = print_poly fmt poly in
+ ()
diff --git a/src_colibri2/theories/LRA/simplex.ml b/src_colibri2/theories/LRA/simplex.ml
index d1a3a6ce7..cb6a8ee6b 100644
--- a/src_colibri2/theories/LRA/simplex.ml
+++ b/src_colibri2/theories/LRA/simplex.ml
@@ -506,12 +506,14 @@ let dom_inter = function
| _ -> assert false
let build = function
- | Expr.Lt -> LRA_build.lt
- | Expr.Leq -> LRA_build.le
- | Expr.Gt -> LRA_build.gt
- | Expr.Geq -> LRA_build.ge
+ | Expr.Lt -> `Lt
+ | Expr.Leq -> `Le
+ | Expr.Gt -> `Gt
+ | Expr.Geq -> `Ge
| _ -> assert false
+let seen = Node.HC.create Fmt.nop "Simplex.seen"
+
(** {2 Initialization} *)
let converter d (f : Ground.t) =
match Ground.sem f with
@@ -520,31 +522,41 @@ let converter d (f : Ground.t) =
tyargs = [];
args;
} ->
- let n, builtin =
+ let n =
let a, b = IArray.extract2_exn args in
(* Special case needed for avoiding infinite loop *)
- if Node.equal a RealValue.zero then (b, ord_inv builtin)
- else if Node.equal b RealValue.zero then (a, builtin)
+ if Node.equal a RealValue.zero then b
+ else if Node.equal b RealValue.zero then a
else
let a, b, builtin =
if Node.compare a b < 0 then (a, b, builtin)
else (b, a, ord_inv builtin)
in
- (LRA_build.sub d a b, builtin)
+ let p = Polynome.of_list Q.zero [ (a, Q.one); (b, Q.minus_one) ] in
+
+ let n = Dom_polynome.node_of_polynome d p in
+ if not (Node.HC.mem seen d n) then (
+ Egraph.register d n;
+ Dom_interval.Propagate.sub d ~a ~b ~r:n;
+ Dom_polynome.assume_equality d n p;
+ Dom_product.propagate_a_cb d ~a ~b ~c:Q.minus_one ~res:n);
+ Dom_interval.Propagate.cmp d (build builtin) ~r:(Ground.node f) ~a:n
+ ~b:RealValue.zero;
+ n
in
- Egraph.register d n;
- let n' = build builtin d n RealValue.zero in
- Egraph.register d n';
- Egraph.merge d (Ground.node f) n';
+ (* todo move to a decision about sign of n *)
+ Choice.register d f (Boolean.chobool (Ground.node f));
+
+ if not (Node.HC.mem seen d n) then (
+ Node.HC.set seen d n ();
- Dom_polynome.events_repr_change d ~node:n DaemonSimplex.enqueue;
- Events.attach_repr d n DaemonSimplex.enqueue;
- Events.attach_dom d n Dom_interval.dom DaemonSimplex.enqueue;
+ Dom_polynome.events_repr_change d ~node:n DaemonSimplex.enqueue;
+ Events.attach_repr d n DaemonSimplex.enqueue;
+ Events.attach_dom d n Dom_interval.dom DaemonSimplex.enqueue;
- Datastructure.Push.push comparisons d n;
- Events.new_pending_daemon d DaemonSimplex.key ();
- Choice.register d f (Boolean.chobool (Ground.node f))
+ Datastructure.Push.push comparisons d n;
+ Events.new_pending_daemon d DaemonSimplex.key ())
| _ -> ()
let init env = Ground.register_converter env converter
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index c3a153e4a..3afcb5a46 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -105,7 +105,7 @@ module ChoBool = struct
let choose_decision node env =
match is env node with
| Some _ ->
- Debug.dprintf2 Debug.decision "[Bool] No decision for %a" Node.pp node;
+ (* Debug.dprintf2 Debug.decision "[Bool] No decision for %a" Node.pp node; *)
Choice.DecNo
| None -> DecTodo
(List.map (fun v env -> make_decision env node v)
diff --git a/src_common/union/why3session.xml b/src_common/union/why3session.xml
index ba4719739..2feb3b6bb 100644
--- a/src_common/union/why3session.xml
+++ b/src_common/union/why3session.xml
@@ -315,7 +315,7 @@
</transf>
</goal>
<goal name="inter'vc.61.1.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.40"/></proof>
+ <proof prover="3"><result status="valid" time="2.75"/></proof>
</goal>
<goal name="inter'vc.61.1.7" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
@@ -730,7 +730,7 @@
</transf>
</goal>
<goal name="inter'vc.125.1.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="5.46"/></proof>
+ <proof prover="3"><result status="valid" time="4.64"/></proof>
</goal>
<goal name="inter'vc.125.1.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -760,7 +760,7 @@
<proof prover="3"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="inter'vc.125.1.7.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.27"/></proof>
+ <proof prover="3"><result status="valid" time="1.03"/></proof>
</goal>
<goal name="inter'vc.125.1.7.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.21"/></proof>
@@ -784,7 +784,7 @@
<proof prover="3"><result status="valid" time="3.64"/></proof>
</goal>
<goal name="inter'vc.125.2.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.19"/></proof>
+ <proof prover="3"><result status="valid" time="2.40"/></proof>
</goal>
<goal name="inter'vc.125.2.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1112,7 +1112,7 @@
<goal name="inter'vc.174.2.7" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="inter'vc.174.2.7.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.30"/></proof>
+ <proof prover="3"><result status="valid" time="2.83"/></proof>
</goal>
<goal name="inter'vc.174.2.7.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.35"/></proof>
@@ -1243,7 +1243,7 @@
</transf>
</goal>
<goal name="inter'vc.192.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="inter'vc.192.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.93"/></proof>
@@ -1478,7 +1478,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="union_on_on'vc.67.0.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.41"/></proof>
+ <proof prover="3"><result status="valid" time="1.68"/></proof>
</goal>
<goal name="union_on_on'vc.67.0.7" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="3.37"/></proof>
@@ -1486,7 +1486,7 @@
</transf>
</goal>
<goal name="union_on_on'vc.67.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.70"/></proof>
+ <proof prover="3"><result status="valid" time="2.44"/></proof>
</goal>
</transf>
</goal>
@@ -1731,7 +1731,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union_on_off'vc.61.1.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.67"/></proof>
+ <proof prover="3"><result status="valid" time="3.10"/></proof>
</goal>
<goal name="union_on_off'vc.61.1.7" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
@@ -1941,7 +1941,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union_off_off'vc.60" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.03"/></proof>
+ <proof prover="3"><result status="valid" time="2.57"/></proof>
</goal>
<goal name="union_off_off'vc.61" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
@@ -1987,7 +1987,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="union_off_off'vc.61.0.7.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.14"/></proof>
+ <proof prover="3"><result status="valid" time="3.57"/></proof>
</goal>
</transf>
</goal>
@@ -2169,7 +2169,7 @@
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="except'vc.19" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.88"/></proof>
+ <proof prover="3"><result status="valid" time="0.62"/></proof>
</goal>
<goal name="except'vc.20" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
@@ -2325,7 +2325,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="add_interval_on'vc.12" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.81"/></proof>
+ <proof prover="3"><result status="valid" time="0.55"/></proof>
</goal>
<goal name="add_interval_on'vc.13" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
@@ -2334,7 +2334,7 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="add_interval_on'vc.15" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.97"/></proof>
+ <proof prover="3"><result status="valid" time="4.59"/></proof>
</goal>
<goal name="add_interval_on'vc.16" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.26"/></proof>
@@ -2385,7 +2385,7 @@
<proof prover="3"><result status="valid" time="0.98"/></proof>
</goal>
<goal name="add_interval_off'vc.11.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.40"/></proof>
+ <proof prover="3"><result status="valid" time="5.08"/></proof>
</goal>
</transf>
</goal>
@@ -2398,7 +2398,7 @@
<goal name="add_interval_off'vc.14" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="add_interval_off'vc.14.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.69"/></proof>
+ <proof prover="3"><result status="valid" time="1.34"/></proof>
</goal>
<goal name="add_interval_off'vc.14.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.12"/></proof>
@@ -2481,7 +2481,7 @@
<proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="add_interval_off_remain'vc.19.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.28"/></proof>
+ <proof prover="3"><result status="valid" time="0.42"/></proof>
</goal>
<goal name="add_interval_off_remain'vc.19.3" expl="postcondition" proved="true">
<transf name="left" proved="true" >
@@ -2494,14 +2494,14 @@
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="add_interval_off_remain'vc.19.3.0.2" expl="left case" proved="true">
- <proof prover="3" timelimit="100"><result status="valid" time="11.06"/></proof>
+ <proof prover="3" timelimit="100"><result status="valid" time="18.98"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="add_interval_off_remain'vc.19.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.75"/></proof>
+ <proof prover="3"><result status="valid" time="3.76"/></proof>
</goal>
</transf>
</goal>
@@ -2519,7 +2519,7 @@
<goal name="add_interval_off_remain'vc.20.3" expl="postcondition" proved="true">
<transf name="left" proved="true" >
<goal name="add_interval_off_remain'vc.20.3.0" expl="left case" proved="true">
- <proof prover="3" timelimit="100"><result status="valid" time="13.72"/></proof>
+ <proof prover="3" timelimit="100"><result status="valid" time="24.12"/></proof>
</goal>
</transf>
</goal>
@@ -2554,7 +2554,7 @@
<goal name="add_interval_off_remain'vc.25.3" expl="postcondition" proved="true">
<transf name="left" proved="true" >
<goal name="add_interval_off_remain'vc.25.3.0" expl="left case" proved="true">
- <proof prover="3" timelimit="100"><result status="valid" time="5.35"/></proof>
+ <proof prover="3" timelimit="100"><result status="valid" time="9.98"/></proof>
</goal>
</transf>
</goal>
@@ -2577,7 +2577,7 @@
<goal name="add_interval_off_remain'vc.26.3" expl="postcondition" proved="true">
<transf name="left" proved="true" >
<goal name="add_interval_off_remain'vc.26.3.0" expl="left case" proved="true">
- <proof prover="3"><result status="valid" time="4.63"/></proof>
+ <proof prover="3"><result status="valid" time="8.36"/></proof>
</goal>
</transf>
</goal>
@@ -2600,7 +2600,7 @@
<goal name="add_interval_off_remain'vc.27.3" expl="postcondition" proved="true">
<transf name="left" proved="true" >
<goal name="add_interval_off_remain'vc.27.3.0" expl="left case" proved="true">
- <proof prover="3"><result status="valid" time="4.27"/></proof>
+ <proof prover="3"><result status="valid" time="7.76"/></proof>
</goal>
</transf>
</goal>
@@ -2612,7 +2612,7 @@
<goal name="add_interval_off_remain'vc.28" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="add_interval_off_remain'vc.28.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.74"/></proof>
</goal>
<goal name="add_interval_off_remain'vc.28.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="1.16"/></proof>
@@ -2630,24 +2630,24 @@
<goal name="add_interval_off_remain'vc.30.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="add_interval_off_remain'vc.30.0.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.19"/></proof>
+ <proof prover="3"><result status="valid" time="2.10"/></proof>
</goal>
<goal name="add_interval_off_remain'vc.30.0.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.51"/></proof>
+ <proof prover="3"><result status="valid" time="1.21"/></proof>
</goal>
<goal name="add_interval_off_remain'vc.30.0.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.20"/></proof>
+ <proof prover="3"><result status="valid" time="0.98"/></proof>
</goal>
<goal name="add_interval_off_remain'vc.30.0.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.46"/></proof>
+ <proof prover="3"><result status="valid" time="0.47"/></proof>
</goal>
<goal name="add_interval_off_remain'vc.30.0.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.21"/></proof>
+ <proof prover="3"><result status="valid" time="0.79"/></proof>
</goal>
</transf>
</goal>
<goal name="add_interval_off_remain'vc.30.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.76"/></proof>
+ <proof prover="3"><result status="valid" time="1.11"/></proof>
</goal>
<goal name="add_interval_off_remain'vc.30.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -2657,7 +2657,7 @@
<goal name="add_interval_off_remain'vc.31" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="add_interval_off_remain'vc.31.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.73"/></proof>
+ <proof prover="3"><result status="valid" time="3.22"/></proof>
</goal>
<goal name="add_interval_off_remain'vc.31.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
@@ -2719,7 +2719,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="add_interval'vc.6" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="1.13"/></proof>
+ <proof prover="3"><result status="valid" time="0.90"/></proof>
</goal>
<goal name="add_interval'vc.7" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -2816,7 +2816,7 @@
<proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" >
<goal name="add_minus_inf_on'vc.12.0" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" >
<goal name="add_minus_inf_on'vc.12.0.0" expl="postcondition">
<proof prover="3"><result status="timeout" time="5.00"/></proof>
@@ -2859,13 +2859,13 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="add_minus_inf_on'vc.20" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" >
<goal name="add_minus_inf_on'vc.20.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="add_minus_inf_on'vc.20.1" expl="postcondition">
- <proof prover="3"><result status="highfailure" time="3.87"/></proof>
+ <proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="add_minus_inf_on'vc.20.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -2873,13 +2873,13 @@
</transf>
</goal>
<goal name="add_minus_inf_on'vc.21" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
<transf name="split_vc" >
<goal name="add_minus_inf_on'vc.21.0" expl="postcondition">
<proof prover="3"><result status="timeout" time="5.00"/></proof>
</goal>
<goal name="add_minus_inf_on'vc.21.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.03"/></proof>
+ <proof prover="3"><result status="valid" time="1.32"/></proof>
</goal>
</transf>
</goal>
--
GitLab