src/theory/quantifiers/sygus/sygus_module.h

   1 /*********************                                                        */
   2 /*! \file sygus_module.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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
  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 CegConjecture;
  29
  30 /** SygusModule
  31  *
  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.
  35  *
  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:
  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, CegConjecture* p);
  52   ~SygusModule() {}
  53   /** initialize
  54    *
  55    * n is the "base instantiation" of the deep-embedding version of the
  56    * synthesis conjecture under candidates (see CegConjecture::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   /** construct candidate
  75    *
  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.
  80    *
  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, k' ) for fresh k' by the
  85    * caller.
  86    *
  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.
  90    *
  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.
  93    */
  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
 100    *
 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, k' ) has a model. The argument
 106    * lem in the call to this function is P( v, k' ).
 107    */
 108   virtual void registerRefinementLemma(Node lem) {}
 109  protected:
 110   /** reference to quantifier engine */
 111   QuantifiersEngine* d_qe;
 112   /** reference to the parent conjecture */
 113   CegConjecture* d_parent;
 114 };
 115
 116 } /* CVC4::theory::quantifiers namespace */
 117 } /* CVC4::theory namespace */
 118 } /* CVC4 namespace */
 119
 120 #endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */