diff options
Diffstat (limited to 'src/theory/builtin/theory_builtin.cpp')
-rw-r--r-- | src/theory/builtin/theory_builtin.cpp | 41 |
1 files changed, 0 insertions, 41 deletions
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index ddfd2ab59..1c779bd79 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -26,47 +26,6 @@ namespace CVC4 { namespace theory { namespace builtin { -Node TheoryBuiltin::simplify(TNode in, Substitutions& outSubstitutions) { - if(in.getKind() == kind::EQUAL) { - Node lhs = d_valuation.simplify(in[0], outSubstitutions); - Node rhs = d_valuation.simplify(in[1], outSubstitutions); - Node n = lhs.eqNode(rhs); - if( n[0].getMetaKind() == kind::metakind::VARIABLE && - n[1].getMetaKind() == kind::metakind::CONSTANT ) { - Debug("simplify:builtin") << "found new substitution! " - << n[0] << " => " << n[1] << endl; - outSubstitutions.push_back(make_pair(n[0], n[1])); - // with our substitutions we've subsumed the equality - return NodeManager::currentNM()->mkConst(true); - } else if( n[1].getMetaKind() == kind::metakind::VARIABLE && - n[0].getMetaKind() == kind::metakind::CONSTANT ) { - Debug("simplify:builtin") << "found new substitution! " - << n[1] << " => " << n[0] << endl; - outSubstitutions.push_back(make_pair(n[1], n[0])); - // with our substitutions we've subsumed the equality - return NodeManager::currentNM()->mkConst(true); - } - } else if(in.getKind() == kind::NOT && in[0].getKind() == kind::DISTINCT) { - TNode::iterator found = in[0].end(); - for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) { - if((*i).getMetaKind() == kind::metakind::CONSTANT) { - found = i; - break; - } - } - if(found != in[0].end()) { - for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) { - if(i != found) { - outSubstitutions.push_back(make_pair(*i, *found)); - } - } - // with our substitutions we've subsumed the (NOT (DISTINCT...)) - return NodeManager::currentNM()->mkConst(true); - } - } - return in; -} - Node TheoryBuiltin::getValue(TNode n) { switch(n.getKind()) { |