diff options
| author | Tim King <taking@cs.nyu.edu> | 2011-05-31 01:06:16 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2011-05-31 01:06:16 +0000 |
| commit | 46a299aa48bcb0bff64bdb607f61f75a05987962 (patch) | |
| tree | 3880ed92599b84b59d4b135ab4513dd7c50f76e4 /test | |
| parent | b9ffc0f2cf5d2f05e5269ffb8b5f58c5d7f71e0c (diff) | |
This commit contains the code for allowing arbitrary equalities in the theory of arithmetic.
* This code has been partially tested. (My testing situation is currently not so great.) The code for testing not preregistering equalities can be compile time enabled by setting the boolean turnOffEqualityPreRegister. Don't be shocked by slowdowns or failures. This does pass make regress as well as a fresh checkout does. (The Mac version has issues.)
* I need to disable the permanent row removal heuristic by default. We need to discuss why this needs to happen. We should probably detect pure QF_LRA/QF_RDL problems and enable this when this can safely be done.
* I have disabled the arithmetic rewrite equality flag. This code needs to be added to the parser.
* For all of the above changes, I have annotated the code with the key word BREADCRUMB.
* I have renamed ArithUnatePropagator to ArithAtomDatabase.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/arith/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/arith/fuzz_3-eq.smt | 46 |
2 files changed, 47 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index a039f028b..700c59b8e 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -8,6 +8,7 @@ TESTS = \ arith.02.cvc \ arith.03.cvc \ delta-minimized-row-vector-bug.smt \ + fuzz_3-eq.smt \ leq.01.smt \ miplibtrick.smt diff --git a/test/regress/regress0/arith/fuzz_3-eq.smt b/test/regress/regress0/arith/fuzz_3-eq.smt new file mode 100644 index 000000000..ef44444b7 --- /dev/null +++ b/test/regress/regress0/arith/fuzz_3-eq.smt @@ -0,0 +1,46 @@ +(benchmark fuzzsmt +:logic QF_LRA +:extrafuns ((v0 Real)) +:extrafuns ((v2 Real)) +:extrafuns ((v1 Real)) +:status sat +:formula +(let (?n1 2) +(let (?n2 (* ?n1 ?n1)) +(let (?n3 (~ v0)) +(let (?n4 (* ?n1 ?n3)) +(let (?n5 (- ?n1 ?n1)) +(let (?n6 (- ?n5 v0)) +(let (?n7 (- ?n4 ?n6)) +(flet ($n8 (= ?n2 ?n7)) +(flet ($n9 false) +(let (?n10 (ite $n9 ?n1 v1)) +(let (?n11 (+ ?n1 v2)) +(flet ($n12 (= ?n10 ?n11)) +(let (?n13 (ite $n9 v0 ?n2)) +(let (?n14 (~ ?n1)) +(let (?n15 (ite $n9 ?n14 ?n1)) +(flet ($n16 (= ?n13 ?n15)) +(flet ($n17 (= ?n1 ?n7)) +(let (?n18 (+ ?n1 ?n1)) +(flet ($n19 (= v2 ?n18)) +(let (?n20 (ite $n19 v2 ?n1)) +(let (?n21 (ite $n17 ?n18 ?n20)) +(flet ($n22 (= ?n21 ?n2)) +(let (?n23 (ite $n9 ?n21 ?n2)) +(flet ($n24 (= ?n23 ?n1)) +(flet ($n25 (= ?n7 ?n2)) +(flet ($n26 (iff $n24 $n25)) +(let (?n27 (~ ?n7)) +(flet ($n28 (= ?n27 ?n1)) +(let (?n29 (ite $n28 ?n1 ?n1)) +(flet ($n30 (= ?n1 ?n29)) +(flet ($n31 (implies $n26 $n30)) +(flet ($n32 (implies $n9 $n9)) +(flet ($n33 (if_then_else $n22 $n31 $n32)) +(flet ($n34 (and $n9 $n33)) +(flet ($n35 (if_then_else $n16 $n34 $n9)) +(flet ($n36 (iff $n12 $n35)) +(flet ($n37 (and $n8 $n36)) +$n37 +)))))))))))))))))))))))))))))))))))))) |