src/theory/quantifiers/sygus_inst.cpp

   1 /*********************                                                        */
   2 /*! \file sygus_inst.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Mathias Preiner, Andrew Reynolds
   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 instantiator class.
  13  **/
  14
  15 #include "theory/quantifiers/sygus_inst.h"
  16
  17 #include <sstream>
  18 #include <unordered_set>
  19
  20 #include "expr/node_algorithm.h"
  21 #include "theory/datatypes/sygus_datatype_utils.h"
  22 #include "theory/quantifiers/sygus/sygus_enumerator.h"
  23 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
  24 #include "theory/quantifiers/sygus/synth_engine.h"
  25 #include "theory/quantifiers_engine.h"
  26 #include "theory/theory_engine.h"
  27
  28 namespace CVC4 {
  29 namespace theory {
  30 namespace quantifiers {
  31
  32 SygusInst::SygusInst(QuantifiersEngine* qe)
  33     : QuantifiersModule(qe),
  34       d_lemma_cache(qe->getUserContext()),
  35       d_ce_lemma_added(qe->getUserContext())
  36 {
  37 }
  38
  39 bool SygusInst::needsCheck(Theory::Effort e)
  40 {
  41   return e >= Theory::EFFORT_LAST_CALL;
  42 }
  43
  44 QuantifiersModule::QEffort SygusInst::needsModel(Theory::Effort e)
  45 {
  46   return QEFFORT_STANDARD;
  47 }
  48
  49 void SygusInst::reset_round(Theory::Effort e)
  50 {
  51   d_active_quant.clear();
  52   d_inactive_quant.clear();
  53
  54   FirstOrderModel* model = d_quantEngine->getModel();
  55   uint32_t nasserted = model->getNumAssertedQuantifiers();
  56
  57   for (uint32_t i = 0; i < nasserted; ++i)
  58   {
  59     Node q = model->getAssertedQuantifier(i);
  60
  61     if (model->isQuantifierActive(q))
  62     {
  63       d_active_quant.insert(q);
  64       Node lit = getCeLiteral(q);
  65
  66       bool value;
  67       if (d_quantEngine->getValuation().hasSatValue(lit, value))
  68       {
  69         if (!value)
  70         {
  71           if (!d_quantEngine->getValuation().isDecision(lit))
  72           {
  73             model->setQuantifierActive(q, false);
  74             d_active_quant.erase(q);
  75             d_inactive_quant.insert(q);
  76             Trace("sygus-inst") << "Set inactive: " << q << std::endl;
  77           }
  78         }
  79       }
  80     }
  81   }
  82 }
  83
  84 void SygusInst::check(Theory::Effort e, QEffort quant_e)
  85 {
  86   Trace("sygus-inst") << "Check " << e << ", " << quant_e << std::endl;
  87
  88   if (quant_e != QEFFORT_STANDARD) return;
  89
  90   FirstOrderModel* model = d_quantEngine->getModel();
  91   Instantiate* inst = d_quantEngine->getInstantiate();
  92   TermDbSygus* db = d_quantEngine->getTermDatabaseSygus();
  93   SygusExplain syexplain(db);
  94   NodeManager* nm = NodeManager::currentNM();
  95
  96   for (const Node& q : d_active_quant)
  97   {
  98     std::vector<Node> terms;
  99     for (const Node& var : q[0])
 100     {
 101       Node dt_var = d_inst_constants[var];
 102       Node dt_eval = d_var_eval[var];
 103       Node value = model->getValue(dt_var);
 104       Node t = datatypes::utils::sygusToBuiltin(value);
 105       terms.push_back(t);
 106
 107       std::vector<Node> exp;
 108       syexplain.getExplanationForEquality(dt_var, value, exp);
 109       Node lem;
 110       if (exp.empty())
 111       {
 112         lem = dt_eval.eqNode(t);
 113       }
 114       else
 115       {
 116         lem = nm->mkNode(kind::IMPLIES,
 117                          exp.size() == 1 ? exp[0] : nm->mkNode(kind::AND, exp),
 118                          dt_eval.eqNode(t));
 119       }
 120
 121       if (d_lemma_cache.find(lem) == d_lemma_cache.end())
 122       {
 123         Trace("sygus-inst") << "Evaluation unfolding: " << lem << std::endl;
 124         d_quantEngine->addLemma(lem, false);
 125         d_lemma_cache.insert(lem);
 126       }
 127     }
 128
 129     if (inst->addInstantiation(q, terms))
 130     {
 131       Trace("sygus-inst") << "Instantiate " << q << std::endl;
 132     }
 133   }
 134 }
 135
 136 bool SygusInst::checkCompleteFor(Node q)
 137 {
 138   return d_inactive_quant.find(q) != d_inactive_quant.end();
 139 }
 140
 141 void SygusInst::registerQuantifier(Node q)
 142 {
 143   Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
 144
 145   Trace("sygus-inst") << "Register " << q << std::endl;
 146
 147   std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
 148   std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exclude_cons;
 149   std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> include_cons;
 150   std::unordered_set<Node, NodeHashFunction> term_irrelevant;
 151
 152   /* Collect extra symbols in 'q' to be used in the grammar. */
 153   std::unordered_set<Node, NodeHashFunction> syms;
 154   expr::getSymbols(q, syms);
 155   for (const TNode& var : syms)
 156   {
 157     TypeNode tn = var.getType();
 158     extra_cons[tn].insert(var);
 159     Trace("sygus-inst") << "Found symbol: " << var << std::endl;
 160   }
 161
 162   /* Construct grammar for each bound variable of 'q'. */
 163   Trace("sygus-inst") << "Process variables of " << q << std::endl;
 164   std::vector<TypeNode> types;
 165   for (const Node& var : q[0])
 166   {
 167     TypeNode tn = CegGrammarConstructor::mkSygusDefaultType(var.getType(),
 168                                                             Node(),
 169                                                             var.toString(),
 170                                                             extra_cons,
 171                                                             exclude_cons,
 172                                                             include_cons,
 173                                                             term_irrelevant);
 174     types.push_back(tn);
 175
 176     Trace("sygus-inst") << "Construct (default) datatype for " << var
 177                         << std::endl
 178                         << tn << std::endl;
 179   }
 180
 181   registerCeLemma(q, types);
 182 }
 183
 184 /* Construct grammars for all bound variables of quantifier 'q'. Currently,
 185  * we use the default grammar of the variable's type.
 186  */
 187 void SygusInst::preRegisterQuantifier(Node q)
 188 {
 189   Trace("sygus-inst") << "preRegister " << q << std::endl;
 190   addCeLemma(q);
 191 }
 192
 193 /*****************************************************************************/
 194 /* private methods                                                           */
 195 /*****************************************************************************/
 196
 197 Node SygusInst::getCeLiteral(Node q)
 198 {
 199   auto it = d_ce_lits.find(q);
 200   if (it != d_ce_lits.end())
 201   {
 202     return it->second;
 203   }
 204
 205   NodeManager* nm = NodeManager::currentNM();
 206   Node sk = nm->mkSkolem("CeLiteral", nm->booleanType());
 207   Node lit = d_quantEngine->getValuation().ensureLiteral(sk);
 208   d_ce_lits[q] = lit;
 209   return lit;
 210 }
 211
 212 void SygusInst::registerCeLemma(Node q, std::vector<TypeNode>& types)
 213 {
 214   Assert(q[0].getNumChildren() == types.size());
 215   Assert(d_ce_lemmas.find(q) == d_ce_lemmas.end());
 216
 217   /* Generate counterexample lemma for 'q'. */
 218   NodeManager* nm = NodeManager::currentNM();
 219   TermDbSygus* db = d_quantEngine->getTermDatabaseSygus();
 220
 221   /* For each variable x_i of \forall x_i . P[x_i], create a fresh datatype
 222    * instantiation constant ic_i with type types[i] and wrap each ic_i in
 223    * DT_SYGUS_EVAL(ic_i), which will be used to instantiate x_i. */
 224   std::vector<Node> vars;
 225   std::vector<Node> evals;
 226   for (size_t i = 0, size = types.size(); i < size; ++i)
 227   {
 228     TypeNode tn = types[i];
 229     TNode var = q[0][i];
 230
 231     /* Create the instantiation constant and set attribute accordingly. */
 232     Node ic = nm->mkInstConstant(tn);
 233     InstConstantAttribute ica;
 234     ic.setAttribute(ica, q);
 235
 236     db->registerEnumerator(ic, ic, nullptr, ROLE_ENUM_MULTI_SOLUTION);
 237
 238     std::vector<Node> args = {ic};
 239     Node svl = tn.getDType().getSygusVarList();
 240     if (!svl.isNull())
 241     {
 242       args.insert(args.end(), svl.begin(), svl.end());
 243     }
 244     Node eval = nm->mkNode(kind::DT_SYGUS_EVAL, args);
 245
 246     d_inst_constants.emplace(std::make_pair(var, ic));
 247     d_var_eval.emplace(std::make_pair(var, eval));
 248
 249     vars.push_back(var);
 250     evals.push_back(eval);
 251   }
 252
 253   Node lit = getCeLiteral(q);
 254   d_quantEngine->addRequirePhase(lit, true);
 255
 256   /* The decision strategy for quantified formula 'q' ensures that its
 257    * counterexample literal is decided on first. It is user-context dependent.
 258    */
 259   Assert(d_dstrat.find(q) == d_dstrat.end());
 260   DecisionStrategy* ds =
 261       new DecisionStrategySingleton("CeLiteral",
 262                                     lit,
 263                                     d_quantEngine->getSatContext(),
 264                                     d_quantEngine->getValuation());
 265
 266   d_dstrat[q].reset(ds);
 267   d_quantEngine->getDecisionManager()->registerStrategy(
 268       DecisionManager::STRAT_QUANT_CEGQI_FEASIBLE, ds);
 269
 270   /* Add counterexample lemma (lit => ~P[x_i/eval_i]) */
 271   Node body =
 272       q[1].substitute(vars.begin(), vars.end(), evals.begin(), evals.end());
 273   Node lem = nm->mkNode(kind::OR, lit.negate(), body.negate());
 274   lem = Rewriter::rewrite(lem);
 275
 276   d_ce_lemmas.emplace(std::make_pair(q, lem));
 277   Trace("sygus-inst") << "Register CE Lemma: " << lem << std::endl;
 278 }
 279
 280 void SygusInst::addCeLemma(Node q)
 281 {
 282   Assert(d_ce_lemmas.find(q) != d_ce_lemmas.end());
 283
 284   /* Already added in previous contexts. */
 285   if (d_ce_lemma_added.find(q) != d_ce_lemma_added.end()) return;
 286
 287   Node lem = d_ce_lemmas[q];
 288   d_quantEngine->addLemma(lem, false);
 289   d_ce_lemma_added.insert(q);
 290   Trace("sygus-inst") << "Add CE Lemma: " << lem << std::endl;
 291 }
 292
 293 }  // namespace quantifiers
 294 }  // namespace theory
 295 }  // namespace CVC4