diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-10-17 03:12:17 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-10-17 03:12:17 +0000 |
commit | bb59480a36fb0f799af53676c07b8fca43c2fff4 (patch) | |
tree | 555fb1210e2e94ba09bb9dd447cac30a6ad2ab70 /test | |
parent | 5cb65d8beac0f06fcafbef99d109c09ad029b14d (diff) |
Sharing work
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/arith/integers/Makefile.am | 72 | ||||
-rw-r--r-- | test/regress/regress0/uflra/Makefile.am | 22 | ||||
-rw-r--r-- | test/regress/regress0/uflra/simple.01.cvc | 6 | ||||
-rw-r--r-- | test/regress/regress0/uflra/simple.02.cvc | 10 | ||||
-rw-r--r-- | test/regress/regress0/uflra/simple.03.cvc | 12 | ||||
-rw-r--r-- | test/regress/regress0/uflra/simple.04.cvc | 15 | ||||
-rw-r--r-- | test/unit/theory/theory_arith_white.h | 8 | ||||
-rw-r--r-- | test/unit/theory/theory_black.h | 4 |
8 files changed, 63 insertions, 86 deletions
diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am index 3d7f40c71..d0340616f 100644 --- a/test/regress/regress0/arith/integers/Makefile.am +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -23,77 +23,7 @@ TESTS = \ arith-int-017.cvc \ arith-int-018.cvc \ arith-int-019.cvc \ - arith-int-020.cvc \ - arith-int-021.cvc \ - arith-int-023.cvc \ - arith-int-024.cvc \ - arith-int-025.cvc \ - arith-int-026.cvc \ - arith-int-027.cvc \ - arith-int-028.cvc \ - arith-int-029.cvc \ - arith-int-030.cvc \ - arith-int-031.cvc \ - arith-int-032.cvc \ - arith-int-033.cvc \ - arith-int-034.cvc \ - arith-int-035.cvc \ - arith-int-036.cvc \ - arith-int-037.cvc \ - arith-int-038.cvc \ - arith-int-039.cvc \ - arith-int-040.cvc \ - arith-int-041.cvc \ - arith-int-044.cvc \ - arith-int-045.cvc \ - arith-int-046.cvc \ - arith-int-048.cvc \ - arith-int-049.cvc \ - arith-int-051.cvc \ - arith-int-052.cvc \ - arith-int-053.cvc \ - arith-int-054.cvc \ - arith-int-055.cvc \ - arith-int-056.cvc \ - arith-int-057.cvc \ - arith-int-058.cvc \ - arith-int-059.cvc \ - arith-int-060.cvc \ - arith-int-061.cvc \ - arith-int-062.cvc \ - arith-int-063.cvc \ - arith-int-064.cvc \ - arith-int-065.cvc \ - arith-int-066.cvc \ - arith-int-067.cvc \ - arith-int-068.cvc \ - arith-int-069.cvc \ - arith-int-070.cvc \ - arith-int-071.cvc \ - arith-int-072.cvc \ - arith-int-073.cvc \ - arith-int-074.cvc \ - arith-int-075.cvc \ - arith-int-076.cvc \ - arith-int-077.cvc \ - arith-int-078.cvc \ - arith-int-079.cvc \ - arith-int-080.cvc \ - arith-int-081.cvc \ - arith-int-083.cvc \ - arith-int-085.cvc \ - arith-int-086.cvc \ - arith-int-087.cvc \ - arith-int-088.cvc \ - arith-int-089.cvc \ - arith-int-090.cvc \ - arith-int-091.cvc \ - arith-int-092.cvc \ - arith-int-093.cvc \ - arith-int-094.cvc \ - arith-int-095.cvc \ - arith-int-096.cvc \ - arith-int-099.cvc + arith-int-020.cvc EXTRA_DIST = $(TESTS) \ arith-int-008.cvc \ diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 5199f2b62..377489ef7 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -6,15 +6,19 @@ MAKEFLAGS = -k # put it below in "TESTS +=" # Regression tests for SMT inputs -#SMT_TESTS = \ -# pb_real_10_0100_10_10.smt \ -# pb_real_10_0100_10_11.smt \ -# pb_real_10_0100_10_15.smt \ -# pb_real_10_0100_10_16.smt \ -# pb_real_10_0100_10_19.smt \ -# pb_real_10_0200_10_22.smt \ -# pb_real_10_0200_10_26.smt \ -# pb_real_10_0200_10_29.smt +SMT_TESTS = \ + simple.01.cvc \ + simple.02.cvc \ + simple.03.cvc \ + simple.04.cvc \ + pb_real_10_0100_10_10.smt \ + pb_real_10_0100_10_11.smt \ + pb_real_10_0100_10_15.smt \ + pb_real_10_0100_10_16.smt \ + pb_real_10_0100_10_19.smt \ + pb_real_10_0200_10_22.smt \ + pb_real_10_0200_10_26.smt \ + pb_real_10_0200_10_29.smt # Regression tests for SMT2 inputs SMT2_TESTS = diff --git a/test/regress/regress0/uflra/simple.01.cvc b/test/regress/regress0/uflra/simple.01.cvc new file mode 100644 index 000000000..8904192ce --- /dev/null +++ b/test/regress/regress0/uflra/simple.01.cvc @@ -0,0 +1,6 @@ +% EXPECT: sat +% EXIT: 10 +x, y: REAL; +f: REAL -> REAL; + +CHECKSAT NOT (f(x) = f(y));
\ No newline at end of file diff --git a/test/regress/regress0/uflra/simple.02.cvc b/test/regress/regress0/uflra/simple.02.cvc new file mode 100644 index 000000000..a14ca8a1f --- /dev/null +++ b/test/regress/regress0/uflra/simple.02.cvc @@ -0,0 +1,10 @@ +% EXPECT: unsat +% EXIT: 20 +x, y: REAL; +f: REAL -> REAL; + +ASSERT (x <= y); +ASSERT (y <= x); +ASSERT NOT (f(x) = f(y)); + +CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/uflra/simple.03.cvc b/test/regress/regress0/uflra/simple.03.cvc new file mode 100644 index 000000000..1fdeed40a --- /dev/null +++ b/test/regress/regress0/uflra/simple.03.cvc @@ -0,0 +1,12 @@ +% EXPECT: sat +% EXIT: 10 +x1, y1, z1: REAL; +x2, y2, z2: REAL; +f: REAL -> REAL; +g: (REAL, REAL) -> REAL; + +ASSERT (z1 = f(x1)); +ASSERT (z2 = f(y1)); +ASSERT NOT (g(z1, z2) = g(z2, y2)); + +CHECKSAT;
\ No newline at end of file diff --git a/test/regress/regress0/uflra/simple.04.cvc b/test/regress/regress0/uflra/simple.04.cvc new file mode 100644 index 000000000..c9c226fa2 --- /dev/null +++ b/test/regress/regress0/uflra/simple.04.cvc @@ -0,0 +1,15 @@ +% EXPECT: unsat +% EXIT: 20 +x1, x2: REAL; +y1, y2: REAL; +f: REAL -> REAL; +g: (REAL, REAL) -> REAL; + +ASSERT (x1 <= x2) AND (x2 <= x1); + +ASSERT NOT (g(x1, y1) = g(x2, y2)); + +ASSERT (y1 <= f(x1)) AND (f(x1) <= y1); +ASSERT (y2 <= f(x2)) AND (f(x2) <= y2); + +CHECKSAT;
\ No newline at end of file diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index f0073cc0b..4787dfd21 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -128,7 +128,7 @@ public: Node leq = d_nm->mkNode(LEQ, x, c); fakeTheoryEnginePreprocess(leq); - d_arith->assertFact(leq); + d_arith->assertFact(leq, true); d_arith->check(d_level); @@ -160,7 +160,7 @@ public: fakeTheoryEnginePreprocess(leq1); fakeTheoryEnginePreprocess(geq1); - d_arith->assertFact(lt1); + d_arith->assertFact(lt1, true); d_arith->check(d_level); @@ -199,7 +199,7 @@ public: fakeTheoryEnginePreprocess(leq1); fakeTheoryEnginePreprocess(geq1); - d_arith->assertFact(leq0); + d_arith->assertFact(leq0, true); d_arith->check(d_level); @@ -235,7 +235,7 @@ public: fakeTheoryEnginePreprocess(leq1); fakeTheoryEnginePreprocess(geq1); - d_arith->assertFact(leq1); + d_arith->assertFact(leq1, true); d_arith->check(d_level); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 63900c19c..be1d4a35b 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -214,8 +214,8 @@ public: void testDone() { TS_ASSERT(d_dummy->doneWrapper()); - d_dummy->assertFact(atom0); - d_dummy->assertFact(atom1); + d_dummy->assertFact(atom0, true); + d_dummy->assertFact(atom1, true); TS_ASSERT(!d_dummy->doneWrapper()); |