src/smt_util/boolean_simplification.cpp

   1 /*********************                                                        */
   2 /*! \file boolean_simplification.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 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 "smt_util/boolean_simplification.h"
  18
  19 namespace CVC4 {
  20
  21 bool
  22 BooleanSimplification::push_back_associative_commute_recursive
  23     (Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode)
  24     throw(AssertionException) {
  25   Node::iterator i = n.begin(), end = n.end();
  26   for(; i != end; ++i){
  27     Node child = *i;
  28     if(child.getKind() == k){
  29       if(! push_back_associative_commute_recursive(child, buffer, k, notK, negateNode)) {
  30         return false;
  31       }
  32     }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){
  33       if(! push_back_associative_commute_recursive(child[0], buffer, notK, k, !negateNode)) {
  34         return false;
  35       }
  36     }else{
  37       if(negateNode){
  38         if(child.isConst()) {
  39           if((k == kind::AND && child.getConst<bool>()) ||
  40              (k == kind::OR && !child.getConst<bool>())) {
  41             buffer.clear();
  42             buffer.push_back(negate(child));
  43             return false;
  44           }
  45         } else {
  46           buffer.push_back(negate(child));
  47         }
  48       }else{
  49         if(child.isConst()) {
  50           if((k == kind::OR && child.getConst<bool>()) ||
  51              (k == kind::AND && !child.getConst<bool>())) {
  52             buffer.clear();
  53             buffer.push_back(child);
  54             return false;
  55           }
  56         } else {
  57           buffer.push_back(child);
  58         }
  59       }
  60     }
  61   }
  62   return true;
  63 }/* BooleanSimplification::push_back_associative_commute_recursive() */
  64
  65 }/* CVC4 namespace */