Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Andres Noetzli, Morgan Deters
       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                 :            :  * AssertionPipeline stores a list of assertions modified by
      14                 :            :  * preprocessing passes.
      15                 :            :  */
      16                 :            : 
      17                 :            : #include "cvc5_private.h"
      18                 :            : 
      19                 :            : #ifndef CVC5__PREPROCESSING__ASSERTION_PIPELINE_H
      20                 :            : #define CVC5__PREPROCESSING__ASSERTION_PIPELINE_H
      21                 :            : 
      22                 :            : #include <vector>
      23                 :            : 
      24                 :            : #include "expr/node.h"
      25                 :            : #include "proof/lazy_proof.h"
      26                 :            : #include "proof/rewrite_proof_generator.h"
      27                 :            : #include "proof/trust_node.h"
      28                 :            : #include "smt/env_obj.h"
      29                 :            : 
      30                 :            : namespace cvc5::internal {
      31                 :            : 
      32                 :            : class ProofGenerator;
      33                 :            : namespace smt {
      34                 :            : class PreprocessProofGenerator;
      35                 :            : }
      36                 :            : 
      37                 :            : namespace preprocessing {
      38                 :            : 
      39                 :            : using IteSkolemMap = std::unordered_map<size_t, Node>;
      40                 :            : 
      41                 :            : /**
      42                 :            :  * Assertion Pipeline stores a list of assertions modified by preprocessing
      43                 :            :  * passes. It is assumed that all assertions after d_realAssertionsEnd were
      44                 :            :  * generated by ITE removal. Hence, d_iteSkolemMap maps into only these.
      45                 :            :  */
      46                 :            : class AssertionPipeline : protected EnvObj
      47                 :            : {
      48                 :            :  public:
      49                 :            :   AssertionPipeline(Env& env);
      50                 :            : 
      51                 :     523118 :   size_t size() const { return d_nodes.size(); }
      52                 :            : 
      53                 :            :   void resize(size_t n) { d_nodes.resize(n); }
      54                 :            : 
      55                 :            :   /**
      56                 :            :    * Clear the list of assertions and assumptions.
      57                 :            :    */
      58                 :            :   void clear();
      59                 :            : 
      60                 :    5934340 :   const Node& operator[](size_t i) const { return d_nodes[i]; }
      61                 :            : 
      62                 :            :   /**
      63                 :            :    * Adds an assertion/assumption to be preprocessed.
      64                 :            :    *
      65                 :            :    * Note that if proofs are provided, a preprocess pass using this method
      66                 :            :    * is required to either provide a proof generator or a trust id that is not
      67                 :            :    * TrustId::UNKNOWN_PREPROCESS_LEMMA.
      68                 :            :    *
      69                 :            :    * @param n The assertion/assumption
      70                 :            :    * @param isInput If true, n is an input formula (an assumption in the main
      71                 :            :    * body of the overall proof).
      72                 :            :    * @param pg The proof generator who can provide a proof of n. The proof
      73                 :            :    * generator is not required and is ignored if isInput is true.
      74                 :            :    * @param trustId The trust id to use if pg is not provided when isInput
      75                 :            :    * is false and proofs are enabled.
      76                 :            :    */
      77                 :            :   void push_back(Node n,
      78                 :            :                  bool isInput = false,
      79                 :            :                  ProofGenerator* pg = nullptr,
      80                 :            :                  TrustId trustId = TrustId::UNKNOWN_PREPROCESS_LEMMA);
      81                 :            :   /** Same as above, with TrustNode */
      82                 :            :   void pushBackTrusted(TrustNode trn,
      83                 :            :                        TrustId trustId = TrustId::UNKNOWN_PREPROCESS_LEMMA);
      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                 :      87975 :   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                 :     103294 :   IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
     128                 :            :   const IteSkolemMap& getIteSkolemMap() const { return d_iteSkolemMap; }
     129                 :            : 
     130                 :            :   /**
     131                 :            :    * Returns true if substitutions must be stored as assertions. This is for
     132                 :            :    * example the case when we do incremental solving.
     133                 :            :    */
     134                 :      37681 :   bool storeSubstsInAsserts() { return d_storeSubstsInAsserts; }
     135                 :            : 
     136                 :            :   /**
     137                 :            :    * Enables storing substitutions as assertions.
     138                 :            :    */
     139                 :            :   void enableStoreSubstsInAsserts();
     140                 :            : 
     141                 :            :   /**
     142                 :            :    * Disables storing substitutions as assertions.
     143                 :            :    */
     144                 :            :   void disableStoreSubstsInAsserts();
     145                 :            : 
     146                 :            :   /**
     147                 :            :    * Adds a substitution node of the form (= lhs rhs) to the assertions.
     148                 :            :    * This conjoins n to assertions at a distinguished index given by
     149                 :            :    * d_substsIndex.
     150                 :            :    *
     151                 :            :    * @param n The substitution node
     152                 :            :    * @param pg The proof generator that can provide a proof of n.
     153                 :            :    * @param trustId The trust id to use if pg is not provided and proofs are
     154                 :            :    * enabled.
     155                 :            :    */
     156                 :            :   void addSubstitutionNode(Node n,
     157                 :            :                            ProofGenerator* pg = nullptr,
     158                 :            :                            TrustId trustId = TrustId::UNKNOWN_PREPROCESS_LEMMA);
     159                 :            : 
     160                 :            :   /**
     161                 :            :    * Checks whether the assertion at a given index represents substitutions.
     162                 :            :    *
     163                 :            :    * @param i The index in question
     164                 :            :    */
     165                 :            :   bool isSubstsIndex(size_t i) const;
     166                 :            :   /** Is in conflict? True if this pipeline contains the false assertion */
     167                 :    2431770 :   bool isInConflict() const { return d_conflict; }
     168                 :            :   /** Is refutation unsound? */
     169                 :      66829 :   bool isRefutationUnsound() const { return d_isRefutationUnsound; }
     170                 :            :   /** Is model unsound? */
     171                 :      66829 :   bool isModelUnsound() const { return d_isModelUnsound; }
     172                 :            :   /** Is negated? */
     173                 :      50008 :   bool isNegated() const { return d_isNegated; }
     174                 :            :   /** mark refutation unsound */
     175                 :            :   void markRefutationUnsound();
     176                 :            :   /** mark model unsound */
     177                 :            :   void markModelUnsound();
     178                 :            :   /** mark negated */
     179                 :            :   void markNegated();
     180                 :            :   //------------------------------------ for proofs
     181                 :            :   /**
     182                 :            :    * Enable proofs for this assertions pipeline. This must be called
     183                 :            :    * explicitly since we construct the assertions pipeline before we know
     184                 :            :    * whether proofs are enabled.
     185                 :            :    *
     186                 :            :    * @param pppg The preprocess proof generator of the proof manager.
     187                 :            :    */
     188                 :            :   void enableProofs(smt::PreprocessProofGenerator* pppg);
     189                 :            :   /** Is proof enabled? */
     190                 :            :   bool isProofEnabled() const;
     191                 :            :   //------------------------------------ end for proofs
     192                 :            :  private:
     193                 :            :   /** Set that we are in conflict */
     194                 :            :   void markConflict();
     195                 :            :   /** Boolean constants */
     196                 :            :   Node d_true;
     197                 :            :   Node d_false;
     198                 :            :   /** The list of current assertions */
     199                 :            :   std::vector<Node> d_nodes;
     200                 :            : 
     201                 :            :   /**
     202                 :            :    * Map from skolem variables to index in d_assertions containing
     203                 :            :    * corresponding introduced Boolean ite
     204                 :            :    */
     205                 :            :   IteSkolemMap d_iteSkolemMap;
     206                 :            : 
     207                 :            :   /** Size of d_nodes when preprocessing starts */
     208                 :            :   size_t d_realAssertionsEnd;
     209                 :            : 
     210                 :            :   /**
     211                 :            :    * If true, we store the substitutions as assertions. This is necessary when
     212                 :            :    * doing incremental solving because we cannot apply them to existing
     213                 :            :    * assertions while preprocessing new assertions.
     214                 :            :    */
     215                 :            :   bool d_storeSubstsInAsserts;
     216                 :            : 
     217                 :            :   /**
     218                 :            :    * The index of the assertions that holds the substitutions.
     219                 :            :    *
     220                 :            :    * TODO(#2473): replace by separate vector of substitution assertions.
     221                 :            :    */
     222                 :            :   std::unordered_set<size_t> d_substsIndices;
     223                 :            : 
     224                 :            :   /** Index of the first assumption */
     225                 :            :   size_t d_assumptionsStart;
     226                 :            :   /** The number of assumptions */
     227                 :            :   size_t d_numAssumptions;
     228                 :            :   /** The proof generator, if one is provided */
     229                 :            :   smt::PreprocessProofGenerator* d_pppg;
     230                 :            :   /** Are we in conflict? */
     231                 :            :   bool d_conflict;
     232                 :            :   /** Is refutation unsound? */
     233                 :            :   bool d_isRefutationUnsound;
     234                 :            :   /** Is model unsound? */
     235                 :            :   bool d_isModelUnsound;
     236                 :            :   /** Is negated? */
     237                 :            :   bool d_isNegated;
     238                 :            :   /**
     239                 :            :    * Maintains proofs for eliminating top-level AND from inputs to this class.
     240                 :            :    */
     241                 :            :   std::unique_ptr<LazyCDProof> d_andElimEpg;
     242                 :            :   /**
     243                 :            :    * Maintains proofs for rewrite steps.
     244                 :            :    */
     245                 :            :   std::unique_ptr<RewriteProofGenerator> d_rewpg;
     246                 :            : }; /* class AssertionPipeline */
     247                 :            : 
     248                 :            : }  // namespace preprocessing
     249                 :            : }  // namespace cvc5::internal
     250                 :            : 
     251                 :            : #endif /* CVC5__PREPROCESSING__ASSERTION_PIPELINE_H */