diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-18 22:51:50 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-18 22:51:50 -0700 |
commit | e8884b9b8ba86ce71807887cab87a5188cce4003 (patch) | |
tree | 3b56553ecc3227eafe7aca057c5e29cd8efb63e0 /src/smt/command.h | |
parent | 3054cd99db968eb85a9195b12e17e83a334e00cb (diff) |
Add logic check for define-fun(s)-rec (#4577)
This commit adds a logic check for `define-fun-rec`/`define-funs-rec` at
the level of the new API that checks whether the logic is quantified and
includes UF. To make sure that the parser actually executes that check,
this commit converts the `DefineFunctionRecCommand` command to use the
new API instead of the old one. This temporarily breaks the `exportTo`
functionality for `DefineFunctionRecCommand` but this is not currently
used within the CVC4 code base (and it seems unlikely that users use
commands).
Diffstat (limited to 'src/smt/command.h')
-rw-r--r-- | src/smt/command.h | 68 |
1 files changed, 39 insertions, 29 deletions
diff --git a/src/smt/command.h b/src/smt/command.h index e09dfe490..f7c780dee 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -39,6 +39,11 @@ namespace CVC4 { +namespace api { +class Solver; +class Term; +} // namespace api + class SmtEngine; class Command; class CommandStatus; @@ -186,27 +191,11 @@ class CVC4_PUBLIC CommandRecoverableFailure : public CommandStatus class CVC4_PUBLIC Command { - protected: - /** - * This field contains a command status if the command has been - * invoked, or NULL if it has not. This field is either a - * dynamically-allocated pointer, or it's a pointer to the singleton - * CommandSuccess instance. Doing so is somewhat asymmetric, but - * it avoids the need to dynamically allocate memory in the common - * case of a successful command. - */ - const CommandStatus* d_commandStatus; - - /** - * True if this command is "muted"---i.e., don't print "success" on - * successful execution. - */ - bool d_muted; - public: typedef CommandPrintSuccess printsuccess; Command(); + Command(api::Solver* solver); Command(const Command& cmd); virtual ~Command(); @@ -281,6 +270,25 @@ class CVC4_PUBLIC Command Expr operator()(Expr e) { return e.exportTo(d_exprManager, d_variableMap); } Type operator()(Type t) { return t.exportTo(d_exprManager, d_variableMap); } }; /* class Command::ExportTransformer */ + + /** The solver instance that this command is associated with. */ + api::Solver* d_solver; + + /** + * This field contains a command status if the command has been + * invoked, or NULL if it has not. This field is either a + * dynamically-allocated pointer, or it's a pointer to the singleton + * CommandSuccess instance. Doing so is somewhat asymmetric, but + * it avoids the need to dynamically allocate memory in the common + * case of a successful command. + */ + const CommandStatus* d_commandStatus; + + /** + * True if this command is "muted"---i.e., don't print "success" on + * successful execution. + */ + bool d_muted; }; /* class Command */ /** @@ -498,18 +506,20 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand class CVC4_PUBLIC DefineFunctionRecCommand : public Command { public: - DefineFunctionRecCommand(Expr func, - const std::vector<Expr>& formals, - Expr formula, + DefineFunctionRecCommand(api::Solver* solver, + api::Term func, + const std::vector<api::Term>& formals, + api::Term formula, bool global); - DefineFunctionRecCommand(const std::vector<Expr>& funcs, - const std::vector<std::vector<Expr> >& formals, - const std::vector<Expr>& formula, + DefineFunctionRecCommand(api::Solver* solver, + const std::vector<api::Term>& funcs, + const std::vector<std::vector<api::Term> >& formals, + const std::vector<api::Term>& formula, bool global); - const std::vector<Expr>& getFunctions() const; - const std::vector<std::vector<Expr> >& getFormals() const; - const std::vector<Expr>& getFormulas() const; + const std::vector<api::Term>& getFunctions() const; + const std::vector<std::vector<api::Term> >& getFormals() const; + const std::vector<api::Term>& getFormulas() const; void invoke(SmtEngine* smtEngine) override; Command* exportTo(ExprManager* exprManager, @@ -519,11 +529,11 @@ class CVC4_PUBLIC DefineFunctionRecCommand : public Command protected: /** functions we are defining */ - std::vector<Expr> d_funcs; + std::vector<api::Term> d_funcs; /** formal arguments for each of the functions we are defining */ - std::vector<std::vector<Expr> > d_formals; + std::vector<std::vector<api::Term> > d_formals; /** formulas corresponding to the bodies of the functions we are defining */ - std::vector<Expr> d_formulas; + std::vector<api::Term> d_formulas; /** * Stores whether this definition is global (i.e. should persist when * popping the user context. |