diff options
author | lianah <lianahady@gmail.com> | 2013-04-12 16:15:30 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-04-30 15:54:24 -0400 |
commit | 6a86536bd25fc7ffa305f25990cf37b8c6566c52 (patch) | |
tree | 197b931f8f391a21eebbf097fd0f4b5adeb53c09 /src/theory/theory_engine.cpp | |
parent | e4f5359675972341858fe167f454ed5da4d8c115 (diff) |
finished implementing bv to bool lifting and added --bv-to-bool option
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 442b1ef1c..6f965879d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -119,7 +119,8 @@ TheoryEngine::TheoryEngine(context::Context* context, d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), d_sharedTermsVisitor(d_sharedTerms), - d_unconstrainedSimp(context, logicInfo) + d_unconstrainedSimp(context, logicInfo), + d_bvToBoolPreprocessor() { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { d_theoryTable[theoryId] = NULL; @@ -1276,6 +1277,12 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { } } +Node TheoryEngine::ppBvToBool(TNode assertion) { + Node result = d_bvToBoolPreprocessor.liftBoolToBV(assertion); + result = Rewriter::rewrite(result); + return result; +} + Node TheoryEngine::ppSimpITE(TNode assertion) { Node result = d_iteSimplifier.simpITE(assertion); |