src/theory/builtin/theory_builtin.cpp

   1 /*********************                                                        */
   2 /*! \file theory_builtin.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Implementation of the builtin theory.
  15  **
  16  ** Implementation of the builtin theory.
  17  **/
  18
  19 #include "theory/builtin/theory_builtin.h"
  20 #include "theory/valuation.h"
  21 #include "expr/kind.h"
  22
  23 using namespace std;
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace builtin {
  28
  29 Node TheoryBuiltin::simplify(TNode in, Substitutions& outSubstitutions) {
  30   if(in.getKind() == kind::EQUAL) {
  31     Node lhs = d_valuation.simplify(in[0], outSubstitutions);
  32     Node rhs = d_valuation.simplify(in[1], outSubstitutions);
  33     Node n = lhs.eqNode(rhs);
  34     if( n[0].getMetaKind() == kind::metakind::VARIABLE &&
  35         n[1].getMetaKind() == kind::metakind::CONSTANT ) {
  36       Debug("simplify:builtin") << "found new substitution! "
  37                                 << n[0] << " => " << n[1] << endl;
  38       outSubstitutions.push_back(make_pair(n[0], n[1]));
  39       // with our substitutions we've subsumed the equality
  40       return NodeManager::currentNM()->mkConst(true);
  41     } else if( n[1].getMetaKind() == kind::metakind::VARIABLE &&
  42                n[0].getMetaKind() == kind::metakind::CONSTANT ) {
  43       Debug("simplify:builtin") << "found new substitution! "
  44                                 << n[1] << " => " << n[0] << endl;
  45       outSubstitutions.push_back(make_pair(n[1], n[0]));
  46       // with our substitutions we've subsumed the equality
  47       return NodeManager::currentNM()->mkConst(true);
  48     }
  49   } else if(in.getKind() == kind::NOT && in[0].getKind() == kind::DISTINCT) {
  50     TNode::iterator found = in[0].end();
  51     for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) {
  52       if((*i).getMetaKind() == kind::metakind::CONSTANT) {
  53         found = i;
  54         break;
  55       }
  56     }
  57     if(found != in[0].end()) {
  58       for(TNode::iterator i = in[0].begin(), i_end = in[0].end(); i != i_end; ++i) {
  59         if(i != found) {
  60           outSubstitutions.push_back(make_pair(*i, *found));
  61         }
  62       }
  63       // with our substitutions we've subsumed the (NOT (DISTINCT...))
  64       return NodeManager::currentNM()->mkConst(true);
  65     }
  66   }
  67   return in;
  68 }
  69
  70 Node TheoryBuiltin::getValue(TNode n) {
  71   switch(n.getKind()) {
  72
  73   case kind::VARIABLE:
  74     // no variables that the builtin theory is responsible for
  75     Unreachable();
  76
  77   case kind::EQUAL: { // 2 args
  78     // has to be an EQUAL over tuples, since all others should be
  79     // handled elsewhere
  80     Assert(n[0].getKind() == kind::TUPLE &&
  81            n[1].getKind() == kind::TUPLE);
  82     return NodeManager::currentNM()->
  83       mkConst( getValue(n[0]) == getValue(n[1]) );
  84   }
  85
  86   case kind::TUPLE: { // 2+ args
  87     NodeBuilder<> nb(kind::TUPLE);
  88     for(TNode::iterator i = n.begin(),
  89           iend = n.end();
  90         i != iend;
  91         ++i) {
  92       nb << d_valuation.getValue(*i);
  93     }
  94     return Node(nb);
  95   }
  96
  97   default:
  98     // all other "builtins" should have been rewritten away or handled
  99     // by the valuation, or handled elsewhere.
 100     Unhandled(n.getKind());
 101   }
 102 }
 103
 104 }/* CVC4::theory::builtin namespace */
 105 }/* CVC4::theory */
 106 }/* CVC4 namespace */