diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-28 07:01:05 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-28 07:01:12 -0500 |
commit | b9332c2897a354cb2f7275a67cb949770b558d25 (patch) | |
tree | 06a0eb1f5e9427d347ecc93aa38cfede870c6f4f /src/theory/quantifiers/term_database.cpp | |
parent | 7d0e58cf61bdb5d867006b6db90ec956f0968d97 (diff) |
More work on inst propagate. Optimization for qcf to check instances eagerly. Improvements to equality query for disequalities.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 36 |
1 files changed, 25 insertions, 11 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 8b09d8e5d..4dcf0e248 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -237,25 +237,23 @@ 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 ) { +Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests ) { std::map< TNode, Node >::iterator itv = visited.find( n ); if( itv != visited.end() ){ return itv->second; } Trace("term-db-eval") << "evaluate term : " << n << std::endl; - Node ret; - if( n.getKind()==BOUND_VARIABLE ){ - return n; + 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.getKind()==FORALL ){ - ret = Node::null(); - }else if( n.hasOperator() ){ + 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 ); + TNode c = evaluateTerm2( n[i], visited, qy, useEntailmentTests ); if( c.isNull() ){ ret = Node::null(); ret_set = true; @@ -267,7 +265,7 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQ ret_set = true; break; }else if( n.getKind()==kind::ITE && i==0 ){ - ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy ); + ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy, useEntailmentTests ); ret_set = true; break; } @@ -295,6 +293,22 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQ } 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; + } + } + 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; + } + } + } + } } } } @@ -355,12 +369,12 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su return TNode::null(); } -Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy ) { +Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy, bool useEntailmentTests ) { if( qy==NULL ){ qy = d_quantEngine->getEqualityQuery(); } std::map< TNode, Node > visited; - return evaluateTerm2( n, visited, qy ); + return evaluateTerm2( n, visited, qy, useEntailmentTests ); } TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) { |