src/theory/quantifiers/sygus/sygus_module.h

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