src/theory/booleans/circuit_propagator.h

   1 /*********************                                                        */
   2 /*! \file circuit_propagator.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Aina Niemetz, Gereon Kremer
   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 A non-clausal circuit propagator for Boolean simplification
  13  **
  14  ** A non-clausal circuit propagator for Boolean simplification.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
  20 #define CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H
  21
  22 #include <functional>
  23 #include <memory>
  24 #include <unordered_map>
  25 #include <vector>
  26
  27 #include "context/cdhashmap.h"
  28 #include "context/cdhashset.h"
  29 #include "context/cdo.h"
  30 #include "context/context.h"
  31 #include "expr/lazy_proof_chain.h"
  32 #include "expr/node.h"
  33 #include "expr/proof_generator.h"
  34 #include "expr/proof_node.h"
  35 #include "theory/eager_proof_generator.h"
  36 #include "theory/theory.h"
  37 #include "theory/trust_node.h"
  38 #include "util/hash.h"
  39
  40 namespace CVC4 {
  41 namespace theory {
  42 namespace booleans {
  43
  44 /**
  45  * The main purpose of the CircuitPropagator class is to maintain the
  46  * state of the circuit for subsequent calls to propagate(), so that
  47  * the same fact is not output twice, so that the same edge in the
  48  * circuit isn't propagated twice, etc.
  49  */
  50 class CircuitPropagator
  51 {
  52  public:
  53   /**
  54    * Value of a particular node
  55    */
  56   enum AssignmentStatus
  57   {
  58     /** Node is currently unassigned */
  59     UNASSIGNED = 0,
  60     /** Node is assigned to true */
  61     ASSIGNED_TO_TRUE,
  62     /** Node is assigned to false */
  63     ASSIGNED_TO_FALSE,
  64   };
  65
  66   typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
  67       BackEdgesMap;
  68
  69   /**
  70    * Construct a new CircuitPropagator.
  71    */
  72   CircuitPropagator(bool enableForward = true, bool enableBackward = true);
  73
  74   /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
  75   bool getAssignment(TNode n) const
  76   {
  77     AssignmentMap::iterator i = d_state.find(n);
  78     Assert(i != d_state.end() && (*i).second != UNASSIGNED);
  79     return (*i).second == ASSIGNED_TO_TRUE;
  80   }
  81
  82   // Use custom context to ensure propagator is reset after use
  83   void initialize() { d_context.push(); }
  84
  85   void setNeedsFinish(bool value) { d_needsFinish = value; }
  86
  87   bool getNeedsFinish() { return d_needsFinish; }
  88
  89   std::vector<TrustNode>& getLearnedLiterals() { return d_learnedLiterals; }
  90
  91   /** Finish the computation and pop the internal context */
  92   void finish();
  93
  94   /** Assert for propagation */
  95   void assertTrue(TNode assertion);
  96
  97   /**
  98    * Propagate through the asserted circuit propagator. New information
  99    * discovered by the propagator are put in the substitutions vector used in
 100    * construction.
 101    *
 102    * @return a trust node encapsulating the proof for a conflict as a lemma that
 103    * proves false, or the null trust node otherwise
 104    */
 105   TrustNode propagate() CVC4_WARN_UNUSED_RESULT;
 106
 107   /**
 108    * Get the back edges of this circuit.
 109    */
 110   const BackEdgesMap& getBackEdges() const { return d_backEdges; }
 111
 112   /** Invert a set value */
 113   static inline AssignmentStatus neg(AssignmentStatus value)
 114   {
 115     Assert(value != UNASSIGNED);
 116     if (value == ASSIGNED_TO_TRUE)
 117       return ASSIGNED_TO_FALSE;
 118     else
 119       return ASSIGNED_TO_TRUE;
 120   }
 121
 122   /** True iff Node is assigned in circuit (either true or false). */
 123   bool isAssigned(TNode n) const
 124   {
 125     AssignmentMap::const_iterator i = d_state.find(n);
 126     return i != d_state.end() && ((*i).second != UNASSIGNED);
 127   }
 128
 129   /** True iff Node is assigned to the value. */
 130   bool isAssignedTo(TNode n, bool value) const
 131   {
 132     AssignmentMap::const_iterator i = d_state.find(n);
 133     if (i == d_state.end()) return false;
 134     if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true;
 135     if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
 136     return false;
 137   }
 138   /**
 139    * Set proof node manager, context and parent proof generator.
 140    *
 141    * If parent is non-null, then it is responsible for the proofs provided
 142    * to this class.
 143    */
 144   void setProof(ProofNodeManager* pnm,
 145                 context::Context* ctx,
 146                 ProofGenerator* defParent);
 147
 148  private:
 149   /** A context-notify object that clears out stale data. */
 150   template <class T>
 151   class DataClearer : context::ContextNotifyObj
 152   {
 153    public:
 154     DataClearer(context::Context* context, T& data)
 155         : context::ContextNotifyObj(context), d_data(data)
 156     {
 157     }
 158
 159    protected:
 160     void contextNotifyPop() override
 161     {
 162       Trace("circuit-prop")
 163           << "CircuitPropagator::DataClearer: clearing data "
 164           << "(size was " << d_data.size() << ")" << std::endl;
 165       d_data.clear();
 166     }
 167
 168    private:
 169     T& d_data;
 170   }; /* class DataClearer<T> */
 171
 172   /** Predicate for use in STL functions. */
 173   class IsAssigned : public std::unary_function<TNode, bool>
 174   {
 175     CircuitPropagator& d_circuit;
 176
 177    public:
 178     IsAssigned(CircuitPropagator& circuit) : d_circuit(circuit) {}
 179
 180     bool operator()(TNode in) const { return d_circuit.isAssigned(in); }
 181   }; /* class IsAssigned */
 182
 183   /** Predicate for use in STL functions. */
 184   class IsAssignedTo : public std::unary_function<TNode, bool>
 185   {
 186     CircuitPropagator& d_circuit;
 187     bool d_value;
 188
 189    public:
 190     IsAssignedTo(CircuitPropagator& circuit, bool value)
 191         : d_circuit(circuit), d_value(value)
 192     {
 193     }
 194
 195     bool operator()(TNode in) const
 196     {
 197       return d_circuit.isAssignedTo(in, d_value);
 198     }
 199   }; /* class IsAssignedTo */
 200
 201   /**
 202    * Assignment status of each node.
 203    */
 204   typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction>
 205       AssignmentMap;
 206
 207   /**
 208    * Assign Node in circuit with the value and add it to the queue; note
 209    * conflicts.
 210    */
 211   void assignAndEnqueue(TNode n,
 212                         bool value,
 213                         std::shared_ptr<ProofNode> proof = nullptr);
 214
 215   /**
 216    * Store a conflict for the case that we have derived both n and n.negate()
 217    * to be true.
 218    */
 219   void makeConflict(Node n);
 220
 221   /**
 222    * Compute the map from nodes to the nodes that use it.
 223    */
 224   void computeBackEdges(TNode node);
 225
 226   /**
 227    * Propagate new information forward in circuit to
 228    * the parents of "in".
 229    */
 230   void propagateForward(TNode child, bool assignment);
 231
 232   /**
 233    * Propagate new information backward in circuit to
 234    * the children of "in".
 235    */
 236   void propagateBackward(TNode parent, bool assignment);
 237
 238   /** Are proofs enabled? */
 239   bool isProofEnabled() const;
 240
 241   context::Context d_context;
 242
 243   /** The propagation queue */
 244   std::vector<TNode> d_propagationQueue;
 245
 246   /**
 247    * We have a propagation queue "clearer" object for when the user
 248    * context pops.  Normally the propagation queue should be empty,
 249    * but this keeps us safe in case there's still some rubbish around
 250    * on the queue.
 251    */
 252   DataClearer<std::vector<TNode>> d_propagationQueueClearer;
 253
 254   /** Are we in conflict? */
 255   context::CDO<TrustNode> d_conflict;
 256
 257   /** Map of substitutions */
 258   std::vector<TrustNode> d_learnedLiterals;
 259
 260   /**
 261    * Similar data clearer for learned literals.
 262    */
 263   DataClearer<std::vector<TrustNode>> d_learnedLiteralClearer;
 264
 265   /**
 266    * Back edges from nodes to where they are used.
 267    */
 268   BackEdgesMap d_backEdges;
 269
 270   /**
 271    * Similar data clearer for back edges.
 272    */
 273   DataClearer<BackEdgesMap> d_backEdgesClearer;
 274
 275   /** Nodes that have been attached already (computed forward edges for) */
 276   // All the nodes we've visited so far
 277   context::CDHashSet<Node, NodeHashFunction> d_seen;
 278
 279   AssignmentMap d_state;
 280
 281   /** Whether to perform forward propagation */
 282   const bool d_forwardPropagation;
 283
 284   /** Whether to perform backward propagation */
 285   const bool d_backwardPropagation;
 286
 287   /* Does the current state require a call to finish()? */
 288   bool d_needsFinish;
 289
 290   /** Adds a new proof for f, or drops it if we already have a proof */
 291   void addProof(TNode f, std::shared_ptr<ProofNode> pf);
 292
 293   /** A pointer to the proof manager */
 294   ProofNodeManager* d_pnm;
 295   /** Eager proof generator that actually stores the proofs */
 296   std::unique_ptr<EagerProofGenerator> d_epg;
 297   /** Connects the proofs to subproofs internally */
 298   std::unique_ptr<LazyCDProofChain> d_proofInternal;
 299   /** Connects the proofs to assumptions externally */
 300   std::unique_ptr<LazyCDProofChain> d_proofExternal;
 301 }; /* class CircuitPropagator */
 302
 303 }  // namespace booleans
 304 }  // namespace theory
 305 }  // namespace CVC4
 306
 307 #endif /* CVC4__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */