From 063327e25ff187ca19e170ded9f853f54e101ee7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 23 Nov 2021 11:02:49 +0100
Subject: [PATCH] [Demon] Fix missing attachment using the monad
---
src_colibri2/core/colibri2_core.mli | 3 +
src_colibri2/core/demon.ml | 17 +-
src_colibri2/core/demon.mli | 2 +
src_colibri2/core/egraph.ml | 4 +-
src_colibri2/tests/solve/all/unsat/dune.inc | 3 +
.../unsat/work_with_fourier_not_simplex.psmt2 | 649 ++++++++++++++++++
src_colibri2/theories/LRA/fourier.ml | 11 +-
src_colibri2/theories/LRA/simplex.ml | 2 +
8 files changed, 683 insertions(+), 8 deletions(-)
create mode 100644 src_colibri2/tests/solve/all/unsat/work_with_fourier_not_simplex.psmt2
diff --git a/src_colibri2/core/colibri2_core.mli b/src_colibri2/core/colibri2_core.mli
index 20578036d..99fde1fa9 100644
--- a/src_colibri2/core/colibri2_core.mli
+++ b/src_colibri2/core/colibri2_core.mli
@@ -1024,6 +1024,9 @@ module Monad : sig
val setv : ('a, _) Value.Kind.t -> Node.t -> 'a option monad -> sequence
+ val exec_ro : (Egraph.rt -> unit) -> 'a monad -> 'a monad
+ (** An hook in the middle, for printing debug message for example *)
+
val ( let+ ) : 'a option monad -> ('a -> 'c) -> 'c option monad
val ( let* ) : 'a option monad -> ('a -> 'c option) -> 'c option monad
diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml
index 6f3fa8e3f..ff08c8bc6 100644
--- a/src_colibri2/core/demon.ml
+++ b/src_colibri2/core/demon.ml
@@ -358,6 +358,7 @@ module Monad = struct
| Bindo : 'a option monad * ('a -> 'b option) -> 'b option monad
| GetV : Node.t * ('b, _) ValueKind.t -> 'b option monad
| GetD : Node.t * 'a DomKind.t -> 'a option monad
+ | Exec : (Egraph.rt -> unit) * 'a monad -> 'a monad
type sequence =
| Sequence : sequence * sequence -> sequence
@@ -373,6 +374,8 @@ module Monad = struct
let getd m n = GetD (n, m)
+ let exec_ro f m = Exec (f, m)
+
let setd m n f = SetD (n, m, f)
let updd m n f = UpdD (n, m, f)
@@ -436,6 +439,9 @@ module Monad = struct
| None -> None
| Some v -> Value.value m v)
| GetD (n, dom) -> Egraph.get_dom d dom n
+ | Exec (f, m) ->
+ f (Egraph.ro d);
+ compute d m
let rec compute_seq d acc : _ -> D.runable = function
| Sequence (a, b) -> compute_seq d (compute_seq d acc a) b
@@ -456,7 +462,10 @@ module Monad = struct
let rec attach_aux : type a. _ Egraph.t -> footprint -> a monad -> bool =
fun d ft -> function
- | Both (a, b) -> Stdlib.( && ) (attach_aux d ft a) (attach_aux d ft b)
+ | Both (a, b) ->
+ let b1 = attach_aux d ft a in
+ let b2 = attach_aux d ft b in
+ Stdlib.(b1 && b2)
| Bind (a, _) -> attach_aux d ft a
| Bindo (a, _) -> attach_aux d ft a
| GetV (n, m) -> (
@@ -470,9 +479,13 @@ module Monad = struct
let s = DomKind.Vector.get_def ft.doms dom Node.S.empty in
DomKind.Vector.set ft.doms dom (Node.S.add n s);
match Egraph.get_dom d dom n with None -> false | Some _ -> true)
+ | Exec (_, m) -> attach_aux d ft m
let rec attach_seq compute d = function
- | Sequence (a, b) -> attach_seq compute d a || attach_seq compute d b
+ | Sequence (a, b) ->
+ let b1 = attach_seq compute d a in
+ let b2 = attach_seq compute d b in
+ b1 || b2
| SetV (_, _, f) -> attach_aux compute d f
| SetD (_, _, f) -> attach_aux compute d f
| UpdD (_, _, f) -> attach_aux compute d f
diff --git a/src_colibri2/core/demon.mli b/src_colibri2/core/demon.mli
index 43f3d1cd4..a1db1ec25 100644
--- a/src_colibri2/core/demon.mli
+++ b/src_colibri2/core/demon.mli
@@ -153,6 +153,8 @@ module Monad : sig
val setv : ('a, _) ValueKind.t -> Node.t -> 'a option monad -> sequence
+ val exec_ro : (Egraph.rt -> unit) -> 'a monad -> 'a monad
+
val ( let+ ) : 'a option monad -> ('a -> 'c) -> 'c option monad
val ( let* ) : 'a option monad -> ('a -> 'c option) -> 'c option monad
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index a38171f0a..1b4f4a80e 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -34,7 +34,7 @@ let debug_few = Debug.register_info_flag
~desc:"for the core solver"
"Egraph.few"
-let print_decision = Colibri2_popop_lib.Debug.register_flag ~desc:"Print@ information@ about@ the@ decisions@ made" "decision"
+let print_decision = Colibri2_popop_lib.Debug.register_info_flag ~desc:"Print@ information@ about@ the@ decisions@ made" "decision"
let print_contradiction = Colibri2_popop_lib.Debug.register_info_flag ~desc:"Print@ information@ about@ the@ contradiction@ found" "contradiction"
let stats_set_dom =
@@ -528,7 +528,7 @@ module Delayed = struct
ignore (run_events t (fun t e -> e t node new_v) events)
let add_pending_merge (t : rw t) node node' =
- Debug.dprintf4 debug "[Egraph] @[add_pending_merge for %a and %a@]"
+ Debug.dprintf4 debug_few "[Egraph] @[add_pending_merge for %a and %a@]"
Node.pp node Node.pp node';
assert (is_registered t node);
assert (is_registered t node');
diff --git a/src_colibri2/tests/solve/all/unsat/dune.inc b/src_colibri2/tests/solve/all/unsat/dune.inc
index a2a7ebd96..4968e3c0f 100644
--- a/src_colibri2/tests/solve/all/unsat/dune.inc
+++ b/src_colibri2/tests/solve/all/unsat/dune.inc
@@ -37,3 +37,6 @@
(rule (alias runtest) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat
--dont-print-result %{dep:union-Union-length0_positiveqtvc_1.psmt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=20M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:union-Union-length0_positiveqtvc_1.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_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})))
diff --git a/src_colibri2/tests/solve/all/unsat/work_with_fourier_not_simplex.psmt2 b/src_colibri2/tests/solve/all/unsat/work_with_fourier_not_simplex.psmt2
new file mode 100644
index 000000000..590d1a32a
--- /dev/null
+++ b/src_colibri2/tests/solve/all/unsat/work_with_fourier_not_simplex.psmt2
@@ -0,0 +1,649 @@
+;; 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 () tqt)
+
+;; v
+(declare-fun v () tqt)
+
+;; u
+(declare-fun u1 () on)
+
+;; v
+(declare-fun v1 () on)
+
+;; Requires
+(assert (ordered_on u1))
+
+;; Requires
+(assert (ordered_on v1))
+
+;; result
+(declare-fun result () on)
+
+;; o
+(declare-fun o () t1)
+
+;; o
+(declare-fun o1 () on)
+
+;; o
+(declare-fun o2 () on)
+
+;; o
+(declare-fun o3 () on)
+
+;; o
+(declare-fun o4 () t1)
+
+;; o
+(declare-fun o5 () off)
+
+;; o
+(declare-fun o6 () on)
+
+;; o
+(declare-fun o7 () off)
+
+;; o
+(declare-fun o8 () t1)
+
+;; b
+(declare-fun b1 () t2)
+
+;; o
+(declare-fun o9 () off)
+
+;; o
+(declare-fun o10 () off)
+
+;; o
+(declare-fun o11 () off)
+
+;; o
+(declare-fun o12 () t1)
+
+;; o
+(declare-fun o13 () off)
+
+;; o
+(declare-fun o14 () on)
+
+;; o
+(declare-fun o15 () off)
+
+;; x
+(declare-fun x44 () t)
+
+;; x
+(declare-fun x45 () t2)
+
+;; x
+(declare-fun x46 () off)
+
+;; H
+(assert (= v1 (OnEnd x44 x45 x46)))
+
+;; x
+(declare-fun x47 () t)
+
+;; x
+(declare-fun x48 () on)
+
+;; H
+(assert (= u1 (OnSin x47 x48)))
+
+;; Ensures
+(assert
+ (let ((subject o12))
+ (ite ((_ is Eq) subject) (equal x47 x44) (ite ((_ is Lt) subject)
+ (infix_ls
+ x47
+ x44) (infix_ls x44 x47)))))
+
+;; H
+(assert (= o12 Eq))
+
+;; H
+(assert (lt_bound_on (real x44) x48))
+
+;; H
+(assert (forall ((r Real)) (=> (<= r (real x44)) (not (mem_off r x46)))))
+
+;; H
+(assert (ordered_off o13))
+
+;; H
+(assert
+ (forall ((x49 Real))
+ (= (and (mem_on x49 x48) (mem_off x49 x46)) (mem_off x49 o13))))
+
+;; H
+(assert
+ (forall ((q Real))
+ (=> (lt_bound_on q x48) (=> (lt_bound_off q x46) (lt_bound_off q o13)))))
+
+;; H
+(assert (= result (OnEnd x44 Strict o13)))
+
+;; Ensures
+(assert (ordered_on result))
+
+;; x
+(declare-fun x49 () Real)
+
+;; H
+(assert (mem_on x49 result))
+
+;; Hinst
+(assert (= (and (mem_on x49 x48) (mem_off x49 x46)) (mem_off x49 o13)))
+
+;; h
+(assert (not (< x49 (real x44))))
+
+;; h
+(assert (not (= x49 (real x44))))
+
+;; Goal inter'vc
+;; File "/home/bobot/Sources/colibrics/src_common/union.mlw", line 330, characters 8-13
+(assert
+ (not (mem_on x49 u1)))
+
+(check-sat)
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index 0aa6ae821..1ddd70a4b 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -163,8 +163,8 @@ let add_eq d eqs p bound origins =
Debug.dprintf2 debug "[Fourier] discard %a" Ground.S.pp origins;
eqs
| Some p, bound ->
- Debug.dprintf4 Debug.contradiction "[LRA/Fourier] Found %a%a0" Q.pp p
- Bound.pp bound;
+ Debug.dprintf6 Debug.contradiction "[LRA/Fourier] Found %a%a0 by %a" Q.pp
+ p Bound.pp bound Ground.S.pp origins;
Egraph.contradiction d
let mk_eq d bound a b =
@@ -273,9 +273,12 @@ module Daemon = struct
let name = "LRA.fourier"
end)
- let enqueue d _ =
- if Datastructure.Ref.get scheduled d then Events.EnqAlready
+ let enqueue d n =
+ if Datastructure.Ref.get scheduled d then (
+ Debug.dprintf2 debug "[Scheduler] Fourier for %a? No" Node.pp n;
+ Events.EnqAlready)
else (
+ Debug.dprintf2 debug "[Scheduler] Fourier for %a? Yes" Node.pp n;
Datastructure.Ref.set scheduled d true;
Events.EnqRun (key, (), None))
diff --git a/src_colibri2/theories/LRA/simplex.ml b/src_colibri2/theories/LRA/simplex.ml
index b71e33c80..d1a3a6ce7 100644
--- a/src_colibri2/theories/LRA/simplex.ml
+++ b/src_colibri2/theories/LRA/simplex.ml
@@ -341,6 +341,8 @@ let find_equalities d vars (env : Sim.Core.t) (s : Sim.Core.solution Lazy.t) =
update_under_approx s;
Debug.dprintf4 debug "[LRA/Simplex] Found %a = %a" Node.pp from
Node.pp to_;
+ Egraph.register d from;
+ Egraph.register d to_;
Egraph.merge d from to_;
test_equality env))
in
--
GitLab