namespace CVC4 {
-CegInstantiation::CegConjecture::CegConjecture() {
+CegInstantiation::CegConjecture::CegConjecture( context::Context* c ) : d_active( c, false ), d_infeasible( c, false ), d_curr_lit( c, 0 ){
+
}
void CegInstantiation::CegConjecture::assign( Node q ) {
d_candidates.push_back( NodeManager::currentNM()->mkSkolem( "e", q[0][i].getType() ) );
}
}
+
void CegInstantiation::CegConjecture::initializeGuard( QuantifiersEngine * qe ){
if( d_guard.isNull() ){
d_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
}
}
-CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ), d_conj_active( c, false ), d_conj_infeasible( c, false ), d_guard_assertions( c ) {
+Node CegInstantiation::CegConjecture::getLiteral( QuantifiersEngine * qe, int i ) {
+ std::map< int, Node >::iterator it = d_lits.find( i );
+ if( it==d_lits.end() ){
+ Node lit = NodeManager::currentNM()->mkNode( LEQ, d_measure_term, NodeManager::currentNM()->mkConst( Rational( i + d_measure_term_size ) ) );
+ lit = Rewriter::rewrite( lit );
+ d_lits[i] = lit;
+
+ Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit, lit.negate() );
+ Trace("cegqi-lemma") << "Fairness split : " << lem << std::endl;
+ qe->getOutputChannel().lemma( lem );
+ qe->getOutputChannel().requirePhase( lit, true );
+ return lit;
+ }else{
+ return it->second;
+ }
+}
+CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
+ d_conj = new CegConjecture( d_quantEngine->getSatContext() );
}
bool CegInstantiation::needsCheck( Theory::Effort e ) {
void CegInstantiation::check( Theory::Effort e, unsigned quant_e ) {
if( quant_e==QuantifiersEngine::QEFFORT_STANDARD ){
Trace("cegqi-engine") << "---Countexample Guided Instantiation Engine---" << std::endl;
- Trace("cegqi-debug") << "Current conjecture status : " << d_conj_active << " " << d_conj_infeasible << std::endl;
- if( d_conj_active && !d_conj_infeasible ){
- checkCegConjecture( &d_conj );
+ Trace("cegqi-engine-debug") << std::endl;
+ Trace("cegqi-engine-debug") << "Current conjecture status : active : " << d_conj->d_active << " feasible : " << !d_conj->d_infeasible << std::endl;
+ if( d_conj->d_active && !d_conj->d_infeasible ){
+ checkCegConjecture( d_conj );
}
Trace("cegqi-engine") << "Finished Countexample Guided Instantiation engine." << std::endl;
}
void CegInstantiation::registerQuantifier( Node q ) {
if( d_quantEngine->getOwner( q )==this ){
- if( !d_conj.isAssigned() ){
+ if( !d_conj->isAssigned() ){
Trace("cegqi") << "Register conjecture : " << q << std::endl;
- d_conj.assign( q );
+ d_conj->assign( q );
//construct base instantiation
- d_conj.d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj.d_candidates ) );
- Trace("cegqi") << "Base instantiation is : " << d_conj.d_base_inst << std::endl;
+ d_conj->d_base_inst = Rewriter::rewrite( d_quantEngine->getInstantiation( q, d_conj->d_candidates ) );
+ Trace("cegqi") << "Base instantiation is : " << d_conj->d_base_inst << std::endl;
if( getTermDatabase()->isQAttrSygus( q ) ){
- Assert( d_conj.d_base_inst.getKind()==NOT );
- Assert( d_conj.d_base_inst[0].getKind()==FORALL );
- for( unsigned j=0; j<d_conj.d_base_inst[0][0].getNumChildren(); j++ ){
- d_conj.d_inner_vars.push_back( d_conj.d_base_inst[0][0][j] );
+ Assert( d_conj->d_base_inst.getKind()==NOT );
+ Assert( d_conj->d_base_inst[0].getKind()==FORALL );
+ for( unsigned j=0; j<d_conj->d_base_inst[0][0].getNumChildren(); j++ ){
+ d_conj->d_inner_vars.push_back( d_conj->d_base_inst[0][0][j] );
}
}else if( getTermDatabase()->isQAttrSynthesis( q ) ){
//add immediate lemma
- Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_base_inst );
+ Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_base_inst );
+ d_quantEngine->getOutputChannel().lemma( lem );
+ }
+ //fairness
+ std::vector< Node > mc;
+ for( unsigned j=0; j<d_conj->d_candidates.size(); j++ ){
+ TypeNode tn = d_conj->d_candidates[j].getType();
+ registerMeasuredType( tn );
+ std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn );
+ if( it!=d_uf_measure.end() ){
+ mc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, it->second, d_conj->d_candidates[j] ) );
+ }
+ }
+ if( !mc.empty() ){
+ d_conj->d_measure_term = mc.size()==1 ? mc[0] : NodeManager::currentNM()->mkNode( PLUS, mc );
+ d_conj->d_measure_term_size = mc.size();
+ Trace("cegqi") << "Measure term is : " << d_conj->d_measure_term << std::endl;
+ //Node ax = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ), d_conj->d_measure_term );
+ //ax = Rewriter::rewrite( ax );
+ //Trace("cegqi-lemma") << "Fairness non-negative axiom : " << ax << std::endl;
+ //d_quantEngine->getOutputChannel().lemma( ax );
}
}else{
- Assert( d_conj.d_quant==q );
+ Assert( d_conj->d_quant==q );
}
}
}
Trace("cegqi-debug") << "Cegqi : Assert : " << n << std::endl;
bool pol = n.getKind()!=NOT;
Node lit = n.getKind()==NOT ? n[0] : n;
- if( lit==d_conj.d_guard ){
- d_guard_assertions[lit] = pol;
- d_conj_infeasible = !pol;
+ if( lit==d_conj->d_guard ){
+ //d_guard_assertions[lit] = pol;
+ d_conj->d_infeasible = !pol;
}
- if( lit==d_conj.d_quant ){
- d_conj_active = true;
+ if( lit==d_conj->d_quant ){
+ d_conj->d_active = true;
}
}
Node CegInstantiation::getNextDecisionRequest() {
- d_conj.initializeGuard( d_quantEngine );
+ d_conj->initializeGuard( d_quantEngine );
bool value;
- if( !d_quantEngine->getValuation().hasSatValue( d_conj.d_guard, value ) ) {
- if( d_guard_assertions.find( d_conj.d_guard )==d_guard_assertions.end() ){
- if( d_conj.d_guard_split.isNull() ){
- Node lem = NodeManager::currentNM()->mkNode( OR, d_conj.d_guard.negate(), d_conj.d_guard );
- d_quantEngine->getOutputChannel().lemma( lem );
+ if( !d_quantEngine->getValuation().hasSatValue( d_conj->d_guard, value ) ) {
+ if( d_conj->d_guard_split.isNull() ){
+ Node lem = NodeManager::currentNM()->mkNode( OR, d_conj->d_guard.negate(), d_conj->d_guard );
+ d_quantEngine->getOutputChannel().lemma( lem );
+ }
+ Trace("cegqi-debug") << "CEGQI : Decide next on : " << d_conj->d_guard << "..." << std::endl;
+ return d_conj->d_guard;
+ }
+ //enforce fairness
+ if( d_conj->isAssigned() ){
+ Node lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+ if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) {
+ if( !value ){
+ d_conj->d_curr_lit.set( d_conj->d_curr_lit.get() + 1 );
+ lit = d_conj->getLiteral( d_quantEngine, d_conj->d_curr_lit.get() );
+ Trace("cegqi-debug") << "CEGQI : Decide on next lit : " << lit << "..." << std::endl;
+ return lit;
}
- Trace("cegqi-debug") << "Decide next on : " << d_conj.d_guard << "..." << std::endl;
- return d_conj.d_guard;
+ }else{
+ Trace("cegqi-debug") << "CEGQI : Decide on current lit : " << lit << "..." << std::endl;
+ return lit;
}
}
+
return Node::null();
}
void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
Node q = conj->d_quant;
- Trace("cegqi-engine-debug") << "Synthesis conjecture : " << q << std::endl;
- Trace("cegqi-engine-debug") << " * Candidate program/output : ";
+ Trace("cegqi-engine") << "Synthesis conjecture : " << q << std::endl;
+ Trace("cegqi-engine") << " * Candidate program/output symbol : ";
for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
- Trace("cegqi-engine-debug") << conj->d_candidates[i] << " ";
+ Trace("cegqi-engine") << conj->d_candidates[i] << " ";
}
- Trace("cegqi-engine-debug") << std::endl;
-
- if( getTermDatabase()->isQAttrSygus( q ) ){
- Trace("cegqi-engine-debug") << " * Values are : ";
- bool success = true;
- std::vector< Node > model_values;
- for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
- Node v = getModelValue( conj->d_candidates[i] );
- model_values.push_back( v );
- Trace("cegqi-engine-debug") << v << " ";
- if( v.isNull() ){
- success = false;
+ Trace("cegqi-engine") << std::endl;
+
+ if( conj->d_ce_sk.empty() ){
+ Trace("cegqi-engine") << " *** Check candidate phase..." << std::endl;
+ if( getTermDatabase()->isQAttrSygus( q ) ){
+
+ std::vector< Node > model_values;
+ if( getModelValues( conj->d_candidates, model_values ) ){
+ //must get a counterexample to the value of the current candidate
+ Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
+ inst = Rewriter::rewrite( inst );
+ //body should be an existential
+ Assert( inst.getKind()==NOT );
+ Assert( inst[0].getKind()==FORALL );
+ //immediately skolemize
+ Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] );
+ Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
+ d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk.negate() ) );
+ conj->d_ce_sk.push_back( inst[0] );
}
- }
- Trace("cegqi-engine-debug") << std::endl;
- if( success ){
- //must get a counterexample to the value of the current candidate
- Node inst = conj->d_base_inst.substitute( conj->d_candidates.begin(), conj->d_candidates.end(), model_values.begin(), model_values.end() );
- inst = Rewriter::rewrite( inst );
- //body should be an existential
- Assert( inst.getKind()==NOT );
- Assert( inst[0].getKind()==FORALL );
- //immediately skolemize
- Node inst_sk = getTermDatabase()->getSkolemizedBody( inst[0] );
- Trace("cegqi-lemma") << "Counterexample lemma : " << inst_sk << std::endl;
- d_quantEngine->addLemma( NodeManager::currentNM()->mkNode( OR, q.negate(), inst_sk ) );
-
- //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate
- Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[inst[0]].size() );
- Node inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(),
- getTermDatabase()->d_skolem_constants[inst[0]].begin(), getTermDatabase()->d_skolem_constants[inst[0]].end() );
- Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine.negate() );
- Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
- d_quantEngine->addLemma( lem );
+ }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
+ std::vector< Node > model_terms;
+ for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
+ Node t = getModelTerm( conj->d_candidates[i] );
+ model_terms.push_back( t );
+ }
+ d_quantEngine->addInstantiation( q, model_terms, false );
}
+ }else{
+ Trace("cegqi-engine") << " *** Refine candidate phase..." << std::endl;
+ for( unsigned j=0; j<conj->d_ce_sk.size(); j++ ){
+ Node ce_q = conj->d_ce_sk[j];
+ Assert( conj->d_inner_vars.size()==getTermDatabase()->d_skolem_constants[ce_q].size() );
+ std::vector< Node > model_values;
+ if( getModelValues( getTermDatabase()->d_skolem_constants[ce_q], model_values ) ){
+ //candidate refinement : the next candidate must satisfy the counterexample found for the current model of the candidate
+ Node inst_ce_refine = conj->d_base_inst[0][1].substitute( conj->d_inner_vars.begin(), conj->d_inner_vars.end(),
+ model_values.begin(), model_values.end() );
+ Node lem = NodeManager::currentNM()->mkNode( OR, conj->d_guard.negate(), inst_ce_refine );
+ Trace("cegqi-lemma") << "Candidate refinement lemma : " << lem << std::endl;
+ d_quantEngine->addLemma( lem );
+ }
+ }
+ conj->d_ce_sk.clear();
+ }
+}
- }else if( getTermDatabase()->isQAttrSynthesis( q ) ){
- std::vector< Node > model_terms;
- for( unsigned i=0; i<conj->d_candidates.size(); i++ ){
- Node t = getModelTerm( conj->d_candidates[i] );
- model_terms.push_back( t );
+bool CegInstantiation::getModelValues( std::vector< Node >& n, std::vector< Node >& v ) {
+ bool success = true;
+ Trace("cegqi-engine") << " * Value is : ";
+ for( unsigned i=0; i<n.size(); i++ ){
+ Node nv = getModelValue( n[i] );
+ v.push_back( nv );
+ Trace("cegqi-engine") << nv << " ";
+ if( nv.isNull() ){
+ success = false;
}
- d_quantEngine->addInstantiation( q, model_terms, false );
}
+ Trace("cegqi-engine") << std::endl;
+ return success;
}
Node CegInstantiation::getModelValue( Node n ) {
}
Node CegInstantiation::getModelTerm( Node n ){
+ //TODO
return getModelValue( n );
}
+void CegInstantiation::registerMeasuredType( TypeNode tn ) {
+ std::map< TypeNode, Node >::iterator it = d_uf_measure.find( tn );
+ if( it==d_uf_measure.end() ){
+ if( tn.isDatatype() ){
+ TypeNode op_tn = NodeManager::currentNM()->mkFunctionType( tn, NodeManager::currentNM()->integerType() );
+ Node op = NodeManager::currentNM()->mkSkolem( "tsize", op_tn, "was created by ceg instantiation to enforce fairness." );
+ d_uf_measure[tn] = op;
+ //cycle through constructors
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+ Node x = NodeManager::currentNM()->mkBoundVar( tn );
+ Node cond = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), x ).negate();
+
+ std::vector< Node > sumc;
+ sumc.push_back( NodeManager::currentNM()->mkConst( Rational(1) ) );
+ for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+ TypeNode tnc = TypeNode::fromType( ((SelectorType)dt[i][j].getSelector().getType()).getRangeType() );
+ if( tnc.isDatatype() ){
+ registerMeasuredType( tnc );
+ sumc.push_back( NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tnc],
+ NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, dt[i][j].getSelector(), x ) ) );
+ }
+ }
+ Node sum = sumc.size()==1 ? sumc[0] : NodeManager::currentNM()->mkNode( PLUS, sumc );
+ Node eq = NodeManager::currentNM()->mkNode( EQUAL, NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tn], x ), sum );
+
+ Node ax = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ),
+ NodeManager::currentNM()->mkNode( OR, cond, eq ) );
+ ax = Rewriter::rewrite( ax );
+ Trace("cegqi-lemma") << "Fairness axiom : " << ax << std::endl;
+ d_quantEngine->getOutputChannel().lemma( ax );
+ }
+ //all are non-negative
+ Node x = NodeManager::currentNM()->mkBoundVar( tn );
+ Node ax = NodeManager::currentNM()->mkNode( FORALL, NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, x ),
+ NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst( Rational(0) ),
+ NodeManager::currentNM()->mkNode( APPLY_UF, d_uf_measure[tn], x ) ) );
+ ax = Rewriter::rewrite( ax );
+ Trace("cegqi-lemma") << "Fairness non-negative axiom : " << ax << std::endl;
+ d_quantEngine->getOutputChannel().lemma( ax );
+ }
+ }
+}
+
}
\ No newline at end of file
namespace theory {
namespace quantifiers {
-
-
class CegInstantiation : public QuantifiersModule
{
typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap;
private:
class CegConjecture {
public:
- CegConjecture();
+ CegConjecture( context::Context* c );
+ /** is conjecture active */
+ context::CDO< bool > d_active;
+ /** is conjecture infeasible */
+ context::CDO< bool > d_infeasible;
/** quantified formula */
Node d_quant;
/** guard */
std::vector< Node > d_candidates;
/** list of variables on inner quantification */
std::vector< Node > d_inner_vars;
- /** is assigned */
- bool isAssigned() { return !d_quant.isNull(); }
- /** assign */
- void assign( Node q );
/** initialize guard */
void initializeGuard( QuantifiersEngine * qe );
+ /** measure term */
+ Node d_measure_term;
+ /** measure sum size */
+ int d_measure_term_size;
+ /** assign */
+ void assign( Node q );
+ /** is assigned */
+ bool isAssigned() { return !d_quant.isNull(); }
+ /** current extential quantifeirs whose couterexamples we must refine */
+ std::vector< Node > d_ce_sk;
+ public: //for fairness
+ /** the cardinality literals */
+ std::map< int, Node > d_lits;
+ /** current cardinality */
+ context::CDO< int > d_curr_lit;
+ /** allocate literal */
+ Node getLiteral( QuantifiersEngine * qe, int i );
+ };
+ class CegFairness {
+ public:
+ CegFairness( context::Context* c );
+ /** which conjecture we are looking at */
+ CegConjecture * d_conj;
+ /** the cardinality literals */
+ std::map< int, Node > d_lits;
+ /** current cardinality */
+ context::CDO< int > d_curr_lit;
+ /** allocate literal */
+ Node getLiteral( int i );
};
/** the quantified formula stating the synthesis conjecture */
- CegConjecture d_conj;
- /** is conjecture active */
- context::CDO< bool > d_conj_active;
- /** is conjecture infeasible */
- context::CDO< bool > d_conj_infeasible;
+ CegConjecture * d_conj;
/** assertions for guards */
- NodeBoolMap d_guard_assertions;
+ //NodeBoolMap d_guard_assertions;
+private: //for enforcing fairness
+ /** measure functions */
+ std::map< TypeNode, Node > d_uf_measure;
+ /** register measured type */
+ void registerMeasuredType( TypeNode tn );
private:
/** check conjecture */
void checkCegConjecture( CegConjecture * conj );
+ /** get model values */
+ bool getModelValues( std::vector< Node >& n, std::vector< Node >& v );
/** get model value */
Node getModelValue( Node n );
/** get model term */
if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){
d_match_values.push_back( val );
d_matches.push_back( InstMatch( &m ) );
- ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->d_instGenMatches++;
+ ((QModelBuilderIG*)qe->getModelBuilder())->d_instGenMatches++;
}
}
}
//for each term we consider, calculate a current match
for( size_t i=0; i<considerTerms.size(); i++ ){
Node n = considerTerms[i];
- bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n );
+ bool isSelected = ((QModelBuilderIG*)qe->getModelBuilder())->isTermSelected( n );
bool hadSuccess CVC4_UNUSED = false;
for( int t=(isSelected ? 0 : 1); t<2; t++ ){
if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
//process all values
for( size_t i=0; i<considerTerms.size(); i++ ){
Node n = considerTerms[i];
- bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->getModelBuilder())->isTermSelected( n );
+ bool isSelected = ((QModelBuilderIG*)qe->getModelBuilder())->isTermSelected( n );
for( int t=(isSelected ? 0 : 1); t<2; t++ ){
//do not consider ground case if it is already congruent to another ground term
if( t==0 || !n.getAttribute(NoMatchAttribute()) ){
}
}
+InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rgfr ) :
+ InstStrategy( qe ), d_tr_strategy( tstrt ){
+ if( rgfr<0 ){
+ d_regenerate = false;
+ }else{
+ d_regenerate_frequency = rgfr;
+ d_regenerate = true;
+ }
+ d_generate_additional = true;
+}
+
void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
//reset triggers
for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger.begin(); it != d_auto_gen_trigger.end(); ++it ){
d_patTerms[1][f].clear();
std::vector< Node > patTermsF;
Trigger::collectPatTerms( d_quantEngine, f, d_quantEngine->getTermDatabase()->getInstConstantBody( f ), patTermsF, d_tr_strategy, d_user_no_gen[f], true );
- Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << ", no-patterns : " << d_user_no_gen.size() << std::endl;
+ Trace("auto-gen-trigger") << "Collected pat terms for " << d_quantEngine->getTermDatabase()->getInstConstantBody( f ) << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
Trace("auto-gen-trigger") << " ";
for( int i=0; i<(int)patTermsF.size(); i++ ){
Trace("auto-gen-trigger") << patTermsF[i] << " ";
std::vector< Node > patTerms;
//try to add single triggers first
for( int i=0; i<(int)d_patTerms[0][f].size(); i++ ){
- if( !d_single_trigger_gen[d_patTerms[0][f][i]] ){
+ if( d_single_trigger_gen.find( d_patTerms[0][f][i] )==d_single_trigger_gen.end() ){
patTerms.push_back( d_patTerms[0][f][i] );
}
}
//if no single triggers exist, add multi trigger terms
- if( patTerms.empty() ){
+ if( patTerms.empty() && ( options::multiTriggerWhenSingle() || d_single_trigger_gen.empty() ) ){
patTerms.insert( patTerms.begin(), d_patTerms[1][f].begin(), d_patTerms[1][f].end() );
}
/** tstrt is the type of triggers to use (maximum depth, minimum depth, or all)
rstrt is the relevance setting for trigger (use only relevant triggers vs. use all)
rgfr is the frequency at which triggers are generated */
- InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rgfr = -1 ) :
- InstStrategy( qe ), d_tr_strategy( tstrt ), d_generate_additional( false ){
- setRegenerateFrequency( rgfr );
- }
+ InstStrategyAutoGenTriggers( QuantifiersEngine* qe, int tstrt, int rgfr = -1 );
~InstStrategyAutoGenTriggers(){}
public:
/** get auto-generated trigger */
inst::Trigger* getAutoGenTrigger( Node f );
/** identify */
std::string identify() const { return std::string("AutoGenTriggers"); }
- /** set regenerate frequency, if fr<0, turn off regenerate */
- void setRegenerateFrequency( int fr ){
- if( fr<0 ){
- d_regenerate = false;
- }else{
- d_regenerate_frequency = fr;
- d_regenerate = true;
- }
- }
- /** set generate additional */
- void setGenerateAdditional( bool val ) { d_generate_additional = val; }
/** add pattern */
void addUserNoPattern( Node f, Node pat );
};/* class InstStrategyAutoGenTriggers */
tstrt = Trigger::TS_MAX_TRIGGER;
}
d_i_ag = new InstStrategyAutoGenTriggers( d_quantEngine, tstrt, 3 );
- d_i_ag->setGenerateAdditional( true );
addInstStrategy( d_i_ag );
//full saturation : instantiate from relevant domain, then arbitrary terms
d_totalLemmas(0)
{
- Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
- if( options::mbqiMode()==MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
- options::mbqiMode()==MBQI_TRUST || options::fmfBoundInt() ){
- Trace("model-engine-debug") << "...make fmc builder." << std::endl;
- d_builder = new fmcheck::FullModelChecker( c, qe );
- }else if( options::mbqiMode()==MBQI_INTERVAL ){
- Trace("model-engine-debug") << "...make interval builder." << std::endl;
- d_builder = new QIntervalBuilder( c, qe );
- }else if( options::mbqiMode()==MBQI_ABS ){
- Trace("model-engine-debug") << "...make abs mbqi builder." << std::endl;
- d_builder = new AbsMbqiBuilder( c, qe );
- }else if( options::mbqiMode()==MBQI_INST_GEN ){
- Trace("model-engine-debug") << "...make inst-gen builder." << std::endl;
- d_builder = new QModelBuilderInstGen( c, qe );
- }else{
- Trace("model-engine-debug") << "...make default model builder." << std::endl;
- d_builder = new QModelBuilderDefault( c, qe );
- }
}
ModelEngine::~ModelEngine() {
- delete d_builder;
+
}
bool ModelEngine::needsCheck( Theory::Effort e ) {
int addedLemmas = 0;
bool needsBuild = true;
FirstOrderModel* fm = d_quantEngine->getModel();
+ quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
if( fm->getNumAssertedQuantifiers()>0 ){
//the following will attempt to build a model and test that it satisfies all asserted universal quantifiers
//quantifiers are initialized, we begin an instantiation round
clSet = double(clock())/double(CLOCKS_PER_SEC);
}
++(d_statistics.d_inst_rounds);
- bool buildAtFullModel = d_builder->optBuildAtFullModel();
+ Assert( mb!=NULL );
+ bool buildAtFullModel = mb->optBuildAtFullModel();
needsBuild = !buildAtFullModel;
//two effort levels: first try exhaustive instantiation without axioms, then with.
int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0;
Trace("model-engine") << "---Model Engine Round---" << std::endl;
//initialize the model
Trace("model-engine-debug") << "Build model..." << std::endl;
- d_builder->d_considerAxioms = effort>=1;
- d_builder->d_addedLemmas = 0;
- d_builder->buildModel( fm, buildAtFullModel );
- addedLemmas += (int)d_builder->d_addedLemmas;
+ mb->d_considerAxioms = effort>=1;
+ mb->d_addedLemmas = 0;
+ mb->buildModel( fm, buildAtFullModel );
+ addedLemmas += (int)mb->d_addedLemmas;
//if builder has lemmas, add and return
if( addedLemmas==0 ){
Trace("model-engine-debug") << "Verify uf ss is minimal..." << std::endl;
debugPrint("fmf-consistent");
if( options::produceModels() && needsBuild ){
// finish building the model
- d_builder->buildModel( fm, true );
+ mb->buildModel( fm, true );
}
//if the check was incomplete, we must set incomplete flag
if( d_incomplete_check ){
int ModelEngine::checkModel(){
FirstOrderModel* fm = d_quantEngine->getModel();
+ quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
//flatten the representatives
//Trace("model-engine-debug") << "Flattening representatives...." << std::endl;
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
//determine if we should check this quantifier
- if( d_builder->isQuantifierActive( f ) ){
+ if( mb->isQuantifierActive( f ) ){
exhaustiveInstantiate( f, e );
if( Trace.isOn("model-engine-warn") ){
if( d_addedLemmas>10000 ){
}
}
//print debug information
- Trace("model-engine-debug") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
+ Trace("model-engine-debug") << "Instantiate axioms : " << ( mb->d_considerAxioms ? "yes" : "no" ) << std::endl;
Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
Trace("model-engine") << d_totalLemmas << std::endl;
return d_addedLemmas;
void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
//first check if the builder can do the exhaustive instantiation
- d_builder->d_triedLemmas = 0;
- d_builder->d_addedLemmas = 0;
- d_builder->d_incomplete_check = false;
- if( d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
+ quantifiers::QModelBuilder * mb = d_quantEngine->getModelBuilder();
+ mb->d_triedLemmas = 0;
+ mb->d_addedLemmas = 0;
+ mb->d_incomplete_check = false;
+ if( mb->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort ) ){
Trace("inst-fmf-ei") << "-> Builder determined instantiation(s)." << std::endl;
- d_triedLemmas += d_builder->d_triedLemmas;
- d_addedLemmas += d_builder->d_addedLemmas;
- d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check;
- d_statistics.d_mbqi_inst_lemmas += d_builder->d_addedLemmas;
+ d_triedLemmas += mb->d_triedLemmas;
+ d_addedLemmas += mb->d_addedLemmas;
+ d_incomplete_check = d_incomplete_check || mb->d_incomplete_check;
+ d_statistics.d_mbqi_inst_lemmas += mb->d_addedLemmas;
}else{
Trace("inst-fmf-ei") << "-> Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
Debug("inst-fmf-ei") << " Instantiation Constants: ";
for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
Node f = d_quantEngine->getModel()->getAssertedQuantifier( i );
Trace( c ) << " ";
- if( !d_builder->isQuantifierActive( f ) ){
+ if( !d_quantEngine->getModelBuilder()->isQuantifierActive( f ) ){
Trace( c ) << "*Inactive* ";
}else{
Trace( c ) << " ";
class ModelEngine : public QuantifiersModule
{
friend class RepSetIterator;
-private:
- /** builder class */
- QModelBuilder* d_builder;
private:
//options
bool optOneQuantPerRound();
public:
ModelEngine( context::Context* c, QuantifiersEngine* qe );
virtual ~ModelEngine();
- //get the builder
- QModelBuilder* getModelBuilder() { return d_builder; }
public:
bool needsCheck( Theory::Effort e );
void check( Theory::Effort e, unsigned quant_e );
choose relational triggers such as x = f(y), x >= f(y)
option purifyTriggers --purify-triggers bool :default false :read-write
purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1
+option multiTriggerWhenSingle --multi-trigger-when-single bool :default true
+ never select multi-triggers when single triggers exist
option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToTriggerSelMode :handler-include "theory/quantifiers/options_handlers.h"
selection mode for triggers
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/trigger.h"
-//#include "theory/rewriterules/efficient_e_matching.h"
-//#include "theory/rewriterules/rr_trigger.h"
#include "theory/quantifiers/bounded_integers.h"
#include "theory/quantifiers/rewrite_engine.h"
#include "theory/quantifiers/quant_conflict_find.h"
#include "theory/quantifiers/relevant_domain.h"
#include "theory/uf/options.h"
#include "theory/uf/theory_uf.h"
+#include "theory/quantifiers/full_model_check.h"
+#include "theory/quantifiers/qinterval_builder.h"
+#include "theory/quantifiers/ambqi_builder.h"
using namespace std;
using namespace CVC4;
eq::EqualityEngine * QuantifiersModule::getEqualityEngine() {
- return d_quantEngine->getTheoryEngine()->getMasterEqualityEngine();
+ return d_quantEngine->getMasterEqualityEngine();
}
bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) {
//d_rr_tr_trie = new rrinst::TriggerTrie;
//d_eem = new EfficientEMatcher( this );
d_hasAddedLemma = false;
-
+
+ bool needsBuilder = false;
+
Trace("quant-engine-debug") << "Initialize model, mbqi : " << options::mbqiMode() << std::endl;
//the model object
}
d_model_engine = new quantifiers::ModelEngine( c, this );
d_modules.push_back( d_model_engine );
+ needsBuilder = true;
}else{
d_model_engine = NULL;
d_bint = NULL;
}else{
d_ceg_inst = NULL;
}
+
+ if( needsBuilder ){
+ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl;
+ if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ||
+ options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBoundInt() ){
+ Trace("quant-engine-debug") << "...make fmc builder." << std::endl;
+ d_builder = new quantifiers::fmcheck::FullModelChecker( c, this );
+ }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
+ Trace("quant-engine-debug") << "...make interval builder." << std::endl;
+ d_builder = new quantifiers::QIntervalBuilder( c, this );
+ }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
+ Trace("quant-engine-debug") << "...make abs mbqi builder." << std::endl;
+ d_builder = new quantifiers::AbsMbqiBuilder( c, this );
+ }else if( options::mbqiMode()==quantifiers::MBQI_INST_GEN ){
+ Trace("quant-engine-debug") << "...make inst-gen builder." << std::endl;
+ d_builder = new quantifiers::QModelBuilderInstGen( c, this );
+ }else{
+ Trace("quant-engine-debug") << "...make default model builder." << std::endl;
+ d_builder = new quantifiers::QModelBuilderDefault( c, this );
+ }
+ }else{
+ d_builder = NULL;
+ }
//options
d_total_inst_count_debug = 0;
}
QuantifiersEngine::~QuantifiersEngine(){
+ delete d_builder;
delete d_rr_engine;
delete d_bint;
delete d_model_engine;
delete d_tr_trie;
delete d_term_db;
delete d_eq_query;
+ delete d_sg_gen;
+ delete d_ceg_inst;
for(std::map< Node, QuantPhaseReq* >::iterator i = d_phase_reqs.begin(); i != d_phase_reqs.end(); ++i) {
delete (*i).second;
}
}
}
-QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
+QuantifiersModule * QuantifiersEngine::getOwner( Node q ) {
std::map< Node, QuantifiersModule * >::iterator it = d_owner.find( q );
if( it==d_owner.end() ){
return NULL;
if( mo!=NULL ){
Trace("quant-warn") << "WARNING: setting owner of " << q << " to " << ( m ? m->identify() : "null" ) << ", but already has owner " << mo->identify() << "!" << std::endl;
}
- d_owner[q] = m;
+ d_owner[q] = m;
}
}
Trace("quant-engine-debug") << " # quantified formulas = " << d_model->getNumAssertedQuantifiers() << std::endl;
Trace("quant-engine-debug") << " Theory engine finished : " << !d_te->needCheck() << std::endl;
+ Trace("quant-engine-ee") << "Equality engine : " << std::endl;
+ debugPrintEqualityEngine( "quant-engine-ee" );
+
if( !getMasterEqualityEngine()->consistent() ){
Trace("quant-engine") << "Master equality engine not consistent, return." << std::endl;
return;
}
}
}
- //also check model engine (it may contain instantiations internally)
- if( d_model_engine->getModelBuilder()->existsInstantiation( f, m, modEq, modInst ) ){
+ //also check model builder (it may contain instantiations internally)
+ if( d_builder && d_builder->existsInstantiation( f, m, modEq, modInst ) ){
return true;
}
return false;
}
eq::EqualityEngine* QuantifiersEngine::getMasterEqualityEngine(){
- return ((quantifiers::TheoryQuantifiers*)getTheoryEngine()->theoryOf( THEORY_QUANTIFIERS ))->getMasterEqualityEngine();
+ return getTheoryEngine()->getMasterEqualityEngine();
+}
+
+void QuantifiersEngine::debugPrintEqualityEngine( const char * c ) {
+ eq::EqualityEngine* ee = getMasterEqualityEngine();
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
+ while( !eqcs_i.isFinished() ){
+ TNode r = (*eqcs_i);
+ bool firstTime = true;
+ Trace(c) << " " << r;
+ Trace(c) << " : { ";
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
+ while( !eqc_i.isFinished() ){
+ TNode n = (*eqc_i);
+ if( r!=n ){
+ if( firstTime ){
+ Trace(c) << std::endl;
+ firstTime = false;
+ }
+ Trace(c) << " " << n << std::endl;
+ }
+ ++eqc_i;
+ }
+ if( !firstTime ){ Trace(c) << " "; }
+ Trace(c) << "}" << std::endl;
+ ++eqcs_i;
+ }
+ Trace(c) << std::endl;
}
void EqualityQueryQuantifiersEngine::reset(){
class QuantConflictFind;
class RewriteEngine;
class RelevantDomain;
+ class QModelBuilder;
class ConjectureGenerator;
class CegInstantiation;
}/* CVC4::theory::quantifiers */
QuantRelevance * d_quant_rel;
/** relevant domain */
quantifiers::RelevantDomain* d_rel_dom;
+ /** model builder */
+ quantifiers::QModelBuilder* d_builder;
/** phase requirements for each quantifier for each instantiation literal */
std::map< Node, QuantPhaseReq* > d_phase_reqs;
/** instantiation engine */
quantifiers::RelevantDomain* getRelevantDomain() { return d_rel_dom; }
/** get quantifier relevance */
QuantRelevance* getQuantifierRelevance() { return d_quant_rel; }
+ /** get the model builder */
+ quantifiers::QModelBuilder* getModelBuilder() { return d_builder; }
/** 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 addTermToDatabase( Node n, bool withinQuant = false );
/** get the master equality engine */
eq::EqualityEngine* getMasterEqualityEngine() ;
+ /** debug print equality engine */
+ void debugPrintEqualityEngine( const char * c );
public:
/** print instantiations */
void printInstantiations( std::ostream& out );
projects / cvc5.git / commitdiff