From: Andrew Reynolds Date: Tue, 16 Oct 2012 21:59:50 +0000 (+0000) Subject: more cleanup of quantifiers code X-Git-Tag: cvc5-1.0.0~7699 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d9d71e0d7885d32ef44fbd08d47b3cccd35ff6f7;p=cvc5.git more cleanup of quantifiers code --- diff --git a/src/theory/arith/theory_arith_instantiator.cpp b/src/theory/arith/theory_arith_instantiator.cpp index 2135f9064..b6c85b7eb 100644 --- a/src/theory/arith/theory_arith_instantiator.cpp +++ b/src/theory/arith/theory_arith_instantiator.cpp @@ -107,9 +107,9 @@ void InstantiatorTheoryArith::assertNode( Node assertion ){ d_quantEngine->addTermToDatabase( assertion ); if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ - setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ - setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) ); } } } @@ -140,7 +140,7 @@ void InstantiatorTheoryArith::processResetInstantiationRound( Theory::Effort eff d_instRows[f].push_back( x ); //this theory has constraints from f Debug("quant-arith") << "Has constraints from " << f << std::endl; - setHasConstraintsFrom( f ); + setQuantifierActive( f ); //set tableaux term if( t.getNumChildren()==0 ){ d_tableaux_term[x] = NodeManager::currentNM()->mkConst( Rational(0) ); diff --git a/src/theory/arrays/theory_arrays_instantiator.cpp b/src/theory/arrays/theory_arrays_instantiator.cpp index b53496f22..a93a01322 100644 --- a/src/theory/arrays/theory_arrays_instantiator.cpp +++ b/src/theory/arrays/theory_arrays_instantiator.cpp @@ -39,9 +39,9 @@ void InstantiatorTheoryArrays::assertNode( Node assertion ){ d_quantEngine->addTermToDatabase( assertion ); if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ - setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ - setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) ); } } } diff --git a/src/theory/datatypes/theory_datatypes_instantiator.cpp b/src/theory/datatypes/theory_datatypes_instantiator.cpp index cc8d9fa30..e9f255c65 100644 --- a/src/theory/datatypes/theory_datatypes_instantiator.cpp +++ b/src/theory/datatypes/theory_datatypes_instantiator.cpp @@ -36,9 +36,9 @@ void InstantiatorTheoryDatatypes::assertNode( Node assertion ){ d_quantEngine->addTermToDatabase( assertion ); if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ - setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ - setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) ); } } } diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index db0eed31e..57b99c59b 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -38,7 +38,9 @@ libquantifiers_la_SOURCES = \ quantifiers_attributes.h \ quantifiers_attributes.cpp \ inst_gen.h \ - inst_gen.cpp + inst_gen.cpp \ + quant_util.h \ + quant_util.cpp EXTRA_DIST = \ kinds \ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 685898515..28eeca624 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -27,7 +27,7 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ), -d_axiom_asserted( c, false ), d_forall_asserts( c ){ +d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){ } diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index df9b55582..c8fcb7c44 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -48,6 +48,8 @@ private: context::CDO< bool > d_axiom_asserted; /** list of quantifiers asserted in the current context */ context::CDList d_forall_asserts; + /** is model set */ + context::CDO< bool > d_isModelSet; public: //for Theory UF: //models for each UF operator std::map< Node, uf::UfModelTree > d_uf_model_tree; @@ -78,9 +80,12 @@ public: virtual ~FirstOrderModel(){} // reset the model void reset(); -public: // initialize the model void initialize( bool considerAxioms = true ); + /** mark model set */ + void markModelSet() { d_isModelSet = true; } + /** is model set */ + bool isModelSet() { return d_isModelSet; } //the following functions are for evaluating quantifier bodies public: /** reset evaluation */ diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp index 324165692..ea58840f5 100755 --- a/src/theory/quantifiers/inst_gen.cpp +++ b/src/theory/quantifiers/inst_gen.cpp @@ -44,8 +44,8 @@ InstGenProcess::InstGenProcess( Node n ) : d_node( n ){ } void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){ - if( !qe->existsInstantiation( f, m, true, true ) ){ - //if( d_inst_trie[val].addInstMatch( qe, f, m, true, NULL, true ) ){ + if( !qe->existsInstantiation( f, m, true ) ){ + //if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){ d_match_values.push_back( val ); d_matches.push_back( InstMatch( &m ) ); //} diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index a74bf0fd5..d00885abf 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -100,8 +100,8 @@ void InstMatch::debugPrint( const char* c ){ } void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){ - for( int i=0; i<(int)qe->getTermDatabase()->d_inst_constants[f].size(); i++ ){ - Node ic = qe->getTermDatabase()->d_inst_constants[f][i]; + for( size_t i=0; igetTermDatabase()->getInstantiationConstant( f, i ); if( d_map.find( ic )==d_map.end() ){ d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic ); } @@ -145,26 +145,6 @@ Node InstMatch::getValue( Node var ){ return Node::null(); } } -/* -void InstMatch::computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match ){ - for( int i=0; i<(int)vars.size(); i++ ){ - std::map< Node, Node >::iterator it = d_map.find( vars[i] ); - if( it!=d_map.end() && !it->second.isNull() ){ - match.push_back( it->second ); - }else{ - match.push_back( qe->getTermDatabase()->getFreeVariableForInstConstant( vars[i] ) ); - } - } -} - -void InstMatch::computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ){ - for( int i=0; i<(int)vars.size(); i++ ){ - if( d_map.find( vars[i] )!=d_map.end() && !d_map[ vars[i] ].isNull() ){ - match.push_back( d_map[ vars[i] ] ); - } - } -} -*/ /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){ @@ -176,7 +156,7 @@ void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, } /** exists match */ -bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio, bool modInst ){ +bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ){ if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){ return true; }else{ @@ -184,7 +164,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) ); std::map< Node, InstMatchTrie >::iterator it = d_data.find( n ); if( it!=d_data.end() ){ - if( it->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){ + if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ return true; } } @@ -194,7 +174,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& Node nl; it = d_data.find( nl ); if( it!=d_data.end() ){ - if( it->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){ + if( it->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ return true; } } @@ -210,7 +190,7 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& if( en!=n ){ std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en ); if( itc!=d_data.end() ){ - if( itc->second.existsInstMatch2( qe, f, m, modEq, index+1, imtio, modInst ) ){ + if( itc->second.existsInstMatch2( qe, f, m, modEq, modInst, index+1, imtio ) ){ return true; } } @@ -223,12 +203,12 @@ bool InstMatchTrie::existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& } } -bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, ImtIndexOrder* imtio, bool modInst ){ - return existsInstMatch2( qe, f, m, modEq, 0, imtio, modInst ); +bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){ + return existsInstMatch2( qe, f, m, modEq, modInst, 0, imtio ); } -bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, ImtIndexOrder* imtio, bool modInst ){ - if( !existsInstMatch( qe, f, m, modEq, imtio, modInst ) ){ +bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, ImtIndexOrder* imtio ){ + if( !existsInstMatch( qe, f, m, modEq, modInst, imtio ) ){ addInstMatch2( qe, f, m, 0, imtio ); return true; }else{ diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index feab91837..a0db1336f 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -122,10 +122,6 @@ public: void makeInternal( QuantifiersEngine* qe ); /** make representative */ void makeRepresentative( QuantifiersEngine* qe ); - /** compute d_match */ - //void computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match ); - /** compute d_match */ - //void computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ); /** get value */ Node getValue( Node var ); /** clear */ @@ -191,7 +187,7 @@ private: /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */ void addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ); /** exists match */ - bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio, bool modInst ); + bool existsInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, bool modInst, int index, ImtIndexOrder* imtio ); public: /** the data */ std::map< Node, InstMatchTrie > d_data; @@ -204,16 +200,16 @@ public: modInst is if we return true if m is an instance of a match that exists */ bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - ImtIndexOrder* imtio = NULL, bool modInst = false ); + bool modInst = false, ImtIndexOrder* imtio = NULL ); /** add match m for quantifier f, take into account equalities if modEq = true, if imtio is non-null, this is the order to add to trie return true if successful */ bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, - ImtIndexOrder* imtio = NULL, bool modInst = false ); + bool modInst = false, ImtIndexOrder* imtio = NULL ); };/* class InstMatchTrie */ -class InstMatchTrieOrdered { +class InstMatchTrieOrdered{ private: InstMatchTrie::ImtIndexOrder* d_imtio; InstMatchTrie d_imt; @@ -226,8 +222,11 @@ public: InstMatchTrie* getTrie() { return &d_imt; } public: /** add match m, return true if successful */ - bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false ){ - return d_imt.addInstMatch( qe, f, m, modEq, d_imtio ); + bool addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ + return d_imt.addInstMatch( qe, f, m, modEq, modInst, d_imtio ); + } + bool existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq = false, bool modInst = false ){ + return d_imt.existsInstMatch( qe, f, m, modEq, modInst, d_imtio ); } };/* class InstMatchTrieOrdered */ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index b402638b1..027ac67eb 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -32,35 +32,6 @@ QuantifiersModule( qe ), d_setIncomplete( setIncomplete ), d_ierCounter( 0 ){ } -bool InstantiationEngine::hasAddedCbqiLemma( Node f ) { - return d_ce_lit.find( f ) != d_ce_lit.end(); -} - -void InstantiationEngine::addCbqiLemma( Node f ){ - Assert( doCbqi( f ) && !hasAddedCbqiLemma( f ) ); - //code for counterexample-based quantifier instantiation - Debug("cbqi") << "Do cbqi for " << f << std::endl; - //make the counterexample body - //Node ceBody = f[1].substitute( d_quantEngine->d_vars[f].begin(), d_quantEngine->d_vars[f].end(), - // d_quantEngine->d_inst_constants[f].begin(), - // d_quantEngine->d_inst_constants[f].end() ); - //get the counterexample literal - Node ceBody = d_quantEngine->getTermDatabase()->getCounterexampleBody( f ); - Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() ); - d_ce_lit[ f ] = ceLit; - d_quantEngine->getTermDatabase()->setInstantiationConstantAttr( ceLit, f ); - // set attributes, mark all literals in the body of n as dependent on cel - //registerLiterals( ceLit, f ); - //require any decision on cel to be phase=true - d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); - Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; - //add counterexample lemma - NodeBuilder<> nb(kind::OR); - nb << f << ceLit; - Node lem = nb; - Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma( lem ); -} bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //if counterexample-based quantifier instantiation is active @@ -70,8 +41,20 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( doCbqi( f ) && !hasAddedCbqiLemma( f ) ){ + d_added_cbqi_lemma[f] = true; + Debug("cbqi") << "Do cbqi for " << f << std::endl; //add cbqi lemma - addCbqiLemma( f ); + //get the counterexample literal + Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); + //require any decision on cel to be phase=true + d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); + Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; + //add counterexample lemma + NodeBuilder<> nb(kind::OR); + nb << f << ceLit; + Node lem = nb; + Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; + d_quantEngine->getOutputChannel().lemma( lem ); addedLemma = true; } } @@ -98,7 +81,7 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( q ); Debug("inst-engine-debug") << "IE: Instantiate " << f << "..." << std::endl; //if this quantifier is active - if( d_quantEngine->getActive( f ) ){ + if( d_quant_active[ f ] ){ //int e_use = d_quantEngine->getRelevance( f )==-1 ? e - 1 : e; int e_use = e; if( e_use>=0 ){ @@ -165,16 +148,12 @@ void InstantiationEngine::check( Theory::Effort e ){ Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl; } bool quantActive = false; - //for each quantifier currently asserted, - // such that the counterexample literal is not in positive in d_counterexample_asserts - // for( BoolMap::iterator i = d_forall_asserts.begin(); i != d_forall_asserts.end(); i++ ) { - // if( (*i).second ) { Debug("quantifiers") << "quantifiers: check: asserted quantifiers size" << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node n = d_quantEngine->getModel()->getAssertedQuantifier( i ); if( options::cbqi() && hasAddedCbqiLemma( n ) ){ - Node cel = d_ce_lit[ n ]; + Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( n ); bool active, value; bool ceValue = false; if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ @@ -183,7 +162,7 @@ void InstantiationEngine::check( Theory::Effort e ){ }else{ active = true; } - d_quantEngine->setActive( n, active ); + d_quant_active[n] = active; if( active ){ Debug("quantifiers") << " Active : " << n; quantActive = true; @@ -203,15 +182,14 @@ void InstantiationEngine::check( Theory::Effort e ){ } Debug("quantifiers") << std::endl; }else{ - d_quantEngine->setActive( n, true ); + d_quant_active[n] = true; quantActive = true; Debug("quantifiers") << " Active : " << n << ", no ce assigned." << std::endl; } Debug("quantifiers-relevance") << "Quantifier : " << n << std::endl; - Debug("quantifiers-relevance") << " Relevance : " << d_quantEngine->getRelevance( n ) << std::endl; - Debug("quantifiers") << " Relevance : " << d_quantEngine->getRelevance( n ) << std::endl; + Debug("quantifiers-relevance") << " Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl; + Debug("quantifiers") << " Relevance : " << d_quantEngine->getQuantifierRelevance()->getRelevance( n ) << std::endl; } - //} if( quantActive ){ bool addedLemmas = doInstantiationRound( e ); //Debug("quantifiers-dec") << "Do instantiation, level = " << d_quantEngine->getValuation().getDecisionLevel() << std::endl; @@ -248,17 +226,17 @@ void InstantiationEngine::check( Theory::Effort e ){ void InstantiationEngine::registerQuantifier( Node f ){ //Notice() << "do cbqi " << f << " ? " << std::endl; - Node ceBody = d_quantEngine->getTermDatabase()->getCounterexampleBody( f ); + Node ceBody = d_quantEngine->getTermDatabase()->getInstConstantBody( f ); if( !doCbqi( f ) ){ d_quantEngine->addTermToDatabase( ceBody, true ); //need to tell which instantiators will be responsible //by default, just chose the UF instantiator - d_quantEngine->getInstantiator( theory::THEORY_UF )->setHasConstraintsFrom( f ); + d_quantEngine->getInstantiator( theory::THEORY_UF )->setQuantifierActive( f ); } //take into account user patterns if( f.getNumChildren()==3 ){ - Node subsPat = d_quantEngine->getTermDatabase()->getSubstitutedNode( f[2], f ); + Node subsPat = d_quantEngine->getTermDatabase()->getInstConstantNode( f[2], f ); //add patterns for( int i=0; i<(int)subsPat.getNumChildren(); i++ ){ //Notice() << "Add pattern " << subsPat[i] << " for " << f << std::endl; @@ -320,22 +298,6 @@ bool InstantiationEngine::doCbqi( Node f ){ -//void InstantiationEngine::registerLiterals( Node n, Node f ){ -// if( n.getAttribute(InstConstantAttribute())==f ){ -// for( int i=0; i<(int)n.getNumChildren(); i++ ){ -// registerLiterals( n[i], f ); -// } -// if( !d_ce_lit[ f ].isNull() ){ -// if( d_quantEngine->d_te->getPropEngine()->isSatLiteral( n ) && n.getKind()!=NOT ){ -// if( n!=d_ce_lit[ f ] && n.notNode()!=d_ce_lit[ f ] ){ -// Debug("quant-dep-dec") << "Make " << n << " dependent on "; -// Debug("quant-dep-dec") << d_ce_lit[ f ] << std::endl; -// d_quantEngine->getOutputChannel().dependentDecision( d_ce_lit[ f ], n ); -// } -// } -// } -// } -//} void InstantiationEngine::debugSat( int reason ){ if( reason==SAT_CBQI ){ @@ -347,7 +309,7 @@ void InstantiationEngine::debugSat( int reason ){ // if( (*i).second ) { for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); - Node cel = d_ce_lit[ f ]; + Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); Assert( !cel.isNull() ); bool value; if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){ @@ -371,26 +333,20 @@ void InstantiationEngine::debugSat( int reason ){ } } -void InstantiationEngine::propagate( Theory::Effort level ){ - //propagate as decision all counterexample literals that are not asserted - for( std::map< Node, Node >::iterator it = d_ce_lit.begin(); it != d_ce_lit.end(); ++it ){ - bool value; - if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){ - //if not already set, propagate as decision - //d_quantEngine->getOutputChannel().propagateAsDecision( it->second ); - Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl; - } - } -} - Node InstantiationEngine::getNextDecisionRequest(){ //propagate as decision all counterexample literals that are not asserted - for( std::map< Node, Node >::iterator it = d_ce_lit.begin(); it != d_ce_lit.end(); ++it ){ - bool value; - if( !d_quantEngine->getValuation().hasSatValue( it->second, value ) ){ - //if not already set, propagate as decision - Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << it->second << std::endl; - return it->second; + if( options::cbqi() ){ + for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); + if( hasAddedCbqiLemma( f ) ){ + Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); + bool value; + if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){ + //if not already set, propagate as decision + Debug("cbqi-prop-as-dec") << "CBQI: propagate as decision " << cel << std::endl; + return cel; + } + } } } return Node::null(); diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 896e17ac8..6d995097a 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -30,16 +30,17 @@ private: typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; /** status of instantiation round (one of InstStrategy::STATUS_*) */ int d_inst_round_status; - /** map from universal quantifiers to their counterexample literals */ - std::map< Node, Node > d_ce_lit; /** whether the instantiation engine should set incomplete if it cannot answer SAT */ bool d_setIncomplete; /** inst round counter */ int d_ierCounter; + /** whether each quantifier is active */ + std::map< Node, bool > d_quant_active; + /** whether we have added cbqi lemma */ + std::map< Node, bool > d_added_cbqi_lemma; private: - bool hasAddedCbqiLemma( Node f ); - void addCbqiLemma( Node f ); -private: + /** has added cbqi lemma */ + bool hasAddedCbqiLemma( Node f ) { return d_added_cbqi_lemma.find( f )!=d_added_cbqi_lemma.end(); } /** helper functions */ bool hasNonArithmeticVariable( Node f ); bool hasApplyUf( Node f ); @@ -65,11 +66,7 @@ public: void registerQuantifier( Node f ); void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } - void propagate( Theory::Effort level ); Node getNextDecisionRequest(); -public: - /** get the corresponding counterexample literal for quantified formula node n */ - Node getCounterexampleLiteralFor( Node f ) { return d_ce_lit.find( f )==d_ce_lit.end() ? Node::null() : d_ce_lit[ f ]; } };/* class InstantiationEngine */ }/* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 6fa02a8d3..3d1ca8f0d 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -51,6 +51,8 @@ void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" ); } TheoryEngineModelBuilder::processBuildModel( m, fullModel ); + //mark that the model has been set + fm->markModelSet(); }else{ d_curr_model = fm; //build model for relevant symbols contained in quantified formulas @@ -338,8 +340,8 @@ void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ) //for each asserted quantifier f, // - determine selection literals // - check which function/predicates have good and bad definitions for satisfying f - for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin(); - it != d_qe->d_phase_reqs[f].end(); ++it ){ + QuantPhaseReq* qpr = d_qe->getPhaseRequirements( f ); + for( std::map< Node, bool >::iterator it = qpr->d_phase_reqs.begin(); it != qpr->d_phase_reqs.end(); ++it ){ //the literal n is phase-required for quantifier f Node n = it->first; Node gn = d_qe->getTermDatabase()->getModelBasis( f, n ); @@ -465,8 +467,10 @@ int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ std::vector< Node > tr_terms; if( lit.getKind()==APPLY_UF ){ //only match predicates that are contrary to this one, use literal matching - Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false ); - d_qe->getTermDatabase()->setInstantiationConstantAttr( eq, f ); + std::vector< Node > children; + children.push_back( lit ); + children.push_back( !phase ? fm->d_true : fm->d_false ); + Node eq = d_qe->getTermDatabase()->mkNodeInstConstant( IFF, children, f ); tr_terms.push_back( eq ); }else if( lit.getKind()==EQUAL ){ //collect trigger terms @@ -532,7 +536,7 @@ void ModelEngineBuilderInstGen::analyzeQuantifiers( FirstOrderModel* fm ){ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){ //determine selection formula, set terms in selection formula as being selected - Node s = getSelectionFormula( d_qe->getTermDatabase()->getCounterexampleBody( f ), + Node s = getSelectionFormula( d_qe->getTermDatabase()->getInstConstantBody( f ), d_qe->getTermDatabase()->getModelBasisBody( f ), true, 0 ); Trace("sel-form") << "Selection formula for " << f << " is " << s << std::endl; if( !s.isNull() ){ @@ -580,7 +584,7 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){ if( !m.isComplete( f ) ){ Trace("inst-gen-debug") << "- partial inst" << std::endl; //if the instantiation does not yet exist - if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true, NULL ) ){ + if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){ //get the partial instantiation pf Node pf = d_qe->getInstantiation( fp, mp ); Trace("inst-gen-pi") << "Partial instantiation of " << f << std::endl; @@ -732,10 +736,10 @@ bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption Node ModelEngineBuilderInstGen::getParentQuantifier( Node f ){ std::map< Node, Node >::iterator it = d_sub_quant_parent.find( f ); - if( it==d_sub_quant_parent.end() ){ + if( it==d_sub_quant_parent.end() || it->second.isNull() ){ return f; }else{ - return getParentQuantifier( it->second ); + return it->second; } } diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 0b73f3c8b..7952d3c21 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -115,7 +115,6 @@ void ModelEngine::check( Theory::Effort e ){ if( options::produceModels() ){ // finish building the model in the standard way d_builder->buildModel( fm, true ); - d_quantEngine->d_model_set = true; } //if the check was incomplete, we must set incomplete flag if( d_incomplete_check ){ @@ -256,7 +255,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){ //if evaluate(...)==1, then the instantiation is already true in the model // depIndex is the index of the least significant variable that this evaluation relies upon depIndex = riter.getNumTerms()-1; - eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), depIndex, &riter ); + eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); if( eval==1 ){ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; }else{ diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index f930fbec7..377fe9aa9 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -64,7 +64,6 @@ public: void registerQuantifier( Node f ); void assertNode( Node f ); Node explain(TNode n){ return Node::null(); } - void propagate( Theory::Effort level ){} void debugPrint( const char* c ); public: /** statistics class */ diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp new file mode 100755 index 000000000..7a2d965b8 --- /dev/null +++ b/src/theory/quantifiers/quant_util.cpp @@ -0,0 +1,144 @@ +/********************* */ +/*! \file quant_util.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: bobot, mdeters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Implementation of quantifier utilities + **/ + +#include "theory/quantifiers/quant_util.h" +#include "theory/quantifiers/inst_match.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; + +void QuantRelevance::registerQuantifier( Node f ){ + //compute symbols in f + std::vector< Node > syms; + computeSymbols( f[1], syms ); + d_syms[f].insert( d_syms[f].begin(), syms.begin(), syms.end() ); + //set initial relevance + int minRelevance = -1; + for( int i=0; i<(int)syms.size(); i++ ){ + d_syms_quants[ syms[i] ].push_back( f ); + int r = getRelevance( syms[i] ); + if( r!=-1 && ( minRelevance==-1 || r& syms ){ + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( std::find( syms.begin(), syms.end(), op )==syms.end() ){ + syms.push_back( op ); + } + } + if( n.getKind()!=FORALL ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + computeSymbols( n[i], syms ); + } + } +} + +/** set relevance */ +void QuantRelevance::setRelevance( Node s, int r ){ + if( d_computeRel ){ + int rOld = getRelevance( s ); + if( rOld==-1 || r phaseReqs2; + computePhaseReqs( n, false, phaseReqs2 ); + for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){ + if( it->second==1 ){ + d_phase_reqs[ it->first ] = true; + }else if( it->second==-1 ){ + d_phase_reqs[ it->first ] = false; + } + } + Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl; + //now, compute if any patterns are equality required + if( computeEq ){ + for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){ + Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl; + if( it->first.getKind()==EQUAL ){ + if( it->first[0].hasAttribute(InstConstantAttribute()) ){ + if( !it->first[1].hasAttribute(InstConstantAttribute()) ){ + d_phase_reqs_equality_term[ it->first[0] ] = it->first[1]; + d_phase_reqs_equality[ it->first[0] ] = it->second; + Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl; + } + }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){ + d_phase_reqs_equality_term[ it->first[1] ] = it->first[0]; + d_phase_reqs_equality[ it->first[1] ] = it->second; + Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl; + } + } + } + } +} + +void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){ + bool newReqPol = false; + bool newPolarity; + if( n.getKind()==NOT ){ + newReqPol = true; + newPolarity = !polarity; + }else if( n.getKind()==OR || n.getKind()==IMPLIES ){ + if( !polarity ){ + newReqPol = true; + newPolarity = false; + } + }else if( n.getKind()==AND ){ + if( polarity ){ + newReqPol = true; + newPolarity = true; + } + }else{ + int val = polarity ? 1 : -1; + if( phaseReqs.find( n )==phaseReqs.end() ){ + phaseReqs[n] = val; + }else if( val!=phaseReqs[n] ){ + phaseReqs[n] = 0; + } + } + if( newReqPol ){ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( n.getKind()==IMPLIES && i==0 ){ + computePhaseReqs( n[i], !newPolarity, phaseReqs ); + }else{ + computePhaseReqs( n[i], newPolarity, phaseReqs ); + } + } + } +} diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h new file mode 100755 index 000000000..1479f910e --- /dev/null +++ b/src/theory/quantifiers/quant_util.h @@ -0,0 +1,77 @@ +/********************* */ +/*! \file quant_util.h + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): mdeters, bobot + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009-2012 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief quantifier util + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__QUANT_UTIL_H +#define __CVC4__THEORY__QUANT_UTIL_H + +#include "theory/theory.h" + +#include +#include +#include + +namespace CVC4 { +namespace theory { + + +class QuantRelevance +{ +private: + /** for computing relavance */ + bool d_computeRel; + /** map from quantifiers to symbols they contain */ + std::map< Node, std::vector< Node > > d_syms; + /** map from symbols to quantifiers */ + std::map< Node, std::vector< Node > > d_syms_quants; + /** relevance for quantifiers and symbols */ + std::map< Node, int > d_relevance; + /** compute symbols */ + void computeSymbols( Node n, std::vector< Node >& syms ); +public: + QuantRelevance( bool cr ) : d_computeRel( cr ){} + ~QuantRelevance(){} + /** register quantifier */ + void registerQuantifier( Node f ); + /** set relevance */ + void setRelevance( Node s, int r ); + /** get relevance */ + int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; } + /** get number of quantifiers for symbol s */ + int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); } +}; + +class QuantPhaseReq +{ +private: + /** helper functions compute phase requirements */ + void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ); +public: + QuantPhaseReq( Node n, bool computeEq = false ); + ~QuantPhaseReq(){} + /** is phase required */ + bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); } + /** get phase requirement */ + bool getPhaseReq( Node lit ) { return d_phase_reqs.find( lit )==d_phase_reqs.end() ? false : d_phase_reqs[ lit ]; } + /** phase requirements for each quantifier for each instantiation literal */ + std::map< Node, bool > d_phase_reqs; + std::map< Node, bool > d_phase_reqs_equality; + std::map< Node, Node > d_phase_reqs_equality_term; +}; + +} +} + +#endif diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index d21ea252c..7bf1f30e9 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -281,11 +281,10 @@ Node QuantifiersRewriter::computeNNF( Node body ){ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, Node& ipl ){ //Notice() << "Compute var elimination for " << f << std::endl; - std::map< Node, bool > litPhaseReq; - QuantifiersEngine::computePhaseReqs( body, false, litPhaseReq ); + QuantPhaseReq qpr( body ); std::vector< Node > vars; std::vector< Node > subs; - for( std::map< Node, bool >::iterator it = litPhaseReq.begin(); it != litPhaseReq.end(); ++it ){ + for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){ //Notice() << " " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl; if( it->first.getKind()==EQUAL ){ if( it->second ){ diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 5261e6876..7b4440c31 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -72,12 +72,12 @@ void RelevantDomain::compute(){ for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ Node f = d_model->getAssertedQuantifier( i ); //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment) - if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, f ) ){ + if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getInstConstantBody( f ), Node::null(), -1, f ) ){ success = false; } //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment) RepDomain range; - if( extendFunctionDomains( d_qe->getTermDatabase()->getCounterexampleBody( f ), range ) ){ + if( extendFunctionDomains( d_qe->getTermDatabase()->getInstConstantBody( f ), range ) ){ success = false; } } diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 0614bb22a..c8c884974 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -259,7 +259,7 @@ Node TermDb::getModelBasis( Node f, Node n ){ Node TermDb::getModelBasisBody( Node f ){ if( d_model_basis_body.find( f )==d_model_basis_body.end() ){ - Node n = getCounterexampleBody( f ); + Node n = getInstConstantBody( f ); d_model_basis_body[f] = getModelBasis( f, n ); } return d_model_basis_body[f]; @@ -301,17 +301,6 @@ void TermDb::makeInstantiationConstantsFor( Node f ){ } } -void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){ - if( !n.hasAttribute(InstLevelAttribute()) ){ - InstLevelAttribute ila; - n.setAttribute(ila,level); - } - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - setInstantiationLevelAttr( n[i], level ); - } -} - - void TermDb::setInstantiationConstantAttr( Node n, Node f ){ if( !n.hasAttribute(InstConstantAttribute()) ){ bool setAttr = false; @@ -336,18 +325,49 @@ void TermDb::setInstantiationConstantAttr( Node n, Node f ){ } -Node TermDb::getCounterexampleBody( Node f ){ - std::map< Node, Node >::iterator it = d_counterexample_body.find( f ); - if( it==d_counterexample_body.end() ){ +Node TermDb::getInstConstantBody( Node f ){ + std::map< Node, Node >::iterator it = d_inst_const_body.find( f ); + if( it==d_inst_const_body.end() ){ makeInstantiationConstantsFor( f ); - Node n = getSubstitutedNode( f[1], f ); - d_counterexample_body[ f ] = n; + Node n = getInstConstantNode( f[1], f ); + d_inst_const_body[ f ] = n; return n; }else{ return it->second; } } +Node TermDb::getCounterexampleLiteral( Node f ){ + if( d_ce_lit.find( f )==d_ce_lit.end() ){ + Node ceBody = getInstConstantBody( f ); + Node ceLit = d_quantEngine->getValuation().ensureLiteral( ceBody.notNode() ); + d_ce_lit[ f ] = ceLit; + setInstantiationConstantAttr( ceLit, f ); + } + return d_ce_lit[ f ]; +} + +Node TermDb::getInstConstantNode( Node n, Node f ){ + return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]); +} + +Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector & vars, + const std::vector & inst_constants){ + Node n2 = n.substitute( vars.begin(), vars.end(), + inst_constants.begin(), + inst_constants.end() ); + setInstantiationConstantAttr( n2, f ); + return n2; +} + +Node TermDb::mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f ){ + Node n = NodeManager::currentNM()->mkNode( k, children ); + setInstantiationConstantAttr( n, f ); + return n; +} + + + Node TermDb::getSkolemizedBody( Node f ){ Assert( f.getKind()==FORALL ); if( d_skolem_body.find( f )==d_skolem_body.end() ){ @@ -367,17 +387,14 @@ Node TermDb::getSkolemizedBody( Node f ){ } -Node TermDb::getSubstitutedNode( Node n, Node f ){ - return convertNodeToPattern(n,f,d_vars[f],d_inst_constants[ f ]); -} - -Node TermDb::convertNodeToPattern( Node n, Node f, const std::vector & vars, - const std::vector & inst_constants){ - Node n2 = n.substitute( vars.begin(), vars.end(), - inst_constants.begin(), - inst_constants.end() ); - setInstantiationConstantAttr( n2, f ); - return n2; +void TermDb::setInstantiationLevelAttr( Node n, uint64_t level ){ + if( !n.hasAttribute(InstLevelAttribute()) ){ + InstLevelAttribute ila; + n.setAttribute(ila,level); + } + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + setInstantiationLevelAttr( n[i], level ); + } } Node TermDb::getFreeVariableForInstConstant( Node n ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 64f3d4980..d63eebf7e 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -109,6 +109,8 @@ public: /* Todo replace int by size_t */ std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction > , NodeHashFunction > d_parents; const std::vector & getParents(TNode n, TNode f, int arg); + +//for model basis private: //map from types to model basis terms std::map< TypeNode, Node > d_model_basis_term; @@ -116,6 +118,8 @@ private: std::map< Node, Node > d_model_basis_op_term; //map from instantiation terms to their model basis equivalent std::map< Node, Node > d_model_basis_body; + /** map from universal quantifiers to model basis terms */ + std::map< Node, std::vector< Node > > d_model_basis_terms; // compute model basis arg void computeModelBasisArgAttribute( Node n ); public: @@ -127,46 +131,37 @@ public: Node getModelBasis( Node f, Node n ); //get model basis body Node getModelBasisBody( Node f ); + +//for inst constant private: - /** map from universal quantifiers to the list of variables */ - std::map< Node, std::vector< Node > > d_vars; - /** map from universal quantifiers to the list of skolem constants */ - std::map< Node, std::vector< Node > > d_skolem_constants; - /** model basis terms */ - std::map< Node, std::vector< Node > > d_model_basis_terms; - /** map from universal quantifiers to their skolemized body */ - std::map< Node, Node > d_skolem_body; + /** map from universal quantifiers to the list of instantiation constants */ + std::map< Node, std::vector< Node > > d_inst_constants; + /** map from universal quantifiers to their inst constant body */ + std::map< Node, Node > d_inst_const_body; + /** map from universal quantifiers to their counterexample literals */ + std::map< Node, Node > d_ce_lit; /** instantiation constants to universal quantifiers */ std::map< Node, Node > d_inst_constants_map; - /** map from universal quantifiers to their counterexample body */ - std::map< Node, Node > d_counterexample_body; - /** free variable for instantiation constant type */ - std::map< TypeNode, Node > d_free_vars; -private: /** make instantiation constants for */ void makeInstantiationConstantsFor( Node f ); -public: - /** map from universal quantifiers to the list of instantiation constants */ - std::map< Node, std::vector< Node > > d_inst_constants; - /** set instantiation level attr */ - void setInstantiationLevelAttr( Node n, uint64_t level ); /** set instantiation constant attr */ void setInstantiationConstantAttr( Node n, Node f ); +public: /** get the i^th instantiation constant of f */ Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; } /** get number of instantiation constants for f */ int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); } /** get the ce body f[e/x] */ - Node getCounterexampleBody( Node f ); - /** get the skolemized body f[e/x] */ - Node getSkolemizedBody( Node f ); + Node getInstConstantBody( Node f ); + /** get counterexample literal (for cbqi) */ + Node getCounterexampleLiteral( Node f ); /** returns node n with bound vars of f replaced by instantiation constants of f node n : is the futur pattern node f : is the quantifier containing which bind the variable return a pattern where the variable are replaced by variable for instantiation. */ - Node getSubstitutedNode( Node n, Node f ); + Node getInstConstantNode( Node n, Node f ); /** same as before but node f is just linked to the new pattern by the applied attribute vars the bind variable @@ -175,15 +170,37 @@ public: Node convertNodeToPattern( Node n, Node f, const std::vector & vars, const std::vector & nvars); + /** get iff term */ + Node getInstConstantIffTerm( Node n, bool pol ); + /** make node, validating the inst constant attribute */ + Node mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f ); + +//for skolem +private: + /** map from universal quantifiers to the list of skolem constants */ + std::map< Node, std::vector< Node > > d_skolem_constants; + /** map from universal quantifiers to their skolemized body */ + std::map< Node, Node > d_skolem_body; +public: + /** get the skolemized body f[e/x] */ + Node getSkolemizedBody( Node f ); + +//miscellaneous +private: + /** map from universal quantifiers to the list of variables */ + std::map< Node, std::vector< Node > > d_vars; + /** free variable for instantiation constant type */ + std::map< TypeNode, Node > d_free_vars; +public: /** get free variable for instantiation constant */ Node getFreeVariableForInstConstant( Node n ); + /** set instantiation level attr */ + void setInstantiationLevelAttr( Node n, uint64_t level ); //for triggers private: /** helper function for compute var contains */ void computeVarContains2( Node n, Node parent ); - /** all triggers will be stored in this trie */ - TrTrie d_tr_trie; /** var contains */ std::map< TNode, std::vector< TNode > > d_var_contains; public: @@ -195,6 +212,10 @@ public: void getVarContains( Node f, std::vector< Node >& pats, std::map< Node, std::vector< Node > >& varContains ); /** get var contains for node n */ void getVarContainsNode( Node f, Node n, std::vector< Node >& varContains ); +private: + /** all triggers will be stored in this trie */ + TrTrie d_tr_trie; +public: /** get trigger */ inst::Trigger* getTrigger( std::vector< Node >& nodes ){ return d_tr_trie.getTrigger( nodes ); } /** add trigger */ diff --git a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp index fc5c66b94..eabb4ceda 100644 --- a/src/theory/quantifiers/theory_quantifiers_instantiator.cpp +++ b/src/theory/quantifiers/theory_quantifiers_instantiator.cpp @@ -34,10 +34,10 @@ void InstantiatorTheoryQuantifiers::assertNode( Node assertion ){ if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ Debug("quant-quant-assert") << " -> has constraints from " << assertion.getAttribute(InstConstantAttribute()) << std::endl; - setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ Debug("quant-quant-assert") << " -> has constraints from " << assertion[0].getAttribute(InstConstantAttribute()) << std::endl; - setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) ); } } } @@ -53,11 +53,9 @@ int InstantiatorTheoryQuantifiers::process( Node f, Theory::Effort effort, int e return InstStrategy::STATUS_UNFINISHED; }else if( e==5 ){ //add random addition - if( isOwnerOf( f ) ){ - InstMatch m; - if( d_quantEngine->addInstantiation( f, m ) ){ - ++(d_statistics.d_instantiations); - } + InstMatch m; + if( d_quantEngine->addInstantiation( f, m ) ){ + ++(d_statistics.d_instantiations); } } return InstStrategy::STATUS_UNKNOWN; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 4d7e93ef2..9d7c8e315 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -34,35 +34,9 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::inst; -//#define COMPUTE_RELEVANCE -//#define REWRITE_ASSERTED_QUANTIFIERS - - /** reset instantiation */ -void InstStrategy::resetInstantiationRound( Theory::Effort effort ){ - d_no_instantiate_temp.clear(); - d_no_instantiate_temp.insert( d_no_instantiate_temp.begin(), d_no_instantiate.begin(), d_no_instantiate.end() ); - processResetInstantiationRound( effort ); -} - -/** do instantiation round method */ -int InstStrategy::doInstantiation( Node f, Theory::Effort effort, int e ){ - if( shouldInstantiate( f ) ){ - int origLemmas = d_quantEngine->getNumLemmasWaiting(); - int retVal = process( f, effort, e ); - if( d_quantEngine->getNumLemmasWaiting()!=origLemmas ){ - for( int i=0; i<(int)d_priority_over.size(); i++ ){ - d_priority_over[i]->d_no_instantiate_temp.push_back( f ); - } - } - return retVal; - }else{ - return STATUS_UNKNOWN; - } -} - QuantifiersEngine::QuantifiersEngine(context::Context* c, TheoryEngine* te): d_te( te ), -d_active( c ){ +d_quant_rel( false ){ //currently do not care about relevance d_eq_query = new EqualityQueryQuantifiersEngine( this ); d_term_db = new quantifiers::TermDb( this ); d_hasAddedLemma = false; @@ -122,8 +96,6 @@ void QuantifiersEngine::check( Theory::Effort e ){ CodeTimer codeTimer(d_time); d_hasAddedLemma = false; - d_model_set = false; - d_resetInstRound = false; if( e==Theory::EFFORT_LAST_CALL ){ ++(d_statistics.d_instantiation_rounds_lc); }else if( e==Theory::EFFORT_FULL ){ @@ -141,7 +113,7 @@ void QuantifiersEngine::check( Theory::Effort e ){ } //build the model if not done so already // this happens if no quantifiers are currently asserted and no model-building module is enabled - if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model_set ){ + if( options::produceModels() && e==Theory::EFFORT_LAST_CALL && !d_hasAddedLemma && !d_model->isModelSet() ){ d_te->getModelBuilder()->buildModel( d_model, true ); } } @@ -161,68 +133,23 @@ std::vector QuantifiersEngine::createInstVariable( std::vector & var void QuantifiersEngine::registerQuantifier( Node f ){ if( std::find( d_quants.begin(), d_quants.end(), f )==d_quants.end() ){ d_quants.push_back( f ); - std::vector< Node > quants; -#ifdef REWRITE_ASSERTED_QUANTIFIERS - //do assertion-time rewriting of quantifier - Node nf = quantifiers::QuantifiersRewriter::rewriteQuant( f, false, false ); - if( nf!=f ){ - Debug("quantifiers-rewrite") << "*** assert-rewrite " << f << std::endl; - Debug("quantifiers-rewrite") << " to " << std::endl; - Debug("quantifiers-rewrite") << nf << std::endl; - //we will instead register all the rewritten quantifiers - if( nf.getKind()==FORALL ){ - quants.push_back( nf ); - }else if( nf.getKind()==AND ){ - for( int i=0; i<(int)nf.getNumChildren(); i++ ){ - quants.push_back( nf[i] ); - } - }else{ - //unhandled: rewrite must go to a quantifier, or conjunction of quantifiers - Assert( false ); - } - }else{ - quants.push_back( f ); + + ++(d_statistics.d_num_quant); + Assert( f.getKind()==FORALL ); + //make instantiation constants for f + d_term_db->makeInstantiationConstantsFor( f ); + //register with quantifier relevance + d_quant_rel.registerQuantifier( f ); + //register with each module + for( int i=0; i<(int)d_modules.size(); i++ ){ + d_modules[i]->registerQuantifier( f ); } -#else - quants.push_back( f ); -#endif - for( int q=0; q<(int)quants.size(); q++ ){ - d_quant_rewritten[f].push_back( quants[q] ); - d_rewritten_quant[ quants[q] ] = f; - ++(d_statistics.d_num_quant); - Assert( quants[q].getKind()==FORALL ); - //register quantifier - d_r_quants.push_back( quants[q] ); - //make instantiation constants for quants[q] - d_term_db->makeInstantiationConstantsFor( quants[q] ); - //compute symbols in quants[q] - std::vector< Node > syms; - computeSymbols( quants[q][1], syms ); - d_syms[quants[q]].insert( d_syms[quants[q]].begin(), syms.begin(), syms.end() ); - //set initial relevance - int minRelevance = -1; - for( int i=0; i<(int)syms.size(); i++ ){ - d_syms_quants[ syms[i] ].push_back( quants[q] ); - int r = getRelevance( syms[i] ); - if( r!=-1 && ( minRelevance==-1 || rregisterQuantifier( quants[q] ); - } - Node ceBody = d_term_db->getCounterexampleBody( quants[q] ); - generatePhaseReqs( quants[q], ceBody ); - //also register it with the strong solver - if( options::finiteModelFind() ){ - ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( quants[q] ); - } + Node ceBody = d_term_db->getInstConstantBody( f ); + //generate the phase requirements + d_phase_reqs[f] = new QuantPhaseReq( ceBody, true ); + //also register it with the strong solver + if( options::finiteModelFind() ){ + ((uf::TheoryUF*)d_te->theoryOf( THEORY_UF ))->getStrongSolver()->registerQuantifier( f ); } } } @@ -236,11 +163,9 @@ void QuantifiersEngine::registerPattern( std::vector & pattern) { void QuantifiersEngine::assertNode( Node f ){ Assert( f.getKind()==FORALL ); - for( int j=0; j<(int)d_quant_rewritten[f].size(); j++ ){ - d_model->assertQuantifier( d_quant_rewritten[f][j] ); - for( int i=0; i<(int)d_modules.size(); i++ ){ - d_modules[i]->assertNode( d_quant_rewritten[f][j] ); - } + d_model->assertQuantifier( f ); + for( int i=0; i<(int)d_modules.size(); i++ ){ + d_modules[i]->assertNode( f ); } } @@ -263,15 +188,12 @@ Node QuantifiersEngine::getNextDecisionRequest(){ } void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){ - //if( !d_resetInstRound ){ - d_resetInstRound = true; for( theory::TheoryId i=theory::THEORY_FIRST; iresetInstantiationRound( level ); } } getTermDatabase()->reset( level ); - //} } void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ @@ -281,16 +203,12 @@ void QuantifiersEngine::addTermToDatabase( Node n, bool withinQuant ){ uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)getInstantiator( THEORY_UF ); d_ith->newTerms(added); } -#ifdef COMPUTE_RELEVANCE //added contains also the Node that just have been asserted in this branch - for( std::set< Node >::iterator i=added.begin(), end=added.end(); - i!=end; i++ ){ + for( std::set< Node >::iterator i=added.begin(), end=added.end(); i!=end; i++ ){ if( !withinQuant ){ - setRelevance( i->getOperator(), 0 ); + d_quant_rel.setRelevance( i->getOperator(), 0 ); } } -#endif - } void QuantifiersEngine::computeTermVector( Node f, InstMatch& m, std::vector< Node >& vars, std::vector< Node >& terms ){ @@ -316,7 +234,7 @@ Node QuantifiersEngine::getInstantiation( Node f, std::vector< Node >& vars, std } Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, uninst_vars ); body = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); - Trace("partial-inst") << "Partial instantiation : " << d_rewritten_quant[f] << std::endl; + Trace("partial-inst") << "Partial instantiation : " << f << std::endl; Trace("partial-inst") << " : " << body << std::endl; } return body; @@ -330,7 +248,7 @@ Node QuantifiersEngine::getInstantiation( Node f, InstMatch& m ){ } bool QuantifiersEngine::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){ - return d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, NULL, modInst ); + return d_inst_match_trie[f].existsInstMatch( this, f, m, modEq, modInst ); } bool QuantifiersEngine::addLemma( Node lem ){ @@ -355,7 +273,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std Node body = getInstantiation( f, vars, terms ); //make the lemma NodeBuilder<> nb(kind::OR); - nb << d_rewritten_quant[f].notNode() << body; + nb << f.notNode() << body; Node lem = nb; //check for duplication if( addLemma( lem ) ){ @@ -462,15 +380,17 @@ void QuantifiersEngine::flushLemmas( OutputChannel* out ){ } void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ - if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE ){ - bool printed = false; + if( options::literalMatchMode()!=quantifiers::LITERAL_MATCH_NONE && d_phase_reqs.find( f )!=d_phase_reqs.end() ){ // doing literal-based matching (consider polarity of literals) for( int i=0; i<(int)nodes.size(); i++ ){ Node prev = nodes[i]; bool nodeChanged = false; - if( isPhaseReq( f, nodes[i] ) ){ - bool preq = getPhaseReq( f, nodes[i] ); - nodes[i] = NodeManager::currentNM()->mkNode( IFF, nodes[i], NodeManager::currentNM()->mkConst(preq) ); + if( d_phase_reqs[f]->isPhaseReq( nodes[i] ) ){ + bool preq = d_phase_reqs[f]->getPhaseReq( nodes[i] ); + std::vector< Node > children; + children.push_back( nodes[i] ); + children.push_back( NodeManager::currentNM()->mkConst(preq) ); + nodes[i] = d_term_db->mkNodeInstConstant( IFF, children, f ); nodeChanged = true; } //else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){ @@ -478,13 +398,7 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ // trNodes[i] = NodeManager::currentNM()->mkNode( EQUAL, trNodes[i], req ); //} if( nodeChanged ){ - if( !printed ){ - Debug("literal-matching") << "LitMatch for " << f << ":" << std::endl; - printed = true; - } Debug("literal-matching") << " Make " << prev << " -> " << nodes[i] << std::endl; - Assert( prev.hasAttribute(InstConstantAttribute()) ); - d_term_db->setInstantiationConstantAttr( nodes[i], prev.getAttribute(InstConstantAttribute()) ); ++(d_statistics.d_lit_phase_req); }else{ ++(d_statistics.d_lit_phase_nreq); @@ -495,76 +409,6 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){ } } -void QuantifiersEngine::computePhaseReqs2( Node n, bool polarity, std::map< Node, int >& phaseReqs ){ - bool newReqPol = false; - bool newPolarity; - if( n.getKind()==NOT ){ - newReqPol = true; - newPolarity = !polarity; - }else if( n.getKind()==OR || n.getKind()==IMPLIES ){ - if( !polarity ){ - newReqPol = true; - newPolarity = false; - } - }else if( n.getKind()==AND ){ - if( polarity ){ - newReqPol = true; - newPolarity = true; - } - }else{ - int val = polarity ? 1 : -1; - if( phaseReqs.find( n )==phaseReqs.end() ){ - phaseReqs[n] = val; - }else if( val!=phaseReqs[n] ){ - phaseReqs[n] = 0; - } - } - if( newReqPol ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( n.getKind()==IMPLIES && i==0 ){ - computePhaseReqs2( n[i], !newPolarity, phaseReqs ); - }else{ - computePhaseReqs2( n[i], newPolarity, phaseReqs ); - } - } - } -} - -void QuantifiersEngine::computePhaseReqs( Node n, bool polarity, std::map< Node, bool >& phaseReqs ){ - std::map< Node, int > phaseReqs2; - computePhaseReqs2( n, polarity, phaseReqs2 ); - for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){ - if( it->second==1 ){ - phaseReqs[ it->first ] = true; - }else if( it->second==-1 ){ - phaseReqs[ it->first ] = false; - } - } -} - -void QuantifiersEngine::generatePhaseReqs( Node f, Node n ){ - computePhaseReqs( n, false, d_phase_reqs[f] ); - Debug("inst-engine-phase-req") << "Phase requirements for " << f << ":" << std::endl; - //now, compute if any patterns are equality required - for( std::map< Node, bool >::iterator it = d_phase_reqs[f].begin(); it != d_phase_reqs[f].end(); ++it ){ - Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl; - if( it->first.getKind()==EQUAL ){ - if( it->first[0].hasAttribute(InstConstantAttribute()) ){ - if( !it->first[1].hasAttribute(InstConstantAttribute()) ){ - d_phase_reqs_equality_term[f][ it->first[0] ] = it->first[1]; - d_phase_reqs_equality[f][ it->first[0] ] = it->second; - Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl; - } - }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){ - d_phase_reqs_equality_term[f][ it->first[1] ] = it->first[0]; - d_phase_reqs_equality[f][ it->first[1] ] = it->second; - Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl; - } - } - } - -} - QuantifiersEngine::Statistics::Statistics(): d_num_quant("QuantifiersEngine::Num_Quantifiers", 0), d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0), @@ -644,39 +488,6 @@ QuantifiersEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_multi_candidates_cache_miss); } -/** compute symbols */ -void QuantifiersEngine::computeSymbols( Node n, std::vector< Node >& syms ){ - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - if( std::find( syms.begin(), syms.end(), op )==syms.end() ){ - syms.push_back( op ); - } - } - if( n.getKind()!=FORALL ){ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - computeSymbols( n[i], syms ); - } - } -} - -/** set relevance */ -void QuantifiersEngine::setRelevance( Node s, int r ){ - int rOld = getRelevance( s ); - if( rOld==-1 || rgetTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine(); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index d0c5832ff..62e5d983e 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -21,6 +21,7 @@ #include "util/hash.h" #include "theory/quantifiers/inst_match.h" #include "theory/rewriterules/rr_inst_match.h" +#include "theory/quantifiers/quant_util.h" #include "util/statistics_registry.h" @@ -36,57 +37,6 @@ namespace theory { class QuantifiersEngine; -class InstStrategy { -public: - enum Status { - STATUS_UNFINISHED, - STATUS_UNKNOWN, - STATUS_SAT, - };/* enum Status */ -protected: - /** reference to the instantiation engine */ - QuantifiersEngine* d_quantEngine; -protected: - /** giving priorities */ - std::vector< InstStrategy* > d_priority_over; - /** do not instantiate list */ - std::vector< Node > d_no_instantiate; - std::vector< Node > d_no_instantiate_temp; - /** reset instantiation */ - virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; - /** process method */ - virtual int process( Node f, Theory::Effort effort, int e ) = 0; -public: - InstStrategy( QuantifiersEngine* ie ) : d_quantEngine( ie ){} - virtual ~InstStrategy(){} - - /** reset instantiation */ - void resetInstantiationRound( Theory::Effort effort ); - /** do instantiation round method */ - int doInstantiation( Node f, Theory::Effort effort, int e ); - /** update status */ - static void updateStatus( int& currStatus, int addStatus ){ - if( addStatus==STATUS_UNFINISHED ){ - currStatus = STATUS_UNFINISHED; - }else if( addStatus==STATUS_UNKNOWN ){ - if( currStatus==STATUS_SAT ){ - currStatus = STATUS_UNKNOWN; - } - } - } - /** identify */ - virtual std::string identify() const { return std::string("Unknown"); } -public: - /** set priority */ - void setPriorityOver( InstStrategy* is ) { d_priority_over.push_back( is ); } - /** set no instantiate */ - void setNoInstantiate( Node n ) { d_no_instantiate.push_back( n ); } - /** should instantiate */ - bool shouldInstantiate( Node n ) { - return std::find( d_no_instantiate_temp.begin(), d_no_instantiate_temp.end(), n )==d_no_instantiate_temp.end(); - } -};/* class InstStrategy */ - class QuantifiersModule { protected: QuantifiersEngine* d_quantEngine; @@ -129,13 +79,13 @@ private: quantifiers::ModelEngine* d_model_engine; /** equality query class */ EqualityQuery* d_eq_query; -public: + /** for computing relevance of quantifiers */ + QuantRelevance d_quant_rel; + /** phase requirements for each quantifier for each instantiation literal */ + std::map< Node, QuantPhaseReq* > d_phase_reqs; +private: /** list of all quantifiers (pre-rewrite) */ std::vector< Node > d_quants; - /** list of all quantifiers (post-rewrite) */ - std::vector< Node > d_r_quants; - /** map from quantifiers to whether they are active */ - BoolMap d_active; /** lemmas produced */ std::map< Node, bool > d_lemmas_produced; /** lemmas waiting */ @@ -150,30 +100,8 @@ public: quantifiers::TermDb* d_term_db; /** extended model object */ quantifiers::FirstOrderModel* d_model; - /** has the model been set? */ - bool d_model_set; - /** has resetInstantiationRound() been called on this check(...) */ - bool d_resetInstRound; - /** universal quantifiers that have been rewritten */ - std::map< Node, std::vector< Node > > d_quant_rewritten; - /** map from rewritten universal quantifiers to the quantifier they are the consequence of */ - std::map< Node, Node > d_rewritten_quant; private: - /** for computing relavance */ - /** map from quantifiers to symbols they contain */ - std::map< Node, std::vector< Node > > d_syms; - /** map from symbols to quantifiers */ - std::map< Node, std::vector< Node > > d_syms_quants; - /** relevance for quantifiers and symbols */ - std::map< Node, int > d_relevance; - /** compute symbols */ - void computeSymbols( Node n, std::vector< Node >& syms ); -private: - /** helper functions compute phase requirements */ - static void computePhaseReqs2( Node n, bool polarity, std::map< Node, int >& phaseReqs ); - KEEP_STATISTIC(TimerStat, d_time, "theory::QuantifiersEngine::time"); - public: QuantifiersEngine(context::Context* c, TheoryEngine* te); ~QuantifiersEngine(); @@ -184,9 +112,7 @@ public: /** get equality query object for the given type. The default is the generic one */ inst::EqualityQuery* getEqualityQuery(TypeNode t); - inst::EqualityQuery* getEqualityQuery() { - return d_eq_query; - } + inst::EqualityQuery* getEqualityQuery() { return d_eq_query; } /** get equality query object for the given type. The default is the one of UF */ rrinst::CandidateGenerator* getRRCanGenClasses(TypeNode t); @@ -204,14 +130,20 @@ public: OutputChannel& getOutputChannel(); /** get default valuation for the quantifiers engine */ Valuation& getValuation(); + /** get quantifier relevance */ + QuantRelevance* getQuantifierRelevance() { return &d_quant_rel; } + /** get phase requirement information */ + QuantPhaseReq* getPhaseRequirements( Node f ) { return d_phase_reqs.find( f )==d_phase_reqs.end() ? NULL : d_phase_reqs[f]; } + /** get phase requirement terms */ + void getPhaseReqTerms( Node f, std::vector< Node >& nodes ); public: /** check at level */ void check( Theory::Effort e ); - /** register (non-rewritten) quantifier */ + /** register quantifier */ void registerQuantifier( Node f ); - /** register (non-rewritten) quantifier */ + /** register quantifier */ void registerPattern( std::vector & pattern); - /** assert (universal) quantifier */ + /** assert universal quantifier */ void assertNode( Node f ); /** propagate */ void propagate( Theory::Effort level ); @@ -253,33 +185,6 @@ public: int getNumQuantifiers() { return (int)d_quants.size(); } /** get quantifier */ Node getQuantifier( int i ) { return d_quants[i]; } - /** set active */ - void setActive( Node n, bool val ) { d_active[n] = val; } - /** get active */ - bool getActive( Node n ) { return d_active.find( n )!=d_active.end() && d_active[n]; } -public: - /** phase requirements for each quantifier for each instantiation literal */ - std::map< Node, std::map< Node, bool > > d_phase_reqs; - std::map< Node, std::map< Node, bool > > d_phase_reqs_equality; - std::map< Node, std::map< Node, Node > > d_phase_reqs_equality_term; -public: - /** is phase required */ - bool isPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )!=d_phase_reqs[f].end(); } - /** get phase requirement */ - bool getPhaseReq( Node f, Node lit ) { return d_phase_reqs[f].find( lit )==d_phase_reqs[f].end() ? false : d_phase_reqs[f][ lit ]; } - /** get term req terms */ - void getPhaseReqTerms( Node f, std::vector< Node >& nodes ); - /** helper functions compute phase requirements */ - static void computePhaseReqs( Node n, bool polarity, std::map< Node, bool >& phaseReqs ); - /** compute phase requirements */ - void generatePhaseReqs( Node f, Node n ); -public: - /** has owner */ - bool hasOwner( Node f ) { return d_owner.find( f )!=d_owner.end(); } - /** get owner */ - Theory* getOwner( Node f ) { return d_owner[f]; } - /** set owner */ - void setOwner( Node f, Theory* t ) { d_owner[f] = t; } public: /** get model */ quantifiers::FirstOrderModel* getModel() { return d_model; } @@ -287,14 +192,6 @@ public: quantifiers::TermDb* getTermDatabase() { return d_term_db; } /** add term to database */ void addTermToDatabase( Node n, bool withinQuant = false ); -private: - /** set relevance */ - void setRelevance( Node s, int r ); -public: - /** get relevance */ - int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; } - /** get number of quantifiers for symbol s */ - int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); } public: /** statistics class */ class Statistics { diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 63a493b07..cdad1e19c 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -186,14 +186,14 @@ Instantiator::~Instantiator() { void Instantiator::resetInstantiationRound(Theory::Effort effort) { for(int i = 0; i < (int) d_instStrategies.size(); ++i) { if(isActiveStrategy(d_instStrategies[i])) { - d_instStrategies[i]->resetInstantiationRound(effort); + d_instStrategies[i]->processResetInstantiationRound(effort); } } processResetInstantiationRound(effort); } int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) { - if(hasConstraintsFrom(f)) { + if( getQuantifierActive(f) ) { int status = process(f, effort, e ); if(d_instStrategies.empty()) { Debug("inst-engine-inst") << "There are no instantiation strategies allocated." << endl; @@ -202,7 +202,7 @@ int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) { if(isActiveStrategy(d_instStrategies[i])) { Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " process " << effort << endl; //call the instantiation strategy's process method - int s_status = d_instStrategies[i]->doInstantiation( f, effort, e ); + int s_status = d_instStrategies[i]->process( f, effort, e ); Debug("inst-engine-inst") << " -> status is " << s_status << endl; InstStrategy::updateStatus(status, s_status); } else { @@ -237,22 +237,6 @@ int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) { // } //} -void Instantiator::setHasConstraintsFrom(Node f) { - d_hasConstraints[f] = true; - if(! d_quantEngine->hasOwner(f)) { - d_quantEngine->setOwner(f, getTheory()); - } else if(d_quantEngine->getOwner(f) != getTheory()) { - d_quantEngine->setOwner(f, NULL); - } -} - -bool Instantiator::hasConstraintsFrom(Node f) { - return d_hasConstraints.find(f) != d_hasConstraints.end() && d_hasConstraints[f]; -} - -bool Instantiator::isOwnerOf(Node f) { - return d_quantEngine->hasOwner(f) && d_quantEngine->getOwner(f) == getTheory(); -} }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 44ee06f91..a57f7646d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -46,7 +46,6 @@ class TheoryEngine; namespace theory { class Instantiator; -class InstStrategy; class QuantifiersEngine; class TheoryModel; @@ -794,6 +793,40 @@ namespace eq{ class EqualityEngine; } +/** instantiation strategy class */ +class InstStrategy { +public: + enum Status { + STATUS_UNFINISHED, + STATUS_UNKNOWN, + STATUS_SAT, + };/* enum Status */ +protected: + /** reference to the instantiation engine */ + QuantifiersEngine* d_quantEngine; +public: + InstStrategy( QuantifiersEngine* qe ) : d_quantEngine( qe ){} + virtual ~InstStrategy(){} + + /** reset instantiation */ + virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; + /** process method, returns a status */ + virtual int process( Node f, Theory::Effort effort, int e ) = 0; + /** update status */ + static void updateStatus( int& currStatus, int addStatus ){ + if( addStatus==STATUS_UNFINISHED ){ + currStatus = STATUS_UNFINISHED; + }else if( addStatus==STATUS_UNKNOWN ){ + if( currStatus==STATUS_SAT ){ + currStatus = STATUS_UNKNOWN; + } + } + } + /** identify */ + virtual std::string identify() const { return std::string("Unknown"); } +};/* class InstStrategy */ + +/** instantiator class */ class Instantiator { friend class QuantifiersEngine; protected: @@ -806,7 +839,7 @@ protected: /** instantiation strategies active */ std::map< InstStrategy*, bool > d_instStrategyActive; /** has constraints from quantifier */ - std::map< Node, bool > d_hasConstraints; + std::map< Node, bool > d_quantActive; /** is instantiation strategy active */ bool isActiveStrategy( InstStrategy* is ) { return d_instStrategyActive.find( is )!=d_instStrategyActive.end() && d_instStrategyActive[is]; @@ -820,13 +853,6 @@ protected: virtual void processResetInstantiationRound( Theory::Effort effort ) = 0; /** process quantifier */ virtual int process( Node f, Theory::Effort effort, int e ) = 0; -public: - /** set has constraints from quantifier f */ - void setHasConstraintsFrom( Node f ); - /** has constraints from */ - bool hasConstraintsFrom( Node f ); - /** is full owner of quantifier f? */ - bool isOwnerOf( Node f ); public: Instantiator(context::Context* c, QuantifiersEngine* qe, Theory* th); virtual ~Instantiator(); @@ -844,6 +870,10 @@ public: /** print debug information */ virtual void debugPrint( const char* c ) {} public: + /** set has constraints from quantifier f */ + void setQuantifierActive( Node f ) { d_quantActive[f] = true; } + /** has constraints from */ + bool getQuantifierActive( Node f ) { return d_quantActive.find(f) != d_quantActive.end() && d_quantActive[f]; } /** reset instantiation round */ void resetInstantiationRound( Theory::Effort effort ); /** do instantiation method*/ diff --git a/src/theory/uf/inst_strategy.cpp b/src/theory/uf/inst_strategy.cpp index 38211ae28..eef2dac79 100644 --- a/src/theory/uf/inst_strategy.cpp +++ b/src/theory/uf/inst_strategy.cpp @@ -36,8 +36,8 @@ using namespace CVC4::theory::inst; struct sortQuantifiersForSymbol { QuantifiersEngine* d_qe; bool operator() (Node i, Node j) { - int nqfsi = d_qe->getNumQuantifiersForSymbol( i.getOperator() ); - int nqfsj = d_qe->getNumQuantifiersForSymbol( j.getOperator() ); + int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() ); + int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() ); if( nqfsinqfsj ){ @@ -223,14 +223,14 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ d_patTerms[0][f].clear(); d_patTerms[1][f].clear(); std::vector< Node > patTermsF; - Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getCounterexampleBody( f ), patTermsF, d_tr_strategy, true ); - Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getCounterexampleBody( f ) << std::endl; + Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, true ); + Debug("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << std::endl; Debug("auto-gen-trigger") << " "; for( int i=0; i<(int)patTermsF.size(); i++ ){ Debug("auto-gen-trigger") << patTermsF[i] << " "; } Debug("auto-gen-trigger") << std::endl; - //extend to literal matching + //extend to literal matching (if applicable) d_quantEngine->getPhaseReqTerms( f, patTermsF ); //sort into single/multi triggers std::map< Node, std::vector< Node > > varContains; @@ -288,7 +288,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ Debug("relevant-trigger") << "Terms based on relevance: " << std::endl; for( int i=0; i<(int)patTerms.size(); i++ ){ Debug("relevant-trigger") << " " << patTerms[i] << " ("; - Debug("relevant-trigger") << d_quantEngine->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl; + Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl; } //Notice() << "Terms based on relevance: " << std::endl; //for( int i=0; i<(int)patTerms.size(); i++ ){ @@ -338,12 +338,12 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ if( index<(int)patTerms.size() ){ //Notice() << "check add additional" << std::endl; //check if similar patterns exist, and if so, add them additionally - int nqfs_curr = d_quantEngine->getNumQuantifiersForSymbol( patTerms[0].getOperator() ); + int nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() ); index++; bool success = true; while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){ success = false; - if( d_quantEngine->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ + if( d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){ d_single_trigger_gen[ patTerms[index] ] = true; Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL, options::smartTriggers() ); diff --git a/src/theory/uf/theory_uf_instantiator.cpp b/src/theory/uf/theory_uf_instantiator.cpp index 40ac4940b..24da83786 100644 --- a/src/theory/uf/theory_uf_instantiator.cpp +++ b/src/theory/uf/theory_uf_instantiator.cpp @@ -126,9 +126,9 @@ void InstantiatorTheoryUf::assertNode( Node assertion ) d_quantEngine->addTermToDatabase( assertion ); if( options::cbqi() ){ if( assertion.hasAttribute(InstConstantAttribute()) ){ - setHasConstraintsFrom( assertion.getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion.getAttribute(InstConstantAttribute()) ); }else if( assertion.getKind()==NOT && assertion[0].hasAttribute(InstConstantAttribute()) ){ - setHasConstraintsFrom( assertion[0].getAttribute(InstConstantAttribute()) ); + setQuantifierActive( assertion[0].getAttribute(InstConstantAttribute()) ); } } } @@ -136,8 +136,8 @@ void InstantiatorTheoryUf::assertNode( Node assertion ) void InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){ if( d_isup ){ d_isup->addUserPattern( f, pat ); + setQuantifierActive( f ); } - setHasConstraintsFrom( f ); }