src/prop/cnf_stream.h

   1 /*********************                                                        */
   2 /*! \file cnf_stream.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Tim King, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 This class transforms a sequence of formulas into clauses.
  13  **
  14  ** This class takes a sequence of formulas.
  15  ** It outputs a stream of clauses that is propositionally
  16  ** equi-satisfiable with the conjunction of the formulas.
  17  ** This stream is maintained in an online fashion.
  18  **
  19  ** Unlike other parts of the system it is aware of the PropEngine's
  20  ** internals such as the representation and translation of [??? -Chris]
  21  **/
  22
  23 #include "cvc4_private.h"
  24
  25 #ifndef CVC4__PROP__CNF_STREAM_H
  26 #define CVC4__PROP__CNF_STREAM_H
  27
  28 #include "context/cdinsert_hashmap.h"
  29 #include "context/cdlist.h"
  30 #include "expr/node.h"
  31 #include "proof/proof_manager.h"
  32 #include "prop/registrar.h"
  33 #include "prop/theory_proxy.h"
  34
  35 namespace CVC4 {
  36
  37 namespace prop {
  38
  39 class PropEngine;
  40
  41 /**
  42  * Comments for the behavior of the whole class... [??? -Chris]
  43  * @author Tim King <taking@cs.nyu.edu>
  44  */
  45 class CnfStream {
  46  public:
  47   /** Cache of what nodes have been registered to a literal. */
  48   typedef context::CDInsertHashMap<SatLiteral, TNode, SatLiteralHashFunction>
  49       LiteralToNodeMap;
  50
  51   /** Cache of what literals have been registered to a node. */
  52   typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction>
  53       NodeToLiteralMap;
  54
  55  protected:
  56   /** The SAT solver we will be using */
  57   SatSolver* d_satSolver;
  58
  59   /** Boolean variables that we translated */
  60   context::CDList<TNode> d_booleanVariables;
  61
  62   /** Map from nodes to literals */
  63   NodeToLiteralMap d_nodeToLiteralMap;
  64
  65   /** Map from literals to nodes */
  66   LiteralToNodeMap d_literalToNodeMap;
  67
  68   /**
  69    * True if the lit-to-Node map should be kept for all lits, not just
  70    * theory lits.  This is true if e.g. replay logging is on, which
  71    * dumps the Nodes corresponding to decision literals.
  72    */
  73   const bool d_fullLitToNodeMap;
  74
  75   /**
  76    * Counter for resource limiting that is used to spend a resource
  77    * every ResourceManager::resourceCounter calls to convertAndAssert.
  78    */
  79   unsigned long d_convertAndAssertCounter;
  80
  81   /** The "registrar" for pre-registration of terms */
  82   Registrar* d_registrar;
  83
  84   /** The name of this CNF stream*/
  85   std::string d_name;
  86
  87   /** Pointer to the proof corresponding to this CnfStream */
  88   CnfProof* d_cnfProof;
  89
  90   /** Remove nots from the node */
  91   TNode stripNot(TNode node) {
  92     while (node.getKind() == kind::NOT) {
  93       node = node[0];
  94     }
  95     return node;
  96   }
  97
  98   /**
  99    * Are we asserting a removable clause (true) or a permanent clause (false).
 100    * This is set at the beginning of convertAndAssert so that it doesn't
 101    * need to be passed on over the stack.  Only pure clauses can be asserted
 102    * as removable.
 103    */
 104   bool d_removable;
 105
 106   /**
 107    * Asserts the given clause to the sat solver.
 108    * @param node the node giving rise to this clause
 109    * @param clause the clause to assert
 110    */
 111   void assertClause(TNode node, SatClause& clause);
 112
 113   /**
 114    * Asserts the unit clause to the sat solver.
 115    * @param node the node giving rise to this clause
 116    * @param a the unit literal of the clause
 117    */
 118   void assertClause(TNode node, SatLiteral a);
 119
 120   /**
 121    * Asserts the binary clause to the sat solver.
 122    * @param node the node giving rise to this clause
 123    * @param a the first literal in the clause
 124    * @param b the second literal in the clause
 125    */
 126   void assertClause(TNode node, SatLiteral a, SatLiteral b);
 127
 128   /**
 129    * Asserts the ternary clause to the sat solver.
 130    * @param node the node giving rise to this clause
 131    * @param a the first literal in the clause
 132    * @param b the second literal in the clause
 133    * @param c the thirs literal in the clause
 134    */
 135   void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
 136
 137   /**
 138    * Acquires a new variable from the SAT solver to represent the node
 139    * and inserts the necessary data it into the mapping tables.
 140    * @param node a formula
 141    * @param isTheoryAtom is this a theory atom that needs to be asserted to
 142    * theory.
 143    * @param preRegister whether to preregister the atom with the theory
 144    * @param canEliminate whether the sat solver can safely eliminate this
 145    * variable.
 146    * @return the literal corresponding to the formula
 147    */
 148   SatLiteral newLiteral(TNode node, bool isTheoryAtom = false,
 149                         bool preRegister = false, bool canEliminate = true);
 150
 151   /**
 152    * Constructs a new literal for an atom and returns it.  Calls
 153    * newLiteral().
 154    *
 155    * @param node the node to convert; there should be no boolean
 156    * structure in this expression.  Assumed to not be in the
 157    * translation cache.
 158    */
 159   SatLiteral convertAtom(TNode node, bool noPreprocessing = false);
 160
 161  public:
 162   /**
 163    * Constructs a CnfStream that sends constructs an equi-satisfiable
 164    * set of clauses and sends them to the given sat solver. This does not take
 165    * ownership of satSolver, registrar, or context.
 166    * @param satSolver the sat solver to use.
 167    * @param registrar the entity that takes care of preregistration of Nodes.
 168    * @param context the context that the CNF should respect.
 169    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping.
 170    * @param name string identifier to distinguish between different instances
 171    * even for non-theory literals.
 172    */
 173   CnfStream(SatSolver* satSolver, Registrar* registrar,
 174             context::Context* context, bool fullLitToNodeMap = false,
 175             std::string name = "");
 176
 177   /**
 178    * Destructs a CnfStream.  This implementation does nothing, but we
 179    * need a virtual destructor for safety in case subclasses have a
 180    * destructor.
 181    */
 182   virtual ~CnfStream() {}
 183
 184   /**
 185    * Converts and asserts a formula.
 186    * @param node node to convert and assert
 187    * @param removable whether the sat solver can choose to remove the clauses
 188    * @param negated whether we are asserting the node negated
 189    */
 190   virtual void convertAndAssert(TNode node, bool removable, bool negated,
 191                                 ProofRule proof_id,
 192                                 TNode from = TNode::null()) = 0;
 193
 194   /**
 195    * Get the node that is represented by the given SatLiteral.
 196    * @param literal the literal from the sat solver
 197    * @return the actual node
 198    */
 199   TNode getNode(const SatLiteral& literal);
 200
 201   /**
 202    * Returns true iff the node has an assigned literal (it might not be
 203    * translated).
 204    * @param node the node
 205    */
 206   bool hasLiteral(TNode node) const;
 207
 208   /**
 209    * Ensure that the given node will have a designated SAT literal that is
 210    * definitionally equal to it.  The result of this function is that the Node
 211    * can be queried via getSatValue(). Essentially, this is like a "convert-but-
 212    * don't-assert" version of convertAndAssert().
 213    */
 214   virtual void ensureLiteral(TNode n, bool noPreregistration = false) = 0;
 215
 216   /**
 217    * Returns the literal that represents the given node in the SAT CNF
 218    * representation.
 219    * @param node [Presumably there are some constraints on the kind of
 220    * node? E.g., it needs to be a boolean? -Chris]
 221    */
 222   SatLiteral getLiteral(TNode node);
 223
 224   /**
 225    * Returns the Boolean variables from the input problem.
 226    */
 227   void getBooleanVariables(std::vector<TNode>& outputVariables) const;
 228
 229   const NodeToLiteralMap& getTranslationCache() const {
 230     return d_nodeToLiteralMap;
 231   }
 232
 233   const LiteralToNodeMap& getNodeCache() const { return d_literalToNodeMap; }
 234
 235   void setProof(CnfProof* proof);
 236 }; /* class CnfStream */
 237
 238 /**
 239  * TseitinCnfStream is based on the following recursive algorithm
 240  * http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
 241  * The general idea is to introduce a new literal that
 242  * will be equivalent to each subexpression in the constructed equi-satisfiable
 243  * formula, then substitute the new literal for the formula, and so on,
 244  * recursively.
 245  *
 246  * This implementation does this in a single recursive pass. [??? -Chris]
 247  */
 248 class TseitinCnfStream : public CnfStream {
 249  public:
 250   /**
 251    * Constructs the stream to use the given sat solver.  This does not take
 252    * ownership of satSolver, registrar, or context.
 253    * @param satSolver the sat solver to use
 254    * @param registrar the entity that takes care of pre-registration of Nodes
 255    * @param context the context that the CNF should respect.
 256    * @param rm the resource manager of the CNF stream
 257    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
 258    * even for non-theory literals
 259    */
 260   TseitinCnfStream(SatSolver* satSolver,
 261                    Registrar* registrar,
 262                    context::Context* context,
 263                    ResourceManager* rm,
 264                    bool fullLitToNodeMap = false,
 265                    std::string name = "");
 266
 267   /**
 268    * Convert a given formula to CNF and assert it to the SAT solver.
 269    * @param node the formula to assert
 270    * @param removable is this something that can be erased
 271    * @param negated true if negated
 272    */
 273   void convertAndAssert(TNode node,
 274                         bool removable,
 275                         bool negated,
 276                         ProofRule rule,
 277                         TNode from = TNode::null()) override;
 278
 279  private:
 280   /**
 281    * Same as above, except that removable is remembered.
 282    */
 283   void convertAndAssert(TNode node, bool negated);
 284
 285   // Each of these formulas handles takes care of a Node of each Kind.
 286   //
 287   // Each handleX(Node &n) is responsible for:
 288   //   - constructing a new literal, l (if necessary)
 289   //   - calling registerNode(n,l)
 290   //   - adding clauses assure that l is equivalent to the Node
 291   //   - calling toCNF on its children (if necessary)
 292   //   - returning l
 293   //
 294   // handleX( n ) can assume that n is not in d_translationCache
 295   SatLiteral handleNot(TNode node);
 296   SatLiteral handleXor(TNode node);
 297   SatLiteral handleImplies(TNode node);
 298   SatLiteral handleIff(TNode node);
 299   SatLiteral handleIte(TNode node);
 300   SatLiteral handleAnd(TNode node);
 301   SatLiteral handleOr(TNode node);
 302
 303   void convertAndAssertAnd(TNode node, bool negated);
 304   void convertAndAssertOr(TNode node, bool negated);
 305   void convertAndAssertXor(TNode node, bool negated);
 306   void convertAndAssertIff(TNode node, bool negated);
 307   void convertAndAssertImplies(TNode node, bool negated);
 308   void convertAndAssertIte(TNode node, bool negated);
 309
 310   /**
 311    * Transforms the node into CNF recursively.
 312    * @param node the formula to transform
 313    * @param negated whether the literal is negated
 314    * @return the literal representing the root of the formula
 315    */
 316   SatLiteral toCNF(TNode node, bool negated = false);
 317
 318   void ensureLiteral(TNode n, bool noPreregistration = false) override;
 319
 320   /** Pointer to resource manager for associated SmtEngine */
 321   ResourceManager* d_resourceManager;
 322 }; /* class TseitinCnfStream */
 323
 324 } /* CVC4::prop namespace */
 325 } /* CVC4 namespace */
 326
 327 #endif /* CVC4__PROP__CNF_STREAM_H */