diff options
Diffstat (limited to 'src')
25 files changed, 2063 insertions, 127 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 2d306d464..e7cc9628e 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -354,6 +354,8 @@ libcvc4_la_SOURCES = \ theory/arith/fc_simplex.cpp \ theory/arith/soi_simplex.h \ theory/arith/soi_simplex.cpp \ + theory/arith/infer_bounds.h \ + theory/arith/infer_bounds.cpp \ theory/arith/approx_simplex.h \ theory/arith/approx_simplex.cpp \ theory/arith/attempt_solution_simplex.h \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 36f9866f4..6dd1f4465 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1192,7 +1192,7 @@ void SmtEngine::setDefaults() { if( options::ufssSymBreak() ){ options::sortInference.set( true ); } - if( options::qcfMode.wasSetByUser() ){ + if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 98aa43e71..f78893324 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -162,7 +162,7 @@ inline int deltaCoeff(Kind k){ * - (NOT (GT left right)) -> LEQ * If none of these match, it returns UNDEFINED_KIND. */ - inline Kind oldSimplifiedKind(TNode literal){ +inline Kind oldSimplifiedKind(TNode literal){ switch(literal.getKind()){ case kind::LT: case kind::GT: @@ -195,6 +195,19 @@ inline int deltaCoeff(Kind k){ } } +inline Kind negateKind(Kind k){ + switch(k){ + case kind::LT: return kind::GEQ; + case kind::GT: return kind::LEQ; + case kind::LEQ: return kind::GT; + case kind::GEQ: return kind::LT; + case kind::EQUAL: return kind::DISTINCT; + case kind::DISTINCT: return kind::EQUAL; + default: + return kind::UNDEFINED_KIND; + } +} + inline Node negateConjunctionAsClause(TNode conjunction){ Assert(conjunction.getKind() == kind::AND); NodeBuilder<> orBuilder(kind::OR); diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 7945b44c3..c2924f239 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -191,6 +191,11 @@ public: return !(*this <= other); } + int compare(const DeltaRational& other) const{ + int cmpRes = c.cmp(other.c); + return (cmpRes != 0) ? cmpRes : (k.cmp(other.k)); + } + DeltaRational& operator=(const DeltaRational& other){ c = other.c; k = other.k; diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp new file mode 100644 index 000000000..05a520d35 --- /dev/null +++ b/src/theory/arith/infer_bounds.cpp @@ -0,0 +1,319 @@ +/********************* */ +/*! \file infer_bounds.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "theory/arith/infer_bounds.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +using namespace inferbounds; + +InferBoundAlgorithm::InferBoundAlgorithm() + : d_alg(None) +{} + +InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a) + : d_alg(a) +{ + Assert(a != Simplex); +} + +InferBoundAlgorithm::InferBoundAlgorithm(const Maybe<int>& simplexRounds) + : d_alg(Simplex) +{} + +Algorithms InferBoundAlgorithm::getAlgorithm() const{ + return d_alg; +} + +const Maybe<int>& InferBoundAlgorithm::getSimplexRounds() const{ + Assert(getAlgorithm() == Simplex); + return d_simplexRounds; +} + + +InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){ + return InferBoundAlgorithm(Lookup); +} + +InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){ + return InferBoundAlgorithm(RowSum); +} + +InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe<int>& rounds){ + return InferBoundAlgorithm(rounds); +} + +ArithEntailmentCheckParameters::ArithEntailmentCheckParameters() + : EntailmentCheckParameters(theory::THEORY_ARITH) + , d_algorithms() +{} + +ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters() +{} + + +void ArithEntailmentCheckParameters::addLookupRowSumAlgorithms(){ + addAlgorithm(InferBoundAlgorithm::mkLookup()); + addAlgorithm(InferBoundAlgorithm::mkRowSum()); +} + +void ArithEntailmentCheckParameters::addAlgorithm(const inferbounds::InferBoundAlgorithm& alg){ + d_algorithms.push_back(alg); +} + +ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::begin() const{ + return d_algorithms.begin(); +} + +ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::end() const{ + return d_algorithms.end(); +} + + +// SimplexInferBoundsParameters::SimplexInferBoundsParameters() +// : d_parameter(1) +// , d_upperBound(true) +// , d_threshold() +// {} + +// SimplexInferBoundsParameters::~SimplexInferBoundsParameters(){} + + + +// int SimplexInferBoundsParameters::getSimplexRoundParameter() const { +// return d_parameter; +// } + +// bool SimplexInferBoundsParameters::findLowerBound() const { +// return ! findUpperBound(); +// } + +// bool SimplexInferBoundsParameters::findUpperBound() const { +// return d_upperBound; +// } + +// void SimplexInferBoundsParameters::setThreshold(const DeltaRational& th){ +// d_threshold = th; +// d_useThreshold = true; +// } + +// bool SimplexInferBoundsParameters::useThreshold() const{ +// return d_useThreshold; +// } + +// const DeltaRational& SimplexInferBoundsParameters::getThreshold() const{ +// return d_threshold; +// } + +// SimplexInferBoundsParameters::SimplexInferBoundsParameters(int p, bool ub) +// : d_parameter(p) +// , d_upperBound(ub) +// , d_useThreshold(false) +// , d_threshold() +// {} + + +InferBoundsResult::InferBoundsResult() + : d_foundBound(false) + , d_budgetExhausted(false) + , d_boundIsProvenOpt(false) + , d_inconsistentState(false) + , d_reachedThreshold(false) + , d_value(false) + , d_term(Node::null()) + , d_upperBound(true) + , d_explanation(Node::null()) +{} + +InferBoundsResult::InferBoundsResult(Node term, bool ub) + : d_foundBound(false) + , d_budgetExhausted(false) + , d_boundIsProvenOpt(false) + , d_inconsistentState(false) + , d_reachedThreshold(false) + , d_value(false) + , d_term(term) + , d_upperBound(ub) + , d_explanation(Node::null()) +{} + +bool InferBoundsResult::foundBound() const { + return d_foundBound; +} +bool InferBoundsResult::boundIsOptimal() const { + return d_boundIsProvenOpt; +} +bool InferBoundsResult::inconsistentState() const { + return d_inconsistentState; +} + +bool InferBoundsResult::boundIsInteger() const{ + return foundBound() && d_value.isIntegral(); +} + +bool InferBoundsResult::boundIsRational() const { + return foundBound() && d_value.infinitesimalIsZero(); +} + +Integer InferBoundsResult::valueAsInteger() const{ + Assert(boundIsInteger()); + return getValue().floor(); +} +const Rational& InferBoundsResult::valueAsRational() const{ + Assert(boundIsRational()); + return getValue().getNoninfinitesimalPart(); +} + +const DeltaRational& InferBoundsResult::getValue() const{ + return d_value; +} + +Node InferBoundsResult::getTerm() const { return d_term; } + +Node InferBoundsResult::getLiteral() const{ + const Rational& q = getValue().getNoninfinitesimalPart(); + NodeManager* nm = NodeManager::currentNM(); + Node qnode = nm->mkConst(q); + + Kind k; + if(d_upperBound){ + // x <= q + c*delta + Assert(getValue().infinitesimalSgn() <= 0); + k = boundIsRational() ? kind::LEQ : kind::LT; + }else{ + // x >= q + c*delta + Assert(getValue().infinitesimalSgn() >= 0); + k = boundIsRational() ? kind::GEQ : kind::GT; + } + Node atom = nm->mkNode(k, getTerm(), qnode); + Node lit = Rewriter::rewrite(atom); + return lit; +} + +/* If there is a bound, this is a node that explains the bound. */ +Node InferBoundsResult::getExplanation() const{ + return d_explanation; +} + + +void InferBoundsResult::setBound(const DeltaRational& dr, Node exp){ + d_foundBound = true; + d_value = dr; + d_explanation = exp; +} + +//bool InferBoundsResult::foundBound() const { return d_foundBound; } +//bool InferBoundsResult::boundIsOptimal() const { return d_boundIsProvenOpt; } +//bool InferBoundsResult::inconsistentState() const { return d_inconsistentState; } + + +void InferBoundsResult::setBudgetExhausted() { d_budgetExhausted = true; } +void InferBoundsResult::setReachedThreshold() { d_reachedThreshold = true; } +void InferBoundsResult::setIsOptimal() { d_boundIsProvenOpt = true; } +void InferBoundsResult::setInconsistent() { d_inconsistentState = true; } + +bool InferBoundsResult::thresholdWasReached() const{ + return d_reachedThreshold; +} +bool InferBoundsResult::budgetIsExhausted() const{ + return d_budgetExhausted; +} + +std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr){ + os << "{InferBoundsResult " << std::endl; + os << "on " << ibr.getTerm() << ", "; + if(ibr.findUpperBound()){ + os << "find upper bound, "; + }else{ + os << "find lower bound, "; + } + if(ibr.foundBound()){ + os << "found a bound: "; + if(ibr.boundIsInteger()){ + os << ibr.valueAsInteger() << "(int), "; + }else if(ibr.boundIsRational()){ + os << ibr.valueAsRational() << "(rat), "; + }else{ + os << ibr.getValue() << "(extended), "; + } + + os << "as term " << ibr.getLiteral() << ", "; + os << "explanation " << ibr.getExplanation() << ", "; + }else { + os << "did not find a bound, "; + } + + if(ibr.boundIsOptimal()){ + os << "(opt), "; + } + + if(ibr.inconsistentState()){ + os << "(inconsistent), "; + } + if(ibr.budgetIsExhausted()){ + os << "(budget exhausted), "; + } + if(ibr.thresholdWasReached()){ + os << "(reached threshold), "; + } + os << "}"; + return os; +} + + +ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects() + : EntailmentCheckSideEffects(theory::THEORY_ARITH) + , d_simplexSideEffects (NULL) +{} + +ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects(){ + if(d_simplexSideEffects != NULL){ + delete d_simplexSideEffects; + d_simplexSideEffects = NULL; + } +} + +InferBoundsResult& ArithEntailmentCheckSideEffects::getSimplexSideEffects(){ + if(d_simplexSideEffects == NULL){ + d_simplexSideEffects = new InferBoundsResult; + } + return *d_simplexSideEffects; +} + +namespace inferbounds { /* namespace arith */ + +std::ostream& operator<<(std::ostream& os, const Algorithms a){ + switch(a){ + case None: os << "AlgNone"; break; + case Lookup: os << "AlgLookup"; break; + case RowSum: os << "AlgRowSum"; break; + case Simplex: os << "AlgSimplex"; break; + default: + Unhandled(); + } + + return os; +} + +} /* namespace inferbounds */ + +} /* namespace arith */ +} /* namespace theory */ +} /* namespace CVC4 */ diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h new file mode 100644 index 000000000..55486080a --- /dev/null +++ b/src/theory/arith/infer_bounds.h @@ -0,0 +1,161 @@ +/********************* */ +/*! \file infer_bounds.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#pragma once + +#include "util/maybe.h" +#include "util/integer.h" +#include "util/rational.h" +#include "expr/node.h" +#include "theory/arith/delta_rational.h" +#include "theory/theory.h" +#include <ostream> + +namespace CVC4 { +namespace theory { +namespace arith { + +namespace inferbounds { + enum Algorithms {None = 0, Lookup, RowSum, Simplex}; + enum SimplexParamKind { Unbounded, NumVars, Direct}; + +class InferBoundAlgorithm { +private: + Algorithms d_alg; + Maybe<int> d_simplexRounds; + InferBoundAlgorithm(Algorithms a); + InferBoundAlgorithm(const Maybe<int>& simplexRounds); + +public: + InferBoundAlgorithm(); + + Algorithms getAlgorithm() const; + const Maybe<int>& getSimplexRounds() const; + + static InferBoundAlgorithm mkLookup(); + static InferBoundAlgorithm mkRowSum(); + static InferBoundAlgorithm mkSimplex(const Maybe<int>& rounds); +}; + +std::ostream& operator<<(std::ostream& os, const Algorithms a); +} /* namespace inferbounds */ + +class ArithEntailmentCheckParameters : public EntailmentCheckParameters { +private: + typedef std::vector<inferbounds::InferBoundAlgorithm> VecInferBoundAlg; + VecInferBoundAlg d_algorithms; + +public: + typedef VecInferBoundAlg::const_iterator const_iterator; + + ArithEntailmentCheckParameters(); + ~ArithEntailmentCheckParameters(); + + void addLookupRowSumAlgorithms(); + void addAlgorithm(const inferbounds::InferBoundAlgorithm& alg); + + const_iterator begin() const; + const_iterator end() const; +}; + + + +class InferBoundsResult { +public: + InferBoundsResult(); + InferBoundsResult(Node term, bool ub); + + void setBound(const DeltaRational& dr, Node exp); + bool foundBound() const; + + void setIsOptimal(); + bool boundIsOptimal() const; + + void setInconsistent(); + bool inconsistentState() const; + + const DeltaRational& getValue() const; + bool boundIsRational() const; + const Rational& valueAsRational() const; + bool boundIsInteger() const; + Integer valueAsInteger() const; + + Node getTerm() const; + Node getLiteral() const; + void setTerm(Node t){ d_term = t; } + + /* If there is a bound, this is a node that explains the bound. */ + Node getExplanation() const; + + bool budgetIsExhausted() const; + void setBudgetExhausted(); + + bool thresholdWasReached() const; + void setReachedThreshold(); + + bool findUpperBound() const { return d_upperBound; } + + void setFindLowerBound() { d_upperBound = false; } + void setFindUpperBound() { d_upperBound = true; } +private: + /* was a bound found */ + bool d_foundBound; + + /* was the budget exhausted */ + bool d_budgetExhausted; + + /* does the bound have to be optimal*/ + bool d_boundIsProvenOpt; + + /* was this started on an inconsistent state. */ + bool d_inconsistentState; + + /* reached the threshold. */ + bool d_reachedThreshold; + + /* the value of the bound */ + DeltaRational d_value; + + /* The input term. */ + Node d_term; + + /* Was the bound found an upper or lower bound.*/ + bool d_upperBound; + + /* Explanation of the bound. */ + Node d_explanation; +}; + +std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr); + +class ArithEntailmentCheckSideEffects : public EntailmentCheckSideEffects{ +public: + ArithEntailmentCheckSideEffects(); + ~ArithEntailmentCheckSideEffects(); + + InferBoundsResult& getSimplexSideEffects(); + +private: + InferBoundsResult* d_simplexSideEffects; +}; + + +} /* namespace arith */ +} /* namespace theory */ +} /* namespace CVC4 */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 960a5a066..74453d985 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -17,6 +17,7 @@ #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" +#include "theory/arith/infer_bounds.h" using namespace std; using namespace CVC4::kind; @@ -100,6 +101,43 @@ Node TheoryArith::getModelValue(TNode var) { return d_internal->getModelValue( var ); } + +std::pair<bool, Node> TheoryArith::entailmentCheck (TNode lit, + const EntailmentCheckParameters* params, + EntailmentCheckSideEffects* out) +{ + const ArithEntailmentCheckParameters* aparams = NULL; + if(params == NULL){ + ArithEntailmentCheckParameters* def = new ArithEntailmentCheckParameters(); + def->addLookupRowSumAlgorithms(); + aparams = def; + }else{ + AlwaysAssert(params->getTheoryId() == getId()); + aparams = dynamic_cast<const ArithEntailmentCheckParameters*>(params); + } + Assert(aparams != NULL); + + ArithEntailmentCheckSideEffects* ase = NULL; + if(out == NULL){ + ase = new ArithEntailmentCheckSideEffects(); + }else{ + AlwaysAssert(out->getTheoryId() == getId()); + ase = dynamic_cast<ArithEntailmentCheckSideEffects*>(out); + } + Assert(ase != NULL); + + std::pair<bool, Node> res = d_internal->entailmentCheck(lit, *aparams, *ase); + + if(params == NULL){ + delete aparams; + } + if(out == NULL){ + delete ase; + } + + return res; +} + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index eaa9a98c6..56a8d9b60 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -21,6 +21,7 @@ #include "expr/node.h" #include "theory/arith/theory_arith_private_forward.h" + namespace CVC4 { namespace theory { @@ -79,6 +80,12 @@ public: void addSharedTerm(TNode n); Node getModelValue(TNode var); + + + std::pair<bool, Node> entailmentCheck(TNode lit, + const EntailmentCheckParameters* params, + EntailmentCheckSideEffects* out); + };/* class TheoryArith */ }/* CVC4::theory::arith namespace */ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index b0e66b564..efc93e26f 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -121,16 +121,21 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_tableauResetDensity(1.6), d_tableauResetPeriod(10), d_conflicts(c), + d_blackBoxConflict(c, Node::null()), d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseConflict(*this, d_conflictBuffer)), d_cmEnabled(c, true), + d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)), d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)), d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)), d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)), + d_pass1SDP(NULL), d_otherSDP(NULL), d_lastContextIntegerAttempted(c,-1), + + d_DELTA_ZERO(0), d_approxCuts(c), d_fullCheckCounter(0), @@ -1822,10 +1827,6 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(){ Assert(!done()); TNode assertion = get(); - if( options::finiteModelFind() && d_quantEngine && d_quantEngine->getBoundedIntegers() ){ - d_quantEngine->getBoundedIntegers()->assertNode(assertion); - } - Kind simpleKind = Comparison::comparisonKind(assertion); ConstraintP constraint = d_constraintDatabase.lookup(assertion); if(constraint == NullConstraint){ @@ -4621,6 +4622,7 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{ return d_rowTracking[ridx]; } + Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) { NodeManager* nm = NodeManager::currentNM(); @@ -4684,6 +4686,900 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) } + + +// InferBoundsResult TheoryArithPrivate::inferBound(TNode term, const InferBoundsParameters& param){ +// Node t = Rewriter::rewrite(term); +// Assert(Polynomial::isMember(t)); +// Polynomial p = Polynomial::parsePolynomial(t); +// if(p.containsConstant()){ +// Constant c = p.getHead().getConstant(); +// if(p.isConstant()){ +// InferBoundsResult res(t, param.findLowerBound()); +// res.setBound((DeltaRational)c.getValue(), mkBoolNode(true)); +// return res; +// }else{ +// Polynomial tail = p.getTail(); +// InferBoundsResult res = inferBound(tail.getNode(), param); +// if(res.foundBound()){ +// DeltaRational newBound = res.getValue() + c.getValue(); +// if(tail.isIntegral()){ +// Integer asInt = (param.findLowerBound()) ? newBound.ceiling() : newBound.floor(); +// newBound = DeltaRational(asInt); +// } +// res.setBound(newBound, res.getExplanation()); +// } +// return res; +// } +// }else if(param.findLowerBound()){ +// InferBoundsParameters find_ub = param; +// find_ub.setFindUpperBound(); +// if(param.useThreshold()){ +// find_ub.setThreshold(- param.getThreshold() ); +// } +// Polynomial negP = -p; +// InferBoundsResult res = inferBound(negP.getNode(), find_ub); +// res.setFindLowerBound(); +// if(res.foundBound()){ +// res.setTerm(p.getNode()); +// res.setBound(-res.getValue(), res.getExplanation()); +// } +// return res; +// }else{ +// Assert(param.findUpperBound()); +// // does not contain a constant +// switch(param.getEffort()){ +// case InferBoundsParameters::Lookup: +// return inferUpperBoundLookup(t, param); +// case InferBoundsParameters::Simplex: +// return inferUpperBoundSimplex(t, param); +// case InferBoundsParameters::LookupAndSimplexOnFailure: +// case InferBoundsParameters::TryBoth: +// { +// InferBoundsResult lookup = inferUpperBoundLookup(t, param); +// if(lookup.foundBound()){ +// if(param.getEffort() == InferBoundsParameters::LookupAndSimplexOnFailure || +// lookup.boundIsOptimal()){ +// return lookup; +// } +// } +// InferBoundsResult simplex = inferUpperBoundSimplex(t, param); +// if(lookup.foundBound() && simplex.foundBound()){ +// return (lookup.getValue() <= simplex.getValue()) ? lookup : simplex; +// }else if(lookup.foundBound()){ +// return lookup; +// }else{ +// return simplex; +// } +// } +// default: +// Unreachable(); +// return InferBoundsResult(); +// } +// } +// } + + +std::pair<bool, Node> TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){ + using namespace inferbounds; + + // l k r + // diff : (l - r) k 0 + Debug("arith::entailCheck") << "TheoryArithPrivate::entailmentCheck(" << lit << ")"<< endl; + Kind k; + int primDir; + Rational lm, rm, dm; + Node lp, rp, dp; + DeltaRational sep; + bool successful = decomposeLiteral(lit, k, primDir, lm, lp, rm, rp, dm, dp, sep); + if(!successful) { return make_pair(false, Node::null()); } + + if(dp.getKind() == CONST_RATIONAL){ + Node eval = Rewriter::rewrite(lit); + Assert(eval.getKind() == kind::CONST_BOOLEAN); + // if true, true is an acceptable explaination + // if false, the node is uninterpreted and eval can be forgotten + return make_pair(eval.getConst<bool>(), eval); + } + Assert(dm != Rational(0)); + Assert(primDir == 1 || primDir == -1); + + int negPrim = -primDir; + + int secDir = (k == EQUAL || k == DISTINCT) ? negPrim: 0; + int negSecDir = (k == EQUAL || k == DISTINCT) ? primDir: 0; + + // primDir*[lm*( lp )] k primDir*[ [rm*( rp )] + sep ] + // primDir*[lm*( lp ) - rm*( rp ) ] k primDir*sep + // primDir*[dm * dp] k primDir*sep + + std::pair<Node, DeltaRational> bestPrimLeft, bestNegPrimRight, bestPrimDiff, tmp; + std::pair<Node, DeltaRational> bestSecLeft, bestNegSecRight, bestSecDiff; + bestPrimLeft.first = Node::null(); bestNegPrimRight.first = Node::null(); bestPrimDiff.first = Node::null(); + bestSecLeft.first = Node::null(); bestNegSecRight.first = Node::null(); bestSecDiff.first = Node::null(); + + + + ArithEntailmentCheckParameters::const_iterator alg, alg_end; + for( alg = params.begin(), alg_end = params.end(); alg != alg_end; ++alg ){ + const inferbounds::InferBoundAlgorithm& ibalg = *alg; + + Debug("arith::entailCheck") << "entailmentCheck trying " << (inferbounds::Algorithms) ibalg.getAlgorithm() << endl; + switch(ibalg.getAlgorithm()){ + case inferbounds::None: + break; + case inferbounds::Lookup: + case inferbounds::RowSum: + { + typedef void (TheoryArithPrivate::*EntailmentCheckFunc)(std::pair<Node, DeltaRational>&, int, TNode) const; + + EntailmentCheckFunc ecfunc = + (ibalg.getAlgorithm() == inferbounds::Lookup) + ? (&TheoryArithPrivate::entailmentCheckBoundLookup) + : (&TheoryArithPrivate::entailmentCheckRowSum); + + (*this.*ecfunc)(tmp, primDir * lm.sgn(), lp); + setToMin(primDir * lm.sgn(), bestPrimLeft, tmp); + + (*this.*ecfunc)(tmp, negPrim * rm.sgn(), rp); + setToMin(negPrim * rm.sgn(), bestNegPrimRight, tmp); + + (*this.*ecfunc)(tmp, secDir * lm.sgn(), lp); + setToMin(secDir * lm.sgn(), bestSecLeft, tmp); + + (*this.*ecfunc)(tmp, negSecDir * rm.sgn(), rp); + setToMin(negSecDir * rm.sgn(), bestNegSecRight, tmp); + + (*this.*ecfunc)(tmp, primDir * dm.sgn(), dp); + setToMin(primDir * dm.sgn(), bestPrimDiff, tmp); + + (*this.*ecfunc)(tmp, secDir * dm.sgn(), dp); + setToMin(secDir * dm.sgn(), bestSecDiff, tmp); + } + break; + case inferbounds::Simplex: + { + // primDir * diffm * diff < c or primDir * diffm * diff > c + tmp = entailmentCheckSimplex(primDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects()); + setToMin(primDir * dm.sgn(), bestPrimDiff, tmp); + + tmp = entailmentCheckSimplex(secDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects()); + setToMin(secDir * dm.sgn(), bestSecDiff, tmp); + } + break; + default: + Unhandled(); + } + + // turn bounds on prim * left and -prim * right into bounds on prim * diff + if(!bestPrimLeft.first.isNull() && !bestNegPrimRight.first.isNull()){ + // primDir*lm* lp <= primDir*lm*L + // -primDir*rm* rp <= -primDir*rm*R + // primDir*lm* lp -primDir*rm* rp <= primDir*lm*L - primDir*rm*R + // primDir [lm* lp -rm* rp] <= primDir[lm*L - *rm*R] + // primDir [dm * dp] <= primDir[lm*L - *rm*R] + // primDir [dm * dp] <= primDir * dm * ([lm*L - *rm*R]/dm) + tmp.second = ((bestPrimLeft.second * lm) - (bestNegPrimRight.second * rm)) / dm; + tmp.first = (bestPrimLeft.first).andNode(bestNegPrimRight.first); + setToMin(primDir, bestPrimDiff, tmp); + } + + // turn bounds on sec * left and sec * right into bounds on sec * diff + if(secDir != 0 && !bestSecLeft.first.isNull() && !bestNegSecRight.first.isNull()){ + // secDir*lm* lp <= secDir*lm*L + // -secDir*rm* rp <= -secDir*rm*R + // secDir*lm* lp -secDir*rm* rp <= secDir*lm*L - secDir*rm*R + // secDir [lm* lp -rm* rp] <= secDir[lm*L - *rm*R] + // secDir [dm * dp] <= secDir[lm*L - *rm*R] + // secDir [dm * dp] <= secDir * dm * ([lm*L - *rm*R]/dm) + tmp.second = ((bestSecLeft.second * lm) - (bestNegSecRight.second * rm)) / dm; + tmp.first = (bestSecLeft.first).andNode(bestNegSecRight.first); + setToMin(secDir, bestSecDiff, tmp); + } + + switch(k){ + case LEQ: + if(!bestPrimDiff.first.isNull()){ + DeltaRational d = (bestPrimDiff.second * dm); + if((primDir > 0 && d <= sep) || (primDir < 0 && d >= sep) ){ + Debug("arith::entailCheck") << "entailmentCheck found " + << primDir << "*" << dm << "*(" << dp<<")" + << " <= " << primDir << "*" << dm << "*" << bestPrimDiff.second + << " <= " << primDir << "*" << sep << endl + << " by " << bestPrimDiff.first << endl; + Assert(bestPrimDiff.second * (Rational(primDir)* dm) <= (sep * Rational(primDir))); + return make_pair(true, bestPrimDiff.first); + } + } + break; + case EQUAL: + if(!bestPrimDiff.first.isNull() && !bestSecDiff.first.isNull()){ + // Is primDir [dm * dp] == primDir * sep entailed? + // Iff [dm * dp] == sep entailed? + // Iff dp == sep / dm entailed? + // Iff dp <= sep / dm and dp >= sep / dm entailed? + + // primDir [dm * dp] <= primDir * dm * U + // secDir [dm * dp] <= secDir * dm * L + + // Suppose primDir * dm > 0 + // then secDir * dm < 0 + // dp >= (secDir * L) / secDir * dm + // dp >= (primDir * L) / primDir * dm + // + // dp <= U / dm + // dp >= L / dm + // dp == sep / dm entailed iff U == L == sep + // Suppose primDir * dm < 0 + // then secDir * dm > 0 + // dp >= U / dm + // dp <= L / dm + // dp == sep / dm entailed iff U == L == sep + if(bestPrimDiff.second == bestSecDiff.second){ + if(bestPrimDiff.second == sep){ + return make_pair(true, (bestPrimDiff.first).andNode(bestSecDiff.first)); + } + } + } + // intentionally fall through to DISTINCT case! + // entailments of negations are eager exit cases for EQUAL + case DISTINCT: + if(!bestPrimDiff.first.isNull()){ + // primDir [dm * dp] <= primDir * dm * U < primDir * sep + if((primDir > 0 && (bestPrimDiff.second * dm < sep)) || + (primDir < 0 && (bestPrimDiff.second * dm > sep))){ + // entailment of negation + if(k == DISTINCT){ + return make_pair(true, bestPrimDiff.first); + }else{ + Assert(k == EQUAL); + return make_pair(false, Node::null()); + } + } + } + if(!bestSecDiff.first.isNull()){ + // If primDir [dm * dp] > primDir * sep, then this is not entailed. + // If primDir [dm * dp] >= primDir * dm * L > primDir * sep + // -primDir * dm * L < -primDir * sep + // secDir * dm * L < secDir * sep + if((secDir > 0 && (bestSecDiff.second * dm < sep)) || + (secDir < 0 && (bestSecDiff.second * dm > sep))){ + if(k == DISTINCT){ + return make_pair(true, bestSecDiff.first); + }else{ + Assert(k == EQUAL); + return make_pair(false, Node::null()); + } + } + } + + break; + default: + Unreachable(); + break; + } + } + return make_pair(false, Node::null()); +} + +bool TheoryArithPrivate::decomposeTerm(Node term, Rational& m, Node& p, Rational& c){ + Node t = Rewriter::rewrite(term); + if(!Polynomial::isMember(t)){ + return false; + } +#warning "DO NOT LET INTO TRUNK!" + ContainsTermITEVisitor ctv; + if(ctv.containsTermITE(t)){ + return false; + } + + Polynomial poly = Polynomial::parsePolynomial(t); + if(poly.isConstant()){ + c = poly.getHead().getConstant().getValue(); + p = mkRationalNode(Rational(0)); + m = Rational(1); + return true; + }else if(poly.containsConstant()){ + c = poly.getHead().getConstant().getValue(); + poly = poly.getTail(); + }else{ + c = Rational(0); + } + Assert(!poly.isConstant()); + Assert(!poly.containsConstant()); + + const bool intVars = poly.allIntegralVariables(); + + if(intVars){ + m = Rational(1); + if(!poly.isIntegral()){ + Integer denom = poly.denominatorLCM(); + m /= denom; + poly = poly * denom; + } + Integer g = poly.gcd(); + m *= g; + poly = poly * Rational(1,g); + Assert(poly.isIntegral()); + Assert(poly.leadingCoefficientIsPositive()); + }else{ + Assert(!intVars); + m = poly.getHead().getConstant().getValue(); + poly = poly * m.inverse(); + Assert(poly.leadingCoefficientIsAbsOne()); + } + p = poly.getNode(); + return true; +} + +void TheoryArithPrivate::setToMin(int sgn, std::pair<Node, DeltaRational>& min, const std::pair<Node, DeltaRational>& e){ + if(sgn != 0){ + if(min.first.isNull() && !e.first.isNull()){ + min = e; + }else if(!min.first.isNull() && !e.first.isNull()){ + if(sgn > 0 && min.second > e.second){ + min = e; + }else if(sgn < 0 && min.second < e.second){ + min = e; + } + } + } +} + +// std::pair<bool, Node> TheoryArithPrivate::entailmentUpperCheck(const Rational& lm, Node lp, const Rational& rm, Node rp, const DeltaRational& sep, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){ + +// Rational negRM = -rm; +// Node diff = NodeManager::currentNM()->mkNode(MULT, mkRationalConstan(lm), lp) + (negRM * rp); + +// Rational diffm; +// Node diffp; +// decompose(diff, diffm, diffNode); + + +// std::pair<Node, DeltaRational> bestUbLeft, bestLbRight, bestUbDiff, tmp; +// bestUbLeft = bestLbRight = bestUbDiff = make_pair(Node::Null(), DeltaRational()); + +// return make_pair(false, Node::null()); +// } + +/** + * Decomposes a literal into the form: + * dir*[lm*( lp )] k dir*[ [rm*( rp )] + sep ] + * dir*[dm* dp] k dir *sep + * dir is either 1 or -1 + */ +bool TheoryArithPrivate::decomposeLiteral(Node lit, Kind& k, int& dir, Rational& lm, Node& lp, Rational& rm, Node& rp, Rational& dm, Node& dp, DeltaRational& sep){ + bool negated = (lit.getKind() == kind::NOT); + TNode atom = negated ? lit[0] : lit; + + TNode left = atom[0]; + TNode right = atom[1]; + + // left : lm*( lp ) + lc + // right: rm*( rp ) + rc + Rational lc, rc; + bool success = decomposeTerm(left, lm, lp, lc); + if(!success){ return false; } + success = decomposeTerm(right, rm, rp, rc); + if(!success){ return false; } + + Node diff = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::MINUS, left, right)); + Rational dc; + success = decomposeTerm(diff, dm, dp, dc); + Assert(success); + + // reduce the kind of the to not include literals + // GT, NOT LEQ + // GEQ, NOT LT + // LT, NOT GEQ + // LEQ, NOT LT + Kind atomKind = atom.getKind(); + Kind normKind = negated ? negateKind(atomKind) : atomKind; + + if(normKind == GEQ || normKind == GT){ + dir = -1; + normKind = (normKind == GEQ) ? LEQ : LT; + }else{ + dir = 1; + } + + Debug("arith::decomp") << "arith::decomp " + << lit << "(" << normKind << "*" << dir << ")"<< endl + << " left:" << lc << " + " << lm << "*(" << lp << ") : " <<left << endl + << " right:" << rc << " + " << rm << "*(" << rp << ") : " << right << endl + << " diff: " << dc << " + " << dm << "*("<< dp <<"): " << diff << endl + << " sep: " << sep << endl; + + + // k in LT, LEQ, EQUAL, DISEQUAL + // [dir*lm*( lp ) + dir*lc] k [dir*rm*( rp ) + dir*rc] + Rational change = rc - lc; + Assert(change == (-dc)); + // [dir*lm*( lp )] k [dir*rm*( rp ) + dir*(rc - lc)] + if(normKind == LT){ + sep = DeltaRational(change, Rational(-1)); + k = LEQ; + }else{ + sep = DeltaRational(change); + k = normKind; + } + // k in LEQ, EQUAL, DISEQUAL + // dir*lm*( lp ) k [dir*rm*( rp )] + dir*(sep + d * delta) + return true; +} + +/** + * Precondition: + * tp is a polynomial not containing an ite. + * either tp is constant or contains no constants. + * Post: + * if tmp.first is not null, then + * sgn * tp <= sgn * tmp.second + */ +void TheoryArithPrivate::entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const { + tmp.first = Node::null(); + if(sgn == 0){ return; } + + Assert(Polynomial::isMember(tp)); + if(tp.getKind() == CONST_RATIONAL){ + tmp.first = mkBoolNode(true); + tmp.second = DeltaRational(tp.getConst<Rational>()); + }else if(d_partialModel.hasArithVar(tp)){ + Assert(tp.getKind() != CONST_RATIONAL); + ArithVar v = d_partialModel.asArithVar(tp); + Assert(v != ARITHVAR_SENTINEL); + ConstraintP c = (sgn > 0) + ? d_partialModel.getUpperBoundConstraint(v) + : d_partialModel.getLowerBoundConstraint(v); + if(c != NullConstraint){ + tmp.first = c->externalExplainByAssertions(); + tmp.second = c->getValue(); + } + } +} + +void TheoryArithPrivate::entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const { + tmp.first = Node::null(); + if(sgn == 0){ return; } + if(tp.getKind() != PLUS){ return; } + Assert(Polynomial::isMember(tp)); + + tmp.second = DeltaRational(0); + NodeBuilder<> nb(kind::AND); + + Polynomial p = Polynomial::parsePolynomial(tp); + for(Polynomial::iterator i = p.begin(), iend = p.end(); i != iend; ++i) { + Monomial m = *i; + Node x = m.getVarList().getNode(); + if(d_partialModel.hasArithVar(x)){ + ArithVar v = d_partialModel.asArithVar(x); + const Rational& coeff = m.getConstant().getValue(); + int dir = sgn * coeff.sgn(); + ConstraintP c = (dir > 0) + ? d_partialModel.getUpperBoundConstraint(v) + : d_partialModel.getLowerBoundConstraint(v); + if(c != NullConstraint){ + tmp.second += c->getValue() * coeff; + c->externalExplainByAssertions(nb); + }else{ + //failed + return; + } + }else{ + // failed + return; + } + } + // success + tmp.first = nb; +} + +std::pair<Node, DeltaRational> TheoryArithPrivate::entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& param, InferBoundsResult& result){ + + if((sgn == 0) || !(d_qflraStatus == Result::SAT && d_errorSet.noSignals()) || tp.getKind() == CONST_RATIONAL){ + return make_pair(Node::null(), DeltaRational()); + } + + Assert(d_qflraStatus == Result::SAT); + Assert(d_errorSet.noSignals()); + Assert(param.getAlgorithm() == inferbounds::Simplex); + + // TODO Move me into a new file + + enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds}; + ResultState finalState = Unset; + + int maxRounds = param.getSimplexRounds().just() + ? param.getSimplexRounds().constValue() + : -1; + + Maybe<DeltaRational> threshold; + // TODO: get this from the parameters + + // setup term + Polynomial p = Polynomial::parsePolynomial(tp); + vector<ArithVar> variables; + vector<Rational> coefficients; + asVectors(p, coefficients, variables); + if(sgn < 0){ + for(size_t i=0, N=coefficients.size(); i < N; ++i){ + coefficients[i] = -coefficients[i]; + } + } + // implicitly an upperbound + Node skolem = mkRealSkolem("tmpVar$$"); + ArithVar optVar = requestArithVar(skolem, false, true); + d_tableau.addRow(optVar, coefficients, variables); + RowIndex ridx = d_tableau.basicToRowIndex(optVar); + + DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false); + d_partialModel.setAssignment(optVar, newAssignment); + d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar)); + + // Setup simplex + d_partialModel.stopQueueingBoundCounts(); + UpdateTrackingCallback utcb(&d_linEq); + d_partialModel.processBoundsQueue(utcb); + d_linEq.startTrackingBoundCounts(); + + // maximize optVar via primal Simplex + int rounds = 0; + while(finalState == Unset){ + ++rounds; + if(maxRounds >= 0 && rounds > maxRounds){ + finalState = ExhaustedRounds; + break; + } + + // select entering by bland's rule + // TODO improve upon bland's + ArithVar entering = ARITHVAR_SENTINEL; + const Tableau::Entry* enteringEntry = NULL; + for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ + const Tableau::Entry& entry = *ri; + ArithVar v = entry.getColVar(); + if(v != optVar){ + int sgn = entry.getCoefficient().sgn(); + Assert(sgn != 0); + bool candidate = (sgn > 0) + ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) + : (d_partialModel.cmpAssignmentLowerBound(v) != 0); + if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){ + entering = v; + enteringEntry = &entry; + } + } + } + if(entering == ARITHVAR_SENTINEL){ + finalState = Inferred; + break; + } + Assert(entering != ARITHVAR_SENTINEL); + Assert(enteringEntry != NULL); + + int esgn = enteringEntry->getCoefficient().sgn(); + Assert(esgn != 0); + + // select leaving and ratio + ArithVar leaving = ARITHVAR_SENTINEL; + DeltaRational minRatio; + const Tableau::Entry* pivotEntry = NULL; + + // Special case check the upper/lowerbound on entering + ConstraintP cOnEntering = (esgn > 0) + ? d_partialModel.getUpperBoundConstraint(entering) + : d_partialModel.getLowerBoundConstraint(entering); + if(cOnEntering != NullConstraint){ + leaving = entering; + minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue(); + } + for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){ + const Tableau::Entry& centry = *ci; + ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex()); + int csgn = centry.getCoefficient().sgn(); + int basicDir = csgn * esgn; + + ConstraintP bound = (basicDir > 0) + ? d_partialModel.getUpperBoundConstraint(basic) + : d_partialModel.getLowerBoundConstraint(basic); + if(bound != NullConstraint){ + DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue(); + DeltaRational ratio = diff/(centry.getCoefficient()); + bool selected = false; + if(leaving == ARITHVAR_SENTINEL){ + selected = true; + }else{ + int cmp = ratio.compare(minRatio); + if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){ + selected = (cmp != 0) || + ((leaving != entering) && (basic < leaving)); + } + } + if(selected){ + leaving = basic; + minRatio = ratio; + pivotEntry = ¢ry; + } + } + } + + + if(leaving == ARITHVAR_SENTINEL){ + finalState = NoBound; + break; + }else if(leaving == entering){ + d_linEq.update(entering, minRatio); + }else{ + DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient()); + d_linEq.pivotAndUpdate(leaving, entering, newLeaving); + // no conflicts clear signals + Assert(d_errorSet.noSignals()); + } + + if(threshold.just()){ + if(d_partialModel.getAssignment(optVar) >= threshold.constValue()){ + finalState = ReachedThreshold; + break; + } + } + }; + + result = InferBoundsResult(tp, sgn > 0); + + // tear down term + switch(finalState){ + case Inferred: + { + NodeBuilder<> nb(kind::AND); + for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ + const Tableau::Entry& e =*ri; + ArithVar colVar = e.getColVar(); + if(colVar != optVar){ + const Rational& q = e.getCoefficient(); + Assert(q.sgn() != 0); + ConstraintP c = (q.sgn() > 0) + ? d_partialModel.getUpperBoundConstraint(colVar) + : d_partialModel.getLowerBoundConstraint(colVar); + c->externalExplainByAssertions(nb); + } + } + Assert(nb.getNumChildren() >= 1); + Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0]; + result.setBound(d_partialModel.getAssignment(optVar), exp); + result.setIsOptimal(); + break; + } + case NoBound: + break; + case ReachedThreshold: + result.setReachedThreshold(); + break; + case ExhaustedRounds: + result.setBudgetExhausted(); + break; + case Unset: + default: + Unreachable(); + break; + }; + + d_linEq.stopTrackingRowIndex(ridx); + d_tableau.removeBasicRow(optVar); + releaseArithVar(optVar); + + d_linEq.stopTrackingBoundCounts(); + d_partialModel.startQueueingBoundCounts(); + + if(result.foundBound()){ + return make_pair(result.getExplanation(), result.getValue()); + }else{ + return make_pair(Node::null(), DeltaRational()); + } +} + +// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const inferbounds::InferBoundAlgorithm& param){ +// Assert(param.findUpperBound()); + +// if(!(d_qflraStatus == Result::SAT && d_errorSet.noSignals())){ +// InferBoundsResult inconsistent; +// inconsistent.setInconsistent(); +// return inconsistent; +// } + +// Assert(d_qflraStatus == Result::SAT); +// Assert(d_errorSet.noSignals()); + +// // TODO Move me into a new file + +// enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds}; +// ResultState finalState = Unset; + +// int maxRounds = 0; +// switch(param.getParamKind()){ +// case InferBoundsParameters::Unbounded: +// maxRounds = -1; +// break; +// case InferBoundsParameters::NumVars: +// maxRounds = d_partialModel.getNumberOfVariables() * param.getSimplexRoundParameter(); +// break; +// case InferBoundsParameters::Direct: +// maxRounds = param.getSimplexRoundParameter(); +// break; +// default: maxRounds = 0; break; +// } + +// // setup term +// Polynomial p = Polynomial::parsePolynomial(t); +// vector<ArithVar> variables; +// vector<Rational> coefficients; +// asVectors(p, coefficients, variables); + +// Node skolem = mkRealSkolem("tmpVar$$"); +// ArithVar optVar = requestArithVar(skolem, false, true); +// d_tableau.addRow(optVar, coefficients, variables); +// RowIndex ridx = d_tableau.basicToRowIndex(optVar); + +// DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false); +// d_partialModel.setAssignment(optVar, newAssignment); +// d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar)); + +// // Setup simplex +// d_partialModel.stopQueueingBoundCounts(); +// UpdateTrackingCallback utcb(&d_linEq); +// d_partialModel.processBoundsQueue(utcb); +// d_linEq.startTrackingBoundCounts(); + +// // maximize optVar via primal Simplex +// int rounds = 0; +// while(finalState == Unset){ +// ++rounds; +// if(maxRounds >= 0 && rounds > maxRounds){ +// finalState = ExhaustedRounds; +// break; +// } + +// // select entering by bland's rule +// // TODO improve upon bland's +// ArithVar entering = ARITHVAR_SENTINEL; +// const Tableau::Entry* enteringEntry = NULL; +// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ +// const Tableau::Entry& entry = *ri; +// ArithVar v = entry.getColVar(); +// if(v != optVar){ +// int sgn = entry.getCoefficient().sgn(); +// Assert(sgn != 0); +// bool candidate = (sgn > 0) +// ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) +// : (d_partialModel.cmpAssignmentLowerBound(v) != 0); +// if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){ +// entering = v; +// enteringEntry = &entry; +// } +// } +// } +// if(entering == ARITHVAR_SENTINEL){ +// finalState = Inferred; +// break; +// } +// Assert(entering != ARITHVAR_SENTINEL); +// Assert(enteringEntry != NULL); + +// int esgn = enteringEntry->getCoefficient().sgn(); +// Assert(esgn != 0); + +// // select leaving and ratio +// ArithVar leaving = ARITHVAR_SENTINEL; +// DeltaRational minRatio; +// const Tableau::Entry* pivotEntry = NULL; + +// // Special case check the upper/lowerbound on entering +// ConstraintP cOnEntering = (esgn > 0) +// ? d_partialModel.getUpperBoundConstraint(entering) +// : d_partialModel.getLowerBoundConstraint(entering); +// if(cOnEntering != NullConstraint){ +// leaving = entering; +// minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue(); +// } +// for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){ +// const Tableau::Entry& centry = *ci; +// ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex()); +// int csgn = centry.getCoefficient().sgn(); +// int basicDir = csgn * esgn; + +// ConstraintP bound = (basicDir > 0) +// ? d_partialModel.getUpperBoundConstraint(basic) +// : d_partialModel.getLowerBoundConstraint(basic); +// if(bound != NullConstraint){ +// DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue(); +// DeltaRational ratio = diff/(centry.getCoefficient()); +// bool selected = false; +// if(leaving == ARITHVAR_SENTINEL){ +// selected = true; +// }else{ +// int cmp = ratio.compare(minRatio); +// if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){ +// selected = (cmp != 0) || +// ((leaving != entering) && (basic < leaving)); +// } +// } +// if(selected){ +// leaving = basic; +// minRatio = ratio; +// pivotEntry = ¢ry; +// } +// } +// } + + +// if(leaving == ARITHVAR_SENTINEL){ +// finalState = NoBound; +// break; +// }else if(leaving == entering){ +// d_linEq.update(entering, minRatio); +// }else{ +// DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient()); +// d_linEq.pivotAndUpdate(leaving, entering, newLeaving); +// // no conflicts clear signals +// Assert(d_errorSet.noSignals()); +// } + +// if(param.useThreshold()){ +// if(d_partialModel.getAssignment(optVar) >= param.getThreshold()){ +// finalState = ReachedThreshold; +// break; +// } +// } +// }; + +// InferBoundsResult result(t, param.findUpperBound()); + +// // tear down term +// switch(finalState){ +// case Inferred: +// { +// NodeBuilder<> nb(kind::AND); +// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ +// const Tableau::Entry& e =*ri; +// ArithVar colVar = e.getColVar(); +// if(colVar != optVar){ +// const Rational& q = e.getCoefficient(); +// Assert(q.sgn() != 0); +// ConstraintP c = (q.sgn() > 0) +// ? d_partialModel.getUpperBoundConstraint(colVar) +// : d_partialModel.getLowerBoundConstraint(colVar); +// c->externalExplainByAssertions(nb); +// } +// } +// Assert(nb.getNumChildren() >= 1); +// Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0]; +// result.setBound(d_partialModel.getAssignment(optVar), exp); +// result.setIsOptimal(); +// break; +// } +// case NoBound: +// break; +// case ReachedThreshold: +// result.setReachedThreshold(); +// break; +// case ExhaustedRounds: +// result.setBudgetExhausted(); +// break; +// case Unset: +// default: +// Unreachable(); +// break; +// }; + +// d_linEq.stopTrackingRowIndex(ridx); +// d_tableau.removeBasicRow(optVar); +// releaseArithVar(optVar); + +// d_linEq.stopTrackingBoundCounts(); +// d_partialModel.startQueueingBoundCounts(); + +// return result; +// } + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 68e839ef8..5e7943e5e 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -64,6 +64,7 @@ #include "theory/arith/arith_utilities.h" #include "theory/arith/delta_rational.h" +#include "theory/arith/infer_bounds.h" #include "theory/arith/partial_model.h" #include "theory/arith/matrix.h" @@ -92,6 +93,13 @@ class BranchCutInfo; class TreeLog; class ApproximateStatistics; +class ArithEntailmentCheckParameters; +class ArithEntailmentCheckSideEffects; +namespace inferbounds { + class InferBoundAlgorithm; +} +class InferBoundsResult; + /** * Implementation of QF_LRA. * Based upon: @@ -146,7 +154,42 @@ public: void releaseArithVar(ArithVar v); void signal(ArithVar v){ d_errorSet.signalVariable(v); } + private: + // t does not contain constants + void entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const; + void entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const; + + std::pair<Node, DeltaRational> entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& p, InferBoundsResult& out); + + //InferBoundsResult inferBound(TNode term, const InferBoundsParameters& p); + //InferBoundsResult inferUpperBoundLookup(TNode t, const InferBoundsParameters& p); + //InferBoundsResult inferUpperBoundSimplex(TNode t, const SimplexInferBoundsParameters& p); + + /** + * Infers either a new upper/lower bound on term in the real relaxation. + * Either: + * - term is malformed (see below) + * - a maximum/minimum is found with the result being a pair + * -- <dr, exp> where + * -- term <?> dr is implies by exp + * -- <?> is <= if inferring an upper bound, >= otherwise + * -- exp is in terms of the assertions to the theory. + * - No upper or lower bound is inferrable in the real relaxation. + * -- Returns <0, Null()> + * - the maximum number of rounds was exhausted: + * -- Returns <v, term> where v is the current feasible value of term + * - Threshold reached: + * -- If theshold != NULL, and a feasible value is found to exceed threshold + * -- Simplex stops and returns <threshold, term> + */ + //std::pair<DeltaRational, Node> inferBound(TNode term, bool lb, int maxRounds = -1, const DeltaRational* threshold = NULL); + +private: + static bool decomposeTerm(Node term, Rational& m, Node& p, Rational& c); + static bool decomposeLiteral(Node lit, Kind& k, int& dir, Rational& lm, Node& lp, Rational& rm, Node& rp, Rational& dm, Node& dp, DeltaRational& sep); + static void setToMin(int sgn, std::pair<Node, DeltaRational>& min, const std::pair<Node, DeltaRational>& e); + /** * The map between arith variables to nodes. */ @@ -427,6 +470,10 @@ public: Node getModelValue(TNode var); + + std::pair<bool, Node> entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out); + + private: /** The constant zero. */ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index c8a08dad9..06858cf92 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -208,6 +208,7 @@ void InstantiationEngine::check( Theory::Effort e ){ clSet = double(clock())/double(CLOCKS_PER_SEC); Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl; } + ++(d_statistics.d_instantiation_rounds); bool quantActive = false; Debug("quantifiers") << "quantifiers: check: asserted quantifiers size" << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; @@ -438,7 +439,8 @@ InstantiationEngine::Statistics::Statistics(): d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0), d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0), d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0), - d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0) + d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0), + d_instantiation_rounds("InstantiationEngine::Rounds", 0 ) { StatisticsRegistry::registerStat(&d_instantiations_user_patterns); StatisticsRegistry::registerStat(&d_instantiations_auto_gen); @@ -447,6 +449,7 @@ InstantiationEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith); StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus); StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes); + StatisticsRegistry::registerStat(&d_instantiation_rounds); } InstantiationEngine::Statistics::~Statistics(){ @@ -457,4 +460,5 @@ InstantiationEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith); StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus); StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes); + StatisticsRegistry::unregisterStat(&d_instantiation_rounds); } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 53777d362..a460f1164 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -149,6 +149,7 @@ public: IntStat d_instantiations_cbqi_arith; IntStat d_instantiations_cbqi_arith_minus; IntStat d_instantiations_cbqi_datatypes; + IntStat d_instantiation_rounds; Statistics(); ~Statistics(); }; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index e733764f0..f4acfb926 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -126,6 +126,8 @@ option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default what effort to apply conflict find mechanism option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h" when to invoke conflict find mechanism for quantifiers +option qcfTConstraint --qcf-tconstraint bool :read-write :default false + enable entailment checks for t-constraints in qcf algorithm option quantRewriteRules --rewrite-rules bool :default true use rewrite rules module diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index e27d438be..2f399be33 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -91,24 +91,44 @@ void QuantInfo::initialize( Node q, Node qn ) { d_mg = new MatchGen( this, qn );
if( d_mg->isValid() ){
- for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
- if( d_vars[j].getKind()!=BOUND_VARIABLE ){
- bool beneathQuant = d_nbeneathQuant.find( d_vars[j] )==d_nbeneathQuant.end();
- d_var_mg[j] = new MatchGen( this, d_vars[j], true, beneathQuant );
- if( !d_var_mg[j]->isValid() ){
- d_mg->setInvalid();
- break;
- }else{
- std::vector< int > bvars;
- d_var_mg[j]->determineVariableOrder( this, bvars );
- }
+ /*
+ for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+ if( d_inMatchConstraint.find( q[0][j] )==d_inMatchConstraint.end() ){
+ Trace("qcf-invalid") << "QCF invalid : variable " << q[0][j] << " does not exist in a matching constraint." << std::endl;
+ d_mg->setInvalid();
+ break;
}
}
-
+ */
if( d_mg->isValid() ){
- std::vector< int > bvars;
- d_mg->determineVariableOrder( this, bvars );
+ for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){
+ if( d_vars[j].getKind()!=BOUND_VARIABLE ){
+ d_var_mg[j] = NULL;
+ bool is_tsym = false;
+ if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){
+ is_tsym = true;
+ d_tsym_vars.push_back( j );
+ }
+ if( !is_tsym || options::qcfTConstraint() ){
+ d_var_mg[j] = new MatchGen( this, d_vars[j], true );
+ }
+ if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){
+ Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;
+ d_mg->setInvalid();
+ break;
+ }else{
+ std::vector< int > bvars;
+ d_var_mg[j]->determineVariableOrder( this, bvars );
+ }
+ }
+ }
+ if( d_mg->isValid() ){
+ std::vector< int > bvars;
+ d_mg->determineVariableOrder( this, bvars );
+ }
}
+ }else{
+ Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;
}
Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;
}
@@ -131,20 +151,24 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) for( unsigned i=1; i<=2; i++ ){
flatten( n[i], beneathQuant );
}
+ registerNode( n[0], false, pol, beneathQuant );
+ }else if( options::qcfTConstraint() ){
+ //a theory-specific predicate
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ flatten( n[i], beneathQuant );
+ }
}
}
- }
- if( isVar( n ) && !beneathQuant ){
- d_nbeneathQuant[n] = true;
- }
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- bool newHasPol;
- bool newPol;
- QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
- //QcfNode * qcfc = new QcfNode( d_c );
- //qcfc->d_parent = qcf;
- //qcf->d_child[i] = qcfc;
- registerNode( n[i], newHasPol, newPol, beneathQuant );
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ bool newHasPol;
+ bool newPol;
+ QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );
+ //QcfNode * qcfc = new QcfNode( d_c );
+ //qcfc->d_parent = qcf;
+ //qcf->d_child[i] = qcfc;
+ registerNode( n[i], newHasPol, newPol, beneathQuant );
+ }
}
}
}
@@ -152,6 +176,10 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) void QuantInfo::flatten( Node n, bool beneathQuant ) {
Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;
if( n.hasBoundVar() ){
+ if( n.getKind()==BOUND_VARIABLE ){
+ d_inMatchConstraint[n] = true;
+ }
+ //if( MatchGen::isHandledUfTerm( n ) || n.getKind()==ITE ){
if( d_var_num.find( n )==d_var_num.end() ){
Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;
d_var_num[n] = d_vars.size();
@@ -165,9 +193,6 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) { flatten( n[i], beneathQuant );
}
}
- if( !beneathQuant ){
- d_nbeneathQuant[n] = true;
- }
}else{
Trace("qcf-qregister-debug2") << "...already processed" << std::endl;
}
@@ -183,6 +208,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) { d_match_term[i] = TNode::null();
}
d_curr_var_deq.clear();
+ d_tconstraints.clear();
//add built-in variable constraints
for( unsigned r=0; r<2; r++ ){
for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();
@@ -270,6 +296,8 @@ bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, boo }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){
//they must actually be disequal if we are looking for conflicts
if( !p->areDisequal( n, cv ) ){
+ //TODO : check for entailed disequal
+
return false;
}
}
@@ -462,6 +490,53 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) { return false;
}
+bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) {
+ if( !d_tconstraints.empty() ){
+ //check constraints
+ for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
+ //apply substitution to the tconstraint
+ Node cons = it->first.substitute( p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].begin(),
+ p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].end(),
+ terms.begin(), terms.end() );
+ cons = it->second ? cons : cons.negate();
+ if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
+ Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;
+ Node rew = Rewriter::rewrite( lit );
+ if( rew==p->d_false ){
+ Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl;
+ return false;
+ }else if( rew!=p->d_true ){
+ //if checking for conflicts, we must be sure that the constraint is entailed
+ if( chEnt ){
+ //check if it is entailed
+ Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;
+ std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );
+ ++(p->d_statistics.d_entailment_checks);
+ Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;
+ if( !et.first ){
+ Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;
+ return false;
+ }else{
+ return true;
+ }
+ }else{
+ Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl;
+ return true;
+ }
+ }else{
+ Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;
+ return true;
+ }
+}
+
bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {
//assign values for variables that were unassigned (usually not necessary, but handles corner cases)
bool doFail = false;
@@ -470,27 +545,124 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign doFail = true;
success = false;
}else{
- d_unassigned.clear();
- d_unassigned_tn.clear();
- std::vector< int > unassigned[2];
- std::vector< TypeNode > unassigned_tn[2];
- for( int i=0; i<getNumVars(); i++ ){
- if( d_match[i].isNull() ){
- int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
- unassigned[rindex].push_back( i );
- unassigned_tn[rindex].push_back( getVar( i ).getType() );
- assigned.push_back( i );
- }
- }
- d_unassigned_nvar = unassigned[0].size();
- for( unsigned i=0; i<2; i++ ){
- d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );
- d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );
+ //solve for interpreted symbol matches
+ // this breaks the invariant that all introduced constraints are over existing terms
+ for( int i=(int)(d_tsym_vars.size()-1); i>=0; i-- ){
+ int index = d_tsym_vars[i];
+ TNode v = getCurrentValue( d_vars[index] );
+ int slv_v = -1;
+ if( v==d_vars[index] ){
+ slv_v = index;
+ }
+ Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;
+ if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){
+ Kind k = d_vars[index].getKind();
+ std::vector< TNode > children;
+ for( unsigned j=0; j<d_vars[index].getNumChildren(); j++ ){
+ int vn = getVarNum( d_vars[index][j] );
+ if( vn!=-1 ){
+ TNode vv = getCurrentValue( d_vars[index][j] );
+ if( vv==d_vars[index][j] ){
+ //we will assign this
+ if( slv_v==-1 ){
+ Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;
+ slv_v = vn;
+ if( p->d_effort!=QuantConflictFind::effort_conflict ){
+ break;
+ }
+ }else{
+ Node z = p->getZero( k );
+ if( !z.isNull() ){
+ Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;
+ assigned.push_back( vn );
+ if( !setMatch( p, vn, z ) ){
+ success = false;
+ break;
+ }
+ }
+ }
+ }else{
+ Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl;
+ children.push_back( vv );
+ }
+ }else{
+ Trace("qcf-tconstraint-debug") << "...sum " << d_vars[index][j] << std::endl;
+ children.push_back( d_vars[index][j] );
+ }
+ }
+ if( success ){
+ if( slv_v!=-1 ){
+ Node lhs;
+ if( children.empty() ){
+ lhs = p->getZero( k );
+ }else if( children.size()==1 ){
+ lhs = children[0];
+ }else{
+ lhs = NodeManager::currentNM()->mkNode( k, children );
+ }
+ Node sum;
+ if( v==d_vars[index] ){
+ sum = lhs;
+ }else{
+ if( p->d_effort==QuantConflictFind::effort_conflict ){
+ Kind kn = k;
+ if( d_vars[index].getKind()==PLUS ){
+ kn = MINUS;
+ }
+ if( kn!=k ){
+ sum = NodeManager::currentNM()->mkNode( kn, v, lhs );
+ }
+ }
+ }
+ if( !sum.isNull() ){
+ assigned.push_back( slv_v );
+ Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;
+ if( !setMatch( p, slv_v, sum ) ){
+ success = false;
+ }
+ p->d_tempCache.push_back( sum );
+ }
+ }else{
+ //must show that constraint is met
+ Node sum = NodeManager::currentNM()->mkNode( k, children );
+ Node eq = sum.eqNode( v );
+ if( !entailmentTest( p, eq ) ){
+ success = false;
+ }
+ p->d_tempCache.push_back( sum );
+ }
+ }
+ }
+
+ if( !success ){
+ break;
+ }
+ }
+ if( success ){
+ //check what is left to assign
+ d_unassigned.clear();
+ d_unassigned_tn.clear();
+ std::vector< int > unassigned[2];
+ std::vector< TypeNode > unassigned_tn[2];
+ for( int i=0; i<getNumVars(); i++ ){
+ if( d_match[i].isNull() ){
+ int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;
+ unassigned[rindex].push_back( i );
+ unassigned_tn[rindex].push_back( getVar( i ).getType() );
+ assigned.push_back( i );
+ }
+ }
+ d_unassigned_nvar = unassigned[0].size();
+ for( unsigned i=0; i<2; i++ ){
+ d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );
+ d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );
+ }
+ d_una_eqc_count.clear();
+ d_una_index = 0;
}
- d_una_eqc_count.clear();
- d_una_index = 0;
}
- if( !d_unassigned.empty() ){
+
+ if( !d_unassigned.empty() && ( success || doContinue ) ){
Trace("qcf-check") << "Assign to unassigned..." << std::endl;
do {
if( doFail ){
@@ -571,6 +743,12 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign }while( success && isMatchSpurious( p ) );
}
if( success ){
+ for( unsigned i=0; i<d_unassigned.size(); i++ ){
+ int ui = d_unassigned[i];
+ if( !d_match[ui].isNull() ){
+ Trace("qcf-check") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;
+ }
+ }
return true;
}else{
for( unsigned i=0; i<assigned.size(); i++ ){
@@ -623,42 +801,21 @@ void QuantInfo::debugPrintMatch( const char * c ) { }
Trace(c) << std::endl;
}
+ if( !d_tconstraints.empty() ){
+ Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl;
+ for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
+ Trace(c) << " " << it->first << " -> " << it->second << std::endl;
+ }
+ }
}
-//void QuantInfo::addFuncParent( int v, Node f, int arg ) {
-// if( std::find( d_f_parent[v][f].begin(), d_f_parent[v][f].end(), arg )==d_f_parent[v][f].end() ){
-// d_f_parent[v][f].push_back( arg );
-// }
-//}
-
-MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){
- Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << ", beneathQuant = " << beneathQuant << std::endl;
+MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){
+ Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;
std::vector< Node > qni_apps;
d_qni_size = 0;
if( isVar ){
Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );
- if( isHandledUfTerm( n ) ){
- d_qni_var_num[0] = qi->getVarNum( n );
- d_qni_size++;
- d_type = typ_var;
- d_type_not = false;
- d_n = n;
- //Node f = getOperator( n );
- for( unsigned j=0; j<d_n.getNumChildren(); j++ ){
- Node nn = d_n[j];
- Trace("qcf-qregister-debug") << " " << d_qni_size;
- if( qi->isVar( nn ) ){
- int v = qi->d_var_num[nn];
- Trace("qcf-qregister-debug") << " is var #" << v << std::endl;
- d_qni_var_num[d_qni_size] = v;
- //qi->addFuncParent( v, f, j );
- }else{
- Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
- d_qni_gterm[d_qni_size] = nn;
- }
- d_qni_size++;
- }
- }else if( n.getKind()==ITE ){
+ if( n.getKind()==ITE ){
d_type = typ_ite_var;
d_type_not = false;
d_n = n;
@@ -678,8 +835,26 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ d_type = typ_invalid;
}
}else{
- //for now, unknown term
- d_type = typ_invalid;
+ d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;
+ d_qni_var_num[0] = qi->getVarNum( n );
+ d_qni_size++;
+ d_type_not = false;
+ d_n = n;
+ //Node f = getOperator( n );
+ for( unsigned j=0; j<d_n.getNumChildren(); j++ ){
+ Node nn = d_n[j];
+ Trace("qcf-qregister-debug") << " " << d_qni_size;
+ if( qi->isVar( nn ) ){
+ int v = qi->d_var_num[nn];
+ Trace("qcf-qregister-debug") << " is var #" << v << std::endl;
+ d_qni_var_num[d_qni_size] = v;
+ //qi->addFuncParent( v, f, j );
+ }else{
+ Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;
+ d_qni_gterm[d_qni_size] = nn;
+ }
+ d_qni_size++;
+ }
}
}else{
if( n.hasBoundVar() ){
@@ -693,10 +868,9 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ if( isHandledBoolConnective( d_n ) ){
//non-literals
d_type = typ_formula;
- bool nBeneathQuant = beneathQuant || d_n.getKind()==FORALL;
for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
if( d_n.getKind()!=FORALL || i==1 ){
- d_children.push_back( MatchGen( qi, d_n[i], false, nBeneathQuant ) );
+ d_children.push_back( MatchGen( qi, d_n[i], false ) );
if( !d_children[d_children.size()-1].isValid() ){
setInvalid();
break;
@@ -726,25 +900,28 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ }else{
d_type = typ_invalid;
//literals
- if( d_n.getKind()==EQUAL ){
- for( unsigned i=0; i<2; i++ ){
+ if( isHandledUfTerm( d_n ) ){
+ Assert( qi->isVar( d_n ) );
+ d_type = typ_pred;
+ }else if( d_n.getKind()==BOUND_VARIABLE ){
+ Assert( d_n.getType().isBoolean() );
+ d_type = typ_bool_var;
+ }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){
+ for( unsigned i=0; i<d_n.getNumChildren(); i++ ){
if( d_n[i].hasBoundVar() ){
if( !qi->isVar( d_n[i] ) ){
Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl;
}
Assert( qi->isVar( d_n[i] ) );
+ if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){
+ d_qni_var_num[i+1] = qi->d_var_num[d_n[i]];
+ }
}else{
d_qni_gterm[i] = d_n[i];
}
}
- d_type = typ_eq;
- }else if( isHandledUfTerm( d_n ) ){
- Assert( qi->isVar( d_n ) );
- d_type = typ_pred;
- }else if( d_n.getKind()==BOUND_VARIABLE ){
- d_type = typ_bool_var;
- }else{
- Trace("qcf-invalid") << "Unhandled : " << d_n << std::endl;
+ d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint;
+ Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;
}
}
}else{
@@ -900,7 +1077,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { //set up processing matches
if( d_type==typ_invalid ){
- //do nothing : return success once?
+ //do nothing
}else if( d_type==typ_ground ){
if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){
d_child_counter = 0;
@@ -933,6 +1110,15 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { d_qn.push_back( qni );
}
d_matched_basis = false;
+ }else if( d_type==typ_tsym || d_type==typ_tconstraint ){
+ for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){
+ int repVar = qi->getCurrentRepVar( it->second );
+ if( qi->d_match[repVar].isNull() ){
+ Debug("qcf-match-debug") << "Force matching on child #" << it->first << ", which is var #" << repVar << std::endl;
+ d_qni_bound[it->first] = repVar;
+ }
+ }
+ d_qn.push_back( NULL );
}else if( d_type==typ_pred || d_type==typ_eq ){
//add initial constraint
Node nn[2];
@@ -1031,7 +1217,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { d_wasSet = false;
return false;
}
- }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var ){
+ }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var || d_type==typ_tconstraint || d_type==typ_tsym ){
bool success = false;
bool terminate = false;
do {
@@ -1043,6 +1229,18 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { d_binding = true;
d_binding_it = d_qni_bound.begin();
doReset = true;
+ //for tconstraint, add constraint
+ if( d_type==typ_tconstraint ){
+ std::map< Node, bool >::iterator it = qi->d_tconstraints.find( d_n );
+ if( it==qi->d_tconstraints.end() ){
+ qi->d_tconstraints[d_n] = d_tgt;
+ //store that we added this constraint
+ d_qni_bound_cons[0] = d_n;
+ }else if( d_tgt!=it->second ){
+ success = false;
+ terminate = true;
+ }
+ }
}else{
Debug("qcf-match-debug") << " - Matching failed" << std::endl;
success = false;
@@ -1128,6 +1326,13 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { }
d_qni_bound.clear();
}
+ if( d_type==typ_tconstraint ){
+ //remove constraint if applicable
+ if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){
+ qi->d_tconstraints.erase( d_n );
+ d_qni_bound_cons.clear();
+ }
+ }
/*
if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){
d_matched_basis = true;
@@ -1869,7 +2074,9 @@ void QuantConflictFind::check( Theory::Effort level ) { if( d_performCheck ){
++(d_statistics.d_inst_rounds);
double clSet = 0;
+ int prevEt = 0;
if( Trace.isOn("qcf-engine") ){
+ prevEt = d_statistics.d_entailment_checks.getData();
clSet = double(clock())/double(CLOCKS_PER_SEC);
Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;
}
@@ -1980,31 +2187,37 @@ void QuantConflictFind::check( Theory::Effort level ) { */
std::vector< Node > terms;
qi->getMatch( terms );
- if( Debug.isOn("qcf-check-inst") ){
- //if( e==effort_conflict ){
- Node inst = d_quantEngine->getInstantiation( q, terms );
- Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
- Assert( evaluate( inst )!=1 );
- Assert( evaluate( inst )==-1 || e>effort_conflict );
- //}
- }
- if( d_quantEngine->addInstantiation( q, terms ) ){
- Trace("qcf-check") << " ... Added instantiation" << std::endl;
- ++addedLemmas;
- if( e==effort_conflict ){
- d_quant_order.insert( d_quant_order.begin(), q );
- d_conflict.set( true );
- ++(d_statistics.d_conflict_inst);
- break;
- }else if( e==effort_prop_eq ){
- ++(d_statistics.d_prop_inst);
+ if( !qi->isTConstraintSpurious( this, terms ) ){
+ if( Debug.isOn("qcf-check-inst") ){
+ //if( e==effort_conflict ){
+ Node inst = d_quantEngine->getInstantiation( q, terms );
+ Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
+ Assert( evaluate( inst )!=1 );
+ Assert( evaluate( inst )==-1 || e>effort_conflict );
+ //}
+ }
+ if( d_quantEngine->addInstantiation( q, terms ) ){
+ Trace("qcf-check") << " ... Added instantiation" << std::endl;
+ Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
+ qi->debugPrintMatch("qcf-inst");
+ Trace("qcf-inst") << std::endl;
+ ++addedLemmas;
+ if( e==effort_conflict ){
+ d_quant_order.insert( d_quant_order.begin(), q );
+ d_conflict.set( true );
+ ++(d_statistics.d_conflict_inst);
+ break;
+ }else if( e==effort_prop_eq ){
+ ++(d_statistics.d_prop_inst);
+ }
+ }else{
+ Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;
+ //Assert( false );
}
- }else{
- Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;
- //Assert( false );
}
//clean up assigned
qi->revertMatch( assigned );
+ d_tempCache.clear();
}else{
Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
}
@@ -2030,6 +2243,8 @@ void QuantConflictFind::check( Theory::Effort level ) { Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
}
Trace("qcf-engine") << std::endl;
+ int currEt = d_statistics.d_entailment_checks.getData();
+ Trace("qcf-engine") << " Entailment checks = " << ( currEt - prevEt ) << std::endl;
}
}
Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
@@ -2275,17 +2490,35 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo QuantConflictFind::Statistics::Statistics():
d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),
d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),
- d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 )
+ d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),
+ d_entailment_checks("QuantConflictFind::Entailment_Checks",0)
{
StatisticsRegistry::registerStat(&d_inst_rounds);
StatisticsRegistry::registerStat(&d_conflict_inst);
StatisticsRegistry::registerStat(&d_prop_inst);
+ StatisticsRegistry::registerStat(&d_entailment_checks);
}
QuantConflictFind::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_inst_rounds);
StatisticsRegistry::unregisterStat(&d_conflict_inst);
StatisticsRegistry::unregisterStat(&d_prop_inst);
+ StatisticsRegistry::unregisterStat(&d_entailment_checks);
}
+TNode QuantConflictFind::getZero( Kind k ) {
+ std::map< Kind, Node >::iterator it = d_zero.find( k );
+ if( it==d_zero.end() ){
+ Node nn;
+ if( k==PLUS ){
+ nn = NodeManager::currentNM()->mkConst( Rational(0) );
+ }
+ d_zero[k] = nn;
+ return nn;
+ }else{
+ return it->second;
+ }
+}
+
+
}
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 71e967653..64ece7ed0 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -84,11 +84,13 @@ public: typ_var,
typ_ite_var,
typ_bool_var,
+ typ_tconstraint,
+ typ_tsym,
};
void debugPrintType( const char * c, short typ, bool isTrace = false );
public:
MatchGen() : d_type( typ_invalid ){}
- MatchGen( QuantInfo * qi, Node n, bool isVar = false, bool beneathQuant = false );
+ MatchGen( QuantInfo * qi, Node n, bool isVar = false );
bool d_tgt;
bool d_tgt_orig;
bool d_wasSet;
@@ -128,7 +130,8 @@ public: ~QuantInfo() { delete d_mg; }
std::vector< TNode > d_vars;
std::map< TNode, int > d_var_num;
- std::map< TNode, bool > d_nbeneathQuant;
+ std::vector< int > d_tsym_vars;
+ std::map< TNode, bool > d_inMatchConstraint;
std::map< int, std::vector< Node > > d_var_constraint[2];
int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }
bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }
@@ -146,6 +149,7 @@ public: std::vector< TNode > d_match;
std::vector< TNode > d_match_term;
std::map< int, std::map< TNode, int > > d_curr_var_deq;
+ std::map< Node, bool > d_tconstraints;
int getCurrentRepVar( int v );
TNode getCurrentValue( TNode n );
TNode getCurrentExpValue( TNode n );
@@ -154,6 +158,8 @@ public: int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );
bool setMatch( QuantConflictFind * p, int v, TNode n );
bool isMatchSpurious( QuantConflictFind * p );
+ bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );
+ bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );
bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );
void revertMatch( std::vector< int >& assigned );
void debugPrintMatch( const char * c );
@@ -174,6 +180,9 @@ private: context::CDO< bool > d_conflict;
bool d_performCheck;
std::vector< Node > d_quant_order;
+ std::map< Kind, Node > d_zero;
+ //for storing nodes created during t-constraint solving (prevents memory leaks)
+ std::vector< Node > d_tempCache;
private:
std::map< Node, Node > d_op_node;
int d_fid_count;
@@ -182,6 +191,7 @@ private: public: //for ground terms
Node d_true;
Node d_false;
+ TNode getZero( Kind k );
private:
Node evaluateTerm( Node n );
int evaluate( Node n, bool pref = false, bool hasPref = false );
@@ -271,6 +281,7 @@ public: IntStat d_inst_rounds;
IntStat d_conflict_inst;
IntStat d_prop_inst;
+ IntStat d_entailment_checks;
Statistics();
~Statistics();
};
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 41108bc2a..757a76baa 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -207,7 +207,7 @@ public: Node getSkolemizedBody( Node f ); //miscellaneous -private: +public: /** map from universal quantifiers to the list of variables */ std::map< Node, std::vector< Node > > d_vars; /** free variable for instantiation constant type */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index c52ee936a..f65e48ec2 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -228,6 +228,32 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstituti return PP_ASSERT_STATUS_UNSOLVED; } +std::pair<bool, Node> Theory::entailmentCheck(TNode lit, + const EntailmentCheckParameters* params, + EntailmentCheckSideEffects* out){ + return make_pair(false, Node::null()); +} + +EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid) + : d_tid(tid) { +} + +EntailmentCheckParameters::~EntailmentCheckParameters(){} + +TheoryId EntailmentCheckParameters::getTheoryId() const { + return d_tid; +} + +EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid) + : d_tid(tid) +{} + +TheoryId EntailmentCheckSideEffects::getTheoryId() const { + return d_tid; +} + +EntailmentCheckSideEffects::~EntailmentCheckSideEffects() { +} }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index c86aa17de..972abe3d8 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -52,6 +52,9 @@ class QuantifiersEngine; class TheoryModel; class SubstitutionMap; +class EntailmentCheckParameters; +class EntailmentCheckSideEffects; + namespace rrinst { class CandidateGenerator; }/* CVC4::theory::rrinst namespace */ @@ -808,6 +811,63 @@ public: * in a queriable form. As this is */ std::hash_set<TNode, TNodeHashFunction> currentlySharedTerms() const; + + /** + * This allows the theory to be queried for whether a literal, lit, is + * entailed by the theory. This returns a pair of a Boolean and a node E. + * + * If the Boolean is true, then E is a formula that entails lit and E is propositionally + * entailed by the assertions to the theory. + * + * If the Boolean is false, it is "unknown" if lit is entailed and E may be + * any node. + * + * The literal lit is either an atom a or (not a), which must belong to the theory: + * There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId(). + * + * There are NO assumptions that a or the subterms of a have been + * preprocessed in any form. This includes ppRewrite, rewriting, + * preregistering, registering, definition expansion or ITE removal! + * + * Theories are free to limit the amount of effort they use and so may + * always opt to return "unknown". Both "unknown" and "not entailed", + * may return for E a non-boolean Node (e.g. Node::null()). (There is no explicit output + * for the negation of lit is entailed.) + * + * If lit is theory valid, the return result may be the Boolean constant + * true for E. + * + * If lit is entailed by multiple assertions on the theory's getFact() + * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or + * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k) + * + * If lit is entailed by a single assertion on the theory's getFact() + * queue, say a, this may return E=a. + * + * The theory may always return false! + * + * The search is controlled by the parameter params. For default behavior, + * this may be left NULL. + * + * Theories that want parameters extend the virtual EntailmentCheckParameters + * class. Users ask the theory for an appropriate subclass from the theory + * and configure that. How this is implemented is on a per theory basis. + * + * The search may provide additional output to guide the user of + * this function. This output is stored in a EntailmentCheckSideEffects* + * output parameter. The implementation of this is theory specific. For + * no output, this is NULL. + * + * Theories may not touch their output stream during an entailment check. + * + * @param lit a literal belonging to the theory. + * @param params the control parameters for the entailment check. + * @param out a theory specific output object of the entailment search. + * @return a pair <b,E> s.t. if b is true, then a formula E such that + * E |= lit in the theory. + */ + virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); + };/* class Theory */ std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); @@ -852,6 +912,26 @@ inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertSta return out; } +class EntailmentCheckParameters { +private: + TheoryId d_tid; +protected: + EntailmentCheckParameters(TheoryId tid); +public: + TheoryId getTheoryId() const; + virtual ~EntailmentCheckParameters(); +};/* class EntailmentCheckParameters */ + +class EntailmentCheckSideEffects { +private: + TheoryId d_tid; +protected: + EntailmentCheckSideEffects(TheoryId tid); +public: + TheoryId getTheoryId() const; + virtual ~EntailmentCheckSideEffects(); +};/* class EntailmentCheckSideEffects */ + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 33ff18126..18968e897 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1658,3 +1658,15 @@ void TheoryEngine::checkTheoryAssertionsWithModel() { } } } + +std::pair<bool, Node> TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* seffects) { + TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit; + theory::TheoryId tid = theory::Theory::theoryOf(mode, atom); + theory::Theory* th = theoryOf(tid); + + Assert(th != NULL); + Assert(params == NULL || tid == params->getTheoryId()); + Assert(seffects == NULL || tid == seffects->getTheoryId()); + + return th->entailmentCheck(lit, params, seffects); +} diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 9a987c9d7..8bc67616f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -83,6 +83,9 @@ namespace theory { namespace eq { class EqualityEngine; } + + class EntailmentCheckParameters; + class EntailmentCheckSideEffects; }/* CVC4::theory namespace */ class DecisionEngine; class RemoveITE; @@ -755,6 +758,12 @@ public: */ Node getModelValue(TNode var); + /** + * Forwards an entailmentCheck according to the given theoryOfMode mode. + * See theory.h for documentation on entailmentCheck(). + */ + std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL); + private: /** Default visitor for pre-registration */ diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index 383f27688..bd23b48c9 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -57,3 +57,26 @@ void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, uns throw std::invalid_argument(ss.str()); } } + +bool Integer::fitsSignedInt() const { + // TODO improve performance + return d_value <= std::numeric_limits<signed int>::max() && + d_value >= std::numeric_limits<signed int>::min(); +} + +bool Integer::fitsUnsignedInt() const { + // TODO improve performance + return sgn() >= 0 && d_value <= std::numeric_limits<unsigned int>::max(); +} + +signed int Integer::getSignedInt() const { + // ensure there isn't overflow + CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()"); + return cln::cl_I_to_int(d_value); +} + +unsigned int Integer::getUnsignedInt() const { + // ensure there isn't overflow + CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()"); + return cln::cl_I_to_uint(d_value); +} diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 05d820dbc..8b56c4b19 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -415,6 +415,16 @@ public: return d_value == -1; } + /** fits the C "signed int" primitive */ + bool fitsSignedInt() const; + + /** fits the C "unsigned int" primitive */ + bool fitsUnsignedInt() const; + + int getSignedInt() const; + + unsigned int getUnsignedInt() const; + long getLong() const { // ensure there isn't overflow CheckArgument(d_value <= std::numeric_limits<long>::max(), this, diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index f2a888340..bb6166523 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -36,3 +36,32 @@ Integer::Integer(const char* s, unsigned base) Integer::Integer(const std::string& s, unsigned base) : d_value(s, base) {} + + +bool Integer::fitsSignedInt() const { + return d_value.fits_sint_p(); +} + +bool Integer::fitsUnsignedInt() const { + return d_value.fits_uint_p(); +} + +signed int Integer::getSignedInt() const { + // ensure there isn't overflow + CheckArgument(d_value <= std::numeric_limits<int>::max(), this, + "Overflow detected in Integer::getSignedInt()"); + CheckArgument(d_value >= std::numeric_limits<int>::min(), this, + "Overflow detected in Integer::getSignedInt()"); + CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()"); + return (signed int) d_value.get_si(); +} + +unsigned int Integer::getUnsignedInt() const { + // ensure there isn't overflow + CheckArgument(d_value <= std::numeric_limits<unsigned int>::max(), this, + "Overflow detected in Integer::getUnsignedInt()"); + CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(), this, + "Overflow detected in Integer::getUnsignedInt()"); + CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()"); + return (unsigned int) d_value.get_ui(); +} diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index a39de7996..68d335aec 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -22,6 +22,7 @@ #include <string> #include <iostream> +#include <limits> #include "util/gmp_util.h" #include "util/exception.h" @@ -417,7 +418,13 @@ public: return d_value.get_str(base); } - //friend std::ostream& operator<<(std::ostream& os, const Integer& n); + bool fitsSignedInt() const; + + bool fitsUnsignedInt() const; + + signed int getSignedInt() const; + + unsigned int getUnsignedInt() const; long getLong() const { long si = d_value.get_si(); diff --git a/src/util/maybe.h b/src/util/maybe.h index e90953e0b..b1c81f76e 100644 --- a/src/util/maybe.h +++ b/src/util/maybe.h @@ -75,6 +75,7 @@ inline std::ostream& operator<<(std::ostream& out, const Maybe<T>& m){ if(m.nothing()){ out << "Nothing"; }else{ + out << "Just "; out << m.constValue(); } out << "}"; |