summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-08-03 20:39:25 +0000
committerMorgan Deters <mdeters@gmail.com>2012-08-03 20:39:25 +0000
commit3daaecd22fe5f6147cb08e5a4e08177b33a2daa2 (patch)
tree46cb65c3673a5678a7779ff970aea9460233f1f1 /src/theory/quantifiers
parente26a44d5f98a9953dffeb07b29a21e7efd501684 (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.cpp2
-rw-r--r--src/theory/quantifiers/rep_set_iterator.cpp2
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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback