GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_module.h Lines: 2 5 40.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_module.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Andres Noetzli
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_module
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
19
20
#include <vector>
21
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
namespace theory {
26
27
class QuantifiersEngine;
28
29
namespace quantifiers {
30
31
class SynthConjecture;
32
class TermDbSygus;
33
class QuantifiersInferenceManager;
34
35
/** SygusModule
36
 *
37
 * This is the base class of sygus modules, owned by SynthConjecture. The
38
 * purpose of this class is to, when applicable, suggest candidate solutions for
39
 * SynthConjecture to test.
40
 *
41
 * In more detail, an instance of the conjecture class (SynthConjecture) creates
42
 * the negated deep embedding form of the synthesis conjecture. In the
43
 * following, assume this is:
44
 *   forall d. exists x. P( d, x )
45
 * where d are of sygus datatype type. The "base instantiation" of this
46
 * conjecture (see SynthConjecture::d_base_inst) is the formula:
47
 *   exists y. P( k, y )
48
 * where k are the "candidate" variables for the conjecture.
49
 *
50
 * Modules implement an initialize function, which determines whether the module
51
 * will take responsibility for the given conjecture.
52
 */
53
class SygusModule
54
{
55
 public:
56
  SygusModule(QuantifiersEngine* qe,
57
              QuantifiersInferenceManager& qim,
58
              SynthConjecture* p);
59
8752
  virtual ~SygusModule() {}
60
  /** initialize
61
   *
62
   * This function initializes the module for solving the given conjecture. This
63
   * typically involves registering enumerators (for constructing terms) via
64
   * calls to TermDbSygus::registerEnumerator.
65
   *
66
   * This function returns true if this module will take responsibility for
67
   * constructing candidates for the given conjecture.
68
   *
69
   * conj is the synthesis conjecture (prior to deep-embedding).
70
   *
71
   * n is the "base instantiation" of the deep-embedding version of the
72
   * synthesis conjecture under candidates (see SynthConjecture::d_base_inst).
73
   *
74
   * This function may add lemmas to the argument lemmas, which should be
75
   * sent out on the output channel of quantifiers by the caller.
76
   */
77
  virtual bool initialize(Node conj,
78
                          Node n,
79
                          const std::vector<Node>& candidates,
80
                          std::vector<Node>& lemmas) = 0;
81
  /** get term list
82
   *
83
   * This gets the list of terms that will appear as arguments to a subsequent
84
   * call to constructCandidates.
85
   */
86
  virtual void getTermList(const std::vector<Node>& candidates,
87
                           std::vector<Node>& terms) = 0;
88
  /** allow partial model
89
   *
90
   * This method returns true if this module does not require that all
91
   * terms returned by getTermList have "proper" model values when calling
92
   * constructCandidates. A term may have a model value that is not proper
93
   * if is excluded by symmetry breaking, e.g. x+0 is not proper. All model
94
   * values that are not proper are replaced by "null" when calling
95
   * constructCandidates.
96
   */
97
49147
  virtual bool allowPartialModel() { return false; }
98
  /** construct candidate
99
   *
100
   * This function takes as input:
101
   *   terms : (a subset of) the terms returned by a call to getTermList,
102
   *   term_values : the current model values of terms,
103
   *   candidates : the list of candidates.
104
   *
105
   * In particular, notice that terms do not include inactive enumerators,
106
   * thus if inactive enumerators were added to getTermList, then the terms
107
   * list passed to this call will be a (strict) subset of that list.
108
   *
109
   * If this function returns true, it adds to candidate_values a list of terms
110
   * of the same length and type as candidates that are candidate solutions
111
   * to the synthesis conjecture in question. This candidate { v } will then be
112
   * tested by testing the (un)satisfiablity of P( v, cex ) for fresh cex by the
113
   * caller.
114
   *
115
   * This function may also add lemmas to lems, which are sent out as lemmas
116
   * on the output channel of quantifiers by the caller. For an example of
117
   * such lemmas, see SygusPbe::constructCandidates.
118
   *
119
   * This function may return false if it does not have a candidate it wants
120
   * to test on this iteration. In this case, lems should be non-empty.
121
   */
122
  virtual bool constructCandidates(const std::vector<Node>& terms,
123
                                   const std::vector<Node>& term_values,
124
                                   const std::vector<Node>& candidates,
125
                                   std::vector<Node>& candidate_values,
126
                                   std::vector<Node>& lems) = 0;
127
  /** register refinement lemma
128
   *
129
   * Assume this module, on a previous call to constructCandidates, added the
130
   * value { v } to candidate_values for candidates = { k }. This function is
131
   * called if the base instantiation of the synthesis conjecture has a model
132
   * under this substitution. In particular, in the above example, this function
133
   * is called when the refinement lemma P( v, cex ) has a model M. In calls to
134
   * this function, the argument vars is cex and lem is P( k, cex^M ).
135
   *
136
   * This function may also add lemmas to lems, which are sent out as lemmas
137
   * on the output channel of quantifiers by the caller. For an example of
138
   * such lemmas, see Cegis::registerRefinementLemma.
139
   */
140
  virtual void registerRefinementLemma(const std::vector<Node>& vars,
141
                                       Node lem,
142
                                       std::vector<Node>& lems)
143
  {
144
  }
145
  /**
146
   * Are we trying to repair constants in candidate solutions?
147
   * If we return true for usingRepairConst is true, then this module has
148
   * attmepted to repair any solutions returned by constructCandidates.
149
   */
150
  virtual bool usingRepairConst() { return false; }
151
152
 protected:
153
  /** reference to quantifier engine */
154
  QuantifiersEngine* d_qe;
155
  /** Reference to the quantifiers inference manager */
156
  QuantifiersInferenceManager& d_qim;
157
  /** sygus term database of d_qe */
158
  TermDbSygus* d_tds;
159
  /** reference to the parent conjecture */
160
  SynthConjecture* d_parent;
161
};
162
163
} /* CVC4::theory::quantifiers namespace */
164
} /* CVC4::theory namespace */
165
} /* CVC4 namespace */
166
167
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */