diff options
| -rw-r--r-- | src/theory/arith/normal_form.cpp | 11 | ||||
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 5 | ||||
| -rw-r--r-- | test/regress/regress0/uflia/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/uflia/error30.smt | 145 |
4 files changed, 159 insertions, 5 deletions
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 5fa6e08c6..986df5f80 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -495,11 +495,14 @@ Polynomial Comparison::normalizedVariablePart() const { Polynomial right = getRight(); if(right.isConstant()){ return left; - }else if(right.containsConstant()){ - Polynomial noConstant = right.getTail(); - return left - noConstant; }else{ - return left - right; + Polynomial noConstant = right.containsConstant() ? right.getTail() : right; + Polynomial diff = left - noConstant; + if(diff.leadingCoefficientIsPositive()){ + return diff; + }else{ + return -diff; + } } } default: diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 9ff9ceeb9..be24e43ba 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -207,6 +207,7 @@ Node TheoryArith::AssertLower(Constraint constraint){ }else if(cmpToUB == 0){ if(isInteger(x_i)){ d_constantIntegerVariables.push_back(x_i); + Debug("dio::push") << x_i << endl; } Constraint ub = d_partialModel.getUpperBoundConstraint(x_i); @@ -296,6 +297,7 @@ Node TheoryArith::AssertUpper(Constraint constraint){ }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i) if(isInteger(x_i)){ d_constantIntegerVariables.push_back(x_i); + Debug("dio::push") << x_i << endl; } Constraint lb = d_partialModel.getLowerBoundConstraint(x_i); if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){ @@ -396,6 +398,7 @@ Node TheoryArith::AssertEquality(Constraint constraint){ if(isInteger(x_i)){ d_constantIntegerVariables.push_back(x_i); + Debug("dio::push") << x_i << endl; } // Don't bother to check whether x_i != c_i is in d_diseq @@ -928,6 +931,7 @@ Node TheoryArith::dioCutting(){ // If the bounds are equal this is already in the dioSolver //Add v = dr as a speculation. Comparison eq = mkIntegerEqualityFromAssignment(v); + Debug("dio::push") <<v << " " << eq.getNode() << endl; Assert(!eq.isBoolean()); d_diosolver.pushInputConstraint(eq, eq.getNode()); // It does not matter what the explanation of eq is. @@ -994,6 +998,7 @@ Node TheoryArith::callDioSolver(){ Assert(orig.getKind() != EQUAL); return orig; }else{ + Debug("dio::push") << v << " " << eq.getNode() << endl; d_diosolver.pushInputConstraint(eq, orig); } } diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index 5b095b500..bfc13ae16 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -20,7 +20,8 @@ SMT_TESTS = \ xs-09-16-3-4-1-5.delta04.smt \ error0.smt2 \ error0.delta01.smt \ - simple_cyclic2.smt2 + simple_cyclic2.smt2 \ + error30.smt # Regression tests for SMT2 inputs SMT2_TESTS = diff --git a/test/regress/regress0/uflia/error30.smt b/test/regress/regress0/uflia/error30.smt new file mode 100644 index 000000000..f543cf0e8 --- /dev/null +++ b/test/regress/regress0/uflia/error30.smt @@ -0,0 +1,145 @@ +(benchmark fuzzsmt +:logic QF_UFLIA +:status sat +:extrafuns ((f0 Int Int Int)) +:extrapreds ((p0 Int Int)) +:extrafuns ((v0 Int)) +:extrafuns ((v1 Int)) +:extrafuns ((v2 Int)) +:formula +(let (?e3 6) +(let (?e4 (f0 v2 v2)) +(let (?e5 (* ?e3 v0)) +(let (?e6 (+ v1 v0)) +(let (?e7 (* v0 ?e3)) +(let (?e8 (* ?e6 (~ ?e3))) +(let (?e9 (* v1 (~ ?e3))) +(let (?e10 (ite (p0 ?e8 v2) 1 0)) +(flet ($e11 (>= ?e7 v2)) +(flet ($e12 (p0 v0 ?e4)) +(flet ($e13 (distinct v2 ?e7)) +(flet ($e14 (> ?e9 ?e6)) +(flet ($e15 (>= ?e9 ?e9)) +(flet ($e16 (< v1 ?e8)) +(flet ($e17 (p0 v1 ?e5)) +(flet ($e18 (> ?e9 v0)) +(flet ($e19 (>= ?e5 ?e7)) +(flet ($e20 (= v1 ?e8)) +(flet ($e21 (p0 ?e5 v0)) +(flet ($e22 (= ?e10 ?e5)) +(let (?e23 (ite $e19 ?e5 v1)) +(let (?e24 (ite $e22 v2 ?e10)) +(let (?e25 (ite $e15 ?e10 ?e24)) +(let (?e26 (ite $e20 ?e4 ?e23)) +(let (?e27 (ite $e16 ?e10 v2)) +(let (?e28 (ite $e17 ?e23 ?e26)) +(let (?e29 (ite $e22 ?e25 ?e26)) +(let (?e30 (ite $e18 ?e10 ?e23)) +(let (?e31 (ite $e11 ?e7 ?e26)) +(let (?e32 (ite $e14 ?e9 ?e27)) +(let (?e33 (ite $e12 ?e8 ?e9)) +(let (?e34 (ite $e13 ?e24 v0)) +(let (?e35 (ite $e21 ?e6 ?e30)) +(flet ($e36 (distinct ?e4 ?e30)) +(flet ($e37 (= ?e8 ?e29)) +(flet ($e38 (p0 ?e6 ?e8)) +(flet ($e39 (p0 ?e7 v0)) +(flet ($e40 (distinct ?e32 ?e5)) +(flet ($e41 (distinct v2 ?e24)) +(flet ($e42 (= v1 ?e29)) +(flet ($e43 (distinct ?e26 ?e26)) +(flet ($e44 (= ?e9 ?e4)) +(flet ($e45 (p0 ?e8 v1)) +(flet ($e46 (= v0 ?e33)) +(flet ($e47 (p0 v0 ?e26)) +(flet ($e48 (distinct ?e32 ?e24)) +(flet ($e49 (= ?e33 ?e29)) +(flet ($e50 (= ?e10 ?e25)) +(flet ($e51 (= v0 ?e30)) +(flet ($e52 (= ?e25 ?e23)) +(flet ($e53 (>= ?e27 ?e31)) +(flet ($e54 (distinct ?e25 ?e25)) +(flet ($e55 (p0 ?e28 ?e30)) +(flet ($e56 (> ?e29 ?e8)) +(flet ($e57 (p0 ?e8 ?e35)) +(flet ($e58 (distinct ?e7 v1)) +(flet ($e59 (distinct ?e7 v1)) +(flet ($e60 (> ?e9 ?e25)) +(flet ($e61 (< ?e33 ?e31)) +(flet ($e62 (< ?e4 ?e6)) +(flet ($e63 (< ?e35 ?e27)) +(flet ($e64 (<= ?e28 ?e23)) +(flet ($e65 (<= ?e8 ?e26)) +(flet ($e66 (<= ?e28 ?e29)) +(flet ($e67 (p0 ?e9 ?e29)) +(flet ($e68 (p0 ?e4 ?e24)) +(flet ($e69 (< ?e24 ?e25)) +(flet ($e70 (= ?e31 ?e7)) +(flet ($e71 (p0 ?e31 ?e10)) +(flet ($e72 (>= ?e28 ?e24)) +(flet ($e73 (< ?e34 ?e31)) +(flet ($e74 (implies $e53 $e22)) +(flet ($e75 (iff $e41 $e55)) +(flet ($e76 (if_then_else $e40 $e20 $e51)) +(flet ($e77 (xor $e75 $e12)) +(flet ($e78 (not $e39)) +(flet ($e79 (iff $e69 $e70)) +(flet ($e80 (or $e21 $e17)) +(flet ($e81 (not $e11)) +(flet ($e82 (if_then_else $e77 $e56 $e79)) +(flet ($e83 (implies $e64 $e38)) +(flet ($e84 (xor $e13 $e74)) +(flet ($e85 (implies $e67 $e68)) +(flet ($e86 (not $e66)) +(flet ($e87 (xor $e19 $e85)) +(flet ($e88 (not $e49)) +(flet ($e89 (iff $e72 $e15)) +(flet ($e90 (not $e16)) +(flet ($e91 (and $e48 $e63)) +(flet ($e92 (iff $e65 $e89)) +(flet ($e93 (xor $e81 $e91)) +(flet ($e94 (implies $e73 $e60)) +(flet ($e95 (iff $e45 $e44)) +(flet ($e96 (xor $e52 $e84)) +(flet ($e97 (not $e43)) +(flet ($e98 (if_then_else $e42 $e96 $e86)) +(flet ($e99 (or $e82 $e57)) +(flet ($e100 (iff $e92 $e47)) +(flet ($e101 (if_then_else $e83 $e83 $e14)) +(flet ($e102 (xor $e95 $e99)) +(flet ($e103 (xor $e58 $e50)) +(flet ($e104 (implies $e36 $e88)) +(flet ($e105 (implies $e18 $e71)) +(flet ($e106 (if_then_else $e59 $e37 $e78)) +(flet ($e107 (xor $e106 $e93)) +(flet ($e108 (iff $e80 $e105)) +(flet ($e109 (not $e100)) +(flet ($e110 (and $e107 $e54)) +(flet ($e111 (if_then_else $e61 $e61 $e76)) +(flet ($e112 (if_then_else $e98 $e108 $e108)) +(flet ($e113 (iff $e112 $e104)) +(flet ($e114 (if_then_else $e46 $e46 $e110)) +(flet ($e115 (not $e90)) +(flet ($e116 (iff $e62 $e114)) +(flet ($e117 (if_then_else $e97 $e115 $e97)) +(flet ($e118 (iff $e117 $e101)) +(flet ($e119 (and $e109 $e109)) +(flet ($e120 (and $e111 $e111)) +(flet ($e121 (xor $e119 $e94)) +(flet ($e122 (xor $e118 $e102)) +(flet ($e123 (implies $e87 $e120)) +(flet ($e124 (xor $e103 $e123)) +(flet ($e125 (implies $e121 $e121)) +(flet ($e126 (or $e113 $e113)) +(flet ($e127 (not $e126)) +(flet ($e128 (if_then_else $e125 $e116 $e127)) +(flet ($e129 (iff $e122 $e128)) +(flet ($e130 (or $e124 $e124)) +(flet ($e131 (or $e130 $e130)) +(flet ($e132 (implies $e129 $e129)) +(flet ($e133 (or $e131 $e131)) +(flet ($e134 (not $e133)) +(flet ($e135 (implies $e132 $e134)) +$e135 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + |