Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases for divisi...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7fcb64219cd540dc1b7c063fbd166a84cd40f3ab..24d6fb0b4b137cb017265819b816d979092fe8e4 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -661,6 +661,15 @@ void SmtEngine::setLogicInternal() throw() {
 
   d_logic.lock();
 
+  // may need to force uninterpreted functions to be on for non-linear
+  if(d_logic.isTheoryEnabled(theory::THEORY_ARITH) &&
+     !d_logic.isLinear() &&
+     !d_logic.isTheoryEnabled(theory::THEORY_UF)){
+    d_logic = d_logic.getUnlockedCopy();
+    d_logic.enableTheory(theory::THEORY_UF);
+    d_logic.lock();
+  }
+
   // Set the options for the theoryOf
   if(!options::theoryOfMode.wasSetByUser()) {
     if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) {

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 3ea8b95507287d7b90bbedd5d4a35282e505122d..4ce1113a4c5cbb99c3a04acd8aa57f86c465d404 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1008,7 +1008,7 @@ Node TheoryArith::axiomIteForTotalIntDivision(Node int_div_like){
   Polynomial rp = Polynomial::parsePolynomial(r);
   Polynomial qp = Polynomial::parsePolynomial(q);
 
-  Node abs_d = (n.isConstant()) ? 
+  Node abs_d = (n.isConstant()) ?
     d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs_$$");
 
   Node eq = Comparison::mkComparison(EQUAL, n, d * qp + rp).getNode();
@@ -1016,9 +1016,7 @@ Node TheoryArith::axiomIteForTotalIntDivision(Node int_div_like){
   Node leq1 = currNM->mkNode(LT, r, abs_d);
 
   Node andE = currNM->mkNode(AND, eq, leq0, leq1);
-    
   Node defDivMode = dEq0.iteNode(qEq0.andNode(rEq0), andE);
-    
   Node lem = abs_d.getMetaKind () == metakind::VARIABLE ?
     defDivMode.andNode(d.makeAbsCondition(Variable(abs_d))) : defDivMode;
 
@@ -1469,130 +1467,6 @@ bool TheoryArith::assertionCases(Constraint constraint){
     return false;
   }
 }
-// Node TheoryArith::assertionCases(TNode assertion){
-//   Constraint constraint = d_constraintDatabase.lookup(assertion);
-
-//   Kind simpleKind = Comparison::comparisonKind(assertion);
-//   Assert(simpleKind != UNDEFINED_KIND);
-//   Assert(constraint != NullConstraint ||
-//          simpleKind == EQUAL ||
-//          simpleKind == DISTINCT );
-//   if(simpleKind == EQUAL || simpleKind == DISTINCT){
-//     Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
-
-//     if(!isSetup(eq)){
-//       //The previous code was equivalent to:
-//       setupAtom(eq);
-//       constraint = d_constraintDatabase.lookup(assertion);
-//     }
-//   }
-//   Assert(constraint != NullConstraint);
-
-//   if(constraint->negationHasProof()){
-//     Constraint negation = constraint->getNegation();
-//     if(negation->isSelfExplaining()){
-//       if(Debug.isOn("whytheoryenginewhy")){
-//         debugPrintFacts();
-//       }
-// //      Warning() << "arith: Theory engine is sending me both a literal and its negation?"
-// //                << "BOOOOOOOOOOOOOOOOOOOOOO!!!!"<< endl;
-//     }
-//     Debug("arith::eq") << constraint << endl;
-//     Debug("arith::eq") << negation << endl;
-
-//     NodeBuilder<> nb(kind::AND);
-//     nb << assertion;
-//     negation->explainForConflict(nb);
-//     Node conflict = nb;
-//     Debug("arith::eq") << "conflict" << conflict << endl;
-//     return conflict;
-//   }
-//   Assert(!constraint->negationHasProof());
-
-//   if(constraint->assertedToTheTheory()){
-//     //Do nothing
-//     return Node::null();
-//   }
-//   Assert(!constraint->assertedToTheTheory());
-//   constraint->setAssertedToTheTheory();
-
-//   ArithVar x_i = constraint->getVariable();
-//   //DeltaRational c_i = determineRightConstant(assertion, simpleKind);
-
-//   //Assert(constraint->getVariable() == determineLeftVariable(assertion, simpleKind));
-//   //Assert(constraint->getValue() == determineRightConstant(assertion, simpleKind));
-//   Assert(!constraint->hasLiteral() || constraint->getLiteral() == assertion);
-
-//   Debug("arith::assertions")  << "arith assertion @" << getSatContext()->getLevel()
-//                               <<"(" << assertion
-//                               << " \\-> "
-//     //<< determineLeftVariable(assertion, simpleKind)
-//                               <<" "<< simpleKind <<" "
-//     //<< determineRightConstant(assertion, simpleKind)
-//                               << ")" << std::endl;
-
-
-//   Debug("arith::constraint") << "arith constraint " << constraint << std::endl;
-
-//   if(!constraint->hasProof()){
-//     Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
-//     constraint->selfExplaining();
-//   }else{
-//     Debug("arith::constraint") << "already has proof: " << constraint->explainForConflict() << endl;
-//   }
-
-//   Assert(!isInteger(x_i) ||
-//          simpleKind == EQUAL ||
-//          simpleKind == DISTINCT ||
-//          simpleKind == GEQ ||
-//          simpleKind == LT);
-
-//   switch(constraint->getType()){
-//   case UpperBound:
-//     if(simpleKind == LT && isInteger(x_i)){
-//       Constraint floorConstraint = constraint->getFloor();
-//       if(!floorConstraint->isTrue()){
-//         if(floorConstraint->negationHasProof()){
-//           return ConstraintValue::explainConflict(constraint, floorConstraint->getNegation());
-//         }else{
-//           floorConstraint->impliedBy(constraint);
-//         }
-//       }
-//       //c_i = DeltaRational(c_i.floor());
-//       //return AssertUpper(x_i, c_i, assertion, floorConstraint);
-//       return AssertUpper(floorConstraint);
-//     }else{
-//       return AssertUpper(constraint);
-//     }
-//     //return AssertUpper(x_i, c_i, assertion, constraint);
-//   case LowerBound:
-//     if(simpleKind == LT && isInteger(x_i)){
-//       Constraint ceilingConstraint = constraint->getCeiling();
-//       if(!ceilingConstraint->isTrue()){
-//         if(ceilingConstraint->negationHasProof()){
-
-//           return ConstraintValue::explainConflict(constraint, ceilingConstraint->getNegation());
-//         }
-//         ceilingConstraint->impliedBy(constraint);
-//       }
-//       //c_i = DeltaRational(c_i.ceiling());
-//       //return AssertLower(x_i, c_i, assertion, ceilingConstraint);
-//       return AssertLower(ceilingConstraint);
-//     }else{
-//       return AssertLower(constraint);
-//     }
-//     //return AssertLower(x_i, c_i, assertion, constraint);
-//   case Equality:
-//     return AssertEquality(constraint);
-//     //return AssertEquality(x_i, c_i, assertion, constraint);
-//   case Disequality:
-//     return AssertDisequality(constraint);
-//     //return AssertDisequality(x_i, c_i, assertion, constraint);
-//   default:
-//     Unreachable();
-//     return Node::null();
-//   }
-// }
 
 /**
  * Looks for the next integer variable without an integer assignment in a round robin fashion.
@@ -2281,11 +2155,11 @@ void TheoryArith::notifyRestart(){
     }else if(d_tableauResetDensity * copySize <=  currSize){
       d_simplex.reduceQueue();
       if(safeToReset()){
-       Debug("arith::reset") << "resetting " << d_restartsCounter << endl;
-       ++d_statistics.d_currSetToSmaller;
-       d_tableau = d_smallTableauCopy;
+        Debug("arith::reset") << "resetting " << d_restartsCounter << endl;
+        ++d_statistics.d_currSetToSmaller;
+        d_tableau = d_smallTableauCopy;
       }else{
-       Debug("arith::reset") << "not safe to reset at the moment " << d_restartsCounter << endl;
+        Debug("arith::reset") << "not safe to reset at the moment " << d_restartsCounter << endl;
       }
     }
   }

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index d0b787f20c6ec6aeeff2a5c1f9167ddc4eaa715c..f2b70e280ff6b2d8cd16b739ca56c7a0fe6d4494 100644 (file)
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -25,7 +25,17 @@ TESTS =      \
        leq.01.smt \
        miplibtrick.smt \
        DTP_k2_n35_c175_s15.smt2 \
-       mod.01.smt2
+       mod.01.smt2 \
+       mod.02.smt2 \
+       mod.03.smt2 \
+       div.01.smt2 \
+       div.02.smt2 \
+       div.03.smt2 \
+       div.04.smt2 \
+       div.05.smt2 \
+       div.06.smt2 \
+       div.07.smt2 \
+       div.08.smt2
 #      problem__003.smt2
 
 EXTRA_DIST = $(TESTS)

diff --git a/test/regress/regress0/arith/div.01.smt2 b/test/regress/regress0/arith/div.01.smt2
new file mode 100644 (file)
index 0000000..d7d5870
--- /dev/null
+++ b/test/regress/regress0/arith/div.01.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unsat)
+(declare-fun n () Int)
+
+(assert (= n 0))
+(assert (= (div (div n n) n)
+           (div (div (div n n) n) n)))
+(assert (distinct (div (div n n) n)
+                  (div (div (div (div (div n n) n) n) n) n)))
+
+(check-sat)

diff --git a/test/regress/regress0/arith/div.02.smt2 b/test/regress/regress0/arith/div.02.smt2
new file mode 100644 (file)
index 0000000..65dc215
--- /dev/null
+++ b/test/regress/regress0/arith/div.02.smt2
@@ -0,0 +1,10 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun n () Int)
+
+(assert (distinct (div n n) 1))
+
+(check-sat)

diff --git a/test/regress/regress0/arith/div.03.smt2 b/test/regress/regress0/arith/div.03.smt2
new file mode 100644 (file)
index 0000000..17de612
--- /dev/null
+++ b/test/regress/regress0/arith/div.03.smt2
@@ -0,0 +1,13 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun x () Int)
+(declare-fun n () Int)
+
+(assert (> n 0))
+(assert (>= x n))
+(assert (< (div x n) 1))
+
+(check-sat)

diff --git a/test/regress/regress0/arith/div.04.smt2 b/test/regress/regress0/arith/div.04.smt2
new file mode 100644 (file)
index 0000000..c30b1cd
--- /dev/null
+++ b/test/regress/regress0/arith/div.04.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun n () Real)
+
+(assert (not (=> (= x y) (= (/ x n) (/ y n)))))
+(assert (<= n 0))
+(assert (>= n 0))
+
+(check-sat)

diff --git a/test/regress/regress0/arith/div.05.smt2 b/test/regress/regress0/arith/div.05.smt2
new file mode 100644 (file)
index 0000000..fcc50ec
--- /dev/null
+++ b/test/regress/regress0/arith/div.05.smt2
@@ -0,0 +1,13 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun n () Real)
+
+(assert (= (/ x n) 0))
+(assert (= (/ y n) 1))
+
+(check-sat)

diff --git a/test/regress/regress0/arith/div.06.smt2 b/test/regress/regress0/arith/div.06.smt2
new file mode 100644 (file)
index 0000000..b33749c
--- /dev/null
+++ b/test/regress/regress0/arith/div.06.smt2
@@ -0,0 +1,15 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun n () Real)
+
+(assert (= (/ x n) 0))
+(assert (= (/ y n) 1))
+(assert (<= n 0))
+(assert (>= n 0))
+
+(check-sat)

diff --git a/test/regress/regress0/arith/div.07.smt2 b/test/regress/regress0/arith/div.07.smt2
new file mode 100644 (file)
index 0000000..4c45b32
--- /dev/null
+++ b/test/regress/regress0/arith/div.07.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_NRA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun n () Real)
+
+(assert (= (/ x n) 0))
+(assert (= (/ y (/ x n)) 1))
+(assert (<= n 0))
+(assert (>= n 0))
+(assert (= x y))
+
+(check-sat)

diff --git a/test/regress/regress0/arith/div.08.smt2 b/test/regress/regress0/arith/div.08.smt2
new file mode 100644 (file)
index 0000000..0b0d73a
--- /dev/null
+++ b/test/regress/regress0/arith/div.08.smt2
@@ -0,0 +1,11 @@
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unsat)
+(declare-fun n () Int)
+
+
+(assert (= (div n n) (div (div n n) n)))
+(assert (distinct (div (div n n) n) (div (div (div n n) n) n)))
+(assert (<= n 0))
+(assert (>= n 0))
+(check-sat)

diff --git a/test/regress/regress0/arith/mod.02.smt2 b/test/regress/regress0/arith/mod.02.smt2
new file mode 100644 (file)
index 0000000..75b25c1
--- /dev/null
+++ b/test/regress/regress0/arith/mod.02.smt2
@@ -0,0 +1,11 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun n () Int)
+
+(assert (distinct n 0))
+(assert (> (mod n n) 0))
+
+(check-sat)

diff --git a/test/regress/regress0/arith/mod.03.smt2 b/test/regress/regress0/arith/mod.03.smt2
new file mode 100644 (file)
index 0000000..760350c
--- /dev/null
+++ b/test/regress/regress0/arith/mod.03.smt2
@@ -0,0 +1,12 @@
+; EXPECT: unknown
+; EXIT: 0
+(set-logic QF_NIA)
+(set-info :smt-lib-version 2.0)
+(set-info :status unknown)
+(declare-fun n () Int)
+(declare-fun x () Int)
+
+(assert (< (mod x n) 0))
+(assert (< (div x n) 0))
+
+(check-sat)