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()) );
}
}
}
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) );
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()) );
}
}
}
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()) );
}
}
}
quantifiers_attributes.h \
quantifiers_attributes.cpp \
inst_gen.h \
- inst_gen.cpp
+ inst_gen.cpp \
+ quant_util.h \
+ quant_util.cpp
EXTRA_DIST = \
kinds \
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 ){
}
context::CDO< bool > d_axiom_asserted;
/** list of quantifiers asserted in the current context */
context::CDList<Node> 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;
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 */
}\r
\r
void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){\r
- if( !qe->existsInstantiation( f, m, true, true ) ){\r
- //if( d_inst_trie[val].addInstMatch( qe, f, m, true, NULL, true ) ){\r
+ if( !qe->existsInstantiation( f, m, true ) ){\r
+ //if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){\r
d_match_values.push_back( val );\r
d_matches.push_back( InstMatch( &m ) );\r
//}\r
}
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; i<f[0].getNumChildren(); i++ ){
+ Node ic = qe->getTermDatabase()->getInstantiationConstant( f, i );
if( d_map.find( ic )==d_map.end() ){
d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
}
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 ){
}
/** 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{
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;
}
}
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;
}
}
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;
}
}
}
}
-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{
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 */
/** 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;
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;
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 */
}
-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
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;
}
}
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 ){
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 ) ){
}else{
active = true;
}
- d_quantEngine->setActive( n, active );
+ d_quant_active[n] = active;
if( active ){
Debug("quantifiers") << " Active : " << n;
quantActive = true;
}
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;
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;
-//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 ){
// 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 ) ){
}
}
-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();
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 );
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 */
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
//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 );
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
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() ){
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;
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;
}
}
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 ){
//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{
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 */
--- /dev/null
+/********************* */\r
+/*! \file quant_util.cpp\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: bobot, mdeters\r
+ ** Minor contributors (to current version): none\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Implementation of quantifier utilities\r
+ **/\r
+\r
+#include "theory/quantifiers/quant_util.h"\r
+#include "theory/quantifiers/inst_match.h"\r
+\r
+using namespace std;\r
+using namespace CVC4;\r
+using namespace CVC4::kind;\r
+using namespace CVC4::context;\r
+using namespace CVC4::theory;\r
+\r
+void QuantRelevance::registerQuantifier( Node f ){\r
+ //compute symbols in f\r
+ std::vector< Node > syms;\r
+ computeSymbols( f[1], syms );\r
+ d_syms[f].insert( d_syms[f].begin(), syms.begin(), syms.end() );\r
+ //set initial relevance\r
+ int minRelevance = -1;\r
+ for( int i=0; i<(int)syms.size(); i++ ){\r
+ d_syms_quants[ syms[i] ].push_back( f );\r
+ int r = getRelevance( syms[i] );\r
+ if( r!=-1 && ( minRelevance==-1 || r<minRelevance ) ){\r
+ minRelevance = r;\r
+ }\r
+ }\r
+ if( minRelevance!=-1 ){\r
+ setRelevance( f, minRelevance+1 );\r
+ }\r
+}\r
+\r
+\r
+/** compute symbols */\r
+void QuantRelevance::computeSymbols( Node n, std::vector< Node >& syms ){\r
+ if( n.getKind()==APPLY_UF ){\r
+ Node op = n.getOperator();\r
+ if( std::find( syms.begin(), syms.end(), op )==syms.end() ){\r
+ syms.push_back( op );\r
+ }\r
+ }\r
+ if( n.getKind()!=FORALL ){\r
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){\r
+ computeSymbols( n[i], syms );\r
+ }\r
+ }\r
+}\r
+\r
+/** set relevance */\r
+void QuantRelevance::setRelevance( Node s, int r ){\r
+ if( d_computeRel ){\r
+ int rOld = getRelevance( s );\r
+ if( rOld==-1 || r<rOld ){\r
+ d_relevance[s] = r;\r
+ if( s.getKind()==FORALL ){\r
+ for( int i=0; i<(int)d_syms[s].size(); i++ ){\r
+ setRelevance( d_syms[s][i], r );\r
+ }\r
+ }else{\r
+ for( int i=0; i<(int)d_syms_quants[s].size(); i++ ){\r
+ setRelevance( d_syms_quants[s][i], r+1 );\r
+ }\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+\r
+QuantPhaseReq::QuantPhaseReq( Node n, bool computeEq ){\r
+ std::map< Node, int > phaseReqs2;\r
+ computePhaseReqs( n, false, phaseReqs2 );\r
+ for( std::map< Node, int >::iterator it = phaseReqs2.begin(); it != phaseReqs2.end(); ++it ){\r
+ if( it->second==1 ){\r
+ d_phase_reqs[ it->first ] = true;\r
+ }else if( it->second==-1 ){\r
+ d_phase_reqs[ it->first ] = false;\r
+ }\r
+ }\r
+ Debug("inst-engine-phase-req") << "Phase requirements for " << n << ":" << std::endl;\r
+ //now, compute if any patterns are equality required\r
+ if( computeEq ){\r
+ for( std::map< Node, bool >::iterator it = d_phase_reqs.begin(); it != d_phase_reqs.end(); ++it ){\r
+ Debug("inst-engine-phase-req") << " " << it->first << " -> " << it->second << std::endl;\r
+ if( it->first.getKind()==EQUAL ){\r
+ if( it->first[0].hasAttribute(InstConstantAttribute()) ){\r
+ if( !it->first[1].hasAttribute(InstConstantAttribute()) ){\r
+ d_phase_reqs_equality_term[ it->first[0] ] = it->first[1];\r
+ d_phase_reqs_equality[ it->first[0] ] = it->second;\r
+ Debug("inst-engine-phase-req") << " " << it->first[0] << ( it->second ? " == " : " != " ) << it->first[1] << std::endl;\r
+ }\r
+ }else if( it->first[1].hasAttribute(InstConstantAttribute()) ){\r
+ d_phase_reqs_equality_term[ it->first[1] ] = it->first[0];\r
+ d_phase_reqs_equality[ it->first[1] ] = it->second;\r
+ Debug("inst-engine-phase-req") << " " << it->first[1] << ( it->second ? " == " : " != " ) << it->first[0] << std::endl;\r
+ }\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+void QuantPhaseReq::computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs ){\r
+ bool newReqPol = false;\r
+ bool newPolarity;\r
+ if( n.getKind()==NOT ){\r
+ newReqPol = true;\r
+ newPolarity = !polarity;\r
+ }else if( n.getKind()==OR || n.getKind()==IMPLIES ){\r
+ if( !polarity ){\r
+ newReqPol = true;\r
+ newPolarity = false;\r
+ }\r
+ }else if( n.getKind()==AND ){\r
+ if( polarity ){\r
+ newReqPol = true;\r
+ newPolarity = true;\r
+ }\r
+ }else{\r
+ int val = polarity ? 1 : -1;\r
+ if( phaseReqs.find( n )==phaseReqs.end() ){\r
+ phaseReqs[n] = val;\r
+ }else if( val!=phaseReqs[n] ){\r
+ phaseReqs[n] = 0;\r
+ }\r
+ }\r
+ if( newReqPol ){\r
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){\r
+ if( n.getKind()==IMPLIES && i==0 ){\r
+ computePhaseReqs( n[i], !newPolarity, phaseReqs );\r
+ }else{\r
+ computePhaseReqs( n[i], newPolarity, phaseReqs );\r
+ }\r
+ }\r
+ }\r
+}\r
--- /dev/null
+/********************* */\r
+/*! \file quant_util.h\r
+ ** \verbatim\r
+ ** Original author: ajreynol\r
+ ** Major contributors: none\r
+ ** Minor contributors (to current version): mdeters, bobot\r
+ ** This file is part of the CVC4 prototype.\r
+ ** Copyright (c) 2009-2012 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief quantifier util\r
+ **/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__THEORY__QUANT_UTIL_H\r
+#define __CVC4__THEORY__QUANT_UTIL_H\r
+\r
+#include "theory/theory.h"\r
+\r
+#include <ext/hash_set>\r
+#include <iostream>\r
+#include <map>\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+\r
+\r
+class QuantRelevance\r
+{\r
+private:\r
+ /** for computing relavance */\r
+ bool d_computeRel;\r
+ /** map from quantifiers to symbols they contain */\r
+ std::map< Node, std::vector< Node > > d_syms;\r
+ /** map from symbols to quantifiers */\r
+ std::map< Node, std::vector< Node > > d_syms_quants;\r
+ /** relevance for quantifiers and symbols */\r
+ std::map< Node, int > d_relevance;\r
+ /** compute symbols */\r
+ void computeSymbols( Node n, std::vector< Node >& syms );\r
+public:\r
+ QuantRelevance( bool cr ) : d_computeRel( cr ){}\r
+ ~QuantRelevance(){}\r
+ /** register quantifier */\r
+ void registerQuantifier( Node f );\r
+ /** set relevance */\r
+ void setRelevance( Node s, int r );\r
+ /** get relevance */\r
+ int getRelevance( Node s ) { return d_relevance.find( s )==d_relevance.end() ? -1 : d_relevance[s]; }\r
+ /** get number of quantifiers for symbol s */\r
+ int getNumQuantifiersForSymbol( Node s ) { return (int)d_syms_quants[s].size(); }\r
+};\r
+\r
+class QuantPhaseReq\r
+{\r
+private:\r
+ /** helper functions compute phase requirements */\r
+ void computePhaseReqs( Node n, bool polarity, std::map< Node, int >& phaseReqs );\r
+public:\r
+ QuantPhaseReq( Node n, bool computeEq = false );\r
+ ~QuantPhaseReq(){}\r
+ /** is phase required */\r
+ bool isPhaseReq( Node lit ) { return d_phase_reqs.find( lit )!=d_phase_reqs.end(); }\r
+ /** get phase requirement */\r
+ bool getPhaseReq( Node lit ) { return d_phase_reqs.find( lit )==d_phase_reqs.end() ? false : d_phase_reqs[ lit ]; }\r
+ /** phase requirements for each quantifier for each instantiation literal */\r
+ std::map< Node, bool > d_phase_reqs;\r
+ std::map< Node, bool > d_phase_reqs_equality;\r
+ std::map< Node, Node > d_phase_reqs_equality_term;\r
+};\r
+\r
+}\r
+}\r
+\r
+#endif\r
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 ){
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;
}
}
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];
}
}
-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;
}
-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<Node> & vars,
+ const std::vector<Node> & 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() ){
}
-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<Node> & vars,
- const std::vector<Node> & 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 ){
/* 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<Node> & 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;
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:
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
Node convertNodeToPattern( Node n, Node f,
const std::vector<Node> & vars,
const std::vector<Node> & 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:
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 */
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()) );
}
}
}
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;
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;
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 ){
}
//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 );
}
}
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 || r<minRelevance ) ){
- minRelevance = r;
- }
- }
-#ifdef COMPUTE_RELEVANCE
- if( minRelevance!=-1 ){
- setRelevance( quants[q], minRelevance+1 );
- }
-#endif
- //register with each module
- for( int i=0; i<(int)d_modules.size(); i++ ){
- d_modules[i]->registerQuantifier( 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 );
}
}
}
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 );
}
}
}
void QuantifiersEngine::resetInstantiationRound( Theory::Effort level ){
- //if( !d_resetInstRound ){
- d_resetInstRound = true;
for( theory::TheoryId i=theory::THEORY_FIRST; i<theory::THEORY_LAST; ++i ){
if( getInstantiator( i ) ){
getInstantiator( i )->resetInstantiationRound( level );
}
}
getTermDatabase()->reset( level );
- //}
}
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 ){
}
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;
}
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 ){
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 ) ){
}
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<bool>(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<bool>(preq) );
+ nodes[i] = d_term_db->mkNodeInstConstant( IFF, children, f );
nodeChanged = true;
}
//else if( qe->isPhaseReqEquality( f, trNodes[i] ) ){
// 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);
}
}
-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),
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 || r<rOld ){
- d_relevance[s] = r;
- if( s.getKind()==FORALL ){
- for( int i=0; i<(int)d_syms[s].size(); i++ ){
- setRelevance( d_syms[s][i], r );
- }
- }else{
- for( int i=0; i<(int)d_syms_quants[s].size(); i++ ){
- setRelevance( d_syms_quants[s][i], r+1 );
- }
- }
- }
-}
-
-
bool EqualityQueryQuantifiersEngine::hasTerm( Node a ){
eq::EqualityEngine* ee = d_qe->getTheoryEngine()->getSharedTermsDatabase()->getEqualityEngine();
#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"
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;
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 */
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();
/** 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);
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<Node> & pattern);
- /** assert (universal) quantifier */
+ /** assert universal quantifier */
void assertNode( Node f );
/** propagate */
void propagate( Theory::Effort level );
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; }
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 {
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;
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 {
// }
//}
-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 */
namespace theory {
class Instantiator;
-class InstStrategy;
class QuantifiersEngine;
class TheoryModel;
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:
/** 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];
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();
/** 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*/
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( nqfsi<nqfsj ){
return true;
}else if( nqfsi>nqfsj ){
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;
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++ ){
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() );
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()) );
}
}
}
void InstantiatorTheoryUf::addUserPattern( Node f, Node pat ){
if( d_isup ){
d_isup->addUserPattern( f, pat );
+ setQuantifierActive( f );
}
- setHasConstraintsFrom( f );
}
projects / cvc5.git / commitdiff