From 6d2def1c2e44974227fb06d3aa199722a4193a04 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 6 Nov 2013 12:31:31 -0600 Subject: [PATCH] Bug fixes for bounded integer quantification. Current best strategy is to turn off MBQI. Disable relevant triggers by default. --- src/theory/quantifiers/bounded_integers.cpp | 4 +- src/theory/quantifiers/first_order_model.cpp | 18 +- src/theory/quantifiers/full_model_check.cpp | 304 +++++++++++------- src/theory/quantifiers/full_model_check.h | 1 + .../quantifiers/instantiation_engine.cpp | 10 + src/theory/quantifiers/model_builder.cpp | 2 +- src/theory/quantifiers/model_engine.cpp | 2 +- src/theory/quantifiers/options | 2 +- src/theory/quantifiers_engine.cpp | 6 +- src/theory/rep_set.cpp | 11 +- src/theory/uf/theory_uf_model.cpp | 16 +- src/theory/uf/theory_uf_strong_solver.cpp | 46 ++- src/theory/uf/theory_uf_strong_solver.h | 4 +- 13 files changed, 267 insertions(+), 159 deletions(-) diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 30ff5242b..ab6b35e01 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -190,7 +190,6 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol, } }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) { Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl; - exit(0); } } @@ -232,7 +231,7 @@ void BoundedIntegers::registerQuantifier( Node f ) { if( f[0][i].getType().isInteger() ){ hasIntType = true; } - else if( f[0][i].getType().isSort() ){ + else if( f[0][i].getType().isSort() || f[0][i].getType().getCardinality().isFinite() ){ finiteTypes++; } } @@ -292,6 +291,7 @@ void BoundedIntegers::registerQuantifier( Node f ) { } }else{ Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f << std::endl; + //Message() << "Bound integers : Cannot infer bounds of " << f << std::endl; } } } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 63cac9c15..fa4961352 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -668,13 +668,19 @@ Node FirstOrderModelFmc::getInterval( Node lb, Node ub ){ } 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; + if( isStar( i ) ){ + return true; + }else if( isInterval( 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; + }else{ + return v==i; } - return true; } diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index bf10369e6..c22d903f9 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -92,10 +92,10 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector int minIndex = -1; if( options::fmfFmcInterval() && inst[index].getType().isInteger() ){ for( std::map::iterator it = d_child.begin(); it != d_child.end(); ++it ){ - if( !m->isInterval( it->first ) ){ - std::cout << "Not an interval during getGenIndex " << it->first << std::endl; - exit( 11 ); - } + //if( !m->isInterval( it->first ) ){ + // std::cout << "Not an interval during getGenIndex " << it->first << std::endl; + // exit( 11 ); + //} //check if it is in the range if( m->isInRange(inst[index], it->first ) ){ int gindex = it->second.getGeneralizationIndex(m, inst, index+1); @@ -392,13 +392,6 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ fm->d_models[op]->reset(); Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl; - for( size_t i=0; id_uf_terms[op].size(); i++ ){ - Node r = fm->getUsedRepresentative(fm->d_uf_terms[op][i]); - Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl; - } - Trace("fmc-model-debug") << std::endl; - - std::vector< Node > add_conds; std::vector< Node > add_values; bool needsDefault = true; @@ -407,8 +400,12 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ if( !n.getAttribute(NoMatchAttribute()) ){ 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 ) ); } } + Trace("fmc-model-debug") << std::endl; //possibly get default if( needsDefault ){ Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op); @@ -487,43 +484,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ if( options::fmfFmcInterval() ){ - Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl; - fm->d_models[op]->debugPrint("fmc-interval-model", op, this); - Trace("fmc-interval-model") << std::endl; - std::vector< int > indices; - for( int i=0; i<(int)fm->d_models[op]->d_cond.size(); i++ ){ - indices.push_back( i ); - } - std::map< int, std::map< int, Node > > changed_vals; - makeIntervalModel( fm, op, indices, 0, changed_vals ); - - std::vector< Node > conds; - std::vector< Node > values; - for( unsigned i=0; id_models[op]->d_cond.size(); i++ ){ - if( changed_vals.find(i)==changed_vals.end() ){ - conds.push_back( fm->d_models[op]->d_cond[i] ); - }else{ - std::vector< Node > children; - children.push_back( op ); - for( unsigned j=0; jd_models[op]->d_cond[i].getNumChildren(); j++ ){ - if( changed_vals[i].find(j)==changed_vals[i].end() ){ - children.push_back( fm->d_models[op]->d_cond[i][j] ); - }else{ - children.push_back( changed_vals[i][j] ); - } - } - Node nc = NodeManager::currentNM()->mkNode( APPLY_UF, children ); - conds.push_back( nc ); - Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to "; - debugPrintCond("fmc-interval-model", nc, true ); - Trace("fmc-interval-model") << std::endl; - } - values.push_back( fm->d_models[op]->d_value[i] ); - } - fm->d_models[op]->reset(); - for( unsigned i=0; id_models[op]->addEntry(fm, conds[i], values[i] ); - } + convertIntervalModel( fm, op ); } Trace("fmc-model-simplify") << "Before simplification : " << std::endl; @@ -535,6 +496,20 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ fm->d_models[op]->debugPrint("fmc-model", op, this); Trace("fmc-model") << std::endl; + + //for debugging + /* + for( size_t i=0; id_uf_terms[op].size(); i++ ){ + std::vector< Node > inst; + for( unsigned j=0; jd_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] ) ); + } + */ } } if( fullModel ){ @@ -588,7 +563,7 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { debugPrint(tr, n[1], dispStar ); }else{ TypeNode tn = n.getType(); - if( d_rep_ids.find(tn)!=d_rep_ids.end() ){ + if( tn.isSort() && d_rep_ids.find(tn)!=d_rep_ids.end() ){ if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) { Trace(tr) << d_rep_ids[tn][n]; }else{ @@ -622,79 +597,100 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, initializeType( fmfmc, f[0][i].getType() ); } - //model check the quantifier - doCheck(fmfmc, f, d_quant_models[f], f[1]); - Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl; - d_quant_models[f].debugPrint("fmc", Node::null(), this); - Trace("fmc") << std::endl; - - //consider all entries going to non-true - for (unsigned i=0; i inst; - for (unsigned j=0; jisStar(d_quant_models[f].d_cond[i][j])) { - hasStar = true; - inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType())); - }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){ - hasStar = true; - //if interval, find a sample point - if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][0]) ){ - if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][1]) ){ - inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j][1].getType())); + if( !options::fmfModelBasedInst() ){ + //just exhaustive instantiate + Node c = mkCondDefault( fmfmc, f ); + d_quant_models[f].addEntry( fmfmc, c, d_false ); + return exhaustiveInstantiate( fmfmc, f, c, -1); + }else{ + //model check the quantifier + doCheck(fmfmc, f, d_quant_models[f], f[1]); + Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl; + d_quant_models[f].debugPrint("fmc", Node::null(), this); + Trace("fmc") << std::endl; + + //consider all entries going to non-true + for (unsigned i=0; i inst; + for (unsigned j=0; jisStar(d_quant_models[f].d_cond[i][j])) { + hasStar = true; + inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType())); + }else if( fmfmc->isInterval(d_quant_models[f].d_cond[i][j])){ + hasStar = true; + //if interval, find a sample point + if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][0]) ){ + if( fmfmc->isStar(d_quant_models[f].d_cond[i][j][1]) ){ + inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j][1].getType())); + }else{ + Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1], + NodeManager::currentNM()->mkConst( Rational(1) ) ); + nn = Rewriter::rewrite( nn ); + inst.push_back( nn ); + } }else{ - Node nn = NodeManager::currentNM()->mkNode( MINUS, d_quant_models[f].d_cond[i][j][1], - NodeManager::currentNM()->mkConst( Rational(1) ) ); - nn = Rewriter::rewrite( nn ); - inst.push_back( nn ); + inst.push_back(d_quant_models[f].d_cond[i][j][0]); } }else{ - inst.push_back(d_quant_models[f].d_cond[i][j][0]); + inst.push_back(d_quant_models[f].d_cond[i][j]); } - }else{ - inst.push_back(d_quant_models[f].d_cond[i][j]); } - } - bool addInst = true; - if( hasStar ){ - //try obvious (specified by inst) - Node ev = d_quant_models[f].evaluate(fmfmc, inst); - if (ev==d_true) { - addInst = false; - } - }else{ - //for debugging - if (Trace.isOn("fmc-test-inst")) { + bool addInst = true; + if( hasStar ){ + //try obvious (specified by inst) Node ev = d_quant_models[f].evaluate(fmfmc, inst); - if( ev==d_true ){ - std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl; - exit(0); - }else{ - Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl; + if (ev==d_true) { + addInst = false; + } + }else{ + //for debugging + if (Trace.isOn("fmc-test-inst")) { + Node ev = d_quant_models[f].evaluate(fmfmc, inst); + if( ev==d_true ){ + std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl; + exit(0); + }else{ + Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl; + } } } - } - if( addInst ){ - InstMatch m; - for( unsigned j=0; jaddInstantiation( f, m ) ){ - Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; - d_addedLemmas++; + if( addInst ){ + if( options::fmfBoundInt() ){ + std::vector< Node > cond; + cond.push_back(d_quant_cond[f]); + cond.insert( cond.end(), inst.begin(), inst.end() ); + //need to do exhaustive instantiate algorithm to set things properly (should only add one instance) + Node c = mkCond( cond ); + int prevInst = d_addedLemmas; + exhaustiveInstantiate( fmfmc, f, c, -1 ); + if( d_addedLemmas==prevInst ){ + d_star_insts[f].push_back(i); + } + }else{ + //just add the instance + InstMatch m; + for( unsigned j=0; jaddInstantiation( f, m ) ){ + Trace("fmc-debug-inst") << "** Added instantiation." << std::endl; + d_addedLemmas++; + }else{ + Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl; + //this can happen if evaluation is unknown + //might try it next effort level + d_star_insts[f].push_back(i); + } + } }else{ - Trace("fmc-debug-inst") << "** Instantiation was duplicate." << std::endl; - //this can happen if evaluation is unknown + Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl; //might try it next effort level d_star_insts[f].push_back(i); } - }else{ - Trace("fmc-debug-inst") << "** Instantiation was already true." << std::endl; - //might try it next effort level - d_star_insts[f].push_back(i); } } } @@ -726,7 +722,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) { RepSetIterator riter( d_qe, &(fm->d_rep_set) ); - Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " "; + Trace("fmc-exh") << "----Exhaustive instantiate based on index " << c_index << " : " << c << " "; debugPrintCond("fmc-exh", c, true); Trace("fmc-exh")<< std::endl; Trace("fmc-exh-debug") << "Set interval domains..." << std::endl; @@ -761,10 +757,12 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No riter.d_domain[i].clear(); riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]); }else{ + Trace("fmc-exh") << "---- Does not have rep : " << c[i] << " for type " << tn << std::endl; return false; } } }else{ + Trace("fmc-exh") << "---- Does not have type : " << tn << std::endl; return false; } } @@ -774,27 +772,36 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No while( !riter.isFinished() ){ d_triedLemmas++; Trace("fmc-exh-debug") << "Inst : "; + std::vector< Node > ev_inst; std::vector< Node > inst; for( int i=0; igetUsedRepresentative( riter.getTerm( i ) ); + Node rr = riter.getTerm( i ); + Node r = rr; + if( r.getType().isSort() ){ + r = fm->getUsedRepresentative( r ); + }else{ + r = fm->getCurrentModelValue( r ); + } debugPrint("fmc-exh-debug", r); - Trace("fmc-exh-debug") << " "; - inst.push_back(r); + Trace("fmc-exh-debug") << " (term : " << rr << ")"; + ev_inst.push_back( r ); + inst.push_back( rr ); } - int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst); + int ev_index = d_quant_models[f].getGeneralizationIndex(fm, ev_inst); Trace("fmc-exh-debug") << ", index = " << ev_index << " / " << d_quant_models[f].d_value.size(); Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index]; if (ev!=d_true) { InstMatch m; - for( int i=0; iaddInstantiation( f, m ) ){ Trace("fmc-exh-debug") << " ...success."; addedLemmas++; + }else{ + Trace("fmc-exh-debug") << ", failed."; } }else{ Trace("fmc-exh-debug") << ", already true"; @@ -808,8 +815,10 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No } } d_addedLemmas += addedLemmas; + Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << std::endl; return true; }else{ + Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl; return false; } } @@ -1048,7 +1057,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, std::map< int, Node > & entries, int index, std::vector< Node > & cond, std::vector< Node > & val, EntryTrie & curr ) { - Trace("fmc-uf-process") << "compose " << index << std::endl; + Trace("fmc-uf-process") << "compose " << index << " / " << val.size() << std::endl; for( unsigned i=1; i & co } Node FullModelChecker::doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk ) { + Trace("fmc-debug2") << "Interval meet : " << i1 << " " << i2 << " " << mk << std::endl; if( fm->isStar( i1 ) ){ return i2; }else if( fm->isStar( i2 ) ){ return i1; - }else{ - if( !fm->isInterval( i1 ) || !fm->isInterval( i2 ) ){ - std::cout << "Not interval during meet! " << i1 << " " << i2 << std::endl; - exit( 0 ); + }else if( !fm->isInterval( i1 ) && fm->isInterval( i2 ) ){ + return doIntervalMeet( fm, i2, i1, mk ); + }else if( !fm->isInterval( i2 ) ){ + if( fm->isInterval( i1 ) ){ + if( fm->isInRange( i2, i1 ) ){ + return i2; + } + }else if( i1==i2 ){ + return i1; } + return Node::null(); + }else{ Node b[2]; for( unsigned j=0; j<2; j++ ){ Node b1 = i1[j]; @@ -1329,6 +1347,46 @@ bool FullModelChecker::useSimpleModels() { return options::fmfFmcSimple(); } +void FullModelChecker::convertIntervalModel( FirstOrderModelFmc * fm, Node op ){ + Trace("fmc-interval-model") << "Changing to interval model, Before : " << std::endl; + fm->d_models[op]->debugPrint("fmc-interval-model", op, this); + Trace("fmc-interval-model") << std::endl; + std::vector< int > indices; + for( int i=0; i<(int)fm->d_models[op]->d_cond.size(); i++ ){ + indices.push_back( i ); + } + std::map< int, std::map< int, Node > > changed_vals; + makeIntervalModel( fm, op, indices, 0, changed_vals ); + + std::vector< Node > conds; + std::vector< Node > values; + for( unsigned i=0; id_models[op]->d_cond.size(); i++ ){ + if( changed_vals.find(i)==changed_vals.end() ){ + conds.push_back( fm->d_models[op]->d_cond[i] ); + }else{ + std::vector< Node > children; + children.push_back( op ); + for( unsigned j=0; jd_models[op]->d_cond[i].getNumChildren(); j++ ){ + if( changed_vals[i].find(j)==changed_vals[i].end() ){ + children.push_back( fm->d_models[op]->d_cond[i][j] ); + }else{ + children.push_back( changed_vals[i][j] ); + } + } + Node nc = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + conds.push_back( nc ); + Trace("fmc-interval-model") << "Interval : Entry #" << i << " changed to "; + debugPrintCond("fmc-interval-model", nc, true ); + Trace("fmc-interval-model") << std::endl; + } + values.push_back( fm->d_models[op]->d_value[i] ); + } + fm->d_models[op]->reset(); + for( unsigned i=0; id_models[op]->addEntry(fm, conds[i], values[i] ); + } +} + void FullModelChecker::makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index, std::map< int, std::map< int, Node > >& changed_vals ) { if( index==(int)fm->d_models[op]->d_cond[0].getNumChildren() ){ diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 6bb375c34..abe05d3c7 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -100,6 +100,7 @@ protected: std::map< int, std::map< int, Node > >& changed_vals ); void makeIntervalModel( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index, std::map< int, std::map< int, Node > >& changed_vals ); + void convertIntervalModel( FirstOrderModelFmc * fm, Node op ); private: void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ); diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 628f8b14a..fa7b4e342 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -181,6 +181,16 @@ bool InstantiationEngine::needsCheck( Theory::Effort e ){ }else{ d_performCheck = true; } + static int ierCounter2 = 0; + if( e==Theory::EFFORT_LAST_CALL ){ + ierCounter2++; + //with bounded integers, skip every other last call, + // since matching loops may occur with infinite quantification + if( ierCounter2%2==0 && options::fmfBoundInt() ){ + d_performCheck = false; + } + } + return d_performCheck; } diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 5edf2de96..ea6f2d775 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -44,7 +44,7 @@ bool QModelBuilder::isQuantifierActive( Node f ) { bool QModelBuilder::optUseModel() { - return options::fmfModelBasedInst(); + return options::fmfModelBasedInst() || options::fmfBoundInt(); } void QModelBuilder::debugModel( FirstOrderModel* fm ){ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index b1a0c4ed4..5ff21bcff 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -34,7 +34,7 @@ using namespace CVC4::theory::inst; ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule( qe ){ - if( options::fmfFullModelCheck() ){ + if( options::fmfFullModelCheck() || options::fmfBoundInt() ){ d_builder = new fmcheck::FullModelChecker( c, qe ); }else if( options::fmfNewInstGen() ){ d_builder = new QModelBuilderInstGen( c, qe ); diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index fd114df04..1eb98e7b7 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -58,7 +58,7 @@ option foPropQuant --fo-prop-quant bool :default false option smartTriggers /--disable-smart-triggers bool :default true disable smart triggers # Whether to use relevent triggers -option relevantTriggers /--disable-relevant-triggers bool :default true +option relevantTriggers --relevant-triggers bool :default false prefer triggers that are more relevant based on SInE style analysis option relationalTriggers --relational-triggers bool :default false choose relational triggers such as x = f(y), x >= f(y) diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 07b0ebea3..54aa7f726 100755 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -50,7 +50,7 @@ d_lemmas_produced_c(u){ d_hasAddedLemma = false; //the model object - if( options::fmfFullModelCheck() ){ + if( options::fmfFullModelCheck() || options::fmfBoundInt() ){ d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); }else{ d_model = new quantifiers::FirstOrderModelIG( c, "FirstOrderModelIG" ); @@ -283,6 +283,10 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std d_temp_inst_debug[f]++; d_total_inst_count_debug++; Trace("inst") << "*** Instantiate " << f << " with " << std::endl; + for( int i=0; i<(int)terms.size(); i++ ){ + Trace("inst") << " " << terms[i]; + Trace("inst") << std::endl; + } //uint64_t maxInstLevel = 0; if( options::cbqi() ){ for( int i=0; i<(int)terms.size(); i++ ){ diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 800e007f7..169688243 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -252,6 +252,7 @@ bool RepSetIterator::resetIndex( int i, bool initial ) { if( d_enum_type[ii]==ENUM_RANGE ){ if( initial || ( d_qe->getBoundedIntegers() && !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ) ){ Trace("bound-int-rsi") << "Getting range of " << d_owner[0][ii] << std::endl; + Node actual_l; Node l, u; if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){ d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u ); @@ -260,6 +261,10 @@ bool RepSetIterator::resetIndex( int i, bool initial ) { if( d_bounds[b].find(ii)!=d_bounds[b].end() ){ Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][ii] << std::endl; if( b==0 && (l.isNull() || d_bounds[b][ii].getConst() > l.getConst()) ){ + if( !l.isNull() ){ + //bound was limited externally, record that the value lower bound is not equal to the term lower bound + actual_l = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii], l ); + } l = d_bounds[b][ii]; }else if( b==1 && (u.isNull() || d_bounds[b][ii].getConst() <= u.getConst()) ){ u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii], @@ -284,6 +289,10 @@ bool RepSetIterator::resetIndex( int i, bool initial ) { d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][ii], this, tl, tu ); } d_lower_bounds[ii] = tl; + if( !actual_l.isNull() ){ + //if bound was limited externally, must consider the offset + d_lower_bounds[ii] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) ); + } if( ra==NodeManager::currentNM()->mkConst(true) ){ long rr = range.getConst().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; @@ -355,7 +364,7 @@ Node RepSetIterator::getTerm( int i ){ Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() ); return d_rep_set->d_type_reps[tn][d_domain[index][d_index[index]]]; }else{ - Trace("rsi-debug") << index << " " << d_lower_bounds[index] << " " << d_index[index] << std::endl; + Trace("rsi-debug") << "Get, with offset : " << index << " " << d_lower_bounds[index] << " " << d_index[index] << std::endl; Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[index], NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) ); t = Rewriter::rewrite( t ); diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index c0d114052..284212ba9 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -345,14 +345,14 @@ void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground d_set_values[ isReq ? 1 : 0 ][ ground ? 1 : 0 ][n] = v; if( optUsePartialDefaults() ){ if( !ground ){ - int defSize = (int)d_defaults.size(); - for( int i=0; igetTheory()->d_equalityEngine.getRepresentative( a ); b = d_thss->getTheory()->d_equalityEngine.getRepresentative( b ); - if( !d_thss->getTheory()->d_equalityEngine.areDisequal( a, b, true ) ){ + int ai = d_regions_map[a]; + int bi = d_regions_map[b]; + if( !d_regions[ai]->isDisequal( a, b, ai==bi ) ){ Debug("uf-ss") << "Assert disequal " << a << " != " << b << "..." << std::endl; //if( reason.getKind()!=NOT || ( reason[0].getKind()!=EQUAL && reason[0].getKind()!=IFF ) || // a!=reason[0][0] || b!=reason[0][1] ){ @@ -559,8 +561,6 @@ void StrongSolverTheoryUF::SortModel::assertDisequal( Node a, Node b, Node reaso //now, add disequalities to regions Assert( d_regions_map.find( a )!=d_regions_map.end() ); Assert( d_regions_map.find( b )!=d_regions_map.end() ); - int ai = d_regions_map[a]; - int bi = d_regions_map[b]; Debug("uf-ss") << " regions: " << ai << " " << bi << std::endl; if( ai==bi ){ //internal disequality @@ -663,11 +663,15 @@ void StrongSolverTheoryUF::SortModel::check( Theory::Effort level, OutputChannel return; } }else{ - if( addSplit( d_regions[i], out ) ){ + int sp = addSplit( d_regions[i], out ); + if( sp==1 ){ addedLemma = true; #ifdef ONE_SPLIT_REGION break; #endif + }else if( sp==-1 ){ + check( level, out ); + return; } } } @@ -771,6 +775,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* } #endif }else{ + Trace("uf-ss-debug") << "Minimize the UF model..." << std::endl; //internal minimize, ensure that model forms a clique: // if two equivalence classes are neither equal nor disequal, add a split int validRegionIndex = -1; @@ -778,7 +783,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* if( d_regions[i]->d_valid ){ if( validRegionIndex!=-1 ){ combineRegions( validRegionIndex, i ); - if( addSplit( d_regions[validRegionIndex], out ) ){ + if( addSplit( d_regions[validRegionIndex], out )!=0 ){ return false; } }else{ @@ -786,7 +791,7 @@ bool StrongSolverTheoryUF::SortModel::minimize( OutputChannel* out, TheoryModel* } } } - if( addSplit( d_regions[validRegionIndex], out ) ){ + if( addSplit( d_regions[validRegionIndex], out )!=0 ){ return false; } } @@ -1074,7 +1079,7 @@ void StrongSolverTheoryUF::SortModel::allocateCardinality( OutputChannel* out ){ } } -bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ +int StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ Node s; if( r->hasSplits() ){ if( !options::ufssSmartSplits() ){ @@ -1120,11 +1125,26 @@ bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ if (!s.isNull() ){ //add lemma to output channel Assert( s.getKind()==EQUAL ); - s = Rewriter::rewrite( s ); Trace("uf-ss-lemma") << "*** Split on " << s << std::endl; + Node ss = Rewriter::rewrite( s ); + if( ss.getKind()!=EQUAL ){ + Node b_t = NodeManager::currentNM()->mkConst( true ); + Node b_f = NodeManager::currentNM()->mkConst( false ); + if( ss==b_f ){ + Trace("uf-ss-lemma") << "....Assert disequal directly : " << s[0] << " " << s[1] << std::endl; + assertDisequal( s[0], s[1], b_t ); + return -1; + }else{ + Trace("uf-ss-warn") << "Split on unknown literal : " << ss << std::endl; + } + if( ss==b_t ){ + Message() << "Bad split " << s << std::endl; + exit( 16 ); + } + } if( options::sortInference()) { for( int i=0; i<2; i++ ){ - int si = d_thss->getSortInference()->getSortId( s[i] ); + int si = d_thss->getSortInference()->getSortId( ss[i] ); Trace("uf-ss-split-si") << si << " "; } Trace("uf-ss-split-si") << std::endl; @@ -1134,13 +1154,13 @@ bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){ //Trace("uf-ss-lemma") << s[0].getType() << " " << s[1].getType() << std::endl; //Notice() << "*** Split on " << s << std::endl; //split on the equality s - out->split( s ); + out->split( ss ); //tell the sat solver to explore the equals branch first - out->requirePhase( s, true ); + out->requirePhase( ss, true ); ++( d_thss->d_statistics.d_split_lemmas ); - return true; + return 1; }else{ - return false; + return 0; } } diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h index 8e568444b..9111ec6a7 100644 --- a/src/theory/uf/theory_uf_strong_solver.h +++ b/src/theory/uf/theory_uf_strong_solver.h @@ -200,8 +200,8 @@ public: private: /** allocate cardinality */ void allocateCardinality( OutputChannel* out ); - /** add split */ - bool addSplit( Region* r, OutputChannel* out ); + /** add split 0 = no split, -1 = entailed disequality added, 1 = split added */ + int addSplit( Region* r, OutputChannel* out ); /** add clique lemma */ void addCliqueLemma( std::vector< Node >& clique, OutputChannel* out ); /** add totality axiom */ -- 2.30.2