Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/smt/sygus_solver.cpp	Lines:	185	212	87.3 %
Date:	2021-05-21	Branches:	334	744	44.9 %


/******************************************************************************
 * 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/skolem_manager.h"
#include "options/option_exception.h"
#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "printer/printer.h"
#include "smt/dump.h"
#include "smt/preprocessor.h"
#include "smt/smt_solver.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(SmtSolver& sms,
                         Preprocessor& pp,
                         context::UserContext* u,
                         OutputManager& outMgr)
    : d_smtSolver(sms),
      d_pp(pp),
      d_sygusConjectureStale(u, true),
      d_outMgr(outMgr)
{
}

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);
  }

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

void SygusSolver::assertSygusConstraint(Node constraint)
{
  Trace("smt") << "SygusSolver::assertSygusConstrant: " << constraint << "\n";
  d_sygusConstraints.push_back(constraint);

  // 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::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
    std::vector<Node> bodyv;
    Trace("smt") << "Sygus : Constructing sygus constraint...\n";
    size_t nconstraints = d_sygusConstraints.size();
    Node body = nconstraints == 0
                    ? nm->mkConst(true)
                    : (nconstraints == 1 ? d_sygusConstraints[0]
                                         : nm->mkNode(AND, d_sygusConstraints));
    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;
    if (Dump.isOn("raw-benchmark"))
    {
      d_outMgr.getPrinter().toStreamCmdCheckSynth(d_outMgr.getDumpOut());
    }

    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, false);

  // Check that synthesis solutions satisfy the conjecture
  if (options::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::printSynthSolution(std::ostream& out)
{
  QuantifiersEngine* qe = d_smtSolver.getQuantifiersEngine();
  if (qe == nullptr)
  {
    InternalError()
        << "SygusSolver::printSynthSolution(): Cannot print synth solution in "
           "the current logic, which does not include quantifiers";
  }
  qe->printSynthSolution(out);
}

void SygusSolver::checkSynthSolution(Assertions& as)
{
  NodeManager* nm = NodeManager::currentNM();
  SkolemManager* sm = nm->getSkolemManager();
  Notice() << "SygusSolver::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
  context::CDList<Node>* alist = as.getAssertionList();
  if (alist == nullptr)
  {
    Trace("check-synth-sol") << "No assertions to check\n";
    return;
  }
  // auxiliary assertions
  std::vector<Node> auxAssertions;
  // expand definitions cache
  std::unordered_map<Node, Node> cache;
  for (Node assertion : *alist)
  {
    Notice() << "SygusSolver::checkSynthSolution(): checking assertion "
             << assertion << std::endl;
    Trace("check-synth-sol") << "Retrieving assertion " << assertion << "\n";
    // Apply any define-funs from the problem.
    Node n = d_pp.expandDefinitions(assertion, cache);
    Notice() << "SygusSolver::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<SmtEngine> solChecker;
    initializeSubsolver(solChecker);
    solChecker->getOptions().set(options::checkSynthSol, false);
    solChecker->getOptions().set(options::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());
    }
    Notice() << "SygusSolver::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 = theory::Rewriter::rewrite(a);
      solChecker->assertFormula(ar);
    }
    Result r = solChecker->checkSat();
    Notice() << "SygusSolver::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
}

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