diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-21 12:15:28 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-21 17:15:28 +0000 |
commit | 624292d7fb5bd27b10bdce285441540d6931fa57 (patch) | |
tree | 73169808ce6106ba4ab18f515bb1752e1227ff3e /src/expr/symbol_manager.cpp | |
parent | bb39d534c89dc2569aa048bb053196bfa5bbb3a1 (diff) |
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.
Diffstat (limited to 'src/expr/symbol_manager.cpp')
-rw-r--r-- | src/expr/symbol_manager.cpp | 30 |
1 files changed, 30 insertions, 0 deletions
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<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 */ @@ -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<api::Term> SymbolManager::Implementation::getModelDeclareTerms() 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 @@ -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<api::Term> SymbolManager::getModelDeclareTerms() const 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); @@ -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(); |