From 8c325a4bf6888e33fb8fdc1e071a8aab4aa20b6f Mon Sep 17 00:00:00 2001 From: Tim King Date: Mon, 12 Nov 2012 22:54:35 +0000 Subject: [PATCH] Delta is now generated in arithmetic to keep consistent the total order of DeltaRational values for lowerbounds, upperbounds, assignments and disequalities. Throws LogicException when a non-linear term is asserted and the the LogicInfo isLinear() disagrees. --- src/theory/arith/arithvar.h | 5 + src/theory/arith/partial_model.cpp | 88 ++++++++------- src/theory/arith/partial_model.h | 27 +++-- src/theory/arith/theory_arith.cpp | 103 ++++++++++++------ src/theory/arith/theory_arith.h | 13 ++- test/regress/regress0/arith/Makefile.am | 4 +- .../regress/regress0/arith/bug443.delta01.smt | 37 +++++++ test/regress/regress0/arith/mult.02.smt2 | 11 ++ 8 files changed, 204 insertions(+), 84 deletions(-) create mode 100644 test/regress/regress0/arith/bug443.delta01.smt create mode 100644 test/regress/regress0/arith/mult.02.smt2 diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h index 5982b7ac5..7cb6c6e99 100644 --- a/src/theory/arith/arithvar.h +++ b/src/theory/arith/arithvar.h @@ -60,6 +60,11 @@ public: virtual void operator()(Node n) = 0; }; +class RationalCallBack { +public: + virtual Rational operator()() const = 0; +}; + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index edba437ab..0ffe67763 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -26,7 +26,7 @@ namespace CVC4 { namespace theory { namespace arith { -ArithPartialModel::ArithPartialModel(context::Context* c) +ArithPartialModel::ArithPartialModel(context::Context* c, RationalCallBack& deltaComputingFunc) : d_mapSize(0), d_hasSafeAssignment(), d_assignment(), @@ -35,9 +35,20 @@ ArithPartialModel::ArithPartialModel(context::Context* c) d_lbc(c), d_deltaIsSafe(false), d_delta(-1,1), + d_deltaComputingFunc(deltaComputingFunc), d_history() { } + +const Rational& ArithPartialModel::getDelta(){ + if(!d_deltaIsSafe){ + Rational nextDelta = d_deltaComputingFunc(); + setDelta(nextDelta); + } + Assert(d_deltaIsSafe); + return d_delta; +} + bool ArithPartialModel::boundsAreEqual(ArithVar x) const{ if(hasLowerBound(x) && hasUpperBound(x)){ return getUpperBound(x) == getLowerBound(x); @@ -54,8 +65,7 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& r){ d_hasSafeAssignment[x] = true; d_history.push_back(x); } - - d_deltaIsSafe = false; + invalidateDelta(); d_assignment[x] = r; } void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r){ @@ -72,7 +82,7 @@ void ArithPartialModel::setAssignment(ArithVar x, const DeltaRational& safe, con } } - d_deltaIsSafe = false; + invalidateDelta(); d_assignment[x] = r; } @@ -93,7 +103,7 @@ void ArithPartialModel::initialize(ArithVar x, const DeltaRational& r){ d_hasSafeAssignment.push_back( false ); // Is wirth mentioning that this is not strictly necessary, but this maintains the internal invariant // that when d_assignment is set this gets set. - d_deltaIsSafe = false; + invalidateDelta(); d_assignment.push_back( r ); d_safeAssignment.push_back( DeltaRational(0) ); @@ -149,7 +159,7 @@ void ArithPartialModel::setLowerBoundConstraint(Constraint c){ Assert(inMaps(x)); Assert(greaterThanLowerBound(x, c->getValue())); - d_deltaIsSafe = false; + invalidateDelta(); d_lbc.set(x, c); } @@ -163,7 +173,7 @@ void ArithPartialModel::setUpperBoundConstraint(Constraint c){ Assert(inMaps(x)); Assert(lessThanUpperBound(x, c->getValue())); - d_deltaIsSafe = false; + invalidateDelta(); d_ubc.set(x, c); } @@ -245,7 +255,7 @@ void ArithPartialModel::clearSafeAssignments(bool revert){ } if(revert && !d_history.empty()){ - d_deltaIsSafe = false; + invalidateDelta(); } d_history.clear(); @@ -275,37 +285,37 @@ void ArithPartialModel::printModel(ArithVar x){ Debug("model") << endl; } -void ArithPartialModel::deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u){ - const Rational& c = l.getNoninfinitesimalPart(); - const Rational& k = l.getInfinitesimalPart(); - const Rational& d = u.getNoninfinitesimalPart(); - const Rational& h = u.getInfinitesimalPart(); - - if(c < d && k > h){ - Rational ep = (d-c)/(k-h); - if(ep < d_delta){ - d_delta = ep; - } - } -} - -void ArithPartialModel::computeDelta(const Rational& init){ - Assert(!d_deltaIsSafe); - d_delta = init; - - for(ArithVar x = 0; x < d_mapSize; ++x){ - const DeltaRational& a = getAssignment(x); - if(hasLowerBound(x)){ - const DeltaRational& l = getLowerBound(x); - deltaIsSmallerThan(l,a); - } - if(hasUpperBound(x)){ - const DeltaRational& u = getUpperBound(x); - deltaIsSmallerThan(a,u); - } - } - d_deltaIsSafe = true; -} +// void ArithPartialModel::deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u){ +// const Rational& c = l.getNoninfinitesimalPart(); +// const Rational& k = l.getInfinitesimalPart(); +// const Rational& d = u.getNoninfinitesimalPart(); +// const Rational& h = u.getInfinitesimalPart(); + +// if(c < d && k > h){ +// Rational ep = (d-c)/(k-h); +// if(ep < d_delta){ +// d_delta = ep; +// } +// } +// } + +// void ArithPartialModel::computeDelta(const Rational& init){ +// Assert(!d_deltaIsSafe); +// d_delta = init; + +// for(ArithVar x = 0; x < d_mapSize; ++x){ +// const DeltaRational& a = getAssignment(x); +// if(hasLowerBound(x)){ +// const DeltaRational& l = getLowerBound(x); +// deltaIsSmallerThan(l,a); +// } +// if(hasUpperBound(x)){ +// const DeltaRational& u = getUpperBound(x); +// deltaIsSmallerThan(a,u); +// } +// } +// d_deltaIsSafe = true; +// } }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index bcc65b85d..49cfd44a1 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -50,8 +50,12 @@ private: context::CDVector d_ubc; context::CDVector d_lbc; + // This is true when setDelta() is called, until invalidateDelta is called bool d_deltaIsSafe; + // Cache of a value of delta to ensure a total order. Rational d_delta; + // Function to call if the value of delta needs to be recomputed. + RationalCallBack& d_deltaComputingFunc; /** * List contains all of the variables that have an unsafe assignment. @@ -62,7 +66,7 @@ private: public: - ArithPartialModel(context::Context* c); + ArithPartialModel(context::Context* c, RationalCallBack& deltaComputation); void setLowerBoundConstraint(Constraint lb); void setUpperBoundConstraint(Constraint ub); @@ -175,20 +179,19 @@ public: return d_ubc[x] != NullConstraint; } - const Rational& getDelta(const Rational& init = Rational(1)){ - Assert(init.sgn() > 0); - if(!d_deltaIsSafe){ - computeDelta(init); - }else if(init < d_delta){ - d_delta = init; - } - return d_delta; + const Rational& getDelta(); + + inline void invalidateDelta() { + d_deltaIsSafe = false; } -private: + void setDelta(const Rational& d){ + d_delta = d; + d_deltaIsSafe = true; + } - void computeDelta(const Rational& init); - void deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u); + +private: /** * This function implements the mostly identical: diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b342c9271..e23262137 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -28,6 +28,7 @@ #include "util/boolean_simplification.h" #include "util/dense_map.h" +#include "smt/logic_exception.h" #include "theory/arith/arith_utilities.h" #include "theory/arith/delta_rational.h" @@ -68,7 +69,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_diseqQueue(c, false), d_currentPropagationList(), d_learnedBounds(c), - d_partialModel(c), + d_partialModel(c, d_deltaComputeCallback), d_tableau(), d_linEq(d_partialModel, d_tableau, d_basicVarModelUpdateCallBack), d_diosolver(c), @@ -81,6 +82,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap, d_raiseConflict), d_simplex(d_linEq, d_raiseConflict), d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager, d_raiseConflict), + d_deltaComputeCallback(this), d_basicVarModelUpdateCallBack(d_simplex), d_DELTA_ZERO(0), d_statistics() @@ -664,6 +666,7 @@ bool TheoryArith::AssertDisequality(Constraint constraint){ }else{ Debug("eq") << "push back" << constraint << endl; d_diseqQueue.push(constraint); + d_partialModel.invalidateDelta(); } return false; @@ -854,6 +857,10 @@ void TheoryArith::setupVariableList(const VarList& vl){ if(!vl.singleton()){ // vl is the product of at least 2 variables // vl : (* v1 v2 ...) + if(getLogicInfo().isLinear()){ + throw LogicException("Non-linear term was asserted to arithmetic in a linear logic."); + } + d_out->setIncomplete(); d_nlIncomplete = true; @@ -885,6 +892,11 @@ void TheoryArith::cautiousSetupPolynomial(const Polynomial& p){ void TheoryArith::setupDivLike(const Variable& v){ Assert(v.isDivLike()); + + if(getLogicInfo().isLinear()){ + throw LogicException("Non-linear term was asserted to arithmetic in a linear logic."); + } + Node vnode = v.getNode(); Assert(isSetup(vnode)); // Otherwise there is some invariant breaking recursion Polynomial m = Polynomial::parsePolynomial(vnode[0]); @@ -2075,44 +2087,74 @@ DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) { } } -Rational TheoryArith::safeDeltaValueForDisequality(){ +Rational TheoryArith::deltaValueForTotalOrder() const{ Rational min(2); - context::CDQueue::const_iterator iter = d_diseqQueue.begin(); - context::CDQueue::const_iterator iter_end = d_diseqQueue.end(); + std::set relevantDeltaValues; + context::CDQueue::const_iterator qiter = d_diseqQueue.begin(); + context::CDQueue::const_iterator qiter_end = d_diseqQueue.end(); - for(; iter != iter_end; ++iter){ - Constraint curr = *iter; - - ArithVar lhsVar = curr->getVariable(); + for(; qiter != qiter_end; ++qiter){ + Constraint curr = *qiter; - const DeltaRational& lhsValue = d_partialModel.getAssignment(lhsVar); const DeltaRational& rhsValue = curr->getValue(); - DeltaRational diff = lhsValue - rhsValue; - Assert(diff.sgn() != 0); - - // diff != 0 - // dinf * delta + dmajor != 0 - // dinf * delta != -dmajor - const Rational& dinf = diff.getInfinitesimalPart(); - const Rational& dmaj = diff.getNoninfinitesimalPart(); - if(dinf.isZero()){ - Assert(!dmaj.isZero()); - }else if(dmaj.isZero()){ - Assert(!dinf.isZero()); - }else{ - // delta != - dmajor / dinf - // if 0 < delta < abs(dmajor/dinf), then - Rational d = (dmaj/dinf).abs(); - Assert(d.sgn() > 0); + relevantDeltaValues.insert(rhsValue); + } + + for(ArithVar v = 0; v < d_variables.size(); ++v){ + const DeltaRational& value = d_partialModel.getAssignment(v); + relevantDeltaValues.insert(value); + if( d_partialModel.hasLowerBound(v)){ + const DeltaRational& lb = d_partialModel.getLowerBound(v); + relevantDeltaValues.insert(lb); + } + if( d_partialModel.hasUpperBound(v)){ + const DeltaRational& ub = d_partialModel.getUpperBound(v); + relevantDeltaValues.insert(ub); + } + } + + if(relevantDeltaValues.size() >= 2){ + std::set::const_iterator iter = relevantDeltaValues.begin(); + std::set::const_iterator iter_end = relevantDeltaValues.end(); + DeltaRational prev = *iter; + ++iter; + for(; iter != iter_end; ++iter){ + const DeltaRational& curr = *iter; + + Assert(prev < curr); + + const Rational& pinf = prev.getInfinitesimalPart(); + const Rational& cinf = curr.getInfinitesimalPart(); - if(d < min){ - min = d; + const Rational& pmaj = prev.getNoninfinitesimalPart(); + const Rational& cmaj = curr.getNoninfinitesimalPart(); + + if(pmaj == cmaj){ + Assert(pinf < cinf); + // any value of delta preserves the order + }else if(pinf == cinf){ + Assert(pmaj < cmaj); + // any value of delta preserves the order + }else{ + Assert(pinf != cinf && pmaj != cmaj); + Rational denDiffAbs = (cinf - pinf).abs(); + + Rational numDiff = (cmaj - pmaj); + Assert(numDiff.sgn() >= 0); + Assert(denDiffAbs.sgn() > 0); + Rational ratio = numDiff / denDiffAbs; + Assert(ratio.sgn() > 0); + + if(ratio < min){ + min = ratio; + } } + prev = curr; } } Assert(min.sgn() > 0); - Rational belowMin = min/Rational(2); + Rational belowMin = min/Rational(2); return belowMin; } @@ -2124,8 +2166,7 @@ void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){ // Delta lasts at least the duration of the function call - const Rational init = safeDeltaValueForDisequality(); - const Rational& delta = d_partialModel.getDelta(init); + const Rational& delta = d_partialModel.getDelta(); std::hash_set shared = currentlySharedTerms(); // TODO: diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 754fa6521..9c2ca7d45 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -322,6 +322,17 @@ private: Node axiomIteForTotalIntDivision(Node int_div_like); + class DeltaComputeCallback : public RationalCallBack { + private: + const TheoryArith* d_ta; + public: + DeltaComputeCallback(const TheoryArith* ta) : d_ta(ta){} + + Rational operator()() const{ + return d_ta->deltaValueForTotalOrder(); + } + } d_deltaComputeCallback; + public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe); virtual ~TheoryArith(); @@ -335,7 +346,7 @@ public: void propagate(Effort e); Node explain(TNode n); - Rational safeDeltaValueForDisequality(); + Rational deltaValueForTotalOrder() const; void collectModelInfo( TheoryModel* m, bool fullModel ); void shutdown(){ } diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index a30c99462..12aa0eecd 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -36,7 +36,9 @@ TESTS = \ div.06.smt2 \ div.07.smt2 \ div.08.smt2 \ - mult.01.smt2 + mult.01.smt2 \ + mult.02.smt2 \ + bug443.delta01.smt # problem__003.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/arith/bug443.delta01.smt b/test/regress/regress0/arith/bug443.delta01.smt new file mode 100644 index 000000000..0b8a0d971 --- /dev/null +++ b/test/regress/regress0/arith/bug443.delta01.smt @@ -0,0 +1,37 @@ +(benchmark fuzzsmt +:logic QF_UFLRA +:extrafuns ((v1 Real)) +:extrafuns ((v2 Real)) +:extrafuns ((v0 Real)) +:extrapreds ((p1 Real)) +:status sat +:formula +(let (?n1 0) +(flet ($n2 (p1 ?n1)) +(let (?n3 1) +(flet ($n4 (= ?n3 v2)) +(let (?n5 5) +(let (?n6 (~ ?n5)) +(let (?n7 (* v2 ?n6)) +(let (?n8 (+ ?n7 v1)) +(flet ($n9 (= ?n5 ?n8)) +(let (?n10 (ite $n9 ?n3 v1)) +(flet ($n11 (= ?n7 ?n10)) +(flet ($n12 (p1 v0)) +(let (?n13 (ite $n12 ?n1 v1)) +(flet ($n14 (p1 ?n13)) +(let (?n15 (~ ?n7)) +(let (?n16 (- ?n3 ?n15)) +(flet ($n17 (>= ?n16 ?n8)) +(flet ($n18 (> ?n16 ?n1)) +(flet ($n19 (= ?n8 v0)) +(let (?n20 (ite $n19 ?n8 ?n16)) +(let (?n21 (ite $n18 ?n20 ?n7)) +(let (?n22 (ite $n17 ?n21 v2)) +(flet ($n23 (> ?n22 v1)) +(flet ($n24 (implies $n14 $n23)) +(flet ($n25 (and $n11 $n24)) +(flet ($n26 (implies $n4 $n25)) +(flet ($n27 (xor $n2 $n26)) +$n27 +)))))))))))))))))))))))))))) diff --git a/test/regress/regress0/arith/mult.02.smt2 b/test/regress/regress0/arith/mult.02.smt2 new file mode 100644 index 000000000..d690e38e8 --- /dev/null +++ b/test/regress/regress0/arith/mult.02.smt2 @@ -0,0 +1,11 @@ +; EXPECT: (error "Non-linear term was asserted to arithmetic in a linear logic.") +; EXIT: 1 +(set-logic QF_LRA) +(set-info :status unknown) +(declare-fun n () Real) + +; This example is test that LRA rejects multiplication terms + +(assert (= (* n n) 1)) + +(check-sat) -- 2.30.2