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                 :            :  * AssertionPipeline stores a list of assertions modified by
      11                 :            :  * preprocessing passes.
      12                 :            :  */
      13                 :            : 
      14                 :            : #include "cvc5_private.h"
      15                 :            : 
      16                 :            : #ifndef CVC5__PREPROCESSING__ASSERTION_PIPELINE_H
      17                 :            : #define CVC5__PREPROCESSING__ASSERTION_PIPELINE_H
      18                 :            : 
      19                 :            : #include <vector>
      20                 :            : 
      21                 :            : #include "expr/node.h"
      22                 :            : #include "proof/lazy_proof.h"
      23                 :            : #include "proof/rewrite_proof_generator.h"
      24                 :            : #include "proof/trust_node.h"
      25                 :            : #include "smt/env_obj.h"
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : 
      29                 :            : class ProofGenerator;
      30                 :            : namespace smt {
      31                 :            : class PreprocessProofGenerator;
      32                 :            : }
      33                 :            : 
      34                 :            : namespace preprocessing {
      35                 :            : 
      36                 :            : using IteSkolemMap = std::unordered_map<size_t, Node>;
      37                 :            : 
      38                 :            : /**
      39                 :            :  * Assertion Pipeline stores a list of assertions modified by preprocessing
      40                 :            :  * passes. It is assumed that all assertions after d_realAssertionsEnd were
      41                 :            :  * generated by ITE removal. Hence, d_iteSkolemMap maps into only these.
      42                 :            :  */
      43                 :            : class AssertionPipeline : protected EnvObj
      44                 :            : {
      45                 :            :  public:
      46                 :            :   AssertionPipeline(Env& env);
      47                 :            : 
      48                 :     352146 :   size_t size() const { return d_nodes.size(); }
      49                 :            : 
      50                 :          2 :   void resize(size_t n) { d_nodes.resize(n); }
      51                 :            : 
      52                 :            :   /**
      53                 :            :    * Clear the list of assertions and assumptions.
      54                 :            :    */
      55                 :            :   void clear();
      56                 :            : 
      57                 :    5306799 :   const Node& operator[](size_t i) const { return d_nodes[i]; }
      58                 :            : 
      59                 :            :   /**
      60                 :            :    * Adds an assertion/assumption to be preprocessed.
      61                 :            :    *
      62                 :            :    * Note that if proofs are provided, a preprocess pass using this method
      63                 :            :    * is required to either provide a proof generator or a trust id that is not
      64                 :            :    * TrustId::UNKNOWN_PREPROCESS_LEMMA.
      65                 :            :    *
      66                 :            :    * @param n The assertion/assumption
      67                 :            :    * @param isInput If true, n is an input formula (an assumption in the main
      68                 :            :    * body of the overall proof).
      69                 :            :    * @param pg The proof generator who can provide a proof of n. The proof
      70                 :            :    * generator is not required and is ignored if isInput is true.
      71                 :            :    * @param trustId The trust id to use if pg is not provided when isInput
      72                 :            :    * is false and proofs are enabled.
      73                 :            :    * @param ensureRew If true, we rewrite all assertions added in this call.
      74                 :            :    */
      75                 :            :   void push_back(Node n,
      76                 :            :                  bool isInput = false,
      77                 :            :                  ProofGenerator* pg = nullptr,
      78                 :            :                  TrustId trustId = TrustId::UNKNOWN_PREPROCESS_LEMMA,
      79                 :            :                  bool ensureRew = false);
      80                 :            :   /** Same as above, with TrustNode */
      81                 :            :   void pushBackTrusted(TrustNode trn,
      82                 :            :                        TrustId trustId = TrustId::UNKNOWN_PREPROCESS_LEMMA,
      83                 :            :                        bool ensureRew = false);
      84                 :            : 
      85                 :            :   /**
      86                 :            :    * Get the constant reference to the underlying assertions. It is only
      87                 :            :    * possible to modify these via the replace methods below.
      88                 :            :    */
      89                 :      48639 :   const std::vector<Node>& ref() const { return d_nodes; }
      90                 :            : 
      91                 :         14 :   std::vector<Node>::const_iterator begin() const { return d_nodes.cbegin(); }
      92                 :         28 :   std::vector<Node>::const_iterator end() const { return d_nodes.cend(); }
      93                 :            : 
      94                 :            :   /*
      95                 :            :    * Replaces assertion i with node n and records the dependency between the
      96                 :            :    * original assertion and its replacement.
      97                 :            :    *
      98                 :            :    * Note that if proofs are provided, a preprocess pass using this method
      99                 :            :    * is required to either provide a proof generator or a trust id that is not
     100                 :            :    * TrustId::UNKNOWN_PREPROCESS_LEMMA.
     101                 :            :    *
     102                 :            :    * @param i The position of the assertion to replace.
     103                 :            :    * @param n The replacement assertion.
     104                 :            :    * @param pg The proof generator who can provide a proof of d_nodes[i] == n,
     105                 :            :    * where d_nodes[i] is the assertion at position i prior to this call.
     106                 :            :    * @param trustId The trust id to use if pg is not provided and proofs are
     107                 :            :    * enabled.
     108                 :            :    */
     109                 :            :   void replace(size_t i,
     110                 :            :                Node n,
     111                 :            :                ProofGenerator* pg = nullptr,
     112                 :            :                TrustId trustId = TrustId::UNKNOWN_PREPROCESS);
     113                 :            :   /**
     114                 :            :    * Same as above, with TrustNode trn, which is of kind REWRITE and proves
     115                 :            :    * d_nodes[i] = n for some n.
     116                 :            :    */
     117                 :            :   void replaceTrusted(size_t i,
     118                 :            :                       TrustNode trn,
     119                 :            :                       TrustId trustId = TrustId::UNKNOWN_PREPROCESS);
     120                 :            :   /**
     121                 :            :    * Ensure assertion at index i is rewritten. If it is not already in
     122                 :            :    * rewritten form, the assertion is replaced by its rewritten form.
     123                 :            :    * @param i The index of the assertion.
     124                 :            :    */
     125                 :            :   void ensureRewritten(size_t i);
     126                 :            : 
     127                 :      64596 :   IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
     128                 :            :   const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
     129                 :            :   /** Remove all ITE-removal map entries for skolem, if any exist. */
     130                 :            :   void removeIteSkolem(TNode skolem);
     131                 :            : 
     132                 :            :   /**
     133                 :            :    * Returns true if substitutions must be stored as assertions. This is for
     134                 :            :    * example the case when we do incremental solving.
     135                 :            :    */
     136                 :      25479 :   bool storeSubstsInAsserts() { return d_storeSubstsInAsserts; }
     137                 :            : 
     138                 :            :   /**
     139                 :            :    * Enables storing substitutions as assertions.
     140                 :            :    */
     141                 :            :   void enableStoreSubstsInAsserts();
     142                 :            : 
     143                 :            :   /**
     144                 :            :    * Disables storing substitutions as assertions.
     145                 :            :    */
     146                 :            :   void disableStoreSubstsInAsserts();
     147                 :            : 
     148                 :            :   /**
     149                 :            :    * Adds a substitution node of the form (= lhs rhs) to the assertions.
     150                 :            :    * This conjoins n to assertions at a distinguished index given by
     151                 :            :    * d_substsIndex.
     152                 :            :    *
     153                 :            :    * @param n The substitution node
     154                 :            :    * @param pg The proof generator that can provide a proof of n.
     155                 :            :    * @param trustId The trust id to use if pg is not provided and proofs are
     156                 :            :    * enabled.
     157                 :            :    */
     158                 :            :   void addSubstitutionNode(Node n,
     159                 :            :                            ProofGenerator* pg = nullptr,
     160                 :            :                            TrustId trustId = TrustId::UNKNOWN_PREPROCESS_LEMMA);
     161                 :            : 
     162                 :            :   /**
     163                 :            :    * Checks whether the assertion at a given index represents substitutions.
     164                 :            :    *
     165                 :            :    * @param i The index in question
     166                 :            :    */
     167                 :            :   bool isSubstsIndex(size_t i) const;
     168                 :            :   /** Is in conflict? True if this pipeline contains the false assertion */
     169                 :    2135192 :   bool isInConflict() const { return d_conflict; }
     170                 :            :   /** Is refutation unsound? */
     171                 :      40208 :   bool isRefutationUnsound() const { return d_isRefutationUnsound; }
     172                 :            :   /** Is model unsound? */
     173                 :      40208 :   bool isModelUnsound() const { return d_isModelUnsound; }
     174                 :            :   /** Is negated? */
     175                 :      31644 :   bool isNegated() const { return d_isNegated; }
     176                 :            :   /** mark refutation unsound */
     177                 :            :   void markRefutationUnsound();
     178                 :            :   /** mark model unsound */
     179                 :            :   void markModelUnsound();
     180                 :            :   /** mark negated */
     181                 :            :   void markNegated();
     182                 :            :   //------------------------------------ for proofs
     183                 :            :   /**
     184                 :            :    * Enable proofs for this assertions pipeline. This must be called
     185                 :            :    * explicitly since we construct the assertions pipeline before we know
     186                 :            :    * whether proofs are enabled.
     187                 :            :    *
     188                 :            :    * @param pppg The preprocess proof generator of the proof manager.
     189                 :            :    */
     190                 :            :   void enableProofs(smt::PreprocessProofGenerator* pppg);
     191                 :            :   /** Is proof enabled? */
     192                 :            :   bool isProofEnabled() const;
     193                 :            :   //------------------------------------ end for proofs
     194                 :            :  private:
     195                 :            :   /** Set that we are in conflict */
     196                 :            :   void markConflict();
     197                 :            :   /** Boolean constants */
     198                 :            :   Node d_true;
     199                 :            :   Node d_false;
     200                 :            :   /** The list of current assertions */
     201                 :            :   std::vector<Node> d_nodes;
     202                 :            : 
     203                 :            :   /**
     204                 :            :    * Map from skolem variables to index in d_assertions containing
     205                 :            :    * corresponding introduced Boolean ite
     206                 :            :    */
     207                 :            :   IteSkolemMap d_iteSkolemMap;
     208                 :            : 
     209                 :            :   /**
     210                 :            :    * If true, we store the substitutions as assertions. This is necessary when
     211                 :            :    * doing incremental solving because we cannot apply them to existing
     212                 :            :    * assertions while preprocessing new assertions.
     213                 :            :    */
     214                 :            :   bool d_storeSubstsInAsserts;
     215                 :            : 
     216                 :            :   /**
     217                 :            :    * The index of the assertions that holds the substitutions.
     218                 :            :    *
     219                 :            :    * TODO(#2473): replace by separate vector of substitution assertions.
     220                 :            :    */
     221                 :            :   std::unordered_set<size_t> d_substsIndices;
     222                 :            : 
     223                 :            :   /** The proof generator, if one is provided */
     224                 :            :   smt::PreprocessProofGenerator* d_pppg;
     225                 :            :   /** Are we in conflict? */
     226                 :            :   bool d_conflict;
     227                 :            :   /** Is refutation unsound? */
     228                 :            :   bool d_isRefutationUnsound;
     229                 :            :   /** Is model unsound? */
     230                 :            :   bool d_isModelUnsound;
     231                 :            :   /** Is negated? */
     232                 :            :   bool d_isNegated;
     233                 :            :   /**
     234                 :            :    * Maintains proofs for eliminating top-level AND from inputs to this class.
     235                 :            :    */
     236                 :            :   std::unique_ptr<LazyCDProof> d_andElimEpg;
     237                 :            :   /**
     238                 :            :    * Maintains proofs for rewrite steps.
     239                 :            :    */
     240                 :            :   std::unique_ptr<RewriteProofGenerator> d_rewpg;
     241                 :            : }; /* class AssertionPipeline */
     242                 :            : 
     243                 :            : }  // namespace preprocessing
     244                 :            : }  // namespace cvc5::internal
     245                 :            : 
     246                 :            : #endif /* CVC5__PREPROCESSING__ASSERTION_PIPELINE_H */