diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-23 16:45:47 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-23 16:45:47 -0500 |
commit | fbc81b67ac1cfeb3afe37f3299180177faaa1ca6 (patch) | |
tree | 69b3028b333262b414ed188d1f575012793e0e2b /src/theory/quantifiers | |
parent | fee510eacd6ea9d35906218ce3d4b88f7d86f8b1 (diff) |
Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/Makefile.am | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/bounded_integers.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 82 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 65 | ||||
-rwxr-xr-x | src/theory/quantifiers/full_model_check.cpp | 571 | ||||
-rwxr-xr-x | src/theory/quantifiers/full_model_check.h | 96 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 157 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 31 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 198 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.h | 54 |
12 files changed, 534 insertions, 737 deletions
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am index 92d780be4..60f2ee7f7 100644 --- a/src/theory/quantifiers/Makefile.am +++ b/src/theory/quantifiers/Makefile.am @@ -23,8 +23,6 @@ libquantifiers_la_SOURCES = \ model_engine.cpp \ modes.cpp \ modes.h \ - relevant_domain.h \ - relevant_domain.cpp \ term_database.h \ term_database.cpp \ first_order_model.h \ diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index 4492e6d2d..e33cd2131 100755 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -355,8 +355,8 @@ void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node }
}
Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl;
- l = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), l );
- u = d_quantEngine->getModelEngine()->getModelBuilder()->getCurrentModelValue( d_quantEngine->getModel(), u );
+ l = d_quantEngine->getModel()->getCurrentModelValue( l );
+ u = d_quantEngine->getModel()->getCurrentModelValue( u );
Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl;
return;
}
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index a11729519..cf4381c02 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -38,15 +38,34 @@ void FirstOrderModel::assertQuantifier( Node n ){ } } -void FirstOrderModel::reset(){ - TheoryModel::reset(); +Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) { + std::vector< Node > children; + if( n.getNumChildren()>0 ){ + if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.push_back( n.getOperator() ); + } + for (unsigned i=0; i<n.getNumChildren(); i++) { + Node nc = getCurrentModelValue( n[i], partial ); + if (nc.isNull()) { + return Node::null(); + }else{ + children.push_back( nc ); + } + } + if( n.getKind()==APPLY_UF ){ + return getCurrentUfModelValue( n, children, partial ); + }else{ + Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children ); + nn = Rewriter::rewrite( nn ); + return nn; + } + }else{ + return getRepresentative(n); + } } -void FirstOrderModel::initialize( bool considerAxioms ){ - //rebuild models - d_uf_model_tree.clear(); - d_uf_model_gen.clear(); - d_array_model.clear(); +void FirstOrderModel::initialize( bool considerAxioms ) { + processInitialize(); //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++ ){ @@ -59,6 +78,23 @@ void FirstOrderModel::initialize( bool considerAxioms ){ } void FirstOrderModel::initializeModelForTerm( Node n ){ + processInitializeModelForTerm( n ); + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + initializeModelForTerm( n[i] ); + } +} + +FirstOrderModelIG::FirstOrderModelIG(context::Context* c, std::string name) : FirstOrderModel(c,name) { + +} + +void FirstOrderModelIG::processInitialize(){ + //rebuild models + d_uf_model_tree.clear(); + d_uf_model_gen.clear(); +} + +void FirstOrderModelIG::processInitializeModelForTerm( Node n ){ if( n.getKind()==APPLY_UF ){ Node op = n.getOperator(); if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){ @@ -82,14 +118,11 @@ void FirstOrderModel::initializeModelForTerm( Node n ){ } } */ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - initializeModelForTerm( n[i] ); - } } //for evaluation of quantifier bodies -void FirstOrderModel::resetEvaluate(){ +void FirstOrderModelIG::resetEvaluate(){ d_eval_uf_use_default.clear(); d_eval_uf_model.clear(); d_eval_term_index_order.clear(); @@ -107,7 +140,7 @@ void FirstOrderModel::resetEvaluate(){ // if eVal = 0, then n' cannot be proven to be equal to phaseReq // if eVal is not 0, then // each n{ri->d_index[0]/x_0...ri->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model -int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ +int FirstOrderModelIG::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ ++d_eval_formulas; //Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl; //Notice() << "Eval " << n << std::endl; @@ -226,7 +259,7 @@ int FirstOrderModel::evaluate( Node n, int& depIndex, RepSetIterator* ri ){ } } -Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ +Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ //Message() << "Eval term " << n << std::endl; Node val; depIndex = ri->getNumTerms()-1; @@ -342,7 +375,7 @@ Node FirstOrderModel::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri ){ return val; } -Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){ +Node FirstOrderModelIG::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex, RepSetIterator* ri ){ depIndex = -1; if( n.getNumChildren()==0 ){ return n; @@ -372,14 +405,14 @@ Node FirstOrderModel::evaluateTermDefault( Node n, int& depIndex, std::vector< i } } -void FirstOrderModel::clearEvalFailed( int index ){ +void FirstOrderModelIG::clearEvalFailed( int index ){ for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){ d_eval_failed[ d_eval_failed_lits[index][i] ] = false; } d_eval_failed_lits[index].clear(); } -void FirstOrderModel::makeEvalUfModel( Node n ){ +void FirstOrderModelIG::makeEvalUfModel( Node n ){ if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){ makeEvalUfIndexOrder( n ); if( !d_eval_uf_use_default[n] ){ @@ -423,7 +456,7 @@ struct sortGetMaxVariableNum { bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));} }; -void FirstOrderModel::makeEvalUfIndexOrder( Node n ){ +void FirstOrderModelIG::makeEvalUfIndexOrder( Node n ){ if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){ #ifdef USE_INDEX_ORDERING //sort arguments in order of least significant vs. most significant variable in default ordering @@ -460,3 +493,18 @@ void FirstOrderModel::makeEvalUfIndexOrder( Node n ){ #endif } } + +Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) { + std::vector< Node > children; + children.push_back(n.getOperator()); + children.insert(children.end(), args.begin(), args.end()); + Node nv = NodeManager::currentNM()->mkNode(APPLY_UF, children); + //make the term model specifically for nv + makeEvalUfModel( nv ); + int argDepIndex; + if( d_eval_uf_use_default[nv] ){ + return d_uf_model_tree[ n.getOperator() ].getValue( this, nv, argDepIndex ); + }else{ + return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex ); + } +}
\ No newline at end of file diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 76f21e19c..491e97097 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -19,7 +19,6 @@ #include "theory/model.h" #include "theory/uf/theory_uf_model.h" -#include "theory/arrays/theory_arrays_model.h" namespace CVC4 { namespace theory { @@ -30,33 +29,22 @@ namespace quantifiers{ class TermDb; +class FirstOrderModelIG; +namespace fmcheck { + class FirstOrderModelFmc; +} + class FirstOrderModel : public TheoryModel { private: - //for initialize model - void initializeModelForTerm( Node n ); /** 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; -public: //for Theory UF: - //models for each UF operator - std::map< Node, uf::UfModelTree > d_uf_model_tree; - //model generators - std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen; -private: - //map from terms to the models used to calculate their value - std::map< Node, bool > d_eval_uf_use_default; - std::map< Node, uf::UfModelTree > d_eval_uf_model; - void makeEvalUfModel( Node n ); - //index ordering to use for each term - std::map< Node, std::vector< int > > d_eval_term_index_order; - void makeEvalUfIndexOrder( Node n ); -public: //for Theory Arrays: - //default value for each non-store array - std::map< Node, arrays::ArrayModel > d_array_model; + /** get current model value */ + virtual Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) = 0; public: //for Theory Quantifiers: /** assert quantifier */ void assertQuantifier( Node n ); @@ -66,19 +54,51 @@ public: //for Theory Quantifiers: Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; } /** bool axiom asserted */ bool isAxiomAsserted() { return d_axiom_asserted; } + /** initialize model for term */ + void initializeModelForTerm( Node n ); + virtual void processInitializeModelForTerm( Node n ) = 0; public: FirstOrderModel( context::Context* c, std::string name ); virtual ~FirstOrderModel(){} - // reset the model - void reset(); + virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; } + virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; } // initialize the model void initialize( bool considerAxioms = true ); + virtual void processInitialize() = 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 ); +};/* class FirstOrderModel */ + + +class FirstOrderModelIG : public FirstOrderModel +{ +public: //for Theory UF: + //models for each UF operator + std::map< Node, uf::UfModelTree > d_uf_model_tree; + //model generators + std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen; +private: + //map from terms to the models used to calculate their value + std::map< Node, bool > d_eval_uf_use_default; + std::map< Node, uf::UfModelTree > d_eval_uf_model; + void makeEvalUfModel( Node n ); + //index ordering to use for each term + std::map< Node, std::vector< int > > d_eval_term_index_order; + void makeEvalUfIndexOrder( Node n ); + /** get current model value */ + 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 * asFirstOrderModelIG() { return this; } + // initialize the model + void processInitialize(); + //for initialize model + void processInitializeModelForTerm( Node n ); /** reset evaluation */ void resetEvaluate(); /** evaluate functions */ @@ -97,7 +117,8 @@ private: void clearEvalFailed( int index ); std::map< Node, bool > d_eval_failed; std::map< int, std::vector< Node > > d_eval_failed_lits; -};/* class FirstOrderModel */ +}; + }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index b5d4648a1..2513cb08e 100755 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -24,8 +24,17 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::theory::inst;
using namespace CVC4::theory::quantifiers::fmcheck;
+struct ModelBasisArgSort
+{
+ std::vector< Node > d_terms;
+ bool operator() (int i,int j) {
+ return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <
+ d_terms[j].getAttribute(ModelBasisArgAttribute()) );
+ }
+};
-bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) {
+
+bool EntryTrie::hasGeneralization( FirstOrderModelFmc * m, Node c, int index ) {
if (index==(int)c.getNumChildren()) {
return d_data!=-1;
}else{
@@ -44,7 +53,7 @@ bool EntryTrie::hasGeneralization( FullModelChecker * m, Node c, int index ) { }
}
-int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index ) {
+int EntryTrie::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index ) {
if (index==(int)inst.size()) {
return d_data;
}else{
@@ -64,7 +73,7 @@ int EntryTrie::getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & }
}
-void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int index ) {
+void EntryTrie::addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index ) {
if (index==(int)c.getNumChildren()) {
if(d_data==-1) {
d_data = data;
@@ -75,7 +84,7 @@ void EntryTrie::addEntry( FullModelChecker * m, Node c, Node v, int data, int in }
}
-void EntryTrie::getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {
+void EntryTrie::getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index, bool is_gen ) {
if (index==(int)c.getNumChildren()) {
if( d_data!=-1) {
if( is_gen ){
@@ -101,13 +110,8 @@ void EntryTrie::getEntries( FullModelChecker * m, Node c, std::vector<int> & com }
}
-bool EntryTrie::getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index) {
-
- return false;
-}
-
-bool Def::addEntry( FullModelChecker * m, Node c, Node v) {
+bool Def::addEntry( FirstOrderModelFmc * m, Node c, Node v) {
if (!d_et.hasGeneralization(m, c)) {
int newIndex = (int)d_cond.size();
if (!d_has_simplified) {
@@ -139,7 +143,7 @@ bool Def::addEntry( FullModelChecker * m, Node c, Node v) { }
}
-Node Def::evaluate( FullModelChecker * m, std::vector<Node>& inst ) {
+Node Def::evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
int gindex = d_et.getGeneralizationIndex(m, inst);
if (gindex!=-1) {
return d_value[gindex];
@@ -148,11 +152,11 @@ Node Def::evaluate( FullModelChecker * m, std::vector<Node>& inst ) { }
}
-int Def::getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst ) {
+int Def::getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst ) {
return d_et.getGeneralizationIndex(m, inst);
}
-void Def::simplify(FullModelChecker * m) {
+void Def::simplify(FirstOrderModelFmc * m) {
d_has_simplified = true;
std::vector< Node > cond;
cond.insert( cond.end(), d_cond.begin(), d_cond.end() );
@@ -186,16 +190,128 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) { }
+
+FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
+FirstOrderModel(c, name), d_qe(qe){
+
+}
+
+Node FirstOrderModelFmc::getUsedRepresentative(Node n) {
+ //Assert( fm->hasTerm(n) );
+ TypeNode tn = n.getType();
+ if( tn.isBoolean() ){
+ return areEqual(n, d_true) ? d_true : d_false;
+ }else{
+ Node r = getRepresentative(n);
+ if (r==d_model_basis_rep[tn]) {
+ r = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+ }
+ return r;
+ }
+}
+
+Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
+ Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;
+ for(unsigned i=0; i<args.size(); i++) {
+ args[i] = getUsedRepresentative(args[i]);
+ }
+ Assert( n.getKind()==APPLY_UF );
+ return d_models[n.getOperator()]->evaluate(this, args);
+}
+
+void FirstOrderModelFmc::processInitialize() {
+ for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
+ it->second->reset();
+ }
+ d_model_basis_rep.clear();
+}
+
+void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
+ if( n.getKind()==APPLY_UF ){
+ if( d_models.find(n.getOperator())==d_models.end()) {
+ d_models[n.getOperator()] = new Def;
+ }
+ }
+}
+
+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());
+}
+
+Node FirstOrderModelFmc::getStar(TypeNode tn) {
+ if( d_type_star.find(tn)==d_type_star.end() ){
+ Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );
+ d_type_star[tn] = st;
+ }
+ return d_type_star[tn];
+}
+
+bool FirstOrderModelFmc::isModelBasisTerm(Node n) {
+ return n==getModelBasisTerm(n.getType());
+}
+
+Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) {
+ return d_qe->getTermDatabase()->getModelBasisTerm(tn);
+}
+
+Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
+ 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);
+ vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
+ }
+ Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
+ Node curr;
+ for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
+ Node v = getUsedRepresentative( d_models[op]->d_value[i] );
+ if( curr.isNull() ){
+ curr = v;
+ }else{
+ //make the condition
+ Node cond = d_models[op]->d_cond[i];
+ std::vector< Node > children;
+ for( unsigned j=0; j<cond.getNumChildren(); j++) {
+ if (!isStar(cond[j])){
+ Node c = getUsedRepresentative( cond[j] );
+ children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
+ }
+ }
+ Assert( !children.empty() );
+ Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
+ curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );
+ }
+ }
+ curr = Rewriter::rewrite( curr );
+ return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
+}
+
+
+
FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :
QModelBuilder( c, qe ){
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
-
void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
d_addedLemmas = 0;
- FirstOrderModel* fm = (FirstOrderModel*)m;
+ FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
if( fullModel ){
//make function values
for( std::map< Node, std::vector< Node > >::iterator it = m->d_uf_terms.begin(); it != m->d_uf_terms.end(); ++it ){
@@ -204,15 +320,13 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ TheoryEngineModelBuilder::processBuildModel( m, fullModel );
//mark that the model has been set
fm->markModelSet();
+ //debug the model
+ debugModel( fm );
}else{
Trace("fmc") << "---Full Model Check reset() " << std::endl;
- for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
- it->second->reset();
- }
+ fm->initialize( d_considerAxioms );
d_quant_models.clear();
- d_models_init.clear();
d_rep_ids.clear();
- d_model_basis_rep.clear();
d_star_insts.clear();
//process representatives
for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
@@ -220,13 +334,11 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ if( it->first.isSort() ){
Trace("fmc") << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(it->first);
- Node rmbt = fm->getRepresentative(mbt);
+ Node rmbt = fm->getUsedRepresentative( mbt);
int mbt_index = -1;
Trace("fmc") << " Model basis term : " << mbt << std::endl;
for( size_t a=0; a<it->second.size(); a++ ){
- //Node r2 = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getRepresentative( it->second[a] );
- //Node ir = ((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getInternalRepresentative( it->second[a], Node::null(), 0 );
- Node r = fm->getRepresentative( it->second[a] );
+ Node r = fm->getUsedRepresentative( it->second[a] );
std::vector< Node > eqc;
((EqualityQueryQuantifiersEngine*)d_qe->getEqualityQuery())->getEquivalenceClass( r, eqc );
Trace("fmc-model-debug") << " " << (it->second[a]==r) << (r==mbt);
@@ -241,7 +353,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ //if this is the model basis eqc, replace with actual model basis term
if (r==rmbt || (mbt_index==-1 && a==(it->second.size()-1))) {
- d_model_basis_rep[it->first] = r;
+ fm->d_model_basis_rep[it->first] = r;
r = mbt;
mbt_index = a;
}
@@ -257,150 +369,63 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){ }
}
}
- }
-}
-
-Node FullModelChecker::getRepresentative(FirstOrderModel * fm, Node n) {
- //Assert( fm->hasTerm(n) );
- TypeNode tn = n.getType();
- if( tn.isBoolean() ){
- return fm->areEqual(n, d_true) ? d_true : d_false;
- }else{
- Node r = fm->getRepresentative(n);
- if (r==d_model_basis_rep[tn]) {
- r = d_qe->getTermDatabase()->getModelBasisTerm(tn);
- }
- return r;
- }
-}
-
-struct ModelBasisArgSort
-{
- std::vector< Node > d_terms;
- bool operator() (int i,int j) {
- return (d_terms[i].getAttribute(ModelBasisArgAttribute()) <
- d_terms[j].getAttribute(ModelBasisArgAttribute()) );
- }
-};
-
-void FullModelChecker::addEntry( FirstOrderModel * fm, Node op, Node c, Node v,
- std::vector< Node > & conds,
- std::vector< Node > & values,
- std::vector< Node > & entry_conds ) {
- std::vector< Node > children;
- std::vector< Node > entry_children;
- children.push_back(op);
- entry_children.push_back(op);
- bool hasNonStar = false;
- for( unsigned i=0; i<c.getNumChildren(); i++) {
- Node ri = getRepresentative(fm, c[i]);
- children.push_back(ri);
- if (isModelBasisTerm(ri)) {
- ri = getStar( ri.getType() );
- }else{
- hasNonStar = true;
- }
- entry_children.push_back(ri);
- }
- Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
- Node nv = getRepresentative(fm, v);
- Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
- if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
- Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
- conds.push_back(n);
- values.push_back(nv);
- entry_conds.push_back(en);
- }
-}
-
-Def * FullModelChecker::getModel(FirstOrderModel * fm, Node op) {
- if( d_models_init.find(op)==d_models_init.end() ){
- if( d_models.find(op)==d_models.end() ){
- d_models[op] = new Def;
- }
- //reset the model
- d_models[op]->reset();
-
- std::vector< Node > conds;
- std::vector< Node > values;
- std::vector< Node > entry_conds;
- Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
- Node r = getRepresentative(fm, fm->d_uf_terms[op][i]);
- Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;
- }
- Trace("fmc-model-debug") << std::endl;
- //initialize the model
- /*
- for( int j=0; j<2; j++ ){
- for( int k=1; k>=0; k-- ){
- Trace("fmc-model-debug")<< "Set values " << j << " " << k << " : " << std::endl;
- for( std::map< Node, Node >::iterator it = fm->d_uf_model_gen[op].d_set_values[j][k].begin();
- it != fm->d_uf_model_gen[op].d_set_values[j][k].end(); ++it ){
- Trace("fmc-model-debug") << " process : " << it->first << " -> " << it->second << std::endl;
- if( j==1 ){
- addEntry(fm, op, it->first, it->second, conds, values, entry_conds);
- }
+ //now, make models
+ for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+ Node op = it->first;
+ //reset the model
+ fm->d_models[op]->reset();
+
+ std::vector< Node > conds;
+ std::vector< Node > values;
+ std::vector< Node > entry_conds;
+ Trace("fmc-model-debug") << fm->d_uf_terms[op].size() << " model values for " << op << " ... " << std::endl;
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+ Node r = fm->getUsedRepresentative(fm->d_uf_terms[op][i]);
+ Trace("fmc-model-debug") << fm->d_uf_terms[op][i] << " -> " << r << std::endl;
+ }
+ Trace("fmc-model-debug") << std::endl;
+ //initialize the model
+ for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
+ Node n = fm->d_uf_terms[op][i];
+ if( !n.getAttribute(NoMatchAttribute()) ){
+ addEntry(fm, op, n, n, conds, values, entry_conds);
}
}
- }
- */
- for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){
- Node n = fm->d_uf_terms[op][i];
- if( !n.getAttribute(NoMatchAttribute()) ){
- addEntry(fm, op, n, n, conds, values, entry_conds);
+ Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
+ //add default value
+ if( fm->hasTerm( nmb ) ){
+ Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
+ addEntry(fm, op, nmb, nmb, conds, values, entry_conds);
+ }else{
+ Node vmb = fm->getSomeDomainElement(nmb.getType());
+ Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
+ Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
+ addEntry(fm, op, nmb, vmb, conds, values, entry_conds);
}
- }
- Node nmb = d_qe->getTermDatabase()->getModelBasisOpTerm(op);
- //add default value
- if( fm->hasTerm( nmb ) ){
- Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
- addEntry(fm, op, nmb, nmb, conds, values, entry_conds);
- }else{
- Node vmb = getSomeDomainElement( fm, nmb.getType() );
- Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
- Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
- addEntry(fm, op, nmb, vmb, conds, values, entry_conds);
- }
-
- //sort based on # default arguments
- std::vector< int > indices;
- ModelBasisArgSort mbas;
- for (int i=0; i<(int)conds.size(); i++) {
- d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
- mbas.d_terms.push_back(conds[i]);
- indices.push_back(i);
- }
- std::sort( indices.begin(), indices.end(), mbas );
+ //sort based on # default arguments
+ std::vector< int > indices;
+ ModelBasisArgSort mbas;
+ for (int i=0; i<(int)conds.size(); i++) {
+ d_qe->getTermDatabase()->computeModelBasisArgAttribute( conds[i] );
+ mbas.d_terms.push_back(conds[i]);
+ indices.push_back(i);
+ }
+ std::sort( indices.begin(), indices.end(), mbas );
- for (int i=0; i<(int)indices.size(); i++) {
- d_models[op]->addEntry(this, entry_conds[indices[i]], values[indices[i]]);
- }
- d_models[op]->debugPrint("fmc-model", op, this);
- Trace("fmc-model") << std::endl;
- d_models[op]->simplify( this );
- Trace("fmc-model-simplify") << "After simplification : " << std::endl;
- d_models[op]->debugPrint("fmc-model-simplify", op, this);
- Trace("fmc-model-simplify") << std::endl;
+ for (int i=0; i<(int)indices.size(); i++) {
+ fm->d_models[op]->addEntry(fm, entry_conds[indices[i]], values[indices[i]]);
+ }
+ fm->d_models[op]->debugPrint("fmc-model", op, this);
+ Trace("fmc-model") << std::endl;
- d_models_init[op] = true;
+ fm->d_models[op]->simplify( fm );
+ Trace("fmc-model-simplify") << "After simplification : " << std::endl;
+ fm->d_models[op]->debugPrint("fmc-model-simplify", op, this);
+ Trace("fmc-model-simplify") << std::endl;
+ }
}
- return d_models[op];
-}
-
-
-bool FullModelChecker::isStar(Node n) {
- return n==getStar(n.getType());
-}
-
-bool FullModelChecker::isModelBasisTerm(Node n) {
- return n==getModelBasisTerm(n.getType());
-}
-
-Node FullModelChecker::getModelBasisTerm(TypeNode tn) {
- return d_qe->getTermDatabase()->getModelBasisTerm(tn);
}
void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) {
@@ -413,10 +438,11 @@ void FullModelChecker::debugPrintCond(const char * tr, Node n, bool dispStar) { }
void FullModelChecker::debugPrint(const char * tr, Node n, bool dispStar) {
+ FirstOrderModelFmc * fm = (FirstOrderModelFmc *)d_qe->getModel();
if( n.isNull() ){
Trace(tr) << "null";
}
- else if(isStar(n) && dispStar) {
+ else if(fm->isStar(n) && dispStar) {
Trace(tr) << "*";
}else{
TypeNode tn = n.getType();
@@ -438,6 +464,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, if (!options::fmfModelBasedInst()) {
return false;
}else{
+ FirstOrderModelFmc * fmfmc = fm->asFirstOrderModelFmc();
if (effort==0) {
//register the quantifier
if (d_quant_cond.find(f)==d_quant_cond.end()) {
@@ -452,7 +479,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, }
//model check the quantifier
- doCheck(fm, f, d_quant_models[f], f[1]);
+ doCheck(fmfmc, f, d_quant_models[f], f[1]);
Trace("fmc") << "Definition for quantifier " << f << " is : " << std::endl;
d_quant_models[f].debugPrint("fmc", Node::null(), this);
Trace("fmc") << std::endl;
@@ -463,9 +490,9 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, bool hasStar = false;
std::vector< Node > inst;
for (unsigned j=0; j<d_quant_models[f].d_cond[i].getNumChildren(); j++) {
- if (isStar(d_quant_models[f].d_cond[i][j])) {
+ if (fmfmc->isStar(d_quant_models[f].d_cond[i][j])) {
hasStar = true;
- inst.push_back(getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
+ inst.push_back(fmfmc->getModelBasisTerm(d_quant_models[f].d_cond[i][j].getType()));
}else{
inst.push_back(d_quant_models[f].d_cond[i][j]);
}
@@ -473,14 +500,14 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, bool addInst = true;
if( hasStar ){
//try obvious (specified by inst)
- Node ev = d_quant_models[f].evaluate(this, inst);
+ Node ev = d_quant_models[f].evaluate(fmfmc, inst);
if (ev==d_true) {
addInst = false;
}
}else{
//for debugging
if (Trace.isOn("fmc-test-inst")) {
- Node ev = d_quant_models[f].evaluate(this, inst);
+ Node ev = d_quant_models[f].evaluate(fmfmc, inst);
if( ev==d_true ){
std::cout << "WARNING: instantiation was true! " << f << " " << d_quant_models[f].d_cond[i] << std::endl;
exit(0);
@@ -518,8 +545,8 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, for( int i=(d_star_insts[f].size()-1); i>=0; i--) {
//get witness for d_star_insts[f][i]
int j = d_star_insts[f][i];
- if( temp.addEntry( this, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
- int lem = exhaustiveInstantiate(fm, f, d_quant_models[f].d_cond[j], j );
+ if( temp.addEntry(fmfmc, d_quant_models[f].d_cond[j], d_quant_models[f].d_value[j] ) ){
+ int lem = exhaustiveInstantiate(fmfmc, f, d_quant_models[f].d_cond[j], j );
if( lem==-1 ){
//something went wrong, resort to exhaustive instantiation
return false;
@@ -534,7 +561,7 @@ bool FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, }
}
-int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index) {
+int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) {
int addedLemmas = 0;
RepSetIterator riter( d_qe, &(fm->d_rep_set) );
Trace("fmc-exh") << "Exhaustive instantiate based on index " << c_index << " : " << c << " ";
@@ -546,7 +573,7 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c TypeNode tn = c[i].getType();
if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
//RepDomain rd;
- if( isStar(c[i]) ){
+ if( fm->isStar(c[i]) ){
//add the full range
//for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();
// it != d_rep_ids[tn].end(); ++it ){
@@ -573,13 +600,13 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c std::vector< Node > inst;
for( int i=0; i<riter.getNumTerms(); i++ ){
//m.set( d_quantEngine, f, riter.d_index_order[i], riter.getTerm( i ) );
- Node r = getRepresentative( fm, riter.getTerm( i ) );
+ Node r = fm->getUsedRepresentative( riter.getTerm( i ) );
debugPrint("fmc-exh-debug", r);
Trace("fmc-exh-debug") << " ";
inst.push_back(r);
}
- int ev_index = d_quant_models[f].getGeneralizationIndex(this, inst);
+ int ev_index = d_quant_models[f].getGeneralizationIndex(fm, inst);
Trace("fmc-exh-debug") << ", index = " << ev_index;
Node ev = ev_index==-1 ? Node::null() : d_quant_models[f].d_value[ev_index];
if (ev!=d_true) {
@@ -600,19 +627,19 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c return addedLemmas;
}
-void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) {
+void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n ) {
Trace("fmc-debug") << "Check " << n << " " << n.getKind() << std::endl;
if( n.getKind() == kind::BOUND_VARIABLE ){
- d.addEntry(this, mkCondDefault(f), n);
+ d.addEntry(fm, mkCondDefault(fm, f), n);
Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl;
}
else if( n.getNumChildren()==0 ){
Node r = n;
if( !fm->hasTerm(n) ){
- r = getSomeDomainElement( fm, n.getType() );
+ r = fm->getSomeDomainElement(n.getType() );
}
- r = getRepresentative(fm, r);
- d.addEntry(this, mkCondDefault(f), r);
+ r = fm->getUsedRepresentative( r);
+ d.addEntry(fm, mkCondDefault(fm, f), r);
}
else if( n.getKind() == kind::NOT ){
//just do directly
@@ -620,7 +647,7 @@ void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) { doNegate( d );
}
else if( n.getKind() == kind::FORALL ){
- d.addEntry(this, mkCondDefault(f), Node::null());
+ d.addEntry(fm, mkCondDefault(fm, f), Node::null());
}
else{
std::vector< int > var_ch;
@@ -655,13 +682,13 @@ void FullModelChecker::doCheck(FirstOrderModel * fm, Node f, Def & d, Node n ) { }else{
Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;
std::vector< Node > cond;
- mkCondDefaultVec(f, cond);
+ mkCondDefaultVec(fm, f, cond);
std::vector< Node > val;
//interpreted compose
doInterpretedCompose( fm, f, d, n, children, 0, cond, val );
}
}
- d.simplify(this);
+ d.simplify(fm);
}
Trace("fmc-debug") << "Definition for " << n << " is : " << std::endl;
d.debugPrint("fmc-debug", Node::null(), this);
@@ -676,62 +703,61 @@ void FullModelChecker::doNegate( Def & dc ) { }
}
-void FullModelChecker::doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq ) {
+void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq ) {
std::vector<Node> cond;
- mkCondDefaultVec(f, cond);
+ mkCondDefaultVec(fm, f, cond);
if (eq[0]==eq[1]){
- d.addEntry(this, mkCond(cond), d_true);
+ d.addEntry(fm, mkCond(cond), d_true);
}else{
int j = getVariableId(f, eq[0]);
int k = getVariableId(f, eq[1]);
TypeNode tn = eq[0].getType();
if( !fm->d_rep_set.hasType( tn ) ){
- getSomeDomainElement( fm, tn ); //to verify the type is initialized
+ fm->getSomeDomainElement( tn ); //to verify the type is initialized
}
for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {
- Node r = getRepresentative( fm, fm->d_rep_set.d_type_reps[tn][i] );
+ Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );
cond[j+1] = r;
cond[k+1] = r;
- d.addEntry( this, mkCond(cond), d_true);
+ d.addEntry( fm, mkCond(cond), d_true);
}
- d.addEntry(this, mkCondDefault(f), d_false);
+ d.addEntry( fm, mkCondDefault(fm, f), d_false);
}
}
-void FullModelChecker::doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v) {
+void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v) {
int j = getVariableId(f, v);
for (unsigned i=0; i<dc.d_cond.size(); i++) {
Node val = dc.d_value[i];
if( dc.d_cond[i][j]!=val ){
- if (isStar(dc.d_cond[i][j])) {
+ if (fm->isStar(dc.d_cond[i][j])) {
std::vector<Node> cond;
mkCondVec(dc.d_cond[i],cond);
cond[j+1] = val;
- d.addEntry(this, mkCond(cond), d_true);
- cond[j+1] = getStar(val.getType());
- d.addEntry(this, mkCond(cond), d_false);
+ d.addEntry(fm, mkCond(cond), d_true);
+ cond[j+1] = fm->getStar(val.getType());
+ d.addEntry(fm, mkCond(cond), d_false);
}else{
- d.addEntry( this, dc.d_cond[i], d_false);
+ d.addEntry( fm, dc.d_cond[i], d_false);
}
}else{
- d.addEntry( this, dc.d_cond[i], d_true);
+ d.addEntry( fm, dc.d_cond[i], d_true);
}
}
}
-void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {
- getModel(fm, op);
+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node op, std::vector< Def > & dc ) {
Trace("fmc-uf-debug") << "Definition : " << std::endl;
- d_models[op]->debugPrint("fmc-uf-debug", op, this);
+ fm->d_models[op]->debugPrint("fmc-uf-debug", op, this);
Trace("fmc-uf-debug") << std::endl;
std::vector< Node > cond;
- mkCondDefaultVec(f, cond);
+ mkCondDefaultVec(fm, f, cond);
std::vector< Node > val;
doUninterpretedCompose( fm, f, op, d, dc, 0, cond, val);
}
-void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,
+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,
std::vector< Def > & dc, int index,
std::vector< Node > & cond, std::vector<Node> & val ) {
Trace("fmc-uf-process") << "process at " << index << std::endl;
@@ -743,19 +769,19 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Nod if (index==(int)dc.size()) {
//we have an entry, now do actual compose
std::map< int, Node > entries;
- doUninterpretedCompose2( fm, f, entries, 0, cond, val, d_models[op]->d_et);
+ doUninterpretedCompose2( fm, f, entries, 0, cond, val, fm->d_models[op]->d_et);
//add them to the definition
- for( unsigned e=0; e<d_models[op]->d_cond.size(); e++ ){
+ for( unsigned e=0; e<fm->d_models[op]->d_cond.size(); e++ ){
if ( entries.find(e)!=entries.end() ){
- d.addEntry(this, entries[e], d_models[op]->d_value[e] );
+ d.addEntry(fm, entries[e], fm->d_models[op]->d_value[e] );
}
}
}else{
for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
- if (isCompat(cond, dc[index].d_cond[i])!=0) {
+ if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {
std::vector< Node > new_cond;
new_cond.insert(new_cond.end(), cond.begin(), cond.end());
- if( doMeet(new_cond, dc[index].d_cond[i]) ){
+ if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){
Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;
val.push_back(dc[index].d_value[i]);
doUninterpretedCompose(fm, f, op, d, dc, index+1, new_cond, val);
@@ -768,7 +794,7 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModel * fm, Node f, Nod }
}
-void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f,
+void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
std::map< int, Node > & entries, int index,
std::vector< Node > & cond, std::vector< Node > & val,
EntryTrie & curr ) {
@@ -788,7 +814,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f, if( v.getKind()==kind::BOUND_VARIABLE ){
int j = getVariableId(f, v);
Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
- if (!isStar(cond[j+1])) {
+ if (!fm->isStar(cond[j+1])) {
v = cond[j+1];
}else{
bind_var = true;
@@ -801,13 +827,13 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f, cond[j+1] = it->first;
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, it->second);
}
- cond[j+1] = getStar(v.getType());
+ cond[j+1] = fm->getStar(v.getType());
}else{
if (curr.d_child.find(v)!=curr.d_child.end()) {
Trace("fmc-uf-process") << "follow value..." << std::endl;
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);
}
- Node st = getStar(v.getType());
+ Node st = fm->getStar(v.getType());
if (curr.d_child.find(st)!=curr.d_child.end()) {
Trace("fmc-uf-process") << "follow star..." << std::endl;
doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);
@@ -816,28 +842,28 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModel * fm, Node f, }
}
-void FullModelChecker::doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,
+void FullModelChecker::doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,
std::vector< Def > & dc, int index,
std::vector< Node > & cond, std::vector<Node> & val ) {
if ( index==(int)dc.size() ){
Node c = mkCond(cond);
Node v = evaluateInterpreted(n, val);
- d.addEntry(this, c, v);
+ d.addEntry(fm, c, v);
}
else {
TypeNode vtn = n.getType();
for (unsigned i=0; i<dc[index].d_cond.size(); i++) {
- if (isCompat(cond, dc[index].d_cond[i])!=0) {
+ if (isCompat(fm, cond, dc[index].d_cond[i])!=0) {
std::vector< Node > new_cond;
new_cond.insert(new_cond.end(), cond.begin(), cond.end());
- if( doMeet(new_cond, dc[index].d_cond[i]) ){
+ if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){
bool process = true;
if (vtn.isBoolean()) {
//short circuit
if( (n.getKind()==OR && dc[index].d_value[i]==d_true) ||
(n.getKind()==AND && dc[index].d_value[i]==d_false) ){
Node c = mkCond(new_cond);
- d.addEntry(this, c, dc[index].d_value[i]);
+ d.addEntry(fm, c, dc[index].d_value[i]);
process = false;
}
}
@@ -852,23 +878,23 @@ void FullModelChecker::doInterpretedCompose( FirstOrderModel * fm, Node f, Def & }
}
-int FullModelChecker::isCompat( std::vector< Node > & cond, Node c ) {
+int FullModelChecker::isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
Assert(cond.size()==c.getNumChildren()+1);
for (unsigned i=1; i<cond.size(); i++) {
- if( cond[i]!=c[i-1] && !isStar(cond[i]) && !isStar(c[i-1]) ) {
+ if( cond[i]!=c[i-1] && !fm->isStar(cond[i]) && !fm->isStar(c[i-1]) ) {
return 0;
}
}
return 1;
}
-bool FullModelChecker::doMeet( std::vector< Node > & cond, Node c ) {
+bool FullModelChecker::doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c ) {
Assert(cond.size()==c.getNumChildren()+1);
for (unsigned i=1; i<cond.size(); i++) {
if( cond[i]!=c[i-1] ) {
- if( isStar(cond[i]) ){
+ if( fm->isStar(cond[i]) ){
cond[i] = c[i-1];
- }else if( !isStar(c[i-1]) ){
+ }else if( !fm->isStar(c[i-1]) ){
return false;
}
}
@@ -880,38 +906,17 @@ Node FullModelChecker::mkCond( std::vector< Node > & cond ) { return NodeManager::currentNM()->mkNode(APPLY_UF, cond);
}
-Node FullModelChecker::mkCondDefault( Node f) {
+Node FullModelChecker::mkCondDefault( FirstOrderModelFmc * fm, Node f) {
std::vector< Node > cond;
- mkCondDefaultVec(f, cond);
+ mkCondDefaultVec(fm, f, cond);
return mkCond(cond);
}
-Node FullModelChecker::getStar(TypeNode tn) {
- if( d_type_star.find(tn)==d_type_star.end() ){
- Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );
- d_type_star[tn] = st;
- }
- return d_type_star[tn];
-}
-
-Node FullModelChecker::getSomeDomainElement(FirstOrderModel * fm, TypeNode tn){
- //check if there is even any domain elements at all
- if (!fm->d_rep_set.hasType(tn)) {
- Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
- Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
- fm->d_rep_set.d_type_reps[tn].push_back(mbt);
- }else if( fm->d_rep_set.d_type_reps[tn].size()==0 ){
- Message() << "empty reps" << std::endl;
- exit(0);
- }
- return fm->d_rep_set.d_type_reps[tn][0];
-}
-
-void FullModelChecker::mkCondDefaultVec( Node f, std::vector< Node > & cond ) {
+void FullModelChecker::mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond ) {
//get function symbol for f
cond.push_back(d_quant_cond[f]);
for (unsigned i=0; i<f[0].getNumChildren(); i++) {
- Node ts = getStar( f[0][i].getType() );
+ Node ts = fm->getStar( f[0][i].getType() );
cond.push_back(ts);
}
}
@@ -964,56 +969,42 @@ Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) }
}
-bool FullModelChecker::useSimpleModels() {
- return options::fmfFullModelCheckSimple();
+Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) {
+ return fm->getFunctionValue(op, argPrefix);
}
-Node FullModelChecker::getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix ) {
- getModel( fm, op );
- 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);
- vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
- }
- Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
- Node curr;
- for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
- Node v = fm->getRepresentative( d_models[op]->d_value[i] );
- if( curr.isNull() ){
- curr = v;
+
+
+void FullModelChecker::addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,
+ std::vector< Node > & conds,
+ std::vector< Node > & values,
+ std::vector< Node > & entry_conds ) {
+ std::vector< Node > children;
+ std::vector< Node > entry_children;
+ children.push_back(op);
+ entry_children.push_back(op);
+ bool hasNonStar = false;
+ for( unsigned i=0; i<c.getNumChildren(); i++) {
+ Node ri = fm->getUsedRepresentative( c[i]);
+ children.push_back(ri);
+ if (fm->isModelBasisTerm(ri)) {
+ ri = fm->getStar( ri.getType() );
}else{
- //make the condition
- Node cond = d_models[op]->d_cond[i];
- std::vector< Node > children;
- for( unsigned j=0; j<cond.getNumChildren(); j++) {
- if (!isStar(cond[j])){
- Node c = fm->getRepresentative( cond[j] );
- children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
- }
- }
- Assert( !children.empty() );
- Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
- curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );
+ hasNonStar = true;
}
+ entry_children.push_back(ri);
+ }
+ Node n = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+ Node nv = fm->getUsedRepresentative( v);
+ Node en = (useSimpleModels() && hasNonStar) ? n : NodeManager::currentNM()->mkNode( APPLY_UF, entry_children );
+ if( std::find(conds.begin(), conds.end(), n )==conds.end() ){
+ Trace("fmc-model-debug") << "- add " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
+ conds.push_back(n);
+ values.push_back(nv);
+ entry_conds.push_back(en);
}
- curr = Rewriter::rewrite( curr );
- return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
}
-Node FullModelChecker::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) {
- Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;
- for(unsigned i=0; i<args.size(); i++) {
- args[i] = getRepresentative(fm, args[i]);
- }
- if( n.getKind()==VARIABLE ){
- Node r = getRepresentative(fm, n);
- return r;
- }else if( n.getKind()==APPLY_UF ){
- getModel(fm, n.getOperator());
- return d_models[n.getOperator()]->evaluate(this, args);
- }else{
- return Node::null();
- }
-}
\ No newline at end of file +bool FullModelChecker::useSimpleModels() {
+ return options::fmfFullModelCheckSimple();
+}
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h index 00a910567..ddf298006 100755 --- a/src/theory/quantifiers/full_model_check.h +++ b/src/theory/quantifiers/full_model_check.h @@ -14,6 +14,7 @@ #define FULL_MODEL_CHECK
#include "theory/quantifiers/model_builder.h"
+#include "theory/quantifiers/first_order_model.h"
namespace CVC4 {
namespace theory {
@@ -21,6 +22,7 @@ namespace quantifiers { namespace fmcheck {
+class FirstOrderModelFmc;
class FullModelChecker;
class EntryTrie
@@ -30,12 +32,10 @@ public: std::map<Node,EntryTrie> d_child;
int d_data;
void reset() { d_data = -1; d_child.clear(); }
- void addEntry( FullModelChecker * m, Node c, Node v, int data, int index = 0 );
- bool hasGeneralization( FullModelChecker * m, Node c, int index = 0 );
- int getGeneralizationIndex( FullModelChecker * m, std::vector<Node> & inst, int index = 0 );
- void getEntries( FullModelChecker * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );
- //if possible, get ground instance of c that evaluates to the entry
- bool getWitness( FullModelChecker * m, FirstOrderModel * fm, Node c, std::vector<Node> & inst, int index = 0 );
+ void addEntry( FirstOrderModelFmc * m, Node c, Node v, int data, int index = 0 );
+ bool hasGeneralization( FirstOrderModelFmc * m, Node c, int index = 0 );
+ int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node> & inst, int index = 0 );
+ void getEntries( FirstOrderModelFmc * m, Node c, std::vector<int> & compat, std::vector<int> & gen, int index = 0, bool is_gen = true );
};
@@ -64,13 +64,42 @@ public: d_status.clear();
d_has_simplified = false;
}
- bool addEntry( FullModelChecker * m, Node c, Node v);
- Node evaluate( FullModelChecker * m, std::vector<Node>& inst );
- int getGeneralizationIndex( FullModelChecker * m, std::vector<Node>& inst );
- void simplify( FullModelChecker * m );
+ bool addEntry( FirstOrderModelFmc * m, Node c, Node v);
+ Node evaluate( FirstOrderModelFmc * m, std::vector<Node>& inst );
+ int getGeneralizationIndex( FirstOrderModelFmc * m, std::vector<Node>& inst );
+ void simplify( FirstOrderModelFmc * m );
void debugPrint(const char * tr, Node op, FullModelChecker * m);
};
+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;
+ std::map<TypeNode, Node > d_type_star;
+ Node getUsedRepresentative(Node n);
+ /** get current model value */
+ Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
+ void processInitializeModelForTerm(Node n);
+public:
+ FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
+ FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
+ // initialize the model
+ void processInitialize();
+
+ Node getFunctionValue(Node op, const char* argPrefix );
+
+ bool isStar(Node n);
+ Node getStar(TypeNode tn);
+ bool isModelBasisTerm(Node n);
+ Node getModelBasisTerm(TypeNode tn);
+ Node getSomeDomainElement(TypeNode tn);
+};
+
class FullModelChecker : public QModelBuilder
{
@@ -78,45 +107,41 @@ protected: Node d_true;
Node d_false;
std::map<TypeNode, std::map< Node, int > > d_rep_ids;
- std::map<TypeNode, Node > d_model_basis_rep;
- std::map<Node, Def * > d_models;
std::map<Node, Def > d_quant_models;
- std::map<Node, bool > d_models_init;
std::map<Node, Node > d_quant_cond;
- std::map<TypeNode, Node > d_type_star;
std::map<Node, std::map< Node, int > > d_quant_var_id;
std::map<Node, std::vector< int > > d_star_insts;
- Node getRepresentative(FirstOrderModel * fm, Node n);
- Node normalizeArgReps(FirstOrderModel * fm, Node op, Node n);
- void addEntry( FirstOrderModel * fm, Node op, Node c, Node v,
+ Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
+ int exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index);
+protected:
+ void addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node v,
std::vector< Node > & conds,
std::vector< Node > & values,
std::vector< Node > & entry_conds );
- int exhaustiveInstantiate(FirstOrderModel * fm, Node f, Node c, int c_index);
private:
- void doCheck(FirstOrderModel * fm, Node f, Def & d, Node n );
+ void doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n );
void doNegate( Def & dc );
- void doVariableEquality( FirstOrderModel * fm, Node f, Def & d, Node eq );
- void doVariableRelation( FirstOrderModel * fm, Node f, Def & d, Def & dc, Node v);
- void doUninterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n, std::vector< Def > & dc );
+ void doVariableEquality( FirstOrderModelFmc * fm, Node f, Def & d, Node eq );
+ void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v);
+ void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc );
- void doUninterpretedCompose( FirstOrderModel * fm, Node f, Node op, Def & d,
+ void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,
std::vector< Def > & dc, int index,
std::vector< Node > & cond, std::vector<Node> & val );
- void doUninterpretedCompose2( FirstOrderModel * fm, Node f,
+ void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
std::map< int, Node > & entries, int index,
std::vector< Node > & cond, std::vector< Node > & val,
EntryTrie & curr);
- void doInterpretedCompose( FirstOrderModel * fm, Node f, Def & d, Node n,
+ void doInterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n,
std::vector< Def > & dc, int index,
std::vector< Node > & cond, std::vector<Node> & val );
- int isCompat( std::vector< Node > & cond, Node c );
- bool doMeet( std::vector< Node > & cond, Node c );
+ int isCompat( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
+ bool doMeet( FirstOrderModelFmc * fm, std::vector< Node > & cond, Node c );
Node mkCond( std::vector< Node > & cond );
- Node mkCondDefault( Node f );
- void mkCondDefaultVec( Node f, std::vector< Node > & cond );
+ Node mkCondDefault( FirstOrderModelFmc * fm, Node f );
+ void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond );
void mkCondVec( Node n, std::vector< Node > & cond );
Node evaluateInterpreted( Node n, std::vector< Node > & vals );
public:
@@ -124,25 +149,20 @@ public: ~FullModelChecker(){}
int getVariableId(Node f, Node n) { return d_quant_var_id[f][n]; }
- bool isStar(Node n);
- Node getStar(TypeNode tn);
- Node getSomeDomainElement(FirstOrderModel * fm, TypeNode tn);
- bool isModelBasisTerm(Node n);
- Node getModelBasisTerm(TypeNode tn);
- Def * getModel(FirstOrderModel * fm, Node op);
void debugPrintCond(const char * tr, Node n, bool dispStar = false);
void debugPrint(const char * tr, Node n, bool dispStar = false);
bool doExhaustiveInstantiation( FirstOrderModel * fm, Node f, int effort, int & lemmas );
- bool useSimpleModels();
- Node getFunctionValue(FirstOrderModel * fm, Node op, const char* argPrefix );
+ Node getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix );
/** process build model */
void processBuildModel(TheoryModel* m, bool fullModel);
/** get current model value */
- Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial );
+ Node getCurrentUfModelValue( FirstOrderModelFmc* fm, Node n, std::vector< Node > & args, bool partial );
+
+ bool useSimpleModels();
};
}
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 76e61707e..88fb7cd8f 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -18,7 +18,6 @@ #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_model.h" #include "theory/uf/theory_uf_strong_solver.h" -#include "theory/arrays/theory_arrays_model.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/model_builder.h" @@ -45,38 +44,37 @@ bool QModelBuilder::optUseModel() { return options::fmfModelBasedInst(); } - -Node QModelBuilder::getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial ) { - std::vector< Node > children; - if( n.getNumChildren()>0 ){ - if( n.getKind()!=APPLY_UF && n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - children.push_back( n.getOperator() ); - } - for (unsigned i=0; i<n.getNumChildren(); i++) { - Node nc = getCurrentModelValue( fm, n[i] ); - if (nc.isNull()) { - return Node::null(); - }else{ - children.push_back( nc ); +void QModelBuilder::debugModel( FirstOrderModel* fm ){ + //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true + if( Trace.isOn("quant-model-warn") ){ + for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ + Node f = fm->getAssertedQuantifier( i ); + std::vector< Node > vars; + for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ + vars.push_back( f[0][j] ); + } + RepSetIterator riter( d_qe, &(fm->d_rep_set) ); + riter.setQuantifier( f ); + while( !riter.isFinished() ){ + std::vector< Node > terms; + for( int i=0; i<riter.getNumTerms(); i++ ){ + terms.push_back( riter.getTerm( i ) ); + } + Node n = d_qe->getInstantiation( f, vars, terms ); + Node val = fm->getValue( n ); + if( val!=fm->d_true ){ + Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl; + Trace("quant-model-warn") << " " << f << std::endl; + Trace("quant-model-warn") << " Evaluates to " << val << std::endl; + } + riter.increment(); } - } - if( n.getKind()==APPLY_UF ){ - return getCurrentUfModelValue( fm, n, children, partial ); - }else{ - Node nn = NodeManager::currentNM()->mkNode( n.getKind(), children ); - nn = Rewriter::rewrite( nn ); - return nn; - } - }else{ - if( n.getKind()==VARIABLE ){ - return getCurrentUfModelValue( fm, n, children, partial ); - }else{ - return n; } } } + bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ if( argIndex<(int)n.getNumChildren() ){ Node r; @@ -97,6 +95,7 @@ bool TermArgBasisTrie::addTerm2( FirstOrderModel* fm, Node n, int argIndex ){ } } + QModelBuilderIG::QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ) : QModelBuilder( c, qe ) { @@ -106,37 +105,9 @@ Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std:: return n; } -void QModelBuilderIG::debugModel( FirstOrderModel* fm ){ - //debug the model: cycle through all instantiations for all quantifiers, report ones that are not true - if( Trace.isOn("quant-model-warn") ){ - for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){ - Node f = fm->getAssertedQuantifier( i ); - std::vector< Node > vars; - for( int j=0; j<(int)f[0].getNumChildren(); j++ ){ - vars.push_back( f[0][j] ); - } - RepSetIterator riter( d_qe, &(fm->d_rep_set) ); - riter.setQuantifier( f ); - while( !riter.isFinished() ){ - std::vector< Node > terms; - for( int i=0; i<riter.getNumTerms(); i++ ){ - terms.push_back( riter.getTerm( i ) ); - } - Node n = d_qe->getInstantiation( f, vars, terms ); - Node val = fm->getValue( n ); - if( val!=fm->d_true ){ - Trace("quant-model-warn") << "******* Instantiation " << n << " for " << std::endl; - Trace("quant-model-warn") << " " << f << std::endl; - Trace("quant-model-warn") << " Evaluates to " << val << std::endl; - } - riter.increment(); - } - } - } -} - void QModelBuilderIG::processBuildModel( TheoryModel* m, bool fullModel ) { - FirstOrderModel* fm = (FirstOrderModel*)m; + FirstOrderModel* f = (FirstOrderModel*)m; + FirstOrderModelIG* fm = f->asFirstOrderModelIG(); if( fullModel ){ Assert( d_curr_model==fm ); //update models @@ -303,16 +274,17 @@ int QModelBuilderIG::initializeQuantifier( Node f, Node fp ){ } void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ + FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); d_uf_model_constructed.clear(); //determine if any functions are constant - for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){ + for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){ Node op = it->first; TermArgBasisTrie tabt; - for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){ + Node n = fmig->d_uf_terms[op][i]; //for calculating if op is constant if( !n.getAttribute(NoMatchAttribute()) ){ - Node v = fm->getRepresentative( n ); + Node v = fmig->getRepresentative( n ); if( i==0 ){ d_uf_prefs[op].d_const_val = v; }else if( v!=d_uf_prefs[op].d_const_val ){ @@ -324,7 +296,7 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ 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 ) ){ + if( !tabt.addTerm( fmig, n ) ){ BasisNoMatchAttribute bnma; n.setAttribute(bnma,true); } @@ -332,10 +304,10 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ } } if( !d_uf_prefs[op].d_const_val.isNull() ){ - fm->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val ); - fm->d_uf_model_gen[op].makeModel( fm, it->second ); + fmig->d_uf_model_gen[op].setDefaultValue( d_uf_prefs[op].d_const_val ); + fmig->d_uf_model_gen[op].makeModel( fmig, it->second ); Debug("fmf-model-cons") << "Function " << op << " is the constant function "; - fm->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val ); + fmig->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val ); Debug("fmf-model-cons") << std::endl; d_uf_model_constructed[op] = true; }else{ @@ -420,6 +392,7 @@ int QModelBuilderDefault::getSelectionScore( std::vector< Node >& uf_terms ) { } void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ + FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl; //the pro/con preferences for this quantifier std::vector< Node > pro_con[2]; @@ -454,7 +427,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ for( int j=0; j<2; j++ ){ if( TermDb::hasInstConstAttr(n[j]) ){ if( n[j].getKind()==APPLY_UF && - fm->d_uf_model_tree.find( gn[j].getOperator() )!=fm->d_uf_model_tree.end() ){ + fmig->d_uf_model_tree.find( gn[j].getOperator() )!=fmig->d_uf_model_tree.end() ){ uf_terms.push_back( gn[j] ); isConst = isConst && hasConstantDefinition( gn[j] ); }else{ @@ -542,7 +515,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ for( int k=0; k<2; k++ ){ for( int j=0; j<(int)pro_con[k].size(); j++ ){ Node op = pro_con[k][j].getOperator(); - Node r = fm->getRepresentative( pro_con[k][j] ); + Node r = fmig->getRepresentative( pro_con[k][j] ); d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); } } @@ -600,6 +573,7 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ } void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ + FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); if( optReconsiderFuncConstants() ){ //reconsider constant functions that weren't necessary if( d_uf_model_constructed[op] ){ @@ -608,8 +582,8 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ Node v = d_uf_prefs[op].d_const_val; if( d_uf_prefs[op].d_value_pro_con[0][v].empty() ){ Debug("fmf-model-cons-debug") << "Consider changing the default value for " << op << std::endl; - fm->d_uf_model_tree[op].clear(); - fm->d_uf_model_gen[op].clear(); + fmig->d_uf_model_tree[op].clear(); + fmig->d_uf_model_gen[op].clear(); d_uf_model_constructed[op] = false; } } @@ -621,20 +595,20 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); Trace("fmf-model-cons") << "Construct model for " << op << "..." << std::endl; //set the values in the model - for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){ + Node n = fmig->d_uf_terms[op][i]; if( isTermActive( n ) ){ - Node v = fm->getRepresentative( n ); - Trace("fmf-model-cons") << "Set term " << n << " : " << fm->d_rep_set.getIndexFor( v ) << " " << v << std::endl; + Node v = fmig->getRepresentative( n ); + Trace("fmf-model-cons") << "Set term " << n << " : " << fmig->d_rep_set.getIndexFor( v ) << " " << v << std::endl; //if this assertion did not help the model, just consider it ground //set n = v in the model tree //set it as ground value - fm->d_uf_model_gen[op].setValue( fm, n, v ); - if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){ + fmig->d_uf_model_gen[op].setValue( fm, n, v ); + if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){ //also set as default value if necessary 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 ); + fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); if( n==defaultTerm ){ //incidentally already set, we will not need to find a default value setDefaultVal = false; @@ -642,7 +616,7 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ } }else{ if( n==defaultTerm ){ - fm->d_uf_model_gen[op].setValue( fm, n, v, false ); + fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); //incidentally already set, we will not need to find a default value setDefaultVal = false; } @@ -655,18 +629,18 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ //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())) { + if (!fmig->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); + fmig->d_rep_set.d_type_reps[defaultTerm.getType()].push_back(mbt); } - defaultVal = fm->d_rep_set.d_type_reps[defaultTerm.getType()][0]; + defaultVal = fmig->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 ); + Trace("fmf-model-cons") << "Set default term : " << fmig->d_rep_set.getIndexFor( defaultVal ) << std::endl; + fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); } Debug("fmf-model-cons") << " Making model..."; - fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] ); + fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] ); d_uf_model_constructed[op] = true; Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl; } @@ -1030,19 +1004,20 @@ void QModelBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, Ins } void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){ + FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); bool setDefaultVal = true; Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op ); //set the values in the model - for( size_t i=0; i<fm->d_uf_terms[op].size(); i++ ){ - Node n = fm->d_uf_terms[op][i]; + for( size_t i=0; i<fmig->d_uf_terms[op].size(); i++ ){ + Node n = fmig->d_uf_terms[op][i]; if( isTermActive( n ) ){ - Node v = fm->getRepresentative( n ); - fm->d_uf_model_gen[op].setValue( fm, n, v ); + Node v = fmig->getRepresentative( n ); + fmig->d_uf_model_gen[op].setValue( fm, n, v ); } //also possible set as default if( d_term_selected.find( n )!=d_term_selected.end() || n==defaultTerm ){ - Node v = fm->getRepresentative( n ); - fm->d_uf_model_gen[op].setValue( fm, n, v, false ); + Node v = fmig->getRepresentative( n ); + fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); if( n==defaultTerm ){ setDefaultVal = false; } @@ -1051,9 +1026,9 @@ void QModelBuilderInstGen::constructModelUf( FirstOrderModel* fm, Node op ){ //set the overall default value if not set already (is this necessary??) if( setDefaultVal ){ Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm ); - fm->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); + fmig->d_uf_model_gen[op].setValue( fm, defaultTerm, defaultVal, false ); } - fm->d_uf_model_gen[op].makeModel( fm, fm->d_uf_model_tree[op] ); + fmig->d_uf_model_gen[op].makeModel( fm, fmig->d_uf_model_tree[op] ); d_uf_model_constructed[op] = true; } diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index f41392eee..715612975 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -33,8 +33,6 @@ protected: context::CDO< FirstOrderModel* > d_curr_model; //quantifiers engine QuantifiersEngine* d_qe; - /** get current model value */ - virtual Node getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::vector< Node > & args, bool partial ) = 0; public: QModelBuilder( context::Context* c, QuantifiersEngine* qe ); virtual ~QModelBuilder(){} @@ -50,8 +48,8 @@ public: bool d_considerAxioms; /** exist instantiation ? */ virtual bool existsInstantiation( Node f, InstMatch& m, bool modEq = true, bool modInst = false ) { return false; } - /** get current model value */ - Node getCurrentModelValue( FirstOrderModel* fm, Node n, bool partial = false ); + //debug model + void debugModel( FirstOrderModel* fm ); }; @@ -123,8 +121,6 @@ protected: //helper functions public: QModelBuilderIG( context::Context* c, QuantifiersEngine* qe ); virtual ~QModelBuilderIG(){} - //debug model - void debugModel( FirstOrderModel* fm ); public: //whether to add inst-gen lemmas virtual bool optInstGen(); diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index c91d9d3ab..32deb9e47 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -18,7 +18,6 @@ #include "theory/uf/theory_uf.h" #include "theory/uf/theory_uf_strong_solver.h" #include "theory/quantifiers/options.h" -#include "theory/arrays/theory_arrays_model.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_attributes.h" @@ -35,8 +34,7 @@ using namespace CVC4::theory::inst; //Model Engine constructor ModelEngine::ModelEngine( context::Context* c, QuantifiersEngine* qe ) : -QuantifiersModule( qe ), -d_rel_domain( qe, qe->getModel() ){ +QuantifiersModule( qe ){ if( options::fmfFullModelCheck() ){ d_builder = new fmcheck::FullModelChecker( c, qe ); @@ -179,9 +177,8 @@ int ModelEngine::checkModel(){ } */ //compute the relevant domain if necessary - if( optUseRelevantDomain() ){ - d_rel_domain.compute(); - } + //if( optUseRelevantDomain() ){ + //} d_triedLemmas = 0; d_testLemmas = 0; d_relevantLemmas = 0; @@ -240,8 +237,12 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){ //create a rep set iterator and iterate over the (relevant) domain of the quantifier RepSetIterator riter( d_quantEngine, &(d_quantEngine->getModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ - Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl; - d_quantEngine->getModel()->resetEvaluate(); + FirstOrderModelIG * fmig = NULL; + if( !options::fmfFullModelCheck() ){ + fmig = (FirstOrderModelIG*)d_quantEngine->getModel(); + Debug("inst-fmf-ei") << "Reset evaluate..." << std::endl; + fmig->resetEvaluate(); + } Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; int tests = 0; int triedLemmas = 0; @@ -252,7 +253,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){ d_testLemmas++; int eval = 0; int depIndex; - if( d_builder->optUseModel() ){ + if( d_builder->optUseModel() && fmig ){ //see if instantiation is already true in current model Debug("fmf-model-eval") << "Evaluating "; riter.debugPrintSmall("fmf-model-eval"); @@ -261,7 +262,7 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){ //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 ); + eval = fmig->evaluate( d_quantEngine->getTermDatabase()->getInstConstantBody( f ), depIndex, &riter ); if( eval==1 ){ Debug("fmf-model-eval") << " Returned success with depIndex = " << depIndex << std::endl; }else{ @@ -296,10 +297,12 @@ int ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } } //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; + if( fmig ){ + d_statistics.d_eval_formulas += fmig->d_eval_formulas; + d_statistics.d_eval_uf_terms += fmig->d_eval_uf_terms; + d_statistics.d_eval_lits += fmig->d_eval_lits; + d_statistics.d_eval_lits_unknown += fmig->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(); diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h index 97aa085ed..0f0ab4fe7 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/model.h" -#include "theory/quantifiers/relevant_domain.h" #include "theory/quantifiers/full_model_check.h" namespace CVC4 { @@ -34,8 +33,6 @@ private: /** builder class */ QModelBuilder* d_builder; private: //analysis of current model: - //relevant domain - RelevantDomain d_rel_domain; //is the exhaustive instantiation incomplete? bool d_incomplete_check; private: diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp deleted file mode 100644 index cf12cf540..000000000 --- a/src/theory/quantifiers/relevant_domain.cpp +++ /dev/null @@ -1,198 +0,0 @@ -/********************* */ -/*! \file relevant_domain.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** 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 relevant domain class - **/ - -#include "theory/quantifiers_engine.h" -#include "theory/quantifiers/relevant_domain.h" -#include "theory/quantifiers/term_database.h" -#include "theory/quantifiers/first_order_model.h" - -using namespace std; -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; - -RelevantDomain::RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ) : d_qe( qe ), d_model( m ){ - -} - -void RelevantDomain::compute(){ - Trace("rel-dom") << "compute relevant domain" << std::endl; - d_quant_inst_domain.clear(); - for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ - Node f = d_model->getAssertedQuantifier( i ); - d_quant_inst_domain[f].resize( f[0].getNumChildren() ); - } - Trace("rel-dom") << "account for ground terms" << std::endl; - //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment) - for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin(); - it != d_model->d_uf_model_tree.end(); ++it ){ - Node op = it->first; - for( size_t i=0; i<d_model->d_uf_terms[op].size(); i++ ){ - Node n = d_model->d_uf_terms[op][i]; - //add arguments to domain - for( int j=0; j<(int)n.getNumChildren(); j++ ){ - if( d_model->d_rep_set.hasType( n[j].getType() ) ){ - Node ra = d_model->getRepresentative( n[j] ); - int raIndex = d_model->d_rep_set.getIndexFor( ra ); - if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground domain: rep set does not contain : " << ra << std::endl; - Assert( raIndex!=-1 ); - if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){ - d_active_domain[op][j].push_back( raIndex ); - } - } - } - //add to range - Node r = d_model->getRepresentative( n ); - int raIndex = d_model->d_rep_set.getIndexFor( r ); - if( raIndex==-1 ) Trace("rel-dom-warn") << "WARNING: Ground range: rep set does not contain : " << r << std::endl; - Assert( raIndex!=-1 ); - if( std::find( d_active_range[op].begin(), d_active_range[op].end(), raIndex )==d_active_range[op].end() ){ - d_active_range[op].push_back( raIndex ); - } - } - } - Trace("rel-dom") << "do quantifiers" << std::endl; - //find fixed point for relevant domain computation - bool success; - do{ - success = true; - for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ - Node f = d_model->getAssertedQuantifier( i ); - //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment) - if( computeRelevantInstantiationDomain( d_qe->getTermDatabase()->getInstConstantBody( f ), Node::null(), -1, f ) ){ - success = false; - } - //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment) - RepDomain range; - if( extendFunctionDomains( d_qe->getTermDatabase()->getInstConstantBody( f ), range ) ){ - success = false; - } - } - }while( !success ); - Trace("rel-dom") << "done compute relevant domain" << std::endl; - /* - //debug printing - Trace("rel-dom") << "Exhaustive instantiate " << f << std::endl; - if( useRelInstDomain ){ - Trace("rel-dom") << "Relevant domain : " << std::endl; - for( size_t i=0; i<d_rel_domain.d_quant_inst_domain[f].size(); i++ ){ - Trace("rel-dom") << " " << i << " : "; - for( size_t j=0; j<d_rel_domain.d_quant_inst_domain[f][i].size(); j++ ){ - Trace("rel-dom") << d_rel_domain.d_quant_inst_domain[f][i][j] << " "; - } - Trace("rel-dom") << std::endl; - } - } - */ -} - -bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ){ - bool domainChanged = false; - if( n.getKind()==INST_CONSTANT ){ - bool domainSet = false; - int vi = n.getAttribute(InstVarNumAttribute()); - Assert( !parent.isNull() ); - if( parent.getKind()==APPLY_UF ){ - //if the child of APPLY_UF term f( ... ), only consider the active domain of f at given argument - Node op = parent.getOperator(); - if( d_active_domain.find( op )!=d_active_domain.end() ){ - for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){ - int d = d_active_domain[op][arg][i]; - if( std::find( d_quant_inst_domain[f][vi].begin(), d_quant_inst_domain[f][vi].end(), d )== - d_quant_inst_domain[f][vi].end() ){ - d_quant_inst_domain[f][vi].push_back( d ); - domainChanged = true; - } - } - domainSet = true; - } - } - if( !domainSet ){ - //otherwise, we must consider the entire domain - TypeNode tn = n.getType(); - if( d_quant_inst_domain_complete[f].find( vi )==d_quant_inst_domain_complete[f].end() ){ - if( d_model->d_rep_set.hasType( tn ) ){ - //it is the complete domain - d_quant_inst_domain[f][vi].clear(); - for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){ - d_quant_inst_domain[f][vi].push_back( i ); - } - domainChanged = true; - } - d_quant_inst_domain_complete[f][vi] = true; - } - } - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - if( computeRelevantInstantiationDomain( n[i], n, i, f ) ){ - domainChanged = true; - } - } - } - return domainChanged; -} - -bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){ - if( n.getKind()==INST_CONSTANT ){ - Node f = TermDb::getInstConstAttr(n); - int var = n.getAttribute(InstVarNumAttribute()); - range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() ); - return false; - }else{ - Node op; - if( n.getKind()==APPLY_UF ){ - op = n.getOperator(); - } - bool domainChanged = false; - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - RepDomain childRange; - if( extendFunctionDomains( n[i], childRange ) ){ - domainChanged = true; - } - if( n.getKind()==APPLY_UF ){ - if( d_active_domain.find( op )!=d_active_domain.end() ){ - for( int j=0; j<(int)childRange.size(); j++ ){ - int v = childRange[j]; - if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){ - d_active_domain[op][i].push_back( v ); - domainChanged = true; - } - } - }else{ - //do this? - } - } - } - //get the range - if( TermDb::hasInstConstAttr(n) ){ - if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){ - range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() ); - }else{ - //infinite range? - } - }else{ - Node r = d_model->getRepresentative( n ); - int index = d_model->d_rep_set.getIndexFor( r ); - if( index==-1 ){ - //we consider all ground terms in bodies of quantifiers to be the first ground representative - range.push_back( 0 ); - }else{ - range.push_back( index ); - } - } - return domainChanged; - } -}
\ No newline at end of file diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h deleted file mode 100644 index 6fc035e8a..000000000 --- a/src/theory/quantifiers/relevant_domain.h +++ /dev/null @@ -1,54 +0,0 @@ -/********************* */ -/*! \file relevant_domain.h - ** \verbatim - ** Original author: Andrew Reynolds - ** Major contributors: Morgan Deters - ** 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 relevant domain class - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H -#define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H - -#include "theory/quantifiers/first_order_model.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class RelevantDomain -{ -private: - QuantifiersEngine* d_qe; - FirstOrderModel* d_model; - - //the domain of the arguments for each operator - std::map< Node, std::map< int, RepDomain > > d_active_domain; - //the range for each operator - std::map< Node, RepDomain > d_active_range; - //for computing relevant instantiation domain, return true if changed - bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, Node f ); - //for computing extended - bool extendFunctionDomains( Node n, RepDomain& range ); -public: - RelevantDomain( QuantifiersEngine* qe, FirstOrderModel* m ); - virtual ~RelevantDomain(){} - //compute the relevant domain - void compute(); - //relevant instantiation domain for each quantifier - std::map< Node, std::vector< RepDomain > > d_quant_inst_domain; - std::map< Node, std::map< int, bool > > d_quant_inst_domain_complete; -};/* class RelevantDomain */ - -}/* CVC4::theory::quantifiers namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */ |