Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Andrew Reynolds, Mathias Preiner, Aina Niemetz
       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                 :            :  * Utilities for skolemization.
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #ifndef CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H
      19                 :            : #define CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H
      20                 :            : 
      21                 :            : #include <unordered_map>
      22                 :            : #include <unordered_set>
      23                 :            : 
      24                 :            : #include "context/cdhashmap.h"
      25                 :            : #include "expr/node.h"
      26                 :            : #include "expr/type_node.h"
      27                 :            : #include "proof/eager_proof_generator.h"
      28                 :            : #include "proof/trust_node.h"
      29                 :            : #include "smt/env_obj.h"
      30                 :            : 
      31                 :            : namespace cvc5::internal {
      32                 :            : 
      33                 :            : class DTypeConstructor;
      34                 :            : 
      35                 :            : namespace theory {
      36                 :            : namespace quantifiers {
      37                 :            : 
      38                 :            : class QuantifiersState;
      39                 :            : class TermRegistry;
      40                 :            : 
      41                 :            : /** Skolemization utility
      42                 :            :  *
      43                 :            :  * This class constructs Skolemization lemmas.
      44                 :            :  * Given a quantified formula q = (forall x. P),
      45                 :            :  * its skolemization lemma is of the form:
      46                 :            :  *   (~ forall x. P ) => ~P * { x -> d_skolem_constants[q] }
      47                 :            :  *
      48                 :            :  * This class also incorporates techniques for
      49                 :            :  * skolemization with "inductive strenghtening", see
      50                 :            :  * Section 2 of Reynolds et al., "Induction for SMT
      51                 :            :  * Solvers", VMCAI 2015. In the case that x is an inductive
      52                 :            :  * datatype or an integer, then we may strengthen the conclusion
      53                 :            :  * based on weak well-founded induction. For example, for
      54                 :            :  * quantification on lists, a skolemization with inductive
      55                 :            :  * strengthening is a lemma of this form:
      56                 :            :  *   (~ forall x : List. P( x ) ) =>
      57                 :            :  *   ~P( k ) ^ ( is-cons( k ) => P( tail( k ) ) )
      58                 :            :  * For the integers it is:
      59                 :            :  *   (~ forall x : Int. P( x ) ) =>
      60                 :            :  *   ~P( k ) ^ ( x>0 => P( x-1 ) )
      61                 :            :  *
      62                 :            :  *
      63                 :            :  * Inductive strenghtening is not enabled by
      64                 :            :  * default and can be enabled by option:
      65                 :            :  *   --quant-ind
      66                 :            :  */
      67                 :            : class Skolemize : protected EnvObj
      68                 :            : {
      69                 :            :   typedef context::CDHashMap<Node, Node> NodeNodeMap;
      70                 :            : 
      71                 :            :  public:
      72                 :            :   Skolemize(Env& env, QuantifiersState& qs, TermRegistry& tr);
      73                 :      99032 :   ~Skolemize() {}
      74                 :            :   /** skolemize quantified formula q
      75                 :            :    * If the return value ret of this function is non-null, then ret is a trust
      76                 :            :    * node corresponding to a new skolemization lemma we generated for q. These
      77                 :            :    * lemmas are constructed once per user-context.
      78                 :            :    */
      79                 :            :   TrustNode process(Node q);
      80                 :            :   /** get the skolem constants */
      81                 :            :   static std::vector<Node> getSkolemConstants(const Node& q);
      82                 :            :   /** get the i^th skolem constant for quantified formula q */
      83                 :            :   static Node getSkolemConstant(const Node& q, size_t i);
      84                 :            :   /** make skolemized body
      85                 :            :    *
      86                 :            :    * This returns the skolemized body n of a
      87                 :            :    * quantified formula q with inductive strenghtening,
      88                 :            :    * where typically n is q[1].
      89                 :            :    *
      90                 :            :    * The skolem constants/functions we generate by this
      91                 :            :    * skolemization are added to sk.
      92                 :            :    *
      93                 :            :    * The argument fvs are used if we are
      94                 :            :    * performing skolemization within a nested quantified
      95                 :            :    * formula. In this case, skolem constants we introduce
      96                 :            :    * must be parameterized based on the types of fvs and must be
      97                 :            :    * applied to fvs.
      98                 :            :    *
      99                 :            :    * The last two arguments sub and sub_vars are used for
     100                 :            :    * to carry the body and indices of other induction
     101                 :            :    * variables if a quantified formula to skolemize
     102                 :            :    * has multiple induction variables. See page 5
     103                 :            :    * of Reynolds et al., VMCAI 2015.
     104                 :            :    */
     105                 :            :   static Node mkSkolemizedBodyInduction(const Options& opts,
     106                 :            :                                         Node q,
     107                 :            :                                         Node n,
     108                 :            :                                         std::vector<TNode>& fvs,
     109                 :            :                                         std::vector<Node>& sk,
     110                 :            :                                         Node& sub,
     111                 :            :                                         std::vector<unsigned>& sub_vars);
     112                 :            :   /** get skolem constants for quantified formula q */
     113                 :            :   bool getSkolemConstantsInduction(Node q, std::vector<Node>& skolems);
     114                 :            :   /** get the skolemized body for quantified formula q
     115                 :            :    *
     116                 :            :    * For example, if q is forall x. P( x ), this returns the formula P( k ) for
     117                 :            :    * a fresh Skolem constant k.
     118                 :            :    */
     119                 :            :   Node getSkolemizedBodyInduction(Node q);
     120                 :            :   /** is n a variable that we can apply inductive strenghtening to? */
     121                 :            :   static bool isInductionTerm(const Options& opts, Node n);
     122                 :            :   /**
     123                 :            :    * Get skolemization vectors, where for each quantified formula that was
     124                 :            :    * skolemized, this is the list of skolems that were used to witness the
     125                 :            :    * negation of that quantified formula (which is equivalent to an existential
     126                 :            :    * one).
     127                 :            :    *
     128                 :            :    * This is used for the command line option
     129                 :            :    *   --dump-instantiations
     130                 :            :    * which prints an informal justification of steps taken by the quantifiers
     131                 :            :    * module.
     132                 :            :    */
     133                 :            :   void getSkolemTermVectors(std::map<Node, std::vector<Node> >& sks) const;
     134                 :            : 
     135                 :            :  private:
     136                 :            :   /** Are proofs enabled? */
     137                 :            :   bool isProofEnabled() const;
     138                 :            :   /** get self selectors
     139                 :            :    * For datatype constructor dtc with type dt,
     140                 :            :    * this collects the set of datatype selector applications,
     141                 :            :    * applied to term n, whose return type in ntn, and stores
     142                 :            :    * them in the vector selfSel.
     143                 :            :    */
     144                 :            :   static void getSelfSel(const DType& dt,
     145                 :            :                          const DTypeConstructor& dc,
     146                 :            :                          Node n,
     147                 :            :                          TypeNode ntn,
     148                 :            :                          std::vector<Node>& selfSel);
     149                 :            :   /** Reference to the quantifiers state */
     150                 :            :   QuantifiersState& d_qstate;
     151                 :            :   /** Reference to the term registry */
     152                 :            :   TermRegistry& d_treg;
     153                 :            :   /** quantified formulas that have been skolemized */
     154                 :            :   NodeNodeMap d_skolemized;
     155                 :            :   /** map from quantified formulas to the list of skolem constants */
     156                 :            :   std::unordered_map<Node, std::vector<Node>> d_skolem_constants;
     157                 :            :   /** map from quantified formulas to their skolemized body */
     158                 :            :   std::unordered_map<Node, Node> d_skolem_body;
     159                 :            :   /** Eager proof generator for skolemization lemmas */
     160                 :            :   std::unique_ptr<EagerProofGenerator> d_epg;
     161                 :            : };
     162                 :            : 
     163                 :            : }  // namespace quantifiers
     164                 :            : }  // namespace theory
     165                 :            : }  // namespace cvc5::internal
     166                 :            : 
     167                 :            : #endif /* CVC5__THEORY__QUANTIFIERS__SKOLEMIZE_H */