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