diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2019-05-17 15:53:17 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2019-05-17 15:53:17 -0500 |
| commit | 7e7ff7814e65721f955c23d8eca953cb3f0f5ad8 (patch) | |
| tree | 24e62338da4b47dbc955514cc31ff78727a1f0e8 /src/smt/model_blocker.h | |
| parent | 5c3c2046414417dfd4e1a15bee9471c82c082e0b (diff) | |
Format
Diffstat (limited to 'src/smt/model_blocker.h')
| -rw-r--r-- | src/smt/model_blocker.h | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h index 836515013..cc667fbf0 100644 --- a/src/smt/model_blocker.h +++ b/src/smt/model_blocker.h @@ -32,14 +32,13 @@ class ModelBlocker { public: /** get model blocker - * + * * This returns a disjunction of literals ~L1 V ... V ~Ln with the following * properties: * (1) L1 ... Ln hold in the current model (given by argument m), * (2) L1 ... Ln are literals that occur in assertions. */ - static Expr getModelBlocker(const std::vector<Expr>& assertions, - Model* m); + static Expr getModelBlocker(const std::vector<Expr>& assertions, Model* m); }; /* class TheoryModelCoreBuilder */ } // namespace CVC4 |