src/smt_util/boolean_simplification.h

   1 /*********************                                                        */
   2 /*! \file boolean_simplification.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Simple routines for Boolean simplification
  13  **
  14  ** Simple, commonly-used routines for Boolean simplification.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__BOOLEAN_SIMPLIFICATION_H
  20 #define CVC4__BOOLEAN_SIMPLIFICATION_H
  21
  22 #include <vector>
  23 #include <algorithm>
  24
  25 #include "base/check.h"
  26 #include "expr/expr_manager_scope.h"
  27 #include "expr/node.h"
  28
  29 namespace CVC4 {
  30
  31 /**
  32  * A class to contain a number of useful functions for simple
  33  * simplification of nodes.  One never uses it as an object (and
  34  * it cannot be constructed).  It is used as a namespace.
  35  */
  36 class BooleanSimplification {
  37   // cannot construct one of these
  38   BooleanSimplification() = delete;
  39   BooleanSimplification(const BooleanSimplification&) = delete;
  40
  41   static bool push_back_associative_commute_recursive(
  42       Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
  43       CVC4_WARN_UNUSED_RESULT;
  44
  45  public:
  46   /**
  47    * The threshold for removing duplicates.  (See removeDuplicates().)
  48    */
  49   static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10;
  50
  51   /**
  52    * Remove duplicate nodes from a vector, modifying it in-place.
  53    * If the vector has size >= DUPLICATE_REMOVAL_THRESHOLD, this
  54    * function is a no-op.
  55    */
  56   static void removeDuplicates(std::vector<Node>& buffer)
  57   {
  58     if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD) {
  59       std::sort(buffer.begin(), buffer.end());
  60       std::vector<Node>::iterator new_end =
  61         std::unique(buffer.begin(), buffer.end());
  62       buffer.erase(new_end, buffer.end());
  63     }
  64   }
  65
  66   /**
  67    * Takes a node with kind AND, collapses all AND and (NOT OR)-kinded
  68    * children of it (as far as possible---see
  69    * push_back_associative_commute()), removes duplicates, and returns
  70    * the resulting Node.
  71    */
  72   static Node simplifyConflict(Node andNode)
  73   {
  74     AssertArgument(!andNode.isNull(), andNode);
  75     AssertArgument(andNode.getKind() == kind::AND, andNode);
  76
  77     std::vector<Node> buffer;
  78     push_back_associative_commute(andNode, buffer, kind::AND, kind::OR);
  79
  80     removeDuplicates(buffer);
  81
  82     if(buffer.size() == 1) {
  83       return buffer[0];
  84     }
  85
  86     NodeBuilder<> nb(kind::AND);
  87     nb.append(buffer);
  88     return nb;
  89   }
  90
  91   /**
  92    * Takes a node with kind OR, collapses all OR and (NOT AND)-kinded
  93    * children of it (as far as possible---see
  94    * push_back_associative_commute()), removes duplicates, and returns
  95    * the resulting Node.
  96    */
  97   static Node simplifyClause(Node orNode)
  98   {
  99     AssertArgument(!orNode.isNull(), orNode);
 100     AssertArgument(orNode.getKind() == kind::OR, orNode);
 101
 102     std::vector<Node> buffer;
 103     push_back_associative_commute(orNode, buffer, kind::OR, kind::AND);
 104
 105     removeDuplicates(buffer);
 106
 107     Assert(buffer.size() > 0);
 108     if(buffer.size() == 1) {
 109       return buffer[0];
 110     }
 111
 112     NodeBuilder<> nb(kind::OR);
 113     nb.append(buffer);
 114     return nb;
 115   }
 116
 117   /**
 118    * Takes a node with kind IMPLIES, converts it to an OR, then
 119    * simplifies the result with simplifyClause().
 120    *
 121    * The input doesn't actually have to be Horn, it seems, but that's
 122    * the common case(?), hence the name.
 123    */
 124   static Node simplifyHornClause(Node implication)
 125   {
 126     AssertArgument(implication.getKind() == kind::IMPLIES, implication);
 127
 128     TNode left = implication[0];
 129     TNode right = implication[1];
 130
 131     Node notLeft = negate(left);
 132     Node clause = NodeBuilder<2>(kind::OR) << notLeft << right;
 133
 134     return simplifyClause(clause);
 135   }
 136
 137   /**
 138    * Aids in reforming a node.  Takes a node of (N-ary) kind k and
 139    * copies its children into an output vector, collapsing its k-kinded
 140    * children into it.  Also collapses negations of notK.  For example:
 141    *
 142    *   push_back_associative_commute( [OR [OR a b] [OR b c d] [NOT [AND e f]]],
 143    *                                  buffer, kind::OR, kind::AND )
 144    *   yields a "buffer" vector of [a b b c d e f]
 145    *
 146    * @param n the node to operate upon
 147    * @param buffer the output vector (must be empty on entry)
 148    * @param k the kind to collapse (should equal the kind of node n)
 149    * @param notK the "negation" of kind k (e.g. OR's negation is AND),
 150    * or kind::UNDEFINED_KIND if none.
 151    * @param negateChildren true if the children of the resulting node
 152    * (that is, the elements in buffer) should all be negated; you want
 153    * this if e.g. you're simplifying the (OR...) in (NOT (OR...)),
 154    * intending to make the result an AND.
 155    */
 156   static inline void push_back_associative_commute(Node n,
 157                                                    std::vector<Node>& buffer,
 158                                                    Kind k,
 159                                                    Kind notK,
 160                                                    bool negateChildren = false)
 161   {
 162     AssertArgument(buffer.empty(), buffer);
 163     AssertArgument(!n.isNull(), n);
 164     AssertArgument(k != kind::UNDEFINED_KIND && k != kind::NULL_EXPR, k);
 165     AssertArgument(notK != kind::NULL_EXPR, notK);
 166     AssertArgument(n.getKind() == k, n,
 167                    "expected node to have kind %s", kindToString(k).c_str());
 168
 169     bool b CVC4_UNUSED =
 170       push_back_associative_commute_recursive(n, buffer, k, notK, false);
 171
 172     if(buffer.size() == 0) {
 173       // all the TRUEs for an AND (resp FALSEs for an OR) were simplified away
 174       buffer.push_back(NodeManager::currentNM()->mkConst(k == kind::AND ? true : false));
 175     }
 176   }/* push_back_associative_commute() */
 177
 178   /**
 179    * Negates a node, doing all the double-negation elimination
 180    * that's possible.
 181    *
 182    * @param n the node to negate (cannot be the null node)
 183    */
 184   static Node negate(TNode n)
 185   {
 186     AssertArgument(!n.isNull(), n);
 187
 188     bool polarity = true;
 189     TNode base = n;
 190     while(base.getKind() == kind::NOT){
 191       base = base[0];
 192       polarity = !polarity;
 193     }
 194     if(n.isConst()) {
 195       return NodeManager::currentNM()->mkConst(!n.getConst<bool>());
 196     }
 197     if(polarity){
 198       return base.notNode();
 199     }else{
 200       return base;
 201     }
 202   }
 203
 204   /**
 205    * Negates an Expr, doing all the double-negation elimination that's
 206    * possible.
 207    *
 208    * @param e the Expr to negate (cannot be the null Expr)
 209    */
 210   static Expr negate(Expr e)
 211   {
 212     ExprManagerScope ems(e);
 213     return negate(Node::fromExpr(e)).toExpr();
 214   }
 215
 216   /**
 217    * Simplify an OR, AND, or IMPLIES.  This function is the identity
 218    * for all other kinds.
 219    */
 220   inline static Node simplify(TNode n)
 221   {
 222     switch(n.getKind()) {
 223     case kind::AND:
 224       return simplifyConflict(n);
 225
 226     case kind::OR:
 227       return simplifyClause(n);
 228
 229     case kind::IMPLIES:
 230       return simplifyHornClause(n);
 231
 232     default:
 233       return n;
 234     }
 235   }
 236
 237 };/* class BooleanSimplification */
 238
 239 }/* CVC4 namespace */
 240
 241 #endif /* CVC4__BOOLEAN_SIMPLIFICATION_H */