//for finite model finding
if( ! options::instWhenMode.wasSetByUser()){
+ //instantiate only on last call
if( options::fmfInstEngine() ){
Trace("smt") << "setting inst when mode to LAST_CALL" << endl;
options::instWhenMode.set( INST_WHEN_LAST_CALL );
}
}
+ if ( ! options::fmfInstGen.wasSetByUser()) {
+ //if full model checking is on, disable inst-gen techniques
+ if( options::fmfFullModelCheck() ){
+ options::fmfInstGen.set( false );
+ }
+ }
//until bugs 371,431 are fixed
if( ! options::minisatUseElim.wasSetByUser()){
inst_strategy_e_matching.h \
inst_strategy_e_matching.cpp \
inst_strategy_cbqi.h \
- inst_strategy_cbqi.cpp
+ inst_strategy_cbqi.cpp \
+ full_model_check.h \
+ full_model_check.cpp \
+ bounded_integers.h \
+ bounded_integers.cpp
EXTRA_DIST = \
kinds \
--- /dev/null
+/********************* */\r
+/*! \file bounded_integers.cpp\r
+ ** \verbatim\r
+ ** Original author: Andrew Reynolds\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Bounded integers module\r
+ **\r
+ ** This class manages integer bounds for quantifiers\r
+ **/\r
+\r
+#include "theory/quantifiers/bounded_integers.h"\r
+#include "theory/quantifiers/quant_util.h"\r
+\r
+using namespace CVC4;\r
+using namespace std;\r
+using namespace CVC4::theory;\r
+using namespace CVC4::theory::quantifiers;\r
+using namespace CVC4::kind;\r
+\r
+BoundedIntegers::BoundedIntegers(QuantifiersEngine* qe) : QuantifiersModule(qe){\r
+\r
+}\r
+\r
+void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {\r
+ if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){\r
+ std::map< Node, Node > msum;\r
+ if (QuantArith::getMonomialSumLit( lit, msum )){\r
+ Trace("bound-integers") << "Literal " << lit << " is monomial sum : " << std::endl;\r
+ for(std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){\r
+ Trace("bound-integers") << " ";\r
+ if( !it->second.isNull() ){\r
+ Trace("bound-integers") << it->second;\r
+ if( !it->first.isNull() ){\r
+ Trace("bound-integers") << " * ";\r
+ }\r
+ }\r
+ if( !it->first.isNull() ){\r
+ Trace("bound-integers") << it->first;\r
+ }\r
+ Trace("bound-integers") << std::endl;\r
+ }\r
+ Trace("bound-integers") << std::endl;\r
+ for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){\r
+ if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE ){\r
+ Node veq;\r
+ if( QuantArith::isolate( it->first, msum, veq, GEQ ) ){\r
+ Trace("bound-integers") << "Isolated for " << it->first << " : " << veq << std::endl;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {\r
+ std::cout << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;\r
+ exit(0);\r
+ }\r
+}\r
+\r
+void BoundedIntegers::process( Node f, Node n, bool pol ){\r
+ if( (( n.getKind()==IMPLIES || n.getKind()==OR) && pol) || (n.getKind()==AND && !pol) ){\r
+ for( unsigned i=0; i<n.getNumChildren(); i++) {\r
+ bool newPol = n.getKind()==IMPLIES && i==0 ? !pol : pol;\r
+ process( f, n[i], newPol );\r
+ }\r
+ }else if( n.getKind()==NOT ){\r
+ process( f, n[0], !pol );\r
+ }else {\r
+ processLiteral( f, n, pol );\r
+ }\r
+}\r
+\r
+void BoundedIntegers::check( Theory::Effort e ) {\r
+\r
+}\r
+\r
+void BoundedIntegers::registerQuantifier( Node f ) {\r
+ bool hasIntType = false;\r
+ for( unsigned i=0; i<f[0].getNumChildren(); i++) {\r
+ if( f[0][i].getType().isInteger() ){\r
+ hasIntType = true;\r
+ break;\r
+ }\r
+ }\r
+ if( hasIntType ){\r
+ process( f, f[1], true );\r
+ }\r
+}\r
+\r
+void BoundedIntegers::assertNode( Node n ) {\r
+\r
+}\r
+\r
+Node BoundedIntegers::getNextDecisionRequest() {\r
+ return Node::null();\r
+}\r
--- /dev/null
+/********************* */\r
+/*! \file bounded_integers.h\r
+** \verbatim\r
+** Original author: Andrew Reynolds\r
+** This file is part of the CVC4 project.\r
+** Copyright (c) 2009-2013 New York University and The University of Iowa\r
+** See the file COPYING in the top-level source directory for licensing\r
+** information.\endverbatim\r
+**\r
+** \brief This class manages integer bounds for quantifiers\r
+**/\r
+\r
+#include "cvc4_private.h"\r
+\r
+#ifndef __CVC4__BOUNDED_INTEGERS_H\r
+#define __CVC4__BOUNDED_INTEGERS_H\r
+\r
+\r
+#include "theory/quantifiers_engine.h"\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+namespace quantifiers {\r
+\r
+class BoundedIntegers : public QuantifiersModule\r
+{\r
+private:\r
+ std::map< Node, std::map< Node, Node > > d_lowers;\r
+ std::map< Node, std::map< Node, Node > > d_uppers;\r
+ std::map< Node, std::map< Node, bool > > d_set;\r
+ void hasFreeVar( Node f, Node n );\r
+ void process( Node f, Node n, bool pol );\r
+ void processLiteral( Node f, Node lit, bool pol );\r
+public:\r
+ BoundedIntegers( QuantifiersEngine* qe );\r
+\r
+ void check( Theory::Effort e );\r
+ void registerQuantifier( Node f );\r
+ void assertNode( Node n );\r
+ Node getNextDecisionRequest();\r
+};\r
+\r
+}\r
+}\r
+}\r
+\r
+#endif
\ No newline at end of file
--- /dev/null
+\r
+/********************* */\r
+/*! \file full_model_check.cpp\r
+ ** \verbatim\r
+ ** Original author: Andrew Reynolds\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Implementation of full model check class\r
+ **/\r
+\r
+#include "theory/quantifiers/full_model_check.h"\r
+#include "theory/quantifiers/first_order_model.h"\r
+#include "theory/quantifiers/options.h"\r
+\r
+using namespace std;\r
+using namespace CVC4;\r
+using namespace CVC4::kind;\r
+using namespace CVC4::context;\r
+using namespace CVC4::theory;\r
+using namespace CVC4::theory::quantifiers;\r
+using namespace CVC4::theory::inst;\r
+using namespace CVC4::theory::quantifiers::fmcheck;\r
+\r
+\r
+bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) {\r
+ if (index==(int)c.getNumChildren()) {\r
+ return d_data!=-1;\r
+ }else{\r
+ Node st = m->getStar(c[index].getType());\r
+ if(d_child.find(st)!=d_child.end()) {\r
+ if( d_child[st].hasGeneralization(m, c, index+1) ){\r
+ return true;\r
+ }\r
+ }\r
+ if( d_child.find( c[index] )!=d_child.end() ){\r
+ if( d_child[ c[index] ].hasGeneralization(m, c, index+1) ){\r
+ return true;\r
+ }\r
+ }\r
+ return false;\r
+ }\r
+}\r
+\r
+int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index ) {\r
+ if (index==(int)inst.size()) {\r
+ return d_data;\r
+ }else{\r
+ int minIndex = -1;\r
+ Node st = m->getStar(inst[index].getType());\r
+ if(d_child.find(st)!=d_child.end()) {\r
+ minIndex = d_child[st].getGeneralizationIndex(m, inst, index+1);\r
+ }\r
+ Node cc = inst[index];\r
+ if( d_child.find( cc )!=d_child.end() ){\r
+ int gindex = d_child[ cc ].getGeneralizationIndex(m, inst, index+1);\r
+ if (minIndex==-1 || (gindex!=-1 && gindex<minIndex) ){\r
+ minIndex = gindex;\r
+ }\r
+ }\r
+ return minIndex;\r
+ }\r
+}\r
+\r
+void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int index ) {\r
+ if (index==(int)c.getNumChildren()) {\r
+ if(d_data==-1) {\r
+ d_data = data;\r
+ }\r
+ }\r
+ else {\r
+ d_child[ c[index] ].addEntry(m,c,v,data,index+1);\r
+ }\r
+}\r
+\r
+void EntryTrie::getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {\r
+ if (index==(int)c.getNumChildren()) {\r
+ if( d_data!=-1) {\r
+ if( is_gen ){\r
+ gen.push_back(d_data);\r
+ }\r
+ compat.push_back(d_data);\r
+ }\r
+ }else{\r
+ if (m->isStar(c[index])) {\r
+ for ( std::map<Node,EntryTrie>::iterator it = d_child.begin(); it != d_child.end(); ++it ){\r
+ it->second.getEntries(m, c, compat, gen, index+1, is_gen );\r
+ }\r
+ }else{\r
+ Node st = m->getStar(c[index].getType());\r
+ if(d_child.find(st)!=d_child.end()) {\r
+ d_child[st].getEntries(m, c, compat, gen, index+1, false);\r
+ }\r
+ if( d_child.find( c[index] )!=d_child.end() ){\r
+ d_child[ c[index] ].getEntries(m, c, compat, gen, index+1, is_gen);\r
+ }\r
+ }\r
+\r
+ }\r
+}\r
+\r
+bool EntryTrie::getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index) {\r
+\r
+ return false;\r
+}\r
+\r
+\r
+bool Def::addEntry( FullModelChecker * m, Node c, Node v) {\r
+ if (!d_et.hasGeneralization(m, c)) {\r
+ int newIndex = (int)d_cond.size();\r
+ if (!d_has_simplified) {\r
+ std::vector<int> compat;\r
+ std::vector<int> gen;\r
+ d_et.getEntries(m, c, compat, gen);\r
+ for( unsigned i=0; i<compat.size(); i++) {\r
+ if( d_status[compat[i]]==status_unk ){\r
+ if( d_value[compat[i]]!=v ){\r
+ d_status[compat[i]] = status_non_redundant;\r
+ }\r
+ }\r
+ }\r
+ for( unsigned i=0; i<gen.size(); i++) {\r
+ if( d_status[gen[i]]==status_unk ){\r
+ if( d_value[gen[i]]==v ){\r
+ d_status[gen[i]] = status_redundant;\r
+ }\r
+ }\r
+ }\r
+ d_status.push_back( status_unk );\r
+ }\r
+ d_et.addEntry(m, c, v, newIndex);\r
+ d_cond.push_back(c);\r
+ d_value.push_back(v);\r
+ return true;\r
+ }else{\r
+ return false;\r
+ }\r
+}\r
+\r
+Node Def::evaluate( FullModelChecker * m, std::vector<Node> inst ) {\r
+ int gindex = d_et.getGeneralizationIndex(m, inst);\r
+ if (gindex!=-1) {\r
+ return d_value[gindex];\r
+ }else{\r
+ return Node::null();\r
+ }\r
+}\r
+\r
+int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst ) {\r
+ return d_et.getGeneralizationIndex(m, inst);\r
+}\r
+\r
+void Def::simplify(FullModelChecker * m) {\r
+ d_has_simplified = true;\r
+ std::vector< Node > cond;\r
+ cond.insert( cond.end(), d_cond.begin(), d_cond.end() );\r
+ d_cond.clear();\r
+ std::vector< Node > value;\r
+ value.insert( value.end(), d_value.begin(), d_value.end() );\r
+ d_value.clear();\r
+ d_et.reset();\r
+ for (unsigned i=0; i<d_status.size(); i++) {\r
+ if( d_status[i]!=status_redundant ){\r
+ addEntry(m, d_cond[i], d_value[i]);\r
+ }\r
+ }\r
+ d_status.clear();\r
+}\r
+\r
+void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {\r
+ if (!op.isNull()) {\r
+ Trace(tr) << "Model for " << op << " : " << std::endl;\r
+ }\r
+ for( unsigned i=0; i<d_cond.size(); i++) {\r
+ //print the condition\r
+ if (!op.isNull()) {\r
+ Trace(tr) << op;\r
+ }\r
+ m->debugPrintCond(tr, d_cond[i], true);\r
+ Trace(tr) << " -> ";\r
+ m->debugPrint(tr, d_value[i]);\r
+ Trace(tr) << std::endl;\r
+ }\r
+}\r
+\r
+\r
+FullModelChecker::FullModelChecker(QuantifiersEngine* qe) : d_qe(qe){\r
+ d_true = NodeManager::currentNM()->mkConst(true);\r
+ d_false = NodeManager::currentNM()->mkConst(false);\r
+}\r
+\r
+void FullModelChecker::reset(FirstOrderModel * fm) {\r
+ Trace("fmc") << "---Full Model Check reset() " << std::endl;\r
+ for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){\r
+ it->second->reset();\r
+ }\r
+ d_quant_models.clear();\r
+ d_models_init.clear();\r
+ d_rep_ids.clear();\r
+ d_model_basis_rep.clear();\r
+ d_star_insts.clear();\r
+ //process representatives\r
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();\r
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){\r
+ if( it->first.isSort() ){\r
+ if( d_type_star.find(it->first)==d_type_star.end() ){\r
+ Node st = NodeManager::currentNM()->mkSkolem( "star_$$", it->first, "skolem created for full-model checking" );\r
+ d_type_star[it->first] = st;\r
+ }\r
+ Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;\r
+ Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);\r
+ Node rmbt = fm->getRepresentative(mbt);\r
+ int mbt_index = -1;\r
+ Trace("fmc") << " Model basis term : " << mbt << std::endl;\r
+ for( size_t a=0; a<it->second.size(); a++ ){\r
+ //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] );\r
+ //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 );\r
+ Node r = fm->getRepresentative( it->second[a] );\r
+ std::vector< Node > eqc;\r
+ ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );\r
+ Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt);\r
+ Trace("fmc-model-debug") << " : " << it->second[a] << " : " << r << " : ";\r
+ //Trace("fmc-model-debug") << r2 << " : " << ir << " : ";\r
+ Trace("fmc-model-debug") << " {";\r
+ //find best selection for representative\r
+ for( size_t i=0; i<eqc.size(); i++ ){\r
+ Trace("fmc-model-debug") << eqc[i] << ", ";\r
+ }\r
+ Trace("fmc-model-debug") << "}" << std::endl;\r
+\r
+ //if this is the model basis eqc, replace with actual model basis term\r
+ if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {\r
+ d_model_basis_rep[it->first] = r;\r
+ r = mbt;\r
+ mbt_index = a;\r
+ }\r
+ d_rep_ids[it->first][r] = (int)a;\r
+ }\r
+ Trace("fmc-model-debug") << std::endl;\r
+\r
+ if (mbt_index==-1) {\r
+ std::cout << " WARNING: model basis term is not a representative!" << std::endl;\r
+ exit(0);\r
+ }else{\r
+ Trace("fmc") << "Star index for " << it->first << " is " << mbt_index << std::endl;\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+Node FullModelChecker::getRepresentative(FirstOrderModel * fm, Node n) {\r
+ //Assert( fm->hasTerm(n) );\r
+ TypeNode tn = n.getType();\r
+ if( tn.isBoolean() ){\r
+ return fm->areEqual(n, d_true) ? d_true : d_false;\r
+ }else{\r
+ Node r = fm->getRepresentative(n);\r
+ if (r==d_model_basis_rep[tn]) {\r
+ r = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
+ }\r
+ return r;\r
+ }\r
+}\r
+\r
+struct ModelBasisArgSort\r
+{\r
+ std::vector< Node > d_terms;\r
+ bool operator() (int i,int j) {\r
+ return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <\r
+ d_terms[j].getAttribute(ModelBasisArgAttribute()) );\r
+ }\r
+};\r
+\r
+void FullModelChecker::addEntry( FirstOrderModel * fm, Node op, Node c, Node v,\r
+ std::vector< Node > & conds,\r
+ std::vector< Node > & values,\r
+ std::vector< Node > & entry_conds ) {\r
+ std::vector< Node > children;\r
+ std::vector< Node > entry_children;\r
+ children.push_back(op);\r
+ entry_children.push_back(op);\r
+ bool hasNonStar = false;\r
+ for( unsigned i=0; i<c.getNumChildren(); i++) {\r
+ Node ri = getRepresentative(fm, c[i]);\r
+ children.push_back(ri);\r
+ if (isModelBasisTerm(ri)) {\r
+ ri = d_type_star[ri.getType()];\r
+ }else{\r
+ hasNonStar = true;\r
+ }\r
+ entry_children.push_back(ri);\r
+ }\r
+ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );\r
+ Node nv = getRepresentative(fm, v);\r
+ Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );\r
+ if( std::find(conds.begin(), conds.end(), n )==conds.end() ){\r
+ Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;\r
+ conds.push_back(n);\r
+ values.push_back(nv);\r
+ entry_conds.push_back(en);\r
+ }\r
+}\r
+\r
+Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) {\r
+ if( d_models_init.find(op)==d_models_init.end() ){\r
+ if( d_models.find(op)==d_models.end() ){\r
+ d_models[op] = new Def;\r
+ //make sure star's are defined\r
+ TypeNode tn = op.getType();\r
+ for(unsigned i=0; i<tn.getNumChildren()-1; i++) {\r
+ if( d_type_star.find(tn[i])==d_type_star.end() ){\r
+ Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn[i], "skolem created for full-model checking" );\r
+ d_type_star[tn[i]] = st;\r
+ }\r
+ }\r
+ }\r
+ //reset the model\r
+ d_models[op]->reset();\r
+\r
+ std::vector< Node > conds;\r
+ std::vector< Node > values;\r
+ std::vector< Node > entry_conds;\r
+ Trace("fmc-model-debug") << "Model values for " << op << " ... " << std::endl;\r
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){\r
+ Node r = getRepresentative(fm, fm->d_uf_terms[op][i]);\r
+ Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;\r
+ }\r
+ Trace("fmc-model-debug") << std::endl;\r
+ //initialize the model\r
+ for( int j=0; j<2; j++ ){\r
+ for( int k=1; k>=0; k-- ){\r
+ Trace("fmc-model-debug")<< "Set values " << j << " " << k << " : " << std::endl;\r
+ for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[j][k].begin();\r
+ it != fm->d_uf_model_gen[op].d_set_values[j][k].end(); ++it ){\r
+ Trace("fmc-model-debug") << " process : " << it->first << " -> " << it->second << std::endl;\r
+ if( j==1 ){\r
+ addEntry(fm, op, it->first, it->second, conds, values, entry_conds);\r
+ }\r
+ }\r
+ }\r
+ }\r
+ //add for default value\r
+ if (!fm->d_uf_model_gen[op].d_default_value.isNull()) {\r
+ Node n = d_qe->getTermDatabase()->getModelBasisOpTerm(op);\r
+ addEntry(fm, op, n, fm->d_uf_model_gen[op].d_default_value, conds, values, entry_conds);\r
+ }\r
+\r
+ //find other default values (TODO: figure out why these entries are added to d_uf_model_gen)\r
+ if( conds.empty() ){\r
+ //for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[1][0].begin();\r
+ // it != fm->d_uf_model_gen[op].d_set_values[1][0].end(); ++it ){\r
+ // Trace("fmc-model-debug") << " process : " << it->first << " -> " << it->second << std::endl;\r
+ // addEntry(fm, op, it->first, it->second, conds, values, entry_conds);\r
+ //}\r
+ Trace("fmc-warn") << "WARNING: No entries for " << op << ", make default entry." << std::endl;\r
+ //choose a complete arbitrary term\r
+ Node n = d_qe->getTermDatabase()->getModelBasisOpTerm(op);\r
+ TypeNode tn = n.getType();\r
+ Node v = fm->d_rep_set.d_type_reps[tn][0];\r
+ addEntry(fm, op, n, v, conds, values, entry_conds);\r
+ }\r
+\r
+ //sort based on # default arguments\r
+ std::vector< int > indices;\r
+ ModelBasisArgSort mbas;\r
+ for (int i=0; i<(int)conds.size(); i++) {\r
+ d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );\r
+ mbas.d_terms.push_back(conds[i]);\r
+ indices.push_back(i);\r
+ }\r
+ std::sort( indices.begin(), indices.end(), mbas );\r
+\r
+\r
+ for (int i=0; i<(int)indices.size(); i++) {\r
+ d_models[op]->addEntry(this, entry_conds[indices[i]], values[indices[i]]);\r
+ }\r
+ d_models[op]->debugPrint("fmc-model", op, this);\r
+ Trace("fmc-model") << std::endl;\r
+\r
+ d_models[op]->simplify( this );\r
+ Trace("fmc-model-simplify") << "After simplification : " << std::endl;\r
+ d_models[op]->debugPrint("fmc-model-simplify", op, this);\r
+ Trace("fmc-model-simplify") << std::endl;\r
+\r
+ d_models_init[op] = true;\r
+ }\r
+ return d_models[op];\r
+}\r
+\r
+\r
+bool FullModelChecker::isStar(Node n) {\r
+ return n==d_type_star[n.getType()];\r
+}\r
+\r
+bool FullModelChecker::isModelBasisTerm(Node n) {\r
+ return n==getModelBasisTerm(n.getType());\r
+}\r
+\r
+Node FullModelChecker::getModelBasisTerm(TypeNode tn) {\r
+ return d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
+}\r
+\r
+void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {\r
+ Trace(tr) << "(";\r
+ for( unsigned j=0; j<n.getNumChildren(); j++) {\r
+ if( j>0 ) Trace(tr) << ", ";\r
+ debugPrint(tr, n[j], dispStar);\r
+ }\r
+ Trace(tr) << ")";\r
+}\r
+\r
+void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {\r
+ if( n.isNull() ){\r
+ Trace(tr) << "null";\r
+ }\r
+ else if(isStar(n) && dispStar) {\r
+ Trace(tr) << "*";\r
+ }else{\r
+ TypeNode tn = n.getType();\r
+ if( d_rep_ids.find(tn)!=d_rep_ids.end() ){\r
+ if (d_rep_ids[tn].find(n)!=d_rep_ids[tn].end()) {\r
+ Trace(tr) << d_rep_ids[tn][n];\r
+ }else{\r
+ Trace(tr) << n;\r
+ }\r
+ }else{\r
+ Trace(tr) << n;\r
+ }\r
+ }\r
+}\r
+\r
+\r
+int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, int effort) {\r
+ int addedLemmas = 0;\r
+ Trace("fmc") << "Full model check " << f << ", effort = " << effort << "..." << std::endl;\r
+ if (effort==0) {\r
+ //register the quantifier\r
+ if (d_quant_cond.find(f)==d_quant_cond.end()) {\r
+ std::vector< TypeNode > types;\r
+ for(unsigned i=0; i<f[0].getNumChildren(); i++){\r
+ types.push_back(f[0][i].getType());\r
+ d_quant_var_id[f][f[0][i]] = i;\r
+ }\r
+ TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() );\r
+ Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );\r
+ d_quant_cond[f] = op;\r
+ }\r
+\r
+ //model check the quantifier\r
+ doCheck(fm, f, d_quant_models[f], f[1]);\r
+ Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;\r
+ d_quant_models[f].debugPrint("fmc", Node::null(), this);\r
+ Trace("fmc") << std::endl;\r
+ //consider all entries going to false\r
+ for (unsigned i=0; i<d_quant_models[f].d_cond.size(); i++) {\r
+ if( d_quant_models[f].d_value[i]!=d_true) {\r
+ Trace("fmc-inst") << "Instantiate based on " << d_quant_models[f].d_cond[i] << "..." << std::endl;\r
+ bool hasStar = false;\r
+ std::vector< Node > inst;\r
+ for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {\r
+ if (isStar(d_quant_models[f].d_cond[i][j])) {\r
+ hasStar = true;\r
+ inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));\r
+ }else{\r
+ inst.push_back(d_quant_models[f].d_cond[i][j]);\r
+ }\r
+ }\r
+ bool addInst = true;\r
+ if( hasStar ){\r
+ //try obvious (specified by inst)\r
+ Node ev = d_quant_models[f].evaluate(this, inst);\r
+ if (ev==d_true) {\r
+ addInst = false;\r
+ }\r
+ }else{\r
+ //for debugging\r
+ if (Trace.isOn("fmc-test-inst")) {\r
+ Node ev = d_quant_models[f].evaluate(this, inst);\r
+ if( ev==d_true ){\r
+ std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;\r
+ exit(0);\r
+ }else{\r
+ Trace("fmc-test-inst") << "...instantiation evaluated to false." << std::endl;\r
+ }\r
+ }\r
+ }\r
+ if( addInst ){\r
+ InstMatch m;\r
+ for( unsigned j=0; j<inst.size(); j++) {\r
+ m.set( d_qe, f, j, inst[j] );\r
+ }\r
+ if (isActive()) {\r
+ if( d_qe->addInstantiation( f, m ) ){\r
+ addedLemmas++;\r
+ }else{\r
+ //this can happen if evaluation is unknown\r
+ //might try it next effort level\r
+ d_star_insts[f].push_back(i);\r
+ }\r
+ }\r
+ }else{\r
+ //might try it next effort level\r
+ d_star_insts[f].push_back(i);\r
+ }\r
+ }\r
+ }\r
+ }else{\r
+ //TODO\r
+ Trace("fmc-exh") << "Definition was : " << std::endl;\r
+ d_quant_models[f].debugPrint("fmc-exh", Node::null(), this);\r
+ Trace("fmc-exh") << std::endl;\r
+ Def temp;\r
+ //simplify the exceptions?\r
+ for( int i=(d_star_insts[f].size()-1); i>=0; i--) {\r
+ //get witness for d_star_insts[f][i]\r
+ int j = d_star_insts[f][i];\r
+ if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){\r
+ int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );\r
+ if( lem==-1 ){\r
+ return -1;\r
+ }else{\r
+ addedLemmas += lem;\r
+ }\r
+ }\r
+ }\r
+ }\r
+ return addedLemmas;\r
+}\r
+\r
+int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {\r
+ int addedLemmas = 0;\r
+ RepSetIterator riter( &(fm->d_rep_set) );\r
+ Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";\r
+ debugPrintCond("fmc-exh", c, true);\r
+ Trace("fmc-exh")<< std::endl;\r
+ if( riter.setQuantifier( f ) ){\r
+ std::vector< RepDomain > dom;\r
+ for (unsigned i=0; i<c.getNumChildren(); i++) {\r
+ TypeNode tn = c[i].getType();\r
+ if( d_rep_ids.find(tn)!=d_rep_ids.end() ){\r
+ RepDomain rd;\r
+ if( isStar(c[i]) ){\r
+ //add the full range\r
+ for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();\r
+ it != d_rep_ids[tn].end(); ++it ){\r
+ rd.push_back(it->second);\r
+ }\r
+ }else{\r
+ if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {\r
+ rd.push_back(d_rep_ids[tn][c[i]]);\r
+ }else{\r
+ return -1;\r
+ }\r
+ }\r
+ dom.push_back(rd);\r
+ }else{\r
+ return -1;\r
+ }\r
+ }\r
+ riter.setDomain(dom);\r
+ //now do full iteration\r
+ while( !riter.isFinished() ){\r
+ Trace("fmc-exh-debug") << "Inst : ";\r
+ std::vector< Node > inst;\r
+ for( int i=0; i<riter.getNumTerms(); i++ ){\r
+ //m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );\r
+ Node r = getRepresentative( fm, riter.getTerm( i ) );\r
+ debugPrint("fmc-exh-debug", r);\r
+ Trace("fmc-exh-debug") << " ";\r
+ inst.push_back(r);\r
+ }\r
+\r
+ int ev_index = d_quant_models[f].getGeneralizationIndex(this, inst);\r
+ Trace("fmc-exh-debug") << ", index = " << ev_index;\r
+ Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];\r
+ if (ev!=d_true) {\r
+ InstMatch m;\r
+ for( int i=0; i<riter.getNumTerms(); i++ ){\r
+ m.set( d_qe, f, i, riter.getTerm( i ) );\r
+ }\r
+ Trace("fmc-exh-debug") << ", add!";\r
+ //add as instantiation\r
+ if( d_qe->addInstantiation( f, m ) ){\r
+ addedLemmas++;\r
+ }\r
+ }\r
+ Trace("fmc-exh-debug") << std::endl;\r
+ riter.increment();\r
+ }\r
+ }\r
+ return addedLemmas;\r
+}\r
+\r
+void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) {\r
+ Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;\r
+ if( n.getKind() == kind::BOUND_VARIABLE ){\r
+ d.addEntry(this, mkCondDefault(f), n);\r
+ }\r
+ else if( n.getNumChildren()==0 ){\r
+ Node r = n;\r
+ if( !fm->hasTerm(n) ){\r
+ if (fm->d_rep_set.hasType(n.getType())) {\r
+ r = fm->d_rep_set.d_type_reps[n.getType()][0];\r
+ }else{\r
+ //should never happen?\r
+ }\r
+ }\r
+ r = getRepresentative(fm, r);\r
+ d.addEntry(this, mkCondDefault(f), r);\r
+ }\r
+ else if( n.getKind() == kind::NOT ){\r
+ //just do directly\r
+ doCheck( fm, f, d, n[0] );\r
+ doNegate( d );\r
+ }\r
+ else if( n.getKind() == kind::FORALL ){\r
+ d.addEntry(this, mkCondDefault(f), Node::null());\r
+ }\r
+ else{\r
+ std::vector< int > var_ch;\r
+ std::vector< Def > children;\r
+ for( int i=0; i<(int)n.getNumChildren(); i++) {\r
+ Def dc;\r
+ doCheck(fm, f, dc, n[i]);\r
+ children.push_back(dc);\r
+ if( n[i].getKind() == kind::BOUND_VARIABLE ){\r
+ var_ch.push_back(i);\r
+ }\r
+ }\r
+\r
+ if( n.getKind()==APPLY_UF ){\r
+ Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl;\r
+ //uninterpreted compose\r
+ doUninterpretedCompose( fm, f, d, n.getOperator(), children );\r
+ } else {\r
+ if( !var_ch.empty() ){\r
+ if( n.getKind()==EQUAL ){\r
+ if( var_ch.size()==2 ){\r
+ Trace("fmc-debug") << "Do variable equality " << n << std::endl;\r
+ doVariableEquality( fm, f, d, n );\r
+ }else{\r
+ Trace("fmc-debug") << "Do variable relation " << n << std::endl;\r
+ doVariableRelation( fm, f, d, var_ch[0]==0 ? children[1] : children[0], var_ch[0]==0 ? n[0] : n[1] );\r
+ }\r
+ }else{\r
+ std::cout << "Don't know how to check " << n << std::endl;\r
+ exit(0);\r
+ }\r
+ }else{\r
+ Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;\r
+ std::vector< Node > cond;\r
+ mkCondDefaultVec(f, cond);\r
+ std::vector< Node > val;\r
+ //interpreted compose\r
+ doInterpretedCompose( fm, f, d, n, children, 0, cond, val );\r
+ }\r
+ }\r
+ d.simplify(this);\r
+ }\r
+ Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;\r
+ d.debugPrint("fmc-debug", Node::null(), this);\r
+ Trace("fmc-debug") << std::endl;\r
+}\r
+\r
+void FullModelChecker::doNegate( Def & dc ) {\r
+ for (unsigned i=0; i<dc.d_cond.size(); i++) {\r
+ if (!dc.d_value[i].isNull()) {\r
+ dc.d_value[i] = dc.d_value[i]==d_true ? d_false : d_true;\r
+ }\r
+ }\r
+}\r
+\r
+void FullModelChecker::doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq ) {\r
+ std::vector<Node> cond;\r
+ mkCondDefaultVec(f, cond);\r
+ if (eq[0]==eq[1]){\r
+ d.addEntry(this, mkCond(cond), d_true);\r
+ }else{\r
+ int j = getVariableId(f, eq[0]);\r
+ int k = getVariableId(f, eq[1]);\r
+ TypeNode tn = eq[0].getType();\r
+ for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {\r
+ Node r = getRepresentative( fm, fm->d_rep_set.d_type_reps[tn][i] );\r
+ cond[j+1] = r;\r
+ cond[k+1] = r;\r
+ d.addEntry( this, mkCond(cond), d_true);\r
+ }\r
+ d.addEntry(this, mkCondDefault(f), d_false);\r
+ }\r
+}\r
+\r
+void FullModelChecker::doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v) {\r
+ int j = getVariableId(f, v);\r
+ for (unsigned i=0; i<dc.d_cond.size(); i++) {\r
+ Node val = dc.d_value[i];\r
+ if( dc.d_cond[i][j]!=val ){\r
+ if (isStar(dc.d_cond[i][j])) {\r
+ std::vector<Node> cond;\r
+ mkCondVec(dc.d_cond[i],cond);\r
+ cond[j+1] = val;\r
+ d.addEntry(this, mkCond(cond), d_true);\r
+ cond[j+1] = d_type_star[val.getType()];\r
+ d.addEntry(this, mkCond(cond), d_false);\r
+ }else{\r
+ d.addEntry( this, dc.d_cond[i], d_false);\r
+ }\r
+ }else{\r
+ d.addEntry( this, dc.d_cond[i], d_true);\r
+ }\r
+ }\r
+}\r
+\r
+void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {\r
+ Trace("fmc-uf-debug") << "Definition : " << std::endl;\r
+ d_models[op]->debugPrint("fmc-uf-debug", op, this);\r
+ Trace("fmc-uf-debug") << std::endl;\r
+\r
+ std::vector< Node > cond;\r
+ mkCondDefaultVec(f, cond);\r
+ std::vector< Node > val;\r
+ doUninterpretedCompose( fm, f, op, d, dc, 0, cond, val);\r
+}\r
+\r
+void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,\r
+ std::vector< Def > & dc, int index,\r
+ std::vector< Node > & cond, std::vector<Node> & val ) {\r
+ Trace("fmc-uf-process") << "process at " << index << std::endl;\r
+ for( unsigned i=1; i<cond.size(); i++) {\r
+ debugPrint("fmc-uf-process", cond[i], true);\r
+ Trace("fmc-uf-process") << " ";\r
+ }\r
+ Trace("fmc-uf-process") << std::endl;\r
+ if (index==(int)dc.size()) {\r
+ //we have an entry, now do actual compose\r
+ std::map< int, Node > entries;\r
+ doUninterpretedCompose2( fm, f, entries, 0, cond, val, d_models[op]->d_et);\r
+ //add them to the definition\r
+ for( unsigned e=0; e<d_models[op]->d_cond.size(); e++ ){\r
+ if ( entries.find(e)!=entries.end() ){\r
+ d.addEntry(this, entries[e], d_models[op]->d_value[e] );\r
+ }\r
+ }\r
+ }else{\r
+ for (unsigned i=0; i<dc[index].d_cond.size(); i++) {\r
+ if (isCompat(cond, dc[index].d_cond[i])!=0) {\r
+ std::vector< Node > new_cond;\r
+ new_cond.insert(new_cond.end(), cond.begin(), cond.end());\r
+ if( doMeet(new_cond, dc[index].d_cond[i]) ){\r
+ Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;\r
+ val.push_back(dc[index].d_value[i]);\r
+ doUninterpretedCompose(fm, f, op, d, dc, index+1, new_cond, val);\r
+ val.pop_back();\r
+ }else{\r
+ Trace("fmc-uf-process") << "index " << i << " failed meet." << std::endl;\r
+ }\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f,\r
+ std::map< int, Node > & entries, int index,\r
+ std::vector< Node > & cond, std::vector< Node > & val,\r
+ EntryTrie & curr ) {\r
+ Trace("fmc-uf-process") << "compose " << index << std::endl;\r
+ for( unsigned i=1; i<cond.size(); i++) {\r
+ debugPrint("fmc-uf-process", cond[i], true);\r
+ Trace("fmc-uf-process") << " ";\r
+ }\r
+ Trace("fmc-uf-process") << std::endl;\r
+ if (index==(int)val.size()) {\r
+ Node c = mkCond(cond);\r
+ Trace("fmc-uf-entry") << "Entry : " << c << " -> index[" << curr.d_data << "]" << std::endl;\r
+ entries[curr.d_data] = c;\r
+ }else{\r
+ Node v = val[index];\r
+ bool bind_var = false;\r
+ if( v.getKind()==kind::BOUND_VARIABLE ){\r
+ int j = getVariableId(f, v);\r
+ Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;\r
+ if (!isStar(cond[j+1])) {\r
+ v = cond[j+1];\r
+ }else{\r
+ bind_var = true;\r
+ }\r
+ }\r
+ if (bind_var) {\r
+ Trace("fmc-uf-process") << "bind variable..." << std::endl;\r
+ int j = getVariableId(f, v);\r
+ for (std::map<Node, EntryTrie>::iterator it = curr.d_child.begin(); it != curr.d_child.end(); ++it) {\r
+ cond[j+1] = it->first;\r
+ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);\r
+ }\r
+ cond[j+1] = getStar(v.getType());\r
+ }else{\r
+ if (curr.d_child.find(v)!=curr.d_child.end()) {\r
+ Trace("fmc-uf-process") << "follow value..." << std::endl;\r
+ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);\r
+ }\r
+ Node st = d_type_star[v.getType()];\r
+ if (curr.d_child.find(st)!=curr.d_child.end()) {\r
+ Trace("fmc-uf-process") << "follow star..." << std::endl;\r
+ doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+void FullModelChecker::doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,\r
+ std::vector< Def > & dc, int index,\r
+ std::vector< Node > & cond, std::vector<Node> & val ) {\r
+ if ( index==(int)dc.size() ){\r
+ Node c = mkCond(cond);\r
+ Node v = evaluateInterpreted(n, val);\r
+ d.addEntry(this, c, v);\r
+ }\r
+ else {\r
+ TypeNode vtn = n.getType();\r
+ for (unsigned i=0; i<dc[index].d_cond.size(); i++) {\r
+ if (isCompat(cond, dc[index].d_cond[i])!=0) {\r
+ std::vector< Node > new_cond;\r
+ new_cond.insert(new_cond.end(), cond.begin(), cond.end());\r
+ if( doMeet(new_cond, dc[index].d_cond[i]) ){\r
+ bool process = true;\r
+ if (vtn.isBoolean()) {\r
+ //short circuit\r
+ if( (n.getKind()==OR && dc[index].d_value[i]==d_true) ||\r
+ (n.getKind()==AND && dc[index].d_value[i]==d_false) ){\r
+ Node c = mkCond(new_cond);\r
+ d.addEntry(this, c, dc[index].d_value[i]);\r
+ process = false;\r
+ }\r
+ }\r
+ if (process) {\r
+ val.push_back(dc[index].d_value[i]);\r
+ doInterpretedCompose(fm, f, d, n, dc, index+1, new_cond, val);\r
+ val.pop_back();\r
+ }\r
+ }\r
+ }\r
+ }\r
+ }\r
+}\r
+\r
+int FullModelChecker::isCompat( std::vector< Node > & cond, Node c ) {\r
+ Assert(cond.size()==c.getNumChildren()+1);\r
+ for (unsigned i=1; i<cond.size(); i++) {\r
+ if( cond[i]!=c[i-1] && !isStar(cond[i]) && !isStar(c[i-1]) ) {\r
+ return 0;\r
+ }\r
+ }\r
+ return 1;\r
+}\r
+\r
+bool FullModelChecker::doMeet( std::vector< Node > & cond, Node c ) {\r
+ Assert(cond.size()==c.getNumChildren()+1);\r
+ for (unsigned i=1; i<cond.size(); i++) {\r
+ if( cond[i]!=c[i-1] ) {\r
+ if( isStar(cond[i]) ){\r
+ cond[i] = c[i-1];\r
+ }else if( !isStar(c[i-1]) ){\r
+ return false;\r
+ }\r
+ }\r
+ }\r
+ return true;\r
+}\r
+\r
+Node FullModelChecker::mkCond( std::vector< Node > & cond ) {\r
+ return NodeManager::currentNM()->mkNode(APPLY_UF, cond);\r
+}\r
+\r
+Node FullModelChecker::mkCondDefault( Node f) {\r
+ std::vector< Node > cond;\r
+ mkCondDefaultVec(f, cond);\r
+ return mkCond(cond);\r
+}\r
+\r
+void FullModelChecker::mkCondDefaultVec( Node f, std::vector< Node > & cond ) {\r
+ //get function symbol for f\r
+ cond.push_back(d_quant_cond[f]);\r
+ for (unsigned i=0; i<f[0].getNumChildren(); i++) {\r
+ cond.push_back(d_type_star[f[0][i].getType()]);\r
+ }\r
+}\r
+\r
+void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) {\r
+ cond.push_back(n.getOperator());\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ cond.push_back( n[i] );\r
+ }\r
+}\r
+\r
+Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {\r
+ if( n.getKind()==EQUAL ){\r
+ return vals[0]==vals[1] ? d_true : d_false;\r
+ }else if( n.getKind()==ITE ){\r
+ if( vals[0]==d_true ){\r
+ return vals[1];\r
+ }else if( vals[0]==d_false ){\r
+ return vals[2];\r
+ }else{\r
+ return vals[1]==vals[2] ? vals[1] : Node::null();\r
+ }\r
+ }else if( n.getKind()==AND || n.getKind()==OR ){\r
+ bool isNull = false;\r
+ for (unsigned i=0; i<vals.size(); i++) {\r
+ if((vals[i]==d_true && n.getKind()==OR) || (vals[i]==d_false && n.getKind()==AND)) {\r
+ return vals[i];\r
+ }else if( vals[i].isNull() ){\r
+ isNull = true;\r
+ }\r
+ }\r
+ return isNull ? Node::null() : vals[0];\r
+ }else{\r
+ std::vector<Node> children;\r
+ if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){\r
+ children.push_back( n.getOperator() );\r
+ }\r
+ for (unsigned i=0; i<vals.size(); i++) {\r
+ if( vals[i].isNull() ){\r
+ return Node::null();\r
+ }else{\r
+ children.push_back( vals[i] );\r
+ }\r
+ }\r
+ Node nc = NodeManager::currentNM()->mkNode(n.getKind(), children);\r
+ Trace("fmc-eval") << "Evaluate " << nc << " to ";\r
+ nc = Rewriter::rewrite(nc);\r
+ Trace("fmc-eval") << nc << std::endl;\r
+ return nc;\r
+ }\r
+}\r
+\r
+bool FullModelChecker::isActive() {\r
+ return options::fmfFullModelCheck();\r
+}\r
+\r
+bool FullModelChecker::useSimpleModels() {\r
+ return options::fmfFullModelCheckSimple();\r
+}\r
--- /dev/null
+/********************* */\r
+/*! \file full_model_check.h\r
+ ** \verbatim\r
+ ** Original author: Andrew Reynolds\r
+ ** This file is part of the CVC4 project.\r
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa\r
+ ** See the file COPYING in the top-level source directory for licensing\r
+ ** information.\endverbatim\r
+ **\r
+ ** \brief Full model check class\r
+ **/\r
+\r
+#ifndef FULL_MODEL_CHECK\r
+#define FULL_MODEL_CHECK\r
+\r
+#include "theory/quantifiers/model_builder.h"\r
+\r
+namespace CVC4 {\r
+namespace theory {\r
+namespace quantifiers {\r
+namespace fmcheck {\r
+\r
+\r
+class FullModelChecker;\r
+\r
+class EntryTrie\r
+{\r
+public:\r
+ EntryTrie() : d_data(-1){}\r
+ std::map<Node,EntryTrie> d_child;\r
+ int d_data;\r
+ void reset() { d_data = -1; d_child.clear(); }\r
+ void addEntry( FullModelChecker * m, Node c, Node v, int data, int index = 0 );\r
+ bool hasGeneralization( FullModelChecker * m, Node c, int index = 0 );\r
+ int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index = 0 );\r
+ void getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );\r
+ //if possible, get ground instance of c that evaluates to the entry\r
+ bool getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index = 0 );\r
+};\r
+\r
+\r
+class Def\r
+{\r
+public:\r
+ EntryTrie d_et;\r
+ //cond is APPLY_UF whose arguments are returned by FullModelChecker::getRepresentative\r
+ std::vector< Node > d_cond;\r
+ //value is returned by FullModelChecker::getRepresentative\r
+ std::vector< Node > d_value;\r
+private:\r
+ enum {\r
+ status_unk,\r
+ status_redundant,\r
+ status_non_redundant\r
+ };\r
+ std::vector< int > d_status;\r
+ bool d_has_simplified;\r
+public:\r
+ Def() : d_has_simplified(false){}\r
+ void reset() {\r
+ d_et.reset();\r
+ d_cond.clear();\r
+ d_value.clear();\r
+ d_status.clear();\r
+ d_has_simplified = false;\r
+ }\r
+ bool addEntry( FullModelChecker * m, Node c, Node v);\r
+ Node evaluate( FullModelChecker * m, std::vector<Node> inst );\r
+ int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> inst );\r
+ void simplify( FullModelChecker * m );\r
+ void debugPrint(const char * tr, Node op, FullModelChecker * m);\r
+};\r
+\r
+\r
+class FullModelChecker\r
+{\r
+private:\r
+ Node d_true;\r
+ Node d_false;\r
+ QuantifiersEngine* d_qe;\r
+ std::map<TypeNode, std::map< Node, int > > d_rep_ids;\r
+ std::map<TypeNode, Node > d_model_basis_rep;\r
+ std::map<Node, Def * > d_models;\r
+ std::map<Node, Def > d_quant_models;\r
+ std::map<Node, bool > d_models_init;\r
+ std::map<Node, Node > d_quant_cond;\r
+ std::map<TypeNode, Node > d_type_star;\r
+ std::map<Node, std::map< Node, int > > d_quant_var_id;\r
+ std::map<Node, std::vector< int > > d_star_insts;\r
+ Node getRepresentative(FirstOrderModel * fm, Node n);\r
+ Node normalizeArgReps(FirstOrderModel * fm, Node op, Node n);\r
+ void addEntry( FirstOrderModel * fm, Node op, Node c, Node v,\r
+ std::vector< Node > & conds,\r
+ std::vector< Node > & values,\r
+ std::vector< Node > & entry_conds );\r
+ int exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index);\r
+private:\r
+ void doCheck(FirstOrderModel * fm, Node f, Def & d, Node n );\r
+\r
+ void doNegate( Def & dc );\r
+ void doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq );\r
+ void doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v);\r
+ void doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n, std::vector< Def > & dc );\r
+\r
+ void doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,\r
+ std::vector< Def > & dc, int index,\r
+ std::vector< Node > & cond, std::vector<Node> & val );\r
+ void doUninterpretedCompose2( FirstOrderModel * fm, Node f,\r
+ std::map< int, Node > & entries, int index,\r
+ std::vector< Node > & cond, std::vector< Node > & val,\r
+ EntryTrie & curr);\r
+\r
+ void doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,\r
+ std::vector< Def > & dc, int index,\r
+ std::vector< Node > & cond, std::vector<Node> & val );\r
+ int isCompat( std::vector< Node > & cond, Node c );\r
+ bool doMeet( std::vector< Node > & cond, Node c );\r
+ Node mkCond( std::vector< Node > & cond );\r
+ Node mkCondDefault( Node f );\r
+ void mkCondDefaultVec( Node f, std::vector< Node > & cond );\r
+ void mkCondVec( Node n, std::vector< Node > & cond );\r
+ Node evaluateInterpreted( Node n, std::vector< Node > & vals );\r
+public:\r
+ FullModelChecker( QuantifiersEngine* qe );\r
+ ~FullModelChecker(){}\r
+\r
+ int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }\r
+ bool isStar(Node n);\r
+ Node getStar(TypeNode tn) { return d_type_star[tn]; }\r
+ bool isModelBasisTerm(Node n);\r
+ Node getModelBasisTerm(TypeNode tn);\r
+ void reset(FirstOrderModel * fm);\r
+ Def * getModel(FirstOrderModel * fm, Node op);\r
+\r
+ void debugPrintCond(const char * tr, Node n, bool dispStar = false);\r
+ void debugPrint(const char * tr, Node n, bool dispStar = false);\r
+\r
+ int exhaustiveInstantiate(FirstOrderModel * fm, Node f, int effort);\r
+ bool hasStarExceptions( Node f ) { return !d_star_insts[f].empty(); }\r
+\r
+ bool isActive();\r
+ bool useSimpleModels();\r
+};\r
+\r
+}\r
+}\r
+}\r
+}\r
+\r
+#endif\r
}
}
+Node InstMatch::get( QuantifiersEngine* qe, Node f, int i ) {
+ return get( qe->getTermDatabase()->getInstantiationConstant( f, i ) );
+}
+
void InstMatch::set(TNode var, TNode n){
Assert( !var.isNull() );
- if( !n.isNull() &&// For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
- //var.getType() == n.getType()
- !n.getType().isSubtypeOf( var.getType() ) ){
- Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
- Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
- Assert(false);
+ if (Trace.isOn("inst-match-warn")) {
+ // For a strange use in inst_match.cpp InstMatchGeneratorSimple::addInstantiations
+ if( !n.isNull() && !n.getType().isSubtypeOf( var.getType() ) ){
+ Trace("inst-match-warn") << var.getAttribute(InstConstantAttribute()) << std::endl;
+ Trace("inst-match-warn") << var << " " << var.getType() << " " << n << " " << n.getType() << std::endl ;
+ }
}
+ Assert( n.isNull() || n.getType().isSubtypeOf( var.getType() ) );
d_map[var] = n;
}
+void InstMatch::set( QuantifiersEngine* qe, Node f, int i, TNode n ) {
+ set( qe->getTermDatabase()->getInstantiationConstant( f, i ), n );
+}
+
/** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
void erase(Node node){ d_map.erase(node); }
/** get */
Node get( TNode var ) { return d_map[var]; }
+ Node get( QuantifiersEngine* qe, Node f, int i );
/** set */
void set(TNode var, TNode n);
+ void set( QuantifiersEngine* qe, Node f, int i, TNode n );
+ /** size */
size_t size(){ return d_map.size(); }
/* iterator */
std::map< Node, Node >::iterator begin(){ return d_map.begin(); };
//we want to add the children of the NOT
d_match_pattern = d_pattern[0];
}
- if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){
- if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){
+ if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
+ if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ||
+ d_match_pattern[0].getKind()==INST_CONSTANT ){
Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );
+ Node mp = d_match_pattern[1];
//swap sides
Node pat = d_pattern;
- d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );
- d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern;
- if( pat.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching
- d_match_pattern = d_match_pattern[1];
+ if(d_match_pattern.getKind()==GEQ){
+ d_pattern = NodeManager::currentNM()->mkNode( kind::GT, d_match_pattern[1], d_match_pattern[0] );
+ d_pattern = d_pattern.negate();
}else{
- d_match_pattern = d_pattern[0][0];
+ d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );
}
- }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){
+ d_pattern = pat.getKind()==NOT ? d_pattern.negate() : d_pattern;
+ d_match_pattern = mp;
+ }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ||
+ d_match_pattern[1].getKind()==INST_CONSTANT ){
Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );
if( d_pattern.getKind()!=NOT ){ //TEMPORARY until we do better implementation of disequality matching
d_match_pattern = d_match_pattern[0];
+ }else if( d_match_pattern[1].getKind()==INST_CONSTANT ){
+ d_match_pattern = d_match_pattern[0];
}
}
}
//candidates will be all disequalities
d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
}
- }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){
+ }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF ||
+ d_pattern.getKind()==GEQ || d_pattern.getKind()==GT || d_pattern.getKind()==NOT ){
Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
if( d_pattern.getKind()==NOT ){
- Unimplemented("Disequal generator unimplemented");
+ if (d_pattern[0][1].getKind()!=INST_CONSTANT) {
+ Unimplemented("Disequal generator unimplemented");
+ }else{
+ d_eq_class = d_pattern[0][1];
+ }
}else{
- Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
- //we are matching only in a particular equivalence class
- d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
//store the equivalence class that we will call d_cg->reset( ... ) on
d_eq_class = d_pattern[1];
}
+ Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
+ //we are matching only in a particular equivalence class
+ d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
+
}else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
//if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){
//Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;
/** get match (not modulo equality) */
bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngine* qe ){
Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
- << m << ")" << ", " << d_children.size() << std::endl;
+ << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
Assert( !d_match_pattern.isNull() );
if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){
return true;
}
}
}
+ //for relational matching
+ if( !d_eq_class.isNull() && d_eq_class.getKind()==INST_CONSTANT ){
+ //also must fit match to equivalence class
+ bool pol = d_pattern.getKind()!=NOT;
+ Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern;
+ Node t_match;
+ if( pol ){
+ if (pat.getKind()==GT) {
+ Node r = NodeManager::currentNM()->mkConst( Rational(-1) );
+ t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
+ }else{
+ t_match = t;
+ }
+ }else{
+ if(pat.getKind()==EQUAL) {
+ Node r = NodeManager::currentNM()->mkConst( Rational(1) );
+ t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
+ }else if( pat.getKind()==IFF ){
+ t_match = NodeManager::currentNM()->mkConst( !q->areEqual( NodeManager::currentNM()->mkConst(true), t ) );
+ }else if( pat.getKind()==GEQ ){
+ Node r = NodeManager::currentNM()->mkConst( Rational(1) );
+ t_match = NodeManager::currentNM()->mkNode(PLUS, t, r);
+ }else if( pat.getKind()==GT ){
+ t_match = t;
+ }
+ }
+ if( !t_match.isNull() && !m.setMatch( q, d_eq_class, t_match ) ){
+ success = false;
+ }
+ }
if( success ){
//now, fit children into match
//we will be requesting candidates for matching terms for each child
//we have a specific equivalence class in mind
//we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
//just look in equivalence class of the RHS
- d_cg->reset( d_eq_class );
+ d_cg->reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class );
}
bool InstMatchGenerator::getNextMatch( Node f, InstMatch& m, QuantifiersEngine* qe ){
if( !success ){
//Debug("matching") << this << " failed, reset " << d_eq_class << std::endl;
//we failed, must reset
- reset( d_eq_class, qe );
+ reset( d_eq_class.getKind()==INST_CONSTANT ? Node::null() : d_eq_class, qe );
}
return success;
}
}
if( gen ){
generateTriggers( f, effort, e, status );
+ if( d_auto_gen_trigger[f].empty() && f.getNumChildren()==2 ){
+ Trace("no-trigger") << "Could not find trigger for " << f << std::endl;
+ }
}
+
//if( e==4 ){
// d_processed_trigger.clear();
// d_quantEngine->getEqualityQuery()->setLiberal( true );
Trace("model-engine-debug") << "Building model..." << std::endl;
//build model for UF
for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+ Trace("model-engine-debug-uf") << "Building model for " << it->first << "..." << std::endl;
constructModelUf( fm, it->first );
}
/*
}
}
//for calculating terms that we don't need to consider
- if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
+ if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())!=0 ){
if( !n.getAttribute(BasisNoMatchAttribute()) ){
//need to consider if it is not congruent modulo model basis
if( !tabt.addTerm( fm, n ) ){
bool ModelEngineBuilder::isTermActive( Node n ){
return !n.getAttribute(NoMatchAttribute()) || //it is not congruent to another active term
- ( n.getAttribute(ModelBasisArgAttribute())==1 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments
+ ( n.getAttribute(ModelBasisArgAttribute())!=0 && !n.getAttribute(BasisNoMatchAttribute()) ); //or it has model basis arguments
//and is not congruent modulo model basis
//to another active term
}
fm->d_uf_model_gen[op].setValue( fm, n, v );
if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){
//also set as default value if necessary
- if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){
+ if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){
Trace("fmf-model-cons") << " Set as default." << std::endl;
fm->d_uf_model_gen[op].setValue( fm, n, v, false );
if( n==defaultTerm ){
Trace("fmf-model-cons") << " Choose default value..." << std::endl;
//chose defaultVal based on heuristic, currently the best ratio of "pro" responses
Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
+ if( defaultVal.isNull() ){
+ if (!fm->d_rep_set.hasType(defaultTerm.getType())) {
+ Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(defaultTerm.getType());
+ fm->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt);
+ }
+ defaultVal = fm->d_rep_set.d_type_reps[defaultTerm.getType()][0];
+ }
Assert( !defaultVal.isNull() );
Trace("fmf-model-cons") << "Set default term : " << fm->d_rep_set.getIndexFor( defaultVal ) << std::endl;
fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false );
if( s.getKind()==APPLY_UF ){
Assert( s.hasAttribute(ModelBasisArgAttribute()) );
if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl;
- if( s.getAttribute(ModelBasisArgAttribute())==1 ){
+ if( s.getAttribute(ModelBasisArgAttribute())!=0 ){
d_term_selected[ s ] = true;
Trace("sel-form-term") << " " << s << " is a selected term." << std::endl;
}
//Model Engine constructor
ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) :
QuantifiersModule( qe ),
-d_rel_domain( qe, qe->getModel() ){
+d_rel_domain( qe, qe->getModel() ),
+d_fmc( qe ){
if( options::fmfNewInstGen() ){
d_builder = new ModelEngineBuilderInstGen( c, qe );
//let the strong solver verify that the model is minimal
//for debugging, this will if there are terms in the model that the strong solver was not notified of
((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->debugModel( fm );
+ //for full model checking
+ if( d_fmc.isActive() ){
+ Trace("model-engine-debug") << "Reset full model checker..." << std::endl;
+ d_fmc.reset( fm );
+ }
Trace("model-engine-debug") << "Check model..." << std::endl;
d_incomplete_check = false;
//print debug
if( it->first.isSort() ){
Trace("model-engine") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
Trace("model-engine-debug") << " ";
+ Node mbt = d_quantEngine->getTermDatabase()->getModelBasisTerm(it->first);
for( size_t i=0; i<it->second.size(); i++ ){
//Trace("model-engine-debug") << it->second[i] << " ";
Node r = ((EqualityQueryQuantifiersEngine*)d_quantEngine->getEqualityQuery())->getRepresentative( it->second[i] );
Trace("model-engine-debug") << r << " ";
}
Trace("model-engine-debug") << std::endl;
+ Trace("model-engine-debug") << " Model basis term : " << mbt << std::endl;
}
}
}
+ //full model checking: construct models for all functions
+ if( d_fmc.isActive() ){
+ for (std::map< Node, uf::UfModelTreeGenerator >::iterator it = fm->d_uf_model_gen.begin(); it != fm->d_uf_model_gen.end(); ++it) {
+ d_fmc.getModel(fm, it->first);
+ }
+ }
//compute the relevant domain if necessary
if( optUseRelevantDomain() ){
d_rel_domain.compute();
d_relevantLemmas = 0;
d_totalLemmas = 0;
Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl;
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- //keep track of total instantiations for statistics
- int totalInst = 1;
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- TypeNode tn = f[0][i].getType();
- if( fm->d_rep_set.hasType( tn ) ){
- totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
- }
- }
- d_totalLemmas += totalInst;
- //determine if we should check this quantifiers
- bool checkQuant = false;
- if( checkOption==check_model_full ){
- checkQuant = d_builder->isQuantifierActive( f );
- }else if( checkOption==check_model_no_inst_gen ){
- checkQuant = !d_builder->hasInstGen( f );
- }
- //if we need to consider this quantifier on this iteration
- if( checkQuant ){
- addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain() );
- if( Trace.isOn("model-engine-warn") ){
- if( addedLemmas>10000 ){
- Debug("fmf-exit") << std::endl;
- debugPrint("fmf-exit");
- exit( 0 );
+ int e_max = d_fmc.isActive() ? 2 : 1;
+ for( int e=0; e<e_max; e++) {
+ if (addedLemmas==0) {
+ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ //keep track of total instantiations for statistics
+ int totalInst = 1;
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ TypeNode tn = f[0][i].getType();
+ if( fm->d_rep_set.hasType( tn ) ){
+ totalInst = totalInst * (int)fm->d_rep_set.d_type_reps[ tn ].size();
+ }
+ }
+ d_totalLemmas += totalInst;
+ //determine if we should check this quantifiers
+ bool checkQuant = false;
+ if( checkOption==check_model_full ){
+ checkQuant = d_builder->isQuantifierActive( f );
+ }else if( checkOption==check_model_no_inst_gen ){
+ checkQuant = !d_builder->hasInstGen( f );
+ }
+ //if we need to consider this quantifier on this iteration
+ if( checkQuant ){
+ addedLemmas += exhaustiveInstantiate( f, optUseRelevantDomain(), e );
+ if( Trace.isOn("model-engine-warn") ){
+ if( addedLemmas>10000 ){
+ Debug("fmf-exit") << std::endl;
+ debugPrint("fmf-exit");
+ exit( 0 );
+ }
+ }
+ if( optOneQuantPerRound() && addedLemmas>0 ){
+ break;
+ }
}
- }
- if( optOneQuantPerRound() && addedLemmas>0 ){
- break;
}
}
}
return addedLemmas;
}
-int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
+int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain, int effort ){
int addedLemmas = 0;
- Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << "..." << std::endl;
- Debug("inst-fmf-ei") << " Instantiation Constants: ";
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
- }
- Debug("inst-fmf-ei") << std::endl;
- //create a rep set iterator and iterate over the (relevant) domain of the quantifier
- RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
- if( riter.setQuantifier( f ) ){
- //set the domain for the iterator (the sufficient set of instantiations to try)
- if( useRelInstDomain ){
- riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
+ bool useModel = d_builder->optUseModel();
+ if (d_fmc.isActive() && effort==0) {
+ addedLemmas = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort);
+ }else if( !d_fmc.isActive() || (effort==1 && d_fmc.hasStarExceptions(f)) ) {
+ if(d_fmc.isActive()){
+ useModel = false;
+ int lem = d_fmc.exhaustiveInstantiate(d_quantEngine->getModel(), f, effort);
+ if( lem!=-1 ){
+ return lem;
+ }
}
- d_quantEngine->getModel()->resetEvaluate();
- int tests = 0;
- int triedLemmas = 0;
- while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
- d_testLemmas++;
- int eval = 0;
- int depIndex;
- if( d_builder->optUseModel() ){
- //see if instantiation is already true in current model
- Debug("fmf-model-eval") << "Evaluating ";
- riter.debugPrintSmall("fmf-model-eval");
- Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
- tests++;
- //if evaluate(...)==1, then the instantiation is already true in the model
- // depIndex is the index of the least significant variable that this evaluation relies upon
- depIndex = riter.getNumTerms()-1;
- eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
- if( eval==1 ){
- Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
- }else{
- Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
- }
+ Trace("inst-fmf-ei") << "Exhaustive instantiate " << f << ", effort = " << effort << "..." << std::endl;
+ Debug("inst-fmf-ei") << " Instantiation Constants: ";
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ Debug("inst-fmf-ei") << d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i ) << " ";
+ }
+ Debug("inst-fmf-ei") << std::endl;
+ //create a rep set iterator and iterate over the (relevant) domain of the quantifier
+ RepSetIterator riter( &(d_quantEngine->getModel()->d_rep_set) );
+ if( riter.setQuantifier( f ) ){
+ Debug("inst-fmf-ei") << "Set domain..." << std::endl;
+ //set the domain for the iterator (the sufficient set of instantiations to try)
+ if( useRelInstDomain ){
+ riter.setDomain( d_rel_domain.d_quant_inst_domain[f] );
}
- if( eval==1 ){
- //instantiation is already true -> skip
- riter.increment2( depIndex );
- }else{
- //instantiation was not shown to be true, construct the match
- InstMatch m;
- for( int i=0; i<riter.getNumTerms(); i++ ){
- m.set( d_quantEngine->getTermDatabase()->getInstantiationConstant( f, riter.d_index_order[i] ), riter.getTerm( i ) );
+ Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl;
+ d_quantEngine->getModel()->resetEvaluate();
+ Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl;
+ int tests = 0;
+ int triedLemmas = 0;
+ while( !riter.isFinished() && ( addedLemmas==0 || !optOneInstPerQuantRound() ) ){
+ d_testLemmas++;
+ int eval = 0;
+ int depIndex;
+ if( useModel ){
+ //see if instantiation is already true in current model
+ Debug("fmf-model-eval") << "Evaluating ";
+ riter.debugPrintSmall("fmf-model-eval");
+ Debug("fmf-model-eval") << "Done calculating terms." << std::endl;
+ tests++;
+ //if evaluate(...)==1, then the instantiation is already true in the model
+ // depIndex is the index of the least significant variable that this evaluation relies upon
+ depIndex = riter.getNumTerms()-1;
+ eval = d_quantEngine->getModel()->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter );
+ if( eval==1 ){
+ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl;
+ }else{
+ Debug("fmf-model-eval") << " Returned " << (eval==-1 ? "failure" : "unknown") << ", depIndex = " << depIndex << std::endl;
+ }
}
- Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
- triedLemmas++;
- d_triedLemmas++;
- //add as instantiation
- if( d_quantEngine->addInstantiation( f, m ) ){
- addedLemmas++;
- //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
- if( eval==-1 && optExhInstEvalSkipMultiple() ){
- riter.increment2( depIndex );
+ if( eval==1 ){
+ //instantiation is already true -> skip
+ riter.increment2( depIndex );
+ }else{
+ //instantiation was not shown to be true, construct the match
+ InstMatch m;
+ for( int i=0; i<riter.getNumTerms(); i++ ){
+ m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
+ }
+ Debug("fmf-model-eval") << "* Add instantiation " << m << std::endl;
+ triedLemmas++;
+ d_triedLemmas++;
+ //add as instantiation
+ if( d_quantEngine->addInstantiation( f, m ) ){
+ addedLemmas++;
+ //if the instantiation is show to be false, and we wish to skip multiple instantiations at once
+ if( eval==-1 && optExhInstEvalSkipMultiple() ){
+ riter.increment2( depIndex );
+ }else{
+ riter.increment();
+ }
}else{
+ Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
riter.increment();
}
- }else{
- Debug("fmf-model-eval") << "* Failed Add instantiation " << m << std::endl;
- riter.increment();
}
}
+ //print debugging information
+ d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas;
+ d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms;
+ d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits;
+ d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown;
+ int relevantInst = 1;
+ for( size_t i=0; i<f[0].getNumChildren(); i++ ){
+ relevantInst = relevantInst * (int)riter.d_domain[i].size();
+ }
+ d_relevantLemmas += relevantInst;
+ Trace("inst-fmf-ei") << "Finished: " << std::endl;
+ //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl;
+ Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl;
+ Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl;
+ Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl;
+ Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl;
+ if( addedLemmas>1000 ){
+ Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
+ //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl;
+ Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl;
+ Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl;
+ Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl;
+ Trace("model-engine-warn") << " # Tests: " << tests << std::endl;
+ Trace("model-engine-warn") << std::endl;
+ }
}
- //print debugging information
- d_statistics.d_eval_formulas += d_quantEngine->getModel()->d_eval_formulas;
- d_statistics.d_eval_uf_terms += d_quantEngine->getModel()->d_eval_uf_terms;
- d_statistics.d_eval_lits += d_quantEngine->getModel()->d_eval_lits;
- d_statistics.d_eval_lits_unknown += d_quantEngine->getModel()->d_eval_lits_unknown;
- int relevantInst = 1;
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- relevantInst = relevantInst * (int)riter.d_domain[i].size();
- }
- d_relevantLemmas += relevantInst;
- Trace("inst-fmf-ei") << "Finished: " << std::endl;
- //Debug("inst-fmf-ei") << " Inst Total: " << totalInst << std::endl;
- Trace("inst-fmf-ei") << " Inst Relevant: " << relevantInst << std::endl;
- Trace("inst-fmf-ei") << " Inst Tried: " << triedLemmas << std::endl;
- Trace("inst-fmf-ei") << " Inst Added: " << addedLemmas << std::endl;
- Trace("inst-fmf-ei") << " # Tests: " << tests << std::endl;
- if( addedLemmas>1000 ){
- Trace("model-engine-warn") << "WARNING: many instantiations produced for " << f << ": " << std::endl;
- //Trace("model-engine-warn") << " Inst Total: " << totalInst << std::endl;
- Trace("model-engine-warn") << " Inst Relevant: " << relevantInst << std::endl;
- Trace("model-engine-warn") << " Inst Tried: " << triedLemmas << std::endl;
- Trace("model-engine-warn") << " Inst Added: " << addedLemmas << std::endl;
- Trace("model-engine-warn") << " # Tests: " << tests << std::endl;
- Trace("model-engine-warn") << std::endl;
- }
+ //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
+ d_incomplete_check = d_incomplete_check || riter.d_incomplete;
}
- //if the iterator is incomplete, we will return unknown instead of sat if no instantiations are added this round
- d_incomplete_check = d_incomplete_check || riter.d_incomplete;
return addedLemmas;
}
#include "theory/quantifiers/model_builder.h"
#include "theory/model.h"
#include "theory/quantifiers/relevant_domain.h"
+#include "theory/quantifiers/full_model_check.h"
namespace CVC4 {
namespace theory {
private: //analysis of current model:
//relevant domain
RelevantDomain d_rel_domain;
+ //full model checker
+ fmcheck::FullModelChecker d_fmc;
//is the exhaustive instantiation incomplete?
bool d_incomplete_check;
private:
//check model
int checkModel( int checkOption );
//exhaustively instantiate quantifier (possibly using mbqi), return number of lemmas produced
- int exhaustiveInstantiate( Node f, bool useRelInstDomain = false );
+ int exhaustiveInstantiate( Node f, bool useRelInstDomain = false, int effort = 0 );
private:
//temporary statistics
int d_triedLemmas;
~ModelEngine(){}
//get the builder
ModelEngineBuilder* getModelBuilder() { return d_builder; }
+ fmcheck::FullModelChecker* getFullModelChecker() { return &d_fmc; }
public:
void check( Theory::Effort e );
void registerQuantifier( Node f );
# Whether to use relevent triggers
option relevantTriggers /--disable-relevant-triggers bool :default true
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)
# Whether to consider terms in the bodies of quantifiers for matching
option registerQuantBodyTerms --register-quant-body-terms bool :default false
option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
disable model-based quantifier instantiation for finite model finding
+option fmfFullModelCheck --fmf-fmc bool :default false
+ enable full model check for finite model finding
+option fmfFullModelCheckSimple /--disable-fmf-fmc-simple bool :default true
+ disable simple models in full model check for finite model finding
+
option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false
only add one instantiation per quantifier per round for fmf
option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false
use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
option fmfNewInstGen --fmf-new-inst-gen bool :default false
use new inst gen technique for answering sat without exhaustive instantiation
-option fmfInstGen /--disable-fmf-inst-gen bool :default true
- disable Inst-Gen instantiation techniques for finite model finding
+option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true
+ enable/disable Inst-Gen instantiation techniques for finite model finding
option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
only perform Inst-Gen instantiation techniques on one quantifier per round
option fmfFreshDistConst --fmf-fresh-dc bool :default false
using namespace CVC4::context;
using namespace CVC4::theory;
+
+bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) {
+ if ( n.getKind()==MULT ){
+ if( n.getNumChildren()==2 && msum.find(n[1])==msum.end() && n[0].isConst() ){
+ msum[n[1]] = n[0];
+ return true;
+ }
+ }else{
+ if( msum.find(n)==msum.end() ){
+ msum[n] = Node::null();
+ return true;
+ }
+ }
+ return false;
+}
+
+bool QuantArith::getMonomialSum( Node n, std::map< Node, Node >& msum ) {
+ if ( n.getKind()==PLUS ){
+ for( unsigned i=0; i<n.getNumChildren(); i++) {
+ if (!getMonomial( n[i], msum )){
+ return false;
+ }
+ }
+ return true;
+ }else{
+ return getMonomial( n, msum );
+ }
+}
+
+bool QuantArith::getMonomialSumLit( Node lit, std::map< Node, Node >& msum ) {
+ if( lit.getKind()==GEQ || lit.getKind()==EQUAL ){
+ if( getMonomialSum( lit[0], msum ) ){
+ if( lit[1].isConst() ){
+ if( !lit[1].getConst<Rational>().isZero() ){
+ msum[Node::null()] = negate( lit[1] );
+ }
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k ) {
+ if( msum.find(v)!=msum.end() ){
+ std::vector< Node > children;
+ Rational r = msum[v].isNull() ? Rational(1) : msum[v].getConst<Rational>();
+ if ( r.sgn()!=0 ){
+ for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
+ if( it->first!=v ){
+ Node m;
+ if( !it->first.isNull() ){
+ if ( !it->second.isNull() ){
+ m = NodeManager::currentNM()->mkNode( MULT, it->second, it->first );
+ }else{
+ m = it->first;
+ }
+ }else{
+ m = it->second;
+ }
+ children.push_back(m);
+ }
+ }
+ veq = children.size()>1 ? NodeManager::currentNM()->mkNode( PLUS, children ) :
+ (children.size()==1 ? children[0] : NodeManager::currentNM()->mkConst( Rational(0) ));
+ if( !r.isNegativeOne() ){
+ if( r.isOne() ){
+ veq = negate(veq);
+ }else{
+ //TODO
+ return false;
+ }
+ }
+ veq = Rewriter::rewrite( veq );
+ veq = NodeManager::currentNM()->mkNode( k, r.sgn()==1 ? v : veq, r.sgn()==1 ? veq : v );
+ return true;
+ }
+ return false;
+ }else{
+ return false;
+ }
+}
+
+Node QuantArith::negate( Node t ) {
+ Node tt = NodeManager::currentNM()->mkNode( MULT, NodeManager::currentNM()->mkConst( Rational(-1) ), t );
+ tt = Rewriter::rewrite( tt );
+ return tt;
+}
+
+
void QuantRelevance::registerQuantifier( Node f ){
//compute symbols in f
std::vector< Node > syms;
namespace theory {
+class QuantArith
+{
+public:
+ static bool getMonomial( Node n, std::map< Node, Node >& msum );
+ static bool getMonomialSum( Node n, std::map< Node, Node >& msum );
+ static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum );
+ static bool isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind k );
+ static Node negate( Node t );
+};
+
+
class QuantRelevance
{
private:
//determine if it has model basis attribute
for( int j=0; j<(int)n.getNumChildren(); j++ ){
if( n[j].getAttribute(ModelBasisAttribute()) ){
- val = 1;
- break;
+ val++;
}
}
ModelBasisArgAttribute mbaa;
};/* class TermArgTrie */
+namespace fmcheck {
+ class FullModelChecker;
+}
+
class TermDb {
friend class ::CVC4::theory::QuantifiersEngine;
friend class ::CVC4::theory::inst::Trigger;
friend class ::CVC4::theory::rrinst::Trigger;
+ friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker;
private:
/** reference to the quantifiers engine */
QuantifiersEngine* d_quantEngine;
using namespace CVC4::theory;
using namespace CVC4::theory::inst;
-//#define NESTED_PATTERN_SELECTION
-
/** trigger class constructor */
Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes, int matchOption, bool smartTriggers ) :
d_quantEngine( qe ), d_f( f ){
}
}
-bool Trigger::isUsableTrigger( Node n, Node f ){
- //return n.getAttribute(InstConstantAttribute())==f && n.getKind()==APPLY_UF;
+bool nodeContainsVar( Node n, Node v ){
+ if( n==v) {
+ return true;
+ }else{
+ for( unsigned i=0; i<n.getNumChildren(); i++) {
+ if( nodeContainsVar(n[i], v) ){
+ return true;
+ }
+ }
+ return false;
+ }
+}
+
+Node Trigger::getIsUsableTrigger( Node n, Node f, bool pol, bool hasPol ) {
+ if( options::relationalTriggers() ){
+ if( n.getKind()==EQUAL || n.getKind()==IFF || n.getKind()==GEQ ){
+ Node rtr;
+ for( unsigned i=0; i<2; i++) {
+ unsigned j = (i==0) ? 1 : 0;
+ if( n[j].getKind()==INST_CONSTANT && isUsableTrigger(n[i], f) && !nodeContainsVar( n[i], n[j] ) ) {
+ rtr = n;
+ break;
+ }
+ }
+ if( n[0].getType().isInteger() ){
+ //try to rearrange?
+ std::map< Node, Node > m;
+ if (QuantArith::getMonomialSumLit(n, m) ){
+ for( std::map< Node, Node >::iterator it = m.begin(); it!=m.end(); ++it ){
+ if( !it->first.isNull() && it->first.getKind()==INST_CONSTANT ){
+ Node veq;
+ if( QuantArith::isolate( it->first, m, veq, n.getKind() ) ){
+ int vti = veq[0]==it->first ? 1 : 0;
+ if( isUsableTrigger(veq[vti], f) && !nodeContainsVar( veq[vti], veq[vti==0 ? 1 : 0]) ){
+ rtr = veq;
+ InstConstantAttribute ica;
+ rtr.setAttribute(ica,veq[vti].getAttribute(InstConstantAttribute()) );
+ }
+ }
+ }
+ }
+ }
+ }
+ if( !rtr.isNull() ){
+ Trace("relational-trigger") << "Relational trigger : " << std::endl;
+ Trace("relational-trigger") << " " << rtr << " (from " << n << ")" << std::endl;
+ Trace("relational-trigger") << " in quantifier " << f << std::endl;
+ if( hasPol ){
+ Trace("relational-trigger") << " polarity : " << pol << std::endl;
+ }
+ Node rtr2 = (hasPol && pol) ? rtr.negate() : rtr;
+ InstConstantAttribute ica;
+ rtr2.setAttribute(ica,rtr.getAttribute(InstConstantAttribute()) );
+ return rtr2;
+ }
+ }
+ }
bool usable = n.getAttribute(InstConstantAttribute())==f && isAtomicTrigger( n ) && isUsable( n, f );
Trace("usable") << n << " usable : " << usable << std::endl;
- return usable;
+ if( usable ){
+ return n;
+ }else{
+ return Node::null();
+ }
+}
+
+bool Trigger::isUsableTrigger( Node n, Node f ){
+ Node nu = getIsUsableTrigger(n,f);
+ return !nu.isNull();
}
bool Trigger::isAtomicTrigger( Node n ){
}
-bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt ){
+bool Trigger::collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol ){
if( patMap.find( n )==patMap.end() ){
patMap[ n ] = false;
+ bool newHasPol = (n.getKind()==IFF || n.getKind()==XOR) ? false : hasPol;
+ bool newPol = n.getKind()==NOT ? !pol : pol;
if( tstrt==TS_MIN_TRIGGER ){
if( n.getKind()==FORALL ){
-#ifdef NESTED_PATTERN_SELECTION
- //return collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt );
- return collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt );
-#else
return false;
-#endif
}else{
bool retVal = false;
for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
+ bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol;
+ bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
+ if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){
retVal = true;
}
}
if( retVal ){
return true;
- }else if( isUsableTrigger( n, f ) ){
- patMap[ n ] = true;
- return true;
}else{
- return false;
+ Node nu = getIsUsableTrigger( n, f, pol, hasPol );
+ if( !nu.isNull() ){
+ patMap[ nu ] = true;
+ return true;
+ }else{
+ return false;
+ }
}
}
}else{
bool retVal = false;
- if( isUsableTrigger( n, f ) ){
- patMap[ n ] = true;
+ Node nu = getIsUsableTrigger( n, f, pol, hasPol );
+ if( !nu.isNull() ){
+ patMap[ nu ] = true;
if( tstrt==TS_MAX_TRIGGER ){
return true;
}else{
retVal = true;
}
}
- if( n.getKind()==FORALL ){
-#ifdef NESTED_PATTERN_SELECTION
- //if( collectPatTerms2( qe, f, qe->getOrCreateCounterexampleBody( n ), patMap, tstrt ) ){
- // retVal = true;
- //}
- if( collectPatTerms2( qe, f, qe->getBoundBody( n ), patMap, tstrt ) ){
- retVal = true;
- }
-#endif
- }else{
+ if( n.getKind()!=FORALL ){
for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( collectPatTerms2( qe, f, n[i], patMap, tstrt ) ){
+ bool newPol2 = (n.getKind()==IMPLIES && i==0) ? !newPol : newPol;
+ bool newHasPol2 = (n.getKind()==ITE && i==0) ? false : newHasPol;
+ if( collectPatTerms2( qe, f, n[i], patMap, tstrt, newPol2, newHasPol2 ) ){
retVal = true;
}
}
}
}
}
- collectPatTerms2( qe, f, n, patMap, tstrt );
+ collectPatTerms2( qe, f, n, patMap, tstrt, true, true );
for( std::map< Node, bool >::iterator it = patMap.begin(); it != patMap.end(); ++it ){
if( it->second ){
patTerms.push_back( it->first );
private:
/** is subterm of trigger usable */
static bool isUsable( Node n, Node f );
+ static Node getIsUsableTrigger( Node n, Node f, bool pol = true, bool hasPol = false );
/** collect all APPLY_UF pattern terms for f in n */
- static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt );
+ static bool collectPatTerms2( QuantifiersEngine* qe, Node f, Node n, std::map< Node, bool >& patMap, int tstrt, bool pol, bool hasPol );
public:
//different strategies for choosing trigger terms
enum {
#include "theory/quantifiers/trigger.h"
#include "theory/rewriterules/efficient_e_matching.h"
#include "theory/rewriterules/rr_trigger.h"
+#include "theory/quantifiers/bounded_integers.h"
using namespace std;
using namespace CVC4;
if( options::finiteModelFind() ){
d_model_engine = new quantifiers::ModelEngine( c, this );
d_modules.push_back( d_model_engine );
+
+ d_bint = new quantifiers::BoundedIntegers( this );
+ d_modules.push_back( d_bint );
}else{
d_model_engine = NULL;
+ d_bint = NULL;
}
//options
virtual void assertNode( Node n ) = 0;
virtual void propagate( Theory::Effort level ){}
virtual Node getNextDecisionRequest() { return TNode::null(); }
- virtual Node explain(TNode n) = 0;
+ virtual Node explain(TNode n) { return TNode::null(); }
};/* class QuantifiersModule */
namespace quantifiers {
class ModelEngine;
class TermDb;
class FirstOrderModel;
+ class BoundedIntegers;
}/* CVC4::theory::quantifiers */
namespace inst {
std::map< Node, QuantPhaseReq* > d_phase_reqs;
/** efficient e-matcher */
EfficientEMatcher* d_eem;
+ /** bounded integers utility */
+ quantifiers::BoundedIntegers * d_bint;
private:
/** list of all quantifiers seen */
std::vector< Node > d_quants;
always use simple clique lemmas for uf strong solver
option ufssDiseqPropagation --uf-ss-deq-prop bool :default false
eagerly propagate disequalities for uf strong solver
+option ufssMinimalModel /--disable-uf-ss-min-model bool :default true
+ disable finding a minimal model in uf strong solver
endmodule
#include "theory/uf/equality_engine.h"
#include "theory/uf/theory_uf.h"
#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers/options.h"
#define RECONSIDER_FUNC_DEFAULT_VALUE
#define USE_PARTIAL_DEFAULT_VALUES
if( !ground ){
int defSize = (int)d_defaults.size();
for( int i=0; i<defSize; i++ ){
- bool isGround;
//for soundness, to allow variable order-independent function interpretations,
// we must ensure that the intersection of all default terms
// is also defined.
//for example, if we have that f( e, a ) = ..., and f( b, e ) = ...,
// then we must define f( b, a ).
- Node ni = getIntersection( m, n, d_defaults[i], isGround );
- if( !ni.isNull() ){
- //if the intersection exists, and is not already defined
- if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
- d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
- //use the current value
- setValue( m, ni, v, isGround, false );
+ if (!options::fmfFullModelCheck()) {
+ bool isGround;
+ Node ni = getIntersection( m, n, d_defaults[i], isGround );
+ if( !ni.isNull() ){
+ //if the intersection exists, and is not already defined
+ if( d_set_values[0][ isGround ? 1 : 0 ].find( ni )==d_set_values[0][ isGround ? 1 : 0 ].end() &&
+ d_set_values[1][ isGround ? 1 : 0 ].find( ni )==d_set_values[1][ isGround ? 1 : 0 ].end() ){
+ //use the current value
+ setValue( m, ni, v, isGround, false );
+ }
}
}
}
static Node toIte( TypeNode type, Node fm_node, const char* argPrefix );
};
+
class UfModelTreeGenerator
{
-private:
+public:
//store for set values
Node d_default_value;
std::map< Node, Node > d_set_values[2][2];
if( d_regions[i]->d_valid ){
std::vector< Node > clique;
if( d_regions[i]->check( level, d_cardinality, clique ) ){
- //add clique lemma
- addCliqueLemma( clique, out );
- return;
+ if( options::ufssMinimalModel() ){
+ //add clique lemma
+ addCliqueLemma( clique, out );
+ return;
+ }
}else{
Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
}
//naive strategy, force region combination involving the first valid region
for( int i=0; i<(int)d_regions_index; i++ ){
if( d_regions[i]->d_valid ){
- forceCombineRegion( i, false );
- recheck = true;
- break;
+ int fcr = forceCombineRegion( i, false );
+ Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl;
+ if( options::ufssMinimalModel() || fcr!=-1 ){
+ recheck = true;
+ break;
+ }
}
}
}
if( recheck ){
+ Trace("uf-ss-debug") << "Must recheck." << std::endl;
check( level, out );
}
}
//now check if region is in conflict
std::vector< Node > clique;
if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
- //explain clique
- addCliqueLemma( clique, &d_thss->getOutputChannel() );
+ if( options::ufssMinimalModel() ){
+ //explain clique
+ addCliqueLemma( clique, &d_thss->getOutputChannel() );
+ }
}
}
}
}
bool StrongSolverTheoryUF::SortModel::addSplit( Region* r, OutputChannel* out ){
+ Node s;
if( r->hasSplits() ){
- Node s;
if( !options::ufssSmartSplits() ){
//take the first split you find
for( NodeBoolMap::iterator it = r->d_splits.begin(); it != r->d_splits.end(); ++it ){
}
}
}
+ Assert( s!=Node::null() );
+ }else{
+ if( !options::ufssMinimalModel() ){
+ //since candidate clique is not reported, we may need to find splits manually
+ for ( std::map< Node, Region::RegionNodeInfo* >::iterator it = r->d_nodes.begin(); it != r->d_nodes.end(); ++it ){
+ if ( it->second->d_valid ){
+ for ( std::map< Node, Region::RegionNodeInfo* >::iterator it2 = r->d_nodes.begin(); it2 != r->d_nodes.end(); ++it2 ){
+ if ( it->second!=it2->second && it2->second->d_valid ){
+ if( !r->isDisequal( it->first, it2->first, 1 ) ){
+ s = NodeManager::currentNM()->mkNode( EQUAL, it->first, it2->first );
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ if (!s.isNull() ){
//add lemma to output channel
- Assert( s!=Node::null() && s.getKind()==EQUAL );
+ Assert( s.getKind()==EQUAL );
s = Rewriter::rewrite( s );
Trace("uf-ss-lemma") << "*** Split on " << s << std::endl;
if( options::sortInference()) {
projects / cvc5.git / commitdiff