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/uf | |
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/uf')
-rw-r--r-- | src/theory/uf/symmetry_breaker.cpp | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp index 26678f21d..6298ff1ca 100644 --- a/src/theory/uf/symmetry_breaker.cpp +++ b/src/theory/uf/symmetry_breaker.cpp @@ -81,13 +81,13 @@ bool SymmetryBreaker::Template::matchRecursive(TNode t, TNode n) { } if(t.getNumChildren() == 0) { - if(t.getMetaKind() == kind::metakind::CONSTANT) { - Assert(n.getMetaKind() == kind::metakind::CONSTANT); + if(t.isConst()) { + Assert(n.isConst()); Debug("ufsymm:match") << "UFSYMM we have constants, failing match" << endl; return false; } - Assert(t.getMetaKind() == kind::metakind::VARIABLE && - n.getMetaKind() == kind::metakind::VARIABLE); + Assert(t.isVar() && + n.isVar()); t = find(t); n = find(n); Debug("ufsymm:match") << "UFSYMM variable match " << t << " , " << n << endl; @@ -218,8 +218,8 @@ Node SymmetryBreaker::normInternal(TNode n) { } else if((*i).getKind() == kind::IFF || (*i).getKind() == kind::EQUAL) { kids.push_back(normInternal(*i)); - if((*i)[0].getMetaKind() == kind::metakind::VARIABLE || - (*i)[1].getMetaKind() == kind::metakind::VARIABLE) { + if((*i)[0].isVar() || + (*i)[1].isVar()) { d_termEqs[(*i)[0]].insert((*i)[1]); d_termEqs[(*i)[1]].insert((*i)[0]); Debug("ufsymm:eq") << "UFSYMM " << (*i)[0] << " <==> " << (*i)[1] << endl; @@ -237,8 +237,8 @@ Node SymmetryBreaker::normInternal(TNode n) { case kind::IFF: case kind::EQUAL: - if(n[0].getMetaKind() == kind::metakind::VARIABLE || - n[1].getMetaKind() == kind::metakind::VARIABLE) { + if(n[0].isVar() || + n[1].isVar()) { d_termEqs[n[0]].insert(n[1]); d_termEqs[n[1]].insert(n[0]); Debug("ufsymm:eq") << "UFSYMM " << n[0] << " <==> " << n[1] << endl; |