src/theory/quantifiers/sygus/sygus_abduct.cpp

   1 /*********************                                                        */
   2 /*! \file sygus_abduct.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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 Implementation of sygus abduction utility, which
  13  ** transforms an arbitrary input into an abduction problem.
  14  **/
  15
  16 #include "theory/quantifiers/sygus/sygus_abduct.h"
  17
  18 #include "expr/datatype.h"
  19 #include "expr/dtype.h"
  20 #include "expr/node_algorithm.h"
  21 #include "expr/sygus_datatype.h"
  22 #include "theory/datatypes/theory_datatypes_utils.h"
  23 #include "theory/quantifiers/quantifiers_attributes.h"
  24 #include "theory/quantifiers/quantifiers_rewriter.h"
  25 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
  26 #include "theory/quantifiers/term_util.h"
  27 #include "theory/rewriter.h"
  28
  29 using namespace std;
  30 using namespace CVC4::kind;
  31
  32 namespace CVC4 {
  33 namespace theory {
  34 namespace quantifiers {
  35
  36 SygusAbduct::SygusAbduct() {}
  37
  38 Node SygusAbduct::mkAbductionConjecture(const std::string& name,
  39                                         const std::vector<Node>& asserts,
  40                                         const std::vector<Node>& axioms,
  41                                         TypeNode abdGType)
  42 {
  43   NodeManager* nm = NodeManager::currentNM();
  44   std::unordered_set<Node, NodeHashFunction> symset;
  45   for (size_t i = 0, size = asserts.size(); i < size; i++)
  46   {
  47     expr::getSymbols(asserts[i], symset);
  48   }
  49   Trace("sygus-abduct-debug")
  50       << "...finish, got " << symset.size() << " symbols." << std::endl;
  51
  52   Trace("sygus-abduct-debug") << "Setup symbols..." << std::endl;
  53   std::vector<Node> syms;
  54   std::vector<Node> vars;
  55   std::vector<Node> varlist;
  56   std::vector<TypeNode> varlistTypes;
  57   for (const Node& s : symset)
  58   {
  59     TypeNode tn = s.getType();
  60     if (tn.isConstructor() || tn.isSelector() || tn.isTester())
  61     {
  62       // datatype symbols should be considered interpreted symbols here, not
  63       // (higher-order) variables.
  64       continue;
  65     }
  66     // Notice that we allow for non-first class (e.g. function) variables here.
  67     // This is applicable to the case where we are doing get-abduct in a logic
  68     // with UF.
  69     std::stringstream ss;
  70     ss << s;
  71     Node var = nm->mkBoundVar(tn);
  72     syms.push_back(s);
  73     vars.push_back(var);
  74     Node vlv = nm->mkBoundVar(ss.str(), tn);
  75     varlist.push_back(vlv);
  76     varlistTypes.push_back(tn);
  77     // set that this variable encodes the term s
  78     SygusVarToTermAttribute sta;
  79     vlv.setAttribute(sta, s);
  80   }
  81   Trace("sygus-abduct-debug") << "...finish" << std::endl;
  82
  83   Trace("sygus-abduct-debug") << "Make abduction predicate..." << std::endl;
  84   // make the abduction predicate to synthesize
  85   TypeNode abdType = varlistTypes.empty() ? nm->booleanType()
  86                                           : nm->mkPredicateType(varlistTypes);
  87   Node abd = nm->mkBoundVar(name.c_str(), abdType);
  88   Trace("sygus-abduct-debug") << "...finish" << std::endl;
  89
  90   // the sygus variable list
  91   Node abvl;
  92   // if provided, we will associate the provide sygus datatype type with the
  93   // function-to-synthesize. However, we must convert it so that its
  94   // free symbols are universally quantified.
  95   if (!abdGType.isNull())
  96   {
  97     Assert(abdGType.isDatatype() && abdGType.getDType().isSygus());
  98     Trace("sygus-abduct-debug") << "Process abduction type:" << std::endl;
  99     Trace("sygus-abduct-debug") << abdGType.getDType().getName() << std::endl;
 100
 101     // substitute the free symbols of the grammar with variables corresponding
 102     // to the formal argument list of the new sygus datatype type.
 103     TypeNode abdGTypeS = datatypes::utils::substituteAndGeneralizeSygusType(
 104         abdGType, syms, varlist);
 105
 106     Assert(abdGTypeS.isDatatype() && abdGTypeS.getDType().isSygus());
 107
 108     Trace("sygus-abduct-debug")
 109         << "Make sygus grammar attribute..." << std::endl;
 110     Node sym = nm->mkBoundVar("sfproxy_abduct", abdGTypeS);
 111     // Set the sygus grammar attribute to indicate that abdGTypeS encodes the
 112     // grammar for abd.
 113     theory::SygusSynthGrammarAttribute ssg;
 114     abd.setAttribute(ssg, sym);
 115     Trace("sygus-abduct-debug") << "Finished setting up grammar." << std::endl;
 116
 117     // use the bound variable list from the new substituted grammar type
 118     const DType& agtsd = abdGTypeS.getDType();
 119     abvl = agtsd.getSygusVarList();
 120     Assert(!abvl.isNull() && abvl.getKind() == BOUND_VAR_LIST);
 121   }
 122   else
 123   {
 124     // the bound variable list of the abduct-to-synthesize is determined by
 125     // the variable list above
 126     abvl = nm->mkNode(BOUND_VAR_LIST, varlist);
 127     // We do not set a grammar type for abd (SygusSynthGrammarAttribute).
 128     // Its grammar will be constructed internally in the default way
 129   }
 130
 131   Trace("sygus-abduct-debug") << "Make abduction predicate app..." << std::endl;
 132   std::vector<Node> achildren;
 133   achildren.push_back(abd);
 134   achildren.insert(achildren.end(), vars.begin(), vars.end());
 135   Node abdApp = vars.empty() ? abd : nm->mkNode(APPLY_UF, achildren);
 136   Trace("sygus-abduct-debug") << "...finish" << std::endl;
 137
 138   Trace("sygus-abduct-debug") << "Set attributes..." << std::endl;
 139   // set the sygus bound variable list
 140   abd.setAttribute(theory::SygusSynthFunVarListAttribute(), abvl);
 141   Trace("sygus-abduct-debug") << "...finish" << std::endl;
 142
 143   Trace("sygus-abduct-debug") << "Make conjecture body..." << std::endl;
 144   Node input = asserts.size() == 1 ? asserts[0] : nm->mkNode(AND, asserts);
 145   input = input.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
 146   // A(x) => ~input( x )
 147   input = nm->mkNode(OR, abdApp.negate(), input.negate());
 148   Trace("sygus-abduct-debug") << "...finish" << std::endl;
 149
 150   Trace("sygus-abduct-debug") << "Make conjecture..." << std::endl;
 151   Node res = input.negate();
 152   if (!vars.empty())
 153   {
 154     Node bvl = nm->mkNode(BOUND_VAR_LIST, vars);
 155     // exists x. ~( A( x ) => ~input( x ) )
 156     res = nm->mkNode(EXISTS, bvl, res);
 157   }
 158   // sygus attribute
 159   Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
 160   theory::SygusAttribute ca;
 161   sygusVar.setAttribute(ca, true);
 162   Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar);
 163   std::vector<Node> iplc;
 164   iplc.push_back(instAttr);
 165   Node aconj = axioms.size() == 0
 166                    ? nm->mkConst(true)
 167                    : (axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms));
 168   aconj = aconj.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
 169   Trace("sygus-abduct") << "---> Assumptions: " << aconj << std::endl;
 170   Node sc = nm->mkNode(AND, aconj, abdApp);
 171   Node vbvl = nm->mkNode(BOUND_VAR_LIST, vars);
 172   sc = nm->mkNode(EXISTS, vbvl, sc);
 173   Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType());
 174   sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc);
 175   instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar);
 176   // build in the side condition
 177   //   exists x. A( x ) ^ input_axioms( x )
 178   // as an additional annotation on the sygus conjecture. In other words,
 179   // the abducts A we procedure must be consistent with our axioms.
 180   iplc.push_back(instAttr);
 181   Node instAttrList = nm->mkNode(INST_PATTERN_LIST, iplc);
 182
 183   Node fbvl = nm->mkNode(BOUND_VAR_LIST, abd);
 184
 185   // forall A. exists x. ~( A( x ) => ~input( x ) )
 186   res = nm->mkNode(FORALL, fbvl, res, instAttrList);
 187   Trace("sygus-abduct-debug") << "...finish" << std::endl;
 188
 189   res = theory::Rewriter::rewrite(res);
 190
 191   Trace("sygus-abduct") << "Generate: " << res << std::endl;
 192
 193   return res;
 194 }
 195
 196 }  // namespace quantifiers
 197 }  // namespace theory
 198 }  // namespace CVC4