summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/term_database.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r--src/theory/quantifiers/term_database.cpp249
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 ) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback