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.cpp177
1 files changed, 95 insertions, 82 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 763a80af3..3d3646d7d 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -205,67 +205,59 @@ void TermDb::computeUfEqcTerms( TNode f ) {
}
}
-//returns a term n' equivalent to n
-// - if hasSubs = true, then n is consider under substitution subs
-// - if mkNewTerms = true, then n' is either null, or a term in the master equality engine
-Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, std::map< TNode, Node >& visited, EqualityQuery * qy ) {
+//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 ) {
std::map< TNode, Node >::iterator itv = visited.find( n );
if( itv != visited.end() ){
return itv->second;
}
- Node ret;
+ Assert( n.getKind()!=BOUND_VARIABLE );
Trace("term-db-eval") << "evaluate term : " << n << std::endl;
- if( qy->hasTerm( n ) ){
- Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
- ret = qy->getRepresentative( n );
- }else if( n.getKind()==BOUND_VARIABLE ){
- if( hasSubs ){
- Assert( subs.find( n )!=subs.end() );
- Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
- if( subsRep ){
- Assert( qy->hasTerm( subs[n] ) );
- Assert( qy->getRepresentative( subs[n] )==subs[n] );
- ret = subs[n];
- }else{
- ret = evaluateTerm2( subs[n], subs, subsRep, hasSubs, visited, qy );
- }
- }
- }else if( n.getKind()==FORALL ){
- ret = n;
- }else{
- if( n.hasOperator() ){
+ Node ret;
+ 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() ){
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], subs, subsRep, hasSubs, visited, qy );
+ TNode c = evaluateTerm2( n[i], visited, qy );
if( c.isNull() ){
- ret = TNode::null();
+ ret = Node::null();
ret_set = true;
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 );
+ ret_set = true;
+ break;
+ }
}
- Trace("term-db-eval") << "Child " << i << " : " << c << std::endl;
- //short-circuit and/or
- if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){
- ret = c;
- ret_set = true;
- break;
- }else{
- args.push_back( c );
- }
+ 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() ){
- Trace("term-db-eval") << "Get term from DB" << std::endl;
- TNode nn = d_func_map_trie[f].existsTerm( args );
- Trace("term-db-eval") << "Got term " << nn << std::endl;
- if( !nn.isNull() && qy->hasTerm( nn ) ){
- Trace("term-db-eval") << "return rep " << std::endl;
+ 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() );
}
}
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() );
@@ -275,6 +267,9 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe
}
}
}
+ }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;
visited[n] = ret;
@@ -282,22 +277,28 @@ Node TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRe
}
-TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
+TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ) {
Assert( !qy->extendsEngine() );
- Trace("term-db-eval") << "evaluate term : " << n << std::endl;
+ Trace("term-db-entail") << "get entailed term : " << n << std::endl;
if( qy->getEngine()->hasTerm( n ) ){
- Trace("term-db-eval") << "...exists in ee, return rep " << std::endl;
+ Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
return n;
}else if( n.getKind()==BOUND_VARIABLE ){
if( hasSubs ){
Assert( subs.find( n )!=subs.end() );
- Trace("term-db-eval") << "...substitution is : " << subs[n] << std::endl;
+ Trace("term-db-entail") << "...substitution is : " << subs[n] << std::endl;
if( subsRep ){
Assert( qy->getEngine()->hasTerm( subs[n] ) );
Assert( qy->getEngine()->getRepresentative( subs[n] )==subs[n] );
return subs[n];
}else{
- return evaluateTerm2( subs[n], subs, subsRep, hasSubs, qy );
+ return getEntailedTerm2( subs[n], subs, subsRep, hasSubs, qy );
+ }
+ }
+ }else if( n.getKind()==ITE ){
+ for( unsigned i=0; i<2; i++ ){
+ if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
+ return getEntailedTerm2( n[ i==0 ? 1 : 2 ], subs, subsRep, hasSubs, qy );
}
}
}else{
@@ -306,17 +307,16 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR
if( !f.isNull() ){
std::vector< TNode > args;
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- TNode c = evaluateTerm2( n[i], subs, subsRep, hasSubs, qy );
+ TNode c = getEntailedTerm2( n[i], subs, subsRep, hasSubs, qy );
if( c.isNull() ){
return TNode::null();
}
c = qy->getEngine()->getRepresentative( c );
- Trace("term-db-eval") << "Got child : " << c << std::endl;
+ Trace("term-db-entail") << " child " << i << " : " << c << std::endl;
args.push_back( c );
}
- Trace("term-db-eval") << "Get term from DB" << std::endl;
- TNode nn = d_func_map_trie[f].existsTerm( args );
- Trace("term-db-eval") << "Got term " << nn << std::endl;
+ TNode nn = qy->getCongruentTerm( f, args );
+ Trace("term-db-entail") << " got congruent term " << nn << " for " << n << std::endl;
return nn;
}
}
@@ -324,39 +324,37 @@ TNode TermDb::evaluateTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsR
return TNode::null();
}
-Node TermDb::evaluateTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool mkNewTerms, EqualityQuery * qy ) {
+Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy ) {
if( qy==NULL ){
qy = d_quantEngine->getEqualityQuery();
}
- if( mkNewTerms ){
- std::map< TNode, Node > visited;
- return evaluateTerm2( n, subs, subsRep, true, visited, qy );
- }else{
- return evaluateTerm2( n, subs, subsRep, true, qy );
+ std::map< TNode, Node > visited;
+ return evaluateTerm2( n, visited, qy );
+}
+
+TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) {
+ if( qy==NULL ){
+ qy = d_quantEngine->getEqualityQuery();
}
+ return getEntailedTerm2( n, subs, subsRep, true, qy );
}
-Node TermDb::evaluateTerm( TNode n, bool mkNewTerms, EqualityQuery * qy ) {
+TNode TermDb::getEntailedTerm( TNode n, EqualityQuery * qy ) {
if( qy==NULL ){
qy = d_quantEngine->getEqualityQuery();
}
std::map< TNode, TNode > subs;
- if( mkNewTerms ){
- std::map< TNode, Node > visited;
- return evaluateTerm2( n, subs, false, false, visited, qy );
- }else{
- return evaluateTerm2( n, subs, false, false, qy );
- }
+ return getEntailedTerm2( n, subs, false, false, qy );
}
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
+bool TermDb::isEntailed2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, bool pol, EqualityQuery * qy ) {
Assert( !qy->extendsEngine() );
- Trace("term-db-eval") << "Check entailed : " << n << ", pol = " << pol << std::endl;
+ Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
Assert( n.getType().isBoolean() );
if( n.getKind()==EQUAL ){
- TNode n1 = evaluateTerm2( n[0], subs, subsRep, hasSubs, qy );
+ TNode n1 = getEntailedTerm2( n[0], subs, subsRep, hasSubs, qy );
if( !n1.isNull() ){
- TNode n2 = evaluateTerm2( n[1], subs, subsRep, hasSubs, qy );
+ TNode n2 = getEntailedTerm2( n[1], subs, subsRep, hasSubs, qy );
if( !n2.isNull() ){
if( n1==n2 ){
return pol;
@@ -372,11 +370,11 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
}
}
}else if( n.getKind()==NOT ){
- return isEntailed( n[0], subs, subsRep, hasSubs, !pol, qy );
+ return isEntailed2( n[0], subs, subsRep, hasSubs, !pol, qy );
}else if( n.getKind()==OR || n.getKind()==AND ){
bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- if( isEntailed( n[i], subs, subsRep, hasSubs, pol, qy ) ){
+ if( isEntailed2( n[i], subs, subsRep, hasSubs, pol, qy ) ){
if( simPol ){
return true;
}
@@ -389,14 +387,14 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
return !simPol;
}else if( n.getKind()==IFF || n.getKind()==ITE ){
for( unsigned i=0; i<2; i++ ){
- if( isEntailed( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
+ if( isEntailed2( n[0], subs, subsRep, hasSubs, i==0, qy ) ){
unsigned ch = ( n.getKind()==IFF || i==0 ) ? 1 : 2;
bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
- return isEntailed( n[ch], subs, subsRep, hasSubs, reqPol, qy );
+ return isEntailed2( n[ch], subs, subsRep, hasSubs, reqPol, qy );
}
}
}else if( n.getKind()==APPLY_UF ){
- TNode n1 = evaluateTerm2( n, subs, subsRep, hasSubs, qy );
+ TNode n1 = getEntailedTerm2( n, subs, subsRep, hasSubs, qy );
if( !n1.isNull() ){
Assert( qy->hasTerm( n1 ) );
if( n1==d_true ){
@@ -411,16 +409,21 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep,
return false;
}
-bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
+bool TermDb::isEntailed( TNode n, bool pol, EqualityQuery * qy ) {
if( qy==NULL ){
+ Assert( d_consistent_ee );
qy = d_quantEngine->getEqualityQuery();
}
- if( d_consistent_ee ){
- return isEntailed( n, subs, subsRep, true, pol, qy );
- }else{
- //don't check entailment wrt an inconsistent ee
- return false;
+ std::map< TNode, TNode > subs;
+ return isEntailed2( n, subs, false, false, pol, qy );
+}
+
+bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool pol, EqualityQuery * qy ) {
+ if( qy==NULL ){
+ Assert( d_consistent_ee );
+ qy = d_quantEngine->getEqualityQuery();
}
+ return isEntailed2( n, subs, subsRep, true, pol, qy );
}
bool TermDb::hasTermCurrent( Node n, bool useMode ) {
@@ -571,7 +574,13 @@ bool TermDb::reset( Theory::Effort effort ){
}
}
}
-
+ //explicitly add inst closure terms to the equality engine to ensure only EE terms are indexed
+ for( std::hash_set< Node, NodeHashFunction >::iterator it = d_iclosure_processed.begin(); it !=d_iclosure_processed.end(); ++it ){
+ Node n = *it;
+ if( !ee->hasTerm( n ) ){
+ ee->addTerm( n );
+ }
+ }
//rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms
for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){
@@ -579,8 +588,8 @@ bool TermDb::reset( Theory::Effort effort ){
Trace("term-db-debug") << "Adding terms for operator " << it->first << std::endl;
for( unsigned i=0; i<it->second.size(); i++ ){
Node n = it->second[i];
- //to be added to term index, term must be relevant, and either exist in EE or be an inst closure term
- if( hasTermCurrent( n ) && ( ee->hasTerm( n ) || d_iclosure_processed.find( n )!=d_iclosure_processed.end() ) ){
+ //to be added to term index, term must be relevant, and exist in EE
+ if( hasTermCurrent( n ) && ee->hasTerm( n ) ){
if( !n.getAttribute(NoMatchAttribute()) ){
if( options::finiteModelFind() ){
computeModelBasisArgAttribute( n );
@@ -681,11 +690,15 @@ TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) {
}
}
-TNode TermDb::existsTerm( Node f, Node n ) {
+TNode TermDb::getCongruentTerm( Node f, Node n ) {
computeArgReps( n );
return d_func_map_trie[f].existsTerm( d_arg_reps[n] );
}
+TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
+ return d_func_map_trie[f].existsTerm( args );
+}
+
Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
Node mbt;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback