1 /*********************                                                        */
2 /*! \file sygus_module.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Andrew Reynolds, Andres Noetzli
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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
11  **
12  ** \brief sygus_module
13  **/
14 
15 #include "cvc4_private.h"
16 
17 #ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
18 #define __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H
19 
20 #include <map>
21 #include "expr/node.h"
22 #include "theory/quantifiers_engine.h"
23 
24 namespace CVC4 {
25 namespace theory {
26 namespace quantifiers {
27 
28 class SynthConjecture;
29 
30 /** SygusModule
31  *
32  * This is the base class of sygus modules, owned by SynthConjecture. The
33  * purpose of this class is to, when applicable, suggest candidate solutions for
34  * SynthConjecture to test.
35  *
36  * In more detail, an instance of the conjecture class (SynthConjecture) 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 SynthConjecture::d_base_inst) is the formula:
42  *   exists y. P( k, y )
43  * where k are the "candidate" variables for the conjecture.
44  *
45  * Modules implement an initialize function, which determines whether the module
46  * will take responsibility for the given conjecture.
47  */
48 class SygusModule
49 {
50  public:
51   SygusModule(QuantifiersEngine* qe, SynthConjecture* p);
~SygusModule()52   virtual ~SygusModule() {}
53   /** initialize
54    *
55    * n is the "base instantiation" of the deep-embedding version of the
56    * synthesis conjecture under candidates (see SynthConjecture::d_base_inst).
57    *
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.
60    *
61    * This function returns true if this module will take responsibility for
62    * constructing candidates for the given conjecture.
63    */
64   virtual bool initialize(Node n,
65                           const std::vector<Node>& candidates,
66                           std::vector<Node>& lemmas) = 0;
67   /** get term list
68    *
69    * This gets the list of terms that will appear as arguments to a subsequent
70    * call to constructCandidates.
71    */
72   virtual void getTermList(const std::vector<Node>& candidates,
73                            std::vector<Node>& terms) = 0;
74   /** allow partial model
75    *
76    * This method returns true if this module does not require that all
77    * terms returned by getTermList have "proper" model values when calling
78    * constructCandidates. A term may have a model value that is not proper
79    * if is excluded by symmetry breaking, e.g. x+0 is not proper. All model
80    * values that are not proper are replaced by "null" when calling
81    * constructCandidates.
82    */
allowPartialModel()83   virtual bool allowPartialModel() { return false; }
84   /** construct candidate
85    *
86    * This function takes as input:
87    *   terms : (a subset of) the terms returned by a call to getTermList,
88    *   term_values : the current model values of terms,
89    *   candidates : the list of candidates.
90    *
91    * In particular, notice that terms do not include inactive enumerators,
92    * thus if inactive enumerators were added to getTermList, then the terms
93    * list passed to this call will be a (strict) subset of that list.
94    *
95    * If this function returns true, it adds to candidate_values a list of terms
96    * of the same length and type as candidates that are candidate solutions
97    * to the synthesis conjecture in question. This candidate { v } will then be
98    * tested by testing the (un)satisfiablity of P( v, cex ) for fresh cex by the
99    * caller.
100    *
101    * This function may also add lemmas to lems, which are sent out as lemmas
102    * on the output channel of quantifiers by the caller. For an example of
103    * such lemmas, see SygusPbe::constructCandidates.
104    *
105    * This function may return false if it does not have a candidate it wants
106    * to test on this iteration. In this case, lems should be non-empty.
107    */
108   virtual bool constructCandidates(const std::vector<Node>& terms,
109                                    const std::vector<Node>& term_values,
110                                    const std::vector<Node>& candidates,
111                                    std::vector<Node>& candidate_values,
112                                    std::vector<Node>& lems) = 0;
113   /** register refinement lemma
114    *
115    * Assume this module, on a previous call to constructCandidates, added the
116    * value { v } to candidate_values for candidates = { k }. This function is
117    * called if the base instantiation of the synthesis conjecture has a model
118    * under this substitution. In particular, in the above example, this function
119    * is called when the refinement lemma P( v, cex ) has a model M. In calls to
120    * this function, the argument vars is cex and lem is P( k, cex^M ).
121    *
122    * This function may also add lemmas to lems, which are sent out as lemmas
123    * on the output channel of quantifiers by the caller. For an example of
124    * such lemmas, see Cegis::registerRefinementLemma.
125    */
registerRefinementLemma(const std::vector<Node> & vars,Node lem,std::vector<Node> & lems)126   virtual void registerRefinementLemma(const std::vector<Node>& vars,
127                                        Node lem,
128                                        std::vector<Node>& lems)
129   {
130   }
131   /**
132    * Are we trying to repair constants in candidate solutions?
133    * If we return true for usingRepairConst is true, then this module has
134    * attmepted to repair any solutions returned by constructCandidates.
135    */
usingRepairConst()136   virtual bool usingRepairConst() { return false; }
137 
138  protected:
139   /** reference to quantifier engine */
140   QuantifiersEngine* d_qe;
141   /** sygus term database of d_qe */
142   quantifiers::TermDbSygus* d_tds;
143   /** reference to the parent conjecture */
144   SynthConjecture* d_parent;
145 };
146 
147 } /* CVC4::theory::quantifiers namespace */
148 } /* CVC4::theory namespace */
149 } /* CVC4 namespace */
150 
151 #endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */
152