if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){\r
std::map< Node, Node > msum;\r
if (QuantArith::getMonomialSumLit( lit, msum )){\r
- Trace("bound-integers") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;\r
+ Trace("bound-integers-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl;\r
for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){\r
- Trace("bound-integers") << " ";\r
+ Trace("bound-integers-debug") << " ";\r
if( !it->second.isNull() ){\r
- Trace("bound-integers") << it->second;\r
+ Trace("bound-integers-debug") << it->second;\r
if( !it->first.isNull() ){\r
- Trace("bound-integers") << " * ";\r
+ Trace("bound-integers-debug") << " * ";\r
}\r
}\r
if( !it->first.isNull() ){\r
- Trace("bound-integers") << it->first;\r
+ Trace("bound-integers-debug") << it->first;\r
}\r
- Trace("bound-integers") << std::endl;\r
+ Trace("bound-integers-debug") << std::endl;\r
}\r
- Trace("bound-integers") << std::endl;\r
+ Trace("bound-integers-debug") << std::endl;\r
for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){\r
if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){\r
Node veq;\r
}\r
veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 );\r
}\r
- Trace("bound-integers") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;\r
+ Trace("bound-integers-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl;\r
Node bv = n1.getKind()==BOUND_VARIABLE ? n1 : n2;\r
if( !isBound( f, bv ) ){\r
if( !hasNonBoundVar( f, n1.getKind()==BOUND_VARIABLE ? n2 : n1 ) ) {\r
- Trace("bound-integers") << "The bound is relevant." << std::endl;\r
+ Trace("bound-integers-debug") << "The bound is relevant." << std::endl;\r
d_bounds[n1.getKind()==BOUND_VARIABLE ? 0 : 1][f][bv] = (n1.getKind()==BOUND_VARIABLE ? n2 : n1);\r
}\r
}\r
}\r
\r
\r
-FullModelChecker::FullModelChecker(QuantifiersEngine* qe) : d_qe(qe){\r
+FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :\r
+QModelBuilder( c, qe ){\r
d_true = NodeManager::currentNM()->mkConst(true);\r
d_false = NodeManager::currentNM()->mkConst(false);\r
}\r
\r
-void FullModelChecker::reset(FirstOrderModel * fm) {\r
- Trace("fmc") << "---Full Model Check reset() " << std::endl;\r
- for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){\r
- it->second->reset();\r
- }\r
- d_quant_models.clear();\r
- d_models_init.clear();\r
- d_rep_ids.clear();\r
- d_model_basis_rep.clear();\r
- d_star_insts.clear();\r
- //process representatives\r
- for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();\r
- it != fm->d_rep_set.d_type_reps.end(); ++it ){\r
- if( it->first.isSort() ){\r
- if( d_type_star.find(it->first)==d_type_star.end() ){\r
- Node st = NodeManager::currentNM()->mkSkolem( "star_$$", it->first, "skolem created for full-model checking" );\r
- d_type_star[it->first] = st;\r
- }\r
- Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;\r
- Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);\r
- Node rmbt = fm->getRepresentative(mbt);\r
- int mbt_index = -1;\r
- Trace("fmc") << " Model basis term : " << mbt << std::endl;\r
- for( size_t a=0; a<it->second.size(); a++ ){\r
- //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] );\r
- //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 );\r
- Node r = fm->getRepresentative( it->second[a] );\r
- std::vector< Node > eqc;\r
- ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );\r
- Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt);\r
- Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";\r
- //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";\r
- Trace("fmc-model-debug") << " {";\r
- //find best selection for representative\r
- for( size_t i=0; i<eqc.size(); i++ ){\r
- Trace("fmc-model-debug") << eqc[i] << ", ";\r
- }\r
- Trace("fmc-model-debug") << "}" << std::endl;\r
\r
- //if this is the model basis eqc, replace with actual model basis term\r
- if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {\r
- d_model_basis_rep[it->first] = r;\r
- r = mbt;\r
- mbt_index = a;\r
+void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){\r
+ d_addedLemmas = 0;\r
+ FirstOrderModel* fm = (FirstOrderModel*)m;\r
+ if( fullModel ){\r
+ //make function values\r
+ for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){\r
+ m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );\r
+ }\r
+ TheoryEngineModelBuilder::processBuildModel( m, fullModel );\r
+ //mark that the model has been set\r
+ fm->markModelSet();\r
+ }else{\r
+ Trace("fmc") << "---Full Model Check reset() " << std::endl;\r
+ for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){\r
+ it->second->reset();\r
+ }\r
+ d_quant_models.clear();\r
+ d_models_init.clear();\r
+ d_rep_ids.clear();\r
+ d_model_basis_rep.clear();\r
+ d_star_insts.clear();\r
+ //process representatives\r
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();\r
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){\r
+ if( it->first.isSort() ){\r
+ Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;\r
+ Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);\r
+ Node rmbt = fm->getRepresentative(mbt);\r
+ int mbt_index = -1;\r
+ Trace("fmc") << " Model basis term : " << mbt << std::endl;\r
+ for( size_t a=0; a<it->second.size(); a++ ){\r
+ //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] );\r
+ //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 );\r
+ Node r = fm->getRepresentative( it->second[a] );\r
+ std::vector< Node > eqc;\r
+ ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );\r
+ Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt);\r
+ Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";\r
+ //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";\r
+ Trace("fmc-model-debug") << " {";\r
+ //find best selection for representative\r
+ for( size_t i=0; i<eqc.size(); i++ ){\r
+ Trace("fmc-model-debug") << eqc[i] << ", ";\r
+ }\r
+ Trace("fmc-model-debug") << "}" << std::endl;\r
+\r
+ //if this is the model basis eqc, replace with actual model basis term\r
+ if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {\r
+ d_model_basis_rep[it->first] = r;\r
+ r = mbt;\r
+ mbt_index = a;\r
+ }\r
+ d_rep_ids[it->first][r] = (int)a;\r
}\r
- d_rep_ids[it->first][r] = (int)a;\r
- }\r
- Trace("fmc-model-debug") << std::endl;\r
+ Trace("fmc-model-debug") << std::endl;\r
\r
- if (mbt_index==-1) {\r
- std::cout << " WARNING: model basis term is not a representative!" << std::endl;\r
- exit(0);\r
- }else{\r
- Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;\r
+ if (mbt_index==-1) {\r
+ std::cout << " WARNING: model basis term is not a representative!" << std::endl;\r
+ exit(0);\r
+ }else{\r
+ Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;\r
+ }\r
}\r
}\r
}\r
Node ri = getRepresentative(fm, c[i]);\r
children.push_back(ri);\r
if (isModelBasisTerm(ri)) {\r
- ri = d_type_star[ri.getType()];\r
+ ri = getStar( ri.getType() );\r
}else{\r
hasNonStar = true;\r
}\r
if( d_models_init.find(op)==d_models_init.end() ){\r
if( d_models.find(op)==d_models.end() ){\r
d_models[op] = new Def;\r
- //make sure star's are defined\r
- TypeNode tn = op.getType();\r
- for(unsigned i=0; i<tn.getNumChildren()-1; i++) {\r
- if( d_type_star.find(tn[i])==d_type_star.end() ){\r
- Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn[i], "skolem created for full-model checking" );\r
- d_type_star[tn[i]] = st;\r
- }\r
- }\r
}\r
//reset the model\r
d_models[op]->reset();\r
std::vector< Node > conds;\r
std::vector< Node > values;\r
std::vector< Node > entry_conds;\r
- Trace("fmc-model-debug") << "Model values for " << op << " ... " << std::endl;\r
+ Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;\r
for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){\r
Node r = getRepresentative(fm, fm->d_uf_terms[op][i]);\r
Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;\r
}\r
Trace("fmc-model-debug") << std::endl;\r
//initialize the model\r
+ /*\r
for( int j=0; j<2; j++ ){\r
for( int k=1; k>=0; k-- ){\r
Trace("fmc-model-debug")<< "Set values " << j << " " << k << " : " << std::endl;\r
}\r
}\r
}\r
- //add for default value\r
- if (!fm->d_uf_model_gen[op].d_default_value.isNull()) {\r
- Node n = d_qe->getTermDatabase()->getModelBasisOpTerm(op);\r
- addEntry(fm, op, n, fm->d_uf_model_gen[op].d_default_value, conds, values, entry_conds);\r
+ */\r
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){\r
+ Node n = fm->d_uf_terms[op][i];\r
+ if( !n.getAttribute(NoMatchAttribute()) ){\r
+ addEntry(fm, op, n, n, conds, values, entry_conds);\r
+ }\r
}\r
-\r
- //find other default values (TODO: figure out why these entries are added to d_uf_model_gen)\r
- if( conds.empty() ){\r
- //for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[1][0].begin();\r
- // it != fm->d_uf_model_gen[op].d_set_values[1][0].end(); ++it ){\r
- // Trace("fmc-model-debug") << " process : " << it->first << " -> " << it->second << std::endl;\r
- // addEntry(fm, op, it->first, it->second, conds, values, entry_conds);\r
- //}\r
- Trace("fmc-warn") << "WARNING: No entries for " << op << ", make default entry." << std::endl;\r
- //choose a complete arbitrary term\r
- Node n = d_qe->getTermDatabase()->getModelBasisOpTerm(op);\r
- TypeNode tn = n.getType();\r
- Node v = fm->d_rep_set.d_type_reps[tn][0];\r
- addEntry(fm, op, n, v, conds, values, entry_conds);\r
+ Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);\r
+ //add default value\r
+ if( fm->hasTerm( nmb ) ){\r
+ Trace("fmc-model-debug") << "Add default " << nmb << std::endl;\r
+ addEntry(fm, op, nmb, nmb, conds, values, entry_conds);\r
+ }else{\r
+ Node vmb = getSomeDomainElement( fm, nmb.getType() );\r
+ Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";\r
+ Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;\r
+ addEntry(fm, op, nmb, vmb, conds, values, entry_conds);\r
}\r
\r
//sort based on # default arguments\r
\r
\r
bool FullModelChecker::isStar(Node n) {\r
- return n==d_type_star[n.getType()];\r
+ return n==getStar(n.getType());\r
}\r
\r
bool FullModelChecker::isModelBasisTerm(Node n) {\r
}\r
\r
\r
-int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, int effort) {\r
- int addedLemmas = 0;\r
+bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) {\r
Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;\r
if (effort==0) {\r
//register the quantifier\r
for( unsigned j=0; j<inst.size(); j++) {\r
m.set( d_qe, f, j, inst[j] );\r
}\r
- if (isActive()) {\r
- if( d_qe->addInstantiation( f, m ) ){\r
- addedLemmas++;\r
- }else{\r
- //this can happen if evaluation is unknown\r
- //might try it next effort level\r
- d_star_insts[f].push_back(i);\r
- }\r
+ if( d_qe->addInstantiation( f, m ) ){\r
+ lemmas++;\r
+ }else{\r
+ //this can happen if evaluation is unknown\r
+ //might try it next effort level\r
+ d_star_insts[f].push_back(i);\r
}\r
}else{\r
//might try it next effort level\r
}\r
}\r
}else{\r
- Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;\r
- Trace("fmc-exh") << "Definition was : " << std::endl;\r
- d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);\r
- Trace("fmc-exh") << std::endl;\r
- Def temp;\r
- //simplify the exceptions?\r
- for( int i=(d_star_insts[f].size()-1); i>=0; i--) {\r
- //get witness for d_star_insts[f][i]\r
- int j = d_star_insts[f][i];\r
- if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){\r
- int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );\r
- if( lem==-1 ){\r
- return -1;\r
- }else{\r
- addedLemmas += lem;\r
+ if (!d_star_insts[f].empty()) {\r
+ Trace("fmc-exh") << "Exhaustive instantiate " << f << std::endl;\r
+ Trace("fmc-exh") << "Definition was : " << std::endl;\r
+ d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);\r
+ Trace("fmc-exh") << std::endl;\r
+ Def temp;\r
+ //simplify the exceptions?\r
+ for( int i=(d_star_insts[f].size()-1); i>=0; i--) {\r
+ //get witness for d_star_insts[f][i]\r
+ int j = d_star_insts[f][i];\r
+ if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){\r
+ int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );\r
+ if( lem==-1 ){\r
+ //something went wrong, resort to exhaustive instantiation\r
+ return false;\r
+ }else{\r
+ lemmas += lem;\r
+ }\r
}\r
}\r
}\r
}\r
- return addedLemmas;\r
+ return true;\r
}\r
\r
int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {\r
Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;\r
if( n.getKind() == kind::BOUND_VARIABLE ){\r
d.addEntry(this, mkCondDefault(f), n);\r
+ Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl;\r
}\r
else if( n.getNumChildren()==0 ){\r
Node r = n;\r
if( !fm->hasTerm(n) ){\r
- if (fm->d_rep_set.hasType(n.getType())) {\r
- r = fm->d_rep_set.d_type_reps[n.getType()][0];\r
- }else{\r
- //should never happen?\r
- }\r
+ r = getSomeDomainElement( fm, n.getType() );\r
}\r
r = getRepresentative(fm, r);\r
d.addEntry(this, mkCondDefault(f), r);\r
int j = getVariableId(f, eq[0]);\r
int k = getVariableId(f, eq[1]);\r
TypeNode tn = eq[0].getType();\r
+ if( !fm->d_rep_set.hasType( tn ) ){\r
+ getSomeDomainElement( fm, tn ); //to verify the type is initialized\r
+ }\r
for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {\r
Node r = getRepresentative( fm, fm->d_rep_set.d_type_reps[tn][i] );\r
cond[j+1] = r;\r
mkCondVec(dc.d_cond[i],cond);\r
cond[j+1] = val;\r
d.addEntry(this, mkCond(cond), d_true);\r
- cond[j+1] = d_type_star[val.getType()];\r
+ cond[j+1] = getStar(val.getType());\r
d.addEntry(this, mkCond(cond), d_false);\r
}else{\r
d.addEntry( this, dc.d_cond[i], d_false);\r
}\r
\r
void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {\r
+ getModel(fm, op);\r
Trace("fmc-uf-debug") << "Definition : " << std::endl;\r
d_models[op]->debugPrint("fmc-uf-debug", op, this);\r
Trace("fmc-uf-debug") << std::endl;\r
Trace("fmc-uf-process") << "follow value..." << std::endl;\r
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);\r
}\r
- Node st = d_type_star[v.getType()];\r
+ Node st = getStar(v.getType());\r
if (curr.d_child.find(st)!=curr.d_child.end()) {\r
Trace("fmc-uf-process") << "follow star..." << std::endl;\r
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);\r
return mkCond(cond);\r
}\r
\r
+Node FullModelChecker::getStar(TypeNode tn) {\r
+ if( d_type_star.find(tn)==d_type_star.end() ){\r
+ Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );\r
+ d_type_star[tn] = st;\r
+ }\r
+ return d_type_star[tn];\r
+}\r
+\r
+Node FullModelChecker::getSomeDomainElement(FirstOrderModel * fm, TypeNode tn){\r
+ //check if there is even any domain elements at all\r
+ if (!fm->d_rep_set.hasType(tn)) {\r
+ Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;\r
+ Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
+ fm->d_rep_set.d_type_reps[tn].push_back(mbt);\r
+ }else if( fm->d_rep_set.d_type_reps[tn].size()==0 ){\r
+ Message() << "empty reps" << std::endl;\r
+ exit(0);\r
+ }\r
+ return fm->d_rep_set.d_type_reps[tn][0];\r
+}\r
+\r
void FullModelChecker::mkCondDefaultVec( Node f, std::vector< Node > & cond ) {\r
//get function symbol for f\r
cond.push_back(d_quant_cond[f]);\r
for (unsigned i=0; i<f[0].getNumChildren(); i++) {\r
- cond.push_back(d_type_star[f[0][i].getType()]);\r
+ Node ts = getStar( f[0][i].getType() );\r
+ cond.push_back(ts);\r
}\r
}\r
\r
}\r
}\r
\r
-bool FullModelChecker::isActive() {\r
- return options::fmfFullModelCheck();\r
-}\r
-\r
bool FullModelChecker::useSimpleModels() {\r
return options::fmfFullModelCheckSimple();\r
}\r
\r
Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix ) {\r
+ getModel( fm, op );\r
TypeNode type = op.getType();\r
std::vector< Node > vars;\r
for( size_t i=0; i<type.getNumChildren()-1; i++ ){\r
};\r
\r
\r
-class FullModelChecker\r
+class FullModelChecker : public QModelBuilder\r
{\r
-private:\r
+protected:\r
Node d_true;\r
Node d_false;\r
- QuantifiersEngine* d_qe;\r
std::map<TypeNode, std::map< Node, int > > d_rep_ids;\r
std::map<TypeNode, Node > d_model_basis_rep;\r
std::map<Node, Def * > d_models;\r
void mkCondVec( Node n, std::vector< Node > & cond );\r
Node evaluateInterpreted( Node n, std::vector< Node > & vals );\r
public:\r
- FullModelChecker( QuantifiersEngine* qe );\r
+ FullModelChecker( context::Context* c, QuantifiersEngine* qe );\r
~FullModelChecker(){}\r
\r
int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }\r
bool isStar(Node n);\r
- Node getStar(TypeNode tn) { return d_type_star[tn]; }\r
+ Node getStar(TypeNode tn);\r
+ Node getSomeDomainElement(FirstOrderModel * fm, TypeNode tn);\r
bool isModelBasisTerm(Node n);\r
Node getModelBasisTerm(TypeNode tn);\r
- void reset(FirstOrderModel * fm);\r
Def * getModel(FirstOrderModel * fm, Node op);\r
\r
void debugPrintCond(const char * tr, Node n, bool dispStar = false);\r
void debugPrint(const char * tr, Node n, bool dispStar = false);\r
\r
- int exhaustiveInstantiate(FirstOrderModel * fm, Node f, int effort);\r
- bool hasStarExceptions( Node f ) { return !d_star_insts[f].empty(); }\r
+ bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas );\r
\r
- bool isActive();\r
bool useSimpleModels();\r
Node getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix );\r
+\r
+ /** process build model */\r
+ void processBuildModel(TheoryModel* m, bool fullModel);\r
};\r
\r
}\r
if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){
d_match_values.push_back( val );
d_matches.push_back( InstMatch( &m ) );
- qe->getModelEngine()->getModelBuilder()->d_instGenMatches++;
+ ((QModelBuilderIG*)qe->getModelEngine()->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 = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );
+ bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->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 = qe->getModelEngine()->getModelBuilder()->isTermSelected( n );
+ bool isSelected = ((QModelBuilderIG*)qe->getModelEngine()->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()) ){
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
+
+QModelBuilder::QModelBuilder( context::Context* c, QuantifiersEngine* qe ) :
+TheoryEngineModelBuilder( qe->getTheoryEngine() ), d_curr_model( c, NULL ), d_qe( qe ){
+ d_considerAxioms = true;
+ d_addedLemmas = 0;
+}
+
+
+bool QModelBuilder::optUseModel() {
+ return options::fmfModelBasedInst();
+}
+
+
bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){
if( argIndex<(int)n.getNumChildren() ){
Node r;
}
}
-ModelEngineBuilder::ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe ) :
-TheoryEngineModelBuilder( qe->getTheoryEngine() ),
-d_qe( qe ), d_curr_model( c, NULL ){
- d_considerAxioms = true;
+QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) :
+QModelBuilder( c, qe ) {
+
}
-void ModelEngineBuilder::debugModel( FirstOrderModel* fm ){
+
+void QModelBuilderIG::debugModel( FirstOrderModel* fm ){
//debug the model: cycle through all instantiations for all quantifiers, report ones that are not true
if( Trace.isOn("quant-model-warn") ){
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
}
}
-void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) {
+void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) {
FirstOrderModel* fm = (FirstOrderModel*)m;
if( fullModel ){
Assert( d_curr_model==fm );
- if( d_qe->getModelEngine()->getFullModelChecker()->isActive() ){
- for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
- fm->d_uf_models[ it->first ] = d_qe->getModelEngine()->getFullModelChecker()->getFunctionValue( fm, it->first, "$x" );
- }
- }else{
- //update models
- for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
- it->second.update( fm );
- Trace("model-func") << "ModelEngineBuilder: Make function value from tree " << it->first << std::endl;
- //construct function values
- fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
- }
+ //update models
+ for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+ it->second.update( fm );
+ Trace("model-func") << "QModelBuilder: Make function value from tree " << it->first << std::endl;
+ //construct function values
+ fm->d_uf_models[ it->first ] = it->second.getFunctionValue( "$x" );
}
TheoryEngineModelBuilder::processBuildModel( m, fullModel );
//mark that the model has been set
}
}
//construct the model if necessary
- if( d_addedLemmas==0 || optExhInstNonInstGenQuant() ){
+ if( d_addedLemmas==0 ){
//if no immediate exceptions, build the model
// this model will be an approximation that will need to be tested via exhaustive instantiation
Trace("model-engine-debug") << "Building model..." << std::endl;
}
}
-int ModelEngineBuilder::initializeQuantifier( Node f, Node fp ){
+int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){
if( d_quant_basis_match_added.find( f )==d_quant_basis_match_added.end() ){
//create the basis match if necessary
if( d_quant_basis_match.find( f )==d_quant_basis_match.end() ){
return 0;
}
-void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
+void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){
d_uf_model_constructed.clear();
//determine if any functions are constant
for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
}
}
-bool ModelEngineBuilder::hasConstantDefinition( Node n ){
+bool QModelBuilderIG::hasConstantDefinition( Node n ){
Node lit = n.getKind()==NOT ? n[0] : n;
if( lit.getKind()==APPLY_UF ){
Node op = lit.getOperator();
return false;
}
-bool ModelEngineBuilder::optUseModel() {
- return options::fmfModelBasedInst();
-}
-
-bool ModelEngineBuilder::optInstGen(){
+bool QModelBuilderIG::optInstGen(){
return options::fmfInstGen();
}
-bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
+bool QModelBuilderIG::optOneQuantPerRoundInstGen(){
return options::fmfInstGenOneQuantPerRound();
}
-bool ModelEngineBuilder::optExhInstNonInstGenQuant(){
- return options::fmfNewInstGen();
-}
-
-void ModelEngineBuilder::setEffort( int effort ){
- d_considerAxioms = effort>=1;
-}
-
-ModelEngineBuilder::Statistics::Statistics():
- d_num_quants_init("ModelEngineBuilder::Number_Quantifiers", 0),
- d_num_partial_quants_init("ModelEngineBuilder::Number_Partial_Quantifiers", 0),
- d_init_inst_gen_lemmas("ModelEngineBuilder::Initialize_Inst_Gen_Lemmas", 0 ),
- d_inst_gen_lemmas("ModelEngineBuilder::Inst_Gen_Lemmas", 0 )
+QModelBuilderIG::Statistics::Statistics():
+ d_num_quants_init("QModelBuilder::Number_Quantifiers", 0),
+ d_num_partial_quants_init("QModelBuilder::Number_Partial_Quantifiers", 0),
+ d_init_inst_gen_lemmas("QModelBuilder::Initialize_Inst_Gen_Lemmas", 0 ),
+ d_inst_gen_lemmas("QModelBuilder::Inst_Gen_Lemmas", 0 )
{
StatisticsRegistry::registerStat(&d_num_quants_init);
StatisticsRegistry::registerStat(&d_num_partial_quants_init);
StatisticsRegistry::registerStat(&d_inst_gen_lemmas);
}
-ModelEngineBuilder::Statistics::~Statistics(){
+QModelBuilderIG::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_num_quants_init);
StatisticsRegistry::unregisterStat(&d_num_partial_quants_init);
StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas);
StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas);
}
-bool ModelEngineBuilder::isQuantifierActive( Node f ){
+bool QModelBuilderIG::isQuantifierActive( Node f ){
return ( d_considerAxioms || !f.getAttribute(AxiomAttribute()) ) && d_quant_sat.find( f )==d_quant_sat.end();
}
-bool ModelEngineBuilder::isTermActive( Node n ){
+bool QModelBuilderIG::isTermActive( Node n ){
return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term
( n.getAttribute(ModelBasisArgAttribute())!=0 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments
//and is not congruent modulo model basis
-void ModelEngineBuilderDefault::reset( FirstOrderModel* fm ){
+void QModelBuilderDefault::reset( FirstOrderModel* fm ){
d_quant_selection_lit.clear();
d_quant_selection_lit_candidates.clear();
d_quant_selection_lit_terms.clear();
}
-int ModelEngineBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) {
+int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) {
/*
size_t maxChildren = 0;
for( size_t i=0; i<uf_terms.size(); i++ ){
return 0;
}
-void ModelEngineBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
+void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){
Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
//the pro/con preferences for this quantifier
std::vector< Node > pro_con[2];
}
}
-int ModelEngineBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
+int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){
int addedLemmas = 0;
//we wish to add all known exceptions to our selection literal for f. this will help to refine our current model.
//This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
return addedLemmas;
}
-void ModelEngineBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
+void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){
if( optReconsiderFuncConstants() ){
//reconsider constant functions that weren't necessary
if( d_uf_model_constructed[op] ){
////////////////////// Inst-Gen style Model Builder ///////////
-void ModelEngineBuilderInstGen::reset( FirstOrderModel* fm ){
+void QModelBuilderInstGen::reset( FirstOrderModel* fm ){
//for new inst gen
d_quant_selection_formula.clear();
d_term_selected.clear();
//d_sub_quant_inst_trie.clear();//*
}
-int ModelEngineBuilderInstGen::initializeQuantifier( Node f, Node fp ){
- int addedLemmas = ModelEngineBuilder::initializeQuantifier( f, fp );
+int QModelBuilderInstGen::initializeQuantifier( Node f, Node fp ){
+ int addedLemmas = QModelBuilderIG::initializeQuantifier( f, fp );
for( size_t i=0; i<d_sub_quants[f].size(); i++ ){
addedLemmas += initializeQuantifier( d_sub_quants[f][i], fp );
}
return addedLemmas;
}
-void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){
+void QModelBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f ){
//Node fp = getParentQuantifier( f );//*
//bool quantRedundant = ( f!=fp && d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) );
//if( f==fp || d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, d_sub_quant_inst[ f ], true ) ){//*
}
-int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
+int QModelBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
int addedLemmas = 0;
if( d_quant_sat.find( f )==d_quant_sat.end() ){
Node fp = d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f];
//if possible, returns a formula n' such that n' => ( n <=> polarity ), and n' is true in the current context,
// and NULL otherwise
-Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){
+Node QModelBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){
Trace("sel-form-debug") << "Looking for selection formula " << n << " " << polarity << std::endl;
Node ret;
if( n.getKind()==NOT ){
return ret;
}
-int ModelEngineBuilderInstGen::getSelectionFormulaScore( Node fn ){
+int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){
if( fn.getType().isBoolean() ){
if( fn.getKind()==APPLY_UF ){
Node op = fn.getOperator();
}
}
-void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){
+void QModelBuilderInstGen::setSelectedTerms( Node s ){
//if it is apply uf and has model basis arguments, then mark term as being "selected"
if( s.getKind()==APPLY_UF ){
}
}
-bool ModelEngineBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){
+bool QModelBuilderInstGen::isUsableSelectionLiteral( Node n, int useOption ){
if( n.getKind()==FORALL ){
return false;
}else if( n.getKind()!=APPLY_UF ){
return true;
}
-void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){
+void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){
if( f!=fp ){
//std::cout << "gpqm " << fp << " " << f << " " << m << std::endl;
//std::cout << " " << fp[0].getNumChildren() << " " << f[0].getNumChildren() << std::endl;
}
}
-void ModelEngineBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){
+void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){
bool setDefaultVal = true;
Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
//set the values in the model
d_uf_model_constructed[op] = true;
}
-bool ModelEngineBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
+bool QModelBuilderInstGen::existsInstantiation( Node f, InstMatch& m, bool modEq, bool modInst ){
return d_child_sub_quant_inst_trie[f].existsInstMatch( d_qe, f, m, modEq, true );
}
\ No newline at end of file
namespace theory {
namespace quantifiers {
+
+class QModelBuilder : public TheoryEngineModelBuilder
+{
+protected:
+ //the model we are working with
+ context::CDO< FirstOrderModel* > d_curr_model;
+ //quantifiers engine
+ QuantifiersEngine* d_qe;
+public:
+ QModelBuilder( context::Context* c, QuantifiersEngine* qe );
+ virtual ~QModelBuilder(){}
+ // is quantifier active?
+ virtual bool isQuantifierActive( Node f ) { return true; }
+ //do exhaustive instantiation
+ virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) { return false; }
+ //whether to construct model
+ virtual bool optUseModel();
+ /** number of lemmas generated while building model */
+ int d_addedLemmas;
+ //consider axioms
+ bool d_considerAxioms;
+ /** exist instantiation ? */
+ virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
+};
+
+
+
+
+
/** Attribute true for nodes that should not be used when considered for inst-gen basis */
struct BasisNoMatchAttributeId {};
/** use the special for boolean flag */
/** model builder class
* This class is capable of building candidate models based on the current quantified formulas
* that are asserted. Use:
- * (1) call ModelEngineBuilder::buildModel( m, false );, where m is a FirstOrderModel
+ * (1) call QModelBuilder::buildModel( m, false );, where m is a FirstOrderModel
* (2) if candidate model is determined to be a real model,
- then call ModelEngineBuilder::buildModel( m, true );
+ then call QModelBuilder::buildModel( m, true );
*/
-class ModelEngineBuilder : public TheoryEngineModelBuilder
+class QModelBuilderIG : public QModelBuilder
{
protected:
- //quantifiers engine
- QuantifiersEngine* d_qe;
- //the model we are working with
- context::CDO< FirstOrderModel* > d_curr_model;
//map from operators to model preference data
std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
//built model uf
/** term has constant definition */
bool hasConstantDefinition( Node n );
public:
- ModelEngineBuilder( context::Context* c, QuantifiersEngine* qe );
- virtual ~ModelEngineBuilder(){}
- /** number of lemmas generated while building model */
- int d_addedLemmas;
- //consider axioms
- bool d_considerAxioms;
- // set effort
- void setEffort( int effort );
+ QModelBuilderIG( context::Context* c, QuantifiersEngine* qe );
+ virtual ~QModelBuilderIG(){}
//debug model
void debugModel( FirstOrderModel* fm );
public:
- //whether to construct model
- virtual bool optUseModel();
//whether to add inst-gen lemmas
virtual bool optInstGen();
//whether to only consider only quantifier per round of inst-gen
virtual bool optOneQuantPerRoundInstGen();
- //whether we should exhaustively instantiate quantifiers where inst-gen is not working
- virtual bool optExhInstNonInstGenQuant();
/** statistics class */
class Statistics {
public:
~Statistics();
};
Statistics d_statistics;
- // is quantifier active?
- bool isQuantifierActive( Node f );
// is term active
bool isTermActive( Node n );
// is term selected
virtual bool isTermSelected( Node n ) { return false; }
- /** exist instantiation ? */
- virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
/** quantifier has inst-gen definition */
virtual bool hasInstGen( Node f ) = 0;
/** did inst gen this round? */
bool didInstGen() { return d_didInstGen; }
+ // is quantifier active?
+ bool isQuantifierActive( Node f );
//temporary stats
int d_numQuantSat;
int d_numQuantNoSelForm;
//temporary stat
int d_instGenMatches;
-};/* class ModelEngineBuilder */
+};/* class QModelBuilder */
-class ModelEngineBuilderDefault : public ModelEngineBuilder
+class QModelBuilderDefault : public QModelBuilderIG
{
private: ///information for (old) InstGen
//map from quantifiers to their selection literals
//theory-specific build models
void constructModelUf( FirstOrderModel* fm, Node op );
public:
- ModelEngineBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){}
- ~ModelEngineBuilderDefault(){}
+ QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
+ ~QModelBuilderDefault(){}
//options
bool optReconsiderFuncConstants() { return true; }
//has inst gen
bool hasInstGen( Node f ) { return !d_quant_selection_lit[f].isNull(); }
};
-class ModelEngineBuilderInstGen : public ModelEngineBuilder
+class QModelBuilderInstGen : public QModelBuilderIG
{
private: ///information for (new) InstGen
//map from quantifiers to their selection formulas
//get parent quantifier
Node getParentQuantifier( Node f ) { return d_sub_quant_parent.find( f )==d_sub_quant_parent.end() ? f : d_sub_quant_parent[f]; }
public:
- ModelEngineBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : ModelEngineBuilder( c, qe ){}
- ~ModelEngineBuilderInstGen(){}
+ QModelBuilderInstGen( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
+ ~QModelBuilderInstGen(){}
// is term selected
bool isTermSelected( Node n ) { return d_term_selected.find( n )!=d_term_selected.end(); }
/** exist instantiation ? */
//Model Engine constructor
ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
QuantifiersModule( qe ),
-d_rel_domain( qe, qe->getModel() ),
-d_fmc( qe ){
+d_rel_domain( qe, qe->getModel() ){
- if( options::fmfNewInstGen() ){
- d_builder = new ModelEngineBuilderInstGen( c, qe );
+ if( options::fmfFullModelCheck() ){
+ d_builder = new fmcheck::FullModelChecker( c, qe );
+ }else if( options::fmfNewInstGen() ){
+ d_builder = new QModelBuilderInstGen( c, qe );
}else{
- d_builder = new ModelEngineBuilderDefault( c, qe );
+ d_builder = new QModelBuilderDefault( c, qe );
}
}
Trace("model-engine") << "---Model Engine Round---" << std::endl;
//initialize the model
Trace("model-engine-debug") << "Build model..." << std::endl;
- d_builder->setEffort( effort );
+ d_builder->d_considerAxioms = effort>=1;
d_builder->buildModel( fm, false );
addedLemmas += (int)d_builder->d_addedLemmas;
//if builder has lemmas, add and return
//let the strong solver verify that the model is minimal
//for debugging, this will if there are terms in the model that the strong solver was not notified of
((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm );
- //for full model checking
- if( d_fmc.isActive() ){
- Trace("model-engine-debug") << "Reset full model checker..." << std::endl;
- d_fmc.reset( fm );
- }
Trace("model-engine-debug") << "Check model..." << std::endl;
d_incomplete_check = false;
//print debug
Debug("fmf-model-complete") << std::endl;
debugPrint("fmf-model-complete");
//successfully built an acceptable model, now check it
- addedLemmas += checkModel( check_model_full );
- }else if( d_builder->didInstGen() && d_builder->optExhInstNonInstGenQuant() ){
- Trace("model-engine-debug") << "Check model for non-inst gen quantifiers..." << std::endl;
- //check quantifiers that inst-gen didn't apply to
- addedLemmas += checkModel( check_model_no_inst_gen );
+ addedLemmas += checkModel();
}
}
if( addedLemmas==0 ){
#endif
}
-int ModelEngine::checkModel( int checkOption ){
+int ModelEngine::checkModel(){
int addedLemmas = 0;
FirstOrderModel* fm = d_quantEngine->getModel();
//for debugging
}
}
//full model checking: construct models for all functions
+ /*
if( d_fmc.isActive() ){
for (std::map< Node, uf::UfModelTreeGenerator >::iterator it = fm->d_uf_model_gen.begin(); it != fm->d_uf_model_gen.end(); ++it) {
d_fmc.getModel(fm, it->first);
}
}
+ */
//compute the relevant domain if necessary
if( optUseRelevantDomain() ){
d_rel_domain.compute();
d_relevantLemmas = 0;
d_totalLemmas = 0;
Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
- int e_max = d_fmc.isActive() ? 2 : 1;
+ int e_max = options::fmfFullModelCheck() ? 2 : 1;
for( int e=0; e<e_max; e++) {
if (addedLemmas==0) {
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
}
}
d_totalLemmas += totalInst;
- //determine if we should check this quantifiers
- bool checkQuant = false;
- if( checkOption==check_model_full ){
- checkQuant = d_builder->isQuantifierActive( f );
- }else if( checkOption==check_model_no_inst_gen ){
- checkQuant = !d_builder->hasInstGen( f );
- }
- //if we need to consider this quantifier on this iteration
- if( checkQuant ){
+ //determine if we should check this quantifier
+ if( d_builder->isQuantifierActive( f ) ){
addedLemmas += exhaustiveInstantiate( f, e );
if( Trace.isOn("model-engine-warn") ){
if( addedLemmas>10000 ){
int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
int addedLemmas = 0;
-
- bool useModel = d_builder->optUseModel();
- if (d_fmc.isActive() && effort==0) {
- addedLemmas = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort);
- }else if( !d_fmc.isActive() || (effort==1 && d_fmc.hasStarExceptions(f)) ) {
- if(d_fmc.isActive()){
- useModel = false;
- int lem = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort);
- if( lem!=-1 ){
- return lem;
- }
- }
+ if( !d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort, addedLemmas ) ){
Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
Debug("inst-fmf-ei") << " Instantiation Constants: ";
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
d_testLemmas++;
int eval = 0;
int depIndex;
- if( useModel ){
+ if( d_builder->optUseModel() ){
//see if instantiation is already true in current model
Debug("fmf-model-eval") << "Evaluating ";
riter.debugPrintSmall("fmf-model-eval");
friend class RepSetIterator;
private:
/** builder class */
- ModelEngineBuilder* d_builder;
+ QModelBuilder* d_builder;
private: //analysis of current model:
//relevant domain
RelevantDomain d_rel_domain;
- //full model checker
- fmcheck::FullModelChecker d_fmc;
//is the exhaustive instantiation incomplete?
bool d_incomplete_check;
private:
bool optOneQuantPerRound();
bool optExhInstEvalSkipMultiple();
private:
- enum{
- check_model_full,
- check_model_no_inst_gen,
- };
//check model
- int checkModel( int checkOption );
+ int checkModel();
//exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
int exhaustiveInstantiate( Node f, int effort = 0 );
private:
ModelEngine( context::Context* c, QuantifiersEngine* qe );
~ModelEngine(){}
//get the builder
- ModelEngineBuilder* getModelBuilder() { return d_builder; }
- fmcheck::FullModelChecker* getFullModelChecker() { return &d_fmc; }
+ QModelBuilder* getModelBuilder() { return d_builder; }
public:
void check( Theory::Effort e );
void registerQuantifier( Node f );
projects / cvc5.git / commitdiff