From a957f6f97f2e83d29f6c5d66f01e40f588ad95c5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 9 Oct 2012 21:59:58 +0000 Subject: [PATCH] fixed datatypes rewriter to detect clashes between non-datatype subfields. cleaned up model code, TheoryModel::getValue is now const. --- src/theory/datatypes/datatypes_rewriter.h | 7 ++ src/theory/model.cpp | 118 +++---------------- src/theory/model.h | 17 +-- src/theory/quantifiers/first_order_model.cpp | 14 --- src/theory/quantifiers/first_order_model.h | 2 - src/theory/quantifiers/model_builder.cpp | 27 ----- src/theory/quantifiers/model_builder.h | 5 - src/theory/rep_set.cpp | 18 +++ src/theory/rep_set.h | 6 +- src/util/util_model.h | 4 +- 10 files changed, 54 insertions(+), 164 deletions(-) diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index fae2c5bff..3ddf1d199 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -126,6 +126,13 @@ public: } } } + }else if( !n1.getType().isDatatype() ){ + //also check for clashes between non-datatypes + Node eq = NodeManager::currentNM()->mkNode( n1.getType().isBoolean() ? kind::IFF : kind::EQUAL, n1, n2 ); + eq = Rewriter::rewrite( eq ); + if( eq==NodeManager::currentNM()->mkConst(false) ){ + return true; + } } return false; } diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 3d918277f..adcf8dacf 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -48,26 +48,26 @@ void TheoryModel::reset(){ d_uf_models.clear(); } -Node TheoryModel::getValue( TNode n ){ +Node TheoryModel::getValue( TNode n ) const{ //apply substitutions Node nn = d_substitutions.apply( n ); //get value in model return getModelValue( nn ); } -Expr TheoryModel::getValue( Expr expr ){ +Expr TheoryModel::getValue( Expr expr ) const{ Node n = Node::fromExpr( expr ); Node ret = getValue( n ); return ret.toExpr(); } /** get cardinality for sort */ -Cardinality TheoryModel::getCardinality( Type t ){ +Cardinality TheoryModel::getCardinality( Type t ) const{ TypeNode tn = TypeNode::fromType( t ); //for now, we only handle cardinalities for uninterpreted sorts if( tn.isSort() ){ if( d_rep_set.hasType( tn ) ){ - return Cardinality( d_rep_set.d_type_reps[tn].size() ); + return Cardinality( d_rep_set.getNumRepresentatives( tn ) ); }else{ return Cardinality( CardinalityUnknown() ); } @@ -76,8 +76,7 @@ Cardinality TheoryModel::getCardinality( Type t ){ } } -Node TheoryModel::getModelValue( TNode n ) -{ +Node TheoryModel::getModelValue( TNode n ) const{ if( n.isConst() ) { return n; } @@ -85,9 +84,10 @@ Node TheoryModel::getModelValue( TNode n ) TypeNode t = n.getType(); if (t.isFunction() || t.isPredicate()) { if (d_enableFuncModels) { - if (d_uf_models.find(n) != d_uf_models.end()) { + std::map< Node, Node >::const_iterator it = d_uf_models.find(n); + if (it != d_uf_models.end()) { // Existing function - return d_uf_models[n]; + return it->second; } // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type vector argTypes = t.getArgTypes(); @@ -108,13 +108,15 @@ Node TheoryModel::getModelValue( TNode n ) std::vector children; if (n.getKind() == APPLY_UF) { Node op = n.getOperator(); - if (d_uf_models.find(op) == d_uf_models.end()) { + std::map< Node, Node >::const_iterator it = d_uf_models.find(op); + if (it == d_uf_models.end()) { // Unknown term - return first enumerated value for this type TypeEnumerator te(n.getType()); return *te; + }else{ + // Plug in uninterpreted function model + children.push_back(it->second); } - // Plug in uninterpreted function model - children.push_back(d_uf_models[op]); } else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { children.push_back(n.getOperator()); @@ -136,82 +138,11 @@ Node TheoryModel::getModelValue( TNode n ) } Node val = d_equalityEngine.getRepresentative(n); Assert(d_reps.find(val) != d_reps.end()); - val = d_reps[val]; - return val; -} - - -Node TheoryModel::getInterpretedValue( TNode n ){ - Trace("model") << "Get interpreted value of " << n << std::endl; - TypeNode type = n.getType(); - if( type.isFunction() || type.isPredicate() ){ - //for function models - if( d_enableFuncModels ){ - if( d_uf_models.find( n )!=d_uf_models.end() ){ - //pre-existing function model - Trace("model") << "Return function value." << std::endl; - return d_uf_models[n]; - }else{ - Trace("model") << "Return arbitrary function value." << std::endl; - //otherwise, choose the constant default value - uf::UfModelTree ufmt( n ); - Node default_v = getInterpretedValue( NodeManager::currentNM()->mkSkolem( "defaultValueQueryVar_$$", type.getRangeType(), - "a placeholder variable to query for a default value in model construction" ) ); - ufmt.setDefaultValue( this, default_v ); - return ufmt.getFunctionValue( "$x" ); - } - }else{ - return n; - } - } else{ - Trace("model-debug") << "check rep..." << std::endl; - Node ret; - //check if the representative is defined - n = d_equalityEngine.hasTerm( n ) ? d_equalityEngine.getRepresentative( n ) : n; - Trace("model-debug") << "rep is..." << n << std::endl; - if( d_reps.find( n )!=d_reps.end() ){ - Trace("model") << "Return value in equality engine."<< std::endl; - return d_reps[n]; - } - Trace("model-debug") << "check apply uf models..." << std::endl; - //if it is APPLY_UF, we must consult the corresponding function if it exists - if( n.getKind()==APPLY_UF ){ - Node op = n.getOperator(); - if( d_uf_models.find( op )!=d_uf_models.end() ){ - std::vector< Node > lam_children; - lam_children.push_back( d_uf_models[ op ] ); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - lam_children.push_back( n[i] ); - } - Node app_lam = NodeManager::currentNM()->mkNode( APPLY_UF, lam_children ); - ret = Rewriter::rewrite( app_lam ); - Trace("model") << "Consult UF model." << std::endl; - } - } - Trace("model-debug") << "check existing..." << std::endl; - if( ret.isNull() ){ - //second, try to choose an existing term as value - std::vector< Node > v_emp; - ret = getDomainValue( type, v_emp ); - if( !ret.isNull() ){ - Trace("model") << "Choose existing value." << std::endl; - } - } - Trace("model-debug") << "check new..." << std::endl; - if( ret.isNull() ){ - //otherwise, choose new value - ret = getNewDomainValue( type ); - if( !ret.isNull() ){ - Trace("model") << "Choose new value." << std::endl; - } - } - if( !ret.isNull() ){ - return ret; - }else{ - //otherwise, just return itself (this usually should not happen) - Trace("model") << "Return self." << std::endl; - return n; - } + std::map< Node, Node >::const_iterator it = d_reps.find( val ); + if( it!=d_reps.end() ){ + return it->second; + }else{ + return Node::null(); } } @@ -710,16 +641,3 @@ void TheoryEngineModelBuilder::processBuildModel(TheoryModel* m, bool fullModel) } } } - - -Node TheoryEngineModelBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){ - //try to get a new domain value - Node rep = m->getNewDomainValue( eqc.getType() ); - if( !rep.isNull() ){ - return rep; - }else{ - //if we can't get new domain value, just return eqc itself (this typically should not happen) - //FIXME: Assertion failure here? - return eqc; - } -} diff --git a/src/theory/model.h b/src/theory/model.h index 3c6d8e116..8498b55e1 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -55,18 +55,13 @@ protected: /** * Get model value function. This function is called by getValue */ - Node getModelValue( TNode n ); - /** get interpreted value - * This function is called when the value of the node cannot be determined by the theory rewriter - * This should function should return a representative in d_reps - */ - virtual Node getInterpretedValue( TNode n ); + Node getModelValue( TNode n ) const; public: /** * Get value function. This should be called only after a ModelBuilder has called buildModel(...) * on this model. */ - Node getValue( TNode n ); + Node getValue( TNode n ) const; /** get existing domain value, with possible exclusions * This function returns a term in d_rep_set.d_type_reps[tn] but not in exclude @@ -113,9 +108,9 @@ public: bool areDisequal( Node a, Node b ); public: /** get value function for Exprs. */ - Expr getValue( Expr expr ); + Expr getValue( Expr expr ) const; /** get cardinality for sort */ - Cardinality getCardinality( Type t ); + Cardinality getCardinality( Type t ) const; public: /** print representative debug function */ void printRepresentativeDebug( const char* c, Node r ); @@ -238,7 +233,7 @@ private: return *(*it).second; } -}; +}; /** TheoryEngineModelBuilder class * This model builder will consult all theories in a theory engine for @@ -254,8 +249,6 @@ protected: /** process build model */ virtual void processBuildModel(TheoryModel* m, bool fullModel); - /** choose representative for unconstrained equivalence class */ - virtual Node chooseRepresentative(TheoryModel* m, Node eqc, bool fullModel); /** normalize representative */ Node normalize(TheoryModel* m, TNode r, std::map& constantReps, bool evalOnly); public: diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 44eb00730..dd36f9917 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -93,20 +93,6 @@ void FirstOrderModel::initializeModelForTerm( Node n ){ } } -Node FirstOrderModel::getInterpretedValue( TNode n ){ - //Trace("fo-model") << "get interpreted value " << n << std::endl; - /*TypeNode type = n.getType(); - if( type.isFunction() || type.isPredicate() ){ - if( d_uf_model_tree.find( n )!=d_uf_model_tree.end() ){ - if( d_uf_models.find( n )==d_uf_models.end() ){ - d_uf_models[n] = d_uf_model_tree[n].getFunctionValue( "$x" ); - } - } - }*/ - return TheoryModel::getInterpretedValue( n ); -} - - //for evaluation of quantifier bodies void FirstOrderModel::resetEvaluate(){ diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index 52688a816..05a7a83c1 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -80,8 +80,6 @@ public: virtual ~FirstOrderModel(){} // reset the model void reset(); - /** get interpreted value */ - Node getInterpretedValue( TNode n ); public: // initialize the model void initialize( bool considerAxioms = true ); diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 805d27008..81efa4289 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -42,33 +42,6 @@ d_qe( qe ), d_curr_model( c, NULL ){ d_considerAxioms = true; } -Node ModelEngineBuilder::chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ){ - if( fullModel ){ - return TheoryEngineModelBuilder::chooseRepresentative( m, eqc, fullModel ); - }else{ - Assert( m->d_equalityEngine.hasTerm( eqc ) ); - Assert( m->d_equalityEngine.getRepresentative( eqc )==eqc ); - //avoid bad representatives - if( isBadRepresentative( eqc ) ){ - eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &m->d_equalityEngine ); - while( !eqc_i.isFinished() ){ - if( !isBadRepresentative( *eqc_i ) ){ - return *eqc_i; - } - ++eqc_i; - } - //otherwise, make new value? - //Message() << "Warning: Bad rep " << eqc << std::endl; - } - return eqc; - } -} - -bool ModelEngineBuilder::isBadRepresentative( Node n ){ - //avoid interpreted symbols - return n.getKind()==SELECT || n.getKind()==APPLY_SELECTOR; -} - void ModelEngineBuilder::processBuildModel( TheoryModel* m, bool fullModel ) { FirstOrderModel* fm = (FirstOrderModel*)m; if( fullModel ){ diff --git a/src/theory/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h index 1366a7650..d838064de 100644 --- a/src/theory/quantifiers/model_builder.h +++ b/src/theory/quantifiers/model_builder.h @@ -45,13 +45,8 @@ protected: std::map< Node, uf::UfModelPreferenceData > d_uf_prefs; //built model uf std::map< Node, bool > d_uf_model_constructed; -protected: /** process build model */ void processBuildModel( TheoryModel* m, bool fullModel ); - /** choose representative for unconstrained equivalence class */ - Node chooseRepresentative( TheoryModel* m, Node eqc, bool fullModel ); - /** bad representative */ - bool isBadRepresentative( Node n ); protected: //analyze model void analyzeModel( FirstOrderModel* fm ); diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index 4a5bb2247..b7d2da713 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -29,12 +29,30 @@ void RepSet::clear(){ d_tmap.clear(); } +int RepSet::getNumRepresentatives( TypeNode tn ) const{ + std::map< TypeNode, std::vector< Node > >::const_iterator it = d_type_reps.find( tn ); + if( it!=d_type_reps.end() ){ + return (int)it->second.size(); + }else{ + return 0; + } +} + void RepSet::add( Node n ){ TypeNode t = n.getType(); d_tmap[ n ] = (int)d_type_reps[t].size(); d_type_reps[t].push_back( n ); } +int RepSet::getIndexFor( Node n ) const { + std::map< Node, int >::const_iterator it = d_tmap.find( n ); + if( it!=d_tmap.end() ){ + return it->second; + }else{ + return -1; + } +} + void RepSet::complete( TypeNode t ){ if( d_type_complete.find( t )==d_type_complete.end() ){ d_type_complete[t] = true; diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index 3427502b1..034ecea46 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -36,11 +36,13 @@ public: /** clear the set */ void clear(); /** has type */ - bool hasType( TypeNode tn ) { return d_type_reps.find( tn )!=d_type_reps.end(); } + bool hasType( TypeNode tn ) const { return d_type_reps.find( tn )!=d_type_reps.end(); } + /** get cardinality for type */ + int getNumRepresentatives( TypeNode tn ) const; /** add representative for type */ void add( Node n ); /** returns index in d_type_reps for node n */ - int getIndexFor( Node n ) { return d_tmap.find( n )!=d_tmap.end() ? d_tmap[n] : -1; } + int getIndexFor( Node n ) const; /** complete all values */ void complete( TypeNode t ); /** debug print */ diff --git a/src/util/util_model.h b/src/util/util_model.h index bb40c9ba4..e67485ce7 100644 --- a/src/util/util_model.h +++ b/src/util/util_model.h @@ -53,9 +53,9 @@ public: public: /** get value for expression */ - virtual Expr getValue(Expr expr) = 0; + virtual Expr getValue(Expr expr) const = 0; /** get cardinality for sort */ - virtual Cardinality getCardinality(Type t) = 0; + virtual Cardinality getCardinality(Type t) const = 0; };/* class Model */ class ModelBuilder { -- 2.30.2