}else{
Node inst =
p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms);
- Node inst_eval = p->getTermDatabase()->evaluateTerm( inst, NULL, options::qcfTConstraint() );
+ inst = Rewriter::rewrite(inst);
+ Node inst_eval = p->getTermDatabase()->evaluateTerm(
+ inst, nullptr, options::qcfTConstraint(), true);
if( Trace.isOn("qcf-instance-check") ){
Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
for( unsigned i=0; i<terms.size(); i++ ){
}
Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl;
}
- if( inst_eval.isNull() || inst_eval==p->getTermUtil()->d_true || !isPropagatingInstance( p, inst_eval ) ){
+ if (inst_eval.isNull()
+ || (inst_eval.isConst() && inst_eval.getConst<bool>()))
+ {
Trace("qcf-instance-check") << "...spurious." << std::endl;
return true;
}else{
+ Assert(p->isPropagatingInstance(inst_eval));
Trace("qcf-instance-check") << "...not spurious." << std::endl;
}
}
return p->d_quantEngine->inConflict();
}
-bool QuantInfo::isPropagatingInstance( QuantConflictFind * p, Node n ) {
- if( n.getKind()==FORALL ){
- //TODO?
- return true;
- }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE ||
- ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) ){
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( !isPropagatingInstance( p, n[i] ) ){
- return false;
- }
- }
- return true;
- }else{
- if( p->getEqualityEngine()->hasTerm( n ) || isGroundSubterm( n ) ){
- return true;
- }
- }
- Trace("qcf-instance-check-debug") << "...not propagating instance because of " << n << std::endl;
- return false;
-}
-
bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {
Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;
Node rew = Rewriter::rewrite( lit );
else
{
d_qni_gterm[i] = d_n[i];
- qi->setGroundSubterm(d_n[i]);
}
}
d_type = d_n.getKind() == EQUAL ? typ_eq : typ_tconstraint;
//we will just evaluate
d_n = n;
d_type = typ_ground;
- qi->setGroundSubterm( d_n );
}
}
Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = ";
return os;
}
+bool QuantConflictFind::isPropagatingInstance(Node n) const
+{
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ std::vector<TNode> visit;
+ TNode cur;
+ visit.push_back(n);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ if (visited.find(cur) == visited.end())
+ {
+ visited.insert(cur);
+ Kind ck = cur.getKind();
+ if (ck == FORALL)
+ {
+ // do nothing
+ }
+ else if (TermUtil::isBoolConnective(ck))
+ {
+ for (TNode cc : cur)
+ {
+ visit.push_back(cc);
+ }
+ }
+ else if (!getEqualityEngine()->hasTerm(cur))
+ {
+ Trace("qcf-instance-check-debug")
+ << "...not propagating instance because of " << n << std::endl;
+ return false;
+ }
+ }
+ } while (!visit.empty());
+ return true;
+}
+
} /* namespace CVC4::theory::quantifiers */
} /* namespace CVC4::theory */
} /* namespace CVC4 */
void getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited );
//optimization: number of variables set, to track when we can stop
std::map< int, bool > d_vars_set;
- std::map< Node, bool > d_ground_terms;
std::vector< Node > d_extra_var;
public:
- void setGroundSubterm( Node t ) { d_ground_terms[t] = true; }
- bool isGroundSubterm( Node t ) { return d_ground_terms.find( t )!=d_ground_terms.end(); }
bool isBaseMatchComplete();
- bool isPropagatingInstance( QuantConflictFind * p, Node n );
public:
QuantInfo();
~QuantInfo();
Statistics d_statistics;
/** Identify this module */
std::string identify() const override { return "QcfEngine"; }
+ /** is n a propagating instance?
+ *
+ * A propagating instance is any formula that consists of Boolean connectives,
+ * equality, quantified formulas, and terms that exist in the current
+ * context (those in the master equality engine).
+ *
+ * Notice the distinction that quantified formulas that do not appear in the
+ * current context are considered to be legal in propagating instances. This
+ * choice is significant for TPTP, where a net of ~200 benchmarks are gained
+ * due to this decision.
+ *
+ * Propagating instances are the second most useful kind of instantiation
+ * after conflicting instances and are used as a second effort in the
+ * algorithm performed by this class.
+ */
+ bool isPropagatingInstance(Node n) const;
};
std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e);
return QEFFORT_NONE;
}
-eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
+eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const
+{
return d_quantEngine->getActiveEqualityEngine();
}
-bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
+bool QuantifiersModule::areEqual(TNode n1, TNode n2) const
+{
return d_quantEngine->getEqualityQuery()->areEqual( n1, n2 );
}
-bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) {
+bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const
+{
return d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 );
}
-TNode QuantifiersModule::getRepresentative( TNode n ) {
+TNode QuantifiersModule::getRepresentative(TNode n) const
+{
return d_quantEngine->getEqualityQuery()->getRepresentative( n );
}
-quantifiers::TermDb * QuantifiersModule::getTermDatabase() {
+QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const
+{
+ return d_quantEngine;
+}
+
+quantifiers::TermDb* QuantifiersModule::getTermDatabase() const
+{
return d_quantEngine->getTermDatabase();
}
-quantifiers::TermUtil * QuantifiersModule::getTermUtil() {
+quantifiers::TermUtil* QuantifiersModule::getTermUtil() const
+{
return d_quantEngine->getTermUtil();
}
virtual std::string identify() const = 0;
//----------------------------general queries
/** get currently used the equality engine */
- eq::EqualityEngine * getEqualityEngine();
+ eq::EqualityEngine* getEqualityEngine() const;
/** are n1 and n2 equal in the current used equality engine? */
- bool areEqual( TNode n1, TNode n2 );
+ bool areEqual(TNode n1, TNode n2) const;
/** are n1 and n2 disequal in the current used equality engine? */
- bool areDisequal(TNode n1, TNode n2);
+ bool areDisequal(TNode n1, TNode n2) const;
/** get the representative of n in the current used equality engine */
- TNode getRepresentative( TNode n );
+ TNode getRepresentative(TNode n) const;
/** get quantifiers engine that owns this module */
- QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; }
+ QuantifiersEngine* getQuantifiersEngine() const;
/** get currently used term database */
- quantifiers::TermDb * getTermDatabase();
+ quantifiers::TermDb* getTermDatabase() const;
/** get currently used term utility object */
- quantifiers::TermUtil * getTermUtil();
+ quantifiers::TermUtil* getTermUtil() const;
//----------------------------end general queries
protected:
/** pointer to the quantifiers engine that owns this module */
}
}
-//return a term n' equivalent to n
-// maximal subterms of n' are representatives in the equality engine qy
-Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests ) {
+Node TermDb::evaluateTerm2(TNode n,
+ std::map<TNode, Node>& visited,
+ std::vector<Node>& exp,
+ EqualityQuery* qy,
+ bool useEntailmentTests,
+ bool computeExp,
+ bool reqHasTerm)
+{
std::map< TNode, Node >::iterator itv = visited.find( n );
if( itv != visited.end() ){
return itv->second;
}
+ size_t prevSize = exp.size();
Trace("term-db-eval") << "evaluate term : " << n << std::endl;
Node ret = n;
if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){
//do nothing
- }else if( !qy->hasTerm( n ) ){
- //term is not known to be equal to a representative in equality engine, evaluate it
- if( n.hasOperator() ){
- TNode f = getMatchOperator( n );
- std::vector< TNode > args;
- bool ret_set = false;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- TNode c = evaluateTerm2( n[i], visited, qy, useEntailmentTests );
- if( c.isNull() ){
- ret = Node::null();
+ }
+ else if (qy->hasTerm(n))
+ {
+ Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
+ ret = qy->getRepresentative(n);
+ if (computeExp)
+ {
+ if (n != ret)
+ {
+ exp.push_back(n.eqNode(ret));
+ }
+ }
+ reqHasTerm = false;
+ }
+ else if (n.hasOperator())
+ {
+ std::vector<TNode> args;
+ bool ret_set = false;
+ Kind k = n.getKind();
+ std::vector<Node> tempExp;
+ for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+ {
+ TNode c = evaluateTerm2(n[i],
+ visited,
+ tempExp,
+ qy,
+ useEntailmentTests,
+ computeExp,
+ reqHasTerm);
+ if (c.isNull())
+ {
+ ret = Node::null();
+ ret_set = true;
+ break;
+ }
+ else if (c == d_true || c == d_false)
+ {
+ // short-circuiting
+ if ((k == AND && c == d_false) || (k == OR && c == d_true))
+ {
+ ret = c;
+ ret_set = true;
+ reqHasTerm = false;
+ break;
+ }
+ else if (k == ITE && i == 0)
+ {
+ ret = evaluateTerm2(n[c == d_true ? 1 : 2],
+ visited,
+ tempExp,
+ qy,
+ useEntailmentTests,
+ computeExp,
+ reqHasTerm);
ret_set = true;
+ reqHasTerm = false;
break;
- }else if( c==d_true || c==d_false ){
- //short-circuiting
- if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){
- ret = c;
- ret_set = true;
- break;
- }else if( n.getKind()==kind::ITE && i==0 ){
- ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy, useEntailmentTests );
- ret_set = true;
- break;
+ }
+ }
+ if (computeExp)
+ {
+ exp.insert(exp.end(), tempExp.begin(), tempExp.end());
+ }
+ Trace("term-db-eval") << " child " << i << " : " << c << std::endl;
+ args.push_back(c);
+ }
+ if (ret_set)
+ {
+ // if we short circuited
+ if (computeExp)
+ {
+ exp.clear();
+ exp.insert(exp.end(), tempExp.begin(), tempExp.end());
+ }
+ }
+ else
+ {
+ // get the (indexed) operator of n, if it exists
+ TNode f = getMatchOperator(n);
+ // if it is an indexed term, return the congruent term
+ if (!f.isNull())
+ {
+ // if f is congruent to a term indexed by this class
+ TNode nn = qy->getCongruentTerm(f, args);
+ Trace("term-db-eval") << " got congruent term " << nn
+ << " from DB for " << n << std::endl;
+ if (!nn.isNull())
+ {
+ if (computeExp)
+ {
+ Assert(nn.getNumChildren() == n.getNumChildren());
+ for (unsigned i = 0, nchild = nn.getNumChildren(); i < nchild; i++)
+ {
+ if (nn[i] != n[i])
+ {
+ exp.push_back(nn[i].eqNode(n[i]));
+ }
+ }
+ }
+ ret = qy->getRepresentative(nn);
+ Trace("term-db-eval") << "return rep" << std::endl;
+ ret_set = true;
+ reqHasTerm = false;
+ Assert(!ret.isNull());
+ if (computeExp)
+ {
+ if (n != ret)
+ {
+ exp.push_back(nn.eqNode(ret));
+ }
}
}
- Trace("term-db-eval") << " child " << i << " : " << c << std::endl;
- args.push_back( c );
}
if( !ret_set ){
- //if it is an indexed term, return the congruent term
- if( !f.isNull() ){
- TNode nn = qy->getCongruentTerm( f, args );
- Trace("term-db-eval") << " got congruent term " << nn << " from DB for " << n << std::endl;
- if( !nn.isNull() ){
- ret = qy->getRepresentative( nn );
- Trace("term-db-eval") << "return rep" << std::endl;
- ret_set = true;
- Assert( !ret.isNull() );
- }
+ Trace("term-db-eval") << "return rewrite" << std::endl;
+ // a theory symbol or a new UF term
+ if (n.getMetaKind() == metakind::PARAMETERIZED)
+ {
+ args.insert(args.begin(), n.getOperator());
}
- if( !ret_set ){
- Trace("term-db-eval") << "return rewrite" << std::endl;
- //a theory symbol or a new UF term
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- args.insert( args.begin(), n.getOperator() );
- }
- ret = NodeManager::currentNM()->mkNode( n.getKind(), args );
- ret = Rewriter::rewrite( ret );
- if( ret.getKind()==kind::EQUAL ){
- if( qy->areDisequal( ret[0], ret[1] ) ){
- ret = d_false;
- }
+ ret = NodeManager::currentNM()->mkNode(n.getKind(), args);
+ ret = Rewriter::rewrite(ret);
+ if (ret.getKind() == EQUAL)
+ {
+ if (qy->areDisequal(ret[0], ret[1]))
+ {
+ ret = d_false;
}
- if( useEntailmentTests ){
- if( ret.getKind()==kind::EQUAL || ret.getKind()==kind::GEQ ){
- for( unsigned j=0; j<2; j++ ){
- std::pair<bool, Node> et = d_quantEngine->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, j==0 ? ret : ret.negate() );
- if( et.first ){
- ret = j==0 ? d_true : d_false;
- break;
+ }
+ if (useEntailmentTests)
+ {
+ if (ret.getKind() == EQUAL || ret.getKind() == GEQ)
+ {
+ TheoryEngine* te = d_quantEngine->getTheoryEngine();
+ for (unsigned j = 0; j < 2; j++)
+ {
+ std::pair<bool, Node> et = te->entailmentCheck(
+ THEORY_OF_TYPE_BASED, j == 0 ? ret : ret.negate());
+ if (et.first)
+ {
+ ret = j == 0 ? d_true : d_false;
+ if (computeExp)
+ {
+ exp.push_back(et.second);
}
+ break;
}
}
}
}
}
}
- }else{
- Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
- ret = qy->getRepresentative( n );
}
- Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << std::endl;
+ // must have the term
+ if (reqHasTerm && !ret.isNull())
+ {
+ Kind k = ret.getKind();
+ if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT
+ && k != FORALL)
+ {
+ if (!qy->hasTerm(ret))
+ {
+ ret = Node::null();
+ }
+ }
+ }
+ Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
+ << ", reqHasTerm = " << reqHasTerm << std::endl;
+ // clear the explanation if failed
+ if (computeExp && ret.isNull())
+ {
+ exp.resize(prevSize);
+ }
visited[n] = ret;
return ret;
}
return TNode::null();
}
-Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy, bool useEntailmentTests ) {
+Node TermDb::evaluateTerm(TNode n,
+ EqualityQuery* qy,
+ bool useEntailmentTests,
+ bool reqHasTerm)
+{
if( qy==NULL ){
qy = d_quantEngine->getEqualityQuery();
}
std::map< TNode, Node > visited;
- return evaluateTerm2( n, visited, qy, useEntailmentTests );
+ std::vector<Node> exp;
+ return evaluateTerm2(
+ n, visited, exp, qy, useEntailmentTests, false, reqHasTerm);
+}
+
+Node TermDb::evaluateTerm(TNode n,
+ std::vector<Node>& exp,
+ EqualityQuery* qy,
+ bool useEntailmentTests,
+ bool reqHasTerm)
+{
+ if (qy == NULL)
+ {
+ qy = d_quantEngine->getEqualityQuery();
+ }
+ std::map<TNode, Node> visited;
+ return evaluateTerm2(
+ n, visited, exp, qy, useEntailmentTests, true, reqHasTerm);
}
TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) {
bool inRelevantDomain(TNode f, unsigned i, TNode r);
/** evaluate term
*
- * Returns a term n' such that n = n' is entailed based on the equality
- * information qy. This function may generate new terms. In particular,
- * we typically rewrite maximal
- * subterms of n to terms that exist in the equality engine specified by qy.
- *
- * useEntailmentTests is whether to use the theory engine's entailmentCheck
- * call, for increased precision. This is not frequently used.
- */
+ * Returns a term n' such that n = n' is entailed based on the equality
+ * information qy. This function may generate new terms. In particular,
+ * we typically rewrite subterms of n of maximal size to terms that exist in
+ * the equality engine specified by qy.
+ *
+ * useEntailmentTests is whether to call the theory engine's entailmentTest
+ * on literals n for which this call fails to find a term n' that is
+ * equivalent to n, for increased precision. This is not frequently used.
+ *
+ * The vector exp stores the explanation for why n evaluates to that term,
+ * that is, if this call returns a non-null node n', then:
+ * exp => n = n'
+ *
+ * If reqHasTerm, then we require that the returned term is a Boolean
+ * combination of terms that exist in the equality engine used by this call.
+ * If no such term is constructable, this call returns null. The motivation
+ * for setting this to true is to "fail fast" if we require the return value
+ * of this function to only involve existing terms. This is used e.g. in
+ * the "propagating instances" portion of conflict-based instantiation
+ * (quant_conflict_find.h).
+ */
+ Node evaluateTerm(TNode n,
+ std::vector<Node>& exp,
+ EqualityQuery* qy = NULL,
+ bool useEntailmentTests = false,
+ bool reqHasTerm = false);
+ /** same as above, without exp */
Node evaluateTerm(TNode n,
EqualityQuery* qy = NULL,
- bool useEntailmentTests = false);
+ bool useEntailmentTests = false,
+ bool reqHasTerm = false);
/** get entailed term
*
* If possible, returns a term n' such that:
/** set has term */
void setHasTerm( Node n );
/** helper for evaluate term */
- Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests );
+ Node evaluateTerm2(TNode n,
+ std::map<TNode, Node>& visited,
+ std::vector<Node>& exp,
+ EqualityQuery* qy,
+ bool useEntailmentTests,
+ bool computeExp,
+ bool reqHasTerm);
/** helper for get entailed term */
TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy );
/** helper for is entailed */
projects / cvc5.git / commitdiff