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
|
/********************* */
/*! \file sygus_module.h
** \verbatim
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 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_module
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
#define __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
#include <map>
#include "expr/node.h"
#include "theory/quantifiers_engine.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
class CegConjecture;
/** SygusModule
*
* This is the base class of sygus modules, owned by CegConjecture. The purpose
* of this class is to, when applicable, suggest candidate solutions for
* CegConjecture to test.
*
* In more detail, an instance of the conjecture class (CegConjecture) creates
* the negated deep embedding form of the synthesis conjecture. In the
* following, assume this is:
* forall d. exists x. P( d, x )
* where d are of sygus datatype type. The "base instantiation" of this
* conjecture (see CegConjecture::d_base_inst) is the formula:
* exists y. P( k, y )
* where k are the "candidate" variables for the conjecture.
*
* Modules implement an initialize function, which determines whether the module
* will take responsibility for the given conjecture.
*/
class SygusModule
{
public:
SygusModule(QuantifiersEngine* qe, CegConjecture* p);
~SygusModule() {}
/** initialize
*
* n is the "base instantiation" of the deep-embedding version of the
* synthesis conjecture under candidates (see CegConjecture::d_base_inst).
*
* This function may add lemmas to the argument lemmas, which should be
* sent out on the output channel of quantifiers by the caller.
*
* This function returns true if this module will take responsibility for
* constructing candidates for the given conjecture.
*/
virtual bool initialize(Node n,
const std::vector<Node>& candidates,
std::vector<Node>& lemmas) = 0;
/** get term list
*
* This gets the list of terms that will appear as arguments to a subsequent
* call to constructCandidates.
*/
virtual void getTermList(const std::vector<Node>& candidates,
std::vector<Node>& terms) = 0;
/** construct candidate
*
* This function takes as input:
* terms : the terms returned by a call to getTermList,
* term_values : the current model values of terms,
* candidates : the list of candidates.
*
* If this function returns true, it adds to candidate_values a list of terms
* of the same length and type as candidates that are candidate solutions
* to the synthesis conjecture in question. This candidate { v } will then be
* tested by testing the (un)satisfiablity of P( v, cex ) for fresh cex by the
* caller.
*
* This function may also add lemmas to lems, which are sent out as lemmas
* on the output channel of quantifiers by the caller. For an example of
* such lemmas, see SygusPbe::constructCandidates.
*
* This function may return false if it does not have a candidate it wants
* to test on this iteration. In this case, lems should be non-empty.
*/
virtual bool constructCandidates(const std::vector<Node>& terms,
const std::vector<Node>& term_values,
const std::vector<Node>& candidates,
std::vector<Node>& candidate_values,
std::vector<Node>& lems) = 0;
/** register refinement lemma
*
* Assume this module, on a previous call to constructCandidates, added the
* value { v } to candidate_values for candidates = { k }. This function is
* called if the base instantiation of the synthesis conjecture has a model
* under this substitution. In particular, in the above example, this function
* is called when the refinement lemma P( v, cex ) has a model M. In calls to
* this function, the argument vars is cex and lem is P( k, cex^M ).
*
* This function may also add lemmas to lems, which are sent out as lemmas
* on the output channel of quantifiers by the caller. For an example of
* such lemmas, see Cegis::registerRefinementLemma.
*/
virtual void registerRefinementLemma(const std::vector<Node>& vars,
Node lem,
std::vector<Node>& lems)
{
}
protected:
/** reference to quantifier engine */
QuantifiersEngine* d_qe;
/** reference to the parent conjecture */
CegConjecture* d_parent;
};
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */
|
