summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/smt_engine.cpp9
-rw-r--r--src/theory/arith/theory_arith.cpp136
-rw-r--r--test/regress/regress0/arith/Makefile.am12
-rw-r--r--test/regress/regress0/arith/div.01.smt212
-rw-r--r--test/regress/regress0/arith/div.02.smt210
-rw-r--r--test/regress/regress0/arith/div.03.smt213
-rw-r--r--test/regress/regress0/arith/div.04.smt212
-rw-r--r--test/regress/regress0/arith/div.05.smt213
-rw-r--r--test/regress/regress0/arith/div.06.smt215
-rw-r--r--test/regress/regress0/arith/div.07.smt214
-rw-r--r--test/regress/regress0/arith/div.08.smt211
-rw-r--r--test/regress/regress0/arith/mod.02.smt211
-rw-r--r--test/regress/regress0/arith/mod.03.smt212
13 files changed, 148 insertions, 132 deletions
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback