From 8b5686a7dd0b559356e9e3bf76be93ad9c726085 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 10 Nov 2012 19:01:49 +0000 Subject: [PATCH] Fix for bug 439. Delta computation now includes disequality information. --- src/theory/arith/partial_model.cpp | 4 +- src/theory/arith/partial_model.h | 9 ++-- src/theory/arith/theory_arith.cpp | 45 ++++++++++++++++++- src/theory/arith/theory_arith.h | 1 + test/regress/regress0/uflra/Makefile.am | 4 +- test/regress/regress0/uflra/neq-deltacomp.smt | 2 +- 6 files changed, 56 insertions(+), 9 deletions(-) diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 73e7943b0..edba437ab 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -289,9 +289,9 @@ void ArithPartialModel::deltaIsSmallerThan(const DeltaRational& l, const DeltaRa } } -void ArithPartialModel::computeDelta(){ +void ArithPartialModel::computeDelta(const Rational& init){ Assert(!d_deltaIsSafe); - d_delta = 1; + d_delta = init; for(ArithVar x = 0; x < d_mapSize; ++x){ const DeltaRational& a = getAssignment(x); diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index 83e2a4f2b..bcc65b85d 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -175,16 +175,19 @@ public: return d_ubc[x] != NullConstraint; } - const Rational& getDelta(){ + const Rational& getDelta(const Rational& init = Rational(1)){ + Assert(init.sgn() > 0); if(!d_deltaIsSafe){ - computeDelta(); + computeDelta(init); + }else if(init < d_delta){ + d_delta = init; } return d_delta; } private: - void computeDelta(); + void computeDelta(const Rational& init); void deltaIsSmallerThan(const DeltaRational& l, const DeltaRational& u); /** diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 4ce1113a4..b342c9271 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2075,14 +2075,57 @@ DeltaRational TheoryArith::getDeltaValueWithNonlinear(TNode n, bool& failed) { } } +Rational TheoryArith::safeDeltaValueForDisequality(){ + Rational min(2); + context::CDQueue::const_iterator iter = d_diseqQueue.begin(); + context::CDQueue::const_iterator iter_end = d_diseqQueue.end(); + + for(; iter != iter_end; ++iter){ + Constraint curr = *iter; + + ArithVar lhsVar = curr->getVariable(); + + 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); + + if(d < min){ + min = d; + } + } + } + + Assert(min.sgn() > 0); + Rational belowMin = min/Rational(2); + return belowMin; +} + void TheoryArith::collectModelInfo( TheoryModel* m, bool fullModel ){ AlwaysAssert(d_qflraStatus == Result::SAT); //AlwaysAssert(!d_nlIncomplete, "Arithmetic solver cannot currently produce models for input with nonlinear arithmetic constraints"); Debug("arith::collectModelInfo") << "collectModelInfo() begin " << endl; + // Delta lasts at least the duration of the function call - const Rational& delta = d_partialModel.getDelta(); + const Rational init = safeDeltaValueForDisequality(); + const Rational& delta = d_partialModel.getDelta(init); std::hash_set shared = currentlySharedTerms(); // TODO: diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index da4a80208..754fa6521 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -335,6 +335,7 @@ public: void propagate(Effort e); Node explain(TNode n); + Rational safeDeltaValueForDisequality(); void collectModelInfo( TheoryModel* m, bool fullModel ); void shutdown(){ } diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 289569b1a..f4797a287 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -35,8 +35,8 @@ SMT_TESTS = \ incorrect1.smt \ incorrect1.delta01.smt \ incorrect1.delta02.smt - error1.smt - + error1.smt \ + neq-deltacomp.smt # Regression tests for SMT2 inputs SMT2_TESTS = diff --git a/test/regress/regress0/uflra/neq-deltacomp.smt b/test/regress/regress0/uflra/neq-deltacomp.smt index 4144fcb79..9185a18c8 100644 --- a/test/regress/regress0/uflra/neq-deltacomp.smt +++ b/test/regress/regress0/uflra/neq-deltacomp.smt @@ -3,7 +3,7 @@ :extrafuns ((v2 Real)) :extrafuns ((v1 Real)) :extrafuns ((v0 Real)) -:status unknown +:status sat :formula (let (?n1 (~ v1)) (flet ($n2 (>= ?n1 v0)) -- 2.30.2