src/smt/sygus_solver.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Gereon Kremer, Haniel Barbosa
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2022 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.
  11  * ****************************************************************************
  12  *
  13  * The solver for SyGuS queries.
  14  */
  15
  16 #include "smt/sygus_solver.h"
  17
  18 #include <sstream>
  19
  20 #include "base/modal_exception.h"
  21 #include "expr/dtype.h"
  22 #include "expr/dtype_cons.h"
  23 #include "expr/skolem_manager.h"
  24 #include "options/base_options.h"
  25 #include "options/option_exception.h"
  26 #include "options/quantifiers_options.h"
  27 #include "options/smt_options.h"
  28 #include "smt/preprocessor.h"
  29 #include "smt/smt_solver.h"
  30 #include "theory/datatypes/sygus_datatype_utils.h"
  31 #include "theory/quantifiers/quantifiers_attributes.h"
  32 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
  33 #include "theory/quantifiers/sygus/sygus_utils.h"
  34 #include "theory/quantifiers_engine.h"
  35 #include "theory/rewriter.h"
  36 #include "theory/smt_engine_subsolver.h"
  37
  38 using namespace cvc5::internal::theory;
  39 using namespace cvc5::internal::kind;
  40
  41 namespace cvc5::internal {
  42 namespace smt {
  43
  44 SygusSolver::SygusSolver(Env& env, SmtSolver& sms)
  45     : EnvObj(env),
  46       d_smtSolver(sms),
  47       d_sygusVars(userContext()),
  48       d_sygusConstraints(userContext()),
  49       d_sygusAssumps(userContext()),
  50       d_sygusFunSymbols(userContext()),
  51       d_sygusConjectureStale(userContext(), true),
  52       d_subsolverCd(userContext(), nullptr)
  53 {
  54 }
  55
  56 SygusSolver::~SygusSolver() {}
  57
  58 void SygusSolver::declareSygusVar(Node var)
  59 {
  60   Trace("smt") << "SygusSolver::declareSygusVar: " << var << " "
  61                << var.getType() << "\n";
  62   d_sygusVars.push_back(var);
  63   // don't need to set that the conjecture is stale
  64 }
  65
  66 void SygusSolver::declareSynthFun(Node fn,
  67                                   TypeNode sygusType,
  68                                   bool isInv,
  69                                   const std::vector<Node>& vars)
  70 {
  71   Trace("smt") << "SygusSolver::declareSynthFun: " << fn << "\n";
  72   NodeManager* nm = NodeManager::currentNM();
  73   d_sygusFunSymbols.push_back(fn);
  74   if (!vars.empty())
  75   {
  76     Node bvl = nm->mkNode(BOUND_VAR_LIST, vars);
  77     // use an attribute to mark its bound variable list
  78     SygusSynthFunVarListAttribute ssfvla;
  79     fn.setAttribute(ssfvla, bvl);
  80   }
  81   // whether sygus type encodes syntax restrictions
  82   if (!sygusType.isNull() && sygusType.isDatatype()
  83       && sygusType.getDType().isSygus())
  84   {
  85     Node sym = nm->mkBoundVar("sfproxy", sygusType);
  86     // use an attribute to mark its grammar
  87     SygusSynthGrammarAttribute ssfga;
  88     fn.setAttribute(ssfga, sym);
  89     // we must expand definitions for sygus operators in the block
  90     expandDefinitionsSygusDt(sygusType);
  91   }
  92
  93   // sygus conjecture is now stale
  94   d_sygusConjectureStale = true;
  95 }
  96
  97 void SygusSolver::assertSygusConstraint(Node n, bool isAssume)
  98 {
  99   Trace("smt") << "SygusSolver::assertSygusConstrant: " << n
 100                << ", isAssume=" << isAssume << "\n";
 101   if (isAssume)
 102   {
 103     d_sygusAssumps.push_back(n);
 104   }
 105   else
 106   {
 107     d_sygusConstraints.push_back(n);
 108   }
 109
 110   // sygus conjecture is now stale
 111   d_sygusConjectureStale = true;
 112 }
 113
 114 void SygusSolver::assertSygusInvConstraint(Node inv,
 115                                            Node pre,
 116                                            Node trans,
 117                                            Node post)
 118 {
 119   Trace("smt") << "SygusSolver::assertSygusInvConstrant: " << inv << " " << pre
 120                << " " << trans << " " << post << "\n";
 121   // build invariant constraint
 122
 123   // get variables (regular and their respective primed versions)
 124   std::vector<Node> terms;
 125   std::vector<Node> vars;
 126   std::vector<Node> primed_vars;
 127   terms.push_back(inv);
 128   terms.push_back(pre);
 129   terms.push_back(trans);
 130   terms.push_back(post);
 131   // variables are built based on the invariant type
 132   NodeManager* nm = NodeManager::currentNM();
 133   std::vector<TypeNode> argTypes = inv.getType().getArgTypes();
 134   for (const TypeNode& tn : argTypes)
 135   {
 136     vars.push_back(nm->mkBoundVar(tn));
 137     d_sygusVars.push_back(vars.back());
 138     std::stringstream ss;
 139     ss << vars.back() << "'";
 140     primed_vars.push_back(nm->mkBoundVar(ss.str(), tn));
 141     d_sygusVars.push_back(primed_vars.back());
 142   }
 143
 144   // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
 145   for (unsigned i = 0; i < 4; ++i)
 146   {
 147     Node op = terms[i];
 148     Trace("smt-debug") << "Make inv-constraint term #" << i << " : " << op
 149                        << " with type " << op.getType() << "...\n";
 150     std::vector<Node> children;
 151     children.push_back(op);
 152     // transition relation applied over both variable lists
 153     if (i == 2)
 154     {
 155       children.insert(children.end(), vars.begin(), vars.end());
 156       children.insert(children.end(), primed_vars.begin(), primed_vars.end());
 157     }
 158     else
 159     {
 160       children.insert(children.end(), vars.begin(), vars.end());
 161     }
 162     terms[i] = nm->mkNode(APPLY_UF, children);
 163     // make application of Inv on primed variables
 164     if (i == 0)
 165     {
 166       children.clear();
 167       children.push_back(op);
 168       children.insert(children.end(), primed_vars.begin(), primed_vars.end());
 169       terms.push_back(nm->mkNode(APPLY_UF, children));
 170     }
 171   }
 172   // make constraints
 173   std::vector<Node> conj;
 174   conj.push_back(nm->mkNode(IMPLIES, terms[1], terms[0]));
 175   Node term0_and_2 = nm->mkNode(AND, terms[0], terms[2]);
 176   conj.push_back(nm->mkNode(IMPLIES, term0_and_2, terms[4]));
 177   conj.push_back(nm->mkNode(IMPLIES, terms[0], terms[3]));
 178   Node constraint = nm->mkNode(AND, conj);
 179
 180   d_sygusConstraints.push_back(constraint);
 181
 182   // sygus conjecture is now stale
 183   d_sygusConjectureStale = true;
 184 }
 185
 186 SynthResult SygusSolver::checkSynth(Assertions& as, bool isNext)
 187 {
 188   Trace("smt") << "SygusSolver::checkSynth" << std::endl;
 189   // if applicable, check if the subsolver is the correct one
 190   if (!isNext)
 191   {
 192     // if we are not using check-synth-next, we always reconstruct the solver.
 193     d_sygusConjectureStale = true;
 194   }
 195   if (usingSygusSubsolver() && d_subsolverCd.get() != d_subsolver.get())
 196   {
 197     // this can occur if we backtrack to a place where we were using a different
 198     // subsolver than the current one. In this case, we should reconstruct
 199     // the subsolver.
 200     d_sygusConjectureStale = true;
 201   }
 202   if (d_sygusConjectureStale)
 203   {
 204     NodeManager* nm = NodeManager::currentNM();
 205     // build synthesis conjecture from asserted constraints and declared
 206     // variables/functions
 207     Trace("smt") << "Sygus : Constructing sygus constraint...\n";
 208     Node body = nm->mkAnd(listToVector(d_sygusConstraints));
 209     // note that if there are no constraints, then assumptions are irrelevant
 210     if (!d_sygusConstraints.empty() && !d_sygusAssumps.empty())
 211     {
 212       Node bodyAssump = nm->mkAnd(listToVector(d_sygusAssumps));
 213       body = nm->mkNode(IMPLIES, bodyAssump, body);
 214     }
 215     body = body.notNode();
 216     Trace("smt") << "...constructed sygus constraint " << body << std::endl;
 217     if (!d_sygusVars.empty())
 218     {
 219       Node boundVars = nm->mkNode(BOUND_VAR_LIST, listToVector(d_sygusVars));
 220       body = nm->mkNode(EXISTS, boundVars, body);
 221       Trace("smt") << "...constructed exists " << body << std::endl;
 222     }
 223     if (!d_sygusFunSymbols.empty())
 224     {
 225       body = quantifiers::SygusUtils::mkSygusConjecture(
 226           listToVector(d_sygusFunSymbols), body);
 227     }
 228     Trace("smt") << "...constructed forall " << body << std::endl;
 229
 230     Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
 231
 232     d_sygusConjectureStale = false;
 233
 234     d_conj = body;
 235
 236     // if we are using a subsolver, initialize it now
 237     if (usingSygusSubsolver())
 238     {
 239       // we generate a new solver engine to do the SyGuS query
 240       initializeSygusSubsolver(d_subsolver, as);
 241
 242       // store the pointer (context-dependent)
 243       d_subsolverCd = d_subsolver.get();
 244
 245       // also assert the internal SyGuS conjecture
 246       d_subsolver->assertFormula(d_conj);
 247     }
 248   }
 249   else
 250   {
 251     Assert(d_subsolver != nullptr);
 252   }
 253   Result r;
 254   if (usingSygusSubsolver())
 255   {
 256     r = d_subsolver->checkSat();
 257   }
 258   else
 259   {
 260     std::vector<Node> query;
 261     query.push_back(d_conj);
 262     r = d_smtSolver.checkSatisfiability(as, query);
 263   }
 264   // The result returned by the above call is typically "unknown", which may
 265   // or may not correspond to a state in which we solved the conjecture
 266   // successfully. Instead we call getSynthSolutions below. If this returns
 267   // true, then we were successful. In this case, we set the synthesis result to
 268   // "solution".
 269   //
 270   // This behavior is done for 2 reasons:
 271   // (1) if we do not negate the synthesis conjecture, the subsolver in some
 272   // cases cannot answer "sat", e.g. in the presence of recursive function
 273   // definitions. Instead the SyGuS language standard itself indicates that
 274   // a correct solution for a conjecture is one where the synthesis conjecture
 275   // is *T-valid* (in the presence of defined recursive functions). In other
 276   // words, a SyGuS query asks to prove that the conjecture is valid when
 277   // witnessed by the given solution.
 278   // (2) we do not want the solver to explicitly answer "unsat" by giving an
 279   // unsatisfiable set of formulas to the underlying PropEngine, or otherwise
 280   // we will not be able to ask for further solutions. This is critical for
 281   // incremental solving where multiple solutions are returned for the same
 282   // set of constraints. Thus, the internal SyGuS solver will mark unknown
 283   // with IncompleteId::QUANTIFIERS_SYGUS_SOLVED. Furthermore, this id may be
 284   // overwritten by other means of incompleteness, so we cannot rely on this
 285   // identifier being the final reason for unknown.
 286   //
 287   // Thus, we use getSynthSolutions as means of knowing the conjecture was
 288   // solved.
 289   SynthResult sr;
 290   std::map<Node, Node> sol_map;
 291   if (getSynthSolutions(sol_map))
 292   {
 293     // if we have solutions, we return "solution"
 294     sr = SynthResult(SynthResult::SOLUTION);
 295     // Check that synthesis solutions satisfy the conjecture
 296     if (options().smt.checkSynthSol)
 297     {
 298       checkSynthSolution(as, sol_map);
 299     }
 300   }
 301   else
 302   {
 303     // otherwise, we return "unknown"
 304     sr = SynthResult(SynthResult::UNKNOWN, UnknownExplanation::UNKNOWN_REASON);
 305   }
 306   return sr;
 307 }
 308
 309 bool SygusSolver::getSynthSolutions(std::map<Node, Node>& solMap)
 310 {
 311   Trace("smt") << "SygusSolver::getSynthSolutions" << std::endl;
 312   if (usingSygusSubsolver())
 313   {
 314     // use the call to get the synth solutions from the subsolver
 315     return d_subsolver->getSubsolverSynthSolutions(solMap);
 316   }
 317   return getSubsolverSynthSolutions(solMap);
 318 }
 319
 320 bool SygusSolver::getSubsolverSynthSolutions(std::map<Node, Node>& solMap)
 321 {
 322   Trace("smt") << "SygusSolver::getSubsolverSynthSolutions" << std::endl;
 323   std::map<Node, std::map<Node, Node>> solMapn;
 324   // fail if the theory engine does not have synthesis solutions
 325   QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
 326   if (qe == nullptr || !qe->getSynthSolutions(solMapn))
 327   {
 328     return false;
 329   }
 330   for (std::pair<const Node, std::map<Node, Node>>& cs : solMapn)
 331   {
 332     for (std::pair<const Node, Node>& s : cs.second)
 333     {
 334       solMap[s.first] = s.second;
 335     }
 336   }
 337   return true;
 338 }
 339
 340 void SygusSolver::checkSynthSolution(Assertions& as,
 341                                      const std::map<Node, Node>& sol_map)
 342 {
 343   if (isVerboseOn(1))
 344   {
 345     verbose(1) << "SyGuS::checkSynthSolution: checking synthesis solution"
 346                << std::endl;
 347   }
 348   if (sol_map.empty())
 349   {
 350     InternalError() << "SygusSolver::checkSynthSolution(): Got empty solution!";
 351     return;
 352   }
 353   Trace("check-synth-sol") << "Got solution map:\n";
 354   // the set of synthesis conjectures in our assertions
 355   std::unordered_set<Node> conjs;
 356   conjs.insert(d_conj);
 357   // For each of the above conjectures, the functions-to-synthesis and their
 358   // solutions. This is used as a substitution below.
 359   std::vector<Node> fvars;
 360   std::vector<Node> fsols;
 361   for (const std::pair<const Node, Node>& pair : sol_map)
 362   {
 363     Trace("check-synth-sol")
 364         << "  " << pair.first << " --> " << pair.second << "\n";
 365     fvars.push_back(pair.first);
 366     fsols.push_back(pair.second);
 367   }
 368
 369   Trace("check-synth-sol") << "Starting new SMT Engine\n";
 370
 371   Trace("check-synth-sol") << "Retrieving assertions\n";
 372   // Build conjecture from original assertions
 373   // check all conjectures
 374   for (const Node& conj : conjs)
 375   {
 376     // Start new SMT engine to check solutions
 377     std::unique_ptr<SolverEngine> solChecker;
 378     initializeSygusSubsolver(solChecker, as);
 379     solChecker->getOptions().writeSmt().checkSynthSol = false;
 380     solChecker->getOptions().writeQuantifiers().sygusRecFun = false;
 381     Assert(conj.getKind() == FORALL);
 382     Node conjBody = conj[1];
 383     // we must expand definitions here, since define-fun may contain the
 384     // function-to-synthesize, which needs to be substituted.
 385     conjBody = d_smtSolver.getPreprocessor()->expandDefinitions(conjBody);
 386     // Apply solution map to conjecture body
 387     conjBody = conjBody.substitute(
 388         fvars.begin(), fvars.end(), fsols.begin(), fsols.end());
 389
 390     if (isVerboseOn(1))
 391     {
 392       verbose(1) << "SyGuS::checkSynthSolution: -- body substitutes to "
 393                  << conjBody << std::endl;
 394     }
 395     Trace("check-synth-sol")
 396         << "Substituted body of assertion to " << conjBody << "\n";
 397     solChecker->assertFormula(conjBody);
 398     Result r = solChecker->checkSat();
 399     if (isVerboseOn(1))
 400     {
 401       verbose(1) << "SyGuS::checkSynthSolution: result is " << r << std::endl;
 402     }
 403     Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
 404     if (r.isUnknown())
 405     {
 406       InternalError() << "SygusSolver::checkSynthSolution(): could not check "
 407                          "solution, result "
 408                          "unknown.";
 409     }
 410     else if (r.getStatus() == Result::SAT)
 411     {
 412       InternalError()
 413           << "SygusSolver::checkSynthSolution(): produced solution leads to "
 414              "satisfiable negated conjecture.";
 415     }
 416   }
 417 }
 418
 419 void SygusSolver::initializeSygusSubsolver(std::unique_ptr<SolverEngine>& se,
 420                                            Assertions& as)
 421 {
 422   initializeSubsolver(se, d_env);
 423   // carry the ordinary define-fun definitions
 424   const context::CDList<Node>& alistDefs = as.getAssertionListDefinitions();
 425   std::unordered_set<Node> processed;
 426   for (const Node& def : alistDefs)
 427   {
 428     // only consider define-fun, represented as (= f (lambda ...)).
 429     if (def.getKind() == EQUAL)
 430     {
 431       Assert(def[0].isVar());
 432       std::vector<Node> formals;
 433       Node dbody = def[1];
 434       if (def[1].getKind() == LAMBDA)
 435       {
 436         formals.insert(formals.end(), def[1][0].begin(), def[1][0].end());
 437         dbody = dbody[1];
 438       }
 439       se->defineFunction(def[0], formals, dbody);
 440       processed.insert(def);
 441     }
 442   }
 443   // Also assert auxiliary assertions
 444   const context::CDList<Node>& alist = as.getAssertionList();
 445   for (size_t i = 0, asize = alist.size(); i < asize; ++i)
 446   {
 447     Node a = alist[i];
 448     // ignore definitions here
 449     if (processed.find(a) == processed.end())
 450     {
 451       se->assertFormula(a);
 452     }
 453   }
 454 }
 455
 456 bool SygusSolver::usingSygusSubsolver() const
 457 {
 458   // use SyGuS subsolver if in incremental mode
 459   return options().base.incrementalSolving;
 460 }
 461
 462 void SygusSolver::expandDefinitionsSygusDt(TypeNode tn) const
 463 {
 464   std::unordered_set<TypeNode> processed;
 465   std::vector<TypeNode> toProcess;
 466   toProcess.push_back(tn);
 467   size_t index = 0;
 468   while (index < toProcess.size())
 469   {
 470     TypeNode tnp = toProcess[index];
 471     index++;
 472     Assert(tnp.isDatatype());
 473     Assert(tnp.getDType().isSygus());
 474     const std::vector<std::shared_ptr<DTypeConstructor>>& cons =
 475         tnp.getDType().getConstructors();
 476     for (const std::shared_ptr<DTypeConstructor>& c : cons)
 477     {
 478       Node op = c->getSygusOp();
 479       // Only expand definitions if the operator is not constant, since
 480       // calling expandDefinitions on them should be a no-op. This check
 481       // ensures we don't try to expand e.g. bitvector extract operators,
 482       // whose type is undefined, and thus should not be passed to
 483       // expandDefinitions.
 484       Node eop = op.isConst()
 485                      ? op
 486                      : d_smtSolver.getPreprocessor()->expandDefinitions(op);
 487       eop = rewrite(eop);
 488       datatypes::utils::setExpandedDefinitionForm(op, eop);
 489       // also must consider the arguments
 490       for (unsigned j = 0, nargs = c->getNumArgs(); j < nargs; ++j)
 491       {
 492         TypeNode tnc = c->getArgType(j);
 493         if (tnc.isDatatype() && tnc.getDType().isSygus()
 494             && processed.find(tnc) == processed.end())
 495         {
 496           toProcess.push_back(tnc);
 497           processed.insert(tnc);
 498         }
 499       }
 500     }
 501   }
 502 }
 503
 504 std::vector<Node> SygusSolver::listToVector(const NodeList& list)
 505 {
 506   std::vector<Node> vec;
 507   for (const Node& n : list)
 508   {
 509     vec.push_back(n);
 510   }
 511   return vec;
 512 }
 513
 514 }  // namespace smt
 515 }  // namespace cvc5::internal