From 624292d7fb5bd27b10bdce285441540d6931fa57 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 21 May 2021 12:15:28 -0500 Subject: [PATCH] Update to sygus standard output for check-synth responses (#6521) This PR does two things: (1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model. (2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model. It also removes the unused command GetSynthSolutionCommand. --- src/api/cpp/cvc5.cpp | 9 -- src/api/cpp/cvc5.h | 6 -- src/expr/symbol_manager.cpp | 30 +++++++ src/expr/symbol_manager.h | 10 +++ src/options/smt_options.toml | 2 +- src/printer/printer.cpp | 5 -- src/printer/printer.h | 3 - src/smt/command.cpp | 84 ++++++------------- src/smt/command.h | 19 ----- src/smt/smt_engine.cpp | 6 -- src/smt/smt_engine.h | 5 -- src/smt/sygus_solver.cpp | 12 --- src/smt/sygus_solver.h | 5 -- .../quantifiers/sygus/synth_conjecture.cpp | 4 +- .../quantifiers/sygus/synth_conjecture.h | 8 +- src/theory/quantifiers/sygus/synth_engine.cpp | 12 --- src/theory/quantifiers/sygus/synth_engine.h | 2 - src/theory/quantifiers_engine.cpp | 9 -- src/theory/quantifiers_engine.h | 2 - test/regress/regress0/sygus/print-debug.sy | 3 +- .../regress0/sygus/print-define-fun.sy | 3 +- test/regress/regress1/sygus/no-var-in-sol.sy | 3 +- 22 files changed, 79 insertions(+), 163 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index b7923321c..0da42f173 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -7437,15 +7437,6 @@ std::vector Solver::getSynthSolutions( 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. !!! diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index f77869c2c..e8f7737a6 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -4118,12 +4118,6 @@ class CVC5_EXPORT Solver */ std::vector getSynthSolutions(const std::vector& 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; diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp index 8d4870966..687f4963f 100644 --- a/src/expr/symbol_manager.cpp +++ b/src/expr/symbol_manager.cpp @@ -40,6 +40,7 @@ class SymbolManager::Implementation 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 @@ -65,10 +66,14 @@ class SymbolManager::Implementation std::vector getModelDeclareSorts() const; /** get model declare terms */ std::vector getModelDeclareTerms() const; + /** get functions to synthesize */ + std::vector 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 */ @@ -91,6 +96,8 @@ class SymbolManager::Implementation 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? */ @@ -192,6 +199,12 @@ std::vector SymbolManager::Implementation::getModelDeclareTerms() return declareTerms; } +std::vector SymbolManager::Implementation::getFunctionsToSynthesize() + const +{ + return std::vector(d_funToSynth.begin(), d_funToSynth.end()); +} + void SymbolManager::Implementation::addModelDeclarationSort(api::Sort s) { Trace("sym-manager") << "SymbolManager: addModelDeclarationSort " << s @@ -206,6 +219,13 @@ void SymbolManager::Implementation::addModelDeclarationTerm(api::Term t) 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 = " @@ -306,6 +326,11 @@ std::vector SymbolManager::getModelDeclareTerms() const return d_implementation->getModelDeclareTerms(); } +std::vector SymbolManager::getFunctionsToSynthesize() const +{ + return d_implementation->getFunctionsToSynthesize(); +} + void SymbolManager::addModelDeclarationSort(api::Sort s) { d_implementation->addModelDeclarationSort(s); @@ -316,6 +341,11 @@ void SymbolManager::addModelDeclarationTerm(api::Term t) d_implementation->addModelDeclarationTerm(t); } +void SymbolManager::addFunctionToSynthesize(api::Term f) +{ + d_implementation->addFunctionToSynthesize(f); +} + size_t SymbolManager::scopeLevel() const { return d_symtabAllocated.getLevel(); diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 271825e07..d8b7e23bd 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -112,6 +112,11 @@ class CVC5_EXPORT SymbolManager * @return The terms we have declared that should be printed in the model. */ std::vector getModelDeclareTerms() const; + /** + * @return The functions we have declared that should be printed in a response + * to check-synth. + */ + std::vector getFunctionsToSynthesize() const; /** * Add declared sort to the list of model declarations. */ @@ -120,6 +125,11 @@ class CVC5_EXPORT SymbolManager * 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 /** diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 880bbe0fb..d1354f777 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -158,7 +158,7 @@ name = "SMT Layer" 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]] diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 927fd1d13..048f5d06b 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -333,11 +333,6 @@ void Printer::toStreamCmdGetInstantiations(std::ostream& out) const 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, diff --git a/src/printer/printer.h b/src/printer/printer.h index 86f3dbb2b..6c00ebad5 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -181,9 +181,6 @@ class Printer /** 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, diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 02cea842a..bf7d5ef3d 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -699,6 +699,7 @@ const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; } void SynthFunCommand::invoke(api::Solver* solver, SymbolManager* sm) { + sm->addFunctionToSynthesize(d_fun); d_commandStatus = CommandSuccess::instance(); } @@ -846,7 +847,7 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm) { if (options::sygusOut() == options::SygusSolutionOutMode::STANDARD) { - d_solution << "(fail)" << endl; + d_solution << "fail" << endl; } else { @@ -857,12 +858,30 @@ void CheckSynthCommand::invoke(api::Solver* solver, SymbolManager* sm) 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 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 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) @@ -2069,57 +2088,6 @@ void GetInstantiationsCommand::toStream(std::ostream& out, 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 */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index 41a3639c9..21ecd1964 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -1091,25 +1091,6 @@ class CVC5_EXPORT GetInstantiationsCommand : public Command 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 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bd38f630d..6377091f2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1629,12 +1629,6 @@ void SmtEngine::getInstantiationTermVectors( } } -void SmtEngine::printSynthSolution( std::ostream& out ) { - SmtScope smts(this); - finishInit(); - d_sygusSolver->printSynthSolution(out); -} - bool SmtEngine::getSynthSolutions(std::map& solMap) { SmtScope smts(this); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index b8cd1c3d7..3128257e6 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -543,11 +543,6 @@ class CVC5_EXPORT SmtEngine * 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. diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp index 37d752230..4e5d6cd8c 100644 --- a/src/smt/sygus_solver.cpp +++ b/src/smt/sygus_solver.cpp @@ -251,18 +251,6 @@ bool SygusSolver::getSynthSolutions(std::map& sol_map) 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(); diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h index 5b3bca928..ff9b7e513 100644 --- a/src/smt/sygus_solver.h +++ b/src/smt/sygus_solver.h @@ -137,11 +137,6 @@ class SygusSolver * is a valid formula. */ bool getSynthSolutions(std::map& sol_map); - /** - * Print solution for synthesis conjectures found by counter-example guided - * instantiation module. - */ - void printSynthSolution(std::ostream& out); private: /** diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index 0eb96e277..e4ec40325 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -995,7 +995,7 @@ void SynthConjecture::printAndContinueStream(const std::vector& enums, // 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); } @@ -1041,7 +1041,7 @@ void SynthConjecture::excludeCurrentSolution(const std::vector& enums, } } -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()); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index a7ecd4ead..4329a9c60 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -134,11 +134,11 @@ class SynthConjecture 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 diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index 173f58060..86c3f62d0 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -246,18 +246,6 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj) 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 >& sol_map) { diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index df73c4821..d37df4e28 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -57,8 +57,6 @@ class SynthEngine : public QuantifiersModule 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 diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2d1eeab84..40f5b901f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -651,15 +651,6 @@ void QuantifiersEngine::getInstantiations(Node q, std::vector& insts) 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& qs) { d_qim.getInstantiate()->getInstantiatedQuantifiedFormulas(qs); diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h index fc29ab8e8..482dbfaee 100644 --- a/src/theory/quantifiers_engine.h +++ b/src/theory/quantifiers_engine.h @@ -134,8 +134,6 @@ public: 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& qs); /** get instantiation term vectors */ diff --git a/test/regress/regress0/sygus/print-debug.sy b/test/regress/regress0/sygus/print-debug.sy index 0de431294..aba9c715f 100644 --- a/test/regress/regress0/sygus/print-debug.sy +++ b/test/regress/regress0/sygus/print-debug.sy @@ -3,8 +3,9 @@ ; 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)))) diff --git a/test/regress/regress0/sygus/print-define-fun.sy b/test/regress/regress0/sygus/print-define-fun.sy index e6c7e4748..520a03d2a 100644 --- a/test/regress/regress0/sygus/print-define-fun.sy +++ b/test/regress/regress0/sygus/print-define-fun.sy @@ -1,6 +1,7 @@ ; 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))))) diff --git a/test/regress/regress1/sygus/no-var-in-sol.sy b/test/regress/regress1/sygus/no-var-in-sol.sy index 333e29d6e..ff2be7b22 100644 --- a/test/regress/regress1/sygus/no-var-in-sol.sy +++ b/test/regress/regress1/sygus/no-var-in-sol.sy @@ -1,7 +1,8 @@ ; 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 -- 2.30.2