diff options
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 366 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 178 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 182 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 344 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.h | 108 | ||||
-rw-r--r-- | src/theory/quantifiers/rep_set_iterator.cpp | 1034 | ||||
-rw-r--r-- | src/theory/quantifiers/rep_set_iterator.h | 240 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 312 |
8 files changed, 1382 insertions, 1382 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 766bd31ae..1c6b47867 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -1,184 +1,184 @@ -/********************* */
-/*! \file first_order_model.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 engine model class
- **/
-
-#include "theory/quantifiers/first_order_model.h"
-#include "theory/quantifiers/rep_set_iterator.h"
-#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/term_database.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-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, true ),
-d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){
-
-}
-
-void FirstOrderModel::reset(){
- //rebuild models
- 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 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_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;
- }
- }
- }
-}
-
-void FirstOrderModel::initializeModelForTerm( Node n ){
- if( n.getKind()==APPLY_UF ){
- Node op = n.getOperator();
- if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){
- TypeNode tn = op.getType();
- tn = tn[ (int)tn.getNumChildren()-1 ];
- //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.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() ){
- Node value = d_array_model[n].getArrayValue();
- out << "(" << n << " " << value << ")" << std::endl;
- }
- */
- DefaultModel::toStreamFunction( n, out );
-}
-
-void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){
- DefaultModel::toStreamType( tn, out );
-}
-
-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_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{
- //std::cout << "no array model generated for " << n << std::endl;
- }
- */
- }else if( n.getKind()==APPLY_UF ){
- 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 );
-}
-
-TermDb* FirstOrderModel::getTermDatabase(){
- return d_term_db;
-}
-
-
-void FirstOrderModel::toStream(std::ostream& out){
- DefaultModel::toStream( out );
-#if 0
- out << "---Current Model---" << std::endl;
- out << "Representatives: " << std::endl;
- 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_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() ){
- Node eqc = (*eqcs_i);
- Node rep = getRepresentative( eqc );
- TypeNode type = rep.getType();
- eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
- while( !eqc_i.isFinished() ){
- //do not print things that have interpretations in model
- if( (*eqc_i).getMetaKind()!=kind::metakind::CONSTANT && !hasInterpretedValue( *eqc_i ) ){
- out << "(" << (*eqc_i) << " " << rep << ")" << std::endl;
- }
- ++eqc_i;
- }
- ++eqcs_i;
- }
- //print functions
- 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;
- }
-#endif
+/********************* */ +/*! \file first_order_model.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 engine model class + **/ + +#include "theory/quantifiers/first_order_model.h" +#include "theory/quantifiers/rep_set_iterator.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/term_database.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +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, true ), +d_term_db( qe->getTermDatabase() ), d_forall_asserts( c ){ + +} + +void FirstOrderModel::reset(){ + //rebuild models + 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 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_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; + } + } + } +} + +void FirstOrderModel::initializeModelForTerm( Node n ){ + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( d_uf_model_tree.find( op )==d_uf_model_tree.end() ){ + TypeNode tn = op.getType(); + tn = tn[ (int)tn.getNumChildren()-1 ]; + //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.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() ){ + Node value = d_array_model[n].getArrayValue(); + out << "(" << n << " " << value << ")" << std::endl; + } + */ + DefaultModel::toStreamFunction( n, out ); +} + +void FirstOrderModel::toStreamType( TypeNode tn, std::ostream& out ){ + DefaultModel::toStreamType( tn, out ); +} + +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_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{ + //std::cout << "no array model generated for " << n << std::endl; + } + */ + }else if( n.getKind()==APPLY_UF ){ + 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 ); +} + +TermDb* FirstOrderModel::getTermDatabase(){ + return d_term_db; +} + + +void FirstOrderModel::toStream(std::ostream& out){ + DefaultModel::toStream( out ); +#if 0 + out << "---Current Model---" << std::endl; + out << "Representatives: " << std::endl; + 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_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() ){ + Node eqc = (*eqcs_i); + Node rep = getRepresentative( eqc ); + TypeNode type = rep.getType(); + eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); + while( !eqc_i.isFinished() ){ + //do not print things that have interpretations in model + if( (*eqc_i).getMetaKind()!=kind::metakind::CONSTANT && !hasInterpretedValue( *eqc_i ) ){ + out << "(" << (*eqc_i) << " " << rep << ")" << std::endl; + } + ++eqc_i; + } + ++eqcs_i; + } + //print functions + 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; + } +#endif }
\ No newline at end of file diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 825518ed0..afa8dab79 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -1,89 +1,89 @@ -/********************* */
-/*! \file first_order_model.h
- ** \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 Model extended classes
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__FIRST_ORDER_MODEL_H
-#define __CVC4__FIRST_ORDER_MODEL_H
-
-#include "theory/model.h"
-#include "theory/uf/theory_uf_model.h"
-#include "theory/arrays/theory_arrays_model.h"
-
-namespace CVC4 {
-namespace theory {
-
-struct ModelBasisAttributeId {};
-typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute;
-//for APPLY_UF terms, 1 : term has direct child with model basis attribute,
-// 0 : term has no direct child with model basis attribute.
-struct ModelBasisArgAttributeId {};
-typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute;
-
-class QuantifiersEngine;
-
-namespace quantifiers{
-
-class TermDb;
-
-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 */
- void toStreamFunction( Node n, std::ostream& out );
- void toStreamType( TypeNode tn, std::ostream& out );
-public: //for Theory UF:
- //models for each UF operator
- std::map< Node, uf::UfModelTree > d_uf_model_tree;
- //model generators
- std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen;
-public: //for Theory Arrays:
- //default value for each non-store array
- 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;
- /** get number of asserted quantifiers */
- int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); }
- /** get asserted quantifier */
- Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; }
-public:
- FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name );
- virtual ~FirstOrderModel(){}
- // 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 */
- void toStream( std::ostream& out );
-};
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file first_order_model.h + ** \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 Model extended classes + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__FIRST_ORDER_MODEL_H +#define __CVC4__FIRST_ORDER_MODEL_H + +#include "theory/model.h" +#include "theory/uf/theory_uf_model.h" +#include "theory/arrays/theory_arrays_model.h" + +namespace CVC4 { +namespace theory { + +struct ModelBasisAttributeId {}; +typedef expr::Attribute<ModelBasisAttributeId, bool> ModelBasisAttribute; +//for APPLY_UF terms, 1 : term has direct child with model basis attribute, +// 0 : term has no direct child with model basis attribute. +struct ModelBasisArgAttributeId {}; +typedef expr::Attribute<ModelBasisArgAttributeId, uint64_t> ModelBasisArgAttribute; + +class QuantifiersEngine; + +namespace quantifiers{ + +class TermDb; + +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 */ + void toStreamFunction( Node n, std::ostream& out ); + void toStreamType( TypeNode tn, std::ostream& out ); +public: //for Theory UF: + //models for each UF operator + std::map< Node, uf::UfModelTree > d_uf_model_tree; + //model generators + std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen; +public: //for Theory Arrays: + //default value for each non-store array + 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; + /** get number of asserted quantifiers */ + int getNumAssertedQuantifiers() { return (int)d_forall_asserts.size(); } + /** get asserted quantifier */ + Node getAssertedQuantifier( int i ) { return d_forall_asserts[i]; } +public: + FirstOrderModel( QuantifiersEngine* qe, context::Context* c, std::string name ); + virtual ~FirstOrderModel(){} + // 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 */ + void toStream( std::ostream& out ); +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 13d500d8e..05eb8f55f 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -1,91 +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
+/********************* */ +/*! \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/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 12206e148..1563a3d1d 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -1,173 +1,173 @@ -/********************* */
-/*! \file relevant_domain.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 relevant domain class
- **/
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/relevant_domain.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/first_order_model.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){
-
-}
-
-void RelevantDomain::compute(){
- d_quant_inst_domain.clear();
- for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
- Node f = d_model->getAssertedQuantifier( i );
- d_quant_inst_domain[f].resize( f[0].getNumChildren() );
- }
- //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment)
- for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin();
- it != d_model->d_uf_model_tree.end(); ++it ){
- Node op = it->first;
- for( size_t i=0; i<d_model->d_uf_terms[op].size(); i++ ){
- Node n = d_model->d_uf_terms[op][i];
- //add arguments to domain
- for( int j=0; j<(int)n.getNumChildren(); j++ ){
- if( d_model->d_rep_set.hasType( n[j].getType() ) ){
- Node ra = d_model->getRepresentative( n[j] );
- int raIndex = d_model->d_rep_set.getIndexFor( ra );
- Assert( raIndex!=-1 );
- if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){
- d_active_domain[op][j].push_back( raIndex );
- }
- }
- }
- //add to range
- Node r = d_model->getRepresentative( n );
- int raIndex = d_model->d_rep_set.getIndexFor( r );
- 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 );
- }
- }
- }
- //find fixed point for relevant domain computation
- bool success;
- do{
- success = true;
- for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){
- Node f = d_model->getAssertedQuantifier( i );
- //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment)
- if( computeRelevantInstantiationDomain( d_model->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, d_quant_inst_domain[f] ) ){
- success = false;
- }
- //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment)
- RepDomain range;
- if( extendFunctionDomains( d_model->getTermDatabase()->getCounterexampleBody( f ), range ) ){
- success = false;
- }
- }
- }while( !success );
-}
-
-bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ){
- bool domainChanged = false;
- if( n.getKind()==INST_CONSTANT ){
- bool domainSet = false;
- int vi = n.getAttribute(InstVarNumAttribute());
- Assert( !parent.isNull() );
- if( parent.getKind()==APPLY_UF ){
- //if the child of APPLY_UF term f( ... ), only consider the active domain of f at given argument
- Node op = parent.getOperator();
- if( d_active_domain.find( op )!=d_active_domain.end() ){
- for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){
- int d = d_active_domain[op][arg][i];
- if( std::find( rd[vi].begin(), rd[vi].end(), d )==rd[vi].end() ){
- rd[vi].push_back( d );
- domainChanged = true;
- }
- }
- domainSet = true;
- }
- }
- if( !domainSet ){
- //otherwise, we must consider the entire domain
- TypeNode tn = n.getType();
- 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_rep_set.d_type_reps[tn].size(); i++ ){
- rd[vi].push_back( i );
- domainChanged = true;
- }
- }
- }else{
- //infinite domain?
- }
- }
- }else{
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){
- domainChanged = true;
- }
- }
- }
- return domainChanged;
-}
-
-bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){
- if( n.getKind()==INST_CONSTANT ){
- Node f = n.getAttribute(InstConstantAttribute());
- int var = n.getAttribute(InstVarNumAttribute());
- range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() );
- return false;
- }else{
- Node op;
- if( n.getKind()==APPLY_UF ){
- op = n.getOperator();
- }
- bool domainChanged = false;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- RepDomain childRange;
- if( extendFunctionDomains( n[i], childRange ) ){
- domainChanged = true;
- }
- if( n.getKind()==APPLY_UF ){
- if( d_active_domain.find( op )!=d_active_domain.end() ){
- for( int j=0; j<(int)childRange.size(); j++ ){
- int v = childRange[j];
- if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){
- d_active_domain[op][i].push_back( v );
- domainChanged = true;
- }
- }
- }else{
- //do this?
- }
- }
- }
- //get the range
- if( n.hasAttribute(InstConstantAttribute()) ){
- if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){
- range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() );
- }else{
- //infinite range?
- }
- }else{
- Node r = d_model->getRepresentative( n );
- range.push_back( d_model->d_rep_set.getIndexFor( r ) );
- }
- return domainChanged;
- }
+/********************* */ +/*! \file relevant_domain.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 relevant domain class + **/ + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/relevant_domain.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +RelevantDomain::RelevantDomain( FirstOrderModel* m ) : d_model( m ){ + +} + +void RelevantDomain::compute(){ + d_quant_inst_domain.clear(); + for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ + Node f = d_model->getAssertedQuantifier( i ); + d_quant_inst_domain[f].resize( f[0].getNumChildren() ); + } + //add ground terms to domain (rule 1 of complete instantiation essentially uf fragment) + for( std::map< Node, uf::UfModelTree >::iterator it = d_model->d_uf_model_tree.begin(); + it != d_model->d_uf_model_tree.end(); ++it ){ + Node op = it->first; + for( size_t i=0; i<d_model->d_uf_terms[op].size(); i++ ){ + Node n = d_model->d_uf_terms[op][i]; + //add arguments to domain + for( int j=0; j<(int)n.getNumChildren(); j++ ){ + if( d_model->d_rep_set.hasType( n[j].getType() ) ){ + Node ra = d_model->getRepresentative( n[j] ); + int raIndex = d_model->d_rep_set.getIndexFor( ra ); + Assert( raIndex!=-1 ); + if( std::find( d_active_domain[op][j].begin(), d_active_domain[op][j].end(), raIndex )==d_active_domain[op][j].end() ){ + d_active_domain[op][j].push_back( raIndex ); + } + } + } + //add to range + Node r = d_model->getRepresentative( n ); + int raIndex = d_model->d_rep_set.getIndexFor( r ); + 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 ); + } + } + } + //find fixed point for relevant domain computation + bool success; + do{ + success = true; + for( int i=0; i<(int)d_model->getNumAssertedQuantifiers(); i++ ){ + Node f = d_model->getAssertedQuantifier( i ); + //compute the domain of relevant instantiations (rule 3 of complete instantiation, essentially uf fragment) + if( computeRelevantInstantiationDomain( d_model->getTermDatabase()->getCounterexampleBody( f ), Node::null(), -1, d_quant_inst_domain[f] ) ){ + success = false; + } + //extend the possible domain for functions (rule 2 of complete instantiation, essentially uf fragment) + RepDomain range; + if( extendFunctionDomains( d_model->getTermDatabase()->getCounterexampleBody( f ), range ) ){ + success = false; + } + } + }while( !success ); +} + +bool RelevantDomain::computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ){ + bool domainChanged = false; + if( n.getKind()==INST_CONSTANT ){ + bool domainSet = false; + int vi = n.getAttribute(InstVarNumAttribute()); + Assert( !parent.isNull() ); + if( parent.getKind()==APPLY_UF ){ + //if the child of APPLY_UF term f( ... ), only consider the active domain of f at given argument + Node op = parent.getOperator(); + if( d_active_domain.find( op )!=d_active_domain.end() ){ + for( size_t i=0; i<d_active_domain[op][arg].size(); i++ ){ + int d = d_active_domain[op][arg][i]; + if( std::find( rd[vi].begin(), rd[vi].end(), d )==rd[vi].end() ){ + rd[vi].push_back( d ); + domainChanged = true; + } + } + domainSet = true; + } + } + if( !domainSet ){ + //otherwise, we must consider the entire domain + TypeNode tn = n.getType(); + 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_rep_set.d_type_reps[tn].size(); i++ ){ + rd[vi].push_back( i ); + domainChanged = true; + } + } + }else{ + //infinite domain? + } + } + }else{ + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( computeRelevantInstantiationDomain( n[i], n, i, rd ) ){ + domainChanged = true; + } + } + } + return domainChanged; +} + +bool RelevantDomain::extendFunctionDomains( Node n, RepDomain& range ){ + if( n.getKind()==INST_CONSTANT ){ + Node f = n.getAttribute(InstConstantAttribute()); + int var = n.getAttribute(InstVarNumAttribute()); + range.insert( range.begin(), d_quant_inst_domain[f][var].begin(), d_quant_inst_domain[f][var].end() ); + return false; + }else{ + Node op; + if( n.getKind()==APPLY_UF ){ + op = n.getOperator(); + } + bool domainChanged = false; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + RepDomain childRange; + if( extendFunctionDomains( n[i], childRange ) ){ + domainChanged = true; + } + if( n.getKind()==APPLY_UF ){ + if( d_active_domain.find( op )!=d_active_domain.end() ){ + for( int j=0; j<(int)childRange.size(); j++ ){ + int v = childRange[j]; + if( std::find( d_active_domain[op][i].begin(), d_active_domain[op][i].end(), v )==d_active_domain[op][i].end() ){ + d_active_domain[op][i].push_back( v ); + domainChanged = true; + } + } + }else{ + //do this? + } + } + } + //get the range + if( n.hasAttribute(InstConstantAttribute()) ){ + if( n.getKind()==APPLY_UF && d_active_range.find( op )!=d_active_range.end() ){ + range.insert( range.end(), d_active_range[op].begin(), d_active_range[op].end() ); + }else{ + //infinite range? + } + }else{ + Node r = d_model->getRepresentative( n ); + range.push_back( d_model->d_rep_set.getIndexFor( r ) ); + } + return domainChanged; + } }
\ No newline at end of file diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 362a39d6a..8c8ea6a42 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -1,54 +1,54 @@ -/********************* */
-/*! \file relevant_domain.h
- ** \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 relevant domain class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__RELEVANT_DOMAIN_H
-#define __CVC4__RELEVANT_DOMAIN_H
-
-#include "theory/quantifiers/first_order_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-class RelevantDomain
-{
-private:
- FirstOrderModel* d_model;
-
- //the domain of the arguments for each operator
- std::map< Node, std::map< int, RepDomain > > d_active_domain;
- //the range for each operator
- std::map< Node, RepDomain > d_active_range;
- //for computing relevant instantiation domain, return true if changed
- bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd );
- //for computing extended
- bool extendFunctionDomains( Node n, RepDomain& range );
-public:
- RelevantDomain( FirstOrderModel* m );
- virtual ~RelevantDomain(){}
- //compute the relevant domain
- void compute();
- //relevant instantiation domain for each quantifier
- std::map< Node, std::vector< RepDomain > > d_quant_inst_domain;
-};
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file relevant_domain.h + ** \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 relevant domain class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__RELEVANT_DOMAIN_H +#define __CVC4__RELEVANT_DOMAIN_H + +#include "theory/quantifiers/first_order_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +class RelevantDomain +{ +private: + FirstOrderModel* d_model; + + //the domain of the arguments for each operator + std::map< Node, std::map< int, RepDomain > > d_active_domain; + //the range for each operator + std::map< Node, RepDomain > d_active_range; + //for computing relevant instantiation domain, return true if changed + bool computeRelevantInstantiationDomain( Node n, Node parent, int arg, std::vector< RepDomain >& rd ); + //for computing extended + bool extendFunctionDomains( Node n, RepDomain& range ); +public: + RelevantDomain( FirstOrderModel* m ); + virtual ~RelevantDomain(){} + //compute the relevant domain + void compute(); + //relevant instantiation domain for each quantifier + std::map< Node, std::vector< RepDomain > > d_quant_inst_domain; +}; + +} +} +} + +#endif diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp index 516f85857..9c1c4c89e 100644 --- a/src/theory/quantifiers/rep_set_iterator.cpp +++ b/src/theory/quantifiers/rep_set_iterator.cpp @@ -1,517 +1,517 @@ -/********************* */
-/*! \file rep_set_iterator.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 relevant domain class
- **/
-
-#include "theory/quantifiers/rep_set_iterator.h"
-#include "theory/quantifiers/model_engine.h"
-#include "theory/quantifiers/term_database.h"
-
-#define USE_INDEX_ORDERING
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::quantifiers;
-
-RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_model( model ){
- //store instantiation constants
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- d_index.push_back( 0 );
- }
- for( size_t i=0; i<f[0].getNumChildren(); i++ ){
- //store default index order
- d_index_order.push_back( i );
- d_var_order[i] = i;
- //store default domain
- d_domain.push_back( RepDomain() );
- 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");
- }
- }
-}
-
-void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){
- d_index_order.clear();
- d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() );
- //make the d_var_order mapping
- for( int i=0; i<(int)d_index_order.size(); i++ ){
- d_var_order[d_index_order[i]] = i;
- }
-}
-
-void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){
- d_domain.clear();
- d_domain.insert( d_domain.begin(), domain.begin(), domain.end() );
- //we are done if a domain is empty
- for( int i=0; i<(int)d_domain.size(); i++ ){
- if( d_domain[i].empty() ){
- d_index.clear();
- }
- }
-}
-
-void RepSetIterator::increment2( int counter ){
- Assert( !isFinished() );
-#ifdef DISABLE_EVAL_SKIP_MULTIPLE
- counter = (int)d_index.size()-1;
-#endif
- //increment d_index
- while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){
- counter--;
- }
- if( counter==-1 ){
- d_index.clear();
- }else{
- for( int i=(int)d_index.size()-1; i>counter; i-- ){
- d_index[i] = 0;
- //d_model->clearEvalFailed( i );
- }
- d_index[counter]++;
- //d_model->clearEvalFailed( counter );
- }
-}
-
-void RepSetIterator::increment(){
- if( !isFinished() ){
- increment2( (int)d_index.size()-1 );
- }
-}
-
-bool RepSetIterator::isFinished(){
- return d_index.empty();
-}
-
-void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){
- for( int i=0; i<(int)d_index.size(); i++ ){
- m.set( qe->getTermDatabase()->getInstantiationConstant( d_f, d_index_order[i] ), getTerm( i ));
- }
-}
-
-Node RepSetIterator::getTerm( int i ){
- TypeNode tn = d_f[0][d_index_order[i]].getType();
- 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_rep_set.d_type_reps[tn][d_domain[index][d_index[index]]];
-}
-
-void RepSetIterator::debugPrint( const char* c ){
- for( int i=0; i<(int)d_index.size(); i++ ){
- Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl;
- }
-}
-
-void RepSetIterator::debugPrintSmall( const char* c ){
- Debug( c ) << "RI: ";
- for( int i=0; i<(int)d_index.size(); i++ ){
- Debug( c ) << d_index[i] << ": " << getTerm( i ) << " ";
- }
- Debug( c ) << std::endl;
-}
-
-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 ) = 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;
- //Notice() << "Eval " << n << std::endl;
- if( n.getKind()==NOT ){
- int val = evaluate( n[0], depIndex );
- return val==1 ? -1 : ( val==-1 ? 1 : 0 );
- }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){
- int baseVal = n.getKind()==AND ? 1 : -1;
- int eVal = baseVal;
- int posDepIndex = d_riter->getNumTerms();
- int negDepIndex = -1;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- //evaluate subterm
- int childDepIndex;
- Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i];
- int eValT = evaluate( nn, childDepIndex );
- if( eValT==baseVal ){
- if( eVal==baseVal ){
- if( childDepIndex>negDepIndex ){
- negDepIndex = childDepIndex;
- }
- }
- }else if( eValT==-baseVal ){
- eVal = -baseVal;
- if( childDepIndex<posDepIndex ){
- posDepIndex = childDepIndex;
- if( posDepIndex==-1 ){
- break;
- }
- }
- }else if( eValT==0 ){
- if( eVal==baseVal ){
- eVal = 0;
- }
- }
- }
- if( eVal!=0 ){
- depIndex = eVal==-baseVal ? posDepIndex : negDepIndex;
- return eVal;
- }else{
- return 0;
- }
- }else if( n.getKind()==IFF || n.getKind()==XOR ){
- int depIndex1;
- int eVal = evaluate( n[0], depIndex1 );
- if( eVal!=0 ){
- int depIndex2;
- int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 );
- if( eVal2!=0 ){
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- return eVal==eVal2 ? 1 : -1;
- }
- }
- return 0;
- }else if( n.getKind()==ITE ){
- int depIndex1, depIndex2;
- int eVal = evaluate( n[0], depIndex1 );
- if( eVal==0 ){
- //evaluate children to see if they are the same value
- int eval1 = evaluate( n[1], depIndex1 );
- if( eval1!=0 ){
- int eval2 = evaluate( n[1], depIndex2 );
- if( eval1==eval2 ){
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- return eval1;
- }
- }
- }else{
- int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2 );
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- return eValT;
- }
- return 0;
- }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] ){
- // return -1;
- // }
- //}
- //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl;
- int retVal = 0;
- depIndex = d_riter->getNumTerms()-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 << ", 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;
- }
-}
-
-Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){
- //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
- if( n.getKind()==INST_CONSTANT ){
- int v = n.getAttribute(InstVarNumAttribute());
- depIndex = d_riter->d_var_order[ v ];
- val = d_riter->getTerm( v );
- }else if( n.getKind()==ITE ){
- int depIndex1, depIndex2;
- int eval = evaluate( n[0], depIndex1 );
- if( eval==0 ){
- //evaluate children to see if they are the same
- Node val1 = evaluateTerm( n[ 1 ], depIndex1 );
- Node val2 = evaluateTerm( n[ 2 ], depIndex2 );
- if( val1==val2 ){
- val = val1;
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- }else{
- return Node::null();
- }
- }else{
- val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2 );
- depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2;
- }
- }else{
- std::vector< int > children_depIndex;
- //for select, pre-process read over writes
- if( n.getKind()==SELECT ){
-#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 = 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 ){
- eval = evaluate( sel.eqNode( arr[1] ), tempIndex );
- depIndex = tempIndex > depIndex ? tempIndex : depIndex;
- if( eval==1 ){
- val = evaluateTerm( arr[2], tempIndex );
- depIndex = tempIndex > depIndex ? tempIndex : depIndex;
- return val;
- }else if( eval==-1 ){
- arr = arr[0];
- }
- }
- arr = evaluateTerm( arr, tempIndex );
- depIndex = tempIndex > depIndex ? tempIndex : depIndex;
- val = NodeManager::currentNM()->mkNode( SELECT, arr, sel );
-#else
- val = evaluateTermDefault( n, depIndex, children_depIndex );
-#endif
- }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;
- //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
- }
- //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;
- }
- }
- return val;
- }
-}
-
-Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){
- depIndex = -1;
- 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;
- }
-}
-
-void RepSetEvaluator::clearEvalFailed( int index ){
- for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){
- d_eval_failed[ d_eval_failed_lits[index][i] ] = false;
- }
- d_eval_failed_lits[index].clear();
-}
-
-void RepSetEvaluator::makeEvalUfModel( Node n ){
- if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){
- makeEvalUfIndexOrder( n );
- if( !d_eval_uf_use_default[n] ){
- Node op = n.getOperator();
- 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 );
- }
- }
-}
-
-struct sortGetMaxVariableNum {
- std::map< Node, int > d_max_var_num;
- int computeMaxVariableNum( Node n ){
- if( n.getKind()==INST_CONSTANT ){
- return n.getAttribute(InstVarNumAttribute());
- }else if( n.hasAttribute(InstConstantAttribute()) ){
- int maxVal = -1;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- int val = getMaxVariableNum( n[i] );
- if( val>maxVal ){
- maxVal = val;
- }
- }
- return maxVal;
- }else{
- return -1;
- }
- }
- int getMaxVariableNum( Node n ){
- std::map< Node, int >::iterator it = d_max_var_num.find( n );
- if( it==d_max_var_num.end() ){
- int num = computeMaxVariableNum( n );
- d_max_var_num[n] = num;
- return num;
- }else{
- return it->second;
- }
- }
- bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));}
-};
-
-void RepSetEvaluator::makeEvalUfIndexOrder( Node n ){
- if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){
-#ifdef USE_INDEX_ORDERING
- //sort arguments in order of least significant vs. most significant variable in default ordering
- std::map< Node, std::vector< int > > argIndex;
- std::vector< Node > args;
- for( int i=0; i<(int)n.getNumChildren(); i++ ){
- if( argIndex.find( n[i] )==argIndex.end() ){
- args.push_back( n[i] );
- }
- argIndex[n[i]].push_back( i );
- }
- sortGetMaxVariableNum sgmvn;
- std::sort( args.begin(), args.end(), sgmvn );
- for( int i=0; i<(int)args.size(); i++ ){
- for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){
- d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] );
- }
- }
- bool useDefault = true;
- for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
- if( i!=d_eval_term_index_order[n][i] ){
- useDefault = false;
- break;
- }
- }
- d_eval_uf_use_default[n] = useDefault;
- Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : ";
- for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){
- Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " ";
- }
- Debug("fmf-index-order") << std::endl;
-#else
- d_eval_uf_use_default[n] = true;
-#endif
- }
-}
-
-
+/********************* */ +/*! \file rep_set_iterator.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 relevant domain class + **/ + +#include "theory/quantifiers/rep_set_iterator.h" +#include "theory/quantifiers/model_engine.h" +#include "theory/quantifiers/term_database.h" + +#define USE_INDEX_ORDERING + +using namespace std; +using namespace CVC4; +using namespace CVC4::kind; +using namespace CVC4::context; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; + +RepSetIterator::RepSetIterator( Node f, FirstOrderModel* model ) : d_f( f ), d_model( model ){ + //store instantiation constants + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + d_index.push_back( 0 ); + } + for( size_t i=0; i<f[0].getNumChildren(); i++ ){ + //store default index order + d_index_order.push_back( i ); + d_var_order[i] = i; + //store default domain + d_domain.push_back( RepDomain() ); + 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"); + } + } +} + +void RepSetIterator::setIndexOrder( std::vector< int >& indexOrder ){ + d_index_order.clear(); + d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() ); + //make the d_var_order mapping + for( int i=0; i<(int)d_index_order.size(); i++ ){ + d_var_order[d_index_order[i]] = i; + } +} + +void RepSetIterator::setDomain( std::vector< RepDomain >& domain ){ + d_domain.clear(); + d_domain.insert( d_domain.begin(), domain.begin(), domain.end() ); + //we are done if a domain is empty + for( int i=0; i<(int)d_domain.size(); i++ ){ + if( d_domain[i].empty() ){ + d_index.clear(); + } + } +} + +void RepSetIterator::increment2( int counter ){ + Assert( !isFinished() ); +#ifdef DISABLE_EVAL_SKIP_MULTIPLE + counter = (int)d_index.size()-1; +#endif + //increment d_index + while( counter>=0 && d_index[counter]==(int)(d_domain[counter].size()-1) ){ + counter--; + } + if( counter==-1 ){ + d_index.clear(); + }else{ + for( int i=(int)d_index.size()-1; i>counter; i-- ){ + d_index[i] = 0; + //d_model->clearEvalFailed( i ); + } + d_index[counter]++; + //d_model->clearEvalFailed( counter ); + } +} + +void RepSetIterator::increment(){ + if( !isFinished() ){ + increment2( (int)d_index.size()-1 ); + } +} + +bool RepSetIterator::isFinished(){ + return d_index.empty(); +} + +void RepSetIterator::getMatch( QuantifiersEngine* qe, InstMatch& m ){ + for( int i=0; i<(int)d_index.size(); i++ ){ + m.set( qe->getTermDatabase()->getInstantiationConstant( d_f, d_index_order[i] ), getTerm( i )); + } +} + +Node RepSetIterator::getTerm( int i ){ + TypeNode tn = d_f[0][d_index_order[i]].getType(); + 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_rep_set.d_type_reps[tn][d_domain[index][d_index[index]]]; +} + +void RepSetIterator::debugPrint( const char* c ){ + for( int i=0; i<(int)d_index.size(); i++ ){ + Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl; + } +} + +void RepSetIterator::debugPrintSmall( const char* c ){ + Debug( c ) << "RI: "; + for( int i=0; i<(int)d_index.size(); i++ ){ + Debug( c ) << d_index[i] << ": " << getTerm( i ) << " "; + } + Debug( c ) << std::endl; +} + +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 ) = 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; + //Notice() << "Eval " << n << std::endl; + if( n.getKind()==NOT ){ + int val = evaluate( n[0], depIndex ); + return val==1 ? -1 : ( val==-1 ? 1 : 0 ); + }else if( n.getKind()==OR || n.getKind()==AND || n.getKind()==IMPLIES ){ + int baseVal = n.getKind()==AND ? 1 : -1; + int eVal = baseVal; + int posDepIndex = d_riter->getNumTerms(); + int negDepIndex = -1; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + //evaluate subterm + int childDepIndex; + Node nn = ( i==0 && n.getKind()==IMPLIES ) ? n[i].notNode() : n[i]; + int eValT = evaluate( nn, childDepIndex ); + if( eValT==baseVal ){ + if( eVal==baseVal ){ + if( childDepIndex>negDepIndex ){ + negDepIndex = childDepIndex; + } + } + }else if( eValT==-baseVal ){ + eVal = -baseVal; + if( childDepIndex<posDepIndex ){ + posDepIndex = childDepIndex; + if( posDepIndex==-1 ){ + break; + } + } + }else if( eValT==0 ){ + if( eVal==baseVal ){ + eVal = 0; + } + } + } + if( eVal!=0 ){ + depIndex = eVal==-baseVal ? posDepIndex : negDepIndex; + return eVal; + }else{ + return 0; + } + }else if( n.getKind()==IFF || n.getKind()==XOR ){ + int depIndex1; + int eVal = evaluate( n[0], depIndex1 ); + if( eVal!=0 ){ + int depIndex2; + int eVal2 = evaluate( n.getKind()==XOR ? n[1].notNode() : n[1], depIndex2 ); + if( eVal2!=0 ){ + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + return eVal==eVal2 ? 1 : -1; + } + } + return 0; + }else if( n.getKind()==ITE ){ + int depIndex1, depIndex2; + int eVal = evaluate( n[0], depIndex1 ); + if( eVal==0 ){ + //evaluate children to see if they are the same value + int eval1 = evaluate( n[1], depIndex1 ); + if( eval1!=0 ){ + int eval2 = evaluate( n[1], depIndex2 ); + if( eval1==eval2 ){ + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + return eval1; + } + } + }else{ + int eValT = evaluate( n[eVal==1 ? 1 : 2], depIndex2 ); + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + return eValT; + } + return 0; + }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] ){ + // return -1; + // } + //} + //Debug("fmf-eval-debug") << "Evaluate literal " << n << std::endl; + int retVal = 0; + depIndex = d_riter->getNumTerms()-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 << ", 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; + } +} + +Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){ + //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 + if( n.getKind()==INST_CONSTANT ){ + int v = n.getAttribute(InstVarNumAttribute()); + depIndex = d_riter->d_var_order[ v ]; + val = d_riter->getTerm( v ); + }else if( n.getKind()==ITE ){ + int depIndex1, depIndex2; + int eval = evaluate( n[0], depIndex1 ); + if( eval==0 ){ + //evaluate children to see if they are the same + Node val1 = evaluateTerm( n[ 1 ], depIndex1 ); + Node val2 = evaluateTerm( n[ 2 ], depIndex2 ); + if( val1==val2 ){ + val = val1; + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + }else{ + return Node::null(); + } + }else{ + val = evaluateTerm( n[ eval==1 ? 1 : 2 ], depIndex2 ); + depIndex = depIndex1>depIndex2 ? depIndex1 : depIndex2; + } + }else{ + std::vector< int > children_depIndex; + //for select, pre-process read over writes + if( n.getKind()==SELECT ){ +#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 = 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 ){ + eval = evaluate( sel.eqNode( arr[1] ), tempIndex ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + if( eval==1 ){ + val = evaluateTerm( arr[2], tempIndex ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + return val; + }else if( eval==-1 ){ + arr = arr[0]; + } + } + arr = evaluateTerm( arr, tempIndex ); + depIndex = tempIndex > depIndex ? tempIndex : depIndex; + val = NodeManager::currentNM()->mkNode( SELECT, arr, sel ); +#else + val = evaluateTermDefault( n, depIndex, children_depIndex ); +#endif + }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; + //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 + } + //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; + } + } + return val; + } +} + +Node RepSetEvaluator::evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ){ + depIndex = -1; + 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; + } +} + +void RepSetEvaluator::clearEvalFailed( int index ){ + for( int i=0; i<(int)d_eval_failed_lits[index].size(); i++ ){ + d_eval_failed[ d_eval_failed_lits[index][i] ] = false; + } + d_eval_failed_lits[index].clear(); +} + +void RepSetEvaluator::makeEvalUfModel( Node n ){ + if( d_eval_uf_model.find( n )==d_eval_uf_model.end() ){ + makeEvalUfIndexOrder( n ); + if( !d_eval_uf_use_default[n] ){ + Node op = n.getOperator(); + 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 ); + } + } +} + +struct sortGetMaxVariableNum { + std::map< Node, int > d_max_var_num; + int computeMaxVariableNum( Node n ){ + if( n.getKind()==INST_CONSTANT ){ + return n.getAttribute(InstVarNumAttribute()); + }else if( n.hasAttribute(InstConstantAttribute()) ){ + int maxVal = -1; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + int val = getMaxVariableNum( n[i] ); + if( val>maxVal ){ + maxVal = val; + } + } + return maxVal; + }else{ + return -1; + } + } + int getMaxVariableNum( Node n ){ + std::map< Node, int >::iterator it = d_max_var_num.find( n ); + if( it==d_max_var_num.end() ){ + int num = computeMaxVariableNum( n ); + d_max_var_num[n] = num; + return num; + }else{ + return it->second; + } + } + bool operator() (Node i,Node j) { return (getMaxVariableNum(i)<getMaxVariableNum(j));} +}; + +void RepSetEvaluator::makeEvalUfIndexOrder( Node n ){ + if( d_eval_term_index_order.find( n )==d_eval_term_index_order.end() ){ +#ifdef USE_INDEX_ORDERING + //sort arguments in order of least significant vs. most significant variable in default ordering + std::map< Node, std::vector< int > > argIndex; + std::vector< Node > args; + for( int i=0; i<(int)n.getNumChildren(); i++ ){ + if( argIndex.find( n[i] )==argIndex.end() ){ + args.push_back( n[i] ); + } + argIndex[n[i]].push_back( i ); + } + sortGetMaxVariableNum sgmvn; + std::sort( args.begin(), args.end(), sgmvn ); + for( int i=0; i<(int)args.size(); i++ ){ + for( int j=0; j<(int)argIndex[ args[i] ].size(); j++ ){ + d_eval_term_index_order[n].push_back( argIndex[ args[i] ][j] ); + } + } + bool useDefault = true; + for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ + if( i!=d_eval_term_index_order[n][i] ){ + useDefault = false; + break; + } + } + d_eval_uf_use_default[n] = useDefault; + Debug("fmf-index-order") << "Will consider the following index ordering for " << n << " : "; + for( int i=0; i<(int)d_eval_term_index_order[n].size(); i++ ){ + Debug("fmf-index-order") << d_eval_term_index_order[n][i] << " "; + } + Debug("fmf-index-order") << std::endl; +#else + d_eval_uf_use_default[n] = true; +#endif + } +} + + diff --git a/src/theory/quantifiers/rep_set_iterator.h b/src/theory/quantifiers/rep_set_iterator.h index f6312ae5c..a5ec266a9 100644 --- a/src/theory/quantifiers/rep_set_iterator.h +++ b/src/theory/quantifiers/rep_set_iterator.h @@ -1,120 +1,120 @@ -/********************* */
-/*! \file rep_set_iterator.h
- ** \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 rep_set_iterator class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__REP_SET_ITERATOR_H
-#define __CVC4__REP_SET_ITERATOR_H
-
-#include "theory/quantifiers_engine.h"
-#include "theory/quantifiers/first_order_model.h"
-
-namespace CVC4 {
-namespace theory {
-namespace quantifiers {
-
-/** this class iterates over a RepSet */
-class RepSetIterator {
-public:
- RepSetIterator( Node f, FirstOrderModel* model );
- ~RepSetIterator(){}
- //pointer to quantifier
- Node d_f;
- //pointer to model
- FirstOrderModel* d_model;
- //index we are considering
- std::vector< int > d_index;
- //domain we are considering
- std::vector< RepDomain > d_domain;
- //ordering for variables we are indexing over
- // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 },
- // then we consider instantiations in this order:
- // a/x a/y a/z
- // a/x b/y a/z
- // b/x a/y a/z
- // b/x b/y a/z
- // ...
- std::vector< int > d_index_order;
- //variables to index they are considered at
- // for example, if d_index_order = { 2, 0, 1 }
- // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 }
- std::map< int, int > d_var_order;
- //the instantiation constants of d_f
- std::vector< Node > d_ic;
- //the current terms we are considering
- std::vector< Node > d_terms;
-public:
- /** set index order */
- void setIndexOrder( std::vector< int >& indexOrder );
- /** set domain */
- void setDomain( std::vector< RepDomain >& domain );
- /** increment the iterator */
- void increment2( int counter );
- void increment();
- /** is the iterator finished? */
- bool isFinished();
- /** produce the match that this iterator represents */
- void getMatch( QuantifiersEngine* qe, InstMatch& m );
- /** get the i_th term we are considering */
- Node getTerm( int i );
- /** get the number of terms we are considering */
- int getNumTerms() { return d_f[0].getNumChildren(); }
- /** debug print */
- void debugPrint( const char* c );
- void debugPrintSmall( const char* c );
-};
-
-class RepSetEvaluator
-{
-private:
- FirstOrderModel* d_model;
- RepSetIterator* d_riter;
-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::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;
- int getMaxVariableNum( int n );
- void makeEvalUfIndexOrder( Node n );
-private:
- //default evaluate term function
- Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex );
- //temporary storing which literals have failed
- void clearEvalFailed( int index );
- std::map< Node, bool > d_eval_failed;
- std::map< int, std::vector< Node > > d_eval_failed_lits;
-public:
- RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri );
- virtual ~RepSetEvaluator(){}
- /** evaluate functions */
- int evaluate( Node n, int& depIndex );
- Node evaluateTerm( Node n, int& depIndex );
-public:
- //statistics
- int d_eval_formulas;
- int d_eval_uf_terms;
- int d_eval_lits;
- int d_eval_lits_unknown;
-};
-
-
-}
-}
-}
-
-#endif
+/********************* */ +/*! \file rep_set_iterator.h + ** \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 rep_set_iterator class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__REP_SET_ITERATOR_H +#define __CVC4__REP_SET_ITERATOR_H + +#include "theory/quantifiers_engine.h" +#include "theory/quantifiers/first_order_model.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +/** this class iterates over a RepSet */ +class RepSetIterator { +public: + RepSetIterator( Node f, FirstOrderModel* model ); + ~RepSetIterator(){} + //pointer to quantifier + Node d_f; + //pointer to model + FirstOrderModel* d_model; + //index we are considering + std::vector< int > d_index; + //domain we are considering + std::vector< RepDomain > d_domain; + //ordering for variables we are indexing over + // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 }, + // then we consider instantiations in this order: + // a/x a/y a/z + // a/x b/y a/z + // b/x a/y a/z + // b/x b/y a/z + // ... + std::vector< int > d_index_order; + //variables to index they are considered at + // for example, if d_index_order = { 2, 0, 1 } + // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 } + std::map< int, int > d_var_order; + //the instantiation constants of d_f + std::vector< Node > d_ic; + //the current terms we are considering + std::vector< Node > d_terms; +public: + /** set index order */ + void setIndexOrder( std::vector< int >& indexOrder ); + /** set domain */ + void setDomain( std::vector< RepDomain >& domain ); + /** increment the iterator */ + void increment2( int counter ); + void increment(); + /** is the iterator finished? */ + bool isFinished(); + /** produce the match that this iterator represents */ + void getMatch( QuantifiersEngine* qe, InstMatch& m ); + /** get the i_th term we are considering */ + Node getTerm( int i ); + /** get the number of terms we are considering */ + int getNumTerms() { return d_f[0].getNumChildren(); } + /** debug print */ + void debugPrint( const char* c ); + void debugPrintSmall( const char* c ); +}; + +class RepSetEvaluator +{ +private: + FirstOrderModel* d_model; + RepSetIterator* d_riter; +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::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; + int getMaxVariableNum( int n ); + void makeEvalUfIndexOrder( Node n ); +private: + //default evaluate term function + Node evaluateTermDefault( Node n, int& depIndex, std::vector< int >& childDepIndex ); + //temporary storing which literals have failed + void clearEvalFailed( int index ); + std::map< Node, bool > d_eval_failed; + std::map< int, std::vector< Node > > d_eval_failed_lits; +public: + RepSetEvaluator( FirstOrderModel* m, RepSetIterator* ri ); + virtual ~RepSetEvaluator(){} + /** evaluate functions */ + int evaluate( Node n, int& depIndex ); + Node evaluateTerm( Node n, int& depIndex ); +public: + //statistics + int d_eval_formulas; + int d_eval_uf_terms; + int d_eval_lits; + int d_eval_lits_unknown; +}; + + +} +} +} + +#endif diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 1ebba49b5..2af6992f7 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -1,156 +1,156 @@ -/**********************/
-/*! \file term_database.h
- ** \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 term database class
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__QUANTIFIERS_TERM_DATABASE_H
-#define __CVC4__QUANTIFIERS_TERM_DATABASE_H
-
-#include "theory/theory.h"
-
-#include <map>
-
-namespace CVC4 {
-namespace theory {
-
-class QuantifiersEngine;
-
-namespace quantifiers {
-
-class TermArgTrie {
-private:
- bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex );
-public:
- /** the data */
- std::map< Node, TermArgTrie > d_data;
-public:
- bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); }
-};/* class TermArgTrie */
-
-class TermDb {
- friend class ::CVC4::theory::QuantifiersEngine;
-private:
- /** reference to the quantifiers engine */
- QuantifiersEngine* d_quantEngine;
- /** calculated no match terms */
- bool d_matching_active;
- /** terms processed */
- std::hash_set< Node, NodeHashFunction > d_processed;
-public:
- TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){}
- ~TermDb(){}
- /** map from APPLY_UF operators to ground terms for that operator */
- std::map< Node, std::vector< Node > > d_op_map;
- /** map from APPLY_UF functions to trie */
- std::map< Node, TermArgTrie > d_func_map_trie;
- /** map from APPLY_UF predicates to trie */
- std::map< Node, TermArgTrie > d_pred_map_trie[2];
- /** map from type nodes to terms of that type */
- std::map< TypeNode, std::vector< Node > > d_type_map;
- /** add a term to the database */
- void addTerm( Node n, std::set< Node >& added, bool withinQuant = false );
- /** reset (calculate which terms are active) */
- void reset( Theory::Effort effort );
- /** set active */
- 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
- map from node "n" to a list of nodes "L", where each node n' in L
- has operator "op", and n'["index"] = n.
- for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... }
- */
- /* Todo replace int by size_t */
- std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction > , NodeHashFunction > d_parents;
- const std::vector<Node> & getParents(TNode n, TNode f, int arg);
-private:
- //map from types to model basis terms
- std::map< TypeNode, Node > d_model_basis_term;
- //map from ops to model basis terms
- std::map< Node, Node > d_model_basis_op_term;
- //map from instantiation terms to their model basis equivalent
- std::map< Node, Node > d_model_basis;
-public:
- //get model basis term
- Node getModelBasisTerm( TypeNode tn, int i = 0 );
- //get model basis term for op
- Node getModelBasisOpTerm( Node op );
- // compute model basis arg
- void computeModelBasisArgAttribute( Node n );
- //register instantiation terms with their corresponding model basis terms
- void registerModelBasis( Node n, Node gn );
- //get model basis
- Node getModelBasis( Node n ) { return d_model_basis[n]; }
-private:
- /** map from universal quantifiers to the list of variables */
- std::map< Node, std::vector< Node > > d_vars;
- /** map from universal quantifiers to the list of skolem constants */
- std::map< Node, std::vector< Node > > d_skolem_constants;
- /** map from universal quantifiers to their skolemized body */
- std::map< Node, Node > d_skolem_body;
- /** instantiation constants to universal quantifiers */
- std::map< Node, Node > d_inst_constants_map;
- /** map from universal quantifiers to their counterexample body */
- std::map< Node, Node > d_counterexample_body;
- /** free variable for instantiation constant type */
- std::map< TypeNode, Node > d_free_vars;
-private:
- /** make instantiation constants for */
- void makeInstantiationConstantsFor( Node f );
-public:
- /** map from universal quantifiers to the list of instantiation constants */
- std::map< Node, std::vector< Node > > d_inst_constants;
- /** set instantiation level attr */
- void setInstantiationLevelAttr( Node n, uint64_t level );
- /** set instantiation constant attr */
- void setInstantiationConstantAttr( Node n, Node f );
- /** get the i^th instantiation constant of f */
- Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; }
- /** get number of instantiation constants for f */
- int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); }
- /** get the ce body f[e/x] */
- Node getCounterexampleBody( Node f );
- /** get the skolemized body f[e/x] */
- Node getSkolemizedBody( Node f );
- /** returns node n with bound vars of f replaced by instantiation constants of f
- node n : is the futur pattern
- node f : is the quantifier containing which bind the variable
- return a pattern where the variable are replaced by variable for
- instantiation.
- */
- Node getSubstitutedNode( Node n, Node f );
- /** same as before but node f is just linked to the new pattern by the
- applied attribute
- vars the bind variable
- nvars the same variable but with an attribute
- */
- Node convertNodeToPattern( Node n, Node f,
- const std::vector<Node> & vars,
- const std::vector<Node> & nvars);
- /** get free variable for instantiation constant */
- Node getFreeVariableForInstConstant( Node n );
-};/* class TermDb */
-
-}
-}
-}
-
-#endif
+/**********************/ +/*! \file term_database.h + ** \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 term database class + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__QUANTIFIERS_TERM_DATABASE_H +#define __CVC4__QUANTIFIERS_TERM_DATABASE_H + +#include "theory/theory.h" + +#include <map> + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +namespace quantifiers { + +class TermArgTrie { +private: + bool addTerm2( QuantifiersEngine* qe, Node n, int argIndex ); +public: + /** the data */ + std::map< Node, TermArgTrie > d_data; +public: + bool addTerm( QuantifiersEngine* qe, Node n ) { return addTerm2( qe, n, 0 ); } +};/* class TermArgTrie */ + +class TermDb { + friend class ::CVC4::theory::QuantifiersEngine; +private: + /** reference to the quantifiers engine */ + QuantifiersEngine* d_quantEngine; + /** calculated no match terms */ + bool d_matching_active; + /** terms processed */ + std::hash_set< Node, NodeHashFunction > d_processed; +public: + TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ), d_matching_active( true ){} + ~TermDb(){} + /** map from APPLY_UF operators to ground terms for that operator */ + std::map< Node, std::vector< Node > > d_op_map; + /** map from APPLY_UF functions to trie */ + std::map< Node, TermArgTrie > d_func_map_trie; + /** map from APPLY_UF predicates to trie */ + std::map< Node, TermArgTrie > d_pred_map_trie[2]; + /** map from type nodes to terms of that type */ + std::map< TypeNode, std::vector< Node > > d_type_map; + /** add a term to the database */ + void addTerm( Node n, std::set< Node >& added, bool withinQuant = false ); + /** reset (calculate which terms are active) */ + void reset( Theory::Effort effort ); + /** set active */ + 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 + map from node "n" to a list of nodes "L", where each node n' in L + has operator "op", and n'["index"] = n. + for example, d_parents[n][f][1] = { f( t1, n ), f( t2, n ), ... } + */ + /* Todo replace int by size_t */ + std::hash_map< Node, std::hash_map< Node, std::hash_map< int, std::vector< Node > >, NodeHashFunction > , NodeHashFunction > d_parents; + const std::vector<Node> & getParents(TNode n, TNode f, int arg); +private: + //map from types to model basis terms + std::map< TypeNode, Node > d_model_basis_term; + //map from ops to model basis terms + std::map< Node, Node > d_model_basis_op_term; + //map from instantiation terms to their model basis equivalent + std::map< Node, Node > d_model_basis; +public: + //get model basis term + Node getModelBasisTerm( TypeNode tn, int i = 0 ); + //get model basis term for op + Node getModelBasisOpTerm( Node op ); + // compute model basis arg + void computeModelBasisArgAttribute( Node n ); + //register instantiation terms with their corresponding model basis terms + void registerModelBasis( Node n, Node gn ); + //get model basis + Node getModelBasis( Node n ) { return d_model_basis[n]; } +private: + /** map from universal quantifiers to the list of variables */ + std::map< Node, std::vector< Node > > d_vars; + /** map from universal quantifiers to the list of skolem constants */ + std::map< Node, std::vector< Node > > d_skolem_constants; + /** map from universal quantifiers to their skolemized body */ + std::map< Node, Node > d_skolem_body; + /** instantiation constants to universal quantifiers */ + std::map< Node, Node > d_inst_constants_map; + /** map from universal quantifiers to their counterexample body */ + std::map< Node, Node > d_counterexample_body; + /** free variable for instantiation constant type */ + std::map< TypeNode, Node > d_free_vars; +private: + /** make instantiation constants for */ + void makeInstantiationConstantsFor( Node f ); +public: + /** map from universal quantifiers to the list of instantiation constants */ + std::map< Node, std::vector< Node > > d_inst_constants; + /** set instantiation level attr */ + void setInstantiationLevelAttr( Node n, uint64_t level ); + /** set instantiation constant attr */ + void setInstantiationConstantAttr( Node n, Node f ); + /** get the i^th instantiation constant of f */ + Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; } + /** get number of instantiation constants for f */ + int getNumInstantiationConstants( Node f ) { return (int)d_inst_constants[f].size(); } + /** get the ce body f[e/x] */ + Node getCounterexampleBody( Node f ); + /** get the skolemized body f[e/x] */ + Node getSkolemizedBody( Node f ); + /** returns node n with bound vars of f replaced by instantiation constants of f + node n : is the futur pattern + node f : is the quantifier containing which bind the variable + return a pattern where the variable are replaced by variable for + instantiation. + */ + Node getSubstitutedNode( Node n, Node f ); + /** same as before but node f is just linked to the new pattern by the + applied attribute + vars the bind variable + nvars the same variable but with an attribute + */ + Node convertNodeToPattern( Node n, Node f, + const std::vector<Node> & vars, + const std::vector<Node> & nvars); + /** get free variable for instantiation constant */ + Node getFreeVariableForInstConstant( Node n ); +};/* class TermDb */ + +} +} +} + +#endif |