diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-09 21:59:58 +0000 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-10-09 21:59:58 +0000 |
commit | a957f6f97f2e83d29f6c5d66f01e40f588ad95c5 (patch) | |
tree | 8b95b65fad71aab9b0baee4b6bfc976b731f9502 /src/theory/quantifiers | |
parent | dba60e91f02ae9ca3c3126c76d79a09c95f95a45 (diff) |
fixed datatypes rewriter to detect clashes between non-datatype subfields. cleaned up model code, TheoryModel::getValue is now const.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 14 | ||||
-rw-r--r-- | src/theory/quantifiers/first_order_model.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 27 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.h | 5 |
4 files changed, 0 insertions, 48 deletions
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 ); |