diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 249 |
1 files changed, 189 insertions, 60 deletions
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 ) { |