void BoundedIntegers::registerQuantifier( Node f ) {\r
Trace("bound-int") << "Register quantifier " << f << std::endl;\r
bool hasIntType = false;\r
+ int finiteTypes = 0;\r
std::map< Node, int > numMap;\r
for( unsigned i=0; i<f[0].getNumChildren(); i++) {\r
numMap[f[0][i]] = i;\r
if( f[0][i].getType().isInteger() ){\r
hasIntType = true;\r
}\r
+ else if( f[0][i].getType().isSort() ){\r
+ finiteTypes++;\r
+ }\r
}\r
if( hasIntType ){\r
bool success;\r
do{\r
+ //std::map< int, std::map< Node, Node > > bound_lit_map;\r
+ //std::map< int, std::map< Node, bool > > bound_lit_pol_map;\r
success = false;\r
process( f, f[1], true );\r
for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){\r
d_range[f][v] = Rewriter::rewrite( r );\r
Trace("bound-int") << " " << d_bounds[0][f][v] << " <= " << v << " <= " << d_bounds[1][f][v] << " (range is " << d_range[f][v] << ")" << std::endl;\r
}\r
- if( d_set[f].size()==f[0].getNumChildren() ){\r
+ if( d_set[f].size()==(f[0].getNumChildren()-finiteTypes) ){\r
d_bound_quants.push_back( f );\r
for( unsigned i=0; i<d_set[f].size(); i++) {\r
Node v = d_set[f][i];\r
if( quantifiers::TermDb::hasBoundVarAttr(r) ){\r
//introduce a new bound\r
Node new_range = NodeManager::currentNM()->mkSkolem( "bir_$$", r.getType(), "bound for term" );\r
- /*\r
- std::vector< Node > bvs;\r
- quantifiers::TermDb::getBoundVars(r, bvs);\r
- Assert(bvs.size()>0);\r
- Node body = NodeManager::currentNM()->mkNode( LEQ, r, new_range );\r
- std::vector< Node > children;\r
- //get all the other bounds\r
- for( unsigned j=0; j<bvs.size(); j++) {\r
- Node l = NodeManager::currentNM()->mkNode( LEQ, NodeManager::currentNM()->mkConst(Rational(0)), bvs[j]);\r
- Node u = NodeManager::currentNM()->mkNode( LEQ, bvs[j], d_range[f][bvs[j]] );\r
- children.push_back(l);\r
- children.push_back(u);\r
- }\r
- Node antec = NodeManager::currentNM()->mkNode( AND, children );\r
- body = NodeManager::currentNM()->mkNode( IMPLIES, antec, body );\r
-\r
- Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, bvs );\r
-\r
- Node lem = NodeManager::currentNM()->mkNode( FORALL, bvl, body );\r
- Trace("bound-int") << "For " << v << ", the quantified formula " << lem << " will be used to minimize the bound." << std::endl;\r
- Trace("bound-int-lemma") << " *** bound int: bounding quantified lemma " << lem << std::endl;\r
- d_quantEngine->getOutputChannel().lemma( lem );\r
- */\r
d_nground_range[f][v] = d_range[f][v];\r
d_range[f][v] = new_range;\r
r = new_range;\r
}
void FirstOrderModelFmc::processInitialize() {
+ if( options::fmfFmcInterval() && intervalOp.isNull() ){
+ std::vector< TypeNode > types;
+ for(unsigned i=0; i<2; i++){
+ types.push_back(NodeManager::currentNM()->integerType());
+ }
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->integerType() );
+ intervalOp = NodeManager::currentNM()->mkSkolem( "interval_$$", typ, "op representing interval" );
+ }
for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
it->second->reset();
}
curr = Rewriter::rewrite( curr );
return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
}
+
+bool FirstOrderModelFmc::isInterval(Node n) {
+ return n.getKind()==APPLY_UF && n.getOperator()==intervalOp;
+}
+
+Node FirstOrderModelFmc::getInterval( Node lb, Node ub ){
+ return NodeManager::currentNM()->mkNode( APPLY_UF, intervalOp, lb, ub );
+}
\ No newline at end of file
std::map<Node, Def * > d_models;
std::map<TypeNode, Node > d_model_basis_rep;
std::map<TypeNode, Node > d_type_star;
+ Node intervalOp;
Node getUsedRepresentative(Node n, bool strict = false);
/** get current model value */
Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
bool isModelBasisTerm(Node n);
Node getModelBasisTerm(TypeNode tn);
Node getSomeDomainElement(TypeNode tn);
+ bool isInterval(Node n);
+ Node getInterval( Node lb, Node ub );
};
}
};\r
\r
\r
+struct ConstRationalSort\r
+{\r
+ std::vector< Node > d_terms;\r
+ bool operator() (int i, int j) {\r
+ return (d_terms[i].getConst<Rational>() < d_terms[j].getConst<Rational>() );\r
+ }\r
+};\r
+\r
+\r
bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {\r
if (index==(int)c.getNumChildren()) {\r
return d_data!=-1;\r
}else{\r
- Node st = m->getStar(c[index].getType());\r
+ TypeNode tn = c[index].getType();\r
+ Node st = m->getStar(tn);\r
if(d_child.find(st)!=d_child.end()) {\r
if( d_child[st].hasGeneralization(m, c, index+1) ){\r
return true;\r
return true;\r
}\r
}\r
+ //for star: check if all children are defined and have generalizations\r
+ if( options::fmfFmcCoverSimplify() && c[index]==st ){\r
+ //check if all children exist and are complete\r
+ int num_child_def = d_child.size() - (d_child.find(st)!=d_child.end() ? 1 : 0);\r
+ if( num_child_def==m->d_rep_set.getNumRepresentatives(tn) ){\r
+ bool complete = true;\r
+ for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
+ if( !m->isStar(it->first) ){\r
+ if( !it->second.hasGeneralization(m, c, index+1) ){\r
+ complete = false;\r
+ break;\r
+ }\r
+ }\r
+ }\r
+ if( complete ){\r
+ return true;\r
+ }\r
+ }\r
+ }\r
+\r
return false;\r
}\r
}\r
if (d_et.hasGeneralization(m, c)) {\r
return false;\r
}\r
- if( options::fmfFmcCoverSimplify() ){\r
- if( d_et.isCovered(m, c, 0) ){\r
- Trace("fmc-cover-simplify") << "Entry " << c << " is covered." << std::endl;\r
- return false;\r
- }\r
- }\r
+ //if( options::fmfFmcCoverSimplify() ){\r
+ // if( d_et.isCovered(m, c, 0) ){\r
+ // Trace("fmc-cover-simplify") << "Entry " << c << " is covered." << std::endl;\r
+ // return false;\r
+ // }\r
+ //}\r
int newIndex = (int)d_cond.size();\r
if (!d_has_simplified) {\r
std::vector<int> compat;\r
}\r
if( !last_all_stars ){\r
Trace("fmc-cover-simplify") << "Need to modify last entry to be all stars." << std::endl;\r
- Trace("fmc-cover-simplify") << "Beforehand: " << std::endl;\r
+ Trace("fmc-cover-simplify") << "Before: " << std::endl;\r
debugPrint("fmc-cover-simplify",Node::null(), mc);\r
Trace("fmc-cover-simplify") << std::endl;\r
std::vector< Node > cond;\r
}\r
Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl;\r
basic_simplify( m );\r
- Trace("fmc-cover-simplify") << "Afterhand: " << std::endl;\r
- debugPrint("fmc-cover-simplify",Node::null(), mc);\r
- Trace("fmc-cover-simplify") << std::endl;\r
- }\r
- }\r
-\r
-\r
-/*\r
- //now do exhaustive covering simplification\r
- if( options::fmfFmcCoverSimplify() && !d_cond.empty() ){\r
- std::vector< int > indices;\r
- std::map< int, std::vector< int > > star_replace;\r
- d_et.exhaustiveSimplify( m, d_cond[0], 0, indices, star_replace );\r
- if( !indices.empty() ){\r
- static bool appSimp = false;\r
- if( !appSimp ){\r
- appSimp = true;\r
- std::cout << "FMC-CS" << std::endl;\r
- }\r
- Trace("fmc-cover-simplify") << "Beforehand: " << std::endl;\r
- debugPrint("fmc-cover-simplify",Node::null(), mc);\r
- Trace("fmc-cover-simplify") << std::endl;\r
- d_has_simplified = false;\r
- Trace("fmc-cover-simplify") << "By exhaustive covering, these indices can be removed : ";\r
- for( unsigned i=0; i<indices.size(); i++) {\r
- Trace("fmc-cover-simplify") << indices[i] << " ";\r
- }\r
- Trace("fmc-cover-simplify") << std::endl;\r
- std::vector< Node > cond;\r
- cond.insert( cond.end(), d_cond.begin(), d_cond.end() );\r
- d_cond.clear();\r
- std::vector< Node > value;\r
- value.insert( value.end(), d_value.begin(), d_value.end() );\r
- d_value.clear();\r
- d_et.reset();\r
- d_has_simplified = false;\r
- for (unsigned i=0; i<cond.size(); i++) {\r
- if( std::find( indices.begin(), indices.end(), i )==indices.end() ){\r
- Node cc = cond[i];\r
- if(star_replace.find(i)!=star_replace.end()) {\r
- std::vector< Node > nc;\r
- nc.push_back( cc.getOperator() );\r
- Trace("fmc-cover-simplify") << "Modify entry : " << cc << std::endl;\r
- for( unsigned j=0; j< cc.getNumChildren(); j++){\r
- if( std::find( star_replace[i].begin(), star_replace[i].end(), j )!=star_replace[i].end() ){\r
- nc.push_back( m->getStar(cc[j].getType()) );\r
- }else{\r
- nc.push_back( cc[j] );\r
- }\r
- }\r
- cc = NodeManager::currentNM()->mkNode( APPLY_UF, nc );\r
- Trace("fmc-cover-simplify") << "Got : " << cc << std::endl;\r
- }\r
- addEntry(m, cc, value[i]);\r
- }\r
- }\r
- Trace("fmc-cover-simplify") << "Finished re-adding entries." << std::endl;\r
- basic_simplify( m );\r
- Trace("fmc-cover-simplify") << "Afterhand: " << std::endl;\r
+ Trace("fmc-cover-simplify") << "After: " << std::endl;\r
debugPrint("fmc-cover-simplify",Node::null(), mc);\r
Trace("fmc-cover-simplify") << std::endl;\r
}\r
}\r
- */\r
}\r
\r
void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {\r
}\r
\r
void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){\r
- d_addedLemmas = 0;\r
FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();\r
if( fullModel ){\r
//make function values\r
//reset the model\r
fm->d_models[op]->reset();\r
\r
- std::vector< Node > conds;\r
- std::vector< Node > values;\r
- std::vector< Node > entry_conds;\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 = fm->getUsedRepresentative(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
+\r
+ std::vector< Node > add_conds;\r
+ std::vector< Node > add_values;\r
+ bool needsDefault = true;\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
+ add_conds.push_back( n );\r
+ add_values.push_back( n );\r
}\r
}\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
+ //possibly get default\r
+ if( needsDefault ){\r
+ Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);\r
+ //add default value if necessary\r
+ if( fm->hasTerm( nmb ) ){\r
+ Trace("fmc-model-debug") << "Add default " << nmb << std::endl;\r
+ add_conds.push_back( nmb );\r
+ add_values.push_back( nmb );\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
+ add_conds.push_back( nmb );\r
+ add_values.push_back( vmb );\r
+ }\r
+ }\r
+\r
+ std::vector< Node > conds;\r
+ std::vector< Node > values;\r
+ std::vector< Node > entry_conds;\r
+ //get the entries for the mdoel\r
+ for( size_t i=0; i<add_conds.size(); i++ ){\r
+ Node c = add_conds[i];\r
+ Node v = add_values[i];\r
+ std::vector< Node > children;\r
+ std::vector< Node > entry_children;\r
+ children.push_back(op);\r
+ entry_children.push_back(op);\r
+ bool hasNonStar = false;\r
+ for( unsigned i=0; i<c.getNumChildren(); i++) {\r
+ Node ri = fm->getUsedRepresentative( c[i]);\r
+ children.push_back(ri);\r
+ if (fm->isModelBasisTerm(ri)) {\r
+ ri = fm->getStar( ri.getType() );\r
+ }else{\r
+ hasNonStar = true;\r
+ }\r
+ entry_children.push_back(ri);\r
+ }\r
+ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
+ Node nv = fm->getUsedRepresentative( v);\r
+ Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );\r
+ if( std::find(conds.begin(), conds.end(), n )==conds.end() ){\r
+ Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;\r
+ conds.push_back(n);\r
+ values.push_back(nv);\r
+ entry_conds.push_back(en);\r
+ }\r
+ else {\r
+ Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;\r
+ }\r
}\r
\r
+\r
//sort based on # default arguments\r
std::vector< int > indices;\r
ModelBasisArgSort mbas;\r
}\r
std::sort( indices.begin(), indices.end(), mbas );\r
\r
-\r
for (int i=0; i<(int)indices.size(); i++) {\r
fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);\r
}\r
fm->d_models[op]->debugPrint("fmc-model", op, this);\r
Trace("fmc-model") << std::endl;\r
\r
+ if( options::fmfFmcInterval() ){\r
+ Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl;\r
+ fm->d_models[op]->debugPrint("fmc-interval-model", op, this);\r
+ Trace("fmc-interval-model") << std::endl;\r
+ std::vector< int > indices;\r
+ for( int i=0; i<(int)fm->d_models[op]->d_cond.size(); i++ ){\r
+ indices.push_back( i );\r
+ }\r
+ std::map< int, std::map< int, Node > > changed_vals;\r
+ makeIntervalModel( fm, op, indices, 0, changed_vals );\r
+ for( std::map< int, std::map< int, Node > >::iterator it = changed_vals.begin(); it != changed_vals.end(); ++it ){\r
+ Trace("fmc-interval-model") << "Entry #" << it->first << " changed : ";\r
+ for( std::map< int, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){\r
+ Trace("fmc-interval-model") << it2->first << " -> " << it2->second << ", ";\r
+ }\r
+ Trace("fmc-interval-model") << std::endl;\r
+ }\r
+ }\r
+\r
+\r
Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;\r
fm->d_models[op]->simplify( this, fm );\r
Trace("fmc-model-simplify") << "After simplification : " << std::endl;\r
}\r
else if(fm->isStar(n) && dispStar) {\r
Trace(tr) << "*";\r
+ }\r
+ else if(fm->isInterval(n)) {\r
+ debugPrint(tr, n[0], dispStar );\r
+ Trace(tr) << "...";\r
+ debugPrint(tr, n[1], dispStar );\r
}else{\r
TypeNode tn = n.getType();\r
if( d_rep_ids.find(tn)!=d_rep_ids.end() ){\r
Trace(tr) << n;\r
}\r
}else{\r
- Trace(tr) << n;\r
+ Trace(tr) << n;\r
}\r
}\r
}\r
\r
\r
-bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) {\r
+bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {\r
Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;\r
- if (!options::fmfModelBasedInst()) {\r
- return false;\r
- }else{\r
+ if( optUseModel() ){\r
FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();\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
+ d_triedLemmas++;\r
if( d_qe->addInstantiation( f, m ) ){\r
- lemmas++;\r
+ d_addedLemmas++;\r
}else{\r
//this can happen if evaluation is unknown\r
//might try it next effort level\r
//get witness for d_star_insts[f][i]\r
int j = d_star_insts[f][i];\r
if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){\r
- int lem = exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j );\r
- if( lem==-1 ){\r
+ if( !exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j ) ){\r
//something went wrong, resort to exhaustive instantiation\r
return false;\r
- }else{\r
- lemmas += lem;\r
}\r
}\r
}\r
}\r
}\r
return true;\r
+ }else{\r
+ return false;\r
}\r
}\r
\r
-int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {\r
- int addedLemmas = 0;\r
+bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {\r
RepSetIterator riter( d_qe, &(fm->d_rep_set) );\r
Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";\r
debugPrintCond("fmc-exh", c, true);\r
Trace("fmc-exh")<< std::endl;\r
if( riter.setQuantifier( f ) ){\r
- std::vector< RepDomain > dom;\r
+ //set the domains based on the entry\r
for (unsigned i=0; i<c.getNumChildren(); i++) {\r
if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {\r
TypeNode tn = c[i].getType();\r
riter.d_domain[i].clear();\r
riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);\r
}else{\r
- return -1;\r
+ return false;\r
}\r
}\r
}else{\r
- return -1;\r
+ return false;\r
}\r
}\r
}\r
int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);\r
Trace("fmc-exh-debug") << ", index = " << ev_index;\r
Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];\r
+ bool successAdd = false;\r
if (ev!=d_true) {\r
InstMatch m;\r
for( int i=0; i<riter.getNumTerms(); i++ ){\r
m.set( d_qe, f, i, riter.getTerm( i ) );\r
}\r
Trace("fmc-exh-debug") << ", add!";\r
+ d_triedLemmas++;\r
//add as instantiation\r
if( d_qe->addInstantiation( f, m ) ){\r
- addedLemmas++;\r
+ Trace("fmc-exh-debug") << " ...success.";\r
+ d_addedLemmas++;\r
+ successAdd = true;\r
}\r
}\r
Trace("fmc-exh-debug") << std::endl;\r
- riter.increment();\r
+ int index = riter.increment();\r
+ Trace("fmc-exh-debug") << "Incremented index " << index << std::endl;\r
+ if (index>=0 && successAdd && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) {\r
+ Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl;\r
+ riter.increment2( index-1 );\r
+ }\r
}\r
+ return true;\r
+ }else{\r
+ return false;\r
}\r
- return addedLemmas;\r
}\r
\r
void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {\r
}\r
\r
\r
+bool FullModelChecker::useSimpleModels() {\r
+ return options::fmfFullModelCheckSimple();\r
+}\r
\r
-void FullModelChecker::addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,\r
- std::vector< Node > & conds,\r
- std::vector< Node > & values,\r
- std::vector< Node > & entry_conds ) {\r
- std::vector< Node > children;\r
- std::vector< Node > entry_children;\r
- children.push_back(op);\r
- entry_children.push_back(op);\r
- bool hasNonStar = false;\r
- for( unsigned i=0; i<c.getNumChildren(); i++) {\r
- Node ri = fm->getUsedRepresentative( c[i]);\r
- children.push_back(ri);\r
- if (fm->isModelBasisTerm(ri)) {\r
- ri = fm->getStar( ri.getType() );\r
+void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,\r
+ std::map< int, std::map< int, Node > >& changed_vals ) {\r
+ if( index==(int)fm->d_models[op]->d_cond[0].getNumChildren() ){\r
+ makeIntervalModel2( fm, op, indices, 0, changed_vals );\r
+ }else{\r
+ TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();\r
+ if( tn.isInteger() ){\r
+ makeIntervalModel(fm,op,indices,index+1, changed_vals );\r
}else{\r
- hasNonStar = true;\r
+ std::map< Node, std::vector< int > > new_indices;\r
+ for( unsigned i=0; i<indices.size(); i++ ){\r
+ Node v = fm->d_models[op]->d_cond[indices[i]][index];\r
+ new_indices[v].push_back( i );\r
+ }\r
+\r
+ for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){\r
+ makeIntervalModel( fm, op, it->second, index+1, changed_vals );\r
+ }\r
}\r
- entry_children.push_back(ri);\r
- }\r
- Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
- Node nv = fm->getUsedRepresentative( v);\r
- Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );\r
- if( std::find(conds.begin(), conds.end(), n )==conds.end() ){\r
- Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;\r
- conds.push_back(n);\r
- values.push_back(nv);\r
- entry_conds.push_back(en);\r
- }\r
- else {\r
- Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;\r
}\r
}\r
\r
-bool FullModelChecker::useSimpleModels() {\r
- return options::fmfFullModelCheckSimple();\r
-}\r
+void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,\r
+ std::map< int, std::map< int, Node > >& changed_vals ) {\r
+ if( index<(int)fm->d_models[op]->d_cond[0].getNumChildren() ){\r
+ TypeNode tn = fm->d_models[op]->d_cond[0][index].getType();\r
+ if( tn.isInteger() ){\r
+ std::map< Node, std::vector< int > > new_indices;\r
+ for( unsigned i=0; i<indices.size(); i++ ){\r
+ Node v = fm->d_models[op]->d_cond[indices[i]][index];\r
+ new_indices[v].push_back( i );\r
+ }\r
+\r
+ std::vector< Node > values;\r
+ for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){\r
+ makeIntervalModel2( fm, op, it->second, index+1, changed_vals );\r
+ if( !fm->isStar(it->first) ){\r
+ values.push_back( it->first );\r
+ }\r
+ }\r
+\r
+ if( tn.isInteger() ){\r
+ //sort values by size\r
+ ConstRationalSort crs;\r
+ std::vector< int > sindices;\r
+ for( unsigned i=0; i<values.size(); i++ ){\r
+ sindices.push_back( (int)i );\r
+ crs.d_terms.push_back( values[i] );\r
+ }\r
+ std::sort( sindices.begin(), sindices.end(), crs );\r
+\r
+ Node ub = fm->getStar( tn );\r
+ for( int i=(int)(sindices.size()-1); i>=0; i-- ){\r
+ Node lb = fm->getStar( tn );\r
+ if( i>0 ){\r
+ lb = values[sindices[i]];\r
+ }\r
+ Node interval = fm->getInterval( lb, ub );\r
+ for( unsigned j=0; j<new_indices[values[sindices[i]]].size(); j++ ){\r
+ changed_vals[new_indices[values[sindices[i]]][j]][index] = interval;\r
+ }\r
+ ub = lb;\r
+ }\r
+ }\r
+ }else{\r
+ makeIntervalModel2( fm, op, indices, index+1, changed_vals );\r
+ }\r
+ }\r
+}
\ No newline at end of file
void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );\r
\r
bool isCovered(FirstOrderModelFmc * m, Node c, int index);\r
-\r
- //void exhaustiveSimplify( FirstOrderModelFmc * m, Node c, int index, std::vector< int >& indices,\r
- // std::map< int, std::vector< int > >& star_replace );\r
void collectIndices(Node c, int index, std::vector< int >& indices );\r
bool isComplete(FirstOrderModelFmc * m, Node c, int index);\r
};\r
std::map<Node, std::map< Node, int > > d_quant_var_id;\r
std::map<Node, std::vector< int > > d_star_insts;\r
Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);\r
- int exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);\r
+ bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);\r
protected:\r
- void addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,\r
- std::vector< Node > & conds,\r
- std::vector< Node > & values,\r
- std::vector< Node > & entry_conds );\r
+ void makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,\r
+ std::map< int, std::map< int, Node > >& changed_vals );\r
+ void makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index,\r
+ std::map< int, std::map< int, Node > >& changed_vals );\r
private:\r
void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );\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
- bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas );\r
+ bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );\r
\r
Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );\r
\r
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::isQuantifierActive( Node f ) {
debugModel( fm );
}else{
d_curr_model = fm;
- d_addedLemmas = 0;
d_didInstGen = false;
//reset the internal information
reset( fm );
}
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 )
+ d_num_quants_init("QModelBuilderIG::Number_Quantifiers", 0),
+ d_num_partial_quants_init("QModelBuilderIG::Number_Partial_Quantifiers", 0),
+ d_init_inst_gen_lemmas("QModelBuilderIG::Initialize_Inst_Gen_Lemmas", 0 ),
+ d_inst_gen_lemmas("QModelBuilderIG::Inst_Gen_Lemmas", 0 ),
+ d_eval_formulas("QModelBuilderIG::Eval_Formulas", 0 ),
+ d_eval_uf_terms("QModelBuilderIG::Eval_Uf_Terms", 0 ),
+ d_eval_lits("QModelBuilderIG::Eval_Lits", 0 ),
+ d_eval_lits_unknown("QModelBuilderIG::Eval_Lits_Unknown", 0 )
{
StatisticsRegistry::registerStat(&d_num_quants_init);
StatisticsRegistry::registerStat(&d_num_partial_quants_init);
StatisticsRegistry::registerStat(&d_init_inst_gen_lemmas);
StatisticsRegistry::registerStat(&d_inst_gen_lemmas);
+ StatisticsRegistry::registerStat(&d_eval_formulas);
+ StatisticsRegistry::registerStat(&d_eval_uf_terms);
+ StatisticsRegistry::registerStat(&d_eval_lits);
+ StatisticsRegistry::registerStat(&d_eval_lits_unknown);
}
QModelBuilderIG::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_num_partial_quants_init);
StatisticsRegistry::unregisterStat(&d_init_inst_gen_lemmas);
StatisticsRegistry::unregisterStat(&d_inst_gen_lemmas);
+ StatisticsRegistry::unregisterStat(&d_eval_formulas);
+ StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
+ StatisticsRegistry::unregisterStat(&d_eval_lits);
+ StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
}
bool QModelBuilderIG::isQuantifierActive( Node f ){
}
+//do exhaustive instantiation
+bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) {
+ if( optUseModel() ){
+
+ RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) );
+ if( riter.setQuantifier( f ) ){
+ FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel();
+ Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
+ fmig->resetEvaluate();
+ Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
+ while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
+ d_triedLemmas++;
+ for( int i=0; i<(int)riter.d_index.size(); i++ ){
+ Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl;
+ }
+ int eval = 0;
+ int depIndex;
+ //see if instantiation is already true in current model
+ Debug("fmf-model-eval") << "Evaluating ";
+ riter.debugPrintSmall("fmf-model-eval");
+ Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+ //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 = fmig->evaluate( d_qe->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
+ if( eval==1 ){
+ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
+ }else{
+ Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+ }
+ if( eval==1 ){
+ //instantiation is already true -> skip
+ riter.increment2( depIndex );
+ }else{
+ //instantiation was not shown to be true, construct the match
+ InstMatch m;
+ for( int i=0; i<riter.getNumTerms(); i++ ){
+ m.set( d_qe, f, riter.d_index_order[i], riter.getTerm( i ) );
+ }
+ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+ //add as instantiation
+ if( d_qe->addInstantiation( f, m ) ){
+ d_addedLemmas++;
+ //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
+ if( eval==-1 ){
+ riter.increment2( depIndex );
+ }else{
+ riter.increment();
+ }
+ }else{
+ Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
+ riter.increment();
+ }
+ }
+ }
+ //print debugging information
+ if( fmig ){
+ d_statistics.d_eval_formulas += fmig->d_eval_formulas;
+ d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
+ d_statistics.d_eval_lits += fmig->d_eval_lits;
+ d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
+ }
+ Trace("inst-fmf-ei") << "Finished: " << std::endl;
+ Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl;
+ Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl;
+ if( d_addedLemmas>1000 ){
+ Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+ Trace("model-engine-warn") << " Inst Tried: " << d_triedLemmas << std::endl;
+ Trace("model-engine-warn") << " Inst Added: " << d_addedLemmas << std::endl;
+ Trace("model-engine-warn") << std::endl;
+ }
+ }
+ //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+ d_incomplete_check = riter.d_incomplete;
+ return true;
+ }else{
+ return false;
+ }
+}
+
void QModelBuilderDefault::reset( FirstOrderModel* fm ){
// is quantifier active?
virtual bool isQuantifierActive( Node f );
//do exhaustive instantiation
- virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas ) { return false; }
+ virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; }
//whether to construct model
virtual bool optUseModel();
- /** number of lemmas generated while building model */
- int d_addedLemmas;
//consider axioms
bool d_considerAxioms;
+ /** number of lemmas generated while building model */
+ //is the exhaustive instantiation incomplete?
+ bool d_incomplete_check;
+ int d_addedLemmas;
+ int d_triedLemmas;
/** exist instantiation ? */
virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; }
//debug model
IntStat d_num_partial_quants_init;
IntStat d_init_inst_gen_lemmas;
IntStat d_inst_gen_lemmas;
+ IntStat d_eval_formulas;
+ IntStat d_eval_uf_terms;
+ IntStat d_eval_lits;
+ IntStat d_eval_lits_unknown;
Statistics();
~Statistics();
};
bool didInstGen() { return d_didInstGen; }
// is quantifier active?
bool isQuantifierActive( Node f );
+ //do exhaustive instantiation
+ bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort );
//temporary stats
int d_numQuantSat;
#include "theory/quantifiers/term_database.h"
#include "theory/quantifiers/quantifiers_attributes.h"
-#define EVAL_FAIL_SKIP_MULTIPLE
-
using namespace std;
using namespace CVC4;
using namespace CVC4::kind;
//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, false );
addedLemmas += (int)d_builder->d_addedLemmas;
//if builder has lemmas, add and return
}
-bool ModelEngine::optOneInstPerQuantRound(){
- return options::fmfOneInstPerRound();
-}
-
-bool ModelEngine::optUseRelevantDomain(){
- return options::fmfRelevantDomain();
-}
-
bool ModelEngine::optOneQuantPerRound(){
return options::fmfOneQuantPerRound();
}
-bool ModelEngine::optExhInstEvalSkipMultiple(){
-#ifdef EVAL_FAIL_SKIP_MULTIPLE
- return true;
-#else
- return false;
-#endif
-}
int ModelEngine::checkModel(){
- int addedLemmas = 0;
FirstOrderModel* fm = d_quantEngine->getModel();
//for debugging
if( Trace.isOn("model-engine") || Trace.isOn("model-engine-debug") ){
}
}
}
- //compute the relevant domain if necessary
- //if( optUseRelevantDomain() ){
- //}
+ //relevant domain?
+
d_triedLemmas = 0;
- d_testLemmas = 0;
- d_relevantLemmas = 0;
+ d_addedLemmas = 0;
d_totalLemmas = 0;
+ //for statistics
+ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ int totalInst = 1;
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ TypeNode tn = f[0][i].getType();
+ if( fm->d_rep_set.hasType( tn ) ){
+ totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+ }
+ }
+ d_totalLemmas += totalInst;
+ }
+
Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1;
for( int e=0; e<e_max; e++) {
- if (addedLemmas==0) {
+ if (d_addedLemmas==0) {
for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
Node f = fm->getAssertedQuantifier( i );
- //keep track of total instantiations for statistics
- int totalInst = 1;
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- TypeNode tn = f[0][i].getType();
- if( fm->d_rep_set.hasType( tn ) ){
- totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
- }
- }
- d_totalLemmas += totalInst;
//determine if we should check this quantifier
if( d_builder->isQuantifierActive( f ) ){
- addedLemmas += exhaustiveInstantiate( f, e );
+ exhaustiveInstantiate( f, e );
if( Trace.isOn("model-engine-warn") ){
- if( addedLemmas>10000 ){
+ if( d_addedLemmas>10000 ){
Debug("fmf-exit") << std::endl;
debugPrint("fmf-exit");
exit( 0 );
}
}
- if( optOneQuantPerRound() && addedLemmas>0 ){
+ if( optOneQuantPerRound() && d_addedLemmas>0 ){
break;
}
}
//print debug information
if( Trace.isOn("model-engine") ){
Trace("model-engine") << "Instantiate axioms : " << ( d_builder->d_considerAxioms ? "yes" : "no" ) << std::endl;
- Trace("model-engine") << "Added Lemmas = " << addedLemmas << " / " << d_triedLemmas << " / ";
- Trace("model-engine") << d_testLemmas << " / " << d_relevantLemmas << " / " << d_totalLemmas << std::endl;
+ Trace("model-engine") << "Added Lemmas = " << d_addedLemmas << " / " << d_triedLemmas << " / ";
+ Trace("model-engine") << d_totalLemmas << std::endl;
}
- d_statistics.d_exh_inst_lemmas += addedLemmas;
- return addedLemmas;
+ d_statistics.d_exh_inst_lemmas += d_addedLemmas;
+ return d_addedLemmas;
}
-int ModelEngine::exhaustiveInstantiate( Node f, int effort ){
- int addedLemmas = 0;
+void ModelEngine::exhaustiveInstantiate( Node f, int effort ){
//first check if the builder can do the exhaustive instantiation
- if( !d_builder->doExhaustiveInstantiation( d_quantEngine->getModel(), f, effort, addedLemmas ) ){
+ 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 ) ){
+ d_triedLemmas += d_builder->d_triedLemmas;
+ d_addedLemmas += d_builder->d_addedLemmas;
+ d_incomplete_check = d_incomplete_check || d_builder->d_incomplete_check;
+ }else{
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++ ){
//create a rep set iterator and iterate over the (relevant) domain of the quantifier
RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) );
if( riter.setQuantifier( f ) ){
- FirstOrderModelIG * fmig = NULL;
- if( !options::fmfFullModelCheck() ){
- fmig = (FirstOrderModelIG*)d_quantEngine->getModel();
- Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
- fmig->resetEvaluate();
- }
Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
- int tests = 0;
int triedLemmas = 0;
- while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
- for( int i=0; i<(int)riter.d_index.size(); i++ ){
- Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl;
- }
- d_testLemmas++;
- int eval = 0;
- int depIndex;
- if( d_builder->optUseModel() && fmig ){
- //see if instantiation is already true in current model
- Debug("fmf-model-eval") << "Evaluating ";
- riter.debugPrintSmall("fmf-model-eval");
- Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
- tests++;
- //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 = fmig->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
- if( eval==1 ){
- Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
- }else{
- Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
- }
+ int addedLemmas = 0;
+ while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){
+ //instantiation was not shown to be true, construct the match
+ InstMatch m;
+ for( int i=0; i<riter.getNumTerms(); i++ ){
+ m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
}
- if( eval==1 ){
- //instantiation is already true -> skip
- riter.increment2( depIndex );
+ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+ triedLemmas++;
+ //add as instantiation
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ addedLemmas++;
}else{
- //instantiation was not shown to be true, construct the match
- InstMatch m;
- for( int i=0; i<riter.getNumTerms(); i++ ){
- m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
- }
- Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
- triedLemmas++;
- d_triedLemmas++;
- //add as instantiation
- if( d_quantEngine->addInstantiation( f, m ) ){
- addedLemmas++;
- //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
- if( eval==-1 && optExhInstEvalSkipMultiple() ){
- riter.increment2( depIndex );
- }else{
- riter.increment();
- }
- }else{
- Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
- riter.increment();
- }
+ Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
}
+ riter.increment();
}
- //print debugging information
- if( fmig ){
- d_statistics.d_eval_formulas += fmig->d_eval_formulas;
- d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms;
- d_statistics.d_eval_lits += fmig->d_eval_lits;
- d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown;
- }
- int relevantInst = 1;
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- relevantInst = relevantInst * (int)riter.d_domain[i].size();
- }
- d_relevantLemmas += relevantInst;
- Trace("inst-fmf-ei") << "Finished: " << std::endl;
- //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl;
- Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl;
- Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl;
- Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl;
- Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl;
- if( addedLemmas>1000 ){
- Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
- //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl;
- Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl;
- Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl;
- Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl;
- Trace("model-engine-warn") << " # Tests: " << tests << std::endl;
- Trace("model-engine-warn") << std::endl;
- }
+ d_addedLemmas += addedLemmas;
+ d_triedLemmas += triedLemmas;
}
- //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+ //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
d_incomplete_check = d_incomplete_check || riter.d_incomplete;
}
- return addedLemmas;
}
void ModelEngine::debugPrint( const char* c ){
ModelEngine::Statistics::Statistics():
d_inst_rounds("ModelEngine::Inst_Rounds", 0),
- d_eval_formulas("ModelEngine::Eval_Formulas", 0 ),
- d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ),
- d_eval_lits("ModelEngine::Eval_Lits", 0 ),
- d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ),
d_exh_inst_lemmas("ModelEngine::Exhaustive_Instantiation_Lemmas", 0 )
{
StatisticsRegistry::registerStat(&d_inst_rounds);
- StatisticsRegistry::registerStat(&d_eval_formulas);
- StatisticsRegistry::registerStat(&d_eval_uf_terms);
- StatisticsRegistry::registerStat(&d_eval_lits);
- StatisticsRegistry::registerStat(&d_eval_lits_unknown);
StatisticsRegistry::registerStat(&d_exh_inst_lemmas);
}
ModelEngine::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_inst_rounds);
- StatisticsRegistry::unregisterStat(&d_eval_formulas);
- StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
- StatisticsRegistry::unregisterStat(&d_eval_lits);
- StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
StatisticsRegistry::unregisterStat(&d_exh_inst_lemmas);
}
/** builder class */
QModelBuilder* d_builder;
private: //analysis of current model:
- //is the exhaustive instantiation incomplete?
- bool d_incomplete_check;
private:
//options
- bool optOneInstPerQuantRound();
- bool optUseRelevantDomain();
bool optOneQuantPerRound();
- bool optExhInstEvalSkipMultiple();
private:
//check model
int checkModel();
- //exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
- int exhaustiveInstantiate( Node f, int effort = 0 );
+ //exhaustively instantiate quantifier (possibly using mbqi)
+ void exhaustiveInstantiate( Node f, int effort = 0 );
private:
//temporary statistics
+ //is the exhaustive instantiation incomplete?
+ bool d_incomplete_check;
+ int d_addedLemmas;
int d_triedLemmas;
- int d_testLemmas;
int d_totalLemmas;
- int d_relevantLemmas;
public:
ModelEngine( context::Context* c, QuantifiersEngine* qe );
~ModelEngine(){}
class Statistics {
public:
IntStat d_inst_rounds;
- IntStat d_eval_formulas;
- IntStat d_eval_uf_terms;
- IntStat d_eval_lits;
- IntStat d_eval_lits_unknown;
IntStat d_exh_inst_lemmas;
Statistics();
~Statistics();
disable simple models in full model check for finite model finding
option fmfFmcCoverSimplify --fmf-fmc-cover-simplify bool :default false
apply covering simplification technique to fmc models
+option fmfFmcInterval --fmf-fmc-interval bool :default false
+ construct interval models for fmc models
option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false
only add one instantiation per quantifier per round for fmf
struct QRewriteRuleAttributeId {};
typedef expr::Attribute<QRewriteRuleAttributeId, Node> QRewriteRuleAttribute;
+//for bounded integers
+struct BoundIntLitAttributeId {};
+typedef expr::Attribute<BoundIntLitAttributeId, uint64_t> BoundIntLitAttribute;
+
class QuantifiersEngine;
return true;
}
-void RepSetIterator::increment2( int counter ){
+int RepSetIterator::increment2( int counter ){
Assert( !isFinished() );
#ifdef DISABLE_EVAL_SKIP_MULTIPLE
counter = (int)d_index.size()-1;
}
if( emptyDomain ){
Trace("rsi-debug") << "This is an empty domain, increment again." << std::endl;
- increment();
+ return increment();
}
}
+ return counter;
}
-void RepSetIterator::increment(){
+int RepSetIterator::increment(){
if( !isFinished() ){
- increment2( (int)d_index.size()-1 );
+ return increment2( (int)d_index.size()-1 );
+ }else{
+ return -1;
}
}
public:
/** set index order */
void setIndexOrder( std::vector< int >& indexOrder );
- /** set domain */
- //void setDomain( std::vector< RepDomain >& domain );
/** increment the iterator at index=counter */
- void increment2( int counter );
+ int increment2( int counter );
/** increment the iterator */
- void increment();
+ int increment();
/** is the iterator finished? */
bool isFinished();
/** get the i_th term we are considering */
if( applyTotality( d_aloc_cardinality ) ){
//must generate new cardinality lemma term
Node var;
- //if( d_aloc_cardinality==1 ){
+ if( d_aloc_cardinality==1 && !options::ufssTotalitySymBreak() ){
//get arbitrary ground term
- //var = d_cardinality_term;
- //}else{
+ var = d_cardinality_term;
+ }else{
std::stringstream ss;
ss << "_c_" << d_aloc_cardinality;
var = NodeManager::currentNM()->mkSkolem( ss.str(), d_type, "is a cardinality lemma term" );
- //}
+ }
d_totality_terms[0].push_back( var );
Trace("mkVar") << "allocateCardinality, mkVar : " << var << " : " << d_type << std::endl;
//must be distinct from all other cardinality terms
projects / cvc5.git / commitdiff