From a23c5715ce7cd279d83e75b232fd24b5c53032ba Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 28 Jun 2013 15:46:13 -0500 Subject: [PATCH] More bug fixes for interval models. --- src/theory/quantifiers/first_order_model.cpp | 14 ++- src/theory/quantifiers/first_order_model.h | 1 + src/theory/quantifiers/full_model_check.cpp | 107 +++++++++++-------- src/theory/quantifiers/full_model_check.h | 2 + src/theory/quantifiers/model_builder.cpp | 37 ++++--- src/theory/quantifiers/model_builder.h | 2 + src/theory/quantifiers/model_engine.cpp | 5 +- src/theory/quantifiers/options | 6 +- 8 files changed, 112 insertions(+), 62 deletions(-) diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 60d62391b..be6844a1e 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -665,4 +665,16 @@ bool FirstOrderModelFmc::isInterval(Node n) { Node FirstOrderModelFmc::getInterval( Node lb, Node ub ){ return NodeManager::currentNM()->mkNode( APPLY_UF, intervalOp, lb, ub ); -} \ No newline at end of file +} + +bool FirstOrderModelFmc::isInRange( Node v, Node i ) { + for( unsigned b=0; b<2; b++ ){ + if( !isStar( i[b] ) ){ + if( ( b==0 && i[b].getConst() > v.getConst() ) || + ( b==1 && i[b].getConst() <= v.getConst() ) ){ + return false; + } + } + } + return true; +} diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 14e9441b4..f6e012660 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -155,6 +155,7 @@ public: Node getSomeDomainElement(TypeNode tn); bool isInterval(Node n); Node getInterval( Node lb, Node ub ); + bool isInRange( Node v, Node i ); }; } diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index ed5dea679..2be9de91c 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -97,17 +97,7 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector exit( 11 ); } //check if it is in the range - bool inRange = true; - for( unsigned b=0; b<2; b++ ){ - if( !m->isStar( it->first[b] ) ){ - if( ( b==0 && it->first[b].getConst() > inst[index].getConst() ) || - ( b==1 && it->first[b].getConst() <= inst[index].getConst() ) ){ - inRange = false; - break; - } - } - } - if( inRange ){ + if( m->isInRange(inst[index], it->first ) ){ int gindex = it->second.getGeneralizationIndex(m, inst, index+1); if( minIndex==-1 || (gindex!=-1 && gindex nc; nc.push_back( cc.getOperator() ); for( unsigned j=0; j< cc.getNumChildren(); j++){ - nc.push_back(m->getStar(cc[j].getType())); + nc.push_back(m->getStarElement(cc[j].getType())); } cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc ); //re-add the entries @@ -331,19 +321,15 @@ QModelBuilder( c, qe ){ d_false = NodeManager::currentNM()->mkConst(false); } +bool FullModelChecker::optBuildAtFullModel() { + //need to build after full model has taken effect if we are constructing interval models + // this is because we need to have a constant in all integer equivalence classes + return options::fmfFmcInterval(); +} + void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc(); - if( fullModel ){ - //make function values - for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){ - m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" ); - } - TheoryEngineModelBuilder::processBuildModel( m, fullModel ); - //mark that the model has been set - fm->markModelSet(); - //debug the model - debugModel( fm ); - }else{ + if( fullModel==optBuildAtFullModel() ){ Trace("fmc") << "---Full Model Check reset() " << std::endl; fm->initialize( d_considerAxioms ); d_quant_models.clear(); @@ -464,6 +450,9 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ bool hasNonStar = false; for( unsigned i=0; igetUsedRepresentative( c[i]); + if( !ri.getType().isSort() && !ri.isConst() ){ + Trace("fmc-warn") << "Warning : model has non-constant argument in model " << ri << std::endl; + } children.push_back(ri); if( !options::fmfFmcInterval() || !ri.getType().isInteger() ){ if (fm->isModelBasisTerm(ri) ) { @@ -475,7 +464,10 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ entry_children.push_back(ri); } Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children ); - Node nv = fm->getUsedRepresentative( v); + Node nv = fm->getUsedRepresentative( v ); + if( !nv.getType().isSort() && !nv.isConst() ){ + Trace("fmc-warn") << "Warning : model has non-constant value in model " << nv << std::endl; + } 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; @@ -555,6 +547,17 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ Trace("fmc-model") << std::endl; } } + if( fullModel ){ + //make function values + for( std::map::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ){ + m->d_uf_models[ it->first ] = getFunctionValue( fm, it->first, "$x" ); + } + TheoryEngineModelBuilder::processBuildModel( m, fullModel ); + //mark that the model has been set + fm->markModelSet(); + //debug the model + debugModel( fm ); + } } void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) { @@ -722,6 +725,9 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No riter.d_bounds[b][i] = c[i][b]; } } + }else if( !fm->isStar(c[i]) ){ + riter.d_bounds[0][i] = c[i]; + riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 ); } } //initialize @@ -915,19 +921,23 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def if (eq[0]==eq[1]){ d.addEntry(fm, mkCond(cond), d_true); }else{ - int j = getVariableId(f, eq[0]); - int k = getVariableId(f, eq[1]); TypeNode tn = eq[0].getType(); - if( !fm->d_rep_set.hasType( tn ) ){ - getSomeDomainElement( fm, tn ); //to verify the type is initialized - } - for (unsigned i=0; id_rep_set.d_type_reps[tn].size(); i++) { - Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] ); - cond[j+1] = r; - cond[k+1] = r; - d.addEntry( fm, mkCond(cond), d_true); + if( tn.isSort() ){ + int j = getVariableId(f, eq[0]); + int k = getVariableId(f, eq[1]); + if( !fm->d_rep_set.hasType( tn ) ){ + getSomeDomainElement( fm, tn ); //to verify the type is initialized + } + for (unsigned i=0; id_rep_set.d_type_reps[tn].size(); i++) { + Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] ); + cond[j+1] = r; + cond[k+1] = r; + d.addEntry( fm, mkCond(cond), d_true); + } + d.addEntry( fm, mkCondDefault(fm, f), d_false); + }else{ + d.addEntry( fm, mkCondDefault(fm, f), Node::null()); } - d.addEntry( fm, mkCondDefault(fm, f), d_false); } } @@ -1058,14 +1068,22 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, } }else{ if( !v.isNull() ){ - if (curr.d_child.find(v)!=curr.d_child.end()) { - Trace("fmc-uf-process") << "follow value..." << std::endl; - doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]); - } - Node st = fm->getStarElement(v.getType()); - if (curr.d_child.find(st)!=curr.d_child.end()) { - Trace("fmc-uf-process") << "follow star..." << std::endl; - doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]); + if( options::fmfFmcInterval() && v.getType().isInteger() ){ + for (std::map::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) { + if( fm->isInRange( v, it->first ) ){ + doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second); + } + } + }else{ + if (curr.d_child.find(v)!=curr.d_child.end()) { + Trace("fmc-uf-process") << "follow value..." << std::endl; + doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]); + } + Node st = fm->getStarElement(v.getType()); + if (curr.d_child.find(st)!=curr.d_child.end()) { + Trace("fmc-uf-process") << "follow star..." << std::endl; + doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]); + } } } } @@ -1187,6 +1205,7 @@ Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) { } void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) { + Trace("fmc-debug") << "Make default vec, intervals = " << options::fmfFmcInterval() << std::endl; //get function symbol for f cond.push_back(d_quant_cond[f]); for (unsigned i=0; i & indices, int index, diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 2cb2198ef..8ebef640c 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -130,6 +130,8 @@ public: FullModelChecker( context::Context* c, QuantifiersEngine* qe ); ~FullModelChecker(){} + bool optBuildAtFullModel(); + int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; } void debugPrintCond(const char * tr, Node n, bool dispStar = false); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index b1851cfa4..073f7057b 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -50,6 +50,9 @@ bool QModelBuilder::optUseModel() { void QModelBuilder::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") ){ + Trace("quant-model-warn") << "Testing quantifier instantiations..." << std::endl; + int tests = 0; + int bad = 0; for( int i=0; igetNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); std::vector< Node > vars; @@ -57,20 +60,30 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){ vars.push_back( f[0][j] ); } RepSetIterator riter( d_qe, &(fm->d_rep_set) ); - riter.setQuantifier( f ); - while( !riter.isFinished() ){ - std::vector< Node > terms; - for( int i=0; i terms; + for( int i=0; igetInstantiation( f, vars, terms ); + Node val = fm->getValue( n ); + if( val!=fm->d_true ){ + Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl; + Trace("quant-model-warn") << " " << f << std::endl; + Trace("quant-model-warn") << " Evaluates to " << val << std::endl; + bad++; + } + riter.increment(); } - Node n = d_qe->getInstantiation( f, vars, terms ); - Node val = fm->getValue( n ); - if( val!=fm->d_true ){ - Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl; - Trace("quant-model-warn") << " " << f << std::endl; - Trace("quant-model-warn") << " Evaluates to " << val << std::endl; + Trace("quant-model-warn") << "Tested " << tests << " instantiations"; + if( bad>0 ){ + Trace("quant-model-warn") << ", " << bad << " failed" << std::endl; } - riter.increment(); + Trace("quant-model-warn") << "." << std::endl; + }else{ + Trace("quant-model-warn") << "Warning: Could not test quantifier " << f << std::endl; } } } diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 0d7c146ba..b96c58767 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -42,6 +42,8 @@ public: virtual bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { return false; } //whether to construct model virtual bool optUseModel(); + //whether to construct model at fullModel = true + virtual bool optBuildAtFullModel() { return false; } //consider axioms bool d_considerAxioms; /** number of lemmas generated while building model */ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index c0fe23b94..0678e230f 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -55,6 +55,7 @@ void ModelEngine::check( Theory::Effort e ){ clSet = double(clock())/double(CLOCKS_PER_SEC); } ++(d_statistics.d_inst_rounds); + bool buildAtFullModel = d_builder->optBuildAtFullModel(); //two effort levels: first try exhaustive instantiation without axioms, then with. int startEffort = ( !fm->isAxiomAsserted() || options::axiomInstMode()==AXIOM_INST_MODE_DEFAULT ) ? 1 : 0; for( int effort=startEffort; effort<2; effort++ ){ @@ -66,7 +67,7 @@ void ModelEngine::check( Theory::Effort e ){ Trace("model-engine-debug") << "Build model..." << std::endl; d_builder->d_considerAxioms = effort>=1; d_builder->d_addedLemmas = 0; - d_builder->buildModel( fm, false ); + d_builder->buildModel( fm, buildAtFullModel ); addedLemmas += (int)d_builder->d_addedLemmas; //if builder has lemmas, add and return if( addedLemmas==0 ){ @@ -103,7 +104,7 @@ void ModelEngine::check( Theory::Effort e ){ //CVC4 will answer SAT or unknown Trace("fmf-consistent") << std::endl; debugPrint("fmf-consistent"); - if( options::produceModels() ){ + if( options::produceModels() && !buildAtFullModel ){ // finish building the model d_builder->buildModel( fm, true ); } diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 1e6f04162..d44f2e770 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -95,10 +95,10 @@ option fmfModelBasedInst /--disable-fmf-mbqi bool :default true option fmfFullModelCheck --fmf-fmc bool :default false enable full model check for finite model finding -option fmfFullModelCheckSimple /--disable-fmf-fmc-simple bool :default true +option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true 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 fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true + disable covering simplification of fmc models option fmfFmcInterval --fmf-fmc-interval bool :default false construct interval models for fmc models -- 2.30.2