virtual void operator()(Node n) = 0;
};
+class RationalCallBack {
+public:
+ virtual Rational operator()() const = 0;
+};
+
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
namespace theory {
namespace arith {
-ArithPartialModel::ArithPartialModel(context::Context* c)
+ArithPartialModel::ArithPartialModel(context::Context* c, RationalCallBack& deltaComputingFunc)
: d_mapSize(0),
d_hasSafeAssignment(),
d_assignment(),
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);
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){
}
}
- d_deltaIsSafe = false;
+ invalidateDelta();
d_assignment[x] = 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) );
Assert(inMaps(x));
Assert(greaterThanLowerBound(x, c->getValue()));
- d_deltaIsSafe = false;
+ invalidateDelta();
d_lbc.set(x, c);
}
Assert(inMaps(x));
Assert(lessThanUpperBound(x, c->getValue()));
- d_deltaIsSafe = false;
+ invalidateDelta();
d_ubc.set(x, c);
}
}
if(revert && !d_history.empty()){
- d_deltaIsSafe = false;
+ invalidateDelta();
}
d_history.clear();
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 */
context::CDVector<Constraint> d_ubc;
context::CDVector<Constraint> 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.
public:
- ArithPartialModel(context::Context* c);
+ ArithPartialModel(context::Context* c, RationalCallBack& deltaComputation);
void setLowerBoundConstraint(Constraint lb);
void setUpperBoundConstraint(Constraint ub);
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:
#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"
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),
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()
}else{
Debug("eq") << "push back" << constraint << endl;
d_diseqQueue.push(constraint);
+ d_partialModel.invalidateDelta();
}
return false;
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;
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]);
}
}
-Rational TheoryArith::safeDeltaValueForDisequality(){
+Rational TheoryArith::deltaValueForTotalOrder() const{
Rational min(2);
- context::CDQueue<Constraint>::const_iterator iter = d_diseqQueue.begin();
- context::CDQueue<Constraint>::const_iterator iter_end = d_diseqQueue.end();
+ std::set<DeltaRational> relevantDeltaValues;
+ context::CDQueue<Constraint>::const_iterator qiter = d_diseqQueue.begin();
+ context::CDQueue<Constraint>::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<DeltaRational>::const_iterator iter = relevantDeltaValues.begin();
+ std::set<DeltaRational>::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;
}
// 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<TNode, TNodeHashFunction> shared = currentlySharedTerms();
// TODO:
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();
void propagate(Effort e);
Node explain(TNode n);
- Rational safeDeltaValueForDisequality();
+ Rational deltaValueForTotalOrder() const;
void collectModelInfo( TheoryModel* m, bool fullModel );
void shutdown(){ }
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)
--- /dev/null
+(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
+))))))))))))))))))))))))))))
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff