diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-12 11:14:08 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-12 11:14:08 -0500 |
| commit | 3ce6e00068c02286704143d82d5f044fdb356516 (patch) | |
| tree | 53d8403a8cc2c92db4cb815861f5c7cd56dee446 /src/smt/model_blocker.cpp | |
| parent | e93c443a0bfb1a66909e8467b24da399be3d01ac (diff) | |
Eliminate uses of Expr in SmtEngine interface (#5240)
This eliminates all use of Expr in the SmtEngine except in a few interfaces (setUserAttribute, getAssignment) whose signature is currently in question.
The next steps will be to (1) eliminate Expr from the smt/model.h interface, (2) replace Type by TypeNode in Sort.
Diffstat (limited to 'src/smt/model_blocker.cpp')
| -rw-r--r-- | src/smt/model_blocker.cpp | 23 |
1 files changed, 7 insertions, 16 deletions
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp index 8d232ed9e..9d15b5690 100644 --- a/src/smt/model_blocker.cpp +++ b/src/smt/model_blocker.cpp @@ -23,24 +23,15 @@ using namespace CVC4::kind; namespace CVC4 { -Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions, +Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions, theory::TheoryModel* m, options::BlockModelsMode mode, - const std::vector<Expr>& exprToBlock) + const std::vector<Node>& exprToBlock) { NodeManager* nm = NodeManager::currentNM(); // convert to nodes - std::vector<Node> tlAsserts; - for (const Expr& a : assertions) - { - Node an = Node::fromExpr(a); - tlAsserts.push_back(an); - } - std::vector<Node> nodesToBlock; - for (const Expr& eb : exprToBlock) - { - nodesToBlock.push_back(Node::fromExpr(eb)); - } + std::vector<Node> tlAsserts = assertions; + std::vector<Node> nodesToBlock = exprToBlock; Trace("model-blocker") << "Compute model blocker, assertions:" << std::endl; Node blocker; if (mode == options::BlockModelsMode::LITERALS) @@ -117,7 +108,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions, // rewrite, this ensures that e.g. the propositional value of // quantified formulas can be queried n = theory::Rewriter::rewrite(n); - Node vn = Node::fromExpr(m->getValue(n.toExpr())); + Node vn = m->getValue(n); Assert(vn.isConst()); if (vn.getConst<bool>() == cpol) { @@ -139,7 +130,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions, } else if (catom.getKind() == ITE) { - Node vcond = Node::fromExpr(m->getValue(cur[0].toExpr())); + Node vcond = m->getValue(cur[0]); Assert(vcond.isConst()); Node cond = cur[0]; Node branch; @@ -282,7 +273,7 @@ Expr ModelBlocker::getModelBlocker(const std::vector<Expr>& assertions, } } Trace("model-blocker") << "...model blocker is " << blocker << std::endl; - return blocker.toExpr(); + return blocker; } } /* namespace CVC4 */ |