diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-14 16:29:32 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-14 21:29:32 +0000 |
| commit | 74c5067d81b8384701cff7f6e7b697d7fe67cf58 (patch) | |
| tree | 686d06c8fe27f122a0c8a6ad05d74c487570e966 /src/smt/command.cpp | |
| parent | d34e563fe48c42aa06eea44191a21dcf29772339 (diff) | |
Support sygus version 2.1 command assume (#7081)
Adds support for global assumptions in sygus files.
Also guards against cases of declare-const, which should be prohibited in sygus.
Diffstat (limited to 'src/smt/command.cpp')
| -rw-r--r-- | src/smt/command.cpp | 27 |
1 files changed, 22 insertions, 5 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index adfd2f71d..4b04abcb2 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -732,7 +732,9 @@ void SynthFunCommand::toStream(std::ostream& out, /* class SygusConstraintCommand */ /* -------------------------------------------------------------------------- */ -SygusConstraintCommand::SygusConstraintCommand(const api::Term& t) : d_term(t) +SygusConstraintCommand::SygusConstraintCommand(const api::Term& t, + bool isAssume) + : d_term(t), d_isAssume(isAssume) { } @@ -740,7 +742,14 @@ void SygusConstraintCommand::invoke(api::Solver* solver, SymbolManager* sm) { try { - solver->addSygusConstraint(d_term); + if (d_isAssume) + { + solver->addSygusAssume(d_term); + } + else + { + solver->addSygusConstraint(d_term); + } d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -753,12 +762,12 @@ api::Term SygusConstraintCommand::getTerm() const { return d_term; } Command* SygusConstraintCommand::clone() const { - return new SygusConstraintCommand(d_term); + return new SygusConstraintCommand(d_term, d_isAssume); } std::string SygusConstraintCommand::getCommandName() const { - return "constraint"; + return d_isAssume ? "assume" : "constraint"; } void SygusConstraintCommand::toStream(std::ostream& out, @@ -766,7 +775,15 @@ void SygusConstraintCommand::toStream(std::ostream& out, size_t dag, Language language) const { - Printer::getPrinter(language)->toStreamCmdConstraint(out, termToNode(d_term)); + if (d_isAssume) + { + Printer::getPrinter(language)->toStreamCmdAssume(out, termToNode(d_term)); + } + else + { + Printer::getPrinter(language)->toStreamCmdConstraint(out, + termToNode(d_term)); + } } /* -------------------------------------------------------------------------- */ |