diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-08 20:26:11 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-08 20:26:11 -0500 |
commit | 2f8caabd570dd5bb2936d9f094b7b302a510aa6d (patch) | |
tree | 5ae3497d2dcd9bf39cc0686a1a0d23b0113571d2 /src/smt/defined_function.h | |
parent | df1ea6b9cdc1f424073151d0f7fda639d4405622 (diff) |
Split ProcessAssertions module from SmtEngine (#4210)
This is a step towards refactoring the SmtEngine. It splits several core components of SmtEnginePrivate to its own independent module, ProcessAssertions which is responsible for applying preprocessing passes , simplification and expand definitions.
The main change involved moving these functions from SmtEnginePrivate to this new class. A few other minor changes were done to make this move:
A few things changed order within processAssertions to allow SmtEnginePrivate-specific things to happen outside of the main scope of processAssertions.
processAssertions had some logic to catch incompatible options and silently disable options. This was moved to setDefaults.
A few data members in SmtEngine were moved to ProcessAssertions.
Two utilities that were sitting in smt_engine.cpp were moved to their own files.
Another refactoring step will be to make ProcessAssertions take only the utilities it needs instead of taking a SmtEngine reference. This requires further detangling of Options.
Diffstat (limited to 'src/smt/defined_function.h')
-rw-r--r-- | src/smt/defined_function.h | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/src/smt/defined_function.h b/src/smt/defined_function.h new file mode 100644 index 000000000..b141ef9cb --- /dev/null +++ b/src/smt/defined_function.h @@ -0,0 +1,60 @@ +/********************* */ +/*! \file defined_function.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Defined function data structure + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__SMT__DEFINED_FUNCTION_H +#define CVC4__SMT__DEFINED_FUNCTION_H + +#include <vector> + +#include "expr/node.h" + +namespace CVC4 { +namespace smt { + +/** + * Representation of a defined function. We keep these around in + * SmtEngine to permit expanding definitions late (and lazily), to + * support getValue() over defined functions, to support user output + * in terms of defined functions, etc. + */ +class DefinedFunction +{ + public: + DefinedFunction() {} + DefinedFunction(Node func, std::vector<Node>& formals, Node formula) + : d_func(func), d_formals(formals), d_formula(formula) + { + } + /** get the function */ + Node getFunction() const { return d_func; } + /** get the formal argument list of the function */ + const std::vector<Node>& getFormals() const { return d_formals; } + /** get the formula that defines it */ + Node getFormula() const { return d_formula; } + + private: + /** the function */ + Node d_func; + /** the formal argument list */ + std::vector<Node> d_formals; + /** the formula */ + Node d_formula; +}; /* class DefinedFunction */ + +} // namespace smt +} // namespace CVC4 + +#endif /* CVC4__SMT__DEFINED_FUNCTION_H */ |