src/proof/simplify_boolean_node.h

   1 /*********************                                                        */
   2 /*! \file simplify_boolean_node.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Guy Katz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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 Simplifying a boolean node, needed for constructing LFSC proofs.
  13  **
  14  **/
  15
  16 #include "cvc4_private.h"
  17
  18 #ifndef __CVC4__SIMPLIFY_BOOLEAN_NODE_H
  19 #define __CVC4__SIMPLIFY_BOOLEAN_NODE_H
  20
  21 namespace CVC4 {
  22
  23 Node simplifyBooleanNode(const Node &n);
  24
  25 }/* CVC4 namespace */
  26
  27 #endif /* __CVC4__SIMPLIFY_BOOLEAN_NODE_H */