diff options
Diffstat (limited to 'src/theory/subs_minimize.h')
| -rw-r--r-- | src/theory/subs_minimize.h | 37 |
1 files changed, 19 insertions, 18 deletions
diff --git a/src/theory/subs_minimize.h b/src/theory/subs_minimize.h index c78467508..571f629dd 100644 --- a/src/theory/subs_minimize.h +++ b/src/theory/subs_minimize.h @@ -21,6 +21,7 @@ #include <vector> #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { namespace theory { @@ -30,10 +31,10 @@ namespace theory { * This class is used for finding a minimal substitution under which an * evaluation holds. */ -class SubstitutionMinimize +class SubstitutionMinimize : protected EnvObj { public: - SubstitutionMinimize(); + SubstitutionMinimize(Env& env); ~SubstitutionMinimize() {} /** find * @@ -45,11 +46,11 @@ class SubstitutionMinimize * If t { vars -> subs } does not rewrite to target, this method returns * false. */ - static bool find(Node t, - Node target, - const std::vector<Node>& vars, - const std::vector<Node>& subs, - std::vector<Node>& reqVars); + bool find(Node t, + Node target, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + std::vector<Node>& reqVars); /** find with implied * * This method should be called on a formula t. @@ -73,26 +74,26 @@ class SubstitutionMinimize * to appear in reqVars, whereas those later in the vars are more likely to * appear in impliedVars. */ - static bool findWithImplied(Node t, - const std::vector<Node>& vars, - const std::vector<Node>& subs, - std::vector<Node>& reqVars, - std::vector<Node>& impliedVars); + bool findWithImplied(Node t, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + std::vector<Node>& reqVars, + std::vector<Node>& impliedVars); private: /** Common helper function for the above functions. */ - static bool findInternal(Node t, - Node target, - const std::vector<Node>& vars, - const std::vector<Node>& subs, - std::vector<Node>& reqVars); + bool findInternal(Node t, + Node target, + const std::vector<Node>& vars, + const std::vector<Node>& subs, + std::vector<Node>& reqVars); /** is singular arg * * Returns true if * <k>( ... t_{arg-1}, n, t_{arg+1}...) = c * always holds for some constant c. */ - static bool isSingularArg(Node n, Kind k, unsigned arg); + bool isSingularArg(Node n, Kind k, unsigned arg); }; } // namespace theory |