diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 243 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 73 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 13 | ||||
-rw-r--r-- | src/theory/quantifiers/full_model_check.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 1 | ||||
-rw-r--r-- | src/theory/quantifiers/modes.cpp | 23 | ||||
-rw-r--r-- | src/theory/quantifiers/modes.h | 16 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/options_handlers.h | 46 | ||||
-rwxr-xr-x | src/theory/quantifiers/qinterval_builder.cpp | 1111 | ||||
-rwxr-xr-x | src/theory/quantifiers/qinterval_builder.h | 155 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 10 |
14 files changed, 1654 insertions, 70 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index bda124e96..c94775aec 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -16,6 +16,8 @@ #include "theory/quantifiers/model_engine.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/qinterval_builder.h" #define USE_INDEX_ORDERING @@ -27,8 +29,9 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::quantifiers::fmcheck; -FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ), -d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){ +FirstOrderModel::FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ) : +TheoryModel( c, name, true ), +d_qe( qe ), d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){ } @@ -66,16 +69,23 @@ Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) { } void FirstOrderModel::initialize( bool considerAxioms ) { - processInitialize(); + processInitialize( true ); //this is called after representatives have been chosen and the equality engine has been built //for each quantifier, collect all operators we care about for( int i=0; i<getNumAssertedQuantifiers(); i++ ){ Node f = getAssertedQuantifier( i ); + processInitializeQuantifier( f ); + if( d_quant_var_id.find( f )==d_quant_var_id.end() ){ + for(unsigned i=0; i<f[0].getNumChildren(); i++){ + d_quant_var_id[f][f[0][i]] = i; + } + } if( considerAxioms || !f.hasAttribute(AxiomAttribute()) ){ //initialize relevant models within bodies of all quantifiers initializeModelForTerm( f[1] ); } } + processInitialize( false ); } void FirstOrderModel::initializeModelForTerm( Node n ){ @@ -85,14 +95,30 @@ void FirstOrderModel::initializeModelForTerm( Node n ){ } } -FirstOrderModelIG::FirstOrderModelIG(context::Context* c, std::string name) : FirstOrderModel(c,name) { +Node FirstOrderModel::getSomeDomainElement(TypeNode tn){ + //check if there is even any domain elements at all + if (!d_rep_set.hasType(tn)) { + Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; + Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); + d_rep_set.add(mbt); + }else if( d_rep_set.d_type_reps[tn].size()==0 ){ + Message() << "empty reps" << std::endl; + exit(0); + } + return d_rep_set.d_type_reps[tn][0]; +} + +FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) : +FirstOrderModel(qe, c,name) { } -void FirstOrderModelIG::processInitialize(){ - //rebuild models - d_uf_model_tree.clear(); - d_uf_model_gen.clear(); +void FirstOrderModelIG::processInitialize( bool ispre ){ + if( ispre ){ + //rebuild models + d_uf_model_tree.clear(); + d_uf_model_gen.clear(); + } } void FirstOrderModelIG::processInitializeModelForTerm( Node n ){ @@ -513,10 +539,8 @@ Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & ar - - FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) : -FirstOrderModel(c, name), d_qe(qe){ +FirstOrderModel(qe, c, name){ } @@ -552,19 +576,21 @@ Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & a return d_models[n.getOperator()]->evaluate(this, args); } -void FirstOrderModelFmc::processInitialize() { - if( options::fmfFmcInterval() && intervalOp.isNull() ){ - std::vector< TypeNode > types; - for(unsigned i=0; i<2; i++){ - types.push_back(NodeManager::currentNM()->integerType()); +void FirstOrderModelFmc::processInitialize( bool ispre ) { + if( ispre ){ + if( options::fmfFmcInterval() && 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" ); } - 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(); + for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){ + it->second->reset(); + } + d_model_basis_rep.clear(); } - d_model_basis_rep.clear(); } void FirstOrderModelFmc::processInitializeModelForTerm(Node n) { @@ -575,19 +601,6 @@ void FirstOrderModelFmc::processInitializeModelForTerm(Node n) { } } -Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){ - //check if there is even any domain elements at all - if (!d_rep_set.hasType(tn)) { - Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl; - Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn); - d_rep_set.d_type_reps[tn].push_back(mbt); - }else if( d_rep_set.d_type_reps[tn].size()==0 ){ - Message() << "empty reps" << std::endl; - exit(0); - } - return d_rep_set.d_type_reps[tn][0]; -} - bool FirstOrderModelFmc::isStar(Node n) { return n==getStar(n.getType()); @@ -684,3 +697,163 @@ bool FirstOrderModelFmc::isInRange( Node v, Node i ) { return v==i; } } + + +FirstOrderModelQInt::FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name) : +FirstOrderModel(qe, c, name) { + +} + +void FirstOrderModelQInt::processInitialize( bool ispre ) { + if( !ispre ){ + Trace("qint-debug") << "Process initialize" << std::endl; + for( std::map<Node, QIntDef * >::iterator it = d_models.begin(); it != d_models.end(); ++it ) { + Node op = it->first; + TypeNode tno = op.getType(); + Trace("qint-debug") << " Init " << op << " " << tno << std::endl; + for( unsigned i=0; i<tno.getNumChildren(); i++) { + //make sure a representative of the type exists + if( !d_rep_set.hasType( tno[i] ) ){ + Node e = getSomeDomainElement( tno[i] ); + Trace("qint-debug") << " * Initialize type " << tno[i] << ", add "; + Trace("qint-debug") << e << " " << e.getType() << std::endl; + //d_rep_set.add( e ); + } + } + } + } +} + +Node FirstOrderModelQInt::getFunctionValue(Node op, const char* argPrefix ) { + Trace("qint-debug") << "Get function value for " << op << std::endl; + TypeNode type = op.getType(); + std::vector< Node > vars; + for( size_t i=0; i<type.getNumChildren()-1; i++ ){ + std::stringstream ss; + ss << argPrefix << (i+1); + Node b = NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ); + vars.push_back( b ); + } + Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars); + Node curr = d_models[op]->getFunctionValue( this, vars ); + Node fv = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr); + Trace("qint-debug") << "Return " << fv << std::endl; + return fv; +} + +Node FirstOrderModelQInt::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { + Debug("qint-debug") << "get curr uf value " << n << std::endl; + return d_models[n]->evaluate( this, args ); +} + +void FirstOrderModelQInt::processInitializeModelForTerm(Node n) { + Debug("qint-debug") << "process init " << n << " " << n.getKind() << std::endl; + + if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){ + Node op = n.getKind()==APPLY_UF ? n.getOperator() : n; + if( d_models.find(op)==d_models.end()) { + Debug("qint-debug") << "init model for " << op << std::endl; + d_models[op] = new QIntDef; + } + } +} + +Node FirstOrderModelQInt::getUsedRepresentative( Node n ) { + if( hasTerm( n ) ){ + if( n.getType().isBoolean() ){ + return areEqual(n, d_true) ? d_true : d_false; + }else{ + return getRepresentative( n ); + } + }else{ + Trace("qint-debug") << "Get rep " << n << " " << n.getType() << std::endl; + Assert( d_rep_set.hasType( n.getType() ) && !d_rep_set.d_type_reps[n.getType()].empty() ); + return d_rep_set.d_type_reps[n.getType()][0]; + } +} + +void FirstOrderModelQInt::processInitializeQuantifier( Node q ) { + if( d_var_order.find( q )==d_var_order.end() ){ + d_var_order[q] = new QuantVarOrder( q ); + d_var_order[q]->debugPrint("qint-var-order"); + Trace("qint-var-order") << std::endl; + } +} +unsigned FirstOrderModelQInt::getOrderedNumVars( Node q ) { + //return q[0].getNumChildren(); + return d_var_order[q]->getNumVars(); +} + +TypeNode FirstOrderModelQInt::getOrderedVarType( Node q, int i ) { + //return q[0][i].getType(); + return d_var_order[q]->getVar( i ).getType(); +} + +int FirstOrderModelQInt::getOrderedVarNumToVarNum( Node q, int i ) { + return getVariableId( q, d_var_order[q]->getVar( i ) ); +} + +bool FirstOrderModelQInt::isLessThan( Node v1, Node v2 ) { + Assert( !v1.isNull() ); + Assert( !v2.isNull() ); + if( v1.getType().isSort() ){ + Assert( getRepId( v1 )!=-1 ); + Assert( getRepId( v2 )!=-1 ); + int rid1 = d_rep_id[v1]; + int rid2 = d_rep_id[v2]; + return rid1<rid2; + }else{ + return false; + } +} + +Node FirstOrderModelQInt::getMin( Node v1, Node v2 ) { + return isLessThan( v1, v2 ) ? v1 : v2; +} + +Node FirstOrderModelQInt::getMax( Node v1, Node v2 ) { + return isLessThan( v1, v2 ) ? v2 : v1; +} + +Node FirstOrderModelQInt::getMaximum( TypeNode tn ) { + return d_max[tn]; +} + +Node FirstOrderModelQInt::getNext( TypeNode tn, Node v ) { + if( v.isNull() ){ + return d_min[tn]; + }else{ + Assert( getRepId( v )!=-1 ); + int rid = d_rep_id[v]; + if( rid==(int)(d_rep_set.d_type_reps[tn].size()-1) ){ + Assert( false ); + return Node::null(); + }else{ + return d_rep_set.d_type_reps[tn][ rid+1 ]; + } + } +} +Node FirstOrderModelQInt::getPrev( TypeNode tn, Node v ) { + if( v.isNull() ){ + Assert( false ); + return Node::null(); + }else{ + Assert( getRepId( v )!=-1 ); + int rid = d_rep_id[v]; + if( rid==0 ){ + return Node::null(); + }else{ + return d_rep_set.d_type_reps[tn][ rid-1 ]; + } + } +} + +bool FirstOrderModelQInt::doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur ) { + Trace("qint-debug2") << "doMeet " << l1 << "..." << u1 << " with " << l2 << "..." << u2 << std::endl; + Assert( !u1.isNull() ); + Assert( !u2.isNull() ); + lr = l1.isNull() ? l2 : ( l2.isNull() ? l1 : getMax( l1, l2 ) ); + ur = getMin( u1, u2 ); + //return lr==ur || lr.isNull() || isLessThan( lr, ur ); + return lr.isNull() || isLessThan( lr, ur ); +} diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index b5bdff9ee..ab3a1aa52 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -33,16 +33,21 @@ class FirstOrderModelIG; namespace fmcheck { class FirstOrderModelFmc; } +class FirstOrderModelQInt; class FirstOrderModel : public TheoryModel { -private: +protected: + /** quant engine */ + QuantifiersEngine * d_qe; /** whether an axiom is asserted */ context::CDO< bool > d_axiom_asserted; /** list of quantifiers asserted in the current context */ context::CDList<Node> d_forall_asserts; /** is model set */ context::CDO< bool > d_isModelSet; + /** get variable id */ + std::map< Node, std::map< Node, int > > d_quant_var_id; /** get current model value */ virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0; public: //for Theory Quantifiers: @@ -57,20 +62,28 @@ public: //for Theory Quantifiers: /** initialize model for term */ void initializeModelForTerm( Node n ); virtual void processInitializeModelForTerm( Node n ) = 0; + virtual void processInitializeQuantifier( Node q ) {} public: - FirstOrderModel( context::Context* c, std::string name ); + FirstOrderModel(QuantifiersEngine * qe, context::Context* c, std::string name ); virtual ~FirstOrderModel(){} virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; } virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; } + virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; } // initialize the model void initialize( bool considerAxioms = true ); - virtual void processInitialize() = 0; + virtual void processInitialize( bool ispre ) = 0; /** mark model set */ void markModelSet() { d_isModelSet = true; } /** is model set */ bool isModelSet() { return d_isModelSet; } /** get current model value */ Node getCurrentModelValue( Node n, bool partial = false ); + /** get variable id */ + int getVariableId(Node f, Node n) { + return d_quant_var_id.find( f )!=d_quant_var_id.end() ? d_quant_var_id[f][n] : -1; + } + /** get some domain element */ + Node getSomeDomainElement(TypeNode tn); };/* class FirstOrderModel */ @@ -93,10 +106,10 @@ private: Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ); //the following functions are for evaluating quantifier bodies public: - FirstOrderModelIG(context::Context* c, std::string name); + FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name); FirstOrderModelIG * asFirstOrderModelIG() { return this; } // initialize the model - void processInitialize(); + void processInitialize( bool ispre ); //for initialize model void processInitializeModelForTerm( Node n ); /** reset evaluation */ @@ -128,8 +141,6 @@ class FirstOrderModelFmc : public FirstOrderModel { friend class FullModelChecker; private: - /** quant engine */ - QuantifiersEngine * d_qe; /** models for UF */ std::map<Node, Def * > d_models; std::map<TypeNode, Node > d_model_basis_rep; @@ -143,8 +154,7 @@ public: FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name); FirstOrderModelFmc * asFirstOrderModelFmc() { return this; } // initialize the model - void processInitialize(); - + void processInitialize( bool ispre ); Node getFunctionValue(Node op, const char* argPrefix ); bool isStar(Node n); @@ -152,7 +162,6 @@ public: Node getStarElement(TypeNode tn); bool isModelBasisTerm(Node n); Node getModelBasisTerm(TypeNode tn); - Node getSomeDomainElement(TypeNode tn); bool isInterval(Node n); Node getInterval( Node lb, Node ub ); bool isInRange( Node v, Node i ); @@ -161,6 +170,50 @@ public: } +class QIntDef; +class QuantVarOrder; +class FirstOrderModelQInt : public FirstOrderModel +{ + friend class QIntervalBuilder; +private: + /** uf op to some representation */ + std::map<Node, QIntDef * > d_models; + /** representatives to ids */ + std::map< Node, int > d_rep_id; + std::map< TypeNode, Node > d_min; + std::map< TypeNode, Node > d_max; + /** quantifiers to information regarding variable ordering */ + std::map<Node, QuantVarOrder * > d_var_order; + /** get current model value */ + Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ); + void processInitializeModelForTerm(Node n); +public: + FirstOrderModelQInt(QuantifiersEngine * qe, context::Context* c, std::string name); + FirstOrderModelQInt * asFirstOrderModelQInt() { return this; } + void processInitialize( bool ispre ); + Node getFunctionValue(Node op, const char* argPrefix ); + + Node getUsedRepresentative( Node n ); + int getRepId( Node n ) { return d_rep_id.find( n )==d_rep_id.end() ? -1 : d_rep_id[n]; } + bool isLessThan( Node v1, Node v2 ); + Node getMin( Node v1, Node v2 ); + Node getMax( Node v1, Node v2 ); + Node getMinimum( TypeNode tn ) { return getNext( tn, Node::null() ); } + Node getMaximum( TypeNode tn ); + bool isMinimum( Node n ) { return n==getMinimum( n.getType() ); } + bool isMaximum( Node n ) { return n==getMaximum( n.getType() ); } + Node getNext( TypeNode tn, Node v ); + Node getPrev( TypeNode tn, Node v ); + bool doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr, Node& ur ); + QuantVarOrder * getVarOrder( Node q ) { return d_var_order[q]; } + + void processInitializeQuantifier( Node q ) ; + unsigned getOrderedNumVars( Node q ); + TypeNode getOrderedVarType( Node q, int i ); + int getOrderedVarNumToVarNum( Node q, int i ); +}; + + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 2f32ec5e6..174e26a5a 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -588,7 +588,6 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, std::vector< TypeNode > types; for(unsigned i=0; i<f[0].getNumChildren(); i++){ types.push_back(f[0][i].getType()); - d_quant_var_id[f][f[0][i]] = i; } TypeNode typ = NodeManager::currentNM()->mkFunctionType( types, NodeManager::currentNM()->booleanType() ); Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" ); @@ -599,7 +598,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, initializeType( fmfmc, f[0][i].getType() ); } - if( !options::fmfModelBasedInst() ){ + if( options::mbqiMode()==MBQI_NONE ){ //just exhaustive instantiate Node c = mkCondDefault( fmfmc, f ); d_quant_models[f].addEntry( fmfmc, c, d_false ); @@ -958,8 +957,8 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def }else{ TypeNode tn = eq[0].getType(); if( tn.isSort() ){ - int j = getVariableId(f, eq[0]); - int k = getVariableId(f, eq[1]); + int j = fm->getVariableId(f, eq[0]); + int k = fm->getVariableId(f, eq[1]); if( !fm->d_rep_set.hasType( tn ) ){ getSomeDomainElement( fm, tn ); //to verify the type is initialized } @@ -977,7 +976,7 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def } void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) { - int j = getVariableId(f, v); + int j = fm->getVariableId(f, v); for (unsigned i=0; i<dc.d_cond.size(); i++) { Node val = dc.d_value[i]; if( val.isNull() ){ @@ -1074,7 +1073,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, Trace("fmc-uf-process") << "Process " << v << std::endl; bool bind_var = false; if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){ - int j = getVariableId(f, v); + 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])) { v = cond[j+1]; @@ -1084,7 +1083,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f, } if (bind_var) { Trace("fmc-uf-process") << "bind variable..." << std::endl; - int j = getVariableId(f, v); + 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; diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 606392831..db5abb01e 100644 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -92,7 +92,6 @@ protected: std::map<Node, Node > d_quant_cond; std::map< TypeNode, Node > d_array_cond; std::map< Node, Node > d_array_term_cond; - std::map<Node, std::map< Node, int > > d_quant_var_id; std::map<Node, std::vector< int > > d_star_insts; void initializeType( FirstOrderModelFmc * fm, TypeNode tn ); Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n); @@ -138,7 +137,6 @@ public: bool optBuildAtFullModel(); - int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; } void debugPrintCond(const char * tr, Node n, bool dispStar = false); void debugPrint(const char * tr, Node n, bool dispStar = false); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index ea6f2d775..468c78978 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -44,7 +44,7 @@ bool QModelBuilder::isQuantifierActive( Node f ) { bool QModelBuilder::optUseModel() { - return options::fmfModelBasedInst() || options::fmfBoundInt(); + return options::mbqiMode()!=MBQI_NONE || options::fmfBoundInt(); } void QModelBuilder::debugModel( FirstOrderModel* fm ){ @@ -124,6 +124,7 @@ Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std:: void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { FirstOrderModel* f = (FirstOrderModel*)m; FirstOrderModelIG* fm = f->asFirstOrderModelIG(); + Trace("model-engine-debug") << "Process build model, fullModel = " << fullModel << " " << optUseModel() << std::endl; if( fullModel ){ Assert( d_curr_model==fm ); //update models @@ -145,7 +146,7 @@ void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { reset( fm ); //only construct first order model if optUseModel() is true if( optUseModel() ){ - Trace("model-engine-debug") << "Initializing quantifiers..." << std::endl; + Trace("model-engine-debug") << "Initializing " << fm->getNumAssertedQuantifiers() << " quantifiers..." << std::endl; //check if any quantifiers are un-initialized for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ Node f = fm->getAssertedQuantifier( i ); @@ -397,7 +398,6 @@ bool QModelBuilderIG::isTermActive( Node n ){ //do exhaustive instantiation bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort ) { if( optUseModel() ){ - RepSetIterator riter( d_qe, &(d_qe->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ FirstOrderModelIG * fmig = (FirstOrderModelIG*)d_qe->getModel(); @@ -456,7 +456,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i d_statistics.d_eval_lits += fmig->d_eval_lits; d_statistics.d_eval_lits_unknown += fmig->d_eval_lits_unknown; } - Trace("inst-fmf-ei") << "Finished: " << std::endl; + Trace("inst-fmf-ei") << "For " << f << ", finished: " << std::endl; Trace("inst-fmf-ei") << " Inst Tried: " << d_triedLemmas << std::endl; Trace("inst-fmf-ei") << " Inst Added: " << d_addedLemmas << std::endl; if( d_addedLemmas>1000 ){ diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 99f5e8df6..5006a8a61 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -21,6 +21,8 @@ #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" +#include "theory/quantifiers/full_model_check.h" +#include "theory/quantifiers/qinterval_builder.h" using namespace std; using namespace CVC4; @@ -34,11 +36,18 @@ using namespace CVC4::theory::inst; ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule( qe ){ - if( options::fmfFullModelCheck() || options::fmfBoundInt() ){ + Trace("model-engine-debug") << "Initialize model engine, mbqi : " << options::mbqiMode() << " " << options::fmfBoundInt() << std::endl; + if( options::mbqiMode()==MBQI_FMC || options::fmfBoundInt() ){ + Trace("model-engine-debug") << "...make fmc builder." << std::endl; d_builder = new fmcheck::FullModelChecker( c, qe ); - }else if( options::fmfNewInstGen() ){ + }else if( options::mbqiMode()==MBQI_INTERVAL ){ + Trace("model-engine-debug") << "...make interval builder." << std::endl; + d_builder = new QIntervalBuilder( c, qe ); + }else if( options::mbqiMode()==MBQI_INST_GEN ){ + Trace("model-engine-debug") << "...make inst-gen builder." << std::endl; d_builder = new QModelBuilderInstGen( c, qe ); }else{ + Trace("model-engine-debug") << "...make default model builder." << std::endl; d_builder = new QModelBuilderDefault( c, qe ); } @@ -203,7 +212,7 @@ int ModelEngine::checkModel(){ } Trace("model-engine-debug") << "Do exhaustive instantiation..." << std::endl; - int e_max = options::fmfFullModelCheck() && options::fmfModelBasedInst() ? 2 : 1; + int e_max = options::mbqiMode()==MBQI_FMC ? 2 : 1; for( int e=0; e<e_max; e++) { if (d_addedLemmas==0) { for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 0c3c74b5f..fcbba7aee 100644 --- a/src/theory/quantifiers/model_engine.h +++ b/src/theory/quantifiers/model_engine.h @@ -20,7 +20,6 @@ #include "theory/quantifiers_engine.h" #include "theory/quantifiers/model_builder.h" #include "theory/theory_model.h" -#include "theory/quantifiers/full_model_check.h" #include "theory/quantifiers/relevant_domain.h" namespace CVC4 { diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp index 7da3b150f..10185914e 100644 --- a/src/theory/quantifiers/modes.cpp +++ b/src/theory/quantifiers/modes.cpp @@ -77,5 +77,28 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::AxiomInstMode m return out; } +std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode) { + switch(mode) { + case theory::quantifiers::MBQI_DEFAULT: + out << "MBQI_DEFAULT"; + break; + case theory::quantifiers::MBQI_NONE: + out << "MBQI_NONE"; + break; + case theory::quantifiers::MBQI_INST_GEN: + out << "MBQI_INST_GEN"; + break; + case theory::quantifiers::MBQI_FMC: + out << "MBQI_FMC"; + break; + case theory::quantifiers::MBQI_INTERVAL: + out << "MBQI_INTERVAL"; + break; + default: + out << "MbqiMode!UNKNOWN"; + } + return out; +} + }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h index edf9c78fe..7c4cb3651 100644 --- a/src/theory/quantifiers/modes.h +++ b/src/theory/quantifiers/modes.h @@ -55,6 +55,22 @@ typedef enum { AXIOM_INST_MODE_PRIORITY, } AxiomInstMode; +typedef enum { + /** default, mbqi from CADE 24 paper */ + MBQI_DEFAULT, + /** no mbqi */ + MBQI_NONE, + /** implementation that mimics inst-gen */ + MBQI_INST_GEN, + /** mbqi from Section 5.4.2 of AJR thesis */ + MBQI_FMC, + /** mbqi with integer intervals */ + //MBQI_FMC_INTERVAL, + /** mbqi with interval abstraction of uninterpreted sorts */ + MBQI_INTERVAL, +} MbqiMode; + + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 1eb98e7b7..f485b981c 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -95,11 +95,9 @@ option internalReps /--disable-quant-internal-reps bool :default true option finiteModelFind --finite-model-find bool :default false use finite model finding heuristic for quantifier instantiation -option fmfModelBasedInst /--disable-fmf-mbqi bool :default true - disable model-based quantifier instantiation for finite model finding +option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToMbqiMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkMbqiMode :predicate-include "theory/quantifiers/options_handlers.h" + choose mode for model-based quantifier instantiation -option fmfFullModelCheck --fmf-fmc bool :default false :read-write - enable full model check for finite model finding option fmfFmcSimple /--disable-fmf-fmc-simple bool :default true disable simple models in full model check for finite model finding option fmfFmcCoverSimplify /--disable-fmf-fmc-cover-simplify bool :default true @@ -115,8 +113,6 @@ option fmfInstEngine --fmf-inst-engine bool :default false use instantiation engine in conjunction with finite model finding option fmfRelevantDomain --fmf-relevant-domain 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 --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true enable Inst-Gen instantiation techniques for finite model finding (default) /disable Inst-Gen instantiation techniques for finite model finding diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h index 410578af0..a119bcaf6 100644 --- a/src/theory/quantifiers/options_handlers.h +++ b/src/theory/quantifiers/options_handlers.h @@ -73,6 +73,28 @@ priority \n\ \n\ "; +static const std::string mbqiModeHelp = "\ +Model-based quantifier instantiation modes currently supported by the --mbqi option:\n\ +\n\ +default \n\ ++ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\ + model finding paper.\n\ +\n\ +none \n\ ++ Disable model-based quantifier instantiation.\n\ +\n\ +instgen \n\ ++ Use instantiation algorithm that mimics Inst-Gen calculus. \n\ +\n\ +fmc \n\ ++ Use algorithm from Section 5.4.2 of thesis Finite Model Finding in Satisfiability. \n\ + Modulo Theories.\n\ +\n\ +interval \n\ ++ Use algorithm that abstracts domain elements as intervals. \n\ +\n\ +"; + inline InstWhenMode stringToInstWhenMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { if(optarg == "pre-full") { return INST_WHEN_PRE_FULL; @@ -135,6 +157,30 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar } } +inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) { + if(optarg == "default") { + return MBQI_DEFAULT; + } else if(optarg == "none") { + return MBQI_NONE; + } else if(optarg == "instgen") { + return MBQI_INST_GEN; + } else if(optarg == "fmc") { + return MBQI_FMC; + } else if(optarg == "interval") { + return MBQI_INTERVAL; + } else if(optarg == "help") { + puts(mbqiModeHelp.c_str()); + exit(1); + } else { + throw OptionException(std::string("unknown option for --mbqi: `") + + optarg + "'. Try --mbqi help."); + } +} + +inline void checkMbqiMode(std::string option, MbqiMode mode, SmtEngine* smt) throw(OptionException) { + +} + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/quantifiers/qinterval_builder.cpp b/src/theory/quantifiers/qinterval_builder.cpp new file mode 100755 index 000000000..ce85cecc0 --- /dev/null +++ b/src/theory/quantifiers/qinterval_builder.cpp @@ -0,0 +1,1111 @@ +/********************* */
+/*! \file qinterval_builder.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of qinterval builder
+ **/
+
+
+#include "theory/quantifiers/qinterval_builder.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+//lower bound is exclusive
+//upper bound is inclusive
+
+struct QIntSort
+{
+ FirstOrderModelQInt * m;
+ bool operator() (Node i, Node j) {
+ return m->isLessThan( i, j );
+ }
+};
+
+void QIntDef::init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u ) {
+ for( unsigned i=0; i<m->getOrderedNumVars( q ); i++ ){
+ l.push_back( Node::null() );
+ u.push_back( m->getMaximum( m->getOrderedVarType( q, i ) ) );
+ }
+}
+
+void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u )
+{
+ Trace(c) << "( ";
+ for( unsigned i=0; i<l.size(); i++ ){
+ if( i>0 ) Trace(c) << ", ";
+ //Trace(c) << l[i] << "..." << u[i];
+ int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1;
+ int uindex = m->getRepId( u[i] );
+ Trace(c) << lindex << "..." << uindex;
+ }
+ Trace(c) << " )";
+}
+
+
+int QIntDef::getEvIndex( FirstOrderModelQInt * m, Node n, bool exc ) {
+ if( n.isNull() ){
+ Assert( exc );
+ return 0;
+ }else{
+ int min = 0;
+ int max = (int)(d_def_order.size()-1);
+ while( min!=max ){
+ int index = (min+max)/2;
+ Assert( index>=0 && index<(int)d_def_order.size() );
+ if( n==d_def_order[index] ){
+ max = index;
+ min = index;
+ }else if( m->isLessThan( n, d_def_order[index] ) ){
+ max = index;
+ }else{
+ min = index+1;
+ }
+ }
+ if( n==d_def_order[min] && exc ){
+ min++;
+ }
+ Assert( min>=0 && min<(int)d_def_order.size() );
+ if( ( min!=0 && !m->isLessThan( d_def_order[min-1], n ) && ( !exc || d_def_order[min-1]!=n ) ) ||
+ ( ( exc || d_def_order[min]!=n ) && !m->isLessThan( n, d_def_order[min] ) ) ){
+ Debug("qint-error") << "ERR size : " << d_def_order.size() << ", exc : " << exc << std::endl;
+ for( unsigned i=0; i<d_def_order.size(); i++ ){
+ Debug("qint-error") << "ERR ch #" << i << " : " << d_def_order[i];
+ Debug("qint-error") << " " << m->getRepId( d_def_order[i] ) << std::endl;
+ }
+ Debug("qint-error") << " : " << n << " " << min << " " << m->getRepId( n ) << std::endl;
+ }
+
+ Assert( min==0 || m->isLessThan( d_def_order[min-1], n ) || ( exc && d_def_order[min-1]==n ) );
+ Assert( ( !exc && n==d_def_order[min] ) || m->isLessThan( n, d_def_order[min] ) );
+ return min;
+ }
+}
+
+void QIntDef::addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
+ Node v, unsigned depth ) {
+ if( depth==0 ){
+ Trace("qint-compose-debug") << "Add entry ";
+ debugPrint( "qint-compose-debug", m, q, l, u );
+ Trace("qint-compose-debug") << " -> " << v << "..." << std::endl;
+ }
+ //Assert( false );
+ if( depth==u.size() ){
+ Assert( d_def_order.empty() );
+ Assert( v.isNull() || v.isConst() || ( v.getType().isSort() && m->getRepId( v )!=-1 ) );
+ d_def_order.push_back( v );
+ }else{
+ /*
+ if( !d_def_order.empty() &&
+ ( l[depth].isNull() || m->isLessThan( l[depth], d_def_order[d_def_order.size()-1] ) ) ){
+ int startEvIndex = getEvIndex( m, l[depth], true );
+ int endEvIndex;
+ if( m->isLessThan( u[depth], d_def_order[d_def_order.size()-1] ) ){
+ endEvIndex = getEvIndex( m, u[depth] );
+ }else{
+ endEvIndex = d_def_order.size()-1;
+ }
+ Trace("qint-compose-debug2") << this << " adding for bounds " << l[depth] << "..." << u[depth] << std::endl;
+ for( int i=startEvIndex; i<=endEvIndex; i++ ){
+ Trace("qint-compose-debug2") << this << " add entry " << d_def_order[i] << std::endl;
+ d_def[d_def_order[i]].addEntry( m, q, l, u, v, depth+1 );
+ }
+ }
+ if( !d_def_order.empty() &&
+ d_def.find(u[depth])==d_def.end() &&
+ !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
+ Trace("qint-compose-debug2") << "Bad : depth : " << depth << std::endl;
+ }
+ Assert( d_def_order.empty() ||
+ d_def.find(u[depth])!=d_def.end() ||
+ m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) );
+
+ if( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
+ Trace("qint-compose-debug2") << this << " add entry new : " << u[depth] << std::endl;
+ d_def_order.push_back( u[depth] );
+ d_def[u[depth]].addEntry( m, q, l, u, v, depth+1 );
+ }
+ */
+ //%%%%%%
+ bool success = true;
+ int nnum = m->getVarOrder( q )->getNextNum( depth );
+ Node pl;
+ Node pu;
+ if( nnum!=-1 ){
+ Trace("qint-compose-debug2") << "...adding entry #" << depth << " is #" << nnum << std::endl;
+ //Assert( l[nnum].isNull() || l[nnum]==l[depth] || m->isLessThan( l[nnum], l[depth] ) );
+ //Assert( u[nnum]==u[depth] || m->isLessThan( u[depth], u[nnum] ) );
+ pl = l[nnum];
+ pu = u[nnum];
+ if( !m->doMeet( l[nnum], u[nnum], l[depth], u[depth], l[nnum], u[nnum] ) ){
+ success = false;
+ }
+ }
+ //%%%%%%
+ if( success ){
+ Node r = u[depth];
+ if( d_def.find( r )!=d_def.end() ){
+ d_def[r].addEntry( m, q, l, u, v, depth+1 );
+ }else{
+ if( !d_def_order.empty() &&
+ !m->isLessThan( d_def_order[d_def_order.size()-1], u[depth] ) ){
+ Trace("qint-compose-debug2") << "Bad : depth : " << depth << " ";
+ Trace("qint-compose-debug2") << d_def_order[d_def_order.size()-1] << " " << u[depth] << std::endl;
+ }
+ Assert( d_def_order.empty() || m->isLessThan( d_def_order[d_def_order.size()-1], r ) );
+ d_def_order.push_back( r );
+ d_def[r].addEntry( m, q, l, u, v, depth+1 );
+ }
+ }
+ if( nnum!=-1 ){
+ l[nnum] = pl;
+ u[nnum] = pu;
+ }
+ }
+}
+
+Node QIntDef::simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
+ unsigned depth ) {
+ if( d_def.empty() ){
+ if( d_def_order.size()!=0 ){
+ Debug("qint-error") << "Simplify, size = " << d_def_order.size() << std::endl;
+ }
+ Assert( d_def_order.size()==1 );
+ return d_def_order[0];
+ }else{
+ Assert( !d_def_order.empty() );
+ std::vector< Node > newDefs;
+ Node curr;
+ for( unsigned i=0; i<d_def_order.size(); i++ ){
+ Node n = d_def[d_def_order[i]].simplify_r( m, q, il, iu, depth+1 );
+ if( i>0 ){
+ if( n==curr && !n.isNull() ){
+ d_def.erase( d_def_order[i-1] );
+ }else{
+ newDefs.push_back( d_def_order[i-1] );
+ }
+ }
+ curr = n;
+ }
+ newDefs.push_back( d_def_order[d_def_order.size()-1] );
+ d_def_order.clear();
+ d_def_order.insert( d_def_order.end(), newDefs.begin(), newDefs.end() );
+ return d_def_order.size()==1 ? curr : Node::null();
+ }
+}
+
+Node QIntDef::simplify( FirstOrderModelQInt * m, Node q ) {
+ std::vector< Node > l;
+ std::vector< Node > u;
+ if( !q.isNull() ){
+ //init_vec( m, q, l, u );
+ }
+ return simplify_r( m, q, l, u, 0 );
+}
+
+bool QIntDef::isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
+ unsigned depth ) {
+ if( d_def_order.empty() ){
+ return false;
+ }else if( d_def.empty() ){
+ return true;
+ }else{
+ //get the current maximum
+ Node mx;
+ if( !q.isNull() ){
+ int pnum = m->getVarOrder( q )->getPrevNum( depth );
+ if( pnum!=-1 ){
+ mx = u[pnum];
+ }
+ }
+ if( mx.isNull() ){
+ mx = m->getMaximum( d_def_order[d_def_order.size()-1].getType() );
+ }
+ //if not current maximum
+ if( d_def_order[d_def_order.size()-1]!=mx ){
+ return false;
+ }else{
+ Node pu = u[depth];
+ for( unsigned i=0; i<d_def_order.size(); i++ ){
+ u[depth] = d_def_order[i];
+ if( !d_def[d_def_order[i]].isTotal_r( m, q, l, u, depth+1 ) ){
+ return false;
+ }
+ }
+ u[depth] = pu;
+ return true;
+ }
+ }
+}
+
+bool QIntDef::isTotal( FirstOrderModelQInt * m, Node q ) {
+ std::vector< Node > l;
+ std::vector< Node > u;
+ if( !q.isNull() ){
+ init_vec( m, q, l, u );
+ }
+ return isTotal_r( m, q, l, u, 0 );
+}
+
+void QIntDef::construct_compose_r( FirstOrderModelQInt * m, Node q,
+ std::vector< Node >& l, std::vector< Node >& u,
+ Node n, QIntDef * f,
+ std::vector< Node >& args,
+ std::map< unsigned, QIntDef >& children,
+ std::map< unsigned, Node >& bchildren,
+ QIntVarNumIndex& vindex, unsigned depth ) {
+ //check for short circuit
+ if( !f ){
+ if( !args.empty() ){
+ if( ( n.getKind()==OR && args[args.size()-1]==m->d_true ) ||
+ ( n.getKind()==AND && args[args.size()-1]==m->d_false ) ){
+ addEntry( m, q, l, u, args[args.size()-1] );
+ return;
+ }
+ }
+ }
+
+ for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << " "; }
+ Trace("qint-compose") << (f ? "U" : "I" ) << "C( ";
+ for( unsigned i=0; i<l.size(); i++ ){
+ if( i>0 ) Trace("qint-compose") << ", ";
+ //Trace("qint-compose") << l[i] << "..." << u[i];
+ int lindex = l[i].isNull() ? 0 : m->getRepId( l[i] ) + 1;
+ int uindex = m->getRepId( u[i] );
+ Trace( "qint-compose" ) << lindex << "..." << uindex;
+ }
+ Trace("qint-compose") << " )...";
+
+ //finished?
+ if( ( f && f->d_def.empty() ) || args.size()==n.getNumChildren() ){
+ if( f ){
+ Assert( f->d_def_order.size()==1 );
+ Trace("qint-compose") << "UVALUE(" << f->d_def_order[0] << ")" << std::endl;
+ addEntry( m, q, l, u, f->d_def_order[0] );
+ }else{
+ Node nn;
+ bool nnSet = false;
+ for( unsigned i=0; i<args.size(); i++ ){
+ if( args[i].isNull() ){
+ nnSet = true;
+ break;
+ }
+ }
+ if( !nnSet ){
+ if( n.getKind()==EQUAL ){
+ nn = NodeManager::currentNM()->mkConst( args[0]==args[1] );
+ }else{
+ //apply the operator to args
+ nn = NodeManager::currentNM()->mkNode( n.getKind(), args );
+ nn = Rewriter::rewrite( nn );
+ }
+ }
+ Trace("qint-compose") << "IVALUE(" << nn << ")" << std::endl;
+ addEntry( m, q, l, u, nn );
+ Trace("qint-compose-debug2") << "...added entry." << std::endl;
+ }
+ }else{
+ //if a non-simple child
+ if( children.find( depth )!=children.end() ){
+ //***************************
+ Trace("qint-compose") << "compound child, recurse" << std::endl;
+ std::vector< int > currIndex;
+ std::vector< int > endIndex;
+ std::vector< Node > prevL;
+ std::vector< Node > prevU;
+ std::vector< QIntDef * > visited;
+ do{
+ Assert( currIndex.size()==visited.size() );
+
+ //populate the vectors
+ while( visited.size()<m->getOrderedNumVars( q ) ){
+ unsigned i = visited.size();
+ QIntDef * qq = visited.empty() ? &children[depth] : visited[i-1]->getChild( currIndex[i-1] );
+ visited.push_back( qq );
+ Node qq_mx = qq->getMaximum();
+ Trace("qint-compose-debug2") << "...Get ev indices " << i << " " << l[i] << " " << u[i] << std::endl;
+ currIndex.push_back( qq->getEvIndex( m, l[i], true ) );
+ Trace("qint-compose-debug2") << "...Done get curr index " << currIndex[currIndex.size()-1] << std::endl;
+ if( m->isLessThan( qq_mx, u[i] ) ){
+ endIndex.push_back( qq->getNumChildren()-1 );
+ }else{
+ endIndex.push_back( qq->getEvIndex( m, u[i] ) );
+ }
+ Trace("qint-compose-debug2") << "...Done get end index " << endIndex[endIndex.size()-1] << std::endl;
+ prevL.push_back( l[i] );
+ prevU.push_back( u[i] );
+ if( !m->doMeet( prevL[i], prevU[i],
+ qq->getLower( currIndex[i] ), qq->getUpper( currIndex[i] ), l[i], u[i] ) ){
+ Assert( false );
+ }
+ }
+ for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << " "; }
+ for( unsigned i=0; i<currIndex.size(); i++ ){
+ Trace("qint-compose") << "[" << currIndex[i] << "/" << endIndex[i] << "]";
+ }
+ Trace("qint-compose") << std::endl;
+ //consider the current
+ int activeIndex = visited.size()-1;
+ QIntDef * qa = visited.empty() ? &children[depth] : visited[activeIndex]->getChild( currIndex[activeIndex] );
+ if( f ){
+ int fIndex = f->getEvIndex( m, qa->getValue() );
+ construct_compose_r( m, q, l, u, n, f->getChild( fIndex ), args, children, bchildren, vindex, depth+1 );
+ }else{
+ args.push_back( qa->getValue() );
+ construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 );
+ args.pop_back();
+ }
+
+ //increment the index (if possible)
+ while( activeIndex>=0 && currIndex[activeIndex]==endIndex[activeIndex] ){
+ currIndex.pop_back();
+ endIndex.pop_back();
+ l[activeIndex] = prevL[activeIndex];
+ u[activeIndex] = prevU[activeIndex];
+ prevL.pop_back();
+ prevU.pop_back();
+ visited.pop_back();
+ activeIndex--;
+ }
+ if( activeIndex>=0 ){
+ for( unsigned i=0; i<depth; i++ ) { Trace("qint-compose") << " "; }
+ Trace("qint-compose-debug") << "Increment at " << activeIndex << std::endl;
+ currIndex[activeIndex]++;
+ if( !m->doMeet( prevL[activeIndex], prevU[activeIndex],
+ visited[activeIndex]->getLower( currIndex[activeIndex] ),
+ visited[activeIndex]->getUpper( currIndex[activeIndex] ),
+ l[activeIndex], u[activeIndex] ) ){
+ Assert( false );
+ }
+ }
+ }while( !visited.empty() );
+ //***************************
+ }else{
+ Assert( bchildren.find( depth )!=bchildren.end() );
+ Node v = bchildren[depth];
+ if( f ){
+ if( v.getKind()==BOUND_VARIABLE ){
+ int vn = vindex.d_var_num[depth];
+ Trace("qint-compose") << "variable #" << vn << ", recurse" << std::endl;
+ //int vn = m->getOrderedVarOccurId( q, n, depth );
+ Trace("qint-compose-debug") << "-process " << v << ", which is var #" << vn << std::endl;
+ Node lprev = l[vn];
+ Node uprev = u[vn];
+ //restrict to last variable in order
+ int pnum = m->getVarOrder( q )->getPrevNum( vn );
+ if( pnum!=-1 ){
+ Trace("qint-compose-debug") << "-restrict to var #" << pnum << " " << l[pnum] << " " << u[pnum] << std::endl;
+ l[vn] = l[pnum];
+ u[vn] = u[pnum];
+ }
+ int startIndex = f->getEvIndex( m, l[vn], true );
+ int endIndex = f->getEvIndex( m, u[vn] );
+ Trace("qint-compose-debug") << "--will process " << startIndex << " " << endIndex << std::endl;
+ for( int i=startIndex; i<=endIndex; i++ ){
+ if( m->doMeet( lprev, uprev, f->getLower( i ), f->getUpper( i ), l[vn], u[vn] ) ){
+ construct_compose_r( m, q, l, u, n, f->getChild( i ), args, children, bchildren, vindex, depth+1 );
+ }else{
+ Assert( false );
+ }
+ }
+ l[vn] = lprev;
+ u[vn] = uprev;
+ }else{
+ Trace("qint-compose") << "value, recurse" << std::endl;
+ //simple
+ int ei = f->getEvIndex( m, v );
+ construct_compose_r( m, q, l, u, n, f->getChild( ei ), args, children, bchildren, vindex, depth+1 );
+ }
+ }else{
+ Trace("qint-compose") << "value, recurse" << std::endl;
+ args.push_back( v );
+ construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, depth+1 );
+ args.pop_back();
+ }
+ }
+ }
+}
+
+
+void QIntDef::construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v ) {
+ if( depth==m->getOrderedNumVars( q ) ){
+ Assert( !v.isNull() );
+ d_def_order.push_back( v );
+ }else{
+ TypeNode tn = m->getOrderedVarType( q, depth );
+ //int vnum = m->getVarOrder( q )->getVar( depth )==
+ if( depth==vn ){
+ for( unsigned i=0; i<m->d_rep_set.d_type_reps[tn].size(); i++ ){
+ Node vv = m->d_rep_set.d_type_reps[tn][i];
+ d_def_order.push_back( vv );
+ d_def[vv].construct_enum_r( m, q, vn, depth+1, vv );
+ }
+ }else if( m->getVarOrder( q )->getVar( depth )==m->getVarOrder( q )->getVar( vn ) && depth>vn ){
+ d_def_order.push_back( v );
+ d_def[v].construct_enum_r( m, q, vn, depth+1, v );
+ }else{
+ Node mx = m->getMaximum( tn );
+ d_def_order.push_back( mx );
+ d_def[mx].construct_enum_r( m, q, vn, depth+1, v );
+ }
+ }
+}
+
+bool QIntDef::construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn ) {
+ TypeNode tn = m->getOrderedVarType( q, vn );
+ if( tn.isSort() ){
+ construct_enum_r( m, q, vn, 0, Node::null() );
+ return true;
+ }else{
+ return false;
+ }
+}
+
+bool QIntDef::construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f,
+ std::map< unsigned, QIntDef >& children,
+ std::map< unsigned, Node >& bchildren, int varChCount,
+ QIntVarNumIndex& vindex ) {
+ Trace("qint-compose") << "Do " << (f ? "uninterpreted" : "interpreted");
+ Trace("qint-compose") << " compose, var count = " << varChCount << "..." << std::endl;
+ std::vector< Node > l;
+ std::vector< Node > u;
+ init_vec( m, q, l, u );
+ if( varChCount==0 || f ){
+ //standard (no variable child) interpreted compose, or uninterpreted compose
+ std::vector< Node > args;
+ construct_compose_r( m, q, l, u, n, f, args, children, bchildren, vindex, 0 );
+ }else{
+ //special cases
+ bool success = false;
+ int varIndex = ( bchildren.find( 0 )!=bchildren.end() && bchildren[0].getKind()==BOUND_VARIABLE ) ? 0 : 1;
+ if( varChCount>1 ){
+ if( n.getKind()==EQUAL ){
+ //make it an enumeration
+ unsigned vn = vindex.d_var_num[0];
+ if( children[0].construct_enum( m, q, vn ) ){
+ bchildren.erase( 0 );
+ varIndex = 1;
+ success = true;
+ }
+ }
+ }else{
+ success = n.getKind()==EQUAL;
+ }
+ if( success ){
+ int oIndex = varIndex==0 ? 1 : 0;
+ Node v = bchildren[varIndex];
+ unsigned vn = vindex.d_var_num[varIndex];
+ if( children.find( oIndex )==children.end() ){
+ Assert( bchildren.find( oIndex )!=bchildren.end() );
+ Node at = bchildren[oIndex];
+ Trace("qint-icompose") << "Basic child, " << at << " with var " << v << std::endl;
+ Node prev = m->getPrev( bchildren[oIndex].getType(), bchildren[oIndex] );
+ Node above = u[vn];
+ if( !prev.isNull() ){
+ u[vn] = prev;
+ addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) );
+ }
+ l[vn] = prev;
+ u[vn] = at;
+ addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( true ) );
+ if( at!=above ){
+ l[vn] = at;
+ u[vn] = above;
+ addEntry( m, q, l, u, NodeManager::currentNM()->mkConst( false ) );
+ }
+ }else{
+ QIntDef * qid = &children[oIndex];
+ qid->debugPrint("qint-icompose", m, q );
+ Trace("qint-icompose") << " against variable..." << v << ", which is var #" << vn << std::endl;
+
+ TypeNode tn = v.getType();
+ QIntDefIter qdi( m, q, qid );
+ while( !qdi.isFinished() ){
+ std::vector< Node > us;
+ qdi.getUppers( us );
+ std::vector< Node > ls;
+ qdi.getLowers( ls );
+ qdi.debugPrint( "qint-icompose" );
+
+ Node n_below = ls[vn];
+ Node n_prev = m->getPrev( tn, qdi.getValue() );
+ Node n_at = qdi.getValue();
+ Node n_above = us[vn];
+ Trace("qint-icompose") << n_below << " < " << n_prev << " < " << n_at << " < " << n_above << std::endl;
+ if( n.getKind()==EQUAL ){
+ bool atLtAbove = m->isLessThan( n_at, n_above );
+ Node currL = n_below;
+ if( n_at==n_above || atLtAbove ){
+ //add for value (at-1)
+ if( !n_prev.isNull() && ( n_below.isNull() || m->isLessThan( n_below, n_prev ) ) ){
+ ls[vn] = currL;
+ us[vn] = n_prev;
+ currL = n_prev;
+ Trace("qint-icompose") << "-add entry(-) at " << ls[vn] << "..." << us[vn] << std::endl;
+ addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( false ) );
+ }
+ //add for value (at)
+ if( ( n_below.isNull() || m->isLessThan( n_below, n_at ) ) && atLtAbove ){
+ ls[vn] = currL;
+ us[vn] = n_at;
+ currL = n_at;
+ Trace("qint-icompose") << "-add entry(=) at " << ls[vn] << "..." << us[vn] << std::endl;
+ addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( true ) );
+ }
+ }
+ ls[vn] = currL;
+ us[vn] = n_above;
+ Trace("qint-icompose") << "-add entry(+) at " << ls[vn] << "..." << us[vn] << std::endl;
+ addEntry( m, q, ls, us, NodeManager::currentNM()->mkConst( n_at==n_above ) );
+ }else{
+ return false;
+ }
+ qdi.increment();
+
+ Trace("qint-icompose-debug") << "Now : " << std::endl;
+ debugPrint("qint-icompose-debug", m, q );
+ Trace("qint-icompose-debug") << std::endl;
+ }
+ }
+
+ Trace("qint-icompose") << "Result : " << std::endl;
+ debugPrint("qint-icompose", m, q );
+ Trace("qint-icompose") << std::endl;
+
+ }else{
+ return false;
+ }
+ }
+ Trace("qint-compose") << "Done i-compose" << std::endl;
+ return true;
+}
+
+
+void QIntDef::construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth ) {
+ d_def.clear();
+ d_def_order.clear();
+ Assert( !fapps.empty() );
+ if( depth==fapps[0].getNumChildren() ){
+ //get representative in model for this term
+ Assert( fapps.size()>=1 );
+ Node r = m->getUsedRepresentative( fapps[0] );
+ d_def_order.push_back( r );
+ }else{
+ std::map< Node, std::vector< Node > > fapp_child;
+ //partition based on evaluations of fapps[1][depth]....fapps[n][depth]
+ for( unsigned i=0; i<fapps.size(); i++ ){
+ Node r = m->getUsedRepresentative( fapps[i][depth] );
+ fapp_child[r].push_back( fapps[i] );
+ }
+ //sort by QIntSort
+ for( std::map< Node, std::vector< Node > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
+ d_def_order.push_back( it->first );
+ }
+ QIntSort qis;
+ qis.m = m;
+ std::sort( d_def_order.begin(), d_def_order.end(), qis );
+ //construct children
+ for( unsigned i=0; i<d_def_order.size(); i++ ){
+ Node n = d_def_order[i];
+ if( i==d_def_order.size()-1 ){
+ d_def_order[i] = m->getMaximum( d_def_order[i].getType() );
+ }
+ Debug("qint-model-debug2") << "Construct for " << n << ", terms = " << fapp_child[n].size() << std::endl;
+ d_def[d_def_order[i]].construct( m, fapp_child[n], depth+1 );
+ }
+ }
+}
+
+Node QIntDef::getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth ) {
+ if( d_def.empty() ){
+ Assert( d_def_order.size()==1 );
+ //must convert to actual domain constant
+ if( d_def_order[0].getType().isSort() ){
+ return m->d_rep_set.d_type_reps[ d_def_order[0].getType() ][ m->getRepId( d_def_order[0] ) ];
+ }else{
+ return m->getUsedRepresentative( d_def_order[0] );
+ }
+ }else{
+ TypeNode tn = vars[depth].getType();
+ Node curr;
+ int rep_id = m->d_rep_set.getNumRepresentatives( tn );
+ for( int i=(int)(d_def_order.size()-1); i>=0; i-- ){
+ int curr_rep_id = i==0 ? 0 : m->getRepId( d_def_order[i-1] )+1;
+ Node ccurr = d_def[d_def_order[i]].getFunctionValue( m, vars, depth+1 );
+ if( curr.isNull() ){
+ curr = ccurr;
+ }else{
+ std::vector< Node > c;
+ Assert( curr_rep_id<rep_id );
+ for( int j=curr_rep_id; j<rep_id; j++ ){
+ c.push_back( vars[depth].eqNode( m->d_rep_set.d_type_reps[tn][j] ) );
+ }
+ Node cond = c.size()==1 ? c[0] : NodeManager::currentNM()->mkNode( OR, c );
+ curr = NodeManager::currentNM()->mkNode( ITE, cond, ccurr, curr );
+ }
+ rep_id = curr_rep_id;
+ }
+ return curr;
+ }
+}
+
+Node QIntDef::evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth ) {
+ if( depth==reps.size() ){
+ Assert( d_def_order.size()==1 );
+ return d_def_order[0];
+ }else{
+ if( d_def.find( reps[depth] )!=d_def.end() ){
+ return d_def[reps[depth]].evaluate_r( m, reps, depth+1 );
+ }else{
+ int ei = getEvIndex( m, reps[depth] );
+ return d_def[d_def_order[ei]].evaluate_r( m, reps, depth+1 );
+ }
+ }
+}
+Node QIntDef::evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth ) {
+ if( depth==n.getNumChildren() ){
+ Assert( d_def_order.size()==1 );
+ return d_def_order[0];
+ }else{
+ Node r = m->getUsedRepresentative( n[depth] );
+ if( d_def.find( r )!=d_def.end() ){
+ return d_def[r].evaluate_n_r( m, n, depth+1 );
+ }else{
+ int ei = getEvIndex( m, r );
+ return d_def[d_def_order[ei]].evaluate_n_r( m, n, depth+1 );
+ }
+ }
+}
+
+
+
+QIntDef * QIntDef::getChild( unsigned i ) {
+ Assert( i<d_def_order.size() );
+ Assert( d_def.find( d_def_order[i] )!=d_def.end() );
+ return &d_def[ d_def_order[i] ];
+}
+
+void QIntDef::debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t ) {
+ /*
+ for( unsigned i=0; i<d_def_order.size(); i++ ){
+ for( int j=0; j<t; j++ ) { Trace(c) << " "; }
+ //Trace(c) << this << " ";
+ Trace(c) << d_def_order[i] << " : " << std::endl;
+ if( d_def.find( d_def_order[i] )!=d_def.end() ){
+ d_def[d_def_order[i]].debugPrint( c, m, t+1 );
+ }
+ }
+ */
+ //if( t==0 ){
+ QIntDefIter qdi( m, q, this );
+ while( !qdi.isFinished() ){
+ qdi.debugPrint( c, t );
+ qdi.increment();
+ }
+ //}
+}
+
+
+QIntDefIter::QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid ) : d_fm( m ), d_q( q ){
+ resetIndex( qid );
+}
+
+void QIntDefIter::debugPrint( const char * c, int t ) {
+ //Trace( c ) << getSize() << " " << d_index_visited.size() << " ";
+ for( int j=0; j<t; j++ ) { Trace(c) << " "; }
+ std::vector< Node > l;
+ std::vector< Node > u;
+ getLowers( l );
+ getUppers( u );
+ QIntDef::debugPrint( c, d_fm, d_q, l, u );
+ Trace( c ) << " -> " << getValue() << std::endl;
+}
+
+void QIntDefIter::resetIndex( QIntDef * qid ){
+ //std::cout << "check : " << qid << " " << qid->d_def_order.size() << " " << qid->d_def.size() << std::endl;
+ if( !qid->d_def.empty() ){
+ //std::cout << "add to visited " << qid << std::endl;
+ d_index.push_back( 0 );
+ d_index_visited.push_back( qid );
+ resetIndex( qid->getChild( 0 ) );
+ }
+}
+
+bool QIntDefIter::increment( int index ) {
+ if( !isFinished() ){
+ index = index==-1 ? (int)(d_index.size()-1) : index;
+ while( (int)(d_index.size()-1)>index ){
+ //std::cout << "remove from visit 1 " << std::endl;
+ d_index.pop_back();
+ d_index_visited.pop_back();
+ }
+ while( index>=0 && d_index[index]>=(int)(d_index_visited[index]->d_def_order.size()-1) ){
+ //std::cout << "remove from visit " << d_index_visited[ d_index_visited.size()-1 ] << std::endl;
+ d_index.pop_back();
+ d_index_visited.pop_back();
+ index--;
+ }
+ if( index>=0 ){
+ //std::cout << "increment at index = " << index << std::endl;
+ d_index[index]++;
+ resetIndex( d_index_visited[index]->getChild( d_index[index] ) );
+ return true;
+ }else{
+ d_index.clear();
+ return false;
+ }
+ }else{
+ return false;
+ }
+}
+
+Node QIntDefIter::getLower( int index ) {
+ if( d_index[index]==0 && !d_q.isNull() ){
+ int pnum = d_fm->getVarOrder( d_q )->getPrevNum( index );
+ if( pnum!=-1 ){
+ return getLower( pnum );
+ }
+ }
+ return d_index_visited[index]->getLower( d_index[index] );
+}
+
+Node QIntDefIter::getUpper( int index ) {
+ return d_index_visited[index]->getUpper( d_index[index] );
+}
+
+void QIntDefIter::getLowers( std::vector< Node >& reps ) {
+ for( unsigned i=0; i<getSize(); i++ ){
+ bool added = false;
+ if( d_index[i]==0 && !d_q.isNull() ){
+ int pnum = d_fm->getVarOrder( d_q )->getPrevNum( i );
+ if( pnum!=-1 ){
+ added = true;
+ reps.push_back( reps[pnum] );
+ }
+ }
+ if( !added ){
+ reps.push_back( getLower( i ) );
+ }
+ }
+}
+
+void QIntDefIter::getUppers( std::vector< Node >& reps ) {
+ for( unsigned i=0; i<getSize(); i++ ){
+ reps.push_back( getUpper( i ) );
+ }
+}
+
+Node QIntDefIter::getValue() {
+ return d_index_visited[ d_index_visited.size()-1 ]->getChild( d_index[d_index.size()-1] )->getValue();
+}
+
+
+//------------------------variable ordering----------------------------
+
+QuantVarOrder::QuantVarOrder( Node q ) : d_q( q ) {
+ d_var_count = 0;
+ initialize( q[1], 0, d_var_occur );
+}
+
+int QuantVarOrder::initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex ) {
+ if( n.getKind()!=FORALL ){
+ //std::vector< Node > vars;
+ //std::vector< int > args;
+ int procVarOn = n.getKind()==APPLY_UF ? 0 : 1;
+ for( int r=0; r<=procVarOn; r++ ){
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( n[i].getKind()==BOUND_VARIABLE && r==procVarOn ){
+ int occ_index = -1;
+ for( unsigned j=0; j<d_var_to_num[n[i]].size(); j++ ){
+ if( d_var_to_num[n[i]][j]>=minVarIndex ){
+ occ_index = d_var_to_num[n[i]][j];
+ }
+ }
+ if( occ_index==-1 ){
+ //need to assign new
+ d_num_to_var[d_var_count] = n[i];
+ if( !d_var_to_num[n[i]].empty() ){
+ int v = d_var_to_num[n[i]][ d_var_to_num[n[i]].size()-1 ];
+ d_num_to_prev_num[ d_var_count ] = v;
+ d_num_to_next_num[ v ] = d_var_count;
+ }
+ d_var_num_index[ d_var_count ] = d_var_to_num[n[i]].size();
+ d_var_to_num[n[i]].push_back( d_var_count );
+ occ_index = d_var_count;
+ d_var_count++;
+ }
+ vindex.d_var_num[i] = occ_index;
+ minVarIndex = occ_index;
+ }else if( r==0 ){
+ minVarIndex = initialize( n[i], minVarIndex, vindex.d_var_index[i] );
+ }
+ }
+ }
+ }
+ return minVarIndex;
+}
+
+bool QuantVarOrder::getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u,
+ std::vector< Node >& inst ) {
+ Debug("qint-var-order-debug2") << "Get for " << d_q << " " << l.size() << " " << u.size() << std::endl;
+ for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
+ Debug("qint-var-order-debug2") << "Get for " << d_q[0][i] << " " << d_var_to_num[d_q[0][i]].size() << std::endl;
+ Node ll = Node::null();
+ Node uu = m->getMaximum( d_q[0][i].getType() );
+ for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){
+ Debug("qint-var-order-debug2") << "Go " << j << std::endl;
+ Node cl = ll;
+ Node cu = uu;
+ int index = d_var_to_num[d_q[0][i]][j];
+ Debug("qint-var-order-debug2") << "Do meet for " << index << "..." << std::endl;
+ Debug("qint-var-order-debug2") << l[index] << " " << u[index] << " " << cl << " " << cu << std::endl;
+ if( !m->doMeet( l[index], u[index], cl, cu, ll, uu ) ){
+ Debug("qint-var-order-debug2") << "FAILED" << std::endl;
+ return false;
+ }
+ Debug("qint-var-order-debug2") << "Result : " << ll << " " << uu << std::endl;
+ }
+ Debug("qint-var-order-debug2") << "Got " << uu << std::endl;
+ inst.push_back( uu );
+ }
+ return true;
+}
+
+void QuantVarOrder::debugPrint( const char * c ) {
+ Trace( c ) << "Variable order for " << d_q << " is : " << std::endl;
+ debugPrint( c, d_q[1], d_var_occur );
+ Trace( c ) << std::endl;
+ for( unsigned i=0; i<d_q[0].getNumChildren(); i++ ){
+ Trace( c ) << d_q[0][i] << " : ";
+ for( unsigned j=0; j<d_var_to_num[d_q[0][i]].size(); j++ ){
+ Trace( c ) << d_var_to_num[d_q[0][i]][j] << " ";
+ }
+ Trace( c ) << std::endl;
+ }
+}
+
+void QuantVarOrder::debugPrint( const char * c, Node n, QIntVarNumIndex& vindex ) {
+ if( n.getKind()==FORALL ){
+ Trace(c) << "NESTED_QUANT";
+ }else{
+ Trace(c) << n.getKind() << "(";
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( i>0 ) Trace( c ) << ",";
+ Trace( c ) << " ";
+ if( n[i].getKind()==BOUND_VARIABLE ){
+ Trace(c) << "VAR[" << vindex.d_var_num[i] << "]";
+ }else{
+ debugPrint( c, n[i], vindex.d_var_index[i] );
+ }
+ if( i==n.getNumChildren()-1 ) Trace( c ) << " ";
+ }
+ Trace(c) << ")";
+ }
+}
+
+QIntervalBuilder::QIntervalBuilder( context::Context* c, QuantifiersEngine* qe ) :
+QModelBuilder( c, qe ){
+ d_true = NodeManager::currentNM()->mkConst( true );
+}
+
+
+//------------------------model construction----------------------------
+
+void QIntervalBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
+ Trace("fmf-qint-debug") << "process build model " << fullModel << std::endl;
+ FirstOrderModel* f = (FirstOrderModel*)m;
+ FirstOrderModelQInt* fm = f->asFirstOrderModelQInt();
+ if( fullModel ){
+ Trace("qint-model") << "Construct model representation..." << std::endl;
+ //make function values
+ for( std::map<Node, QIntDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ if( it->first.getType().getNumChildren()>1 ){
+ Trace("qint-model") << "Construct for " << it->first << "..." << std::endl;
+ m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );
+ }
+ }
+ TheoryEngineModelBuilder::processBuildModel( m, fullModel );
+ //mark that the model has been set
+ fm->markModelSet();
+ //debug the model
+ debugModel( fm );
+ }else{
+ fm->initialize( d_considerAxioms );
+ //process representatives
+ fm->d_rep_id.clear();
+ fm->d_max.clear();
+ fm->d_min.clear();
+ Trace("qint-model") << std::endl << "Making representatives..." << std::endl;
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+ it != fm->d_rep_set.d_type_reps.end(); ++it ){
+ if( it->first.isSort() ){
+ if( it->second.empty() ){
+ std::cout << "Empty rep for " << it->first << std::endl;
+ exit(0);
+ }
+ Trace("qint-model") << "Representatives for " << it->first << " : " << std::endl;
+ for( unsigned i=0; i<it->second.size(); i++ ){
+ Trace("qint-model") << i << " : " << it->second[i] << std::endl;
+ fm->d_rep_id[it->second[i]] = i;
+ }
+ fm->d_min[it->first] = it->second[0];
+ fm->d_max[it->first] = it->second[it->second.size()-1];
+ }else{
+ //TODO: enumerate?
+ }
+ }
+ Trace("qint-model") << std::endl << "Making function definitions..." << std::endl;
+ //construct the models for functions
+ for( std::map<Node, QIntDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ Node f = it->first;
+ Trace("qint-model-debug") << "Building Model for " << f << std::endl;
+ //reset the model
+ //get all (non-redundant) f-applications
+ std::vector< Node > fapps;
+ Trace("qint-model-debug") << "Initial terms: " << std::endl;
+ for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
+ Node n = fm->d_uf_terms[f][i];
+ if( !n.getAttribute(NoMatchAttribute()) ){
+ Trace("qint-model-debug") << " " << n << std::endl;
+ fapps.push_back( n );
+ }
+ }
+ if( fapps.empty() ){
+ //choose arbitrary value
+ Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
+ Trace("qint-model-debug") << "Initial terms empty, add " << mbt << std::endl;
+ fapps.push_back( mbt );
+ }
+ //construct the interval model
+ it->second->construct( fm, fapps );
+ Trace("qint-model-debug") << "Definition for " << f << " : " << std::endl;
+ it->second->debugPrint("qint-model-debug", fm, Node::null() );
+
+ it->second->simplify( fm, Node::null() );
+ Trace("qint-model") << "(Simplified) definition for " << f << " : " << std::endl;
+ it->second->debugPrint("qint-model", fm, Node::null() );
+
+ if( Debug.isOn("qint-model-debug") ){
+ for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
+ Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
+ Debug("qint-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
+ Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
+ }
+ }
+ }
+ }
+}
+
+
+//--------------------model checking---------------------------------------
+
+//do exhaustive instantiation
+bool QIntervalBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
+ Trace("qint-check") << "exhaustive instantiation " << q << " " << effort << std::endl;
+ if (effort==0) {
+
+ FirstOrderModelQInt * fmqint = fm->asFirstOrderModelQInt();
+ QIntDef qid;
+ doCheck( fmqint, q, qid, q[1], fmqint->d_var_order[q]->d_var_occur );
+ //now process entries
+ Trace("qint-inst") << "Interpretation for " << q << " is : " << std::endl;
+ qid.debugPrint( "qint-inst", fmqint, q );
+ Trace("qint-inst") << std::endl;
+ Debug("qint-check-debug2") << "Make iterator..." << std::endl;
+ QIntDefIter qdi( fmqint, q, &qid );
+ while( !qdi.isFinished() ){
+ if( qdi.getValue()!=d_true ){
+ Debug("qint-check-debug2") << "Set up vectors..." << std::endl;
+ std::vector< Node > l;
+ std::vector< Node > u;
+ std::vector< Node > inst;
+ qdi.getLowers( l );
+ qdi.getUppers( u );
+ Debug("qint-check-debug2") << "Get instantiation..." << std::endl;
+ if( fmqint->d_var_order[q]->getInstantiation( fmqint, l, u, inst ) ){
+ Trace("qint-inst") << "** Instantiate with ";
+ //just add the instance
+ InstMatch m;
+ for( unsigned j=0; j<inst.size(); j++) {
+ m.set( d_qe, q, j, inst[j] );
+ Trace("qint-inst") << inst[j] << " ";
+ }
+ Trace("qint-inst") << std::endl;
+ d_triedLemmas++;
+ if( d_qe->addInstantiation( q, m ) ){
+ Trace("qint-inst") << " ...added instantiation." << std::endl;
+ d_addedLemmas++;
+ }else{
+ Trace("qint-inst") << " ...duplicate instantiation" << std::endl;
+ //verify that instantiation is witness for current entry
+ if( Debug.isOn("qint-check-debug2") ){
+ Debug("qint-check-debug2") << "Check if : ";
+ std::vector< Node > exp_inst;
+ for( unsigned i=0; i<fmqint->getOrderedNumVars( q ); i++ ){
+ int index = fmqint->getOrderedVarNumToVarNum( q, i );
+ exp_inst.push_back( inst[ index ] );
+ Debug("qint-check-debug2") << inst[index] << " ";
+ }
+ Debug("qint-check-debug2") << " evaluates to " << qdi.getValue() << std::endl;
+ Assert( qid.evaluate( fmqint, exp_inst )==qdi.getValue() );
+ }
+ }
+ }else{
+ Trace("qint-inst") << "** Spurious instantiation." << std::endl;
+ }
+ }
+ qdi.increment();
+ }
+ }
+ return true;
+}
+
+bool QIntervalBuilder::doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n,
+ QIntVarNumIndex& vindex ) {
+ Assert( n.getKind()!=FORALL );
+ std::map< unsigned, QIntDef > children;
+ std::map< unsigned, Node > bchildren;
+ int varChCount = 0;
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){
+ if( n[i].getKind()==FORALL ){
+ bchildren[i] = Node::null();
+ }else if( n[i].getKind() == BOUND_VARIABLE ){
+ varChCount++;
+ bchildren[i] = n[i];
+ }else if( m->hasTerm( n[i] ) ){
+ bchildren[i] = m->getUsedRepresentative( n[i] );
+ }else{
+ if( !doCheck( m, q, children[i], n[i], vindex.d_var_index[i] ) ){
+ bchildren[i] = Node::null();
+ }
+ }
+ }
+ Trace("qint-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl;
+ if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){
+ Node op = n.getKind() == APPLY_UF ? n.getOperator() : n;
+ //uninterpreted compose
+ qid.construct_compose( m, q, n, m->d_models[op], children, bchildren, varChCount, vindex );
+ }else if( !qid.construct_compose( m, q, n, NULL, children, bchildren, varChCount, vindex ) ){
+ Trace("qint-check-debug") << "** Cannot produce definition for " << n << std::endl;
+ return false;
+ }
+ Trace("qint-check-debug2") << "Definition for " << n << " is : " << std::endl;
+ qid.debugPrint("qint-check-debug2", m, q);
+ qid.simplify( m, q );
+ Trace("qint-check-debug") << "(Simplified) Definition for " << n << " is : " << std::endl;
+ qid.debugPrint("qint-check-debug", m, q);
+ Trace("qint-check-debug") << std::endl;
+ Assert( qid.isTotal( m, q ) );
+ return true;
+}
diff --git a/src/theory/quantifiers/qinterval_builder.h b/src/theory/quantifiers/qinterval_builder.h new file mode 100755 index 000000000..8f48776cc --- /dev/null +++ b/src/theory/quantifiers/qinterval_builder.h @@ -0,0 +1,155 @@ +/********************* */
+/*! \file qinterval_builder.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief qinterval model class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef QINTERVAL_BUILDER
+#define QINTERVAL_BUILDER
+
+#include "theory/quantifiers/model_builder.h"
+#include "theory/quantifiers/first_order_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class FirstOrderModelQInt;
+
+class QIntVarNumIndex
+{
+public:
+ std::map< int, int > d_var_num;
+ std::map< int, QIntVarNumIndex > d_var_index;
+};
+
+class QIntDef
+{
+private:
+ Node evaluate_r( FirstOrderModelQInt * m, std::vector< Node >& reps, unsigned depth );
+ Node evaluate_n_r( FirstOrderModelQInt * m, Node n, unsigned depth );
+ void construct_compose_r( FirstOrderModelQInt * m, Node q,
+ std::vector< Node >& l, std::vector< Node >& u, Node n, QIntDef * f,
+ std::vector< Node >& args,
+ std::map< unsigned, QIntDef >& children,
+ std::map< unsigned, Node >& bchildren,
+ QIntVarNumIndex& vindex,
+ unsigned depth );
+
+ void construct_enum_r( FirstOrderModelQInt * m, Node q, unsigned vn, unsigned depth, Node v );
+ int getEvIndex( FirstOrderModelQInt * m, Node n, bool exc = false );
+ void addEntry( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u,
+ Node v, unsigned depth = 0 );
+ Node simplify_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
+ unsigned depth );
+ bool isTotal_r( FirstOrderModelQInt * m, Node q, std::vector< Node >& il, std::vector< Node >& iu,
+ unsigned depth );
+public:
+ QIntDef(){}
+ std::map< Node, QIntDef > d_def;
+ std::vector< Node > d_def_order;
+
+ void construct( FirstOrderModelQInt * m, std::vector< Node >& fapps, unsigned depth = 0 );
+ bool construct_compose( FirstOrderModelQInt * m, Node q, Node n, QIntDef * f,
+ std::map< unsigned, QIntDef >& children,
+ std::map< unsigned, Node >& bchildren, int varChCount,
+ QIntVarNumIndex& vindex );
+ bool construct_enum( FirstOrderModelQInt * m, Node q, unsigned vn );
+
+ Node evaluate( FirstOrderModelQInt * m, std::vector< Node >& reps ) { return evaluate_r( m, reps, 0 ); }
+ Node evaluate_n( FirstOrderModelQInt * m, Node n ) { return evaluate_n_r( m, n, 0 ); }
+
+ void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, int t = 0 );
+ QIntDef * getChild( unsigned i );
+ Node getValue() { return d_def_order[0]; }
+ Node getLower( unsigned i ) { return i==0 ? Node::null() : d_def_order[i-1]; }
+ Node getUpper( unsigned i ) { return d_def_order[i]; }
+ Node getMaximum() { return d_def_order.empty() ? Node::null() : getUpper( d_def_order.size()-1 ); }
+ int getNumChildren() { return d_def_order.size(); }
+ bool isTotal( FirstOrderModelQInt * m, Node q );
+
+ Node simplify( FirstOrderModelQInt * m, Node q );
+ Node getFunctionValue( FirstOrderModelQInt * m, std::vector< Node >& vars, unsigned depth = 0 );
+
+ static void init_vec( FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );
+ static void debugPrint( const char * c, FirstOrderModelQInt * m, Node q, std::vector< Node >& l, std::vector< Node >& u );
+};
+
+class QIntDefIter {
+private:
+ FirstOrderModelQInt * d_fm;
+ Node d_q;
+ void resetIndex( QIntDef * qid );
+public:
+ QIntDefIter( FirstOrderModelQInt * m, Node q, QIntDef * qid );
+ void debugPrint( const char * c, int t = 0 );
+ std::vector< QIntDef * > d_index_visited;
+ std::vector< int > d_index;
+ bool isFinished() { return d_index.empty(); }
+ bool increment( int index = -1 );
+ unsigned getSize() { return d_index.size(); }
+ Node getLower( int index );
+ Node getUpper( int index );
+ void getLowers( std::vector< Node >& reps );
+ void getUppers( std::vector< Node >& reps );
+ Node getValue();
+};
+
+
+class QuantVarOrder
+{
+private:
+ int initialize( Node n, int minVarIndex, QIntVarNumIndex& vindex );
+ int d_var_count;
+ Node d_q;
+ void debugPrint( const char * c, Node n, QIntVarNumIndex& vindex );
+public:
+ QuantVarOrder( Node q );
+ std::map< int, Node > d_num_to_var;
+ std::map< int, int > d_num_to_prev_num;
+ std::map< int, int > d_num_to_next_num;
+ std::map< Node, std::vector< int > > d_var_to_num;
+ std::map< int, int > d_var_num_index;
+ //std::map< Node, std::map< int, int > > d_var_occur;
+ //int getVarNum( Node n, int arg ) { return d_var_occur[n][arg]; }
+ unsigned getNumVars() { return d_var_count; }
+ Node getVar( int i ) { return d_num_to_var[i]; }
+ int getPrevNum( int i ) { return d_num_to_prev_num.find( i )!=d_num_to_prev_num.end() ? d_num_to_prev_num[i] : -1; }
+ int getNextNum( int i ) { return d_num_to_next_num.find( i )!=d_num_to_next_num.end() ? d_num_to_next_num[i] : -1; }
+ int getVarNumIndex( int i ) { return d_var_num_index[i]; }
+ bool getInstantiation( FirstOrderModelQInt * m, std::vector< Node >& l, std::vector< Node >& u,
+ std::vector< Node >& inst );
+ void debugPrint( const char * c );
+ QIntVarNumIndex d_var_occur;
+};
+
+class QIntervalBuilder : public QModelBuilder
+{
+private:
+ Node d_true;
+ bool doCheck( FirstOrderModelQInt * m, Node q, QIntDef & qid, Node n,
+ QIntVarNumIndex& vindex );
+public:
+ QIntervalBuilder( context::Context* c, QuantifiersEngine* qe );
+ //process build model
+ void processBuildModel(TheoryModel* m, bool fullModel);
+ //do exhaustive instantiation
+ bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
+};
+
+
+}
+}
+}
+
+#endif
\ No newline at end of file diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index e18a4e0dc..6b1368be1 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -146,6 +146,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ if( !d_func_map_trie[ it->first ].addTerm( d_quantEngine, n ) ){ NoMatchAttribute nma; n.setAttribute(nma,true); + Debug("term-db-cong") << n << " is redundant." << std::endl; congruentCount++; }else{ nonCongruentCount++; @@ -173,6 +174,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ if( !d_pred_map_trie[i][op].addTerm( d_quantEngine, en ) ){ NoMatchAttribute nma; en.setAttribute(nma,true); + Debug("term-db-cong") << en << " is redundant." << std::endl; congruentCount++; }else{ nonCongruentCount++; @@ -222,10 +224,14 @@ Node TermDb::getModelBasisOpTerm( Node op ){ TypeNode t = op.getType(); std::vector< Node > children; children.push_back( op ); - for( size_t i=0; i<t.getNumChildren()-1; i++ ){ + for( int i=0; i<(int)(t.getNumChildren()-1); i++ ){ children.push_back( getModelBasisTerm( t[i] ) ); } - d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + if( children.size()==1 ){ + d_model_basis_op_term[op] = op; + }else{ + d_model_basis_op_term[op] = NodeManager::currentNM()->mkNode( APPLY_UF, children ); + } } return d_model_basis_op_term[op]; } |