diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-12 21:10:36 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-12 21:10:36 +0000 |
commit | 3d97646be5eb3f2b50028875f4d899698228e8c7 (patch) | |
tree | 691e57f07b76c3413cebabb7ece4536eb309de16 /src/prop | |
parent | 2bc4c351bbf89103577fa9f33ebb395f5d61826a (diff) |
hooked up "we are incomplete" flag after conversation with Tim (a theory notifies the theory engine through its output channel); some cleanup; add a regression for bug #216
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/prop_engine.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index de60b5f7d..d7b1e6d99 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -58,13 +58,12 @@ public: }; PropEngine::PropEngine(const Options* opts, DecisionEngine* de, - TheoryEngine* te, Context* context) -: d_inCheckSat(false), + TheoryEngine* te, Context* context) : + d_inCheckSat(false), d_options(opts), d_decisionEngine(de), d_theoryEngine(te), - d_context(context) -{ + d_context(context) { Debug("prop") << "Constructing the PropEngine" << endl; d_satSolver = new SatSolver(this, d_theoryEngine, d_context, d_options); d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver); @@ -129,6 +128,9 @@ Result PropEngine::checkSat() { Debug("prop") << "PropEngine::checkSat() => " << (result ? "true" : "false") << endl; + if(result && d_theoryEngine->isIncomplete()) { + return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE); + } return Result(result ? Result::SAT : Result::UNSAT); } |