src/theory/quantifiers/sygus/sygus_interpol.h

   1 /*********************                                                        */
   2 /*! \file sygus_interpol.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Ying Sheng
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 interpolation utility, which transforms an input of axioms and
  13  ** conjecture into an interpolation problem, and solve it.
  14  **/
  15
  16 #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
  17 #define CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H
  18
  19 #include <string>
  20 #include <vector>
  21
  22 #include "expr/node.h"
  23 #include "expr/type.h"
  24 #include "smt/smt_engine.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace quantifiers {
  29 /**
  30  * This is an utility for the SMT-LIB command (get-interpol <term>).
  31  * The utility turns a set of quantifier-free assertions into a sygus
  32  * conjecture that encodes an interpolation problem, and then solve the
  33  * interpolation problem by synthesizing it. In detail, if our input formula is
  34  * F( x ) for free symbol x, and is partitioned into axioms Fa and conjecture Fc
  35  * then the sygus conjecture we construct is:
  36  *
  37  * exists A. forall x. ( (Fa( x ) => A( x )) ^ (A( x ) => Fc( x )) )
  38  *
  39  * where A( x ) is a predicate over the free symbols of our input that are
  40  * shared between Fa and Fc. In other words, A( x ) must be implied by our
  41  * axioms Fa( x ) and implies Fc( x ). Then, to solve the interpolation problem,
  42  * we just need to synthesis A( x ).
  43  */
  44 class SygusInterpol
  45 {
  46  public:
  47   SygusInterpol();
  48
  49   SygusInterpol(LogicInfo logic);
  50
  51   /**
  52    * Returns the sygus conjecture in interpol corresponding to the interpolation
  53    * problem for input problem (F above) given by axioms (Fa above), and conj
  54    * (Fc above). And solve the interpolation by sygus. Note that axioms is
  55    * expected to be a subset of assertions in SMT-LIB.
  56    *
  57    * @param name the name for the interpol-to-synthesize.
  58    * @param axioms the assertions (Fa above)
  59    * @param conj the conjecture (Fc above)
  60    * @param itpGType (if non-null) a sygus datatype type that encodes the
  61    * grammar that should be used for solutions of the interpolation conjecture.
  62    * @interpol the solution to the sygus conjecture.
  63    */
  64   bool SolveInterpolation(const std::string& name,
  65                           const std::vector<Node>& axioms,
  66                           const Node& conj,
  67                           const TypeNode& itpGType,
  68                           Expr& interpol);
  69
  70  private:
  71   /**
  72    * Collects symbols from axioms (axioms) and conjecture (conj), which are
  73    * stored in d_syms, and computes the shared symbols between axioms and
  74    * conjecture, stored in d_symSetShared.
  75    *
  76    * @param axioms the assertions (Fa above)
  77    * @param conj the conjecture (Fc above)
  78    */
  79   void collectSymbols(const std::vector<Node>& axioms, const Node& conj);
  80
  81   /**
  82    * Creates free variables and shared free variables from d_syms and
  83    * d_symSetShared, which are stored in d_vars and d_varsShared. And also
  84    * creates the corresponding set of variables for the formal argument list,
  85    * which is stored in d_vlvs and d_vlvsShared. Extracts the types of shared
  86    * variables, which are stored in d_varTypesShared. Creates the formal
  87    * argument list of the interpol-to-synthese, stored in d_ibvlShared.
  88    *
  89    * When using default grammar, the needsShared is true. When using
  90    * user-defined gramar, the needsShared is false.
  91    *
  92    * @param needsShared If it is true, the argument list of the
  93    * interpol-to-synthesis will be restricted to be over shared variables. If it
  94    * is false, the argument list will be over all the variables.
  95    */
  96   void createVariables(bool needsShared);
  97
  98   /**
  99    * Get include_cons for mkSygusDefaultType.
 100    * mkSygusDefaultType() is a function to make default grammar. It has an
 101    * arguemnt include_cons, which will restrict what operators we want in the
 102    * grammar. The return value depends on options::produceInterpols(). In
 103    * ASSUMPTIONS option, it will return the operators from axioms. In CONJECTURE
 104    * option, it will return the operators from conj. In SHARED option, it will
 105    * return the oprators shared by axioms and conj. In ALL option, it will
 106    * return the operators from either axioms or conj.
 107    *
 108    * @param axioms input argument
 109    * @param conj input argument
 110    * @param result the return value
 111    */
 112   void getIncludeCons(
 113       const std::vector<Node>& axioms,
 114       const Node& conj,
 115       std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& result);
 116
 117   /**
 118    * Set up the grammar for the interpol-to-synthesis.
 119    *
 120    * The user-defined grammar will be encoded by itpGType. The options for
 121    * grammar is given by options::produceInterpols(). In DEFAULT option, it will
 122    * set up the grammar from itpGType. And if itpGType is null, it will set up
 123    * the default grammar, which is built according to a policy handled by
 124    * getIncludeCons().
 125    *
 126    * @param itpGType (if non-null) a sygus datatype type that encodes the
 127    * grammar that should be used for solutions of the interpolation conjecture.
 128    * @param axioms the assertions (Fa above)
 129    * @param conj the conjecture (Fc above)
 130    */
 131   TypeNode setSynthGrammar(const TypeNode& itpGType,
 132                            const std::vector<Node>& axioms,
 133                            const Node& conj);
 134
 135   /**
 136    * Make the interpolation predicate.
 137    *
 138    * @param name the name of the interpol-to-synthesis.
 139    */
 140   Node mkPredicate(const std::string& name);
 141
 142   /**
 143    * Make the sygus conjecture to be synthesis.
 144    *
 145    * @param itp the interpolation predicate.
 146    * @param axioms the assertions (Fa above)
 147    * @param conj the conjecture (Fc above)
 148    */
 149   void mkSygusConjecture(Node itp,
 150                          const std::vector<Node>& axioms,
 151                          const Node& conj);
 152
 153   /**
 154    * Get the synthesis solution, stored in interpol.
 155    *
 156    * @param interpol the solution to the sygus conjecture.
 157    * @param itp the interpolation predicate.
 158    */
 159   bool findInterpol(Expr& interpol, Node itp);
 160
 161   /** The SMT engine subSolver
 162    *
 163    * This is a fresh copy of the SMT engine which is used for solving the
 164    * interpolation problem. In particular, consider the input: (assert A)
 165    *   (get-interpol s B)
 166    * In the copy of the SMT engine where these commands are issued, we maintain
 167    * A in the assertion stack. In solving the interpolation problem, we will
 168    * need to call a SMT engine solver with a different assertion stack, which is
 169    * a sygus conjecture build from A and B. Then to solve the interpolation
 170    * problem, instead of modifying the assertion stack to remove A and add the
 171    * sygus conjecture (exists I. ...), we invoke a fresh copy of the SMT engine
 172    * and leave the original assertion stack unchanged. This copy of the SMT
 173    * engine will have the assertion stack with the sygus conjecture. This copy
 174    * of the SMT engine can be further queried for information regarding further
 175    * solutions.
 176    */
 177   std::unique_ptr<SmtEngine> d_subSolver;
 178
 179   /**
 180    * The logic for the local copy of SMT engine (d_subSolver).
 181    */
 182   LogicInfo d_logic;
 183   /**
 184    * symbols from axioms and conjecture.
 185    */
 186   std::vector<Node> d_syms;
 187   /**
 188    * unordered set for shared symbols between axioms and conjecture.
 189    */
 190   std::unordered_set<Node, NodeHashFunction> d_symSetShared;
 191   /**
 192    * free variables created from d_syms.
 193    */
 194   std::vector<Node> d_vars;
 195   /**
 196    * variables created from d_syms for formal argument list.
 197    */
 198   std::vector<Node> d_vlvs;
 199   /**
 200    * free variables created from d_symSetShared.
 201    */
 202   std::vector<Node> d_varsShared;
 203   /**
 204    * variables created from d_symShared for formal argument list.
 205    */
 206   std::vector<Node> d_vlvsShared;
 207   /**
 208    * types of shared variables between axioms and conjecture.
 209    */
 210   std::vector<TypeNode> d_varTypesShared;
 211   /**
 212    * formal argument list of the interpol-to-synthesis.
 213    */
 214   Node d_ibvlShared;
 215
 216   /**
 217    * the sygus conjecture to synthesis for interpolation problem
 218    */
 219   Node d_sygusConj;
 220 };
 221
 222 }  // namespace quantifiers
 223 }  // namespace theory
 224 }  // namespace CVC4
 225
 226 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INTERPOL_H */