src/smt/sygus_solver.cpp

   1 /*********************                                                        */
   2 /*! \file sygus_solver.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
   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 The solver for sygus queries
  13  **/
  14
  15 #include "smt/sygus_solver.h"
  16
  17 #include "expr/dtype.h"
  18 #include "options/quantifiers_options.h"
  19 #include "options/smt_options.h"
  20 #include "printer/printer.h"
  21 #include "smt/dump.h"
  22 #include "smt/preprocessor.h"
  23 #include "smt/smt_solver.h"
  24 #include "theory/quantifiers/quantifiers_attributes.h"
  25 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
  26 #include "theory/smt_engine_subsolver.h"
  27
  28 using namespace CVC4::theory;
  29 using namespace CVC4::kind;
  30
  31 namespace CVC4 {
  32 namespace smt {
  33
  34 SygusSolver::SygusSolver(SmtSolver& sms,
  35                          Preprocessor& pp,
  36                          context::UserContext* u,
  37                          OutputManager& outMgr)
  38     : d_smtSolver(sms),
  39       d_pp(pp),
  40       d_sygusConjectureStale(u, true),
  41       d_outMgr(outMgr)
  42 {
  43 }
  44
  45 SygusSolver::~SygusSolver() {}
  46
  47 void SygusSolver::declareSygusVar(const std::string& id,
  48                                   Node var,
  49                                   TypeNode type)
  50 {
  51   Trace("smt") << "SygusSolver::declareSygusVar: " << id << " " << var << " "
  52                << type << "\n";
  53   Assert(var.getType() == type);
  54   d_sygusVars.push_back(var);
  55   // don't need to set that the conjecture is stale
  56 }
  57
  58 void SygusSolver::declareSynthFun(const std::string& id,
  59                                   Node fn,
  60                                   TypeNode sygusType,
  61                                   bool isInv,
  62                                   const std::vector<Node>& vars)
  63 {
  64   Trace("smt") << "SygusSolver::declareSynthFun: " << id << "\n";
  65   NodeManager* nm = NodeManager::currentNM();
  66   d_sygusFunSymbols.push_back(fn);
  67   if (!vars.empty())
  68   {
  69     Node bvl = nm->mkNode(BOUND_VAR_LIST, vars);
  70     // use an attribute to mark its bound variable list
  71     SygusSynthFunVarListAttribute ssfvla;
  72     fn.setAttribute(ssfvla, bvl);
  73   }
  74   // whether sygus type encodes syntax restrictions
  75   if (sygusType.isDatatype() && sygusType.getDType().isSygus())
  76   {
  77     Node sym = nm->mkBoundVar("sfproxy", sygusType);
  78     // use an attribute to mark its grammar
  79     SygusSynthGrammarAttribute ssfga;
  80     fn.setAttribute(ssfga, sym);
  81   }
  82
  83   // sygus conjecture is now stale
  84   setSygusConjectureStale();
  85 }
  86
  87 void SygusSolver::assertSygusConstraint(Node constraint)
  88 {
  89   Trace("smt") << "SygusSolver::assertSygusConstrant: " << constraint << "\n";
  90   d_sygusConstraints.push_back(constraint);
  91
  92   // sygus conjecture is now stale
  93   setSygusConjectureStale();
  94 }
  95
  96 void SygusSolver::assertSygusInvConstraint(Node inv,
  97                                            Node pre,
  98                                            Node trans,
  99                                            Node post)
 100 {
 101   Trace("smt") << "SygusSolver::assertSygusInvConstrant: " << inv << " " << pre
 102                << " " << trans << " " << post << "\n";
 103   // build invariant constraint
 104
 105   // get variables (regular and their respective primed versions)
 106   std::vector<Node> terms;
 107   std::vector<Node> vars;
 108   std::vector<Node> primed_vars;
 109   terms.push_back(inv);
 110   terms.push_back(pre);
 111   terms.push_back(trans);
 112   terms.push_back(post);
 113   // variables are built based on the invariant type
 114   NodeManager* nm = NodeManager::currentNM();
 115   std::vector<TypeNode> argTypes = inv.getType().getArgTypes();
 116   for (const TypeNode& tn : argTypes)
 117   {
 118     vars.push_back(nm->mkBoundVar(tn));
 119     d_sygusVars.push_back(vars.back());
 120     std::stringstream ss;
 121     ss << vars.back() << "'";
 122     primed_vars.push_back(nm->mkBoundVar(ss.str(), tn));
 123     d_sygusVars.push_back(primed_vars.back());
 124   }
 125
 126   // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
 127   for (unsigned i = 0; i < 4; ++i)
 128   {
 129     Node op = terms[i];
 130     Trace("smt-debug") << "Make inv-constraint term #" << i << " : " << op
 131                        << " with type " << op.getType() << "...\n";
 132     std::vector<Node> children;
 133     children.push_back(op);
 134     // transition relation applied over both variable lists
 135     if (i == 2)
 136     {
 137       children.insert(children.end(), vars.begin(), vars.end());
 138       children.insert(children.end(), primed_vars.begin(), primed_vars.end());
 139     }
 140     else
 141     {
 142       children.insert(children.end(), vars.begin(), vars.end());
 143     }
 144     terms[i] = nm->mkNode(APPLY_UF, children);
 145     // make application of Inv on primed variables
 146     if (i == 0)
 147     {
 148       children.clear();
 149       children.push_back(op);
 150       children.insert(children.end(), primed_vars.begin(), primed_vars.end());
 151       terms.push_back(nm->mkNode(APPLY_UF, children));
 152     }
 153   }
 154   // make constraints
 155   std::vector<Node> conj;
 156   conj.push_back(nm->mkNode(IMPLIES, terms[1], terms[0]));
 157   Node term0_and_2 = nm->mkNode(AND, terms[0], terms[2]);
 158   conj.push_back(nm->mkNode(IMPLIES, term0_and_2, terms[4]));
 159   conj.push_back(nm->mkNode(IMPLIES, terms[0], terms[3]));
 160   Node constraint = nm->mkNode(AND, conj);
 161
 162   d_sygusConstraints.push_back(constraint);
 163
 164   // sygus conjecture is now stale
 165   setSygusConjectureStale();
 166 }
 167
 168 Result SygusSolver::checkSynth(Assertions& as)
 169 {
 170   if (options::incrementalSolving())
 171   {
 172     // TODO (project #7)
 173     throw ModalException(
 174         "Cannot make check-synth commands when incremental solving is enabled");
 175   }
 176   Trace("smt") << "SygusSolver::checkSynth" << std::endl;
 177   std::vector<Node> query;
 178   if (d_sygusConjectureStale)
 179   {
 180     NodeManager* nm = NodeManager::currentNM();
 181     // build synthesis conjecture from asserted constraints and declared
 182     // variables/functions
 183     Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
 184     Node inst_attr = nm->mkNode(INST_ATTRIBUTE, sygusVar);
 185     Node sygusAttr = nm->mkNode(INST_PATTERN_LIST, inst_attr);
 186     std::vector<Node> bodyv;
 187     Trace("smt") << "Sygus : Constructing sygus constraint...\n";
 188     size_t nconstraints = d_sygusConstraints.size();
 189     Node body = nconstraints == 0
 190                     ? nm->mkConst(true)
 191                     : (nconstraints == 1 ? d_sygusConstraints[0]
 192                                          : nm->mkNode(AND, d_sygusConstraints));
 193     body = body.notNode();
 194     Trace("smt") << "...constructed sygus constraint " << body << std::endl;
 195     if (!d_sygusVars.empty())
 196     {
 197       Node boundVars = nm->mkNode(BOUND_VAR_LIST, d_sygusVars);
 198       body = nm->mkNode(EXISTS, boundVars, body);
 199       Trace("smt") << "...constructed exists " << body << std::endl;
 200     }
 201     if (!d_sygusFunSymbols.empty())
 202     {
 203       Node boundVars = nm->mkNode(BOUND_VAR_LIST, d_sygusFunSymbols);
 204       body = nm->mkNode(FORALL, boundVars, body, sygusAttr);
 205     }
 206     Trace("smt") << "...constructed forall " << body << std::endl;
 207
 208     // set attribute for synthesis conjecture
 209     SygusAttribute sa;
 210     sygusVar.setAttribute(sa, true);
 211
 212     Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
 213     if (Dump.isOn("raw-benchmark"))
 214     {
 215       d_outMgr.getPrinter().toStreamCmdCheckSynth(d_outMgr.getDumpOut());
 216     }
 217
 218     d_sygusConjectureStale = false;
 219
 220     // TODO (project #7): if incremental, we should push a context and assert
 221     query.push_back(body);
 222   }
 223
 224   Result r = d_smtSolver.checkSatisfiability(as, query, false, false);
 225
 226   // Check that synthesis solutions satisfy the conjecture
 227   if (options::checkSynthSol()
 228       && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
 229   {
 230     checkSynthSolution(as);
 231   }
 232   return r;
 233 }
 234
 235 bool SygusSolver::getSynthSolutions(std::map<Node, Node>& sol_map)
 236 {
 237   Trace("smt") << "SygusSolver::getSynthSolutions" << std::endl;
 238   std::map<Node, std::map<Node, Node>> sol_mapn;
 239   // fail if the theory engine does not have synthesis solutions
 240   TheoryEngine* te = d_smtSolver.getTheoryEngine();
 241   Assert(te != nullptr);
 242   if (!te->getSynthSolutions(sol_mapn))
 243   {
 244     return false;
 245   }
 246   for (std::pair<const Node, std::map<Node, Node>>& cs : sol_mapn)
 247   {
 248     for (std::pair<const Node, Node>& s : cs.second)
 249     {
 250       sol_map[s.first] = s.second;
 251     }
 252   }
 253   return true;
 254 }
 255
 256 void SygusSolver::checkSynthSolution(Assertions& as)
 257 {
 258   NodeManager* nm = NodeManager::currentNM();
 259   Notice() << "SygusSolver::checkSynthSolution(): checking synthesis solution"
 260            << std::endl;
 261   std::map<Node, std::map<Node, Node>> sol_map;
 262   // Get solutions and build auxiliary vectors for substituting
 263   TheoryEngine* te = d_smtSolver.getTheoryEngine();
 264   if (!te->getSynthSolutions(sol_map))
 265   {
 266     InternalError()
 267         << "SygusSolver::checkSynthSolution(): No solution to check!";
 268     return;
 269   }
 270   if (sol_map.empty())
 271   {
 272     InternalError() << "SygusSolver::checkSynthSolution(): Got empty solution!";
 273     return;
 274   }
 275   Trace("check-synth-sol") << "Got solution map:\n";
 276   // the set of synthesis conjectures in our assertions
 277   std::unordered_set<Node, NodeHashFunction> conjs;
 278   // For each of the above conjectures, the functions-to-synthesis and their
 279   // solutions. This is used as a substitution below.
 280   std::map<Node, std::vector<Node>> fvarMap;
 281   std::map<Node, std::vector<Node>> fsolMap;
 282   for (const std::pair<const Node, std::map<Node, Node>>& cmap : sol_map)
 283   {
 284     Trace("check-synth-sol") << "For conjecture " << cmap.first << ":\n";
 285     conjs.insert(cmap.first);
 286     std::vector<Node>& fvars = fvarMap[cmap.first];
 287     std::vector<Node>& fsols = fsolMap[cmap.first];
 288     for (const std::pair<const Node, Node>& pair : cmap.second)
 289     {
 290       Trace("check-synth-sol")
 291           << "  " << pair.first << " --> " << pair.second << "\n";
 292       fvars.push_back(pair.first);
 293       fsols.push_back(pair.second);
 294     }
 295   }
 296   Trace("check-synth-sol") << "Starting new SMT Engine\n";
 297
 298   Trace("check-synth-sol") << "Retrieving assertions\n";
 299   // Build conjecture from original assertions
 300   context::CDList<Node>* alist = as.getAssertionList();
 301   if (alist == nullptr)
 302   {
 303     Trace("check-synth-sol") << "No assertions to check\n";
 304     return;
 305   }
 306   // auxiliary assertions
 307   std::vector<Node> auxAssertions;
 308   // expand definitions cache
 309   std::unordered_map<Node, Node, NodeHashFunction> cache;
 310   for (Node assertion : *alist)
 311   {
 312     Notice() << "SygusSolver::checkSynthSolution(): checking assertion "
 313              << assertion << std::endl;
 314     Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n";
 315     // Apply any define-funs from the problem.
 316     Node n = d_pp.expandDefinitions(assertion, cache);
 317     Notice() << "SygusSolver::checkSynthSolution(): -- expands to " << n
 318              << std::endl;
 319     Trace("check-synth-sol") << "Expanded assertion " << n << "\n";
 320     if (conjs.find(n) == conjs.end())
 321     {
 322       Trace("check-synth-sol") << "It is an auxiliary assertion\n";
 323       auxAssertions.push_back(n);
 324     }
 325     else
 326     {
 327       Trace("check-synth-sol") << "It is a synthesis conjecture\n";
 328     }
 329   }
 330   // check all conjectures
 331   for (Node conj : conjs)
 332   {
 333     // Start new SMT engine to check solutions
 334     std::unique_ptr<SmtEngine> solChecker;
 335     initializeSubsolver(solChecker);
 336     solChecker->getOptions().set(options::checkSynthSol, false);
 337     solChecker->getOptions().set(options::sygusRecFun, false);
 338     // get the solution for this conjecture
 339     std::vector<Node>& fvars = fvarMap[conj];
 340     std::vector<Node>& fsols = fsolMap[conj];
 341     // Apply solution map to conjecture body
 342     Node conjBody;
 343     /* Whether property is quantifier free */
 344     if (conj[1].getKind() != EXISTS)
 345     {
 346       conjBody = conj[1].substitute(
 347           fvars.begin(), fvars.end(), fsols.begin(), fsols.end());
 348     }
 349     else
 350     {
 351       conjBody = conj[1][1].substitute(
 352           fvars.begin(), fvars.end(), fsols.begin(), fsols.end());
 353
 354       /* Skolemize property */
 355       std::vector<Node> vars, skos;
 356       for (unsigned j = 0, size = conj[1][0].getNumChildren(); j < size; ++j)
 357       {
 358         vars.push_back(conj[1][0][j]);
 359         std::stringstream ss;
 360         ss << "sk_" << j;
 361         skos.push_back(nm->mkSkolem(ss.str(), conj[1][0][j].getType()));
 362         Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to "
 363                                  << skos.back() << "\n";
 364       }
 365       conjBody = conjBody.substitute(
 366           vars.begin(), vars.end(), skos.begin(), skos.end());
 367     }
 368     Notice() << "SygusSolver::checkSynthSolution(): -- body substitutes to "
 369              << conjBody << std::endl;
 370     Trace("check-synth-sol")
 371         << "Substituted body of assertion to " << conjBody << "\n";
 372     solChecker->assertFormula(conjBody);
 373     // Assert all auxiliary assertions. This may include recursive function
 374     // definitions that were added as assertions to the sygus problem.
 375     for (Node a : auxAssertions)
 376     {
 377       solChecker->assertFormula(a);
 378     }
 379     Result r = solChecker->checkSat();
 380     Notice() << "SygusSolver::checkSynthSolution(): result is " << r
 381              << std::endl;
 382     Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
 383     if (r.asSatisfiabilityResult().isUnknown())
 384     {
 385       InternalError() << "SygusSolver::checkSynthSolution(): could not check "
 386                          "solution, result "
 387                          "unknown.";
 388     }
 389     else if (r.asSatisfiabilityResult().isSat())
 390     {
 391       InternalError()
 392           << "SygusSolver::checkSynthSolution(): produced solution leads to "
 393              "satisfiable negated conjecture.";
 394     }
 395   }
 396 }
 397
 398 void SygusSolver::setSygusConjectureStale()
 399 {
 400   if (d_sygusConjectureStale)
 401   {
 402     // already stale
 403     return;
 404   }
 405   d_sygusConjectureStale = true;
 406   // TODO (project #7): if incremental, we should pop a context
 407 }
 408
 409 }  // namespace smt
 410 }  // namespace CVC4