Branch data     Line data    Source code

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