diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/Makefile.am | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 88 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 15 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 417 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 91 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 339 | ||||
-rw-r--r-- | src/theory/quantifiers/model_engine.h | 67 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 24 | ||||
-rw-r--r-- | src/theory/quantifiers/rep_set_iterator.cpp | 298 | ||||
-rw-r--r-- | src/theory/quantifiers/rep_set_iterator.h | 6 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 121 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 3 |
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
|