CVC5_API_TRY_CATCH_END;
}
-void Solver::printSynthSolution(std::ostream& out) const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- //////// all checks before this line
- d_smtEngine->printSynthSolution(out);
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
/*
* !!! This is only temporarily available until the parser is fully migrated to
* the new API. !!!
*/
std::vector<Term> getSynthSolutions(const std::vector<Term>& terms) const;
- /**
- * Print solution for synthesis conjecture to the given output stream.
- * @param out the output stream
- */
- void printSynthSolution(std::ostream& out) const;
-
// !!! This is only temporarily available until the parser is fully migrated
// to the new API. !!!
SmtEngine* getSmtEngine(void) const;
d_namedAsserts(&d_context),
d_declareSorts(&d_context),
d_declareTerms(&d_context),
+ d_funToSynth(&d_context),
d_hasPushedScope(&d_context, false)
{
// use an outermost push, to be able to clear all definitions
std::vector<api::Sort> getModelDeclareSorts() const;
/** get model declare terms */
std::vector<api::Term> getModelDeclareTerms() const;
+ /** get functions to synthesize */
+ std::vector<api::Term> getFunctionsToSynthesize() const;
/** Add declared sort to the list of model declarations. */
void addModelDeclarationSort(api::Sort s);
/** Add declared term to the list of model declarations. */
void addModelDeclarationTerm(api::Term t);
+ /** Add function to the list of functions to synthesize. */
+ void addFunctionToSynthesize(api::Term t);
/** reset */
void reset();
/** reset assertions */
SortList d_declareSorts;
/** Declared terms (for model printing) */
TermList d_declareTerms;
+ /** Functions to synthesize (for response to check-synth) */
+ TermList d_funToSynth;
/**
* Have we pushed a scope (e.g. a let or quantifier) in the current context?
*/
return declareTerms;
}
+std::vector<api::Term> SymbolManager::Implementation::getFunctionsToSynthesize()
+ const
+{
+ return std::vector<api::Term>(d_funToSynth.begin(), d_funToSynth.end());
+}
+
void SymbolManager::Implementation::addModelDeclarationSort(api::Sort s)
{
Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s
d_declareTerms.push_back(t);
}
+void SymbolManager::Implementation::addFunctionToSynthesize(api::Term f)
+{
+ Trace("sym-manager") << "SymbolManager: addFunctionToSynthesize " << f
+ << std::endl;
+ d_funToSynth.push_back(f);
+}
+
void SymbolManager::Implementation::pushScope(bool isUserContext)
{
Trace("sym-manager") << "SymbolManager: pushScope, isUserContext = "
return d_implementation->getModelDeclareTerms();
}
+std::vector<api::Term> SymbolManager::getFunctionsToSynthesize() const
+{
+ return d_implementation->getFunctionsToSynthesize();
+}
+
void SymbolManager::addModelDeclarationSort(api::Sort s)
{
d_implementation->addModelDeclarationSort(s);
d_implementation->addModelDeclarationTerm(t);
}
+void SymbolManager::addFunctionToSynthesize(api::Term f)
+{
+ d_implementation->addFunctionToSynthesize(f);
+}
+
size_t SymbolManager::scopeLevel() const
{
return d_symtabAllocated.getLevel();
* @return The terms we have declared that should be printed in the model.
*/
std::vector<api::Term> getModelDeclareTerms() const;
+ /**
+ * @return The functions we have declared that should be printed in a response
+ * to check-synth.
+ */
+ std::vector<api::Term> getFunctionsToSynthesize() const;
/**
* Add declared sort to the list of model declarations.
*/
* Add declared term to the list of model declarations.
*/
void addModelDeclarationTerm(api::Term t);
+ /**
+ * Add a function to synthesize. This ensures the solution for f is printed
+ * in a successful response to check-synth.
+ */
+ void addFunctionToSynthesize(api::Term f);
//---------------------------- end named expressions
/**
category = "regular"
long = "sygus-out=MODE"
type = "SygusSolutionOutMode"
- default = "STATUS_AND_DEF"
+ default = "STANDARD"
help = "output mode for sygus"
help_mode = "Modes for sygus solution output."
[[option.mode.STATUS]]
printUnknownCommand(out, "get-instantiations");
}
-void Printer::toStreamCmdGetSynthSolution(std::ostream& out) const
-{
- printUnknownCommand(out, "get-synth-solution");
-}
-
void Printer::toStreamCmdGetInterpol(std::ostream& out,
const std::string& name,
Node conj,
/** Print get-instantiations command */
void toStreamCmdGetInstantiations(std::ostream& out) const;
- /** Print get-synth-solution command */
- void toStreamCmdGetSynthSolution(std::ostream& out) const;
-
/** Print get-interpol command */
void toStreamCmdGetInterpol(std::ostream& out,
const std::string& name,
void SynthFunCommand::invoke(api::Solver* solver, SymbolManager* sm)
{
+ sm->addFunctionToSynthesize(d_fun);
d_commandStatus = CommandSuccess::instance();
}
{
if (options::sygusOut() == options::SygusSolutionOutMode::STANDARD)
{
- d_solution << "(fail)" << endl;
+ d_solution << "fail" << endl;
}
else
{
if (d_result.isUnsat()
&& options::sygusOut() != options::SygusSolutionOutMode::STATUS)
{
- // printing a synthesis solution is a non-constant
- // method, since it invokes a sophisticated algorithm
- // (Figure 5 of Reynolds et al. CAV 2015).
- // Hence, we must call here print solution here,
- // instead of during printResult.
- solver->printSynthSolution(d_solution);
+ std::vector<api::Term> synthFuns = sm->getFunctionsToSynthesize();
+ d_solution << "(" << std::endl;
+ Printer* p = Printer::getPrinter(language::output::LANG_SYGUS_V2);
+ for (api::Term& f : synthFuns)
+ {
+ api::Term sol = solver->getSynthSolution(f);
+ std::vector<api::Term> formals;
+ if (sol.getKind() == api::LAMBDA)
+ {
+ formals.insert(formals.end(), sol[0].begin(), sol[0].end());
+ sol = sol[1];
+ }
+ api::Sort rangeSort = f.getSort();
+ if (rangeSort.isFunction())
+ {
+ rangeSort = rangeSort.getFunctionCodomainSort();
+ }
+ p->toStreamCmdDefineFunction(d_solution,
+ f.toString(),
+ termVectorToNodes(formals),
+ sortToTypeNode(rangeSort),
+ termToNode(sol));
+ }
+ d_solution << ")" << std::endl;
}
}
catch (exception& e)
Printer::getPrinter(language)->toStreamCmdGetInstantiations(out);
}
-/* -------------------------------------------------------------------------- */
-/* class GetSynthSolutionCommand */
-/* -------------------------------------------------------------------------- */
-
-GetSynthSolutionCommand::GetSynthSolutionCommand() : d_solver(nullptr) {}
-void GetSynthSolutionCommand::invoke(api::Solver* solver, SymbolManager* sm)
-{
- try
- {
- d_solver = solver;
- d_commandStatus = CommandSuccess::instance();
- }
- catch (exception& e)
- {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-void GetSynthSolutionCommand::printResult(std::ostream& out,
- uint32_t verbosity) const
-{
- if (!ok())
- {
- this->Command::printResult(out, verbosity);
- }
- else
- {
- d_solver->printSynthSolution(out);
- }
-}
-
-Command* GetSynthSolutionCommand::clone() const
-{
- GetSynthSolutionCommand* c = new GetSynthSolutionCommand();
- c->d_solver = d_solver;
- return c;
-}
-
-std::string GetSynthSolutionCommand::getCommandName() const
-{
- return "get-synth-solution";
-}
-
-void GetSynthSolutionCommand::toStream(std::ostream& out,
- int toDepth,
- size_t dag,
- OutputLanguage language) const
-{
- Printer::getPrinter(language)->toStreamCmdGetSynthSolution(out);
-}
-
/* -------------------------------------------------------------------------- */
/* class GetInterpolCommand */
/* -------------------------------------------------------------------------- */
api::Solver* d_solver;
}; /* class GetInstantiationsCommand */
-class CVC5_EXPORT GetSynthSolutionCommand : public Command
-{
- public:
- GetSynthSolutionCommand();
-
- void invoke(api::Solver* solver, SymbolManager* sm) override;
- void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* clone() const override;
- std::string getCommandName() const override;
- void toStream(
- std::ostream& out,
- int toDepth = -1,
- size_t dag = 1,
- OutputLanguage language = language::output::LANG_AUTO) const override;
-
- protected:
- api::Solver* d_solver;
-}; /* class GetSynthSolutionCommand */
-
/** The command (get-interpol s B (G)?)
*
* This command asks for an interpolant from the current set of assertions and
}
}
-void SmtEngine::printSynthSolution( std::ostream& out ) {
- SmtScope smts(this);
- finishInit();
- d_sygusSolver->printSynthSolution(out);
-}
-
bool SmtEngine::getSynthSolutions(std::map<Node, Node>& solMap)
{
SmtScope smts(this);
* in the proper format.
*/
void printProof();
- /**
- * Print solution for synthesis conjectures found by counter-example guided
- * instantiation module.
- */
- void printSynthSolution(std::ostream& out);
/**
* Get synth solution.
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();
* is a valid formula.
*/
bool getSynthSolutions(std::map<Node, Node>& sol_map);
- /**
- * Print solution for synthesis conjectures found by counter-example guided
- * instantiation module.
- */
- void printSynthSolution(std::ostream& out);
private:
/**
// we have generated a solution, print it
// get the current output stream
Options& sopts = smt::currentSmtEngine()->getOptions();
- printSynthSolution(*sopts.getOut());
+ printSynthSolutionInternal(*sopts.getOut());
excludeCurrentSolution(enums, values);
}
}
}
-void SynthConjecture::printSynthSolution(std::ostream& out)
+void SynthConjecture::printSynthSolutionInternal(std::ostream& out)
{
Trace("cegqi-sol-debug") << "Printing synth solution..." << std::endl;
Assert(d_quant[0].getNumChildren() == d_embed_quant[0].getNumChildren());
bool doRefine();
//-------------------------------end for counterexample-guided check/refine
/**
- * Prints the synthesis solution to output stream out. This invokes solution
- * reconstruction if the conjecture is single invocation. Otherwise, it
- * returns the solution found by sygus enumeration.
+ * Prints the current synthesis solution to output stream out. This is
+ * currently used for printing solutions for sygusStream only. We do not
+ * enclose solutions in parentheses.
*/
- void printSynthSolution(std::ostream& out);
+ void printSynthSolutionInternal(std::ostream& out);
/** get synth solutions
*
* This method returns true if this class has a solution available to the
return conj->doRefine();
}
-void SynthEngine::printSynthSolution(std::ostream& out)
-{
- Assert(!d_conjs.empty());
- for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
- {
- if (d_conjs[i]->isAssigned())
- {
- d_conjs[i]->printSynthSolution(out);
- }
- }
-}
-
bool SynthEngine::getSynthSolutions(
std::map<Node, std::map<Node, Node> >& sol_map)
{
void registerQuantifier(Node q) override;
/** Identify this module (for debugging, dynamic configuration, etc..) */
std::string identify() const override { return "SynthEngine"; }
- /** print solution for synthesis conjectures */
- void printSynthSolution(std::ostream& out);
/** get synth solutions
*
* This function adds entries to sol_map that map functions-to-synthesize
d_qim.getInstantiate()->getInstantiations(q, insts);
}
-void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
- if (d_qmodules->d_synth_e)
- {
- d_qmodules->d_synth_e->printSynthSolution(out);
- }else{
- out << "Internal error : module for synth solution not found." << std::endl;
- }
-}
-
void QuantifiersEngine::getInstantiatedQuantifiedFormulas(std::vector<Node>& qs)
{
d_qim.getInstantiate()->getInstantiatedQuantifiedFormulas(qs);
public:
//----------user interface for instantiations (see quantifiers/instantiate.h)
- /** print solution for synthesis conjectures */
- void printSynthSolution(std::ostream& out);
/** get list of quantified formulas that were instantiated */
void getInstantiatedQuantifiedFormulas(std::vector<Node>& qs);
/** get instantiation term vectors */
; EXPECT: (sygus-candidate (f 0))
; EXPECT: (sygus-enum 1)
; EXPECT: (sygus-candidate (f 1))
-; EXPECT: unsat
+; EXPECT: (
; EXPECT: (define-fun f () Int 1)
+; EXPECT: )
(set-logic LIA)
(synth-fun f () Int ((Start Int)) ((Start Int (0 1))))
; COMMAND-LINE: --lang=sygus2
-; EXPECT: unsat
+; EXPECT: (
; EXPECT: (define-fun g ((x Int)) Int (f 0))
+; EXPECT: )
(set-logic LIA)
(define-fun f ((x Int)) Int (+ x 1))
(synth-fun g ((x Int)) Int ((Start Int)) ((Start Int ((f 0)))))
; COMMAND-LINE: --sygus-si=all --dag-thresh=0
-; EXPECT: unsat
+; EXPECT: (
; EXPECT: (define-fun f1 ((x Bool) (y Bool)) Bool (ite true true false))
; EXPECT: (define-fun f2 ((x Bool) (y Bool)) Bool (ite x (ite y false (not false)) (not (ite false false (not false)))))
+; EXPECT: )
; Test ensures that the solution does not contain a random variable
projects / cvc5.git / commitdiff