summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r--src/theory/quantifiers/Makefile.am4
-rw-r--r--src/theory/quantifiers/first_order_model.cpp88
-rw-r--r--src/theory/quantifiers/first_order_model.h15
-rw-r--r--src/theory/quantifiers/model_builder.cpp417
-rw-r--r--src/theory/quantifiers/model_builder.h91
-rw-r--r--src/theory/quantifiers/model_engine.cpp339
-rw-r--r--src/theory/quantifiers/model_engine.h67
-rw-r--r--src/theory/quantifiers/relevant_domain.cpp24
-rw-r--r--src/theory/quantifiers/rep_set_iterator.cpp298
-rw-r--r--src/theory/quantifiers/rep_set_iterator.h6
-rw-r--r--src/theory/quantifiers/term_database.cpp121
-rw-r--r--src/theory/quantifiers/term_database.h3
12 files changed, 830 insertions, 643 deletions
diff --git a/src/theory/quantifiers/Makefile.am b/src/theory/quantifiers/Makefile.am
index ae5b99c06..316e2fbff 100644
--- a/src/theory/quantifiers/Makefile.am
+++ b/src/theory/quantifiers/Makefile.am
@@ -24,6 +24,8 @@ libquantifiers_la_SOURCES = \
term_database.h \
term_database.cpp \
first_order_model.h \
- first_order_model.cpp
+ first_order_model.cpp \
+ model_builder.h \
+ model_builder.cpp
EXTRA_DIST = kinds \ No newline at end of file
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 71a48b33d..766bd31ae 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -17,7 +17,7 @@
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/rep_set_iterator.h"
#include "theory/quantifiers/model_engine.h"
-#include "theory/uf/theory_uf_strong_solver.h"
+#include "theory/quantifiers/term_database.h"
using namespace std;
using namespace CVC4;
@@ -26,25 +26,37 @@ using namespace CVC4::context;
using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name ),
+FirstOrderModel::FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ) : DefaultModel( c, name, true ),
d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){
}
-void FirstOrderModel::initialize(){
+void FirstOrderModel::reset(){
//rebuild models
- d_uf_model.clear();
+ d_uf_model_tree.clear();
+ d_uf_model_gen.clear();
d_array_model.clear();
+ DefaultModel::reset();
+}
+
+void FirstOrderModel::addTerm( Node n ){
+ //std::vector< Node > added;
+ //d_term_db->addTerm( n, added, false );
+ DefaultModel::addTerm( n );
+}
+
+void FirstOrderModel::initialize(){
+ //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 );
- //initialize model for term
+ //initialize relevant models within bodies of all quantifiers
initializeModelForTerm( f[1] );
}
-
+ //for debugging
if( Options::current()->printModelEngine ){
- for( std::map< TypeNode, std::vector< Node > >::iterator it = d_ra.d_type_reps.begin(); it != d_ra.d_type_reps.end(); ++it ){
- if( uf::StrongSolverTheoryUf::isRelevantType( it->first ) ){
+ for( std::map< TypeNode, std::vector< Node > >::iterator it = d_rep_set.d_type_reps.begin(); it != d_rep_set.d_type_reps.end(); ++it ){
+ if( it->first.isSort() ){
Message() << "Cardinality( " << it->first << " )" << " = " << it->second.size() << std::endl;
}
}
@@ -54,33 +66,44 @@ void FirstOrderModel::initialize(){
void FirstOrderModel::initializeModelForTerm( Node n ){
if( n.getKind()==APPLY_UF ){
Node op = n.getOperator();
- if( d_uf_model.find( op )==d_uf_model.end() ){
+ if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){
TypeNode tn = op.getType();
tn = tn[ (int)tn.getNumChildren()-1 ];
- if( tn==NodeManager::currentNM()->booleanType() || uf::StrongSolverTheoryUf::isRelevantType( tn ) ){
- d_uf_model[ op ] = uf::UfModel( op, this );
+ //only generate models for predicates and functions with uninterpreted range types
+ if( tn==NodeManager::currentNM()->booleanType() || tn.isSort() ){
+ d_uf_model_tree[ op ] = uf::UfModelTree( op );
+ d_uf_model_gen[ op ].clear();
}
}
}
- if( n.getKind()!=STORE && n.getType().isArray() ){
- d_array_model[n] = Node::null();
+ /*
+ if( n.getType().isArray() ){
+ while( n.getKind()==STORE ){
+ n = n[0];
+ }
+ Node nn = getRepresentative( n );
+ if( d_array_model.find( nn )==d_array_model.end() ){
+ d_array_model[nn] = arrays::ArrayModel( nn, this );
+ }
}
+ */
for( int i=0; i<(int)n.getNumChildren(); i++ ){
initializeModelForTerm( n[i] );
}
}
void FirstOrderModel::toStreamFunction( Node n, std::ostream& out ){
+ /*
if( d_uf_model.find( n )!=d_uf_model.end() ){
//d_uf_model[n].toStream( out );
Node value = d_uf_model[n].getFunctionValue();
out << "(" << n << " " << value << ")";
- //}else if( d_array_model.find( n )!=d_array_model.end() ){
- //out << "(" << n << " " << d_array_model[n] << ")" << std::endl;
- // out << "(" << n << " Array)" << std::endl;
- }else{
- DefaultModel::toStreamFunction( n, out );
+ }else if( d_array_model.find( n )!=d_array_model.end() ){
+ Node value = d_array_model[n].getArrayValue();
+ out << "(" << n << " " << value << ")" << std::endl;
}
+ */
+ DefaultModel::toStreamFunction( n, out );
}
void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){
@@ -91,14 +114,29 @@ Node FirstOrderModel::getInterpretedValue( TNode n ){
Debug("fo-model") << "get interpreted value " << n << std::endl;
TypeNode type = n.getType();
if( type.isFunction() || type.isPredicate() ){
- if( d_uf_model.find( n )!=d_uf_model.end() ){
- return d_uf_model[n].getFunctionValue();
+ if( d_uf_models.find( n )==d_uf_models.end() ){
+ //use the model tree to generate the model
+ Node fn = d_uf_model_tree[n].getFunctionValue();
+ d_uf_models[n] = fn;
+ return fn;
+ }
+ /*
+ }else if( type.isArray() ){
+ if( d_array_model.find( n )!=d_array_model.end() ){
+ return d_array_model[n].getArrayValue();
}else{
- return n;
+ //std::cout << "no array model generated for " << n << std::endl;
}
+ */
}else if( n.getKind()==APPLY_UF ){
- int depIndex;
- return d_uf_model[ n.getOperator() ].getValue( n, depIndex );
+ Node op = n.getOperator();
+ if( d_uf_model_tree.find( op )!=d_uf_model_tree.end() ){
+ //consult the uf model
+ int depIndex;
+ return d_uf_model_tree[ op ].getValue( this, n, depIndex );
+ }
+ }else if( n.getKind()==SELECT ){
+
}
return DefaultModel::getInterpretedValue( n );
}
@@ -113,14 +151,14 @@ void FirstOrderModel::toStream(std::ostream& out){
#if 0
out << "---Current Model---" << std::endl;
out << "Representatives: " << std::endl;
- d_ra.toStream( out );
+ d_rep_set.toStream( out );
out << "Functions: " << std::endl;
for( std::map< Node, uf::UfModel >::iterator it = d_uf_model.begin(); it != d_uf_model.end(); ++it ){
it->second.toStream( out );
out << std::endl;
}
#elif 0
- d_ra.toStream( out );
+ d_rep_set.toStream( out );
//print everything not related to UF in equality engine
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
while( !eqcs_i.isFinished() ){
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 832acbee3..825518ed0 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -21,6 +21,7 @@
#include "theory/model.h"
#include "theory/uf/theory_uf_model.h"
+#include "theory/arrays/theory_arrays_model.h"
namespace CVC4 {
namespace theory {
@@ -43,6 +44,8 @@ class FirstOrderModel : public DefaultModel
private:
//pointer to term database
TermDb* d_term_db;
+ //add term function
+ void addTerm( Node n );
//for initialize model
void initializeModelForTerm( Node n );
/** to stream functions */
@@ -50,10 +53,12 @@ private:
void toStreamType( TypeNode tn, std::ostream& out );
public: //for Theory UF:
//models for each UF operator
- std::map< Node, uf::UfModel > d_uf_model;
+ std::map< Node, uf::UfModelTree > d_uf_model_tree;
+ //model generators
+ std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
public: //for Theory Arrays:
//default value for each non-store array
- std::map< Node, Node > d_array_model;
+ std::map< Node, arrays::ArrayModel > d_array_model;
public: //for Theory Quantifiers:
/** list of quantifiers asserted in the current context */
context::CDList<Node> d_forall_asserts;
@@ -64,11 +69,13 @@ public: //for Theory Quantifiers:
public:
FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name );
virtual ~FirstOrderModel(){}
- // initialize the model
- void initialize();
+ // reset the model
+ void reset();
/** get interpreted value */
Node getInterpretedValue( TNode n );
public:
+ // initialize the model
+ void initialize();
/** get term database */
TermDb* getTermDatabase();
/** to stream function */
diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
new file mode 100644
index 000000000..9cd5020fb
--- /dev/null
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -0,0 +1,417 @@
+/********************* */
+/*! \file model_builder.cpp
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of model builder class
+ **/
+
+#include "theory/quantifiers/model_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/theory_uf_model.h"
+#include "theory/uf/theory_uf_instantiator.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"
+
+//#define ME_PRINT_WARNINGS
+
+#define RECONSIDER_FUNC_CONSTANT
+//#define ONE_QUANT_PER_ROUND_INST_GEN
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) :
+TheoryEngineModelBuilder( qe->getTheoryEngine() ),
+d_qe( qe ){
+
+}
+
+Node ModelEngineBuilder::chooseRepresentative( TheoryModel* m, Node eqc ){
+ Assert( m->d_equalityEngine.hasTerm( eqc ) );
+ Assert( m->d_equalityEngine.getRepresentative( eqc )==eqc );
+ //avoid interpreted symbols
+ if( isBadRepresentative( eqc ) ){
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &m->d_equalityEngine );
+ while( !eqc_i.isFinished() ){
+ if( !isBadRepresentative( *eqc_i ) ){
+ return *eqc_i;
+ }
+ ++eqc_i;
+ }
+ //otherwise, make new value?
+ //Message() << "Warning: Bad rep " << eqc << std::endl;
+ }
+ return eqc;
+}
+
+bool ModelEngineBuilder::isBadRepresentative( Node n ){
+ return n.getKind()==SELECT || n.getKind()==APPLY_SELECTOR;
+}
+
+void ModelEngineBuilder::processBuildModel( TheoryModel* m ) {
+ d_addedLemmas = 0;
+ //only construct first order model if optUseModel() is true
+ if( optUseModel() ){
+ FirstOrderModel* fm = (FirstOrderModel*)m;
+ //initialize model
+ fm->initialize();
+ //analyze the functions
+ analyzeModel( fm );
+ //analyze the quantifiers
+ Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl;
+ analyzeQuantifiers( fm );
+ //if applicable, find exceptions
+ if( optInstGen() ){
+ //now, see if we know that any exceptions via InstGen exist
+ Debug("fmf-model-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
+ for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ if( d_quant_sat.find( f )==d_quant_sat.end() ){
+ d_addedLemmas += doInstGen( fm, f );
+ if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){
+ break;
+ }
+ }
+ }
+ if( Options::current()->printModelEngine ){
+ if( d_addedLemmas>0 ){
+ Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
+ }else{
+ Message() << "No InstGen lemmas..." << std::endl;
+ }
+ }
+ Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl;
+ }
+ if( d_addedLemmas==0 ){
+ //if no immediate exceptions, build the model
+ // this model will be an approximation that will need to be tested via exhaustive instantiation
+ Debug("fmf-model-debug") << "Building model..." << std::endl;
+ finishBuildModel( fm );
+ }
+ }
+}
+
+void ModelEngineBuilder::analyzeModel( FirstOrderModel* fm ){
+ //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 ){
+ Node op = it->first;
+ 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()) ){
+ Node v = fm->getRepresentative( n );
+ if( i==0 ){
+ d_uf_prefs[op].d_const_val = v;
+ }else if( v!=d_uf_prefs[op].d_const_val ){
+ d_uf_prefs[op].d_const_val = Node::null();
+ break;
+ }
+ }
+ }
+ 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 );
+ Debug("fmf-model-cons") << "Function " << op << " is the constant function ";
+ fm->printRepresentativeDebug( "fmf-model-cons", d_uf_prefs[op].d_const_val );
+ Debug("fmf-model-cons") << std::endl;
+ d_uf_model_constructed[op] = true;
+ }else{
+ d_uf_model_constructed[op] = false;
+ }
+ }
+}
+
+void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){
+ d_quant_selection_lits.clear();
+ d_quant_sat.clear();
+ d_uf_prefs.clear();
+ int quantSatInit = 0;
+ int nquantSatInit = 0;
+ //analyze the preferences of each quantifier
+ for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){
+ Node f = fm->getAssertedQuantifier( i );
+ Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
+ std::vector< Node > pro_con[2];
+ std::vector< Node > constantSatOps;
+ bool constantSatReconsider;
+ //for each asserted quantifier f,
+ // - determine which literals form model basis for each quantifier
+ // - check which function/predicates have good and bad definitions according to f
+ for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin();
+ it != d_qe->d_phase_reqs[f].end(); ++it ){
+ Node n = it->first;
+ Node gn = d_qe->getTermDatabase()->getModelBasis( n );
+ Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl;
+ //calculate preference
+ int pref = 0;
+ bool value;
+ if( d_qe->getValuation().hasSatValue( gn, value ) ){
+ if( value!=it->second ){
+ //store this literal as a model basis literal
+ // this literal will force a default values in model that (modulo exceptions) shows
+ // that f is satisfied by the model
+ d_quant_selection_lits[f].push_back( value ? n : n.notNode() );
+ pref = 1;
+ }else{
+ pref = -1;
+ }
+ }
+ if( pref!=0 ){
+ //Store preferences for UF
+ bool isConst = !n.hasAttribute(InstConstantAttribute());
+ std::vector< Node > uf_terms;
+ if( gn.getKind()==APPLY_UF ){
+ uf_terms.push_back( gn );
+ isConst = !d_uf_prefs[gn.getOperator()].d_const_val.isNull();
+ }else if( gn.getKind()==EQUAL ){
+ isConst = true;
+ for( int j=0; j<2; j++ ){
+ if( n[j].hasAttribute(InstConstantAttribute()) ){
+ if( n[j].getKind()==APPLY_UF ){
+ Node op = gn[j].getOperator();
+ if( fm->d_uf_model_tree.find( op )!=fm->d_uf_model_tree.end() ){
+ uf_terms.push_back( gn[j] );
+ isConst = isConst && !d_uf_prefs[op].d_const_val.isNull();
+ }else{
+ isConst = false;
+ }
+ }else{
+ isConst = false;
+ }
+ }
+ }
+ }
+ Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" );
+ Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
+ if( pref==1 && isConst ){
+ d_quant_sat[f] = true;
+ //instead, just note to the model for each uf term that f is pro its definition
+ constantSatReconsider = false;
+ constantSatOps.clear();
+ for( int j=0; j<(int)uf_terms.size(); j++ ){
+ Node op = uf_terms[j].getOperator();
+ constantSatOps.push_back( op );
+ if( d_uf_prefs[op].d_reconsiderModel ){
+ constantSatReconsider = true;
+ }
+ }
+ if( !constantSatReconsider ){
+ break;
+ }
+ }else{
+ int pcIndex = pref==1 ? 0 : 1;
+ for( int j=0; j<(int)uf_terms.size(); j++ ){
+ pro_con[pcIndex].push_back( uf_terms[j] );
+ }
+ }
+ }
+ }
+ if( d_quant_sat.find( f )!=d_quant_sat.end() ){
+ Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: ";
+ for( int i=0; i<(int)constantSatOps.size(); i++ ){
+ Debug("fmf-model-prefs") << constantSatOps[i] << " ";
+ d_uf_prefs[constantSatOps[i]].d_reconsiderModel = false;
+ }
+ Debug("fmf-model-prefs") << std::endl;
+ quantSatInit++;
+ d_statistics.d_pre_sat_quant += quantSatInit;
+ }else{
+ nquantSatInit++;
+ d_statistics.d_pre_nsat_quant += quantSatInit;
+ //note quantifier's value preferences to models
+ 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] );
+ d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
+ }
+ }
+ }
+ }
+ Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl;
+}
+
+int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){
+ //we wish to add all known exceptions to our model basis literal(s)
+ // this will help to refine our current model.
+ //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
+ // effectively acting as partial instantiations instead of pointwise instantiations.
+ int addedLemmas = 0;
+ for( int i=0; i<(int)d_quant_selection_lits[f].size(); i++ ){
+ bool phase = d_quant_selection_lits[f][i].getKind()!=NOT;
+ Node lit = d_quant_selection_lits[f][i].getKind()==NOT ? d_quant_selection_lits[f][i][0] : d_quant_selection_lits[f][i];
+ Assert( lit.hasAttribute(InstConstantAttribute()) );
+ std::vector< Node > tr_terms;
+ if( lit.getKind()==APPLY_UF ){
+ //only match predicates that are contrary to this one, use literal matching
+ Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
+ fm->getTermDatabase()->setInstantiationConstantAttr( eq, f );
+ tr_terms.push_back( eq );
+ }else if( lit.getKind()==EQUAL ){
+ //collect trigger terms
+ for( int j=0; j<2; j++ ){
+ if( lit[j].hasAttribute(InstConstantAttribute()) ){
+ if( lit[j].getKind()==APPLY_UF ){
+ tr_terms.push_back( lit[j] );
+ }else{
+ tr_terms.clear();
+ break;
+ }
+ }
+ }
+ if( tr_terms.size()==1 && !phase ){
+ //equality between a function and a ground term, use literal matching
+ tr_terms.clear();
+ tr_terms.push_back( lit );
+ }
+ }
+ //if applicable, try to add exceptions here
+ if( !tr_terms.empty() ){
+ //make a trigger for these terms, add instantiations
+ inst::Trigger* tr = inst::Trigger::mkTrigger( d_qe, f, tr_terms );
+ //Notice() << "Trigger = " << (*tr) << std::endl;
+ tr->resetInstantiationRound();
+ tr->reset( Node::null() );
+ //d_qe->d_optInstMakeRepresentative = false;
+ //d_qe->d_optMatchIgnoreModelBasis = true;
+ addedLemmas += tr->addInstantiations( d_quant_basis_match[f] );
+ }
+ }
+ return addedLemmas;
+}
+
+void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){
+ //build model for UF
+ for( std::map< Node, uf::UfModelTree >::iterator it = fm->d_uf_model_tree.begin(); it != fm->d_uf_model_tree.end(); ++it ){
+ finishBuildModelUf( fm, it->first );
+ }
+ /*
+ //build model for arrays
+ for( std::map< Node, arrays::ArrayModel >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){
+ //consult the model basis select term
+ // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term
+ TypeNode tn = it->first.getType();
+ Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) );
+ it->second.setDefaultValue( fm->getRepresentative( selModelBasis ) );
+ }
+ */
+ Debug("fmf-model-debug") << "Done building models." << std::endl;
+}
+
+void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, Node op ){
+#ifdef RECONSIDER_FUNC_CONSTANT
+ if( d_uf_model_constructed[op] ){
+ if( d_uf_prefs[op].d_reconsiderModel ){
+ //if we are allowed to reconsider default value, then see if the default value can be improved
+ 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();
+ d_uf_model_constructed[op] = false;
+ }
+ }
+ }
+#endif
+ if( !d_uf_model_constructed[op] ){
+ //construct the model for the uninterpretted function/predicate
+ bool setDefaultVal = true;
+ Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
+ Debug("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];
+ fm->getTermDatabase()->computeModelBasisArgAttribute( n );
+ if( !n.getAttribute(NoMatchAttribute()) || n.getAttribute(ModelBasisArgAttribute())==1 ){
+ Node v = fm->getRepresentative( n );
+ //if this assertion did not help the model, just consider it ground
+ //set n = v in the model tree
+ Debug("fmf-model-cons") << " Set " << n << " = ";
+ fm->printRepresentativeDebug( "fmf-model-cons", v );
+ Debug("fmf-model-cons") << std::endl;
+ //set it as ground value
+ fm->d_uf_model_gen[op].setValue( fm, n, v );
+ if( fm->d_uf_model_gen[op].optUsePartialDefaults() ){
+ //also set as default value if necessary
+ //if( n.getAttribute(ModelBasisArgAttribute())==1 && !d_term_pro_con[0][n].empty() ){
+ if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){
+ fm->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;
+ }
+ }
+ }else{
+ if( n==defaultTerm ){
+ fm->d_uf_model_gen[op].setValue( fm, n, v, false );
+ //incidentally already set, we will not need to find a default value
+ setDefaultVal = false;
+ }
+ }
+ }
+ }
+ //set the overall default value if not set already (is this necessary??)
+ if( setDefaultVal ){
+ Debug("fmf-model-cons") << " Choose default value..." << std::endl;
+ //chose defaultVal based on heuristic, currently the best ratio of "pro" responses
+ Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
+ Assert( !defaultVal.isNull() );
+ fm->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] );
+ d_uf_model_constructed[op] = true;
+ Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl;
+ }
+}
+
+void ModelEngineBuilder::finishProcessBuildModel( TheoryModel* m ){
+ for( std::map< Node, Node >::iterator it = m->d_reps.begin(); it != m->d_reps.end(); ++it ){
+ //build proper representatives (TODO)
+ }
+}
+
+bool ModelEngineBuilder::optUseModel() {
+ return Options::current()->fmfModelBasedInst;
+}
+
+bool ModelEngineBuilder::optInstGen(){
+ return Options::current()->fmfInstGen;
+}
+
+bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
+#ifdef ONE_QUANT_PER_ROUND_INST_GEN
+ return true;
+#else
+ return false;
+#endif
+}
+
+ModelEngineBuilder::Statistics::Statistics():
+ d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0),
+ d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0)
+{
+ StatisticsRegistry::registerStat(&d_pre_sat_quant);
+ StatisticsRegistry::registerStat(&d_pre_nsat_quant);
+}
+
+ModelEngineBuilder::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_pre_sat_quant);
+ StatisticsRegistry::unregisterStat(&d_pre_nsat_quant);
+}
diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
new file mode 100644
index 000000000..13d500d8e
--- /dev/null
+++ b/src/theory/quantifiers/model_builder.h
@@ -0,0 +1,91 @@
+/********************* */
+/*! \file model_builder.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Model Builder class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__QUANTIFIERS_MODEL_BUILDER_H
+#define __CVC4__QUANTIFIERS_MODEL_BUILDER_H
+
+#include "theory/quantifiers_engine.h"
+#include "theory/model.h"
+#include "theory/uf/theory_uf_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+//the model builder
+class ModelEngineBuilder : public TheoryEngineModelBuilder
+{
+protected:
+ //quantifiers engine
+ QuantifiersEngine* d_qe;
+ //map from operators to model preference data
+ std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
+ //built model uf
+ std::map< Node, bool > d_uf_model_constructed;
+ /** process build model */
+ void processBuildModel( TheoryModel* m );
+ /** choose representative for unconstrained equivalence class */
+ Node chooseRepresentative( TheoryModel* m, Node eqc );
+ /** bad representative */
+ bool isBadRepresentative( Node n );
+protected:
+ //analyze model
+ void analyzeModel( FirstOrderModel* fm );
+ //analyze quantifiers
+ void analyzeQuantifiers( FirstOrderModel* fm );
+ //build model
+ void finishBuildModel( FirstOrderModel* fm );
+ //theory-specific build models
+ void finishBuildModelUf( FirstOrderModel* fm, Node op );
+ //do InstGen techniques for quantifier, return number of lemmas produced
+ int doInstGen( FirstOrderModel* fm, Node f );
+public:
+ ModelEngineBuilder( QuantifiersEngine* qe );
+ virtual ~ModelEngineBuilder(){}
+ /** finish model */
+ void finishProcessBuildModel( TheoryModel* m );
+public:
+ /** number of lemmas generated while building model */
+ int d_addedLemmas;
+ //map from quantifiers to if are constant SAT
+ std::map< Node, bool > d_quant_sat;
+ //map from quantifiers to the instantiation literals that their model is dependent upon
+ std::map< Node, std::vector< Node > > d_quant_selection_lits;
+public:
+ //map from quantifiers to model basis match
+ std::map< Node, InstMatch > d_quant_basis_match;
+ //options
+ bool optUseModel();
+ bool optInstGen();
+ bool optOneQuantPerRoundInstGen();
+ /** statistics class */
+ class Statistics {
+ public:
+ IntStat d_pre_sat_quant;
+ IntStat d_pre_nsat_quant;
+ Statistics();
+ ~Statistics();
+ };
+ Statistics d_statistics;
+};
+
+}
+}
+}
+
+#endif
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 663f270eb..ddaaa5b6f 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -21,16 +21,13 @@
#include "theory/uf/theory_uf.h"
#include "theory/uf/theory_uf_strong_solver.h"
#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/arrays/theory_arrays_model.h"
#include "theory/quantifiers/first_order_model.h"
#include "theory/quantifiers/term_database.h"
//#define ME_PRINT_WARNINGS
-//#define DISABLE_EVAL_SKIP_MULTIPLE
-
-#define RECONSIDER_FUNC_CONSTANT
#define EVAL_FAIL_SKIP_MULTIPLE
-//#define ONE_QUANT_PER_ROUND_INST_GEN
//#define ONE_QUANT_PER_ROUND
using namespace std;
@@ -41,324 +38,6 @@ using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
using namespace CVC4::theory::inst;
-ModelEngineBuilder::ModelEngineBuilder( QuantifiersEngine* qe ) :
-TheoryEngineModelBuilder( qe->getTheoryEngine() ),
-d_qe( qe ){
-
-}
-
-Node ModelEngineBuilder::chooseRepresentative( TheoryModel* tm, Node eqc ){
- return eqc;
-}
-
-void ModelEngineBuilder::processBuildModel( TheoryModel* m ) {
- d_addedLemmas = 0;
- //only construct first order model if optUseModel() is true
- if( optUseModel() ){
- FirstOrderModel* fm = (FirstOrderModel*)m;
- //initialize model
- fm->initialize();
- //analyze the quantifiers
- Debug("fmf-model-debug") << "Analyzing quantifiers..." << std::endl;
- analyzeQuantifiers( fm );
- //if applicable, find exceptions
- if( optInstGen() ){
- //now, see if we know that any exceptions via InstGen exist
- Debug("fmf-model-debug") << "Perform InstGen techniques for quantifiers..." << std::endl;
- for( int i=0; i<fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- if( d_quant_sat.find( f )==d_quant_sat.end() ){
- d_addedLemmas += doInstGen( fm, f );
- if( optOneQuantPerRoundInstGen() && d_addedLemmas>0 ){
- break;
- }
- }
- }
- if( Options::current()->printModelEngine ){
- if( d_addedLemmas>0 ){
- Message() << "InstGen, added lemmas = " << d_addedLemmas << std::endl;
- }else{
- Message() << "No InstGen lemmas..." << std::endl;
- }
- }
- Debug("fmf-model-debug") << "---> Added lemmas = " << d_addedLemmas << std::endl;
- }
- if( d_addedLemmas==0 ){
- //if no immediate exceptions, build the model
- // this model will be an approximation that will need to be tested via exhaustive instantiation
- Debug("fmf-model-debug") << "Building model..." << std::endl;
- finishBuildModel( fm );
- }
- }
-}
-
-void ModelEngineBuilder::analyzeQuantifiers( FirstOrderModel* fm ){
- d_quant_selection_lits.clear();
- d_quant_sat.clear();
- d_uf_prefs.clear();
- int quantSatInit = 0;
- int nquantSatInit = 0;
- //analyze the preferences of each quantifier
- for( int i=0; i<(int)fm->getNumAssertedQuantifiers(); i++ ){
- Node f = fm->getAssertedQuantifier( i );
- Debug("fmf-model-prefs") << "Analyze quantifier " << f << std::endl;
- std::vector< Node > pro_con[2];
- std::vector< Node > constantSatOps;
- bool constantSatReconsider;
- //for each asserted quantifier f,
- // - determine which literals form model basis for each quantifier
- // - check which function/predicates have good and bad definitions according to f
- for( std::map< Node, bool >::iterator it = d_qe->d_phase_reqs[f].begin();
- it != d_qe->d_phase_reqs[f].end(); ++it ){
- Node n = it->first;
- Node gn = d_qe->getTermDatabase()->getModelBasis( n );
- Debug("fmf-model-req") << " Req: " << n << " -> " << it->second << std::endl;
- //calculate preference
- int pref = 0;
- bool value;
- if( d_qe->getValuation().hasSatValue( gn, value ) ){
- if( value!=it->second ){
- //store this literal as a model basis literal
- // this literal will force a default values in model that (modulo exceptions) shows
- // that f is satisfied by the model
- d_quant_selection_lits[f].push_back( value ? n : n.notNode() );
- pref = 1;
- }else{
- pref = -1;
- }
- }
- if( pref!=0 ){
- //Store preferences for UF
- bool isConst = !n.hasAttribute(InstConstantAttribute());
- std::vector< Node > uf_terms;
- if( gn.getKind()==APPLY_UF ){
- uf_terms.push_back( gn );
- isConst = fm->d_uf_model[gn.getOperator()].isConstant();
- }else if( gn.getKind()==EQUAL ){
- isConst = true;
- for( int j=0; j<2; j++ ){
- if( n[j].hasAttribute(InstConstantAttribute()) ){
- if( n[j].getKind()==APPLY_UF ){
- Node op = gn[j].getOperator();
- if( fm->d_uf_model.find( op )!=fm->d_uf_model.end() ){
- uf_terms.push_back( gn[j] );
- isConst = isConst && fm->d_uf_model[op].isConstant();
- }else{
- isConst = false;
- }
- }else{
- isConst = false;
- }
- }
- }
- }
- Debug("fmf-model-prefs") << " It is " << ( pref==1 ? "pro" : "con" );
- Debug("fmf-model-prefs") << " the definition of " << n << std::endl;
- if( pref==1 && isConst ){
- d_quant_sat[f] = true;
- //instead, just note to the model for each uf term that f is pro its definition
- constantSatReconsider = false;
- constantSatOps.clear();
- for( int j=0; j<(int)uf_terms.size(); j++ ){
- Node op = uf_terms[j].getOperator();
- constantSatOps.push_back( op );
- if( d_uf_prefs[op].d_reconsiderModel ){
- constantSatReconsider = true;
- }
- }
- if( !constantSatReconsider ){
- break;
- }
- }else{
- int pcIndex = pref==1 ? 0 : 1;
- for( int j=0; j<(int)uf_terms.size(); j++ ){
- pro_con[pcIndex].push_back( uf_terms[j] );
- }
- }
- }
- }
- if( d_quant_sat.find( f )!=d_quant_sat.end() ){
- Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: ";
- for( int i=0; i<(int)constantSatOps.size(); i++ ){
- Debug("fmf-model-prefs") << constantSatOps[i] << " ";
- d_uf_prefs[constantSatOps[i]].d_reconsiderModel = false;
- }
- Debug("fmf-model-prefs") << std::endl;
- quantSatInit++;
- d_statistics.d_pre_sat_quant += quantSatInit;
- }else{
- nquantSatInit++;
- d_statistics.d_pre_nsat_quant += quantSatInit;
- //note quantifier's value preferences to models
- 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] );
- d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 );
- }
- }
- }
- }
- Debug("fmf-model-prefs") << "Pre-Model Completion: Quantifiers SAT: " << quantSatInit << " / " << (quantSatInit+nquantSatInit) << std::endl;
-}
-
-int ModelEngineBuilder::doInstGen( FirstOrderModel* fm, Node f ){
- //we wish to add all known exceptions to our model basis literal(s)
- // this will help to refine our current model.
- //This step is advantageous over exhaustive instantiation, since we are adding instantiations that involve model basis terms,
- // effectively acting as partial instantiations instead of pointwise instantiations.
- int addedLemmas = 0;
- for( int i=0; i<(int)d_quant_selection_lits[f].size(); i++ ){
- bool phase = d_quant_selection_lits[f][i].getKind()!=NOT;
- Node lit = d_quant_selection_lits[f][i].getKind()==NOT ? d_quant_selection_lits[f][i][0] : d_quant_selection_lits[f][i];
- Assert( lit.hasAttribute(InstConstantAttribute()) );
- std::vector< Node > tr_terms;
- if( lit.getKind()==APPLY_UF ){
- //only match predicates that are contrary to this one, use literal matching
- Node eq = NodeManager::currentNM()->mkNode( IFF, lit, !phase ? fm->d_true : fm->d_false );
- fm->getTermDatabase()->setInstantiationConstantAttr( eq, f );
- tr_terms.push_back( eq );
- }else if( lit.getKind()==EQUAL ){
- //collect trigger terms
- for( int j=0; j<2; j++ ){
- if( lit[j].hasAttribute(InstConstantAttribute()) ){
- if( lit[j].getKind()==APPLY_UF ){
- tr_terms.push_back( lit[j] );
- }else{
- tr_terms.clear();
- break;
- }
- }
- }
- if( tr_terms.size()==1 && !phase ){
- //equality between a function and a ground term, use literal matching
- tr_terms.clear();
- tr_terms.push_back( lit );
- }
- }
- //if applicable, try to add exceptions here
- if( !tr_terms.empty() ){
- //make a trigger for these terms, add instantiations
- Trigger* tr = Trigger::mkTrigger( d_qe, f, tr_terms );
- //Notice() << "Trigger = " << (*tr) << std::endl;
- tr->resetInstantiationRound();
- tr->reset( Node::null() );
- //d_qe->d_optInstMakeRepresentative = false;
- //d_qe->d_optMatchIgnoreModelBasis = true;
- addedLemmas += tr->addInstantiations( d_quant_basis_match[f] );
- }
- }
- return addedLemmas;
-}
-
-void ModelEngineBuilder::finishBuildModel( FirstOrderModel* fm ){
- //build model for UF
- for( std::map< Node, uf::UfModel >::iterator it = fm->d_uf_model.begin(); it != fm->d_uf_model.end(); ++it ){
- finishBuildModelUf( fm, it->second );
- }
- //build model for arrays
- for( std::map< Node, Node >::iterator it = fm->d_array_model.begin(); it != fm->d_array_model.end(); ++it ){
- //consult the model basis select term
- // i.e. the default value for array A is the value of select( A, e ), where e is the model basis term
- TypeNode tn = it->first.getType();
- Node selModelBasis = NodeManager::currentNM()->mkNode( SELECT, it->first, fm->getTermDatabase()->getModelBasisTerm( tn[0] ) );
- it->second = fm->getRepresentative( selModelBasis );
- }
- Debug("fmf-model-debug") << "Done building models." << std::endl;
-}
-
-void ModelEngineBuilder::finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model ){
- Node op = model.getOperator();
-#ifdef RECONSIDER_FUNC_CONSTANT
- if( model.isModelConstructed() && model.isConstant() ){
- if( d_uf_prefs[op].d_reconsiderModel ){
- //if we are allowed to reconsider default value, then see if the default value can be improved
- Node t = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
- Node v = model.getConstantValue( t );
- 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;
- model.clearModel();
- }
- }
- }
-#endif
- if( !model.isModelConstructed() ){
- //construct the model for the uninterpretted function/predicate
- bool setDefaultVal = true;
- Node defaultTerm = d_qe->getTermDatabase()->getModelBasisOpTerm( op );
- Debug("fmf-model-cons") << "Construct model for " << op << "..." << std::endl;
- //set the values in the model
- for( size_t i=0; i<model.d_ground_asserts.size(); i++ ){
- Node n = model.d_ground_asserts[i];
- Node v = model.d_ground_asserts_reps[i];
- //if this assertion did not help the model, just consider it ground
- //set n = v in the model tree
- Debug("fmf-model-cons") << " Set " << n << " = ";
- fm->printRepresentativeDebug( "fmf-model-cons", v );
- Debug("fmf-model-cons") << std::endl;
- //set it as ground value
- model.setValue( n, v );
- if( model.optUsePartialDefaults() ){
- //also set as default value if necessary
- //if( n.getAttribute(ModelBasisArgAttribute())==1 && !d_term_pro_con[0][n].empty() ){
- if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())==1 ){
- model.setValue( n, v, false );
- if( n==defaultTerm ){
- //incidentally already set, we will not need to find a default value
- setDefaultVal = false;
- }
- }
- }else{
- if( n==defaultTerm ){
- model.setValue( n, v, false );
- //incidentally already set, we will not need to find a default value
- setDefaultVal = false;
- }
- }
- }
- //set the overall default value if not set already (is this necessary??)
- if( setDefaultVal ){
- Debug("fmf-model-cons") << " Choose default value..." << std::endl;
- //chose defaultVal based on heuristic, currently the best ratio of "pro" responses
- Node defaultVal = d_uf_prefs[op].getBestDefaultValue( defaultTerm, fm );
- Assert( !defaultVal.isNull() );
- model.setValue( defaultTerm, defaultVal, false );
- }
- Debug("fmf-model-cons") << " Making model...";
- model.setModel();
- Debug("fmf-model-cons") << " Finished constructing model for " << op << "." << std::endl;
- }
-}
-
-bool ModelEngineBuilder::optUseModel() {
- return Options::current()->fmfModelBasedInst;
-}
-
-bool ModelEngineBuilder::optInstGen(){
- return Options::current()->fmfInstGen;
-}
-
-bool ModelEngineBuilder::optOneQuantPerRoundInstGen(){
-#ifdef ONE_QUANT_PER_ROUND_INST_GEN
- return true;
-#else
- return false;
-#endif
-}
-
-ModelEngineBuilder::Statistics::Statistics():
- d_pre_sat_quant("ModelEngineBuilder::Status_quant_pre_sat", 0),
- d_pre_nsat_quant("ModelEngineBuilder::Status_quant_pre_non_sat", 0)
-{
- StatisticsRegistry::registerStat(&d_pre_sat_quant);
- StatisticsRegistry::registerStat(&d_pre_nsat_quant);
-}
-
-ModelEngineBuilder::Statistics::~Statistics(){
- StatisticsRegistry::unregisterStat(&d_pre_sat_quant);
- StatisticsRegistry::unregisterStat(&d_pre_nsat_quant);
-}
-
//Model Engine constructor
ModelEngine::ModelEngine( QuantifiersEngine* qe ) :
QuantifiersModule( qe ),
@@ -448,6 +127,8 @@ void ModelEngine::check( Theory::Effort e ){
//CVC4 will answer SAT
Debug("fmf-consistent") << std::endl;
debugPrint("fmf-consistent");
+ // finish building the model in the standard way
+ d_builder.finishProcessBuildModel( d_quantEngine->getModel() );
}else{
//otherwise, the search will continue
d_quantEngine->flushLemmas( &d_quantEngine->getOutputChannel() );
@@ -601,12 +282,13 @@ int ModelEngine::exhaustiveInstantiate( Node f, bool useRelInstDomain ){
}
}
d_statistics.d_eval_formulas += reval.d_eval_formulas;
- d_statistics.d_eval_eqs += reval.d_eval_eqs;
d_statistics.d_eval_uf_terms += reval.d_eval_uf_terms;
+ d_statistics.d_eval_lits += reval.d_eval_lits;
+ d_statistics.d_eval_lits_unknown += reval.d_eval_lits_unknown;
int totalInst = 1;
int relevantInst = 1;
for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- totalInst = totalInst * (int)d_quantEngine->getModel()->d_ra.d_type_reps[ f[0][i].getType() ].size();
+ totalInst = totalInst * (int)d_quantEngine->getModel()->d_rep_set.d_type_reps[ f[0][i].getType() ].size();
relevantInst = relevantInst * (int)riter.d_domain[i].size();
}
d_totalLemmas += totalInst;
@@ -658,15 +340,17 @@ void ModelEngine::debugPrint( const char* c ){
ModelEngine::Statistics::Statistics():
d_inst_rounds("ModelEngine::Inst_Rounds", 0),
d_eval_formulas("ModelEngine::Eval_Formulas", 0 ),
- d_eval_eqs("ModelEngine::Eval_Equalities", 0 ),
d_eval_uf_terms("ModelEngine::Eval_Uf_Terms", 0 ),
+ d_eval_lits("ModelEngine::Eval_Lits", 0 ),
+ d_eval_lits_unknown("ModelEngine::Eval_Lits_Unknown", 0 ),
d_num_quants_init("ModelEngine::Num_Quants", 0 ),
d_num_quants_init_fail("ModelEngine::Num_Quants_No_Basis", 0 )
{
StatisticsRegistry::registerStat(&d_inst_rounds);
StatisticsRegistry::registerStat(&d_eval_formulas);
- StatisticsRegistry::registerStat(&d_eval_eqs);
StatisticsRegistry::registerStat(&d_eval_uf_terms);
+ StatisticsRegistry::registerStat(&d_eval_lits);
+ StatisticsRegistry::registerStat(&d_eval_lits_unknown);
StatisticsRegistry::registerStat(&d_num_quants_init);
StatisticsRegistry::registerStat(&d_num_quants_init_fail);
}
@@ -674,8 +358,9 @@ ModelEngine::Statistics::Statistics():
ModelEngine::Statistics::~Statistics(){
StatisticsRegistry::unregisterStat(&d_inst_rounds);
StatisticsRegistry::unregisterStat(&d_eval_formulas);
- StatisticsRegistry::unregisterStat(&d_eval_eqs);
StatisticsRegistry::unregisterStat(&d_eval_uf_terms);
+ StatisticsRegistry::unregisterStat(&d_eval_lits);
+ StatisticsRegistry::unregisterStat(&d_eval_lits_unknown);
StatisticsRegistry::unregisterStat(&d_num_quants_init);
StatisticsRegistry::unregisterStat(&d_num_quants_init_fail);
}
diff --git a/src/theory/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index b01139826..1139332fe 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -11,81 +11,25 @@
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Model Engine classes
+ ** \brief Model Engine class
**/
#include "cvc4_private.h"
-#ifndef __CVC4__MODEL_ENGINE_H
-#define __CVC4__MODEL_ENGINE_H
+#ifndef __CVC4__QUANTIFIERS_MODEL_ENGINE_H
+#define __CVC4__QUANTIFIERS_MODEL_ENGINE_H
#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/theory_quantifiers.h"
+#include "theory/quantifiers/model_builder.h"
#include "theory/model.h"
-#include "theory/uf/theory_uf_model.h"
#include "theory/quantifiers/relevant_domain.h"
namespace CVC4 {
namespace theory {
-
-namespace uf{
- class StrongSolverTheoryUf;
-}
-
namespace quantifiers {
-
-//the model builder
-class ModelEngineBuilder : public TheoryEngineModelBuilder
-{
-protected:
- //quantifiers engine
- QuantifiersEngine* d_qe;
- //map from operators to model preference data
- std::map< Node, uf::UfModelPreferenceData > d_uf_prefs;
- /** choose representative */
- Node chooseRepresentative( TheoryModel* tm, Node eqc );
- /** use constants for representatives */
- void processBuildModel( TheoryModel* m );
- //analyze quantifiers
- void analyzeQuantifiers( FirstOrderModel* fm );
- //build model
- void finishBuildModel( FirstOrderModel* fm );
- //theory-specific build models
- void finishBuildModelUf( FirstOrderModel* fm, uf::UfModel& model );
- //do InstGen techniques for quantifier, return number of lemmas produced
- int doInstGen( FirstOrderModel* fm, Node f );
-public:
- ModelEngineBuilder( QuantifiersEngine* qe );
- virtual ~ModelEngineBuilder(){}
-public:
- /** number of lemmas generated while building model */
- int d_addedLemmas;
- //map from quantifiers to if are constant SAT
- std::map< Node, bool > d_quant_sat;
- //map from quantifiers to the instantiation literals that their model is dependent upon
- std::map< Node, std::vector< Node > > d_quant_selection_lits;
-public:
- //map from quantifiers to model basis match
- std::map< Node, InstMatch > d_quant_basis_match;
- //options
- bool optUseModel();
- bool optInstGen();
- bool optOneQuantPerRoundInstGen();
- /** statistics class */
- class Statistics {
- public:
- IntStat d_pre_sat_quant;
- IntStat d_pre_nsat_quant;
- Statistics();
- ~Statistics();
- };
- Statistics d_statistics;
-};
-
class ModelEngine : public QuantifiersModule
{
- friend class uf::UfModel;
friend class RepSetIterator;
private:
/** builder class */
@@ -128,8 +72,9 @@ public:
public:
IntStat d_inst_rounds;
IntStat d_eval_formulas;
- IntStat d_eval_eqs;
IntStat d_eval_uf_terms;
+ IntStat d_eval_lits;
+ IntStat d_eval_lits_unknown;
IntStat d_num_quants_init;
IntStat d_num_quants_init_fail;
Statistics();
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index e7ae1d1c7..12206e148 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -37,16 +37,16 @@ void RelevantDomain::compute(){
d_quant_inst_domain[f].resize( f[0].getNumChildren() );
}
//add ground terms to domain (rule 1 of complete instantiation essentially uf fragment)
- for( std::map< Node, uf::UfModel >::iterator it = d_model->d_uf_model.begin();
- it != d_model->d_uf_model.end(); ++it ){
+ 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( int i=0; i<(int)it->second.d_ground_asserts.size(); i++ ){
- Node n = it->second.d_ground_asserts[i];
+ 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_ra.hasType( n[j].getType() ) ){
+ if( d_model->d_rep_set.hasType( n[j].getType() ) ){
Node ra = d_model->getRepresentative( n[j] );
- int raIndex = d_model->d_ra.getIndexFor( ra );
+ int raIndex = d_model->d_rep_set.getIndexFor( ra );
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 );
@@ -54,8 +54,8 @@ void RelevantDomain::compute(){
}
}
//add to range
- Node r = it->second.d_ground_asserts_reps[i];
- int raIndex = d_model->d_ra.getIndexFor( r );
+ Node r = d_model->getRepresentative( n );
+ int raIndex = d_model->d_rep_set.getIndexFor( r );
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 );
@@ -104,10 +104,10 @@ bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, in
if( !domainSet ){
//otherwise, we must consider the entire domain
TypeNode tn = n.getType();
- if( d_model->d_ra.hasType( tn ) ){
- if( rd[vi].size()!=d_model->d_ra.d_type_reps[tn].size() ){
+ if( d_model->d_rep_set.hasType( tn ) ){
+ if( rd[vi].size()!=d_model->d_rep_set.d_type_reps[tn].size() ){
rd[vi].clear();
- for( size_t i=0; i<d_model->d_ra.d_type_reps[tn].size(); i++ ){
+ for( size_t i=0; i<d_model->d_rep_set.d_type_reps[tn].size(); i++ ){
rd[vi].push_back( i );
domainChanged = true;
}
@@ -166,7 +166,7 @@ bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
}
}else{
Node r = d_model->getRepresentative( n );
- range.push_back( d_model->d_ra.getIndexFor( r ) );
+ range.push_back( d_model->d_rep_set.getIndexFor( r ) );
}
return domainChanged;
}
diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp
index a29f815db..516f85857 100644
--- a/src/theory/quantifiers/rep_set_iterator.cpp
+++ b/src/theory/quantifiers/rep_set_iterator.cpp
@@ -38,8 +38,28 @@ RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_m
d_var_order[i] = i;
//store default domain
d_domain.push_back( RepDomain() );
- for( int j=0; j<(int)d_model->d_ra.d_type_reps[d_f[0][i].getType()].size(); j++ ){
- d_domain[i].push_back( j );
+ TypeNode tn = d_f[0][i].getType();
+ if( tn.isSort() ){
+ if( d_model->d_rep_set.hasType( tn ) ){
+ for( int j=0; j<(int)d_model->d_rep_set.d_type_reps[d_f[0][i].getType()].size(); j++ ){
+ d_domain[i].push_back( j );
+ }
+ }else{
+ Unimplemented("Cannot create instantiation iterator for unknown uninterpretted sort");
+ }
+ }else if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
+ Unimplemented("Cannot create instantiation iterator for arithmetic quantifier");
+ }else if( tn.isDatatype() ){
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ //if finite, then use type enumerator
+ if( dt.isFinite() ){
+ //DO_THIS: use type enumerator
+ Unimplemented("Not yet implemented: instantiation iterator for finite datatype quantifier");
+ }else{
+ Unimplemented("Cannot create instantiation iterator for infinite datatype quantifier");
+ }
+ }else{
+ Unimplemented("Cannot create instantiation iterator for quantifier");
}
}
}
@@ -103,9 +123,9 @@ void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){
Node RepSetIterator::getTerm( int i ){
TypeNode tn = d_f[0][d_index_order[i]].getType();
- Assert( d_model->d_ra.d_type_reps.find( tn )!=d_model->d_ra.d_type_reps.end() );
+ Assert( d_model->d_rep_set.d_type_reps.find( tn )!=d_model->d_rep_set.d_type_reps.end() );
int index = d_index_order[i];
- return d_model->d_ra.d_type_reps[tn][d_domain[index][d_index[index]]];
+ return d_model->d_rep_set.d_type_reps[tn][d_domain[index][d_index[index]]];
}
void RepSetIterator::debugPrint( const char* c ){
@@ -123,14 +143,18 @@ void RepSetIterator::debugPrintSmall( const char* c ){
}
RepSetEvaluator::RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ) : d_model( m ), d_riter( ri ){
-
+ d_eval_formulas = 0;
+ d_eval_uf_terms = 0;
+ d_eval_lits = 0;
+ d_eval_lits_unknown = 0;
}
-//if evaluate( n, phaseReq ) = eVal,
-// if eVal = d_riter->d_index.size()
-// then the formula n instantiated with d_riter cannot be proven to be equal to phaseReq
-// otherwise,
-// each n{d_riter->d_index[0]/x_0...d_riter->d_index[eVal]/x_eVal, */x_(eVal+1) ... */x_n } is equal to phaseReq in the current model
+//if evaluate( n ) = eVal,
+// let n' = d_riter * n be the formula n instantiated with the current values in r_iter
+// if eVal = 1, then n' is true, if eVal = -1, then n' is false,
+// if eVal = 0, then n' cannot be proven to be equal to phaseReq
+// if eVal is not 0, then
+// each n{d_riter->d_index[0]/x_0...d_riter->d_index[depIndex]/x_depIndex, */x_(depIndex+1) ... */x_n } is equivalent in the current model
int RepSetEvaluator::evaluate( Node n, int& depIndex ){
++d_eval_formulas;
//Debug("fmf-eval-debug") << "Evaluate " << n << " " << phaseReq << std::endl;
@@ -208,6 +232,7 @@ int RepSetEvaluator::evaluate( Node n, int& depIndex ){
}else if( n.getKind()==FORALL ){
return 0;
}else{
+ ++d_eval_lits;
////if we know we will fail again, immediately return
//if( d_eval_failed.find( n )!=d_eval_failed.end() ){
// if( d_eval_failed[n] ){
@@ -215,89 +240,46 @@ int RepSetEvaluator::evaluate( Node n, int& depIndex ){
// }
//}
//Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;
- //this should be a literal
- //Node gn = n.substitute( d_riter->d_ic.begin(), d_riter->d_ic.end(), d_riter->d_terms.begin(), d_riter->d_terms.end() );
- //Debug("fmf-eval-debug") << " Ground version = " << gn << std::endl;
int retVal = 0;
depIndex = d_riter->getNumTerms()-1;
- if( n.getKind()==APPLY_UF ){
- //case for boolean predicates
- Node val = evaluateTerm( n, depIndex );
- if( d_model->hasTerm( val ) ){
- if( d_model->areEqual( val, d_model->d_true ) ){
- retVal = 1;
- }else{
- retVal = -1;
- }
- }
- }else if( n.getKind()==EQUAL ){
- //case for equality
- retVal = evaluateEquality( n[0], n[1], depIndex );
- }else{
- std::vector< int > cdi;
- Node val = evaluateTermDefault( n, depIndex, cdi );
- if( !val.isNull() ){
- val = Rewriter::rewrite( val );
- if( val==d_model->d_true ){
- retVal = 1;
- }else if( val==d_model->d_false ){
- retVal = -1;
+ Node val = evaluateTerm( n, depIndex );
+ if( !val.isNull() ){
+ if( d_model->areEqual( val, d_model->d_true ) ){
+ retVal = 1;
+ }else if( d_model->areEqual( val, d_model->d_false ) ){
+ retVal = -1;
+ }else{
+ if( val.getKind()==EQUAL ){
+ if( d_model->areEqual( val[0], val[1] ) ){
+ retVal = 1;
+ }else if( d_model->areDisequal( val[0], val[1] ) ){
+ retVal = -1;
+ }
}
}
}
if( retVal!=0 ){
- Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depends = " << depIndex << std::endl;
+ Debug("fmf-eval-debug") << "Evaluate literal: return " << retVal << ", depIndex = " << depIndex << std::endl;
}else{
+ ++d_eval_lits_unknown;
Debug("fmf-eval-amb") << "Neither true nor false : " << n << std::endl;
//std::cout << "Neither true nor false : " << n << std::endl;
+ //std::cout << " Value : " << val << std::endl;
+ //for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ // std::cout << " " << i << " : " << n[i].getType() << std::endl;
+ //}
}
return retVal;
}
}
-int RepSetEvaluator::evaluateEquality( Node n1, Node n2, int& depIndex ){
- ++d_eval_eqs;
- //Notice() << "Eval eq " << n1 << " " << n2 << std::endl;
- Debug("fmf-eval-debug") << "Evaluate equality: " << std::endl;
- Debug("fmf-eval-debug") << " " << n1 << " = " << n2 << std::endl;
- int depIndex1, depIndex2;
- Node val1 = evaluateTerm( n1, depIndex1 );
- Node val2 = evaluateTerm( n2, depIndex2 );
- Debug("fmf-eval-debug") << " Values : ";
- d_model->printRepresentativeDebug( "fmf-eval-debug", val1 );
- Debug("fmf-eval-debug") << " = ";
- d_model->printRepresentativeDebug( "fmf-eval-debug", val2 );
- Debug("fmf-eval-debug") << std::endl;
- int retVal = 0;
- if( !val1.isNull() && !val2.isNull() ){
- if( d_model->areEqual( val1, val2 ) ){
- retVal = 1;
- }else if( d_model->areDisequal( val1, val2 ) ){
- retVal = -1;
- }else{
- Node eq = val1.eqNode( val2 );
- eq = Rewriter::rewrite( eq );
- if( eq==d_model->d_true ){
- retVal = 1;
- }else if( eq==d_model->d_false ){
- retVal = -1;
- }
- }
- }
- if( retVal!=0 ){
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- Debug("fmf-eval-debug") << " value = " << (retVal==1) << ", depIndex = " << depIndex << std::endl;
- }else{
- depIndex = d_riter->getNumTerms()-1;
- Debug("fmf-eval-amb") << "Neither equal nor disequal : " << n1 << " , " << n2 << std::endl;
- //std::cout << "Neither equal nor disequal : " << n1 << " , " << n2 << std::endl;
- }
- return retVal;
-}
-
Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
- //Notice() << "Eval term " << n << std::endl;
- if( n.hasAttribute(InstConstantAttribute()) ){
+ //Message() << "Eval term " << n << std::endl;
+ if( !n.hasAttribute(InstConstantAttribute()) ){
+ //if evaluating a ground term, just consult the standard getValue functionality
+ depIndex = -1;
+ return d_model->getValue( n );
+ }else{
Node val;
depIndex = d_riter->getNumTerms()-1;
//check the type of n
@@ -311,7 +293,7 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
if( eval==0 ){
//evaluate children to see if they are the same
Node val1 = evaluateTerm( n[ 1 ], depIndex1 );
- Node val2 = evaluateTerm( n[ 1 ], depIndex1 );
+ Node val2 = evaluateTerm( n[ 2 ], depIndex2 );
if( val1==val2 ){
val = val1;
depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
@@ -323,19 +305,24 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
}
}else{
-#if 0
+ std::vector< int > children_depIndex;
//for select, pre-process read over writes
if( n.getKind()==SELECT ){
- Node selIndex = evaluateTerm( n[1], depIndex );
- if( selIndex.isNull() ){
+#if 1
+ //std::cout << "Evaluate " << n << std::endl;
+ Node sel = evaluateTerm( n[1], depIndex );
+ if( sel.isNull() ){
depIndex = d_riter->getNumTerms()-1;
return Node::null();
}
- Node arr = n[0];
+ Node arr = d_model->getRepresentative( n[0] );
+ //if( n[0]!=d_model->getRepresentative( n[0] ) ){
+ // std::cout << n[0] << " is " << d_model->getRepresentative( n[0] ) << std::endl;
+ //}
+ int tempIndex;
int eval = 1;
while( arr.getKind()==STORE && eval!=0 ){
- int tempIndex;
- eval = evaluateEquality( selIndex, arr[1], tempIndex );
+ eval = evaluate( sel.eqNode( arr[1] ), tempIndex );
depIndex = tempIndex > depIndex ? tempIndex : depIndex;
if( eval==1 ){
val = evaluateTerm( arr[2], tempIndex );
@@ -345,90 +332,97 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
arr = arr[0];
}
}
- n = NodeManager::currentNM()->mkNode( SELECT, arr, selIndex );
- }
+ arr = evaluateTerm( arr, tempIndex );
+ depIndex = tempIndex > depIndex ? tempIndex : depIndex;
+ val = NodeManager::currentNM()->mkNode( SELECT, arr, sel );
+#else
+ val = evaluateTermDefault( n, depIndex, children_depIndex );
#endif
- //default term evaluate : evaluate all children, recreate the value
- std::vector< int > children_depIndex;
- val = evaluateTermDefault( n, depIndex, children_depIndex );
- //case split on the type of term
- if( n.getKind()==APPLY_UF ){
- Node op = n.getOperator();
- //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
- //if it is a defined UF, then consult the interpretation
- ++d_eval_uf_terms;
- int argDepIndex = 0;
- if( d_model->d_uf_model.find( op )!=d_model->d_uf_model.end() ){
- //make the term model specifically for n
- makeEvalUfModel( n );
- //now, consult the model
- if( d_eval_uf_use_default[n] ){
- val = d_model->d_uf_model[op].d_tree.getValue( d_model, val, argDepIndex );
- }else{
- val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex );
- }
+ }else{
+ //default term evaluate : evaluate all children, recreate the value
+ val = evaluateTermDefault( n, depIndex, children_depIndex );
+ }
+ if( !val.isNull() ){
+ bool setVal = false;
+ //custom ways of evaluating terms
+ if( n.getKind()==APPLY_UF ){
+ Node op = n.getOperator();
//Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
- //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );
- Assert( !val.isNull() );
- }else{
- d_eval_uf_use_default[n] = true;
- argDepIndex = (int)n.getNumChildren();
+ //if it is a defined UF, then consult the interpretation
+ if( d_model->d_uf_model_tree.find( op )!=d_model->d_uf_model_tree.end() ){
+ ++d_eval_uf_terms;
+ int argDepIndex = 0;
+ //make the term model specifically for n
+ makeEvalUfModel( n );
+ //now, consult the model
+ if( d_eval_uf_use_default[n] ){
+ val = d_model->d_uf_model_tree[op].getValue( d_model, val, argDepIndex );
+ }else{
+ val = d_eval_uf_model[ n ].getValue( d_model, val, argDepIndex );
+ }
+ //Debug("fmf-eval-debug") << "Evaluate term " << n << " (" << gn << ")" << std::endl;
+ //d_eval_uf_model[ n ].debugPrint("fmf-eval-debug", d_qe );
+ Assert( !val.isNull() );
+ //recalculate the depIndex
+ depIndex = -1;
+ for( int i=0; i<argDepIndex; i++ ){
+ int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
+ Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
+ if( children_depIndex[index]>depIndex ){
+ depIndex = children_depIndex[index];
+ }
+ }
+ setVal = true;
+ }
+ }else if( n.getKind()==SELECT ){
+ //we are free to interpret this term however we want
}
- //recalculate the depIndex
- depIndex = -1;
- for( int i=0; i<argDepIndex; i++ ){
- int index = d_eval_uf_use_default[n] ? i : d_eval_term_index_order[n][i];
- Debug("fmf-eval-debug") << "Add variables from " << index << "..." << std::endl;
- if( children_depIndex[index]>depIndex ){
- depIndex = children_depIndex[index];
+ //if not set already, rewrite and consult model for interpretation
+ if( !setVal ){
+ val = Rewriter::rewrite( val );
+ if( val.getMetaKind()!=kind::metakind::CONSTANT ){
+ //FIXME: we cannot do this until we trust all theories collectModelInfo!
+ //val = d_model->getInterpretedValue( val );
+ //val = d_model->getRepresentative( val );
}
}
Debug("fmf-eval-debug") << "Evaluate term " << n << " = ";
d_model->printRepresentativeDebug( "fmf-eval-debug", val );
Debug("fmf-eval-debug") << ", depIndex = " << depIndex << std::endl;
- }else if( n.getKind()==SELECT ){
- if( d_model->d_array_model.find( n[0] )!=d_model->d_array_model.end() ){
- //consult the default value for the array DO_THIS
- //val = Rewriter::rewrite( val );
- //val = d_model->d_array_model[ n[0] ];
- val = Rewriter::rewrite( val );
- }else{
- val = Rewriter::rewrite( val );
- }
- }else{
- val = Rewriter::rewrite( val );
}
}
return val;
- }else{
- depIndex = -1;
- return n;
}
}
Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){
- //first we must evaluate the arguments
- std::vector< Node > children;
- if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){
- children.push_back( n.getOperator() );
- }
depIndex = -1;
- //for each argument, calculate its value, and the variables its value depends upon
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- childDepIndex.push_back( -1 );
- Node nn = evaluateTerm( n[i], childDepIndex[i] );
- if( nn.isNull() ){
- depIndex = d_riter->getNumTerms()-1;
- return nn;
- }else{
- children.push_back( nn );
- if( childDepIndex[i]>depIndex ){
- depIndex = childDepIndex[i];
+ if( n.getNumChildren()==0 ){
+ return n;
+ }else{
+ //first we must evaluate the arguments
+ std::vector< Node > children;
+ if( n.getMetaKind()==kind::metakind::PARAMETERIZED ){
+ children.push_back( n.getOperator() );
+ }
+ //for each argument, calculate its value, and the variables its value depends upon
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ childDepIndex.push_back( -1 );
+ Node nn = evaluateTerm( n[i], childDepIndex[i] );
+ if( nn.isNull() ){
+ depIndex = d_riter->getNumTerms()-1;
+ return nn;
+ }else{
+ children.push_back( nn );
+ if( childDepIndex[i]>depIndex ){
+ depIndex = childDepIndex[i];
+ }
}
}
+ //recreate the value
+ Node val = NodeManager::currentNM()->mkNode( n.getKind(), children );
+ return val;
}
- //recreate the value
- return NodeManager::currentNM()->mkNode( n.getKind(), children );
}
void RepSetEvaluator::clearEvalFailed( int index ){
@@ -443,8 +437,8 @@ void RepSetEvaluator::makeEvalUfModel( Node n ){
makeEvalUfIndexOrder( n );
if( !d_eval_uf_use_default[n] ){
Node op = n.getOperator();
- d_eval_uf_model[n] = uf::UfModelTreeOrdered( op, d_eval_term_index_order[n] );
- d_model->d_uf_model[op].makeModel( d_eval_uf_model[n] );
+ d_eval_uf_model[n] = uf::UfModelTree( op, d_eval_term_index_order[n] );
+ d_model->d_uf_model_gen[op].makeModel( d_model, d_eval_uf_model[n] );
//Debug("fmf-index-order") << "Make model for " << n << " : " << std::endl;
//d_eval_uf_model[n].debugPrint( "fmf-index-order", d_qe, 2 );
}
diff --git a/src/theory/quantifiers/rep_set_iterator.h b/src/theory/quantifiers/rep_set_iterator.h
index 308d09a38..f6312ae5c 100644
--- a/src/theory/quantifiers/rep_set_iterator.h
+++ b/src/theory/quantifiers/rep_set_iterator.h
@@ -85,7 +85,7 @@ private:
private: //for Theory UF:
//map from terms to the models used to calculate their value
std::map< Node, bool > d_eval_uf_use_default;
- std::map< Node, uf::UfModelTreeOrdered > d_eval_uf_model;
+ 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;
@@ -103,13 +103,13 @@ public:
virtual ~RepSetEvaluator(){}
/** evaluate functions */
int evaluate( Node n, int& depIndex );
- int evaluateEquality( Node n1, Node n2, int& depIndex );
Node evaluateTerm( Node n, int& depIndex );
public:
//statistics
int d_eval_formulas;
- int d_eval_eqs;
int d_eval_uf_terms;
+ int d_eval_lits;
+ int d_eval_lits_unknown;
};
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 55715353d..945c82bf9 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -45,7 +45,7 @@ using namespace CVC4::theory::inst;
}
}
-void addTermEfficient( Node n, std::set< Node >& added){
+void TermDb::addTermEfficient( Node n, std::set< Node >& added){
static AvailableInTermDb aitdi;
if (Trigger::isAtomicTrigger( n ) && !n.getAttribute(aitdi)){
//Already processed but new in this branch
@@ -60,70 +60,69 @@ void addTermEfficient( Node n, std::set< Node >& added){
void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
- //don't add terms in quantifier bodies
+ //don't add terms in quantifier bodies
if( withinQuant && !Options::current()->registerQuantBodyTerms ){
return;
}
- if( d_processed.find( n )==d_processed.end() ){
+ if( d_processed.find( n )==d_processed.end() ){
++(d_quantEngine->d_statistics.d_term_in_termdb);
d_processed.insert(n);
+ d_type_map[ n.getType() ].push_back( n );
n.setAttribute(AvailableInTermDb(),true);
- //if this is an atomic trigger, consider adding it
+ //if this is an atomic trigger, consider adding it
//Call the children?
- if( Trigger::isAtomicTrigger( n ) || n.getKind() == kind::APPLY_CONSTRUCTOR ){
- if( !n.hasAttribute(InstConstantAttribute()) ){
- Debug("term-db") << "register trigger term " << n << std::endl;
+ if( Trigger::isAtomicTrigger( n ) ){
+ if( !n.hasAttribute(InstConstantAttribute()) ){
+ Debug("term-db") << "register trigger term " << n << std::endl;
//std::cout << "register trigger term " << n << std::endl;
- Node op = n.getOperator();
- d_op_map[op].push_back( n );
- d_type_map[ n.getType() ].push_back( n );
+ Node op = n.getOperator();
+ d_op_map[op].push_back( n );
added.insert( n );
- uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- addTerm( n[i], added, withinQuant );
- if( Options::current()->efficientEMatching ){
- if( d_parents[n[i]][op].empty() ){
- //must add parent to equivalence class info
- Node nir = d_ith->getRepresentative( n[i] );
- uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir );
- if( eci_nir ){
- eci_nir->d_pfuns[ op ] = true;
- }
- }
- //add to parent structure
- if( std::find( d_parents[n[i]][op][i].begin(), d_parents[n[i]][op][i].end(), n )==d_parents[n[i]][op][i].end() ){
- d_parents[n[i]][op][i].push_back( n );
+ uf::InstantiatorTheoryUf* d_ith = (uf::InstantiatorTheoryUf*)d_quantEngine->getInstantiator( THEORY_UF );
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ addTerm( n[i], added, withinQuant );
+ if( Options::current()->efficientEMatching ){
+ if( d_parents[n[i]][op].empty() ){
+ //must add parent to equivalence class info
+ Node nir = d_ith->getRepresentative( n[i] );
+ uf::EqClassInfo* eci_nir = d_ith->getEquivalenceClassInfo( nir );
+ if( eci_nir ){
+ eci_nir->d_pfuns[ op ] = true;
+ }
+ }
+ //add to parent structure
+ if( std::find( d_parents[n[i]][op][i].begin(), d_parents[n[i]][op][i].end(), n )==d_parents[n[i]][op][i].end() ){
+ d_parents[n[i]][op][i].push_back( n );
Assert(!getParents(n[i],op,i).empty());
- }
- }
- if( Options::current()->eagerInstQuant ){
- if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
- int addedLemmas = 0;
- for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
- addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n );
- }
- //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
- d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->getTheory( THEORY_QUANTIFIERS )->getOutputChannel() );
- }
- }
- }
- }
+ }
+ }
+ if( Options::current()->eagerInstQuant ){
+ if( !n.hasAttribute(InstLevelAttribute()) && n.getAttribute(InstLevelAttribute())==0 ){
+ int addedLemmas = 0;
+ for( int i=0; i<(int)d_ith->d_op_triggers[op].size(); i++ ){
+ addedLemmas += d_ith->d_op_triggers[op][i]->addTerm( n );
+ }
+ //Message() << "Terms, added lemmas: " << addedLemmas << std::endl;
+ d_quantEngine->flushLemmas( &d_quantEngine->getTheoryEngine()->getTheory( THEORY_QUANTIFIERS )->getOutputChannel() );
+ }
+ }
+ }
+ }
}else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- addTerm( n[i], added, withinQuant );
- }
- }
+ for( int i=0; i<(int)n.getNumChildren(); i++ ){
+ addTerm( n[i], added, withinQuant );
+ }
+ }
}else{
- if( Options::current()->efficientEMatching &&
- !n.hasAttribute(InstConstantAttribute())){
- //Efficient e-matching must be notified
- //The term in triggers are not important here
- Debug("term-db") << "New in this branch term " << n << std::endl;
- addTermEfficient(n,added);
- }
- }
-};
+ if( Options::current()->efficientEMatching && !n.hasAttribute(InstConstantAttribute())){
+ //Efficient e-matching must be notified
+ //The term in triggers are not important here
+ Debug("term-db") << "New in this branch term " << n << std::endl;
+ addTermEfficient(n,added);
+ }
+ }
+}
void TermDb::reset( Theory::Effort effort ){
int nonCongruentCount = 0;
@@ -158,7 +157,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
for( int i=0; i<2; i++ ){
Node n = NodeManager::currentNM()->mkConst( i==1 );
eq::EqClassIterator eqc( d_quantEngine->getEqualityQuery()->getRepresentative( n ),
- ((uf::TheoryUF*)d_quantEngine->getTheoryEngine()->getTheory( THEORY_UF ))->getEqualityEngine() );
+ d_quantEngine->getEqualityQuery()->getEngine() );
while( !eqc.isFinished() ){
Node en = (*eqc);
if( en.getKind()==APPLY_UF && !en.hasAttribute(InstConstantAttribute()) ){
@@ -194,12 +193,18 @@ void TermDb::registerModelBasis( Node n, Node gn ){
Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
- std::stringstream ss;
- ss << Expr::setlanguage(Options::current()->outputLanguage);
- ss << "e_" << tn;
- d_model_basis_term[tn] = NodeManager::currentNM()->mkVar( ss.str(), tn );
+ Node mbt;
+ if( d_type_map[ tn ].empty() ){
+ std::stringstream ss;
+ ss << Expr::setlanguage(Options::current()->outputLanguage);
+ ss << "e_" << tn;
+ mbt = NodeManager::currentNM()->mkVar( ss.str(), tn );
+ }else{
+ mbt = d_type_map[ tn ][ 0 ];
+ }
ModelBasisAttribute mba;
- d_model_basis_term[tn].setAttribute(mba,true);
+ mbt.setAttribute(mba,true);
+ d_model_basis_term[tn] = mbt;
}
return d_model_basis_term[tn];
}
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 5004a82dc..1ebba49b5 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -68,6 +68,9 @@ public:
void setMatchingActive( bool a ) { d_matching_active = a; }
/** get active */
bool getMatchingActive() { return d_matching_active; }
+private:
+ /** for efficient e-matching */
+ void addTermEfficient( Node n, std::set< Node >& added);
public:
/** parent structure (for efficient E-matching):
n -> op -> index -> L
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback