diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 33 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 2 |
5 files changed, 43 insertions, 3 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 8e6673fb9..1f4d398be 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -39,6 +39,7 @@ d_qe( qe ), d_out( out ), d_use_vts_delta( use_vts_delta ), d_use_vts_inf( use_v d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) ); d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) ); d_true = NodeManager::currentNM()->mkConst( true ); + d_is_nested_quant = false; } void CegInstantiator::computeProgVars( Node n ){ @@ -1202,8 +1203,13 @@ void CegInstantiator::processAssertions() { //collect all assertions from theory for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) { Node lit = (*it).assertion; - d_curr_asserts[tid].push_back( lit ); - Trace("cbqi-proc-debug") << "...add : " << lit << std::endl; + Node atom = lit.getKind()==NOT ? lit[0] : lit; + if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){ + d_curr_asserts[tid].push_back( lit ); + Trace("cbqi-proc-debug") << "...add : " << lit << std::endl; + }else{ + Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl; + } if( lit.getKind()==EQUAL ){ std::map< Node, std::map< Node, Node > >::iterator itae = d_aux_eq.find( lit ); if( itae!=d_aux_eq.end() ){ @@ -1338,6 +1344,25 @@ void CegInstantiator::addToAuxVarSubstitution( std::vector< Node >& subs_lhs, st subs_rhs.push_back( r ); } +void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) { + if( n.getKind()==FORALL ){ + d_is_nested_quant = true; + }else{ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( TermDb::isBoolConnective( n.getKind() ) ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + collectCeAtoms( n[i], visited ); + } + }else{ + if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){ + d_ce_atoms.push_back( n ); + } + } + } + } +} + void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) { Assert( d_vars.empty() ); d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() ); @@ -1367,6 +1392,10 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st } lems[i] = rlem; } + //collect atoms from lem[0]: we will only do bounds coming from original body + d_is_nested_quant = false; + std::map< Node, bool > visited; + collectCeAtoms( lems[0], visited ); } //old implementation diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h index 9b3b15dc5..9fe938f16 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.h +++ b/src/theory/quantifiers/inst_strategy_cbqi.h @@ -65,7 +65,12 @@ private: std::map< Node, std::map< Node, Node > > d_aux_eq; //the CE variables std::vector< Node > d_vars; + //atoms of the CE lemma + bool d_is_nested_quant; + std::vector< Node > d_ce_atoms; private: + //collect atoms + void collectCeAtoms( Node n, std::map< Node, bool >& visited ); //for adding instantiations during check void computeProgVars( Node n ); //solved form, involves substitution with coefficients diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index b7d82bc9e..9e13ef5eb 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1649,7 +1649,7 @@ void MatchGen::setInvalid() { } bool MatchGen::isHandledBoolConnective( TNode n ) { - return n.getType().isBoolean() && ( n.getKind()==OR || n.getKind()==AND || n.getKind()==IFF || n.getKind()==ITE || n.getKind()==FORALL || n.getKind()==NOT ); + return n.getType().isBoolean() && TermDb::isBoolConnective( n.getKind() ); } bool MatchGen::isHandledUfTerm( TNode n ) { diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 366c7ce07..2c9430876 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -1549,6 +1549,10 @@ bool TermDb::isComm( Kind k ) { k==BITVECTOR_PLUS || k==BITVECTOR_MULT || k==BITVECTOR_AND || k==BITVECTOR_OR || k==BITVECTOR_XOR || k==BITVECTOR_XNOR; } +bool TermDb::isBoolConnective( Kind k ) { + return k==OR || k==AND || k==IFF || k==ITE || k==FORALL || k==NOT; +} + void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){ if( std::find( d_op_triggers[op].begin(), d_op_triggers[op].end(), tr )==d_op_triggers[op].end() ){ d_op_triggers[op].push_back( tr ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 682a9f8e0..1b0b72bf9 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -394,6 +394,8 @@ public: static bool isAssoc( Kind k ); /** is comm */ static bool isComm( Kind k ); + /** is bool connective */ + static bool isBoolConnective( Kind k ); //for sygus private: |