diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/normal_form.cpp | 11 | ||||
-rw-r--r-- | src/theory/arith/theory_arith.cpp | 5 |
2 files changed, 12 insertions, 4 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); } } |