diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-03 20:39:25 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-03 20:39:25 +0000 |
commit | 3daaecd22fe5f6147cb08e5a4e08177b33a2daa2 (patch) | |
tree | 46cb65c3673a5678a7779ff970aea9460233f1f1 /src/theory/quantifiers | |
parent | e26a44d5f98a9953dffeb07b29a21e7efd501684 (diff) |
fix uses of getMetaKind() from outside the expr package. (they now use isConst() and isVar() as appropriate)
also some base infrastructure for the new ::isConst().
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/first_order_model.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/rep_set_iterator.cpp | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 5d7317cbc..fd616948c 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -168,7 +168,7 @@ void FirstOrderModel::toStream(std::ostream& out){ 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 ) ){ + if( !(*eqc_i).isConst() && !hasInterpretedValue( *eqc_i ) ){ out << "(" << (*eqc_i) << " " << rep << ")" << std::endl; } ++eqc_i; diff --git a/src/theory/quantifiers/rep_set_iterator.cpp b/src/theory/quantifiers/rep_set_iterator.cpp index 9c1c4c89e..7461f3477 100644 --- a/src/theory/quantifiers/rep_set_iterator.cpp +++ b/src/theory/quantifiers/rep_set_iterator.cpp @@ -380,7 +380,7 @@ Node RepSetEvaluator::evaluateTerm( Node n, int& depIndex ){ //if not set already, rewrite and consult model for interpretation if( !setVal ){ val = Rewriter::rewrite( val ); - if( val.getMetaKind()!=kind::metakind::CONSTANT ){ + if( !val.isConst() ){ //FIXME: we cannot do this until we trust all theories collectModelInfo! //val = d_model->getInterpretedValue( val ); //val = d_model->getRepresentative( val ); |