diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-25 13:36:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-25 13:36:09 -0500 |
commit | 8374a8dd4bf740bf26748c1dbe1616ad798cf624 (patch) | |
tree | 97b08464f2ab9b31a4f763f0d570082125c78bc6 /src/smt | |
parent | 1af865f3429c0dd5910b5a8d1e12d690c3623dfa (diff) |
Remove sygus1 parser (#4651)
We no longer support sygus v1 inputs. This PR removes support for sygus v1 (as well as a deprecated "z3str" variant of smt lib 2 which is subsumed by the new strings standard).
As mentioned in the release notes, CVC4 1.8 supports a conversion from sygus v1 to v2 script.
This removal is required for further updates to the new API. Further infrastructure (e.g. the sygus print callback) will be removed in a separate PR.
FYI @abdoo8080 .
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/command.cpp | 42 | ||||
-rw-r--r-- | src/smt/command.h | 32 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 9 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 10 |
4 files changed, 0 insertions, 93 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 962882309..cbb2076dd 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -606,48 +606,6 @@ std::string DeclareSygusVarCommand::getCommandName() const } /* -------------------------------------------------------------------------- */ -/* class DeclareSygusPrimedVarCommand */ -/* -------------------------------------------------------------------------- */ - -DeclareSygusPrimedVarCommand::DeclareSygusPrimedVarCommand( - const std::string& id, Type t) - : DeclarationDefinitionCommand(id), d_type(t) -{ -} - -Type DeclareSygusPrimedVarCommand::getType() const { return d_type; } - -void DeclareSygusPrimedVarCommand::invoke(SmtEngine* smtEngine) -{ - try - { - smtEngine->declareSygusPrimedVar(d_symbol, d_type); - d_commandStatus = CommandSuccess::instance(); - } - catch (exception& e) - { - d_commandStatus = new CommandFailure(e.what()); - } -} - -Command* DeclareSygusPrimedVarCommand::exportTo( - ExprManager* exprManager, ExprManagerMapCollection& variableMap) -{ - return new DeclareSygusPrimedVarCommand( - d_symbol, d_type.exportTo(exprManager, variableMap)); -} - -Command* DeclareSygusPrimedVarCommand::clone() const -{ - return new DeclareSygusPrimedVarCommand(d_symbol, d_type); -} - -std::string DeclareSygusPrimedVarCommand::getCommandName() const -{ - return "declare-primed-var"; -} - -/* -------------------------------------------------------------------------- */ /* class DeclareSygusFunctionCommand */ /* -------------------------------------------------------------------------- */ diff --git a/src/smt/command.h b/src/smt/command.h index f7c780dee..efb4f2f4a 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -675,38 +675,6 @@ class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand Type d_type; }; -/** Declares a sygus primed variable, for invariant problems - * - * We do not actually build expressions for the declared variables because they - * are unnecessary for building SyGuS problems. - */ -class CVC4_PUBLIC DeclareSygusPrimedVarCommand - : public DeclarationDefinitionCommand -{ - public: - DeclareSygusPrimedVarCommand(const std::string& id, Type type); - /** returns the declared primed variable's type */ - Type getType() const; - - /** invokes this command - * - * The type of the primed variable is communicated to the SMT engine for - * debugging purposes when a synthesis conjecture is built later on. - */ - void invoke(SmtEngine* smtEngine) override; - /** exports command to given expression manager */ - Command* exportTo(ExprManager* exprManager, - ExprManagerMapCollection& variableMap) override; - /** creates a copy of this command */ - Command* clone() const override; - /** returns this command's name */ - std::string getCommandName() const override; - - protected: - /** the type of the declared primed variable */ - Type d_type; -}; - /** Declares a sygus universal function variable */ class CVC4_PUBLIC DeclareSygusFunctionCommand : public DeclarationDefinitionCommand diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b826ef23d..a6d89aaf5 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1873,15 +1873,6 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type) // don't need to set that the conjecture is stale } -void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type) -{ - SmtScope smts(this); - finalOptionsAreSet(); - // do nothing (the command is spurious) - Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n"; - // don't need to set that the conjecture is stale -} - void SmtEngine::declareSygusFunctionVar(const std::string& id, Expr var, Type type) diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index b1e3313d8..8a9a60251 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -404,16 +404,6 @@ class CVC4_PUBLIC SmtEngine void declareSygusVar(const std::string& id, Expr var, Type type); /** - * Store information for debugging sygus invariants setup. - * - * Since in SyGuS the commands "declare-primed-var" are not necessary for - * building invariant constraints, we only use them to check that the number - * of variables declared corresponds to the number of arguments of the - * invariant-to-synthesize. - */ - void declareSygusPrimedVar(const std::string& id, Type type); - - /** * Add a function variable declaration. * * Is SyGuS semantics declared functions are treated in the same manner as |