diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-28 16:21:53 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-28 16:21:53 -0500 |
| commit | 66e80ff2464bfd7fb0904d972b43b96ff2bd9da8 (patch) | |
| tree | 5a5d1918a0c9f696edf7b9be556f879f673aacd4 /src/api | |
| parent | eb812afac2884131b21948aee3da9d8c1e92ba98 (diff) | |
Remove more uses of Expr (#5357)
This PR removes more uses of Expr, mostly related to UnsatCore.
It makes UnsatCore a cvc4_private object storing Node instead of Expr.
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cvc4cpp.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index e198c0d89..be82a517f 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -51,6 +51,7 @@ #include "options/main_options.h" #include "options/options.h" #include "options/smt_options.h" +#include "proof/unsat_core.h" #include "smt/model.h" #include "smt/smt_engine.h" #include "smt/smt_mode.h" @@ -5145,7 +5146,7 @@ std::vector<Term> Solver::getUnsatCore(void) const * return std::vector<Term>(core.begin(), core.end()); * here since constructor is private */ std::vector<Term> res; - for (const Expr& e : core) + for (const Node& e : core) { res.push_back(Term(this, e)); } |