diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-09-22 22:12:17 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-22 22:12:17 -0500 |
| commit | 5c062833d435e3dde5db3a8223c379a3e8cca520 (patch) | |
| tree | 6be788d43297565e4a7bc769b45ec54930abb8df /src/parser/smt2/smt2.cpp | |
| parent | 56f2e6dc41fa5fbeff1755978fa1854e800846b5 (diff) | |
Refactor Commands to use the Public API. (#5105)
This is work towards eliminating the Expr layer. This PR does the following:
Replace Expr/Type with Term/Sort in the API for commands.
Remove the command export functionality which is not supported.
Since many commands now call the Solver functions instead of the SmtEngine ones, their behavior may be a slightly different. For example, (get-unsat-assumptions) now only works in incremental mode. In some cases, CVC4 will not recover from non-fatal errors.
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 387117335..e7bb8795c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -525,8 +525,8 @@ std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Grammar* grammar) { Debug("parser-sygus") << "...read synth fun " << d_id << std::endl; d_smt2->popScope(); - return std::unique_ptr<Command>(new SynthFunCommand( - d_smt2->d_solver, d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar)); + return std::unique_ptr<Command>( + new SynthFunCommand(d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar)); } std::unique_ptr<Command> Smt2::invConstraint( @@ -556,8 +556,7 @@ std::unique_ptr<Command> Smt2::invConstraint( terms.push_back(getVariable(name)); } - return std::unique_ptr<Command>( - new SygusInvConstraintCommand(api::termVectorToExprs(terms))); + return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms)); } Command* Smt2::setLogic(std::string name, bool fromCommand) @@ -776,8 +775,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars, const std::vector<api::Term>& ntSymbols) { - d_allocGrammars.emplace_back(new api::Grammar( - std::move(d_solver->mkSygusGrammar(boundVars, ntSymbols)))); + d_allocGrammars.emplace_back( + new api::Grammar(d_solver->mkSygusGrammar(boundVars, ntSymbols))); return d_allocGrammars.back().get(); } |