From 2979089be3bc655d8bdd6245e193f356b4f7c93c Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 8 Nov 2012 23:54:18 +0000 Subject: [PATCH] Turns on TheoryUF when non-linear arithmetic is turned on. Adds test cases for division by 0. --- src/smt/smt_engine.cpp | 9 ++ src/theory/arith/theory_arith.cpp | 136 +----------------------- test/regress/regress0/arith/Makefile.am | 12 ++- test/regress/regress0/arith/div.01.smt2 | 12 +++ test/regress/regress0/arith/div.02.smt2 | 10 ++ test/regress/regress0/arith/div.03.smt2 | 13 +++ test/regress/regress0/arith/div.04.smt2 | 12 +++ test/regress/regress0/arith/div.05.smt2 | 13 +++ test/regress/regress0/arith/div.06.smt2 | 15 +++ test/regress/regress0/arith/div.07.smt2 | 14 +++ test/regress/regress0/arith/div.08.smt2 | 11 ++ test/regress/regress0/arith/mod.02.smt2 | 11 ++ test/regress/regress0/arith/mod.03.smt2 | 12 +++ 13 files changed, 148 insertions(+), 132 deletions(-) create mode 100644 test/regress/regress0/arith/div.01.smt2 create mode 100644 test/regress/regress0/arith/div.02.smt2 create mode 100644 test/regress/regress0/arith/div.03.smt2 create mode 100644 test/regress/regress0/arith/div.04.smt2 create mode 100644 test/regress/regress0/arith/div.05.smt2 create mode 100644 test/regress/regress0/arith/div.06.smt2 create mode 100644 test/regress/regress0/arith/div.07.smt2 create mode 100644 test/regress/regress0/arith/div.08.smt2 create mode 100644 test/regress/regress0/arith/mod.02.smt2 create mode 100644 test/regress/regress0/arith/mod.03.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 7fcb64219..24d6fb0b4 100644 --- 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 3ea8b9550..4ce1113a4 100644 --- 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 d0b787f20..f2b70e280 100644 --- 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 index 000000000..d7d587021 --- /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 index 000000000..65dc21549 --- /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 index 000000000..17de612bb --- /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 index 000000000..c30b1cd2f --- /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 index 000000000..fcc50ec98 --- /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 index 000000000..b33749cc6 --- /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 index 000000000..4c45b32c8 --- /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 index 000000000..0b0d73ac1 --- /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 index 000000000..75b25c181 --- /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 index 000000000..760350c89 --- /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) -- 2.30.2