1 /********************* */
2 /*! \file sygus_module.h
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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
12 ** \brief sygus_module
15 #include "cvc4_private.h"
17 #ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
18 #define __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
21 #include "expr/node.h"
22 #include "theory/quantifiers_engine.h"
26 namespace quantifiers
{
32 * This is the base class of sygus modules, owned by CegConjecture. The purpose
33 * of this class is to, when applicable, suggest candidate solutions for
34 * CegConjecture to test.
36 * In more detail, an instance of the conjecture class (CegConjecture) creates
37 * the negated deep embedding form of the synthesis conjecture. In the
38 * following, assume this is:
39 * forall d. exists x. P( d, x )
40 * where d are of sygus datatype type. The "base instantiation" of this
41 * conjecture (see CegConjecture::d_base_inst) is the formula:
43 * where k are the "candidate" variables for the conjecture.
45 * Modules implement an initialize function, which determines whether the module
46 * will take responsibility for the given conjecture.
51 SygusModule(QuantifiersEngine
* qe
, CegConjecture
* p
);
55 * n is the "base instantiation" of the deep-embedding version of the
56 * synthesis conjecture under candidates (see CegConjecture::d_base_inst).
58 * This function may add lemmas to the argument lemmas, which should be
59 * sent out on the output channel of quantifiers by the caller.
61 * This function returns true if this module will take responsibility for
62 * constructing candidates for the given conjecture.
64 virtual bool initialize(Node n
,
65 const std::vector
<Node
>& candidates
,
66 std::vector
<Node
>& lemmas
) = 0;
69 * This gets the list of terms that will appear as arguments to a subsequent
70 * call to constructCandidates.
72 virtual void getTermList(const std::vector
<Node
>& candidates
,
73 std::vector
<Node
>& terms
) = 0;
74 /** construct candidate
76 * This function takes as input:
77 * terms : the terms returned by a call to getTermList,
78 * term_values : the current model values of terms,
79 * candidates : the list of candidates.
81 * If this function returns true, it adds to candidate_values a list of terms
82 * of the same length and type as candidates that are candidate solutions
83 * to the synthesis conjecture in question. This candidate { v } will then be
84 * tested by testing the (un)satisfiablity of P( v, cex ) for fresh cex by the
87 * This function may also add lemmas to lems, which are sent out as lemmas
88 * on the output channel of quantifiers by the caller. For an example of
89 * such lemmas, see SygusPbe::constructCandidates.
91 * This function may return false if it does not have a candidate it wants
92 * to test on this iteration. In this case, lems should be non-empty.
94 virtual bool constructCandidates(const std::vector
<Node
>& terms
,
95 const std::vector
<Node
>& term_values
,
96 const std::vector
<Node
>& candidates
,
97 std::vector
<Node
>& candidate_values
,
98 std::vector
<Node
>& lems
) = 0;
99 /** register refinement lemma
101 * Assume this module, on a previous call to constructCandidates, added the
102 * value { v } to candidate_values for candidates = { k }. This function is
103 * called if the base instantiation of the synthesis conjecture has a model
104 * under this substitution. In particular, in the above example, this function
105 * is called when the refinement lemma P( v, cex ) has a model M. In calls to
106 * this function, the argument vars is cex and lem is P( k, cex^M ).
108 * This function may also add lemmas to lems, which are sent out as lemmas
109 * on the output channel of quantifiers by the caller. For an example of
110 * such lemmas, see Cegis::registerRefinementLemma.
112 virtual void registerRefinementLemma(const std::vector
<Node
>& vars
,
114 std::vector
<Node
>& lems
)
119 /** reference to quantifier engine */
120 QuantifiersEngine
* d_qe
;
121 /** reference to the parent conjecture */
122 CegConjecture
* d_parent
;
125 } /* CVC4::theory::quantifiers namespace */
126 } /* CVC4::theory namespace */
127 } /* CVC4 namespace */
129 #endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */