diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-12-08 10:10:20 +0000 |
commit | 2163539a8b839acf98bda0e1a65f1fcca5232fb2 (patch) | |
tree | 207a09896626f678172ec774459defa6690b0200 /src/smt/smt_engine.cpp | |
parent | abe5fb451ae66a4bedc88d870e99f76de4eb323c (diff) |
work on propositional layer, expression builder support for large expressions, output classes, and minisat
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 05ee12462..412c0f3af 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -27,11 +27,12 @@ void SmtEngine::processAssertionList() { for(std::vector<Expr>::iterator i = d_assertions.begin(); i != d_assertions.end(); ++i) - ;//d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i); + d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i); } Result SmtEngine::check() { processAssertionList(); + d_prop.solve(d_expr); return Result(Result::VALIDITY_UNKNOWN); } @@ -56,7 +57,7 @@ Result SmtEngine::query(Expr e) { return check(); } -Result SmtEngine::assert(Expr e) { +Result SmtEngine::assertFormula(Expr e) { e = preprocess(e); addFormula(e); return quickCheck(); |