diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp | 37 | ||||
-rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 84 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.cpp | 395 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/full_model_check.h | 11 | ||||
-rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 37 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 5 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 28 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.h | 6 |
11 files changed, 73 insertions, 549 deletions
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 3f2dc7cc6..cfcfcc5a5 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -571,43 +571,6 @@ void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) { } } -/* TODO? -bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) { - std::map< Node, bool >::iterator itq = d_quant.find( f ); - if( itq==d_quant.end() ){ - //generate triggers - Node bd = d_quantEngine->getTermUtil()->getInstConstantBody( f ); - std::vector< Node > vars; - std::vector< Node > patTerms; - bool ret = Trigger::isLocalTheoryExt( bd, vars, patTerms ); - if( ret ){ - d_quant[f] = ret; - //add all variables to trigger that don't already occur - for( unsigned i=0; i<f[0].getNumChildren(); i++ ){ - Node x = d_quantEngine->getTermUtil()->getInstantiationConstant( f, i ); - if( std::find( vars.begin(), vars.end(), x )==vars.end() ){ - patTerms.push_back( x ); - } - } - Trace("local-t-ext") << "Local theory extensions trigger for " << f << " : " << std::endl; - for( unsigned i=0; i<patTerms.size(); i++ ){ - Trace("local-t-ext") << " " << patTerms[i] << std::endl; - } - Trace("local-t-ext") << std::endl; - Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, true, Trigger::TR_GET_OLD ); - d_lte_trigger[f] = tr; - }else{ - Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl; - Trace("local-t-ext-warn") << "WARNING: not local theory extensions : " << f << std::endl; - } - d_quant[f] = ret; - return ret; - }else{ - return itq->second; - } -} -*/ - } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index 1d582f597..ac07e13fb 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -67,7 +67,9 @@ bool EqualityQueryQuantifiersEngine::processInferences( Theory::Effort e ) { } Trace("term-db-lemma") << " add split on : " << eq << std::endl; } - d_qe->addSplit( eq ); + eq = Rewriter::rewrite(eq); + Node split = NodeManager::currentNM()->mkNode(OR, eq, eq.negate()); + d_qe->addLemma(split); return false; }else{ ee->assertEquality( eq, true, eq_exp ); diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index e844b4eca..9d83c589f 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -387,16 +387,6 @@ Node FirstOrderModel::getModelBasis(Node q, Node n) return gn; } -Node FirstOrderModel::getModelBasisBody(Node q) -{ - if (d_model_basis_body.find(q) == d_model_basis_body.end()) - { - Node n = d_qe->getTermUtil()->getInstConstantBody(q); - d_model_basis_body[q] = getModelBasis(q, n); - } - return d_model_basis_body[q]; -} - void FirstOrderModel::computeModelBasisArgAttribute(Node n) { if (!n.hasAttribute(ModelBasisArgAttribute())) @@ -471,8 +461,6 @@ void FirstOrderModelIG::resetEvaluate(){ d_eval_uf_use_default.clear(); d_eval_uf_model.clear(); d_eval_term_index_order.clear(); - d_eval_failed.clear(); - d_eval_failed_lits.clear(); d_eval_formulas = 0; d_eval_uf_terms = 0; d_eval_lits = 0; @@ -563,12 +551,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ return 0; }else{ ++d_eval_lits; - ////if we know we will fail again, immediately return - //if( d_eval_failed.find( n )!=d_eval_failed.end() ){ - // if( d_eval_failed[n] ){ - // return -1; - // } - //} //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl; int retVal = 0; depIndex = ri->getNumTerms()-1; @@ -594,11 +576,6 @@ int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ ++d_eval_lits_unknown; Trace("fmf-eval-amb") << "Neither true nor false : " << n << std::endl; Trace("fmf-eval-amb") << " value : " << val << std::endl; - //std::cout << "Neither true nor false : " << n << std::endl; - //std::cout << " Value : " << val << std::endl; - //for( int i=0; i<(int)n.getNumChildren(); i++ ){ - // std::cout << " " << i << " : " << n[i].getType() << std::endl; - //} } return retVal; } @@ -723,13 +700,6 @@ Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector< } } -void FirstOrderModelIG::clearEvalFailed( int index ){ - for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){ - d_eval_failed[ d_eval_failed_lits[index][i] ] = false; - } - d_eval_failed_lits[index].clear(); -} - void FirstOrderModelIG::makeEvalUfModel( Node n ){ if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){ makeEvalUfIndexOrder( n ); @@ -856,14 +826,6 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a void FirstOrderModelFmc::processInitialize( bool ispre ) { if( ispre ){ - if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && 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(); } @@ -895,14 +857,6 @@ Node FirstOrderModelFmc::getStar(TypeNode tn) { return it->second; } -Node FirstOrderModelFmc::getStarElement(TypeNode tn) { - Node st = getStar(tn); - if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && tn.isInteger() ){ - st = getInterval( st, st ); - } - return st; -} - Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { Trace("fmc-model") << "Get function value for " << op << std::endl; TypeNode type = op.getType(); @@ -947,14 +901,8 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { std::vector< Node > children; for( unsigned j=0; j<cond.getNumChildren(); j++) { TypeNode tn = vars[j].getType(); - if (isInterval(cond[j])){ - if( !isStar(cond[j][0]) ){ - children.push_back( NodeManager::currentNM()->mkNode( GEQ, vars[j], cond[j][0] ) ); - } - if( !isStar(cond[j][1]) ){ - children.push_back( NodeManager::currentNM()->mkNode( LT, vars[j], cond[j][1] ) ); - } - }else if( !isStar(cond[j]) ){ + if (!isStar(cond[j])) + { Node c = getRepresentative( cond[j] ); c = getRepresentative( c ); children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) ); @@ -972,34 +920,6 @@ Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) { 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 ); -} - -bool FirstOrderModelFmc::isInRange( Node v, Node i ) { - 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<Rational>() > v.getConst<Rational>() ) || - ( b==1 && i[b].getConst<Rational>() <= v.getConst<Rational>() ) ){ - return false; - } - } - } - return true; - }else{ - return v==i; - } -} - - - FirstOrderModelAbs::FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name) : FirstOrderModel(qe, c, name) { diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index cf6ee003d..748bf12da 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -137,8 +137,6 @@ class FirstOrderModel : public TheoryModel Node getModelBasisOpTerm(Node op); /** get model basis */ Node getModelBasis(Node q, Node n); - /** get model basis body */ - Node getModelBasisBody(Node q); /** get model basis arg */ unsigned getModelBasisArg(Node n); /** get some domain element */ @@ -234,10 +232,6 @@ public: private: //default evaluate term function Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ); - //temporary storing which literals have failed - void clearEvalFailed( int index ); - std::map< Node, bool > d_eval_failed; - std::map< int, std::vector< Node > > d_eval_failed_lits; };/* class FirstOrderModelIG */ @@ -253,7 +247,6 @@ class FirstOrderModelFmc : public FirstOrderModel /** models for UF */ std::map<Node, Def * > d_models; std::map<TypeNode, Node > d_type_star; - Node intervalOp; /** get current model value */ void processInitializeModelForTerm(Node n) override; @@ -267,10 +260,6 @@ class FirstOrderModelFmc : public FirstOrderModel bool isStar(Node n); Node getStar(TypeNode tn); - Node getStarElement(TypeNode tn); - bool isInterval(Node n); - Node getInterval( Node lb, Node ub ); - bool isInRange( Node v, Node i ); };/* class FirstOrderModelFmc */ }/* CVC4::theory::quantifiers::fmcheck namespace */ diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index b4e9aa1e9..481048105 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -40,16 +40,6 @@ struct ModelBasisArgSort } }; - -struct ConstRationalSort -{ - std::vector< Node > d_terms; - bool operator() (int i, int j) { - return (d_terms[i].getConst<Rational>() < d_terms[j].getConst<Rational>() ); - } -}; - - bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) { if (index==(int)c.getNumChildren()) { return d_data!=-1; @@ -100,27 +90,18 @@ int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> return d_data; }else{ int minIndex = -1; - if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && inst[index].getType().isInteger() ){ - for( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){ - //check if it is in the range - if( m->isInRange(inst[index], it->first ) ){ - int gindex = it->second.getGeneralizationIndex(m, inst, index+1); - if( minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){ - minIndex = gindex; - } - } - } - }else{ - Node st = m->getStar(inst[index].getType()); - if(d_child.find(st)!=d_child.end()) { - minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1); - } - Node cc = inst[index]; - if( cc!=st && d_child.find( cc )!=d_child.end() ){ - int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1); - if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){ - minIndex = gindex; - } + Node st = m->getStar(inst[index].getType()); + if (d_child.find(st) != d_child.end()) + { + minIndex = d_child[st].getGeneralizationIndex(m, inst, index + 1); + } + Node cc = inst[index]; + if (cc != st && d_child.find(cc) != d_child.end()) + { + int gindex = d_child[cc].getGeneralizationIndex(m, inst, index + 1); + if (minIndex == -1 || (gindex != -1 && gindex < minIndex)) + { + minIndex = gindex; } } return minIndex; @@ -167,35 +148,6 @@ void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & c } } -void EntryTrie::collectIndices(Node c, int index, std::vector< int >& indices ) { - if (index==(int)c.getNumChildren()) { - if( d_data!=-1 ){ - indices.push_back( d_data ); - } - }else{ - for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){ - it->second.collectIndices(c, index+1, indices ); - } - } -} - -bool EntryTrie::isComplete(FirstOrderModelFmc * m, Node c, int index) { - if( d_complete==-1 ){ - d_complete = 1; - if (index<(int)c.getNumChildren()) { - Node st = m->getStar(c[index].getType()); - if(d_child.find(st)!=d_child.end()) { - if (!d_child[st].isComplete(m, c, index+1)) { - d_complete = 0; - } - }else{ - d_complete = 0; - } - } - } - return d_complete==1; -} - bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) { if (d_et.hasGeneralization(m, c)) { Trace("fmc-debug") << "Already has generalization, skip." << std::endl; @@ -269,7 +221,8 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) { bool last_all_stars = true; Node cc = d_cond[d_cond.size()-1]; for( unsigned i=0; i<cc.getNumChildren(); i++ ){ - if( !m->isInterval(cc[i]) && !m->isStar(cc[i]) ){ + if (!m->isStar(cc[i])) + { last_all_stars = false; break; } @@ -291,7 +244,7 @@ void Def::simplify(FullModelChecker * mc, FirstOrderModelFmc * m) { std::vector< Node > nc; nc.push_back( cc.getOperator() ); for( unsigned j=0; j< cc.getNumChildren(); j++){ - nc.push_back(m->getStarElement(cc[j].getType())); + nc.push_back(m->getStar(cc[j].getType())); } cond[cond.size()-1] = NodeManager::currentNM()->mkNode( APPLY_UF, nc ); //re-add the entries @@ -476,13 +429,14 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ Node ri = fm->getRepresentative( 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 (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; @@ -525,11 +479,6 @@ bool FullModelChecker::processBuildModel(TheoryModel* m){ fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]); } - - 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; @@ -612,11 +561,8 @@ void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) { else if(fm->isStar(n) && dispStar) { Trace(tr) << "*"; } - else if(fm->isInterval(n)) { - debugPrint(tr, n[0], dispStar ); - Trace(tr) << "..."; - debugPrint(tr, n[1], dispStar ); - }else{ + else + { TypeNode tn = n.getType(); if( tn.isSort() && d_rep_ids.find(tn)!=d_rep_ids.end() ){ if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) { @@ -671,21 +617,6 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i if (fmfmc->isStar(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{ - inst.push_back(d_quant_models[f].d_cond[i][j][0]); - } }else{ inst.push_back(d_quant_models[f].d_cond[i][j]); } @@ -816,15 +747,7 @@ class RepBoundFmcEntry : public QRepBoundExt virtual RepSetIterator::RsiEnumType setBound( Node owner, unsigned i, std::vector<Node>& elements) override { - if (d_fm->isInterval(d_entry[i])) - { - // explicitly add the interval? - } - else if (d_fm->isStar(d_entry[i])) - { - // must add the full range - } - else + if (!d_fm->isStar(d_entry[i])) { // only need to consider the single point elements.push_back(d_entry[i]); @@ -1144,7 +1067,8 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){ int j = fm->getVariableId(f, v); Trace("fmc-uf-process") << v << " is variable #" << j << std::endl; - if (!fm->isStar(cond[j+1]) && !fm->isInterval(cond[j+1])) { + if (!fm->isStar(cond[j + 1])) + { v = cond[j+1]; }else{ bind_var = true; @@ -1153,41 +1077,30 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, if (bind_var) { Trace("fmc-uf-process") << "bind variable..." << std::endl; int j = fm->getVariableId(f, v); - if( fm->isStar(cond[j+1]) ){ - for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) { - cond[j+1] = it->first; - doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second); - } - cond[j+1] = fm->getStar(v.getType()); - }else{ - Node orig = cond[j+1]; - for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) { - Node nw = doIntervalMeet( fm, it->first, orig ); - if( !nw.isNull() ){ - cond[j+1] = nw; - doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second); - } - } - cond[j+1] = orig; + Assert(fm->isStar(cond[j + 1])); + for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); + it != curr.d_child.end(); + ++it) + { + cond[j + 1] = it->first; + doUninterpretedCompose2( + fm, f, entries, index + 1, cond, val, it->second); } + cond[j + 1] = fm->getStar(v.getType()); }else{ if( !v.isNull() ){ - if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && v.getType().isInteger() ){ - for (std::map<Node, EntryTrie>::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]); - } + 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->getStar(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]); } } } @@ -1240,15 +1153,9 @@ int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & c Trace("fmc-debug3") << "isCompat " << c << std::endl; Assert(cond.size()==c.getNumChildren()+1); for (unsigned i=1; i<cond.size(); i++) { - if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){ - Node iv = doIntervalMeet( fm, cond[i], c[i-1], false ); - if( iv.isNull() ){ - return 0; - } - }else{ - if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) { - return 0; - } + if (cond[i] != c[i - 1] && !fm->isStar(cond[i]) && !fm->isStar(c[i - 1])) + { + return 0; } } return 1; @@ -1259,63 +1166,17 @@ bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & co Assert(cond.size()==c.getNumChildren()+1); for (unsigned i=1; i<cond.size(); i++) { if( cond[i]!=c[i-1] ) { - if( options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL && cond[i].getType().isInteger() ){ - Node iv = doIntervalMeet( fm, cond[i], c[i-1] ); - if( !iv.isNull() ){ - cond[i] = iv; - }else{ - return false; - } - }else{ - if( fm->isStar(cond[i]) ){ - cond[i] = c[i-1]; - }else if( !fm->isStar(c[i-1]) ){ - return false; - } - } - } - } - return true; -} - -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 ) ){ - return doIntervalMeet( fm, i2, i1, mk ); - }else if( !fm->isInterval( i2 ) ){ - if( fm->isInterval( i1 ) ){ - if( fm->isInRange( i2, i1 ) ){ - return i2; + if (fm->isStar(cond[i])) + { + cond[i] = c[i - 1]; } - }else if( i1==i2 ){ - return i1; - } - return Node::null(); - }else{ - Node b[2]; - for( unsigned j=0; j<2; j++ ){ - Node b1 = i1[j]; - Node b2 = i2[j]; - if( fm->isStar( b1 ) ){ - b[j] = b2; - }else if( fm->isStar( b2 ) ){ - b[j] = b1; - }else if( b1.getConst<Rational>() < b2.getConst<Rational>() ){ - b[j] = j==0 ? b2 : b1; - }else{ - b[j] = j==0 ? b1 : b2; + else if (!fm->isStar(c[i - 1])) + { + return false; } } - if( fm->isStar( b[0] ) || fm->isStar( b[1] ) || b[0].getConst<Rational>() < b[1].getConst<Rational>() ){ - return mk ? fm->getInterval( b[0], b[1] ) : i1; - }else{ - return Node::null(); - } } + return true; } Node FullModelChecker::mkCond( std::vector< Node > & cond ) { @@ -1329,11 +1190,11 @@ 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::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL) << std::endl; + Trace("fmc-debug") << "Make default vec" << std::endl; //get function symbol for f cond.push_back(d_quant_cond[f]); for (unsigned i=0; i<f[0].getNumChildren(); i++) { - Node ts = fm->getStarElement( f[0][i].getType() ); + Node ts = fm->getStar(f[0][i].getType()); Assert( ts.getType()==f[0][i].getType() ); cond.push_back(ts); } @@ -1346,21 +1207,6 @@ void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) { } } -Node FullModelChecker::mkArrayCond( Node a ) { - if( d_array_term_cond.find(a)==d_array_term_cond.end() ){ - if( d_array_cond.find(a.getType())==d_array_cond.end() ){ - TypeNode typ = NodeManager::currentNM()->mkFunctionType( a.getType(), NodeManager::currentNM()->booleanType() ); - Node op = NodeManager::currentNM()->mkSkolem( "fmc", typ, "op created for full-model checking" ); - d_array_cond[a.getType()] = op; - } - std::vector< Node > cond; - cond.push_back(d_array_cond[a.getType()]); - cond.push_back(a); - d_array_term_cond[a] = NodeManager::currentNM()->mkNode(APPLY_UF, cond ); - } - return d_array_term_cond[a]; -} - Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) { if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){ if (!vals[0].isNull() && !vals[1].isNull()) { @@ -1423,122 +1269,3 @@ Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const 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; i<fm->d_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; j<fm->d_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; i<conds.size(); i++ ){ - fm->d_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() ){ - makeIntervalModel2( fm, op, indices, 0, changed_vals ); - }else{ - TypeNode tn = fm->d_models[op]->d_cond[0][index].getType(); - if( tn.isInteger() ){ - makeIntervalModel(fm,op,indices,index+1, changed_vals ); - }else{ - std::map< Node, std::vector< int > > new_indices; - for( unsigned i=0; i<indices.size(); i++ ){ - Node v = fm->d_models[op]->d_cond[indices[i]][index]; - new_indices[v].push_back( indices[i] ); - } - - for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){ - makeIntervalModel( fm, op, it->second, index+1, changed_vals ); - } - } - } -} - -void FullModelChecker::makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index, - std::map< int, std::map< int, Node > >& changed_vals ) { - Debug("fmc-interval-model-debug") << "Process " << index << " with indicies : "; - for( unsigned i=0; i<indices.size(); i++ ){ - Debug("fmc-interval-model-debug") << indices[i] << " "; - } - Debug("fmc-interval-model-debug") << std::endl; - - if( index<(int)fm->d_models[op]->d_cond[0].getNumChildren() ){ - TypeNode tn = fm->d_models[op]->d_cond[0][index].getType(); - if( tn.isInteger() ){ - std::map< Node, std::vector< int > > new_indices; - for( unsigned i=0; i<indices.size(); i++ ){ - Node v = fm->d_models[op]->d_cond[indices[i]][index]; - new_indices[v].push_back( indices[i] ); - if( !v.isConst() ){ - Trace("fmc-warn") << "WARNING: for interval, model has non-constant : " << v << std::endl; - Trace("fmc-warn") << "From condition : " << fm->d_models[op]->d_cond[indices[i]] << std::endl; - } - } - - std::vector< Node > values; - for( std::map< Node, std::vector< int > >::iterator it = new_indices.begin(); it != new_indices.end(); ++it ){ - makeIntervalModel2( fm, op, it->second, index+1, changed_vals ); - values.push_back( it->first ); - } - - if( tn.isInteger() ){ - //sort values by size - ConstRationalSort crs; - std::vector< int > sindices; - for( unsigned i=0; i<values.size(); i++ ){ - sindices.push_back( (int)i ); - crs.d_terms.push_back( values[i] ); - } - std::sort( sindices.begin(), sindices.end(), crs ); - - Node ub = fm->getStar( tn ); - for( int i=(int)(sindices.size()-1); i>=0; i-- ){ - Node lb = fm->getStar( tn ); - if( i>0 ){ - lb = values[sindices[i]]; - } - Node interval = fm->getInterval( lb, ub ); - for( unsigned j=0; j<new_indices[values[sindices[i]]].size(); j++ ){ - Debug("fmc-interval-model-debug") << "Change " << new_indices[values[sindices[i]]][j] << ", " << index << " to " << interval << std::endl; - changed_vals[new_indices[values[sindices[i]]][j]][index] = interval; - } - ub = lb; - } - } - }else{ - makeIntervalModel2( fm, op, indices, index+1, changed_vals ); - } - } -} diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index c28910700..f0f9a1798 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -42,9 +42,6 @@ public: bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 ); int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 ); void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true ); - - void collectIndices(Node c, int index, std::vector< int >& indices ); - bool isComplete(FirstOrderModelFmc * m, Node c, int index); };/* class EntryTrie */ @@ -114,12 +111,6 @@ protected: //--------------------end for preinitialization Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); bool exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index); -protected: - void makeIntervalModel2( FirstOrderModelFmc * fm, Node op, std::vector< int > & indices, int index, - 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 ); @@ -140,13 +131,11 @@ private: std::vector< Def > & dc, int index, std::vector< Node > & cond, std::vector<Node> & val ); int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ); - Node doIntervalMeet( FirstOrderModelFmc * fm, Node i1, Node i2, bool mk = true ); bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ); Node mkCond( std::vector< Node > & cond ); Node mkCondDefault( FirstOrderModelFmc * fm, Node f ); void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ); void mkCondVec( Node n, std::vector< Node > & cond ); - Node mkArrayCond( Node a ); Node evaluateInterpreted( Node n, std::vector< Node > & vals ); Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ); public: diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index b3d9af953..f05246ddb 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -218,7 +218,9 @@ int ModelEngine::checkModel(){ Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; // FMC uses two sub-effort levels - int e_max = options::mbqiMode()==MBQI_FMC || options::mbqiMode()==MBQI_FMC_INTERVAL ? 2 : ( options::mbqiMode()==MBQI_TRUST ? 0 : 1 ); + int e_max = options::mbqiMode() == MBQI_FMC + ? 2 + : (options::mbqiMode() == MBQI_TRUST ? 0 : 1); for( int e=0; e<e_max; e++) { d_incomplete_quants.clear(); for( unsigned i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 8cf8a7042..842671a5e 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -57,22 +57,6 @@ TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, Output TheoryQuantifiers::~TheoryQuantifiers() { } -void TheoryQuantifiers::setMasterEqualityEngine(eq::EqualityEngine* eq) { - -} - -void TheoryQuantifiers::addSharedTerm(TNode t) { - Debug("quantifiers-other") << "TheoryQuantifiers::addSharedTerm(): " - << t << endl; -} - - -void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) { - Debug("quantifiers-other") << "TheoryQuantifiers::notifyEq(): " - << lhs << " = " << rhs << endl; - -} - void TheoryQuantifiers::finishInit() { // quantifiers are not evaluated in getModelValue @@ -119,27 +103,6 @@ void TheoryQuantifiers::ppNotifyAssertions( } } -Node TheoryQuantifiers::getValue(TNode n) { - //NodeManager* nodeManager = NodeManager::currentNM(); - switch(n.getKind()) { - case FORALL: - case EXISTS: - bool value; - if( d_valuation.hasSatValue( n, value ) ){ - return NodeManager::currentNM()->mkConst(value); - }else{ - return NodeManager::currentNM()->mkConst(false); //FIX_THIS? - } - break; - default: - Unhandled(n.getKind()); - } -} - -void TheoryQuantifiers::computeCareGraph() { - //do nothing -} - bool TheoryQuantifiers::collectModelInfo(TheoryModel* m) { for(assertions_iterator i = facts_begin(); i != facts_end(); ++i) { diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 2eb3f70be..074e288c6 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -39,9 +39,6 @@ class TheoryQuantifiers : public Theory { const LogicInfo& logicInfo); ~TheoryQuantifiers(); - void setMasterEqualityEngine(eq::EqualityEngine* eq) override; - void addSharedTerm(TNode t) override; - void notifyEq(TNode lhs, TNode rhs); /** finish initialization */ void finishInit() override; void preRegisterTerm(TNode n) override; @@ -49,7 +46,6 @@ class TheoryQuantifiers : public Theory { void ppNotifyAssertions(const std::vector<Node>& assertions) override; void check(Effort e) override; Node getNextDecisionRequest(unsigned& priority) override; - Node getValue(TNode n); bool collectModelInfo(TheoryModel* m) override; void shutdown() override {} std::string identify() const override @@ -64,7 +60,6 @@ class TheoryQuantifiers : public Theory { private: void assertUniversal( Node n ); void assertExistential( Node n ); - void computeCareGraph() override; /** number of instantiations */ int d_numInstantiations; int d_baseDecLevel; diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 3d966726b..73d2de401 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -247,8 +247,10 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, // if we require specialized ways of building the model if( needsBuilder ){ Trace("quant-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBound() << std::endl; - if( options::mbqiMode()==quantifiers::MBQI_FMC || options::mbqiMode()==quantifiers::MBQI_FMC_INTERVAL || - options::mbqiMode()==quantifiers::MBQI_TRUST || options::fmfBound() ){ + if (options::mbqiMode() == quantifiers::MBQI_FMC + || options::mbqiMode() == quantifiers::MBQI_TRUST + || options::fmfBound()) + { Trace("quant-engine-debug") << "...make fmc builder." << std::endl; d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" ); d_builder = new quantifiers::fmcheck::FullModelChecker( c, this ); @@ -873,11 +875,6 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ addTermToDatabase(d_term_util->getInstConstantBody(f), true); } -void QuantifiersEngine::propagate( Theory::Effort level ){ - CodeTimer codeTimer(d_statistics.d_time); - -} - Node QuantifiersEngine::getNextDecisionRequest( unsigned& priority ){ unsigned min_priority = 0; Node dec; @@ -989,23 +986,6 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){ d_phase_req_waiting[lit] = req; } -bool QuantifiersEngine::addSplit( Node n, bool reqPhase, bool reqPhasePol ){ - n = Rewriter::rewrite( n ); - Node lem = NodeManager::currentNM()->mkNode( OR, n, n.notNode() ); - if( addLemma( lem ) ){ - Debug("inst") << "*** Add split " << n<< std::endl; - return true; - } - return false; -} - -bool QuantifiersEngine::addSplitEquality( Node n1, Node n2, bool reqPhase, bool reqPhasePol ){ - //Assert( !areEqual( n1, n2 ) ); - //Assert( !areDisequal( n1, n2 ) ); - Node fm = NodeManager::currentNM()->mkNode( EQUAL, n1, n2 ); - return addSplit( fm ); -} - bool QuantifiersEngine::addEPRAxiom( TypeNode tn ) { if( d_qepr ){ Assert( !options::incrementalSolving() ); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index 56fe06257..674954023 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -289,8 +289,6 @@ public: void registerPattern( std::vector<Node> & pattern); /** assert universal quantifier */ void assertQuantifier( Node q, bool pol ); - /** propagate */ - void propagate( Theory::Effort level ); /** get next decision request */ Node getNextDecisionRequest( unsigned& priority ); private: @@ -314,10 +312,6 @@ public: bool removeLemma( Node lem ); /** add require phase */ void addRequirePhase( Node lit, bool req ); - /** split on node n */ - bool addSplit( Node n, bool reqPhase = false, bool reqPhasePol = true ); - /** add split equality */ - bool addSplitEquality( Node n1, Node n2, bool reqPhase = false, bool reqPhasePol = true ); /** add EPR axiom */ bool addEPRAxiom( TypeNode tn ); /** mark relevant quantified formula, this will indicate it should be checked before the others */ |