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
189
190
191
192
193
194
195
196
197
198
199
200
201
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 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.
* ****************************************************************************
*
* The solver for SyGuS queries.
*/
#include "cvc5_private.h"
#ifndef CVC5__SMT__SYGUS_SOLVER_H
#define CVC5__SMT__SYGUS_SOLVER_H
#include "context/cdo.h"
#include "expr/node.h"
#include "expr/type_node.h"
#include "smt/assertions.h"
#include "util/result.h"
namespace cvc5 {
class OutputManager;
namespace smt {
class Preprocessor;
class SmtSolver;
/**
* A solver for sygus queries.
*
* This class is responsible for responding to check-synth commands. It calls
* check satisfiability using an underlying SmtSolver object.
*
* It also maintains a reference to a preprocessor for implementing
* checkSynthSolution.
*/
class SygusSolver
{
public:
SygusSolver(Env& env, SmtSolver& sms, Preprocessor& pp);
~SygusSolver();
/**
* Add variable declaration.
*
* Declared SyGuS variables may be used in SyGuS constraints, in which they
* are assumed to be universally quantified.
*
* In SyGuS semantics, declared functions are treated in the same manner as
* declared variables, i.e. as universally quantified (function) variables
* which can occur in the SyGuS constraints that compose the conjecture to
* which a function is being synthesized. Thus declared functions should use
* this method as well.
*/
void declareSygusVar(Node var);
/**
* Add a function-to-synthesize declaration.
*
* The given type may not correspond to the actual function type but to a
* datatype encoding the syntax restrictions for the
* function-to-synthesize. In this case this information is stored to be used
* during solving.
*
* vars contains the arguments of the function-to-synthesize. These variables
* are also stored to be used during solving.
*
* isInv determines whether the function-to-synthesize is actually an
* invariant. This information is necessary if we are dumping a command
* corresponding to this declaration, so that it can be properly printed.
*/
void declareSynthFun(Node func,
TypeNode type,
bool isInv,
const std::vector<Node>& vars);
/** Add a regular sygus constraint or assumption.*/
void assertSygusConstraint(Node n, bool isAssume);
/**
* Add an invariant constraint.
*
* Invariant constraints are not explicitly declared: they are given in terms
* of the invariant-to-synthesize, the pre condition, transition relation and
* post condition. The actual constraint is built based on the inputs of these
* place holder predicates :
*
* PRE(x) -> INV(x)
* INV() ^ TRANS(x, x') -> INV(x')
* INV(x) -> POST(x)
*
* The regular and primed variables are retrieved from the declaration of the
* invariant-to-synthesize.
*/
void assertSygusInvConstraint(Node inv, Node pre, Node trans, Node post);
/**
* Assert a synthesis conjecture to the current context and call
* check(). Returns sat, unsat, or unknown result.
*
* The actual synthesis conjecture is built based on the previously
* communicated information to this module (universal variables, defined
* functions, functions-to-synthesize, and which constraints compose it). The
* built conjecture is a higher-order formula of the form
*
* exists f1...fn . forall v1...vm . F
*
* in which f1...fn are the functions-to-synthesize, v1...vm are the declared
* universal variables and F is the set of declared constraints.
*/
Result checkSynth(Assertions& as);
/**
* Get synth solution.
*
* This method returns true if we are in a state immediately preceded by
* a successful call to checkSynth.
*
* This method adds entries to sol_map that map functions-to-synthesize with
* their solutions, for all active conjectures. This should be called
* immediately after the solver answers unsat for sygus input.
*
* Specifically, given a sygus conjecture of the form
* exists x1...xn. forall y1...yn. P( x1...xn, y1...yn )
* where x1...xn are second order bound variables, we map each xi to
* lambda term in sol_map such that
* forall y1...yn. P( sol_map[x1]...sol_map[xn], y1...yn )
* is a valid formula.
*/
bool getSynthSolutions(std::map<Node, Node>& sol_map);
private:
/**
* Check that a solution to a synthesis conjecture is indeed a solution.
*
* The check is made by determining if the negation of the synthesis
* conjecture in which the functions-to-synthesize have been replaced by the
* synthesized solutions, which is a quantifier-free formula, is
* unsatisfiable. If not, then the found solutions are wrong.
*/
void checkSynthSolution(Assertions& as);
/**
* Set sygus conjecture is stale. The sygus conjecture is stale if either:
* (1) no sygus conjecture has been added as an assertion to this SMT engine,
* (2) there is a sygus conjecture that has been added as an assertion
* internally to this SMT engine, and there have been further calls such that
* the asserted conjecture is no longer up-to-date.
*
* This method should be called when new sygus constraints are asserted and
* when functions-to-synthesize are declared. This function pops a user
* context if we are in incremental mode and the sygus conjecture was
* previously not stale.
*/
void setSygusConjectureStale();
/**
* Expand definitions in sygus datatype tn, which ensures that all
* sygus constructors that are used to build values of sygus datatype
* tn are associated with their expanded definition form.
*
* This method is required at this level since sygus grammars may include
* user-defined functions. Thus, we must use the preprocessor here to
* associate the use of those functions with their expanded form, since
* the internal sygus solver must reason about sygus operators after
* expansion.
*/
void expandDefinitionsSygusDt(TypeNode tn) const;
/** Reference to the env class */
Env& d_env;
/** The SMT solver, which is used during checkSynth. */
SmtSolver& d_smtSolver;
/** The preprocessor, used for checkSynthSolution. */
Preprocessor& d_pp;
/**
* sygus variables declared (from "declare-var" and "declare-fun" commands)
*
* The SyGuS semantics for declared variables is that they are implicitly
* universally quantified in the constraints.
*/
std::vector<Node> d_sygusVars;
/** sygus constraints */
std::vector<Node> d_sygusConstraints;
/** sygus assumptions */
std::vector<Node> d_sygusAssumps;
/** functions-to-synthesize */
std::vector<Node> d_sygusFunSymbols;
/**
* Whether we need to reconstruct the sygus conjecture.
*/
context::CDO<bool> d_sygusConjectureStale;
};
} // namespace smt
} // namespace cvc5
#endif /* CVC5__SMT__SYGUS_SOLVER_H */
|
