}
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()))
{
return n.getAttribute(ModelBasisArgAttribute());
}
+Node FirstOrderModelIG::UfModelTreeGenerator::getIntersection(TheoryModel* m,
+ Node n1,
+ Node n2,
+ bool& isGround)
+{
+ isGround = true;
+ std::vector<Node> 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<Node, Node>::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) {
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<Node, Node> d_set_values[2][2];
+ /** stores the set of non-ground keys in the above maps */
+ std::vector<Node> 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<Node, uf::UfModelTree> d_uf_model_tree;
+ /** model generators for each UF operator */
+ std::map<Node, UfModelTreeGenerator> d_uf_model_gen;
+
+ private:
//map from terms to the models used to calculate their value
std::map< Node, bool > d_eval_uf_use_default;
std::map< Node, uf::UfModelTree > d_eval_uf_model;
}
}
+void 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<double>(d_value_pro_con[0][v].size()))
+ / (1.0 + static_cast<double>(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),
//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; i<itut->second.size(); i++ ){
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() ){
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 ){
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{
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);
}
}
}
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;
//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;
}
unsigned getNumTriedLemmas() { return d_triedLemmas; }
};
-
-
-
-
class TermArgBasisTrie {
public:
/** the data */
typedef context::CDHashMap<Node, bool, NodeHashFunction> 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<Node> 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<Node, std::vector<Node> > 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<Node, UfModelPreferenceData> d_uf_prefs;
//built model uf
std::map< Node, bool > d_uf_model_constructed;
//whether inst gen was done
public:
QModelBuilderDefault( context::Context* c, QuantifiersEngine* qe ) : QModelBuilderIG( c, qe ){}
- //options
- bool optReconsiderFuncConstants() { return true; }
//has inst gen
bool hasInstGen(Node f) override
{
#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;
}
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<defSize; i++ ){
- //for soundness, 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 UfModelTreeGenerator::makeModel( TheoryModel* m, UfModelTree& tree ){
- for( int j=0; j<2; j++ ){
- for( int k=0; k<2; k++ ){
- for( std::map< Node, Node >::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; i<d_values.size(); i++ ){
- Node v = d_values[i];
- double score = ( 1.0 + (double)d_value_pro_con[0][v].size() )/( 1.0 + (double)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;
- }
- }
-#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;
-}
namespace theory {
namespace uf {
-// TODO (#1302) : some of these classes should be moved to
-// src/theory/quantifiers/
class UfModelTreeNode
{
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 );
-};
-
-
}
}
}
projects / cvc5.git / commitdiff