GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/skolemize.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file skolemize.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Abdalrhman Mohamed
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief utilities for skolemization
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
18
#define CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H
19
20
#include <unordered_map>
21
#include <unordered_set>
22
23
#include "context/cdhashmap.h"
24
#include "expr/node.h"
25
#include "expr/type_node.h"
26
#include "theory/eager_proof_generator.h"
27
#include "theory/trust_node.h"
28
29
namespace CVC4 {
30
31
class DTypeConstructor;
32
33
namespace theory {
34
35
class SortInference;
36
37
namespace quantifiers {
38
39
class QuantifiersState;
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
68
{
69
  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
70
71
 public:
72
  Skolemize(QuantifiersState& qs, ProofNodeManager* pnm);
73
8992
  ~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 skolem constants for quantified formula q */
81
  bool getSkolemConstants(Node q, std::vector<Node>& skolems);
82
  /** get the i^th skolem constant for quantified formula q */
83
  Node getSkolemConstant(Node q, unsigned 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 arguments fvTypes and 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 fvTypes 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 mkSkolemizedBody(Node q,
106
                               Node n,
107
                               std::vector<TypeNode>& fvTypes,
108
                               std::vector<TNode>& fvs,
109
                               std::vector<Node>& sk,
110
                               Node& sub,
111
                               std::vector<unsigned>& sub_vars);
112
  /** get the skolemized body for quantified formula q */
113
  Node getSkolemizedBody(Node q);
114
  /** is n a variable that we can apply inductive strenghtening to? */
115
  static bool isInductionTerm(Node n);
116
  /**
117
   * Get skolemization vectors, where for each quantified formula that was
118
   * skolemized, this is the list of skolems that were used to witness the
119
   * negation of that quantified formula (which is equivalent to an existential
120
   * one).
121
   *
122
   * This is used for the command line option
123
   *   --dump-instantiations
124
   * which prints an informal justification of steps taken by the quantifiers
125
   * module.
126
   */
127
  void getSkolemTermVectors(std::map<Node, std::vector<Node> >& sks) const;
128
129
 private:
130
  /** Are proofs enabled? */
131
  bool isProofEnabled() const;
132
  /** get self selectors
133
   * For datatype constructor dtc with type dt,
134
   * this collects the set of datatype selector applications,
135
   * applied to term n, whose return type in ntn, and stores
136
   * them in the vector selfSel.
137
   */
138
  static void getSelfSel(const DType& dt,
139
                         const DTypeConstructor& dc,
140
                         Node n,
141
                         TypeNode ntn,
142
                         std::vector<Node>& selfSel);
143
  /** Reference to the quantifiers state */
144
  QuantifiersState& d_qstate;
145
  /** quantified formulas that have been skolemized */
146
  NodeNodeMap d_skolemized;
147
  /** map from quantified formulas to the list of skolem constants */
148
  std::unordered_map<Node, std::vector<Node>, NodeHashFunction>
149
      d_skolem_constants;
150
  /** map from quantified formulas to their skolemized body */
151
  std::unordered_map<Node, Node, NodeHashFunction> d_skolem_body;
152
  /** Pointer to the proof node manager */
153
  ProofNodeManager* d_pnm;
154
  /** Eager proof generator for skolemization lemmas */
155
  std::unique_ptr<EagerProofGenerator> d_epg;
156
};
157
158
} /* CVC4::theory::quantifiers namespace */
159
} /* CVC4::theory namespace */
160
} /* CVC4 namespace */
161
162
#endif /* CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */