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,
      68                 :            :                     bool enableForward = true,
      69                 :            :                     bool enableBackward = true);
      70                 :            : 
      71                 :            :   /** Get Node assignment in circuit.  Assert-fails if Node is unassigned. */
      72                 :     572513 :   bool getAssignment(TNode n) const
      73                 :            :   {
      74                 :     572513 :     AssignmentMap::iterator i = d_state.find(n);
      75 [ +  - ][ +  - ]:     572513 :     Assert(i != d_state.end() && (*i).second != UNASSIGNED);
         [ -  + ][ -  + ]
                 [ -  - ]
      76                 :     572513 :     return (*i).second == ASSIGNED_TO_TRUE;
      77                 :            :   }
      78                 :            : 
      79                 :            :   // Use custom context to ensure propagator is reset after use
      80                 :            :   void initialize();
      81                 :            : 
      82                 :      29315 :   std::vector<TrustNode>& getLearnedLiterals() { return d_learnedLiterals; }
      83                 :            : 
      84                 :            :   /** Assert for propagation */
      85                 :            :   void assertTrue(TNode assertion);
      86                 :            : 
      87                 :            :   /**
      88                 :            :    * Propagate through the asserted circuit propagator. New information
      89                 :            :    * discovered by the propagator are put in the substitutions vector used in
      90                 :            :    * construction.
      91                 :            :    *
      92                 :            :    * @return a trust node encapsulating the proof for a conflict as a lemma that
      93                 :            :    * proves false, or the null trust node otherwise
      94                 :            :    */
      95                 :            :   CVC5_WARN_UNUSED_RESULT TrustNode propagate();
      96                 :            : 
      97                 :            :   /**
      98                 :            :    * Get the back edges of this circuit.
      99                 :            :    */
     100                 :        192 :   const BackEdgesMap& getBackEdges() const { return d_backEdges; }
     101                 :            : 
     102                 :            :   /** Invert a set value */
     103                 :            :   static inline AssignmentStatus neg(AssignmentStatus value)
     104                 :            :   {
     105                 :            :     Assert(value != UNASSIGNED);
     106                 :            :     if (value == ASSIGNED_TO_TRUE)
     107                 :            :       return ASSIGNED_TO_FALSE;
     108                 :            :     else
     109                 :            :       return ASSIGNED_TO_TRUE;
     110                 :            :   }
     111                 :            : 
     112                 :            :   /** True iff Node is assigned in circuit (either true or false). */
     113                 :      33962 :   bool isAssigned(TNode n) const
     114                 :            :   {
     115                 :      33962 :     AssignmentMap::const_iterator i = d_state.find(n);
     116 [ +  + ][ +  - ]:      33962 :     return i != d_state.end() && ((*i).second != UNASSIGNED);
     117                 :            :   }
     118                 :            : 
     119                 :            :   /** True iff Node is assigned to the value. */
     120                 :   16793838 :   bool isAssignedTo(TNode n, bool value) const
     121                 :            :   {
     122                 :   16793838 :     AssignmentMap::const_iterator i = d_state.find(n);
     123         [ +  + ]:   16793838 :     if (i == d_state.end()) return false;
     124 [ +  + ][ +  + ]:   16230998 :     if (value && ((*i).second == ASSIGNED_TO_TRUE)) return true;
                 [ +  + ]
     125 [ +  + ][ +  + ]:    1231218 :     if (!value && ((*i).second == ASSIGNED_TO_FALSE)) return true;
                 [ +  + ]
     126                 :      50493 :     return false;
     127                 :            :   }
     128                 :            :   /**
     129                 :            :    * Enable proofs based on context and parent proof generator.
     130                 :            :    *
     131                 :            :    * If parent is non-null, then it is responsible for the proofs provided
     132                 :            :    * to this class.
     133                 :            :    */
     134                 :            :   void enableProofs(context::Context* ctx, ProofGenerator* defParent);
     135                 :            : 
     136                 :            :  private:
     137                 :            :   /** A context-notify object that clears out stale data. */
     138                 :            :   template <class T>
     139                 :            :   class DataClearer : context::ContextNotifyObj
     140                 :            :   {
     141                 :            :    public:
     142                 :     120525 :     DataClearer(context::Context* context, T& data)
     143                 :     120525 :         : context::ContextNotifyObj(context), d_data(data)
     144                 :            :     {
     145                 :     120525 :     }
     146                 :            : 
     147                 :            :    protected:
     148                 :      15045 :     void contextNotifyPop() override
     149                 :            :     {
     150         [ +  - ]:      30090 :       Trace("circuit-prop")
     151                 :          0 :           << "CircuitPropagator::DataClearer: clearing data "
     152                 :      15045 :           << "(size was " << d_data.size() << ")" << std::endl;
     153                 :      15045 :       d_data.clear();
     154                 :      15045 :     }
     155                 :            : 
     156                 :            :    private:
     157                 :            :     T& d_data;
     158                 :            :   }; /* class DataClearer<T> */
     159                 :            : 
     160                 :            :   /**
     161                 :            :    * Assignment status of each node.
     162                 :            :    */
     163                 :            :   typedef context::CDHashMap<TNode, AssignmentStatus> AssignmentMap;
     164                 :            : 
     165                 :            :   /**
     166                 :            :    * Assign Node in circuit with the value and add it to the queue; note
     167                 :            :    * conflicts.
     168                 :            :    */
     169                 :            :   void assignAndEnqueue(TNode n,
     170                 :            :                         bool value,
     171                 :            :                         std::shared_ptr<ProofNode> proof = nullptr);
     172                 :            : 
     173                 :            :   /**
     174                 :            :    * Store a conflict for the case that we have derived both n and n.negate()
     175                 :            :    * to be true.
     176                 :            :    */
     177                 :            :   void makeConflict(Node n);
     178                 :            : 
     179                 :            :   /**
     180                 :            :    * Compute the map from nodes to the nodes that use it.
     181                 :            :    */
     182                 :            :   void computeBackEdges(TNode node);
     183                 :            : 
     184                 :            :   /**
     185                 :            :    * Propagate new information forward in circuit to
     186                 :            :    * the parents of "in".
     187                 :            :    */
     188                 :            :   void propagateForward(TNode child, bool assignment);
     189                 :            : 
     190                 :            :   /**
     191                 :            :    * Propagate new information backward in circuit to
     192                 :            :    * the children of "in".
     193                 :            :    */
     194                 :            :   void propagateBackward(TNode parent, bool assignment);
     195                 :            : 
     196                 :            :   /** Are proofs enabled? */
     197                 :            :   bool isProofEnabled() const;
     198                 :            : 
     199                 :            :   context::Context d_context;
     200                 :            : 
     201                 :            :   /** The propagation queue */
     202                 :            :   std::vector<TNode> d_propagationQueue;
     203                 :            : 
     204                 :            :   /**
     205                 :            :    * We have a propagation queue "clearer" object for when the user
     206                 :            :    * context pops.  Normally the propagation queue should be empty,
     207                 :            :    * but this keeps us safe in case there's still some rubbish around
     208                 :            :    * on the queue.
     209                 :            :    */
     210                 :            :   DataClearer<std::vector<TNode>> d_propagationQueueClearer;
     211                 :            : 
     212                 :            :   /** Are we in conflict? */
     213                 :            :   context::CDO<TrustNode> d_conflict;
     214                 :            : 
     215                 :            :   /** Map of substitutions */
     216                 :            :   std::vector<TrustNode> d_learnedLiterals;
     217                 :            : 
     218                 :            :   /**
     219                 :            :    * Similar data clearer for learned literals.
     220                 :            :    */
     221                 :            :   DataClearer<std::vector<TrustNode>> d_learnedLiteralClearer;
     222                 :            : 
     223                 :            :   /**
     224                 :            :    * Back edges from nodes to where they are used.
     225                 :            :    */
     226                 :            :   BackEdgesMap d_backEdges;
     227                 :            : 
     228                 :            :   /**
     229                 :            :    * Similar data clearer for back edges.
     230                 :            :    */
     231                 :            :   DataClearer<BackEdgesMap> d_backEdgesClearer;
     232                 :            : 
     233                 :            :   /** Nodes that have been attached already (computed forward edges for) */
     234                 :            :   // All the nodes we've visited so far
     235                 :            :   context::CDHashSet<Node> d_seen;
     236                 :            : 
     237                 :            :   AssignmentMap d_state;
     238                 :            : 
     239                 :            :   /** Whether to perform forward propagation */
     240                 :            :   const bool d_forwardPropagation;
     241                 :            : 
     242                 :            :   /** Whether to perform backward propagation */
     243                 :            :   const bool d_backwardPropagation;
     244                 :            : 
     245                 :            :   /* Does the current state require a call to finish()? */
     246                 :            :   bool d_needsFinish;
     247                 :            : 
     248                 :            :   /** Adds a new proof for f, or drops it if we already have a proof */
     249                 :            :   void addProof(TNode f, std::shared_ptr<ProofNode> pf);
     250                 :            : 
     251                 :            :   /** Eager proof generator that actually stores the proofs */
     252                 :            :   std::unique_ptr<EagerProofGenerator> d_epg;
     253                 :            :   /** Connects the proofs to subproofs internally */
     254                 :            :   std::unique_ptr<LazyCDProofChain> d_proofInternal;
     255                 :            :   /** Connects the proofs to assumptions externally */
     256                 :            :   std::unique_ptr<LazyCDProofChain> d_proofExternal;
     257                 :            : }; /* class CircuitPropagator */
     258                 :            : 
     259                 :            : }  // namespace booleans
     260                 :            : }  // namespace theory
     261                 :            : }  // namespace cvc5::internal
     262                 :            : 
     263                 :            : #endif /* CVC5__THEORY__BOOLEANS__CIRCUIT_PROPAGATOR_H */