diff options
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 68 | ||||
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.h | 20 | ||||
| -rw-r--r-- | src/theory/quantifiers/quant_util.cpp | 23 | ||||
| -rw-r--r-- | src/theory/quantifiers/quant_util.h | 14 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.cpp | 249 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 46 |
6 files changed, 308 insertions, 112 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 203c3d6a7..dc18a2005 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -583,7 +583,9 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node }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++ ){ @@ -591,10 +593,13 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node } 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; } } @@ -615,27 +620,6 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node 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 ); @@ -1047,7 +1031,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) else { d_qni_gterm[i] = d_n[i]; - qi->setGroundSubterm(d_n[i]); } } d_type = d_n.getKind() == EQUAL ? typ_eq : typ_tconstraint; @@ -1058,7 +1041,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) //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 = "; @@ -2211,6 +2193,42 @@ std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e) { 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 */ diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index b40840756..f22910191 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -126,13 +126,9 @@ private: //for completing match 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(); @@ -272,6 +268,22 @@ public: 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); diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index 6d28c574a..01f362d25 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -30,27 +30,38 @@ QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::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(); } diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index 3cfd3b2df..ba59c18e8 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -138,19 +138,19 @@ class QuantifiersModule { 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 */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 51cc15c12..abb84ccd7 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -509,88 +509,196 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { } } -//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; } @@ -645,12 +753,33 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su 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 ) { diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 3cc8dbaa9..fcbd65729 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -178,17 +178,37 @@ class TermDb : public QuantifiersUtil { 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: @@ -307,7 +327,13 @@ class TermDb : public QuantifiersUtil { /** 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 */ |