src/theory/quantifiers/sygus/cegis_unif.cpp

   1 /*********************                                                        */
   2 /*! \file cegis_unif.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Haniel Barbosa
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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 class for cegis with unification techniques
  13  **/
  14
  15 #include "theory/quantifiers/sygus/cegis_unif.h"
  16
  17 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
  18 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
  19 #include "theory/quantifiers/sygus/term_database_sygus.h"
  20
  21 using namespace CVC4::kind;
  22
  23 namespace CVC4 {
  24 namespace theory {
  25 namespace quantifiers {
  26
  27 CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p)
  28     : SygusModule(qe, p)
  29 {
  30   d_tds = d_qe->getTermDatabaseSygus();
  31 }
  32
  33 CegisUnif::~CegisUnif() {}
  34 bool CegisUnif::initialize(Node n,
  35                            const std::vector<Node>& candidates,
  36                            std::vector<Node>& lemmas)
  37 {
  38   Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
  39   Assert(candidates.size() > 0);
  40   if (candidates.size() > 1)
  41   {
  42     return false;
  43   }
  44   d_candidate = candidates[0];
  45   Trace("cegis-unif") << "Initialize unif utility for " << d_candidate
  46                       << "...\n";
  47   d_sygus_unif.initialize(d_qe, candidates, d_enums, lemmas);
  48   Assert(!d_enums.empty());
  49   Trace("cegis-unif") << "Initialize " << d_enums.size() << " enumerators for "
  50                       << d_candidate << "...\n";
  51   /* initialize the enumerators */
  52   for (const Node& e : d_enums)
  53   {
  54     d_tds->registerEnumerator(e, d_candidate, d_parent, true);
  55     Node g = d_tds->getActiveGuardForEnumerator(e);
  56     d_enum_to_active_guard[e] = g;
  57   }
  58   return true;
  59 }
  60
  61 void CegisUnif::getTermList(const std::vector<Node>& candidates,
  62                             std::vector<Node>& terms)
  63 {
  64   Assert(candidates.size() == 1);
  65   Valuation& valuation = d_qe->getValuation();
  66   for (const Node& e : d_enums)
  67   {
  68     Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
  69     Node g = d_enum_to_active_guard[e];
  70     /* Get whether the active guard for this enumerator is if so, then there may
  71        exist more values for it, and hence we add it to terms. */
  72     Node gstatus = valuation.getSatValue(g);
  73     if (!gstatus.isNull() && gstatus.getConst<bool>())
  74     {
  75       terms.push_back(e);
  76     }
  77   }
  78 }
  79
  80 bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
  81                                     const std::vector<Node>& enum_values,
  82                                     const std::vector<Node>& candidates,
  83                                     std::vector<Node>& candidate_values,
  84                                     std::vector<Node>& lems)
  85 {
  86   Assert(enums.size() == enum_values.size());
  87   if (enums.empty())
  88   {
  89     return false;
  90   }
  91   unsigned min_term_size = 0;
  92   std::vector<unsigned> enum_consider;
  93   Trace("cegis-unif-enum") << "Register new enumerated values :\n";
  94   for (unsigned i = 0, size = enums.size(); i < size; ++i)
  95   {
  96     Trace("cegis-unif-enum") << "  " << enums[i] << " -> " << enum_values[i]
  97                              << std::endl;
  98     unsigned sz = d_tds->getSygusTermSize(enum_values[i]);
  99     if (i == 0 || sz < min_term_size)
 100     {
 101       enum_consider.clear();
 102       min_term_size = sz;
 103       enum_consider.push_back(i);
 104     }
 105     else if (sz == min_term_size)
 106     {
 107       enum_consider.push_back(i);
 108     }
 109   }
 110   /* only consider the enumerators that are at minimum size (for fairness) */
 111   Trace("cegis-unif-enum") << "...register " << enum_consider.size() << " / "
 112                            << enums.size() << std::endl;
 113   NodeManager* nm = NodeManager::currentNM();
 114   for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; ++i)
 115   {
 116     unsigned j = enum_consider[i];
 117     Node e = enums[j];
 118     Node v = enum_values[j];
 119     std::vector<Node> enum_lems;
 120     d_sygus_unif.notifyEnumeration(e, v, enum_lems);
 121     /* the lemmas must be guarded by the active guard of the enumerator */
 122     Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
 123     Node g = d_enum_to_active_guard[e];
 124     for (unsigned j = 0, size = enum_lems.size(); j < size; ++j)
 125     {
 126       enum_lems[j] = nm->mkNode(OR, g.negate(), enum_lems[j]);
 127     }
 128     lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
 129   }
 130   /* build candidate solution */
 131   Assert(candidates.size() == 1);
 132   if (d_sygus_unif.constructSolution(candidate_values))
 133   {
 134     Node vc = candidate_values[0];
 135     Trace("cegis-unif-enum") << "... candidate solution :" << vc << "\n";
 136     return true;
 137   }
 138   return false;
 139 }
 140
 141 Node CegisUnif::purifyLemma(Node n,
 142                             bool ensureConst,
 143                             std::vector<Node>& model_guards,
 144                             BoolNodePairMap& cache)
 145 {
 146   Trace("cegis-unif-purify") << "PurifyLemma : " << n << "\n";
 147   BoolNodePairMap::const_iterator it = cache.find(BoolNodePair(ensureConst, n));
 148   if (it != cache.end())
 149   {
 150     Trace("cegis-unif-purify") << "... already visited " << n << "\n";
 151     return it->second;
 152   }
 153   /* Recurse */
 154   unsigned size = n.getNumChildren();
 155   Kind k = n.getKind();
 156   bool fapp = k == APPLY_UF && size > 0 && n[0] == d_candidate;
 157   bool childChanged = false;
 158   std::vector<Node> children;
 159   for (unsigned i = 0; i < size; ++i)
 160   {
 161     if (i == 0 && fapp)
 162     {
 163       children.push_back(n[0]);
 164       continue;
 165     }
 166     Node child = purifyLemma(n[i], ensureConst || fapp, model_guards, cache);
 167     children.push_back(child);
 168     childChanged = childChanged || child != n[i];
 169   }
 170   Node nb;
 171   if (childChanged)
 172   {
 173     if (n.hasOperator())
 174     {
 175       children.insert(children.begin(), n.getOperator());
 176     }
 177     nb = NodeManager::currentNM()->mkNode(k, children);
 178     Trace("cegis-unif-purify") << "PurifyLemma : transformed " << n << " into "
 179                                << nb << "\n";
 180   }
 181   else
 182   {
 183     nb = n;
 184   }
 185   /* get model value of non-top level applications of d_candidate */
 186   if (ensureConst && fapp)
 187   {
 188     Node nv = d_parent->getModelValue(nb);
 189     Trace("cegis-unif-purify") << "PurifyLemma : model value for " << nb
 190                                << " is " << nv << "\n";
 191     /* test if different, then update model_guards */
 192     if (nv != nb)
 193     {
 194       Trace("cegis-unif-purify") << "PurifyLemma : adding model eq\n";
 195       model_guards.push_back(
 196           NodeManager::currentNM()->mkNode(EQUAL, nv, nb).negate());
 197       nb = nv;
 198     }
 199   }
 200   nb = Rewriter::rewrite(nb);
 201   /* every non-top level application of function-to-synthesize must be reduced
 202      to a concrete constant */
 203   Assert(!ensureConst || nb.isConst());
 204   Trace("cegis-unif-purify") << "... caching [" << n << "] = " << nb << "\n";
 205   cache[BoolNodePair(ensureConst, n)] = nb;
 206   return nb;
 207 }
 208
 209 void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
 210                                         Node lem,
 211                                         std::vector<Node>& lems)
 212 {
 213   Node plem;
 214   std::vector<Node> model_guards;
 215   BoolNodePairMap cache;
 216   Trace("cegis-unif") << "Registering lemma at CegisUnif : " << lem << "\n";
 217   /* Make the purified lemma which will guide the unification utility. */
 218   plem = purifyLemma(lem, false, model_guards, cache);
 219   if (!model_guards.empty())
 220   {
 221     model_guards.push_back(plem);
 222     plem = NodeManager::currentNM()->mkNode(OR, model_guards);
 223   }
 224   plem = Rewriter::rewrite(plem);
 225   Trace("cegis-unif") << "Purified lemma : " << plem << "\n";
 226   d_refinement_lemmas.push_back(plem);
 227   /* Notify lemma to unification utility */
 228   d_sygus_unif.addRefLemma(plem);
 229   /* Make the refinement lemma and add it to lems. This lemma is guarded by the
 230      parent's guard, which has the semantics "this conjecture has a solution",
 231      hence this lemma states: if the parent conjecture has a solution, it
 232      satisfies the specification for the given concrete point. */
 233   /* Store lemma for external modules */
 234   lems.push_back(
 235       NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem));
 236 }
 237
 238 }  // namespace quantifiers
 239 }  // namespace theory
 240 }  // namespace CVC4