Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/sygus_solver.cpp	Lines:	211	233	90.6 %
Date:	2021-11-06	Branches:	391	854	45.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * The solver for SyGuS queries.
 */

#include "smt/sygus_solver.h"

#include <sstream>

#include "base/modal_exception.h"
#include "expr/dtype.h"
#include "expr/dtype_cons.h"
#include "expr/skolem_manager.h"
#include "options/base_options.h"
#include "options/option_exception.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "smt/preprocessor.h"
#include "smt/smt_solver.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/quantifiers_attributes.h"
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
#include "theory/quantifiers/sygus/sygus_utils.h"
#include "theory/quantifiers_engine.h"
#include "theory/rewriter.h"
#include "theory/smt_engine_subsolver.h"

using namespace cvc5::theory;
using namespace cvc5::kind;

namespace cvc5 {
namespace smt {

SygusSolver::SygusSolver(Env& env, SmtSolver& sms)
    : EnvObj(env), d_smtSolver(sms), d_sygusConjectureStale(userContext(), true)
{
}

SygusSolver::~SygusSolver() {}

void SygusSolver::declareSygusVar(Node var)
{
  Trace("smt") << "SygusSolver::declareSygusVar: " << var << " "
               << var.getType() << "\n";
  d_sygusVars.push_back(var);
  // don't need to set that the conjecture is stale
}

void SygusSolver::declareSynthFun(Node fn,
                                  TypeNode sygusType,
                                  bool isInv,
                                  const std::vector<Node>& vars)
{
  Trace("smt") << "SygusSolver::declareSynthFun: " << fn << "\n";
  NodeManager* nm = NodeManager::currentNM();
  d_sygusFunSymbols.push_back(fn);
  if (!vars.empty())
  {
    Node bvl = nm->mkNode(BOUND_VAR_LIST, vars);
    // use an attribute to mark its bound variable list
    SygusSynthFunVarListAttribute ssfvla;
    fn.setAttribute(ssfvla, bvl);
  }
  // whether sygus type encodes syntax restrictions
  if (!sygusType.isNull() && sygusType.isDatatype()
      && sygusType.getDType().isSygus())
  {
    Node sym = nm->mkBoundVar("sfproxy", sygusType);
    // use an attribute to mark its grammar
    SygusSynthGrammarAttribute ssfga;
    fn.setAttribute(ssfga, sym);
    // we must expand definitions for sygus operators in the block
    expandDefinitionsSygusDt(sygusType);
  }

  // sygus conjecture is now stale
  setSygusConjectureStale();
}

void SygusSolver::assertSygusConstraint(Node n, bool isAssume)
{
  Trace("smt") << "SygusSolver::assertSygusConstrant: " << n
               << ", isAssume=" << isAssume << "\n";
  if (isAssume)
  {
    d_sygusAssumps.push_back(n);
  }
  else
  {
    d_sygusConstraints.push_back(n);
  }

  // sygus conjecture is now stale
  setSygusConjectureStale();
}

void SygusSolver::assertSygusInvConstraint(Node inv,
                                           Node pre,
                                           Node trans,
                                           Node post)
{
  Trace("smt") << "SygusSolver::assertSygusInvConstrant: " << inv << " " << pre
               << " " << trans << " " << post << "\n";
  // build invariant constraint

  // get variables (regular and their respective primed versions)
  std::vector<Node> terms;
  std::vector<Node> vars;
  std::vector<Node> primed_vars;
  terms.push_back(inv);
  terms.push_back(pre);
  terms.push_back(trans);
  terms.push_back(post);
  // variables are built based on the invariant type
  NodeManager* nm = NodeManager::currentNM();
  std::vector<TypeNode> argTypes = inv.getType().getArgTypes();
  for (const TypeNode& tn : argTypes)
  {
    vars.push_back(nm->mkBoundVar(tn));
    d_sygusVars.push_back(vars.back());
    std::stringstream ss;
    ss << vars.back() << "'";
    primed_vars.push_back(nm->mkBoundVar(ss.str(), tn));
    d_sygusVars.push_back(primed_vars.back());
  }

  // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
  for (unsigned i = 0; i < 4; ++i)
  {
    Node op = terms[i];
    Trace("smt-debug") << "Make inv-constraint term #" << i << " : " << op
                       << " with type " << op.getType() << "...\n";
    std::vector<Node> children;
    children.push_back(op);
    // transition relation applied over both variable lists
    if (i == 2)
    {
      children.insert(children.end(), vars.begin(), vars.end());
      children.insert(children.end(), primed_vars.begin(), primed_vars.end());
    }
    else
    {
      children.insert(children.end(), vars.begin(), vars.end());
    }
    terms[i] = nm->mkNode(APPLY_UF, children);
    // make application of Inv on primed variables
    if (i == 0)
    {
      children.clear();
      children.push_back(op);
      children.insert(children.end(), primed_vars.begin(), primed_vars.end());
      terms.push_back(nm->mkNode(APPLY_UF, children));
    }
  }
  // make constraints
  std::vector<Node> conj;
  conj.push_back(nm->mkNode(IMPLIES, terms[1], terms[0]));
  Node term0_and_2 = nm->mkNode(AND, terms[0], terms[2]);
  conj.push_back(nm->mkNode(IMPLIES, term0_and_2, terms[4]));
  conj.push_back(nm->mkNode(IMPLIES, terms[0], terms[3]));
  Node constraint = nm->mkNode(AND, conj);

  d_sygusConstraints.push_back(constraint);

  // sygus conjecture is now stale
  setSygusConjectureStale();
}

Result SygusSolver::checkSynth(Assertions& as)
{
  if (options().base.incrementalSolving)
  {
    // TODO (project #7)
    throw ModalException(
        "Cannot make check-synth commands when incremental solving is enabled");
  }
  Trace("smt") << "SygusSolver::checkSynth" << std::endl;
  std::vector<Node> query;
  if (d_sygusConjectureStale)
  {
    NodeManager* nm = NodeManager::currentNM();
    // build synthesis conjecture from asserted constraints and declared
    // variables/functions
    Trace("smt") << "Sygus : Constructing sygus constraint...\n";
    Node body = nm->mkAnd(d_sygusConstraints);
    // note that if there are no constraints, then assumptions are irrelevant
    if (!d_sygusConstraints.empty() && !d_sygusAssumps.empty())
    {
      Node bodyAssump = nm->mkAnd(d_sygusAssumps);
      body = nm->mkNode(IMPLIES, bodyAssump, body);
    }
    body = body.notNode();
    Trace("smt") << "...constructed sygus constraint " << body << std::endl;
    if (!d_sygusVars.empty())
    {
      Node boundVars = nm->mkNode(BOUND_VAR_LIST, d_sygusVars);
      body = nm->mkNode(EXISTS, boundVars, body);
      Trace("smt") << "...constructed exists " << body << std::endl;
    }
    if (!d_sygusFunSymbols.empty())
    {
      body =
          quantifiers::SygusUtils::mkSygusConjecture(d_sygusFunSymbols, body);
    }
    Trace("smt") << "...constructed forall " << body << std::endl;

    Trace("smt") << "Check synthesis conjecture: " << body << std::endl;

    d_sygusConjectureStale = false;

    // TODO (project #7): if incremental, we should push a context and assert
    query.push_back(body);
  }

  Result r = d_smtSolver.checkSatisfiability(as, query, false);

  // Check that synthesis solutions satisfy the conjecture
  if (options().smt.checkSynthSol
      && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
  {
    checkSynthSolution(as);
  }
  return r;
}

bool SygusSolver::getSynthSolutions(std::map<Node, Node>& sol_map)
{
  Trace("smt") << "SygusSolver::getSynthSolutions" << std::endl;
  std::map<Node, std::map<Node, Node>> sol_mapn;
  // fail if the theory engine does not have synthesis solutions
  QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
  if (qe == nullptr || !qe->getSynthSolutions(sol_mapn))
  {
    return false;
  }
  for (std::pair<const Node, std::map<Node, Node>>& cs : sol_mapn)
  {
    for (std::pair<const Node, Node>& s : cs.second)
    {
      sol_map[s.first] = s.second;
    }
  }
  return true;
}

void SygusSolver::checkSynthSolution(Assertions& as)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  if (isVerboseOn(1))
  {
    verbose(1) << "SyGuS::checkSynthSolution: checking synthesis solution"
               << std::endl;
  }
  std::map<Node, std::map<Node, Node>> sol_map;
  // Get solutions and build auxiliary vectors for substituting
  QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
  if (qe == nullptr || !qe->getSynthSolutions(sol_map))
  {
    InternalError()
        << "SygusSolver::checkSynthSolution(): No solution to check!";
    return;
  }
  if (sol_map.empty())
  {
    InternalError() << "SygusSolver::checkSynthSolution(): Got empty solution!";
    return;
  }
  Trace("check-synth-sol") << "Got solution map:\n";
  // the set of synthesis conjectures in our assertions
  std::unordered_set<Node> conjs;
  // For each of the above conjectures, the functions-to-synthesis and their
  // solutions. This is used as a substitution below.
  std::map<Node, std::vector<Node>> fvarMap;
  std::map<Node, std::vector<Node>> fsolMap;
  for (const std::pair<const Node, std::map<Node, Node>>& cmap : sol_map)
  {
    Trace("check-synth-sol") << "For conjecture " << cmap.first << ":\n";
    conjs.insert(cmap.first);
    std::vector<Node>& fvars = fvarMap[cmap.first];
    std::vector<Node>& fsols = fsolMap[cmap.first];
    for (const std::pair<const Node, Node>& pair : cmap.second)
    {
      Trace("check-synth-sol")
          << "  " << pair.first << " --> " << pair.second << "\n";
      fvars.push_back(pair.first);
      fsols.push_back(pair.second);
    }
  }
  Trace("check-synth-sol") << "Starting new SMT Engine\n";

  Trace("check-synth-sol") << "Retrieving assertions\n";
  // Build conjecture from original assertions
  const context::CDList<Node>& alist = as.getAssertionList();
  Assert(options().smt.produceAssertions)
      << "Expected produce assertions to be true when checking synthesis "
         "solution";
  // auxiliary assertions
  std::vector<Node> auxAssertions;
  // expand definitions cache
  std::unordered_map<Node, Node> cache;
  for (const Node& assertion : alist)
  {
    if (isVerboseOn(1))
    {
      verbose(1) << "SyGuS::checkSynthSolution: checking assertion "
                 << assertion << std::endl;
    }
    Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n";
    // Apply any define-funs from the problem.
    Node n = d_smtSolver.getPreprocessor()->expandDefinitions(assertion, cache);
    if (isVerboseOn(1))
    {
      verbose(1) << "SyGuS::checkSynthSolution: -- expands to " << n
                 << std::endl;
    }
    Trace("check-synth-sol") << "Expanded assertion " << n << "\n";
    if (conjs.find(n) == conjs.end())
    {
      Trace("check-synth-sol") << "It is an auxiliary assertion\n";
      auxAssertions.push_back(n);
    }
    else
    {
      Trace("check-synth-sol") << "It is a synthesis conjecture\n";
    }
  }
  // check all conjectures
  for (Node conj : conjs)
  {
    // Start new SMT engine to check solutions
    std::unique_ptr<SolverEngine> solChecker;
    initializeSubsolver(solChecker, d_env);
    solChecker->getOptions().smt.checkSynthSol = false;
    solChecker->getOptions().quantifiers.sygusRecFun = false;
    // get the solution for this conjecture
    std::vector<Node>& fvars = fvarMap[conj];
    std::vector<Node>& fsols = fsolMap[conj];
    // Apply solution map to conjecture body
    Node conjBody;
    /* Whether property is quantifier free */
    if (conj[1].getKind() != EXISTS)
    {
      conjBody = conj[1].substitute(
          fvars.begin(), fvars.end(), fsols.begin(), fsols.end());
    }
    else
    {
      conjBody = conj[1][1].substitute(
          fvars.begin(), fvars.end(), fsols.begin(), fsols.end());

      /* Skolemize property */
      std::vector<Node> vars, skos;
      for (unsigned j = 0, size = conj[1][0].getNumChildren(); j < size; ++j)
      {
        vars.push_back(conj[1][0][j]);
        std::stringstream ss;
        ss << "sk_" << j;
        skos.push_back(sm->mkDummySkolem(ss.str(), conj[1][0][j].getType()));
        Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to "
                                 << skos.back() << "\n";
      }
      conjBody = conjBody.substitute(
          vars.begin(), vars.end(), skos.begin(), skos.end());
    }

    if (isVerboseOn(1))
    {
      verbose(1) << "SyGuS::checkSynthSolution: -- body substitutes to "
                 << conjBody << std::endl;
    }
    Trace("check-synth-sol")
        << "Substituted body of assertion to " << conjBody << "\n";
    solChecker->assertFormula(conjBody);
    // Assert all auxiliary assertions. This may include recursive function
    // definitions that were added as assertions to the sygus problem.
    for (Node a : auxAssertions)
    {
      // We require rewriting here, e.g. so that define-fun from the original
      // problem are rewritten to true. If this is not the case, then the
      // assertions module of the subsolver will complain about assertions
      // with free variables.
      Node ar = rewrite(a);
      solChecker->assertFormula(ar);
    }
    Result r = solChecker->checkSat();
    if (isVerboseOn(1))
    {
      verbose(1) << "SyGuS::checkSynthSolution: result is " << r << std::endl;
    }
    Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
    if (r.asSatisfiabilityResult().isUnknown())
    {
      InternalError() << "SygusSolver::checkSynthSolution(): could not check "
                         "solution, result "
                         "unknown.";
    }
    else if (r.asSatisfiabilityResult().isSat())
    {
      InternalError()
          << "SygusSolver::checkSynthSolution(): produced solution leads to "
             "satisfiable negated conjecture.";
    }
  }
}

void SygusSolver::setSygusConjectureStale()
{
  if (d_sygusConjectureStale)
  {
    // already stale
    return;
  }
  d_sygusConjectureStale = true;
  // TODO (project #7): if incremental, we should pop a context
}

void SygusSolver::expandDefinitionsSygusDt(TypeNode tn) const
{
  std::unordered_set<TypeNode> processed;
  std::vector<TypeNode> toProcess;
  toProcess.push_back(tn);
  size_t index = 0;
  while (index < toProcess.size())
  {
    TypeNode tnp = toProcess[index];
    index++;
    Assert(tnp.isDatatype());
    Assert(tnp.getDType().isSygus());
    const std::vector<std::shared_ptr<DTypeConstructor>>& cons =
        tnp.getDType().getConstructors();
    for (const std::shared_ptr<DTypeConstructor>& c : cons)
    {
      Node op = c->getSygusOp();
      // Only expand definitions if the operator is not constant, since
      // calling expandDefinitions on them should be a no-op. This check
      // ensures we don't try to expand e.g. bitvector extract operators,
      // whose type is undefined, and thus should not be passed to
      // expandDefinitions.
      Node eop = op.isConst()
                     ? op
                     : d_smtSolver.getPreprocessor()->expandDefinitions(op);
      eop = rewrite(eop);
      datatypes::utils::setExpandedDefinitionForm(op, eop);
      // also must consider the arguments
      for (unsigned j = 0, nargs = c->getNumArgs(); j < nargs; ++j)
      {
        TypeNode tnc = c->getArgType(j);
        if (tnc.isDatatype() && tnc.getDType().isSygus()
            && processed.find(tnc) == processed.end())
        {
          toProcess.push_back(tnc);
          processed.insert(tnc);
        }
      }
    }
  }
}

}  // namespace smt
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 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::theory;
39		using namespace cvc5::kind;
40
41		namespace cvc5 {
42		namespace smt {
43
44	18632	SygusSolver::SygusSolver(Env& env, SmtSolver& sms)
45	18632	: EnvObj(env), d_smtSolver(sms), d_sygusConjectureStale(userContext(), true)
46		{
47	18632	}
48
49	31766	SygusSolver::~SygusSolver() {}
50
51	730	void SygusSolver::declareSygusVar(Node var)
52		{
53	1460	Trace("smt") << "SygusSolver::declareSygusVar: " << var << " "
54	730	<< var.getType() << "\n";
55	730	d_sygusVars.push_back(var);
56		// don't need to set that the conjecture is stale
57	730	}
58
59	717	void SygusSolver::declareSynthFun(Node fn,
60		TypeNode sygusType,
61		bool isInv,
62		const std::vector<Node>& vars)
63		{
64	717	Trace("smt") << "SygusSolver::declareSynthFun: " << fn << "\n";
65	717	NodeManager* nm = NodeManager::currentNM();
66	717	d_sygusFunSymbols.push_back(fn);
67	717	if (!vars.empty())
68		{
69	1294	Node bvl = nm->mkNode(BOUND_VAR_LIST, vars);
70		// use an attribute to mark its bound variable list
71		SygusSynthFunVarListAttribute ssfvla;
72	647	fn.setAttribute(ssfvla, bvl);
73		}
74		// whether sygus type encodes syntax restrictions
75	2151	if (!sygusType.isNull() && sygusType.isDatatype()
76	1019	&& sygusType.getDType().isSygus())
77		{
78	600	Node sym = nm->mkBoundVar("sfproxy", sygusType);
79		// use an attribute to mark its grammar
80		SygusSynthGrammarAttribute ssfga;
81	300	fn.setAttribute(ssfga, sym);
82		// we must expand definitions for sygus operators in the block
83	300	expandDefinitionsSygusDt(sygusType);
84		}
85
86		// sygus conjecture is now stale
87	717	setSygusConjectureStale();
88	717	}
89
90	1264	void SygusSolver::assertSygusConstraint(Node n, bool isAssume)
91		{
92	2528	Trace("smt") << "SygusSolver::assertSygusConstrant: " << n
93	1264	<< ", isAssume=" << isAssume << "\n";
94	1264	if (isAssume)
95		{
96	6	d_sygusAssumps.push_back(n);
97		}
98		else
99		{
100	1258	d_sygusConstraints.push_back(n);
101		}
102
103		// sygus conjecture is now stale
104	1264	setSygusConjectureStale();
105	1264	}
106
107	31	void SygusSolver::assertSygusInvConstraint(Node inv,
108		Node pre,
109		Node trans,
110		Node post)
111		{
112	62	Trace("smt") << "SygusSolver::assertSygusInvConstrant: " << inv << " " << pre
113	31	<< " " << trans << " " << post << "\n";
114		// build invariant constraint
115
116		// get variables (regular and their respective primed versions)
117	62	std::vector<Node> terms;
118	62	std::vector<Node> vars;
119	62	std::vector<Node> primed_vars;
120	31	terms.push_back(inv);
121	31	terms.push_back(pre);
122	31	terms.push_back(trans);
123	31	terms.push_back(post);
124		// variables are built based on the invariant type
125	31	NodeManager* nm = NodeManager::currentNM();
126	62	std::vector<TypeNode> argTypes = inv.getType().getArgTypes();
127	220	for (const TypeNode& tn : argTypes)
128		{
129	189	vars.push_back(nm->mkBoundVar(tn));
130	189	d_sygusVars.push_back(vars.back());
131	378	std::stringstream ss;
132	189	ss << vars.back() << "'";
133	189	primed_vars.push_back(nm->mkBoundVar(ss.str(), tn));
134	189	d_sygusVars.push_back(primed_vars.back());
135		}
136
137		// make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
138	155	for (unsigned i = 0; i < 4; ++i)
139		{
140	248	Node op = terms[i];
141	248	Trace("smt-debug") << "Make inv-constraint term #" << i << " : " << op
142	124	<< " with type " << op.getType() << "...\n";
143	248	std::vector<Node> children;
144	124	children.push_back(op);
145		// transition relation applied over both variable lists
146	124	if (i == 2)
147		{
148	31	children.insert(children.end(), vars.begin(), vars.end());
149	31	children.insert(children.end(), primed_vars.begin(), primed_vars.end());
150		}
151		else
152		{
153	93	children.insert(children.end(), vars.begin(), vars.end());
154		}
155	124	terms[i] = nm->mkNode(APPLY_UF, children);
156		// make application of Inv on primed variables
157	124	if (i == 0)
158		{
159	31	children.clear();
160	31	children.push_back(op);
161	31	children.insert(children.end(), primed_vars.begin(), primed_vars.end());
162	31	terms.push_back(nm->mkNode(APPLY_UF, children));
163		}
164		}
165		// make constraints
166	62	std::vector<Node> conj;
167	31	conj.push_back(nm->mkNode(IMPLIES, terms[1], terms[0]));
168	62	Node term0_and_2 = nm->mkNode(AND, terms[0], terms[2]);
169	31	conj.push_back(nm->mkNode(IMPLIES, term0_and_2, terms[4]));
170	31	conj.push_back(nm->mkNode(IMPLIES, terms[0], terms[3]));
171	62	Node constraint = nm->mkNode(AND, conj);
172
173	31	d_sygusConstraints.push_back(constraint);
174
175		// sygus conjecture is now stale
176	31	setSygusConjectureStale();
177	31	}
178
179	392	Result SygusSolver::checkSynth(Assertions& as)
180		{
181	392	if (options().base.incrementalSolving)
182		{
183		// TODO (project #7)
184		throw ModalException(
185		"Cannot make check-synth commands when incremental solving is enabled");
186		}
187	392	Trace("smt") << "SygusSolver::checkSynth" << std::endl;
188	784	std::vector<Node> query;
189	392	if (d_sygusConjectureStale)
190		{
191	392	NodeManager* nm = NodeManager::currentNM();
192		// build synthesis conjecture from asserted constraints and declared
193		// variables/functions
194	392	Trace("smt") << "Sygus : Constructing sygus constraint...\n";
195	784	Node body = nm->mkAnd(d_sygusConstraints);
196		// note that if there are no constraints, then assumptions are irrelevant
197	392	if (!d_sygusConstraints.empty() && !d_sygusAssumps.empty())
198		{
199	8	Node bodyAssump = nm->mkAnd(d_sygusAssumps);
200	4	body = nm->mkNode(IMPLIES, bodyAssump, body);
201		}
202	392	body = body.notNode();
203	392	Trace("smt") << "...constructed sygus constraint " << body << std::endl;
204	392	if (!d_sygusVars.empty())
205		{
206	544	Node boundVars = nm->mkNode(BOUND_VAR_LIST, d_sygusVars);
207	272	body = nm->mkNode(EXISTS, boundVars, body);
208	272	Trace("smt") << "...constructed exists " << body << std::endl;
209		}
210	392	if (!d_sygusFunSymbols.empty())
211		{
212	392	body =
213	784	quantifiers::SygusUtils::mkSygusConjecture(d_sygusFunSymbols, body);
214		}
215	392	Trace("smt") << "...constructed forall " << body << std::endl;
216
217	392	Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
218
219	392	d_sygusConjectureStale = false;
220
221		// TODO (project #7): if incremental, we should push a context and assert
222	392	query.push_back(body);
223		}
224
225	392	Result r = d_smtSolver.checkSatisfiability(as, query, false);
226
227		// Check that synthesis solutions satisfy the conjecture
228	756	if (options().smt.checkSynthSol
229	756	&& r.asSatisfiabilityResult().isSat() == Result::UNSAT)
230		{
231	177	checkSynthSolution(as);
232		}
233	756	return r;
234		}
235
236	111	bool SygusSolver::getSynthSolutions(std::map<Node, Node>& sol_map)
237		{
238	111	Trace("smt") << "SygusSolver::getSynthSolutions" << std::endl;
239	222	std::map<Node, std::map<Node, Node>> sol_mapn;
240		// fail if the theory engine does not have synthesis solutions
241	111	QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
242	111	if (qe == nullptr \|\| !qe->getSynthSolutions(sol_mapn))
243		{
244		return false;
245		}
246	218	for (std::pair<const Node, std::map<Node, Node>>& cs : sol_mapn)
247		{
248	250	for (std::pair<const Node, Node>& s : cs.second)
249		{
250	143	sol_map[s.first] = s.second;
251		}
252		}
253	111	return true;
254		}
255
256	177	void SygusSolver::checkSynthSolution(Assertions& as)
257		{
258	177	NodeManager* nm = NodeManager::currentNM();
259	177	SkolemManager* sm = nm->getSkolemManager();
260	177	if (isVerboseOn(1))
261		{
262	1	verbose(1) << "SyGuS::checkSynthSolution: checking synthesis solution"
263	1	<< std::endl;
264		}
265	354	std::map<Node, std::map<Node, Node>> sol_map;
266		// Get solutions and build auxiliary vectors for substituting
267	177	QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
268	177	if (qe == nullptr \|\| !qe->getSynthSolutions(sol_map))
269		{
270		InternalError()
271		<< "SygusSolver::checkSynthSolution(): No solution to check!";
272		return;
273		}
274	177	if (sol_map.empty())
275		{
276		InternalError() << "SygusSolver::checkSynthSolution(): Got empty solution!";
277		return;
278		}
279	177	Trace("check-synth-sol") << "Got solution map:\n";
280		// the set of synthesis conjectures in our assertions
281	354	std::unordered_set<Node> conjs;
282		// For each of the above conjectures, the functions-to-synthesis and their
283		// solutions. This is used as a substitution below.
284	354	std::map<Node, std::vector<Node>> fvarMap;
285	354	std::map<Node, std::vector<Node>> fsolMap;
286	354	for (const std::pair<const Node, std::map<Node, Node>>& cmap : sol_map)
287		{
288	177	Trace("check-synth-sol") << "For conjecture " << cmap.first << ":\n";
289	177	conjs.insert(cmap.first);
290	177	std::vector<Node>& fvars = fvarMap[cmap.first];
291	177	std::vector<Node>& fsols = fsolMap[cmap.first];
292	504	for (const std::pair<const Node, Node>& pair : cmap.second)
293		{
294	654	Trace("check-synth-sol")
295	327	<< " " << pair.first << " --> " << pair.second << "\n";
296	327	fvars.push_back(pair.first);
297	327	fsols.push_back(pair.second);
298		}
299		}
300	177	Trace("check-synth-sol") << "Starting new SMT Engine\n";
301
302	177	Trace("check-synth-sol") << "Retrieving assertions\n";
303		// Build conjecture from original assertions
304	177	const context::CDList<Node>& alist = as.getAssertionList();
305	177	Assert(options().smt.produceAssertions)
306		<< "Expected produce assertions to be true when checking synthesis "
307		"solution";
308		// auxiliary assertions
309	354	std::vector<Node> auxAssertions;
310		// expand definitions cache
311	354	std::unordered_map<Node, Node> cache;
312	630	for (const Node& assertion : alist)
313		{
314	453	if (isVerboseOn(1))
315		{
316	4	verbose(1) << "SyGuS::checkSynthSolution: checking assertion "
317	4	<< assertion << std::endl;
318		}
319	453	Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n";
320		// Apply any define-funs from the problem.
321	906	Node n = d_smtSolver.getPreprocessor()->expandDefinitions(assertion, cache);
322	453	if (isVerboseOn(1))
323		{
324	8	verbose(1) << "SyGuS::checkSynthSolution: -- expands to " << n
325	4	<< std::endl;
326		}
327	453	Trace("check-synth-sol") << "Expanded assertion " << n << "\n";
328	453	if (conjs.find(n) == conjs.end())
329		{
330	446	Trace("check-synth-sol") << "It is an auxiliary assertion\n";
331	446	auxAssertions.push_back(n);
332		}
333		else
334		{
335	7	Trace("check-synth-sol") << "It is a synthesis conjecture\n";
336		}
337		}
338		// check all conjectures
339	354	for (Node conj : conjs)
340		{
341		// Start new SMT engine to check solutions
342	354	std::unique_ptr<SolverEngine> solChecker;
343	177	initializeSubsolver(solChecker, d_env);
344	177	solChecker->getOptions().smt.checkSynthSol = false;
345	177	solChecker->getOptions().quantifiers.sygusRecFun = false;
346		// get the solution for this conjecture
347	177	std::vector<Node>& fvars = fvarMap[conj];
348	177	std::vector<Node>& fsols = fsolMap[conj];
349		// Apply solution map to conjecture body
350	354	Node conjBody;
351		/* Whether property is quantifier free */
352	177	if (conj[1].getKind() != EXISTS)
353		{
354	177	conjBody = conj[1].substitute(
355		fvars.begin(), fvars.end(), fsols.begin(), fsols.end());
356		}
357		else
358		{
359		conjBody = conj[1][1].substitute(
360		fvars.begin(), fvars.end(), fsols.begin(), fsols.end());
361
362		/* Skolemize property */
363		std::vector<Node> vars, skos;
364		for (unsigned j = 0, size = conj[1][0].getNumChildren(); j < size; ++j)
365		{
366		vars.push_back(conj[1][0][j]);
367		std::stringstream ss;
368		ss << "sk_" << j;
369		skos.push_back(sm->mkDummySkolem(ss.str(), conj[1][0][j].getType()));
370		Trace("check-synth-sol") << "\tSkolemizing " << conj[1][0][j] << " to "
371		<< skos.back() << "\n";
372		}
373		conjBody = conjBody.substitute(
374		vars.begin(), vars.end(), skos.begin(), skos.end());
375		}
376
377	177	if (isVerboseOn(1))
378		{
379	1	verbose(1) << "SyGuS::checkSynthSolution: -- body substitutes to "
380	1	<< conjBody << std::endl;
381		}
382	354	Trace("check-synth-sol")
383	177	<< "Substituted body of assertion to " << conjBody << "\n";
384	177	solChecker->assertFormula(conjBody);
385		// Assert all auxiliary assertions. This may include recursive function
386		// definitions that were added as assertions to the sygus problem.
387	623	for (Node a : auxAssertions)
388		{
389		// We require rewriting here, e.g. so that define-fun from the original
390		// problem are rewritten to true. If this is not the case, then the
391		// assertions module of the subsolver will complain about assertions
392		// with free variables.
393	892	Node ar = rewrite(a);
394	446	solChecker->assertFormula(ar);
395		}
396	354	Result r = solChecker->checkSat();
397	177	if (isVerboseOn(1))
398		{
399	1	verbose(1) << "SyGuS::checkSynthSolution: result is " << r << std::endl;
400		}
401	177	Trace("check-synth-sol") << "Satsifiability check: " << r << "\n";
402	177	if (r.asSatisfiabilityResult().isUnknown())
403		{
404		InternalError() << "SygusSolver::checkSynthSolution(): could not check "
405		"solution, result "
406		"unknown.";
407		}
408	177	else if (r.asSatisfiabilityResult().isSat())
409		{
410		InternalError()
411		<< "SygusSolver::checkSynthSolution(): produced solution leads to "
412		"satisfiable negated conjecture.";
413		}
414		}
415	177	}
416
417	2012	void SygusSolver::setSygusConjectureStale()
418		{
419	2012	if (d_sygusConjectureStale)
420		{
421		// already stale
422	2012	return;
423		}
424		d_sygusConjectureStale = true;
425		// TODO (project #7): if incremental, we should pop a context
426		}
427
428	300	void SygusSolver::expandDefinitionsSygusDt(TypeNode tn) const
429		{
430	600	std::unordered_set<TypeNode> processed;
431	600	std::vector<TypeNode> toProcess;
432	300	toProcess.push_back(tn);
433	300	size_t index = 0;
434	2008	while (index < toProcess.size())
435		{
436	1708	TypeNode tnp = toProcess[index];
437	854	index++;
438	854	Assert(tnp.isDatatype());
439	854	Assert(tnp.getDType().isSygus());
440		const std::vector<std::shared_ptr<DTypeConstructor>>& cons =
441	854	tnp.getDType().getConstructors();
442	5185	for (const std::shared_ptr<DTypeConstructor>& c : cons)
443		{
444	8662	Node op = c->getSygusOp();
445		// Only expand definitions if the operator is not constant, since
446		// calling expandDefinitions on them should be a no-op. This check
447		// ensures we don't try to expand e.g. bitvector extract operators,
448		// whose type is undefined, and thus should not be passed to
449		// expandDefinitions.
450	4331	Node eop = op.isConst()
451		? op
452	8662	: d_smtSolver.getPreprocessor()->expandDefinitions(op);
453	4331	eop = rewrite(eop);
454	4331	datatypes::utils::setExpandedDefinitionForm(op, eop);
455		// also must consider the arguments
456	8912	for (unsigned j = 0, nargs = c->getNumArgs(); j < nargs; ++j)
457		{
458	9162	TypeNode tnc = c->getArgType(j);
459	13743	if (tnc.isDatatype() && tnc.getDType().isSygus()
460	9162	&& processed.find(tnc) == processed.end())
461		{
462	554	toProcess.push_back(tnc);
463	554	processed.insert(tnc);
464		}
465		}
466		}
467		}
468	300	}
469
470		} // namespace smt
471	31137	} // namespace cvc5