diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-02-19 20:29:58 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-02-19 20:29:58 +0000 |
| commit | ce0e796ad92f040fb75435bd7880bc28a60b0374 (patch) | |
| tree | 00a390f0347a30978b482cbbb6e074c6dc5a99d2 /src/smt | |
| parent | 34b455b1d74fdc06dd2f874fa2bc8d73127fbedf (diff) | |
* Attribute infrastructure -- static design. Documentation is coming.
See test/unit/expr/node_white.h for use examples, including how to
define new attribute kinds.
Also:
* fixes to test infrastructure
* minor changes to code formatting throughout
* attribute tests in test/unit/expr/node_white.h
* fixes to NodeManagerScope ordering
* use NodeValue::getKind() to properly deal with UNDEFINED_KIND
(removing compiler warning)
* ExprManager: add proper NodeManagerScope to public-facing member
functions
* store variable names and types in attributes
* SoftNode is a placeholder, not a real implementation
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/smt_engine.cpp | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 8bca39df4..24795111f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -75,8 +75,8 @@ void SmtEngine::addFormula(const Node& e) { } Result SmtEngine::checkSat(const BoolExpr& e) { - Debug("smt") << "SMT checkSat(" << e << ")" << std::endl; NodeManagerScope nms(d_nodeManager); + Debug("smt") << "SMT checkSat(" << e << ")" << std::endl; Node node_e = preprocess(e.getNode()); addFormula(node_e); Result r = check().asSatisfiabilityResult(); @@ -85,8 +85,8 @@ Result SmtEngine::checkSat(const BoolExpr& e) { } Result SmtEngine::query(const BoolExpr& e) { - Debug("smt") << "SMT query(" << e << ")" << std::endl; NodeManagerScope nms(d_nodeManager); + Debug("smt") << "SMT query(" << e << ")" << std::endl; Node node_e = preprocess(d_nodeManager->mkNode(NOT, e.getNode())); addFormula(node_e); Result r = check().asValidityResult(); @@ -95,25 +95,34 @@ Result SmtEngine::query(const BoolExpr& e) { } Result SmtEngine::assertFormula(const BoolExpr& e) { - Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl; NodeManagerScope nms(d_nodeManager); + Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl; Node node_e = preprocess(e.getNode()); addFormula(node_e); return quickCheck().asValidityResult(); } Expr SmtEngine::simplify(const Expr& e) { + NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT simplify(" << e << ")" << std::endl; - Expr simplify(const Expr& e); + Unimplemented(); +} + +Model SmtEngine::getModel() { + NodeManagerScope nms(d_nodeManager); Unimplemented(); } void SmtEngine::push() { + NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT push()" << std::endl; + Unimplemented(); } void SmtEngine::pop() { + NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT pop()" << std::endl; + Unimplemented(); } }/* CVC4 namespace */ |