1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
|
/********************* */
/*! \file sygus_unif.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief sygus_unif
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H
#include <map>
#include "expr/node.h"
#include "theory/quantifiers/sygus/sygus_unif_strat.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
/** Sygus unification utility
*
* This utility implements synthesis-by-unification style approaches for a
* set of functions-to-synthesize. These approaches include a combination of:
* (1) Decision tree learning, inspired by Alur et al TACAS 2017,
* (2) Divide-and-conquer via string concatenation.
*
* This class maintains, for each function-to-synthesize f:
* (1) A "strategy tree" based on the syntactic restrictions for f that is
* constructed during initialize (d_strategy),
*
* Based on the above, solutions can be constructed via calls to
* constructSolution.
*/
class SygusUnif
{
public:
SygusUnif();
virtual ~SygusUnif();
/** initialize candidate
*
* This initializes this class with functions-to-synthesize f. We also call
* this a "candidate variable". This function can be called more than once
* for different functions-to-synthesize in the same conjecture.
*
* This call constructs a set of enumerators for the relevant subfields of
* the grammar of f and adds them to enums. These enumerators are those that
* should be later given to calls to notifyEnumeration below.
*
* This also may result in lemmas being added to strategy_lemmas,
* which correspond to static symmetry breaking predicates (for example,
* those that exclude ITE from enumerators whose role is enum_io when the
* strategy is ITE_strat). The lemmas are associated with a strategy point of
* the respective function-to-synthesize.
*/
virtual void initializeCandidate(
QuantifiersEngine* qe,
Node f,
std::vector<Node>& enums,
std::map<Node, std::vector<Node>>& strategy_lemmas);
/**
* Notify that the value v has been enumerated for enumerator e. This call
* will add lemmas L to lemmas such that L entails e^M != v for all future
* models M.
*/
virtual void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) = 0;
/** construct solution
*
* This attempts to construct a solution for each function-to-synthesize
* based on the current set of enumerated values. Returns null if it cannot
* for some function (for example, if the set of enumerated values is
* insufficient, or if a non-deterministic strategy aborts).
*
* This call may add lemmas to lemmas that should be sent out on an output
* channel by the caller.
*/
virtual bool constructSolution(std::vector<Node>& sols,
std::vector<Node>& lemmas);
protected:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
/** sygus term database of d_qe */
quantifiers::TermDbSygus* d_tds;
//-----------------------debug printing
/** print ind indentations on trace c */
static void indent(const char* c, int ind);
/** print (pol ? vals : !vals) as a bit-string on trace c */
static void print_val(const char* c,
std::vector<Node>& vals,
bool pol = true);
//-----------------------end debug printing
/** the candidates for this class */
std::vector<Node> d_candidates;
/** maps a function-to-synthesize to the above information */
std::map<Node, SygusUnifStrategy> d_strategy;
/** domain-specific enumerator exclusion techniques
*
* Returns true if the value v for e can be excluded based on a
* domain-specific exclusion technique like the ones below.
*
* results : the values of v under the input examples,
* exp : if this function returns true, then exp contains a (possibly
* generalize) explanation for why v can be excluded.
*/
bool getExplanationForEnumeratorExclude(Node e,
Node v,
std::vector<Node>& results,
std::vector<Node>& exp);
/** returns true if we can exlude values of e based on negative str.contains
*
* Values v for e may be excluded if we realize that the value of v under the
* substitution for some input example will never be contained in some output
* example. For details on this technique, see NegContainsSygusInvarianceTest
* in sygus_invariance.h.
*
* This function depends on whether e is being used to enumerate values
* for any node that is conditional in the strategy graph. For example,
* nodes that are children of ITE strategy nodes are conditional. If any node
* is conditional, then this function returns false.
*/
bool useStrContainsEnumeratorExclude(Node e);
/** cache for the above function */
std::map<Node, bool> d_use_str_contains_eexc;
//------------------------------ constructing solutions
/** implementation-dependent initialize construct solution
*
* Called once before each attempt to construct solutions.
*/
virtual void initializeConstructSol() = 0;
/** implementation-dependent initialize construct solution
*
* Called once before each attempt to construct solution for a
* function-to-synthesize f.
*/
virtual void initializeConstructSolFor(Node f) = 0;
/** implementation-dependent function for construct solution.
*
* Construct a solution based on enumerator e for function-to-synthesize of
* this class with node role nrole in context x.
*
* ind is the term depth of the context (for debugging).
*/
virtual Node constructSol(
Node f, Node e, NodeRole nrole, int ind, std::vector<Node>& lemmas) = 0;
/** Heuristically choose the best solved term from solved in context x,
* currently return the first. */
virtual Node constructBestSolvedTerm(const std::vector<Node>& solved);
/** Heuristically choose the best solved string term from solved in context
* x, currently return the first. */
virtual Node constructBestStringSolvedTerm(const std::vector<Node>& solved);
/** Heuristically choose the best solved conditional term from solved in
* context x, currently random */
virtual Node constructBestSolvedConditional(const std::vector<Node>& solved);
/** Heuristically choose the best conditional term from conds in context x,
* currently random */
virtual Node constructBestConditional(const std::vector<Node>& conds);
/** Heuristically choose the best string to concatenate from strs to the
* solution in context x, currently random
* incr stores the vector of indices that are incremented by this solution in
* example outputs.
* total_inc[x] is the sum of incr[x] for each x in strs.
*/
virtual Node constructBestStringToConcat(
const std::vector<Node>& strs,
const std::map<Node, unsigned>& total_inc,
const std::map<Node, std::vector<unsigned> >& incr);
//------------------------------ end constructing solutions
};
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */
|
