src/util/boolean_simplification.h

   1 /*********************                                                        */
   2 /*! \file bitvector.h
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: cconway
   6  ** Minor contributors (to current version): mdeters
   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 [[ Add one-line brief description here ]]
  15  **
  16  ** [[ Add lengthier description here ]]
  17  ** \todo document this file
  18  **/
  19
  20 #include "cvc4_private.h"
  21
  22 #ifndef __CVC4__BOOLEAN_SIMPLIFICATION_H
  23 #define __CVC4__BOOLEAN_SIMPLIFICATION_H
  24
  25 #include "expr/node.h"
  26 #include "util/Assert.h"
  27 #include <vector>
  28
  29
  30 namespace CVC4 {
  31
  32 class BooleanSimplification {
  33 public:
  34
  35   static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10;
  36
  37   static void removeDuplicates(std::vector<Node>& buffer){
  38     if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD){
  39       std::sort(buffer.begin(), buffer.end());
  40       std::vector<Node>::iterator new_end = std::unique(buffer.begin(), buffer.end());
  41       buffer.erase(new_end, buffer.end());
  42     }
  43   }
  44
  45   static Node simplifyConflict(Node andNode){
  46     Assert(andNode.getKind() == kind::AND);
  47     std::vector<Node> buffer;
  48     push_back_associative_commute(andNode, buffer, kind::AND, kind::OR, false);
  49
  50     removeDuplicates(buffer);
  51
  52     NodeBuilder<> nb(kind::AND);
  53     nb.append(buffer);
  54     return nb;
  55   }
  56
  57   static Node simplifyClause(Node orNode){
  58     Assert(orNode.getKind() == kind::OR);
  59     std::vector<Node> buffer;
  60     push_back_associative_commute(orNode, buffer, kind::OR, kind::AND, false);
  61
  62     removeDuplicates(buffer);
  63
  64     NodeBuilder<> nb(kind::OR);
  65     nb.append(buffer);
  66     return nb;
  67   }
  68
  69   static Node simplifyHornClause(Node implication){
  70     Assert(implication.getKind() == kind::IMPLIES);
  71     TNode left = implication[0];
  72     TNode right = implication[1];
  73     Node notLeft = NodeBuilder<1>(kind::NOT)<<left;
  74     Node clause = NodeBuilder<2>(kind::OR)<< notLeft << right;
  75     return simplifyClause(clause);
  76   }
  77
  78   static void push_back_associative_commute(Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode){
  79     Node::iterator i = n.begin(), end = n.end();
  80     for(; i != end; ++i){
  81       Node child = *i;
  82       if(child.getKind() == k){
  83         push_back_associative_commute(child, buffer, k, notK, negateNode);
  84       }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){
  85         push_back_associative_commute(child, buffer, notK, k, !negateNode);
  86       }else{
  87         if(negateNode){
  88           buffer.push_back(negate(child));
  89         }else{
  90           buffer.push_back(child);
  91         }
  92       }
  93     }
  94   }
  95
  96   static Node negate(TNode n){
  97     bool polarity = true;
  98     TNode base = n;
  99     while(base.getKind() == kind::NOT){
 100       base = base[0];
 101       polarity = !polarity;
 102     }
 103     if(polarity){
 104       return base.notNode();
 105     }else{
 106       return base;
 107     }
 108   }
 109
 110 };/* class BitVector */
 111
 112
 113
 114 }/* CVC4 namespace */
 115
 116 #endif /* __CVC4__BITVECTOR_H */