diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:30 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-02 09:16:36 -0500 |
commit | f65b945119341ae8afa69bd0b7dc005c9fcc768b (patch) | |
tree | c264125578d3b8edd752740701789f7b1e4e26bb /src/theory/quantifiers/term_database.cpp | |
parent | 53c301aa808218abe725014e01bddc19fe11a116 (diff) |
Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, do not combine quantifier prefixes with annotations. Eliminate use of context-dependent attributes in quantifiers.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 47 |
1 files changed, 28 insertions, 19 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 4dcf0e248..b143286cc 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -84,7 +84,7 @@ void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { } } -TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { +TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_inactive_map( c ), d_op_id_count( 0 ), d_typ_id_count( 0 ) { d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); @@ -178,6 +178,8 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant, bool wi } } } + }else{ + setTermInactive( n ); } rec = true; } @@ -210,7 +212,7 @@ void TermDb::computeUfEqcTerms( TNode f ) { for( unsigned i=0; i<d_op_map[f].size(); i++ ){ TNode n = d_op_map[f][i]; if( hasTermCurrent( n ) ){ - if( !n.getAttribute(NoMatchAttribute()) ){ + if( isTermActive( n ) ){ computeArgReps( n ); TNode r = ee->hasTerm( n ) ? ee->getRepresentative( n ) : n; d_func_map_eqc_trie[f].d_data[r].addTerm( n, d_arg_reps[n] ); @@ -471,6 +473,18 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return isEntailed2( n, subs, subsRep, true, pol, qy ); } +bool TermDb::isTermActive( Node n ) { + return d_inactive_map.find( n )==d_inactive_map.end(); + //return !n.getAttribute(NoMatchAttribute()); +} + +void TermDb::setTermInactive( Node n ) { + d_inactive_map[n] = true; + //Trace("term-db-debug2") << "set no match attribute" << std::endl; + //NoMatchAttribute nma; + //n.setAttribute(nma,true); +} + bool TermDb::hasTermCurrent( Node n, bool useMode ) { if( !useMode ){ return d_has_map.find( n )!=d_has_map.end(); @@ -636,7 +650,7 @@ bool TermDb::reset( Theory::Effort effort ){ Node n = it->second[i]; //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( isTermActive( n ) ){ if( options::finiteModelFind() ){ computeModelBasisArgAttribute( n ); } @@ -651,13 +665,11 @@ bool TermDb::reset( Theory::Effort effort ){ } } Trace("term-db-debug") << std::endl; - if( ee->hasTerm( n ) ){ - Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; - } + Trace("term-db-debug") << " and value : " << ee->getRepresentative( n ) << std::endl; Node at = d_func_map_trie[ it->first ].addOrGetTerm( n, d_arg_reps[n] ); + Trace("term-db-debug2") << "...add term returned " << at << std::endl; if( at!=n && ee->areEqual( at, n ) ){ - NoMatchAttribute nma; - n.setAttribute(nma,true); + setTermInactive( n ); Trace("term-db-debug") << n << " is redundant." << std::endl; congruentCount++; }else{ @@ -846,9 +858,8 @@ void TermDb::makeInstantiationConstantsFor( Node q ){ ic.setAttribute( ivna, i ); InstConstantAttribute ica; ic.setAttribute( ica, q ); - //also set the no-match attribute - NoMatchAttribute nma; - ic.setAttribute(nma,true); + //also set the term inactive + setTermInactive( ic ); } } } @@ -906,11 +917,6 @@ Node TermDb::getInstConstAttr( Node n ) { } InstConstantAttribute ica; n.setAttribute(ica, q); - if( !q.isNull() ){ - //also set the no-match attribute - NoMatchAttribute nma; - n.setAttribute(nma,true); - } } return n.getAttribute(InstConstantAttribute()); } @@ -1019,9 +1025,12 @@ Node TermDb::getCounterexampleLiteral( Node q ){ Node TermDb::getInstConstantNode( Node n, Node q ){ makeInstantiationConstantsFor( q ); - Node n2 = n.substitute( d_vars[q].begin(), d_vars[q].end(), - d_inst_constants[q].begin(), d_inst_constants[q].end() ); - return n2; + return n.substitute( d_vars[q].begin(), d_vars[q].end(), d_inst_constants[q].begin(), d_inst_constants[q].end() ); +} + +Node TermDb::getVariableNode( Node n, Node q ) { + makeInstantiationConstantsFor( q ); + return n.substitute( d_inst_constants[q].begin(), d_inst_constants[q].end(), d_vars[q].begin(), d_vars[q].end() ); } Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) { |