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

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_repair_const.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner
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 sygus_repair_const
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H
19
20
#include <unordered_set>
21
#include "expr/node.h"
22
23
namespace CVC4 {
24
25
class LogicInfo;
26
27
namespace theory {
28
29
class QuantifiersEngine;
30
31
namespace quantifiers {
32
33
class TermDbSygus;
34
35
/** SygusRepairConst
36
 *
37
 * This module is used to repair portions of candidate solutions. In particular,
38
 * given a synthesis conjecture:
39
 *   exists f. forall x. P( f, x )
40
 * and a candidate solution f = \x. t[x,r] where r are repairable terms, this
41
 * function checks whether there exists a term of the form \x. t[x,c'] for some
42
 * constants c' such that:
43
 *   forall x. P( (\x. t[x,c']), x )  [***]
44
 * is satisfiable, where notice that the above formula after beta-reduction may
45
 * be one in pure first-order logic in a decidable theory (say linear
46
 * arithmetic). To check this, we invoke a separate instance of the SmtEngine
47
 * within repairSolution(...) below, which if satisfiable gives us the
48
 * valuation for c'.
49
 */
50
class SygusRepairConst
51
{
52
 public:
53
  SygusRepairConst(QuantifiersEngine* qe);
54
2188
  ~SygusRepairConst() {}
55
  /** initialize
56
   *
57
   * Initialize this class with the base instantiation (body) of the sygus
58
   * conjecture (see SynthConjecture::d_base_inst) and its candidate variables
59
   * (see SynthConjecture::d_candidates).
60
   */
61
  void initialize(Node base_inst, const std::vector<Node>& candidates);
62
  /** repair solution
63
   *
64
   * This function is called when candidates -> candidate_values is a (failed)
65
   * candidate solution for the synthesis conjecture.
66
   *
67
   * If this function returns true, then this class adds to repair_cv the
68
   * repaired version of the solution candidate_values for each candidate,
69
   * where for each index i, repair_cv[i] is obtained by replacing constant
70
   * subterms in candidate_values[i] with others, and
71
   *    candidates -> repair_cv
72
   * is a solution for the synthesis conjecture associated with this class.
73
   * Moreover, it is the case that
74
   *    repair_cv[j] != candidate_values[j], for at least one j.
75
   * We always consider applications of the "any constant" constructors in
76
   * candidate_values to be repairable. In addition, if the flag
77
   * useConstantsAsHoles is true, we consider all constants whose (sygus) type
78
   * admit alls constants to be repairable.
79
   * The repaired solution has the property that it satisfies the synthesis
80
   * conjecture whose body is given by sygusBody.
81
   */
82
  bool repairSolution(Node sygusBody,
83
                      const std::vector<Node>& candidates,
84
                      const std::vector<Node>& candidate_values,
85
                      std::vector<Node>& repair_cv,
86
                      bool useConstantsAsHoles = false);
87
  /**
88
   * Same as above, but where sygusBody is the body (base_inst) provided to the
89
   * call to initialize of this class.
90
   */
91
  bool repairSolution(const std::vector<Node>& candidates,
92
                      const std::vector<Node>& candidate_values,
93
                      std::vector<Node>& repair_cv,
94
                      bool useConstantsAsHoles = false);
95
  /**
96
   * Return whether this module has the possibility to repair solutions. This is
97
   * true if this module has been initialized, and at least one candidate has
98
   * an "any constant" constructor.
99
   */
100
  bool isActive() const;
101
  /** must repair?
102
   *
103
   * This returns true if n must be repaired for it to be a valid solution.
104
   * This corresponds to whether n contains a subterm that is a symbolic
105
   * constructor like the "any constant" constructor.
106
   */
107
  static bool mustRepair(Node n);
108
109
 private:
110
  /** reference to quantifier engine */
111
  QuantifiersEngine* d_qe;
112
  /** pointer to the sygus term database of d_qe */
113
  TermDbSygus* d_tds;
114
  /**
115
   * The "base instantiation" of the deep embedding form of the synthesis
116
   * conjecture associated with this class, see CegConjecture::d_base_inst.
117
   */
118
  Node d_base_inst;
119
  /**
120
   * whether any sygus type for the candidate variables of d_base_inst (the
121
   * syntactic restrictions) allows all constants. If this flag is false, then
122
   * this class is a no-op.
123
   */
124
  bool d_allow_constant_grammar;
125
  /** map from skeleton variables to first-order variables */
126
  std::map<Node, Node> d_sk_to_fo;
127
  /** reverse map of d_sk_to_fo */
128
  std::map<Node, Node> d_fo_to_sk;
129
  /** a cache of satisfiability queries of the form [***] above we have tried */
130
  std::unordered_set<Node, NodeHashFunction> d_queries;
131
  /**
132
   * Register information for sygus type tn, tprocessed stores the set of
133
   * already registered types.
134
   */
135
  void registerSygusType(TypeNode tn, std::map<TypeNode, bool>& tprocessed);
136
  /** is repairable?
137
   *
138
   * This returns true if n can be repaired by this class. In particular, we
139
   * return true if n is an "any constant" constructor, or it is a constructor
140
   * for a constant in a type that allows all constants and useConstantsAsHoles
141
   * is true.
142
   */
143
  static bool isRepairable(Node n, bool useConstantsAsHoles);
144
  /** get skeleton
145
   *
146
   * Returns a skeleton for sygus datatype value n, where the subterms of n that
147
   * are repairable are replaced by free variables. Since we are interested in
148
   * returning canonical skeletons, the free variables we use in this
149
   * replacement are taken from TermDbSygus, where we track indices
150
   * in free_var_count. Variables we introduce in this way are added to sk_vars.
151
   * The mapping sk_vars_to_subs contains entries v -> c, where v is a
152
   * variable in sk_vars, and c is the term in n that it replaced. The flag
153
   * useConstantsAsHoles affects which terms we consider to be repairable.
154
   */
155
  Node getSkeleton(Node n,
156
                   std::map<TypeNode, int>& free_var_count,
157
                   std::vector<Node>& sk_vars,
158
                   std::map<Node, Node>& sk_vars_to_subs,
159
                   bool useConstantsAsHoles);
160
  /** get first-order query
161
   *
162
   * This function returns a formula that is equivalent to the negation of the
163
   * synthesis conjecture whose body is given in the first argument, where
164
   * candidates are replaced by candidate_skeletons,
165
   * whose free variables are in the set sk_vars. The returned formula
166
   * is a first-order (quantified) formula in the background logic, without UF,
167
   * of the form [***] above.
168
   */
169
  Node getFoQuery(Node body,
170
                  const std::vector<Node>& candidates,
171
                  const std::vector<Node>& candidate_skeletons,
172
                  const std::vector<Node>& sk_vars);
173
  /** fit to logic
174
   *
175
   * This function ensures that a query of the form [***] above fits the given
176
   * logic. In our approach for constant repair, replacing constants by
177
   * variables may introduce e.g. non-linearity. If non-linear arithmetic is
178
   * not enabled, we must undo some of the variables we introduced when
179
   * inferring candidate skeletons.
180
   *
181
   * body is the (sygus) form of the original synthesis conjecture we are
182
   * considering in this call.
183
   *
184
   * This function may remove variables from sk_vars and the map
185
   * sk_vars_to_subs. The skeletons candidate_skeletons are obtained by
186
   * getSkeleton(...) on the resulting vectors. If this function returns a
187
   * non-null node n', then n' is getFoQuery(...) on the resulting vectors, and
188
   * n' is in the given logic. The function may return null if it is not
189
   * possible to find a n' of this form.
190
   *
191
   * It uses the function below to choose which variables to remove from
192
   * sk_vars.
193
   */
194
  Node fitToLogic(Node body,
195
                  LogicInfo& logic,
196
                  Node n,
197
                  const std::vector<Node>& candidates,
198
                  std::vector<Node>& candidate_skeletons,
199
                  std::vector<Node>& sk_vars,
200
                  std::map<Node, Node>& sk_vars_to_subs);
201
  /** get fit to logic exclusion variable
202
   *
203
   * If n is not in the given logic, then this method either returns false,
204
   * or returns true and sets exvar to some variable in the domain of
205
   * d_fo_to_sk, that must be replaced by a constant for n to be in the given
206
   * logic. For example, for logic linear arithemic, for input:
207
   *    x * y = 5
208
   * where x is in the domain of d_fo_to_sk, this function returns true and sets
209
   * exvar to x.
210
   * If n is in the given logic, this method returns true.
211
   */
212
  bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar);
213
};
214
215
} /* CVC4::theory::quantifiers namespace */
216
} /* CVC4::theory namespace */
217
} /* CVC4 namespace */
218
219
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */