diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-14 13:35:53 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-12-14 13:35:53 -0600 |
commit | e16ab44a2b4622bb5745633cbafd43a0023a518c (patch) | |
tree | d980bdc3dc771abfc8101036d1e2aaebc8020134 /src/theory/arith/bound_inference.h | |
parent | ad34df900d79aad64558b354a866870715bfd007 (diff) | |
parent | effb0d47ba5bfaebae17dcd06153489dccd90eff (diff) |
Merge branch 'master' into cav22-stringscav22-strings
Diffstat (limited to 'src/theory/arith/bound_inference.h')
-rw-r--r-- | src/theory/arith/bound_inference.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/arith/bound_inference.h b/src/theory/arith/bound_inference.h index e8d7a294f..a3043ee93 100644 --- a/src/theory/arith/bound_inference.h +++ b/src/theory/arith/bound_inference.h @@ -21,6 +21,7 @@ #include <vector> #include "expr/node.h" +#include "smt/env_obj.h" namespace cvc5 { namespace theory { @@ -53,9 +54,10 @@ namespace arith { * A utility class that extracts direct bounds on arithmetic terms from theory * atoms. */ - class BoundInference + class BoundInference : protected EnvObj { public: + BoundInference(Env& env); void reset(); /** @@ -110,8 +112,6 @@ namespace arith { /** Print the current variable bounds. */ std::ostream& operator<<(std::ostream& os, const BoundInference& bi); -std::map<Node, std::pair<Node,Node>> getBounds(const std::vector<Node>& assertions); - } // namespace arith } // namespace theory } // namespace cvc5 |