From d5f90728466b978cb97a1dba8108a0780529645a Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Fri, 30 Jul 2021 18:54:32 +0200
Subject: [PATCH] rename test
---
debug | 92 -------------------
farith2/thry/Intv32.v | 3 -
.../tests/solve/smt_fp/unsat/dune.inc | 4 +-
.../unsat/{test.smt2 => propagate_le_ge.smt2} | 0
4 files changed, 2 insertions(+), 97 deletions(-)
delete mode 100644 debug
rename src_colibri2/tests/solve/smt_fp/unsat/{test.smt2 => propagate_le_ge.smt2} (100%)
diff --git a/debug b/debug
deleted file mode 100644
index 01efd4e9e..000000000
--- a/debug
+++ /dev/null
@@ -1,92 +0,0 @@
-[pre] set-logic: ALL
-<0.003511>[post] other_1: TODO
-<0.003578>
-<0.003586>[pre] antecedent: (fp.eq (_ +zero 8 24) (_ -zero 8 24))
-<0.003646>[post] hyp_1: hyp: fp.eq plus_zero minus_zero
-<0.003731>
-<0.003738>
-<0.003780>[Egraph] @0 is plus_zero
-<0.003799>[Egraph] @1 is minus_zero
-<0.003821>[Egraph] @2 is fp.eq(@0, @1)
-<0.003844>[Scheduler] New waiting daemon
-<0.003879>[Egraph.few] merge @⊤(@⊤) -> @2(@2)[pre] prove
-<0.003905>[post] prove_1: solve-assuming:
-<0.003927>
-<0.003935>
-<0.003949>[Scheduler] Step 1
-<0.003976>[Egraph] set_dom for @2 with Prop
-<0.004008>[Scheduler] New waiting daemon
-<0.004025>[Scheduler] New waiting daemon
-<0.004064>[Egraph] set_dom for @0 with [-∞, +∞] + NaN
-<0.004091>[Egraph] set_dom for @1 with [-∞, +∞] + NaN
-<0.004133>[FP] domains : a = [-∞, +∞] + NaN, b = [-∞, +∞] + NaN
-<0.004168>[FP] domains : a = [-∞, +∞] + NaN, b = [-∞, +∞] + NaN
-<0.004184>[Scheduler] New waiting daemon
-<0.004219>[Egraph] set_dom for @0 with
-<0.004237>Find_new_event @0 @0
-<0.004261>[Egraph] set_dom for @1 with
-<0.004276>Find_new_event @1 @1
-<0.004294>[Egraph] set_dom for @2 with
-<0.004309>Find_new_event @2 @2
-<0.004336>[Scheduler] Step 2
-<0.004359>[Egraph] set_dom for @0 with FloatingPoint_8_24
-<0.004384>[Egraph] @3 is +0
-<0.004403>[Scheduler] New waiting daemon
-<0.004422>[Egraph] set_dom for @0 with
-<0.004437>Find_new_event @0 @0
-<0.004452>Find_new_event @0 @0
-<0.004493>[Egraph] merge dom FP_ARITH (@0(@0),some [-∞, +∞] + NaN) <- (@3(@3),none)
-<0.004518>[Egraph] set_dom for @3 with [-∞, +∞] + NaN
-<0.004538>[Egraph] merge dom Ground.tys (@0(@0),some FloatingPoint_8_24) <- (@3(@3),none)
-<0.004558>[Egraph] set_dom for @0 with FloatingPoint_8_24
-<0.004573>[Egraph] set_dom for @3 with FloatingPoint_8_24
-<0.004591>[Egraph] merge dom Quantifier.info (@0(@0),some ) <- (@3(@3),none)
-<0.004607>[Egraph] set_dom for @3 with
-<0.004627>[Scheduler] New waiting daemon
-<0.004642>[Egraph.few] merge @3(@3) -> @0(@0)
-<0.004658>[Scheduler] Step 3
-<0.004674>[Egraph] set_dom for @1 with FloatingPoint_8_24
-<0.004694>[Egraph] @4 is -0
-<0.004710>[Scheduler] New waiting daemon
-<0.004729>[Egraph] set_dom for @1 with
-<0.004745>Find_new_event @1 @1
-<0.004759>Find_new_event @1 @1
-<0.004793>[Egraph] merge dom FP_ARITH (@1(@1),some [-∞, +∞] + NaN) <- (@4(@4),none)
-<0.004818>[Egraph] set_dom for @4 with [-∞, +∞] + NaN
-<0.004837>[Egraph] merge dom Ground.tys (@1(@1),some FloatingPoint_8_24) <- (@4(@4),none)
-<0.004855>[Egraph] set_dom for @1 with FloatingPoint_8_24
-<0.004870>[Egraph] set_dom for @4 with FloatingPoint_8_24
-<0.004888>[Egraph] merge dom Quantifier.info (@1(@1),some ) <- (@4(@4),none)
-<0.004904>[Egraph] set_dom for @4 with
-<0.004924>[Egraph.few] merge @4(@4) -> @1(@1)
-<0.004938>[Scheduler] Step 4
-<0.004975>INTER [-∞, +∞] + NaN [-∞, +∞] + NaN = [-∞, +∞] + NaN
-<0.005012>INTER [-∞, +∞] + NaN [-∞, +∞] + NaN = [-∞, +∞] + NaN
-<0.005025>[Scheduler] Step 5
-<0.005041>[Scheduler] Step 6
-<0.005053>[Scheduler] Step 7
-<0.005068>[Scheduler] LastEffort: 0
-<0.005079>[Scheduler] FixModel
-<0.005091>[Scheduler] Step 8
-<0.005116>[Egraph] set_value for @2 with true
-<0.005129>[Scheduler] Step 9
-<0.005180>FixModel wto:
-<0.005193>FixModel with ground terms
-<0.005208>FixModel with limit at 2
-<0.005221>[Scheduler] push from 0 (dec waiting:0)
-<0.005237>[Scheduler] Step 10
-<0.005252>FixModel check_ground terms
-<0.005278>[Scheduler] sat(10)
-<0.005353>Fourier.run : 0
-<0.005361>new_instantiation : 0
-<0.005367>instantiation : 0
-<0.005373>Scheduler.fix_model : 3
-<0.005381>Scheduler.step : 7
-<0.005387>Scheduler.conflict : 0
-<0.005393>Scheduler.decision : 0
-<0.005399>Scheduler.lasteffort : 0
-<0.005405>Scheduler.daemon : 6
-<0.005419>Egraph.register : 7
-<0.005425>Egraph.set_value/merge: 7
-<0.005433>Egraph.set_dom/merge : 18
-<0.005442>
\ No newline at end of file
diff --git a/farith2/thry/Intv32.v b/farith2/thry/Intv32.v
index 3e42d4ee8..5c135e067 100644
--- a/farith2/thry/Intv32.v
+++ b/farith2/thry/Intv32.v
@@ -75,9 +75,6 @@ Module Intv32.
end.
Program Definition s0 : Interval prec emax := Intv _ _ (B754_zero false) (B754_zero true) false.
-
-
- Compute (is_singleton s0).
Program Theorem is_singleton_correct :
forall (I : t) (x : float32), (is_singleton I = Some x) -> (forall y, contains I y -> x = y).
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
index 0d0e27d06..5d8594119 100644
--- a/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
+++ b/src_colibri2/tests/solve/smt_fp/unsat/dune.inc
@@ -8,5 +8,5 @@
--dont-print-result %{dep:nan_neq_float32.smt2})))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:nan_neq_float32.smt2})))
(rule (alias runtest) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat
---dont-print-result %{dep:test.smt2})))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:test.smt2})))
+--dont-print-result %{dep:propagate_le_ge.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=10M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:propagate_le_ge.smt2})))
diff --git a/src_colibri2/tests/solve/smt_fp/unsat/test.smt2 b/src_colibri2/tests/solve/smt_fp/unsat/propagate_le_ge.smt2
similarity index 100%
rename from src_colibri2/tests/solve/smt_fp/unsat/test.smt2
rename to src_colibri2/tests/solve/smt_fp/unsat/propagate_le_ge.smt2
--
GitLab