diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-08-31 17:44:42 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-01 09:46:59 -0500 |
commit | 2cadfe31cfddaff7eff4cd220273d0bab3d2792d (patch) | |
tree | 5a519bf9fe2da10e03ec2a4faf167c09ae1792f7 /src/theory/quantifiers/term_database.cpp | |
parent | 07c4b6c27aac497c74695dd559adfee0d9e8e83f (diff) |
Updates to cbqi. New strategy --cbqi-nested-qe to do qe on nested quantifiers during instantiation. Decide on innermost ce lits first, register nested counterexample lemmas eagerly.
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 27 |
1 files changed, 23 insertions, 4 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5d8564adf..f253d655b 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1319,19 +1319,25 @@ bool TermDb::mayComplete( TypeNode tn ) { void TermDb::computeVarContains( Node n, std::vector< Node >& varContains ) { std::map< Node, bool > visited; - computeVarContains2( n, varContains, visited ); + computeVarContains2( n, INST_CONSTANT, varContains, visited ); } -void TermDb::computeVarContains2( Node n, std::vector< Node >& varContains, std::map< Node, bool >& visited ){ +void TermDb::computeQuantContains( Node n, std::vector< Node >& quantContains ) { + std::map< Node, bool > visited; + computeVarContains2( n, FORALL, quantContains, visited ); +} + + +void TermDb::computeVarContains2( Node n, Kind k, std::vector< Node >& varContains, std::map< Node, bool >& visited ){ if( visited.find( n )==visited.end() ){ visited[n] = true; - if( n.getKind()==INST_CONSTANT ){ + if( n.getKind()==k ){ if( std::find( varContains.begin(), varContains.end(), n )==varContains.end() ){ varContains.push_back( n ); } }else{ for( unsigned i=0; i<n.getNumChildren(); i++ ){ - computeVarContains2( n[i], varContains, visited ); + computeVarContains2( n[i], k, varContains, visited ); } } } @@ -2163,6 +2169,10 @@ void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){ qa.d_quant_elim_partial = true; //don't set owner, should happen naturally } + if( avar.hasAttribute(QuantIdNumAttribute()) ){ + qa.d_qid_num = avar.getAttribute(QuantIdNumAttribute()); + Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num << " : " << q << std::endl; + } if( avar.getKind()==REWRITE_RULE ){ Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl; Assert( i==0 ); @@ -2254,6 +2264,15 @@ bool TermDb::isQAttrQuantElimPartial( Node q ) { } } +int TermDb::getQAttrQuantIdNum( Node q ) { + std::map< Node, QAttributes >::iterator it = d_qattr.find( q ); + if( it==d_qattr.end() ){ + return -1; + }else{ + return it->second.d_qid_num; + } +} + TermDbSygus::TermDbSygus( context::Context* c, QuantifiersEngine* qe ) : d_quantEngine( qe ){ d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); |