summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/full_model_check.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/full_model_check.cpp')
-rw-r--r--src/theory/quantifiers/full_model_check.cpp347
1 files changed, 176 insertions, 171 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 7e528fef3..ac23dae29 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -257,7 +257,9 @@ void Def::basic_simplify( FirstOrderModelFmc * m ) {
}
void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
+ Trace("fmc-simplify") << "Simplify definition, #cond = " << d_cond.size() << std::endl;
basic_simplify( m );
+ Trace("fmc-simplify") << "post-basic simplify, #cond = " << d_cond.size() << std::endl;
//check if the last entry is not all star, if so, we can make the last entry all stars
if( !d_cond.empty() ){
@@ -300,6 +302,7 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) {
Trace("fmc-cover-simplify") << std::endl;
}
}
+ Trace("fmc-simplify") << "finish simplify, #cond = " << d_cond.size() << std::endl;
}
void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
@@ -325,94 +328,96 @@ QModelBuilder( c, qe ){
d_false = NodeManager::currentNM()->mkConst(false);
}
-void FullModelChecker::preProcessBuildModel(TheoryModel* m, bool fullModel) {
+bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
//standard pre-process
- preProcessBuildModelStd( m, fullModel );
+ if( !preProcessBuildModelStd( m ) ){
+ return false;
+ }
FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
- if( !fullModel ){
- Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
- d_preinitialized_types.clear();
- //traverse equality engine
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
- while( !eqcs_i.isFinished() ){
- TypeNode tr = (*eqcs_i).getType();
- d_preinitialized_types[tr] = true;
- ++eqcs_i;
- }
+ Trace("fmc") << "---Full Model Check preprocess() " << std::endl;
+ d_preinitialized_types.clear();
+ //traverse equality engine
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( fm->d_equalityEngine );
+ while( !eqcs_i.isFinished() ){
+ TypeNode tr = (*eqcs_i).getType();
+ d_preinitialized_types[tr] = true;
+ ++eqcs_i;
+ }
- //must ensure model basis terms exists in model for each relevant type
- fm->initialize();
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
- Node op = it->first;
- TypeNode tno = op.getType();
- for( unsigned i=0; i<tno.getNumChildren(); i++) {
- preInitializeType( fm, tno[i] );
- }
+ //must ensure model basis terms exists in model for each relevant type
+ fm->initialize();
+ for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ Node op = it->first;
+ TypeNode tno = op.getType();
+ for( unsigned i=0; i<tno.getNumChildren(); i++) {
+ preInitializeType( fm, tno[i] );
}
- //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
- if( !options::fmfEmptySorts() ){
- for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node q = fm->getAssertedQuantifier( i );
- //make sure all types are set
- for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
- preInitializeType( fm, q[0][j].getType() );
- }
+ }
+ //do not have to introduce terms for sorts of domains of quantified formulas if we are allowed to assume empty sorts
+ if( !options::fmfEmptySorts() ){
+ for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node q = fm->getAssertedQuantifier( i );
+ //make sure all types are set
+ for( unsigned j=0; j<q[0].getNumChildren(); j++ ){
+ preInitializeType( fm, q[0][j].getType() );
}
}
}
+ return true;
}
-void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
+bool FullModelChecker::processBuildModel(TheoryModel* m){
FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
- if( !fullModel ){
- Trace("fmc") << "---Full Model Check reset() " << std::endl;
- d_quant_models.clear();
- d_rep_ids.clear();
- d_star_insts.clear();
- //process representatives
- for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
- it != fm->d_rep_set.d_type_reps.end(); ++it ){
- if( it->first.isSort() ){
- Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
- for( size_t a=0; a<it->second.size(); a++ ){
- Node r = fm->getUsedRepresentative( it->second[a] );
- if( Trace.isOn("fmc-model-debug") ){
- std::vector< Node > eqc;
- ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
- Trace("fmc-model-debug") << " " << (it->second[a]==r);
- Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
- //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
- Trace("fmc-model-debug") << " {";
- for( size_t i=0; i<eqc.size(); i++ ){
- Trace("fmc-model-debug") << eqc[i] << ", ";
- }
- Trace("fmc-model-debug") << "}" << std::endl;
+ Trace("fmc") << "---Full Model Check reset() " << std::endl;
+ d_quant_models.clear();
+ d_rep_ids.clear();
+ d_star_insts.clear();
+ //process representatives
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){
+ if( it->first.isSort() ){
+ Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
+ for( size_t a=0; a<it->second.size(); a++ ){
+ Node r = fm->getUsedRepresentative( it->second[a] );
+ if( Trace.isOn("fmc-model-debug") ){
+ std::vector< Node > eqc;
+ ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
+ Trace("fmc-model-debug") << " " << (it->second[a]==r);
+ Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";
+ //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";
+ Trace("fmc-model-debug") << " {";
+ for( size_t i=0; i<eqc.size(); i++ ){
+ Trace("fmc-model-debug") << eqc[i] << ", ";
}
- d_rep_ids[it->first][r] = (int)a;
+ Trace("fmc-model-debug") << "}" << std::endl;
}
- Trace("fmc-model-debug") << std::endl;
+ d_rep_ids[it->first][r] = (int)a;
}
+ Trace("fmc-model-debug") << std::endl;
}
+ }
- //now, make models
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
- Node op = it->first;
- //reset the model
- fm->d_models[op]->reset();
-
- Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;
- std::vector< Node > add_conds;
- std::vector< Node > add_values;
- bool needsDefault = true;
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
- Node n = fm->d_uf_terms[op][i];
+ //now, make models
+ for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ Node op = it->first;
+ //reset the model
+ fm->d_models[op]->reset();
+
+ std::vector< Node > add_conds;
+ std::vector< Node > add_values;
+ bool needsDefault = true;
+ std::map< Node, std::vector< Node > >::iterator itut = fm->d_uf_terms.find( op );
+ if( itut!=fm->d_uf_terms.end() ){
+ Trace("fmc-model-debug") << itut->second.size() << " model values for " << op << " ... " << std::endl;
+ for( size_t i=0; i<itut->second.size(); i++ ){
+ Node n = itut->second[i];
if( d_qe->getTermDatabase()->isTermActive( n ) ){
add_conds.push_back( n );
add_values.push_back( n );
Node r = fm->getUsedRepresentative(n);
Trace("fmc-model-debug") << n << " -> " << r << std::endl;
- //AlwaysAssert( fm->areEqual( fm->d_uf_terms[op][i], r ) );
+ //AlwaysAssert( fm->areEqual( itut->second[i], r ) );
}else{
if( Trace.isOn("fmc-model-debug") ){
Node r = fm->getUsedRepresentative(n);
@@ -420,127 +425,126 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
}
}
}
- Trace("fmc-model-debug") << std::endl;
- //possibly get default
- if( needsDefault ){
- Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
- //add default value if necessary
- if( fm->hasTerm( nmb ) ){
- Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
- add_conds.push_back( nmb );
- add_values.push_back( nmb );
- }else{
- Node vmb = getSomeDomainElement(fm, nmb.getType());
- Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
- Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
- add_conds.push_back( nmb );
- add_values.push_back( vmb );
- }
+ }else{
+ Trace("fmc-model-debug") << "No model values for " << op << " ... " << std::endl;
+ }
+ Trace("fmc-model-debug") << std::endl;
+ //possibly get default
+ if( needsDefault ){
+ Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+ //add default value if necessary
+ if( fm->hasTerm( nmb ) ){
+ Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
+ add_conds.push_back( nmb );
+ add_values.push_back( nmb );
+ }else{
+ Node vmb = getSomeDomainElement(fm, nmb.getType());
+ Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
+ Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
+ add_conds.push_back( nmb );
+ add_values.push_back( vmb );
}
+ }
- std::vector< Node > conds;
- std::vector< Node > values;
- std::vector< Node > entry_conds;
- //get the entries for the mdoel
- for( size_t i=0; i<add_conds.size(); i++ ){
- Node c = add_conds[i];
- Node v = add_values[i];
- std::vector< Node > children;
- std::vector< Node > entry_children;
- children.push_back(op);
- entry_children.push_back(op);
- bool hasNonStar = false;
- for( unsigned i=0; i<c.getNumChildren(); i++) {
- Node ri = fm->getUsedRepresentative( c[i] );
- children.push_back(ri);
- bool isStar = false;
- if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
- if (fm->isModelBasisTerm(ri) ) {
- ri = fm->getStar( ri.getType() );
- isStar = true;
- }else{
- hasNonStar = true;
- }
- }
- if( !isStar && !ri.isConst() ){
- Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
- Assert( false );
+ std::vector< Node > conds;
+ std::vector< Node > values;
+ std::vector< Node > entry_conds;
+ //get the entries for the mdoel
+ for( size_t i=0; i<add_conds.size(); i++ ){
+ Node c = add_conds[i];
+ Node v = add_values[i];
+ std::vector< Node > children;
+ std::vector< Node > entry_children;
+ children.push_back(op);
+ entry_children.push_back(op);
+ bool hasNonStar = false;
+ for( unsigned i=0; i<c.getNumChildren(); i++) {
+ Node ri = fm->getUsedRepresentative( c[i] );
+ children.push_back(ri);
+ bool isStar = false;
+ if( options::mbqiMode()!=quantifiers::MBQI_FMC_INTERVAL || !ri.getType().isInteger() ){
+ if (fm->isModelBasisTerm(ri) ) {
+ ri = fm->getStar( ri.getType() );
+ isStar = true;
+ }else{
+ hasNonStar = true;
}
- entry_children.push_back(ri);
}
- Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
- Node nv = fm->getUsedRepresentative( v );
- if( !nv.isConst() ){
- Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
+ if( !isStar && !ri.isConst() ){
+ Trace("fmc-warn") << "Warning : model for " << op << " has non-constant argument in model " << ri << " (from " << c[i] << ")" << std::endl;
Assert( false );
}
- Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
- if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
- Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
- conds.push_back(n);
- values.push_back(nv);
- entry_conds.push_back(en);
- }
- else {
- Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
- }
+ entry_children.push_back(ri);
+ }
+ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+ Node nv = fm->getUsedRepresentative( v );
+ if( !nv.isConst() ){
+ Trace("fmc-warn") << "Warning : model for " << op << " has non-constant value in model " << nv << std::endl;
+ Assert( false );
+ }
+ Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
+ if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
+ Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
+ conds.push_back(n);
+ values.push_back(nv);
+ entry_conds.push_back(en);
}
+ else {
+ Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
+ }
+ }
- //sort based on # default arguments
- std::vector< int > indices;
- ModelBasisArgSort mbas;
- for (int i=0; i<(int)conds.size(); i++) {
- d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
- mbas.d_terms.push_back(conds[i]);
- indices.push_back(i);
- }
- std::sort( indices.begin(), indices.end(), mbas );
+ //sort based on # default arguments
+ std::vector< int > indices;
+ ModelBasisArgSort mbas;
+ for (int i=0; i<(int)conds.size(); i++) {
+ d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
+ mbas.d_terms.push_back(conds[i]);
+ indices.push_back(i);
+ }
+ std::sort( indices.begin(), indices.end(), mbas );
- for (int i=0; i<(int)indices.size(); i++) {
- fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
- }
+ for (int i=0; i<(int)indices.size(); i++) {
+ fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
+ }
- if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){
- convertIntervalModel( fm, op );
- }
+ if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL ){
+ convertIntervalModel( fm, op );
+ }
- Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
- fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
- Trace("fmc-model-simplify") << std::endl;
+ Trace("fmc-model-simplify") << "Before simplification : " << std::endl;
+ fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
+ Trace("fmc-model-simplify") << std::endl;
- Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;
- fm->d_models[op]->simplify( this, fm );
+ Trace("fmc-model-simplify") << "Simplifying " << op << "..." << std::endl;
+ fm->d_models[op]->simplify( this, fm );
- fm->d_models[op]->debugPrint("fmc-model", op, this);
- Trace("fmc-model") << std::endl;
+ fm->d_models[op]->debugPrint("fmc-model", op, this);
+ Trace("fmc-model") << std::endl;
- //for debugging
- /*
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
- std::vector< Node > inst;
- for( unsigned j=0; j<fm->d_uf_terms[op][i].getNumChildren(); j++ ){
- Node r = fm->getUsedRepresentative( fm->d_uf_terms[op][i][j] );
- inst.push_back( r );
- }
- Node ev = fm->d_models[op]->evaluate( fm, inst );
- Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl;
- AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) );
+ //for debugging
+ /*
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+ std::vector< Node > inst;
+ for( unsigned j=0; j<fm->d_uf_terms[op][i].getNumChildren(); j++ ){
+ Node r = fm->getUsedRepresentative( fm->d_uf_terms[op][i][j] );
+ inst.push_back( r );
}
- */
- }
- }else{
- //make function values
- for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
- m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );
+ Node ev = fm->d_models[op]->evaluate( fm, inst );
+ Trace("fmc-model-debug") << ".....Checking eval( " << fm->d_uf_terms[op][i] << " ) = " << ev << std::endl;
+ AlwaysAssert( fm->areEqual( ev, fm->d_uf_terms[op][i] ) );
}
- TheoryEngineModelBuilder::processBuildModel( m, fullModel );
- //mark that the model has been set
- fm->markModelSet();
- //debug the model
- debugModel( fm );
+ */
+ }
+ Assert( d_addedLemmas==0 );
+
+ //make function values
+ for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){
+ m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" );
}
+ return TheoryEngineModelBuilder::processBuildModel( m );
}
void FullModelChecker::preInitializeType( FirstOrderModelFmc * fm, TypeNode tn ){
@@ -617,6 +621,7 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i
//model check the quantifier
doCheck(fmfmc, f, d_quant_models[f], f[1]);
Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
+ Assert( !d_quant_models[f].d_cond.empty() );
d_quant_models[f].debugPrint("fmc", Node::null(), this);
Trace("fmc") << std::endl;
@@ -890,7 +895,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
*/
} else {
if( !var_ch.empty() ){
- if( n.getKind()==EQUAL ){
+ if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
if( var_ch.size()==2 ){
Trace("fmc-debug") << "Do variable equality " << n << std::endl;
doVariableEquality( fm, f, d, n );
@@ -1273,7 +1278,7 @@ Node FullModelChecker::mkArrayCond( Node a ) {
}
Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {
- if( n.getKind()==EQUAL ){
+ if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
if (!vals[0].isNull() && !vals[1].isNull()) {
return vals[0]==vals[1] ? d_true : d_false;
}else{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback