From 2947a2f2af0e9a40c3be9ba2e84f634c36e0dd0f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 8 Aug 2018 13:09:19 -0500 Subject: Move uf model code from uf to quantifiers (#2095) --- src/theory/quantifiers/first_order_model.cpp | 115 ++++++++++++++++++++- src/theory/quantifiers/first_order_model.h | 57 +++++++++-- src/theory/quantifiers/fmf/model_builder.cpp | 129 ++++++++++++++--------- src/theory/quantifiers/fmf/model_builder.h | 37 +++++-- src/theory/uf/theory_uf_model.cpp | 148 --------------------------- src/theory/uf/theory_uf_model.h | 46 --------- 6 files changed, 273 insertions(+), 259 deletions(-) (limited to 'src/theory') diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 9d83c589f..b3dc9965b 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -398,7 +398,7 @@ void FirstOrderModel::computeModelBasisArgAttribute(Node n) } uint64_t val = 0; // determine if it has model basis attribute - for (unsigned j = 0; j < n.getNumChildren(); j++) + for (unsigned j = 0, nchild = n.getNumChildren(); j < nchild; j++) { if (n[j].getAttribute(ModelBasisAttribute())) { @@ -416,6 +416,119 @@ unsigned FirstOrderModel::getModelBasisArg(Node n) return n.getAttribute(ModelBasisArgAttribute()); } +Node FirstOrderModelIG::UfModelTreeGenerator::getIntersection(TheoryModel* m, + Node n1, + Node n2, + bool& isGround) +{ + isGround = true; + std::vector children; + children.push_back(n1.getOperator()); + for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++) + { + if (n1[i] == n2[i]) + { + if (n1[i].getAttribute(ModelBasisAttribute())) + { + isGround = false; + } + children.push_back(n1[i]); + } + else if (n1[i].getAttribute(ModelBasisAttribute())) + { + children.push_back(n2[i]); + } + else if (n2[i].getAttribute(ModelBasisAttribute())) + { + children.push_back(n1[i]); + } + else if (m->areEqual(n1[i], n2[i])) + { + children.push_back(n1[i]); + } + else + { + return Node::null(); + } + } + return NodeManager::currentNM()->mkNode(APPLY_UF, children); +} + +void FirstOrderModelIG::UfModelTreeGenerator::setValue( + TheoryModel* m, Node n, Node v, bool ground, bool isReq) +{ + Assert(!n.isNull()); + Assert(!v.isNull()); + d_set_values[isReq ? 1 : 0][ground ? 1 : 0][n] = v; + if (!ground) + { + for (unsigned i = 0, defSize = d_defaults.size(); i < defSize; i++) + { + // for correctness, to allow variable order-independent function + // interpretations, we must ensure that the intersection of all default + // terms is also defined. + // for example, if we have that f( e, a ) = ..., and f( b, e ) = ..., + // then we must define f( b, a ). + bool isGround; + Node ni = getIntersection(m, n, d_defaults[i], isGround); + if (!ni.isNull()) + { + // if the intersection exists, and is not already defined + if (d_set_values[0][isGround ? 1 : 0].find(ni) + == d_set_values[0][isGround ? 1 : 0].end() + && d_set_values[1][isGround ? 1 : 0].find(ni) + == d_set_values[1][isGround ? 1 : 0].end()) + { + // use the current value + setValue(m, ni, v, isGround, false); + } + } + } + d_defaults.push_back(n); + } + if (isReq + && d_set_values[0][ground ? 1 : 0].find(n) + != d_set_values[0][ground ? 1 : 0].end()) + { + d_set_values[0][ground ? 1 : 0].erase(n); + } +} + +void FirstOrderModelIG::UfModelTreeGenerator::makeModel(TheoryModel* m, + uf::UfModelTree& tree) +{ + for (int j = 0; j < 2; j++) + { + for (int k = 0; k < 2; k++) + { + for (std::map::iterator it = d_set_values[j][k].begin(); + it != d_set_values[j][k].end(); + ++it) + { + tree.setValue(m, it->first, it->second, k == 1); + } + } + } + if (!d_default_value.isNull()) + { + tree.setDefaultValue(m, d_default_value); + } + tree.simplify(); +} + +void FirstOrderModelIG::UfModelTreeGenerator::clear() +{ + d_default_value = Node::null(); + for (int j = 0; j < 2; j++) + { + for (int k = 0; k < 2; k++) + { + d_set_values[j][k].clear(); + } + } + d_defaults.clear(); +} + FirstOrderModelIG::FirstOrderModelIG(QuantifiersEngine * qe, context::Context* c, std::string name) : FirstOrderModel(qe, c,name) { diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index c33e2c6b7..059250f8d 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -193,15 +193,58 @@ class FirstOrderModel : public TheoryModel void computeModelBasisArgAttribute(Node n); };/* class FirstOrderModel */ - class FirstOrderModelIG : public FirstOrderModel { -public: //for Theory UF: - //models for each UF operator - std::map< Node, uf::UfModelTree > d_uf_model_tree; - //model generators - std::map< Node, uf::UfModelTreeGenerator > d_uf_model_gen; -private: + public: // for Theory UF: + /** class for generating models for uninterpreted functions + * + * This implements the model construction from page 6 of Reynolds et al, + * "Quantifier Instantiation Techniques for Finite Model Finding in SMT", + * CADE 2013. + */ + class UfModelTreeGenerator + { + public: + UfModelTreeGenerator() {} + ~UfModelTreeGenerator() {} + /** set default value */ + void setDefaultValue(Node v) { d_default_value = v; } + /** set value */ + void setValue( + TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true); + /** make model */ + void makeModel(TheoryModel* m, uf::UfModelTree& tree); + /** reset */ + void clear(); + + public: + /** the overall default value */ + Node d_default_value; + /** + * Stores (required, ground) values in key, value pairs of the form + * ( P( a, b ), c ), which indicates P( a, b ) has value c in the model. + * The "non-ground" values indicate that the key has a "model-basis" + * variable, for example, ( P( _, b ), c ) indicates that P( x, b ) has the + * value b for any value of x. + */ + std::map d_set_values[2][2]; + /** stores the set of non-ground keys in the above maps */ + std::vector d_defaults; + /** + * Returns the term corresponding to the intersection of n1 and n2, if it + * exists, for example, for P( _, a ) and P( b, _ ), this method returns + * P( b, a ), where _ is the "model basis" variable. We take into account + * equality between arguments, so if a=b, then the intersection of P( a, a ) + * and P( b, _ ) is P( a, a ). + */ + Node getIntersection(TheoryModel* m, Node n1, Node n2, bool& isGround); + }; + /** models for each UF operator */ + std::map d_uf_model_tree; + /** model generators for each UF operator */ + std::map d_uf_model_gen; + + private: //map from terms to the models used to calculate their value std::map< Node, bool > d_eval_uf_use_default; std::map< Node, uf::UfModelTree > d_eval_uf_model; diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index cc542f0c3..fcc9cd060 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -166,9 +166,81 @@ bool TermArgBasisTrie::addTerm(FirstOrderModel* fm, Node n, unsigned argIndex) } } +void QModelBuilderIG::UfModelPreferenceData::setValuePreference(Node q, + Node r, + bool isPro) +{ + if (std::find(d_values.begin(), d_values.end(), r) == d_values.end()) + { + d_values.push_back(r); + } + int index = isPro ? 0 : 1; + if (std::find( + d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), q) + == d_value_pro_con[index][r].end()) + { + d_value_pro_con[index][r].push_back(q); + } +} + +Node QModelBuilderIG::UfModelPreferenceData::getBestDefaultValue( + Node defaultTerm, TheoryModel* m) +{ + Node defaultVal; + double maxScore = -1; + for (size_t i = 0, size = d_values.size(); i < size; i++) + { + Node v = d_values[i]; + double score = (1.0 + static_cast(d_value_pro_con[0][v].size())) + / (1.0 + static_cast(d_value_pro_con[1][v].size())); + Debug("fmf-model-cons-debug") << " - score( "; + m->printRepresentativeDebug("fmf-model-cons-debug", v); + Debug("fmf-model-cons-debug") << " ) = " << score << std::endl; + if (score > maxScore) + { + defaultVal = v; + maxScore = score; + } + } + if (maxScore < 1.0) + { + // consider finding another value, if possible + Debug("fmf-model-cons-debug") + << "Poor choice for default value, score = " << maxScore << std::endl; + TypeNode tn = defaultTerm.getType(); + Node newDefaultVal = m->getRepSet()->getDomainValue(tn, d_values); + if (!newDefaultVal.isNull()) + { + defaultVal = newDefaultVal; + Debug("fmf-model-cons-debug") << "-> Change default value to "; + m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal); + Debug("fmf-model-cons-debug") << std::endl; + } + else + { + Debug("fmf-model-cons-debug") + << "-> Could not find arbitrary element of type " + << tn[tn.getNumChildren() - 1] << std::endl; + Debug("fmf-model-cons-debug") << " Excluding: " << d_values; + Debug("fmf-model-cons-debug") << std::endl; + } + } + // get the default term (this term must be defined non-ground in model) + Debug("fmf-model-cons-debug") << " Choose "; + m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal); + Debug("fmf-model-cons-debug") + << " as default value (" << defaultTerm << ")" << std::endl; + Debug("fmf-model-cons-debug") + << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() + << std::endl; + Debug("fmf-model-cons-debug") + << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() + << std::endl; + return defaultVal; +} + QModelBuilderIG::QModelBuilderIG(context::Context* c, QuantifiersEngine* qe) : QModelBuilder(c, qe), - d_basisNoMatch(c), d_didInstGen(false), d_numQuantSat(0), d_numQuantInstGen(0), @@ -347,7 +419,6 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ //determine if any functions are constant for( std::map< Node, uf::UfModelTree >::iterator it = fmig->d_uf_model_tree.begin(); it != fmig->d_uf_model_tree.end(); ++it ){ Node op = it->first; - TermArgBasisTrie tabt; std::map< Node, std::vector< Node > >::iterator itut = fmig->d_uf_terms.find( op ); if( itut!=fmig->d_uf_terms.end() ){ for( size_t i=0; isecond.size(); i++ ){ @@ -360,14 +431,6 @@ void QModelBuilderIG::analyzeModel( FirstOrderModel* fm ){ d_uf_prefs[op].d_const_val = Node::null(); break; } - //for calculating terms that we don't need to consider - //if( d_qe->getTermDatabase()->isTermActive( n ) || n.getAttribute(ModelBasisArgAttribute())!=0 ){ - if( d_basisNoMatch.find( n )==d_basisNoMatch.end() ){ - //need to consider if it is not congruent modulo model basis - if( !tabt.addTerm( fmig, n ) ){ - d_basisNoMatch[n] = true; - } - } } } if( !d_uf_prefs[op].d_const_val.isNull() ){ @@ -604,15 +667,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ d_qe->getModel()->setQuantifierActive( f, false ); //check if choosing this literal would add any additional constraints to default definitions selectLitConstraints = false; - for( int j=0; j<(int)uf_terms.size(); j++ ){ - Node op = uf_terms[j].getOperator(); - if( d_uf_prefs[op].d_reconsiderModel ){ - selectLitConstraints = true; - } - } - if( !selectLitConstraints ){ - selectLit = true; - } + selectLit = true; } //also check if it is naturally a better literal if( !selectLit ){ @@ -662,7 +717,6 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ Debug("fmf-model-prefs") << " * Constant SAT due to definition of ops: "; for( int i=0; i<(int)selectionLitTerms.size(); i++ ){ Debug("fmf-model-prefs") << selectionLitTerms[i] << " "; - d_uf_prefs[ selectionLitTerms[i].getOperator() ].d_reconsiderModel = false; } Debug("fmf-model-prefs") << std::endl; }else{ @@ -671,7 +725,7 @@ void QModelBuilderDefault::analyzeQuantifier( FirstOrderModel* fm, Node f ){ for( int j=0; j<(int)pro_con[k].size(); j++ ){ Node op = pro_con[k][j].getOperator(); Node r = fmig->getRepresentative( pro_con[k][j] ); - d_uf_prefs[op].setValuePreference( f, pro_con[k][j], r, k==0 ); + d_uf_prefs[op].setValuePreference(f, r, k == 0); } } } @@ -731,21 +785,6 @@ int QModelBuilderDefault::doInstGen( FirstOrderModel* fm, Node f ){ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ FirstOrderModelIG* fmig = fm->asFirstOrderModelIG(); - if( optReconsiderFuncConstants() ){ - //reconsider constant functions that weren't necessary - if( d_uf_model_constructed[op] ){ - 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; - fmig->d_uf_model_tree[op].clear(); - fmig->d_uf_model_gen[op].clear(); - d_uf_model_constructed[op] = false; - } - } - } - } if( !d_uf_model_constructed[op] ){ //construct the model for the uninterpretted function/predicate bool setDefaultVal = true; @@ -765,19 +804,13 @@ void QModelBuilderDefault::constructModelUf( FirstOrderModel* fm, Node op ){ //set n = v in the model tree //set it as ground value fmig->d_uf_model_gen[op].setValue( fm, n, v ); - if( fmig->d_uf_model_gen[op].optUsePartialDefaults() ){ - //also set as default value if necessary - if( n.hasAttribute(ModelBasisArgAttribute()) && n.getAttribute(ModelBasisArgAttribute())!=0 ){ - Trace("fmf-model-cons") << " Set as default." << std::endl; - fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); - if( n==defaultTerm ){ - //incidentally already set, we will not need to find a default value - setDefaultVal = false; - } - } - }else{ + // also set as default value if necessary + if (n.hasAttribute(ModelBasisArgAttribute()) + && n.getAttribute(ModelBasisArgAttribute()) != 0) + { + Trace("fmf-model-cons") << " Set as default." << std::endl; + fmig->d_uf_model_gen[op].setValue(fm, n, v, false); if( n==defaultTerm ){ - fmig->d_uf_model_gen[op].setValue( fm, n, v, false ); //incidentally already set, we will not need to find a default value setDefaultVal = false; } diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index b08537e9f..353883a20 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -56,10 +56,6 @@ public: unsigned getNumTriedLemmas() { return d_triedLemmas; } }; - - - - class TermArgBasisTrie { public: /** the data */ @@ -80,9 +76,34 @@ class QModelBuilderIG : public QModelBuilder typedef context::CDHashMap BoolMap; protected: - BoolMap d_basisNoMatch; - //map from operators to model preference data - std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; + /** + * This class stores temporary information useful to model engine for + * constructing models for uninterpreted functions. + */ + class UfModelPreferenceData + { + public: + UfModelPreferenceData() {} + virtual ~UfModelPreferenceData() {} + /** any constant value of the type */ + Node d_const_val; + /** list of possible default values */ + std::vector d_values; + /** + * Map from values to the set of quantified formulas that are (pro, con) + * that value. A quantified formula may be "pro" a particular default + * value of an uninterpreted function if that value is likely to satisfy + * many points in its domain. For example, forall x. P( f( x ) ) may be + * "pro" the default value true for P. + */ + std::map > d_value_pro_con[2]; + /** set that quantified formula q is pro/con the default value of r */ + void setValuePreference(Node q, Node r, bool isPro); + /** get best default value */ + Node getBestDefaultValue(Node defaultTerm, TheoryModel* m); + }; + /** map from operators to model preference data */ + std::map d_uf_prefs; //built model uf std::map< Node, bool > d_uf_model_constructed; //whether inst gen was done @@ -189,8 +210,6 @@ class QModelBuilderDefault : public QModelBuilderIG public: QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){} - //options - bool optReconsiderFuncConstants() { return true; } //has inst gen bool hasInstGen(Node f) override { diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp index 8c994217d..3d656cf24 100644 --- a/src/theory/uf/theory_uf_model.cpp +++ b/src/theory/uf/theory_uf_model.cpp @@ -24,10 +24,6 @@ #include "theory/uf/equality_engine.h" #include "theory/uf/theory_uf.h" - -#define RECONSIDER_FUNC_DEFAULT_VALUE -#define USE_PARTIAL_DEFAULT_VALUES - using namespace std; using namespace CVC4; using namespace CVC4::kind; @@ -317,147 +313,3 @@ Node UfModelTree::getFunctionValue( const char* argPrefix, bool simplify ){ } return getFunctionValue( vars, simplify ); } - -Node UfModelTreeGenerator::getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ){ - //Notice() << "Get intersection " << n1 << " " << n2 << std::endl; - isGround = true; - std::vector< Node > children; - children.push_back( n1.getOperator() ); - for( int i=0; i<(int)n1.getNumChildren(); i++ ){ - if( n1[i]==n2[i] ){ - if( n1[i].getAttribute(ModelBasisAttribute()) ){ - isGround = false; - } - children.push_back( n1[i] ); - }else if( n1[i].getAttribute(ModelBasisAttribute()) ){ - children.push_back( n2[i] ); - }else if( n2[i].getAttribute(ModelBasisAttribute()) ){ - children.push_back( n1[i] ); - }else if( m->areEqual( n1[i], n2[i] ) ){ - children.push_back( n1[i] ); - }else{ - return Node::null(); - } - } - return NodeManager::currentNM()->mkNode( APPLY_UF, children ); -} - -void UfModelTreeGenerator::setValue( TheoryModel* m, Node n, Node v, bool ground, bool isReq ){ - Assert( !n.isNull() ); - Assert( !v.isNull() ); - d_set_values[ isReq ? 1 : 0 ][ ground ? 1 : 0 ][n] = v; - if( optUsePartialDefaults() ){ - if( !ground ){ - int defSize = (int)d_defaults.size(); - for( int i=0; i::iterator it = d_set_values[j][k].begin(); it != d_set_values[j][k].end(); ++it ){ - tree.setValue( m, it->first, it->second, k==1 ); - } - } - } - if( !d_default_value.isNull() ){ - tree.setDefaultValue( m, d_default_value ); - } - tree.simplify(); -} - -bool UfModelTreeGenerator::optUsePartialDefaults(){ -#ifdef USE_PARTIAL_DEFAULT_VALUES - return true; -#else - return false; -#endif -} - -void UfModelTreeGenerator::clear(){ - d_default_value = Node::null(); - for( int j=0; j<2; j++ ){ - for( int k=0; k<2; k++ ){ - d_set_values[j][k].clear(); - } - } - d_defaults.clear(); -} - - -void UfModelPreferenceData::setValuePreference( Node f, Node n, Node r, bool isPro ){ - if( std::find( d_values.begin(), d_values.end(), r )==d_values.end() ){ - d_values.push_back( r ); - } - int index = isPro ? 0 : 1; - if( std::find( d_value_pro_con[index][r].begin(), d_value_pro_con[index][r].end(), f )==d_value_pro_con[index][r].end() ){ - d_value_pro_con[index][r].push_back( f ); - } - d_term_pro_con[index][n].push_back( f ); -} - -Node UfModelPreferenceData::getBestDefaultValue( Node defaultTerm, TheoryModel* m ){ - Node defaultVal; - double maxScore = -1; - for( size_t i=0; iprintRepresentativeDebug( "fmf-model-cons-debug", v ); - Debug("fmf-model-cons-debug") << " ) = " << score << std::endl; - if( score>maxScore ){ - defaultVal = v; - maxScore = score; - } - } -#ifdef RECONSIDER_FUNC_DEFAULT_VALUE - if( maxScore<1.0 ){ - //consider finding another value, if possible - Debug("fmf-model-cons-debug") << "Poor choice for default value, score = " << maxScore << std::endl; - TypeNode tn = defaultTerm.getType(); - Node newDefaultVal = m->getRepSet()->getDomainValue(tn, d_values); - if( !newDefaultVal.isNull() ){ - defaultVal = newDefaultVal; - Debug("fmf-model-cons-debug") << "-> Change default value to "; - m->printRepresentativeDebug( "fmf-model-cons-debug", defaultVal ); - Debug("fmf-model-cons-debug") << std::endl; - }else{ - Debug("fmf-model-cons-debug") << "-> Could not find arbitrary element of type " << tn[(int)tn.getNumChildren()-1] << std::endl; - Debug("fmf-model-cons-debug") << " Excluding: "; - for( int i=0; i<(int)d_values.size(); i++ ){ - Debug("fmf-model-cons-debug") << d_values[i] << " "; - } - Debug("fmf-model-cons-debug") << std::endl; - } - } -#endif - //get the default term (this term must be defined non-ground in model) - Debug("fmf-model-cons-debug") << " Choose "; - m->printRepresentativeDebug("fmf-model-cons-debug", defaultVal ); - Debug("fmf-model-cons-debug") << " as default value (" << defaultTerm << ")" << std::endl; - Debug("fmf-model-cons-debug") << " # quantifiers pro = " << d_value_pro_con[0][defaultVal].size() << std::endl; - Debug("fmf-model-cons-debug") << " # quantifiers con = " << d_value_pro_con[1][defaultVal].size() << std::endl; - return defaultVal; -} diff --git a/src/theory/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h index 0fc0421b6..201faccee 100644 --- a/src/theory/uf/theory_uf_model.h +++ b/src/theory/uf/theory_uf_model.h @@ -23,8 +23,6 @@ namespace CVC4 { namespace theory { namespace uf { -// TODO (#1302) : some of these classes should be moved to -// src/theory/quantifiers/ class UfModelTreeNode { public: @@ -148,50 +146,6 @@ public: } }; - -class UfModelTreeGenerator -{ -public: - //store for set values - Node d_default_value; - std::map< Node, Node > d_set_values[2][2]; - // defaults - std::vector< Node > d_defaults; - Node getIntersection( TheoryModel* m, Node n1, Node n2, bool& isGround ); -public: - UfModelTreeGenerator(){} - ~UfModelTreeGenerator(){} - /** set default value */ - void setDefaultValue( Node v ) { d_default_value = v; } - /** set value */ - void setValue( TheoryModel* m, Node n, Node v, bool ground = true, bool isReq = true ); - /** make model */ - void makeModel( TheoryModel* m, UfModelTree& tree ); - /** uses partial default values */ - bool optUsePartialDefaults(); - /** reset */ - void clear(); -}; - -//this class stores temporary information useful to model engine for constructing model -class UfModelPreferenceData -{ -public: - UfModelPreferenceData() : d_reconsiderModel( false ){} - virtual ~UfModelPreferenceData(){} - Node d_const_val; - // preferences for default values - std::vector< Node > d_values; - std::map< Node, std::vector< Node > > d_value_pro_con[2]; - std::map< Node, std::vector< Node > > d_term_pro_con[2]; - bool d_reconsiderModel; - /** set value preference */ - void setValuePreference( Node f, Node n, Node r, bool isPro ); - /** get best default value */ - Node getBestDefaultValue( Node defaultTerm, TheoryModel* m ); -}; - - } } } -- cgit v1.2.3