src/theory/booleans/theory_bool.cpp

   1 /*********************                                                        */
   2 /*! \file theory_bool.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, 2011  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 The theory of booleans.
  15  **
  16  ** The theory of booleans.
  17  **/
  18
  19 #include "theory/theory.h"
  20 #include "theory/booleans/theory_bool.h"
  21 #include "theory/booleans/circuit_propagator.h"
  22 #include "theory/valuation.h"
  23 #include "util/boolean_simplification.h"
  24
  25 #include <vector>
  26 #include <stack>
  27 #include "util/hash.h"
  28
  29 using namespace std;
  30
  31 namespace CVC4 {
  32 namespace theory {
  33 namespace booleans {
  34
  35 Node TheoryBool::getValue(TNode n) {
  36   NodeManager* nodeManager = NodeManager::currentNM();
  37
  38   switch(n.getKind()) {
  39   case kind::VARIABLE:
  40     // case for Boolean vars is implemented in TheoryEngine (since it
  41     // appeals to the PropEngine to get the value)
  42     Unreachable();
  43
  44   case kind::EQUAL: // 2 args
  45     // should be handled by IFF
  46     Unreachable();
  47
  48   case kind::NOT: // 1 arg
  49     return nodeManager->mkConst(! d_valuation.getValue(n[0]).getConst<bool>());
  50
  51   case kind::AND: { // 2+ args
  52     for(TNode::iterator i = n.begin(),
  53             iend = n.end();
  54           i != iend;
  55           ++i) {
  56       if(! d_valuation.getValue(*i).getConst<bool>()) {
  57         return nodeManager->mkConst(false);
  58       }
  59     }
  60     return nodeManager->mkConst(true);
  61   }
  62
  63   case kind::IFF: // 2 args
  64     return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() ==
  65                                  d_valuation.getValue(n[1]).getConst<bool>() );
  66
  67   case kind::IMPLIES: // 2 args
  68     return nodeManager->mkConst( (! d_valuation.getValue(n[0]).getConst<bool>()) ||
  69                                  d_valuation.getValue(n[1]).getConst<bool>() );
  70
  71   case kind::OR: { // 2+ args
  72     for(TNode::iterator i = n.begin(),
  73             iend = n.end();
  74           i != iend;
  75           ++i) {
  76       if(d_valuation.getValue(*i).getConst<bool>()) {
  77         return nodeManager->mkConst(true);
  78       }
  79     }
  80     return nodeManager->mkConst(false);
  81   }
  82
  83   case kind::XOR: // 2 args
  84     return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() !=
  85                                  d_valuation.getValue(n[1]).getConst<bool>() );
  86
  87   case kind::ITE: // 3 args
  88     // all ITEs should be gone except (bool,bool,bool) ones
  89     Assert( n[1].getType() == nodeManager->booleanType() &&
  90             n[2].getType() == nodeManager->booleanType() );
  91     return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() ?
  92                                  d_valuation.getValue(n[1]).getConst<bool>() :
  93                                  d_valuation.getValue(n[2]).getConst<bool>() );
  94
  95   default:
  96     Unhandled(n.getKind());
  97   }
  98 }
  99
 100 static void
 101 findAtoms(TNode in, vector<TNode>& atoms,
 102           hash_map<TNode, vector<TNode>, TNodeHashFunction>& backEdges) {
 103   Kind k CVC4_UNUSED = in.getKind();
 104   Assert(kindToTheoryId(k) == THEORY_BOOL);
 105
 106   stack< pair<TNode, TNode::iterator> > trail;
 107   hash_set<TNode, TNodeHashFunction> seen;
 108   trail.push(make_pair(in, in.begin()));
 109
 110   while(!trail.empty()) {
 111     pair<TNode, TNode::iterator>& pr = trail.top();
 112     Debug("simplify") << "looking at: " << pr.first << endl;
 113     if(pr.second == pr.first.end()) {
 114       trail.pop();
 115     } else {
 116       if(pr.second == pr.first.begin()) {
 117         Debug("simplify") << "first visit: " << pr.first << endl;
 118         // first time we've visited this node?
 119         if(seen.find(pr.first) == seen.end()) {
 120           Debug("simplify") << "+ haven't seen it yet." << endl;
 121           seen.insert(pr.first);
 122         } else {
 123           Debug("simplify") << "+ saw it before." << endl;
 124           trail.pop();
 125           continue;
 126         }
 127       }
 128       TNode n = *pr.second++;
 129       if(seen.find(n) == seen.end()) {
 130         Debug("simplify") << "back edge " << n << " to " << pr.first << endl;
 131         backEdges[n].push_back(pr.first);
 132         Kind nk = n.getKind();
 133         if(kindToTheoryId(nk) == THEORY_BOOL) {
 134           trail.push(make_pair(n, n.begin()));
 135         } else {
 136           Debug("simplify") << "atom: " << n << endl;
 137           atoms.push_back(n);
 138         }
 139       }
 140     }
 141   }
 142 }
 143
 144 Node TheoryBool::simplify(TNode in, Substitutions& outSubstitutions) {
 145   const unsigned prev = outSubstitutions.size();
 146
 147   if(kindToTheoryId(in.getKind()) != THEORY_BOOL) {
 148     Assert(in.getMetaKind() == kind::metakind::VARIABLE &&
 149            in.getType().isBoolean());
 150     return in;
 151   }
 152
 153   // form back edges and atoms
 154   vector<TNode> atoms;
 155   hash_map<TNode, vector<TNode>, TNodeHashFunction> backEdges;
 156   Debug("simplify") << "finding atoms..." << endl << push;
 157   findAtoms(in, atoms, backEdges);
 158   Debug("simplify") << pop << "done finding atoms..." << endl;
 159
 160   hash_map<TNode, Node, TNodeHashFunction> simplified;
 161
 162   vector<Node> newFacts;
 163   CircuitPropagator circuit(atoms, backEdges);
 164   Debug("simplify") << "propagate..." << endl;
 165   if(circuit.propagate(in, true, newFacts)) {
 166     Notice() << "Found a conflict in nonclausal Boolean reasoning" << endl;
 167     return NodeManager::currentNM()->mkConst(false);
 168   }
 169   Debug("simplify") << "done w/ propagate..." << endl;
 170
 171   for(vector<Node>::iterator i = newFacts.begin(), i_end = newFacts.end(); i != i_end; ++i) {
 172     TNode a = *i;
 173     if(a.getKind() == kind::NOT) {
 174       if(a[0].getMetaKind() == kind::metakind::VARIABLE ) {
 175         Debug("simplify") << "found bool unit ~" << a[0] << "..." << endl;
 176         outSubstitutions.push_back(make_pair(a[0], NodeManager::currentNM()->mkConst(false)));
 177       } else if(kindToTheoryId(a[0].getKind()) != THEORY_BOOL) {
 178         Debug("simplify") << "simplifying: " << a << endl;
 179         simplified[a] = d_valuation.simplify(a, outSubstitutions);
 180         Debug("simplify") << "done simplifying, got: " << simplified[a] << endl;
 181       }
 182     } else {
 183       if(a.getMetaKind() == kind::metakind::VARIABLE) {
 184         Debug("simplify") << "found bool unit " << a << "..." << endl;
 185         outSubstitutions.push_back(make_pair(a, NodeManager::currentNM()->mkConst(true)));
 186       } else if(kindToTheoryId(a.getKind()) != THEORY_BOOL) {
 187         Debug("simplify") << "simplifying: " << a << endl;
 188         simplified[a] = d_valuation.simplify(a, outSubstitutions);
 189         Debug("simplify") << "done simplifying, got: " << simplified[a] << endl;
 190       }
 191     }
 192   }
 193
 194   Debug("simplify") << "substituting in root..." << endl;
 195   Node n = in.substitute(outSubstitutions.begin(), outSubstitutions.end());
 196   Debug("simplify") << "got: " << n << endl;
 197   if(Debug.isOn("simplify")) {
 198     Debug("simplify") << "new substitutions:" << endl;
 199     copy(outSubstitutions.begin() + prev, outSubstitutions.end(),
 200          ostream_iterator< pair<TNode, TNode> >(Debug("simplify"), "\n"));
 201     Debug("simplify") << "done." << endl;
 202   }
 203   if(outSubstitutions.size() > prev) {
 204     NodeBuilder<> b(kind::AND);
 205     b << n;
 206     for(Substitutions::iterator i = outSubstitutions.begin() + prev,
 207           i_end = outSubstitutions.end();
 208         i != i_end;
 209         ++i) {
 210       if((*i).first.getType().isBoolean()) {
 211         if((*i).second.getMetaKind() == kind::metakind::CONSTANT) {
 212           if((*i).second.getConst<bool>()) {
 213             b << (*i).first;
 214           } else {
 215             b << BooleanSimplification::negate((*i).first);
 216           }
 217         } else {
 218           b << (*i).first.iffNode((*i).second);
 219         }
 220       } else {
 221         b << (*i).first.eqNode((*i).second);
 222       }
 223     }
 224     n = b;
 225   }
 226   Debug("simplify") << "final boolean simplification returned: " << n << endl;
 227   return n;
 228 }
 229
 230
 231 }/* CVC4::theory::booleans namespace */
 232 }/* CVC4::theory namespace */
 233 }/* CVC4 namespace */