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                 :            :  * proof rewrite rule class
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_private.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__REWRITER__REWRITE_PROOF_RULE__H
      16                 :            : #define CVC5__REWRITER__REWRITE_PROOF_RULE__H
      17                 :            : 
      18                 :            : #include <string>
      19                 :            : #include <unordered_set>
      20                 :            : #include <vector>
      21                 :            : 
      22                 :            : #include "expr/nary_match_trie.h"
      23                 :            : #include "expr/node.h"
      24                 :            : #include "rewriter/rewrites.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : namespace rewriter {
      28                 :            : 
      29                 :            : /**
      30                 :            :  * The level for a rewrite, which determines which proof signature they are a
      31                 :            :  * part of.
      32                 :            :  */
      33                 :            : enum class Level
      34                 :            : {
      35                 :            :   NORMAL,
      36                 :            :   EXPERT,
      37                 :            : };
      38                 :            : 
      39                 :            : /**
      40                 :            :  * The definition of a (conditional) rewrite rule. An instance of this
      41                 :            :  * class is generated for each DSL rule provided in the rewrite files. The
      42                 :            :  * interface of this class is used by the proof reconstruction algorithm.
      43                 :            :  */
      44                 :            : class RewriteProofRule
      45                 :            : {
      46                 :            :  public:
      47                 :            :   RewriteProofRule();
      48                 :            :   /**
      49                 :            :    * Initialize this rule.
      50                 :            :    * @param id The identifier of this rule
      51                 :            :    * @param userFvs The (user-provided) free variable list of the rule. This
      52                 :            :    * is used only to track the original names of the arguments to the rule.
      53                 :            :    * @param fvs The internal free variable list of the rule. Notice these
      54                 :            :    * variables are normalized such that *all* proof rules use the same
      55                 :            :    * variables, per type. In detail, the n^th argument left-to-right of a given
      56                 :            :    * type T is the same for all rules. This is to facilitate parallel matching.
      57                 :            :    * @param cond The conditions of the rule, normalized to fvs.
      58                 :            :    * @param conc The conclusion of the rule, which is an equality of the form
      59                 :            :    * (= t s), where t is specified as rewriting to s. This equality is
      60                 :            :    * normalized to fvs.
      61                 :            :    * @param context The term context for the conclusion of the rule. This is
      62                 :            :    * non-null for all rules that should be applied to fixed-point. The context
      63                 :            :    * is a lambda term that specifies the next position of the term to rewrite.
      64                 :            :    * @param _level The level of the rewrite, which determines which proof
      65                 :            :    * signature they should be added to (normal or expert).
      66                 :            :    */
      67                 :            :   void init(ProofRewriteRule id,
      68                 :            :             const std::vector<Node>& userFvs,
      69                 :            :             const std::vector<Node>& fvs,
      70                 :            :             const std::vector<Node>& cond,
      71                 :            :             Node conc,
      72                 :            :             Node context,
      73                 :            :             Level _level);
      74                 :            :   /** get id */
      75                 :            :   ProofRewriteRule getId() const;
      76                 :            :   /** get name */
      77                 :            :   const char* getName() const;
      78                 :            :   /** Get user variable list */
      79                 :            :   const std::vector<Node>& getUserVarList() const;
      80                 :            :   /** Get variable list */
      81                 :            :   const std::vector<Node>& getVarList() const;
      82                 :            :   /** The context that the rule is applied in */
      83                 :      25309 :   Node getContext() const { return d_context; }
      84                 :            :   /**
      85                 :            :    * Get path to context variable, for example if
      86                 :            :    * d_context is (lambda x (f a (g x b))), then d_pathToCtx = [1,0].
      87                 :            :    */
      88                 :       2287 :   const std::vector<size_t> getPathToContextVar() const { return d_pathToCtx; }
      89                 :            :   /**
      90                 :            :    * Does the statement of this rule mention an indexed operator whose indices
      91                 :            :    * are given as explicit arguments (APPLY_INDEXED_SYMBOLIC)? If so, instances
      92                 :            :    * of this rule must be folded when constructing proofs, since such terms
      93                 :            :    * have no counterpart in external proof formats.
      94                 :            :    */
      95                 :            :   bool hasIndexedOperator() const;
      96                 :            :   /** Does this rule have conditions? */
      97                 :            :   bool hasConditions() const;
      98                 :            :   /** Get (declared) conditions */
      99                 :            :   const std::vector<Node>& getConditions() const;
     100                 :            :   /**
     101                 :            :    * Get the conditions of the rule under the substitution { vs -> ss }.
     102                 :            :    */
     103                 :            :   bool getObligations(const std::vector<Node>& vs,
     104                 :            :                       const std::vector<Node>& ss,
     105                 :            :                       std::vector<Node>& vcs) const;
     106                 :            :   /**
     107                 :            :    * Check match, return true if h matches the head of this rule; notifies
     108                 :            :    * the match notify object ntm.
     109                 :            :    *
     110                 :            :    * Note this method is not run as the main matching algorithm for rewrite
     111                 :            :    * proof reconstruction, which considers all rules in parallel. This method
     112                 :            :    * can be used for debugging matches of h against the head of this rule.
     113                 :            :    */
     114                 :            :   void getMatches(Node h, expr::NotifyMatch* ntm) const;
     115                 :            :   /**
     116                 :            :    * Get (uninstantiated) conclusion of the rule.
     117                 :            :    * @param includeContext If we should include the context of this rule (if
     118                 :            :    * the RARE rule is given a "context" as described in the constructor).
     119                 :            :    * @return The (uninstantiated) conclusion of the rule.
     120                 :            :    */
     121                 :            :   Node getConclusion(bool includeContext = false) const;
     122                 :            :   /**
     123                 :            :    * Get conclusion of the rule for the substituted terms ss for the variables
     124                 :            :    * v = getVarList() of this rule.
     125                 :            :    *
     126                 :            :    * @param ss The terms to substitute in this rule. Each ss[i] is the same sort
     127                 :            :    * as v[i] if v[i] is not a list variable, or is an SEXPR if v[i] is a list
     128                 :            :    * variable,
     129                 :            :    * @return the substituted conclusion of the rule.
     130                 :            :    */
     131                 :            :   Node getConclusionFor(const std::vector<Node>& ss) const;
     132                 :            :   /**
     133                 :            :    * Get conclusion of the rule for the substituted terms ss.
     134                 :            :    * Additionally computes the "witness term" for each variable in the rule
     135                 :            :    * which gives the corresponding term.
     136                 :            :    * In particular, for each v[i] where v = getVarList(),
     137                 :            :    * witnessTerms[i] is either:
     138                 :            :    * (UNDEFINED_KIND, {t}), specifying that v -> t,
     139                 :            :    * (k, {t1...tn}), specifying that v -> (<k> t1 ... tn).
     140                 :            :    * Note that we don't construct (<k> t1 ... tn) since it may be illegal to
     141                 :            :    * do so if e.g. k=or, and n=1 due to restrictions on the arity of Kinds.
     142                 :            :    *
     143                 :            :    * @param ss The terms to substitute in this rule. Each ss[i] is the same sort
     144                 :            :    * as v[i] if v[i] is not a list variable, or is an SEXPR if v[i] is a list
     145                 :            :    * variable,
     146                 :            :    * @param witnessTerms The computed witness terms for each variable of this
     147                 :            :    * rule.
     148                 :            :    * @return the substituted conclusion of the rule.
     149                 :            :    */
     150                 :            :   Node getConclusionFor(
     151                 :            :       const std::vector<Node>& ss,
     152                 :            :       std::vector<std::pair<Kind, std::vector<Node>>>& witnessTerms) const;
     153                 :            :   /**
     154                 :            :    * @return the list of applications of Kind::TYPE_OF that appear in the
     155                 :            :    * conclusion or a premise. These require special handling by the
     156                 :            :    * printer.
     157                 :            :    */
     158                 :            :   std::vector<Node> getExplicitTypeOfList() const;
     159                 :            :   /**
     160                 :            :    * Is variable explicit? An explicit variable is one that does not occur
     161                 :            :    * in a condition and thus its value must be specified in a proof
     162                 :            :    * in languages that allow for implicit/unspecified hole arguments.
     163                 :            :    */
     164                 :            :   bool isExplicitVar(Node v) const;
     165                 :            :   /**
     166                 :            :    * Get list context. This returns the parent kind of the list variable v.
     167                 :            :    * For example, for
     168                 :            :    *   (define-rule bool-or-true ((xs Bool :list) (ys Bool :list))
     169                 :            :    *      (or xs true ys) true)
     170                 :            :    * The variable xs has list context `OR`.
     171                 :            :    *
     172                 :            :    * If v is in an ambiguous context, an exception will have been thrown
     173                 :            :    * in the constructor of this class.
     174                 :            :    *
     175                 :            :    * This method returns UNDEFINED_KIND if there is no list context for v,
     176                 :            :    * e.g. if v is not a list variable.
     177                 :            :    */
     178                 :            :   Kind getListContext(Node v) const;
     179                 :            :   /** Was this rule marked as being applied to fixed point? */
     180                 :            :   bool isFixedPoint() const;
     181                 :            :   /**
     182                 :            :    * Get condition definitions given an application vs -> ss of this rule.
     183                 :            :    * This is used to handle variables that do not occur in the left hand side
     184                 :            :    * of rewrite rules and are defined in conditions of this rule.
     185                 :            :    * @param vs The matched variables of this rule.
     186                 :            :    * @param ss The terms to substitute in this rule for each vs.
     187                 :            :    * @param dvs The variables for which a definition can now be inferred.
     188                 :            :    * @param dss The terms that each dvs are defined as, for each dvs.
     189                 :            :    */
     190                 :            :   void getConditionalDefinitions(const std::vector<Node>& vs,
     191                 :            :                                  const std::vector<Node>& ss,
     192                 :            :                                  std::vector<Node>& dvs,
     193                 :            :                                  std::vector<Node>& dss) const;
     194                 :            :   /** Get the signature level for the rewrite rule */
     195                 :            :   Level getSignatureLevel() const;
     196                 :            : 
     197                 :            :  private:
     198                 :            :   /** The id of the rule */
     199                 :            :   ProofRewriteRule d_id;
     200                 :            :   /** The conditions of the rule */
     201                 :            :   std::vector<Node> d_cond;
     202                 :            :   /** The conclusion of the rule (an equality) */
     203                 :            :   Node d_conc;
     204                 :            :   /** Is the rule applied in some fixed point context? */
     205                 :            :   Node d_context;
     206                 :            :   /** The level */
     207                 :            :   Level d_level;
     208                 :            :   /** the ordered list of free variables, provided by the user */
     209                 :            :   std::vector<Node> d_userFvs;
     210                 :            :   /** the ordered list of free variables */
     211                 :            :   std::vector<Node> d_fvs;
     212                 :            :   /** number of free variables */
     213                 :            :   size_t d_numFv;
     214                 :            :   /** Whether this rule mentions an indexed operator, see above */
     215                 :            :   bool d_hasIndexedOp;
     216                 :            :   /**
     217                 :            :    * The free variables that do not occur in the conditions. These cannot be
     218                 :            :    * "holes" in a proof.
     219                 :            :    */
     220                 :            :   std::unordered_set<Node> d_noOccVars;
     221                 :            :   /** Maps variables to the term they are defined to be */
     222                 :            :   std::map<Node, Node> d_condDefinedVars;
     223                 :            :   /** The context for list variables (see expr::getListVarContext). */
     224                 :            :   std::map<Node, Node> d_listVarCtx;
     225                 :            :   /** The match trie (for fixed point matching) */
     226                 :            :   expr::NaryMatchTrie d_mt;
     227                 :            :   /** Path to context variable */
     228                 :            :   std::vector<size_t> d_pathToCtx;
     229                 :            : };
     230                 :            : 
     231                 :            : }  // namespace rewriter
     232                 :            : }  // namespace cvc5::internal
     233                 :            : 
     234                 :            : #endif /* CVC5__REWRITER__REWRITE_PROOF_RULE__H */