diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-10-21 19:32:08 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-10-21 19:32:08 -0500 |
commit | 81d4a2a0e337e341ac1373de0be8762617372ffc (patch) | |
tree | eec38cb65373f9df09fde442fc69bd2088f7d005 /src/smt/model_blocker.h | |
parent | 638c0bfdc798116925f839118dffd86581a58d43 (diff) | |
parent | f9de5395d78bc5338ca800e539e91795730cbd29 (diff) |
Merge branch 'master' into fixErrorSetfixErrorSet
Diffstat (limited to 'src/smt/model_blocker.h')
-rw-r--r-- | src/smt/model_blocker.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 42219e220..5e41de6a3 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -22,6 +22,7 @@ #include "expr/node.h" #include "options/smt_options.h" +#include "smt/env_obj.h" namespace cvc5 { @@ -32,9 +33,10 @@ class TheoryModel; /** * A utility for blocking the current model. */ -class ModelBlocker +class ModelBlocker : protected EnvObj { public: + ModelBlocker(Env& e); /** get model blocker * * This returns a disjunction of literals ~L1 V ... V ~Ln with the following @@ -63,7 +65,7 @@ class ModelBlocker * our input. In other words, we do not return ~(x < 0) V ~(w < 0) since the * left disjunct is always false. */ - static Node getModelBlocker( + Node getModelBlocker( const std::vector<Node>& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, |