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
|
/********************* */
/*! \file cegis.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 cegis
**/
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__QUANTIFIERS__CEGIS_H
#define __CVC4__THEORY__QUANTIFIERS__CEGIS_H
#include <map>
#include "theory/quantifiers/sygus/sygus_module.h"
#include "theory/quantifiers/sygus_sampler.h"
namespace CVC4 {
namespace theory {
namespace quantifiers {
/** Cegis
*
* The default sygus module for synthesis, counterexample-guided inductive
* synthesis (CEGIS).
*
* It initializes a list of sygus enumerators that are one-to-one with
* candidates, and returns a list of candidates that are the model values
* of these enumerators on calls to constructCandidates.
*
* It implements an optimization (getRefinementEvalLemmas) that evaluates all
* previous refinement lemmas for a term before returning it as a candidate
* in calls to constructCandidates.
*/
class Cegis : public SygusModule
{
public:
Cegis(QuantifiersEngine* qe, CegConjecture* p);
~Cegis() {}
/** initialize */
virtual bool initialize(Node n,
const std::vector<Node>& candidates,
std::vector<Node>& lemmas) override;
/** get term list */
virtual void getTermList(const std::vector<Node>& candidates,
std::vector<Node>& enums) override;
/** construct candidate */
virtual bool constructCandidates(const std::vector<Node>& enums,
const std::vector<Node>& enum_values,
const std::vector<Node>& candidates,
std::vector<Node>& candidate_values,
std::vector<Node>& lems) override;
/** register refinement lemma
*
* This function stores lem as a refinement lemma, and adds it to lems.
*/
virtual void registerRefinementLemma(const std::vector<Node>& vars,
Node lem,
std::vector<Node>& lems) override;
protected:
/** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */
std::vector<Node> d_base_vars;
/**
* If CegConjecture::d_base_inst is exists y. P( d, y ), then this is the
* formula P( CegConjecture::d_candidates, y ).
*/
Node d_base_body;
//-----------------------------------refinement lemmas
/** refinement lemmas */
std::vector<Node> d_refinement_lemmas;
/** get number of refinement lemmas we have added so far */
unsigned getNumRefinementLemmas() { return d_refinement_lemmas.size(); }
/** get refinement lemma
*
* If d_embed_quant is forall d. exists y. P( d, y ), then a refinement
* lemma is one of the form ~P( d_candidates, c ) for some c.
*/
Node getRefinementLemma(unsigned i) { return d_refinement_lemmas[i]; }
/** sample add refinement lemma
*
* This function will check if there is a sample point in d_sampler that
* refutes the candidate solution (d_quant_vars->vals). If so, it adds a
* refinement lemma to the lists d_refinement_lemmas that corresponds to that
* sample point, and adds a lemma to lems if cegisSample mode is not trust.
*/
bool sampleAddRefinementLemma(const std::vector<Node>& candidates,
const std::vector<Node>& vals,
std::vector<Node>& lems);
/** evaluates candidate values on current refinement lemmas
*
* Returns true if refinement lemmas are added after evaluation, false
* otherwise.
*
* Also eagerly unfolds evaluation functions in a heuristic manner, which is
* useful e.g. for boolean connectives
*/
bool addEvalLemmas(const std::vector<Node>& candidates,
const std::vector<Node>& candidate_values);
//-----------------------------------end refinement lemmas
/** Get refinement evaluation lemmas
*
* Given a candidate solution ms for candidates vs, this function adds lemmas
* to lems based on evaluating the conjecture, instantiated for ms, on lemmas
* for previous refinements (d_refinement_lemmas).
*/
void getRefinementEvalLemmas(const std::vector<Node>& vs,
const std::vector<Node>& ms,
std::vector<Node>& lems);
/** sampler object for the option cegisSample()
*
* This samples points of the type of the inner variables of the synthesis
* conjecture (d_base_vars).
*/
SygusSampler d_cegis_sampler;
/** cegis sample refine points
*
* Stores the list of indices of sample points in d_cegis_sampler we have
* added as refinement lemmas.
*/
std::unordered_set<unsigned> d_cegis_sample_refine;
};
} /* CVC4::theory::quantifiers namespace */
} /* CVC4::theory namespace */
} /* CVC4 namespace */
#endif /* __CVC4__THEORY__QUANTIFIERS__CEGIS_H */
|
