diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-10-28 12:04:06 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-28 17:04:06 +0000 |
| commit | 08eb3932ec2e666c40275c8eab1ca49a61158943 (patch) | |
| tree | accf4982976e2161080e9bf56506eec3beeb630b /src/smt/command.h | |
| parent | dd850b74cb3ff5ab043ccfa124443791dcbcc0bf (diff) | |
Add a `define-fun` command for each `:named` term. (#7308)
This PR is step towards enabling -o raw-benchmark for regressions. It creates a define-fun command for each named term. This allows us to reparse dumped benchmarks containing named terms, but we still lose track of those terms and do not print them in response to (get-assignment) and (get-unsat-core) commands. This PR also simplifies the interface for DefineFunCommand interface and removes support for (define ...) command.
Diffstat (limited to 'src/smt/command.h')
| -rw-r--r-- | src/smt/command.h | 32 |
1 files changed, 9 insertions, 23 deletions
diff --git a/src/smt/command.h b/src/smt/command.h index 400f3492e..5733eb3e5 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -494,17 +494,15 @@ class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand { public: DefineFunctionCommand(const std::string& id, - api::Term func, - api::Term formula, - bool global); + api::Sort sort, + api::Term formula); DefineFunctionCommand(const std::string& id, - api::Term func, const std::vector<api::Term>& formals, - api::Term formula, - bool global); + api::Sort sort, + api::Term formula); - api::Term getFunction() const; const std::vector<api::Term>& getFormals() const; + api::Sort getSort() const; api::Term getFormula() const; void invoke(api::Solver* solver, SymbolManager* sm) override; @@ -516,17 +514,12 @@ class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand Language language = Language::LANG_AUTO) const override; protected: - /** The function we are defining */ - api::Term d_func; /** The formal arguments for the function we are defining */ std::vector<api::Term> d_formals; + /** The co-domain sort of the function we are defining */ + api::Sort d_sort; /** The formula corresponding to the body of the function we are defining */ api::Term d_formula; - /** - * Stores whether this definition is global (i.e. should persist when - * popping the user context. - */ - bool d_global; }; /* class DefineFunctionCommand */ /** @@ -539,12 +532,10 @@ class CVC5_EXPORT DefineFunctionRecCommand : public Command public: DefineFunctionRecCommand(api::Term func, const std::vector<api::Term>& formals, - api::Term formula, - bool global); + api::Term formula); DefineFunctionRecCommand(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<api::Term>& formula); const std::vector<api::Term>& getFunctions() const; const std::vector<std::vector<api::Term> >& getFormals() const; @@ -565,11 +556,6 @@ class CVC5_EXPORT DefineFunctionRecCommand : public Command std::vector<std::vector<api::Term> > d_formals; /** formulas corresponding to the bodies of the functions we are defining */ std::vector<api::Term> d_formulas; - /** - * Stores whether this definition is global (i.e. should persist when - * popping the user context. - */ - bool d_global; }; /* class DefineFunctionRecCommand */ /** |