Branch data     Line data    Source code

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