diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-06 20:57:44 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-06 20:57:44 -0600 |
commit | 691abe521ea8a7e87db51e22880cf101d59bf3e7 (patch) | |
tree | a3e7e336a64597a03b3142bd6cd39c7d42322bec /src/smt/command.h | |
parent | a97411d90188fc3ceda419faf7be4b3508e305a5 (diff) |
Add command for define-fun-rec and add to API (#1412)
Diffstat (limited to 'src/smt/command.h')
-rw-r--r-- | src/smt/command.h | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/src/smt/command.h b/src/smt/command.h index 33f58aa99..ba7baa738 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -464,6 +464,39 @@ public: };/* class DefineNamedFunctionCommand */ /** + * The command when parsing define-fun-rec or define-funs-rec. + * This command will assert a set of quantified formulas that specify + * the (mutually recursive) function definitions provided to it. + */ +class CVC4_PUBLIC DefineFunctionRecCommand : public Command +{ + public: + DefineFunctionRecCommand(Expr func, + const std::vector<Expr>& formals, + Expr formula) throw(); + DefineFunctionRecCommand(const std::vector<Expr>& funcs, + const std::vector<std::vector<Expr> >& formals, + const std::vector<Expr>& formula) throw(); + ~DefineFunctionRecCommand() throw() {} + const std::vector<Expr>& getFunctions() const throw(); + const std::vector<std::vector<Expr> >& getFormals() const throw(); + const std::vector<Expr>& getFormulas() const throw(); + void invoke(SmtEngine* smtEngine) override; + Command* exportTo(ExprManager* exprManager, + ExprManagerMapCollection& variableMap) override; + Command* clone() const override; + std::string getCommandName() const throw() override; + + protected: + /** functions we are defining */ + std::vector<Expr> d_funcs; + /** formal arguments for each of the functions we are defining */ + std::vector<std::vector<Expr> > d_formals; + /** formulas corresponding to the bodies of the functions we are defining */ + std::vector<Expr> d_formulas; +}; /* class DefineFunctionRecCommand */ + +/** * The command when an attribute is set by a user. In SMT-LIBv2 this is done * via the syntax (! expr :attr) */ |