summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
authorlianah <lianahady@gmail.com>2013-04-12 16:15:30 -0400
committerlianah <lianahady@gmail.com>2013-04-30 15:54:24 -0400
commit6a86536bd25fc7ffa305f25990cf37b8c6566c52 (patch)
tree197b931f8f391a21eebbf097fd0f4b5adeb53c09 /src/theory/theory_engine.cpp
parente4f5359675972341858fe167f454ed5da4d8c115 (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.cpp9
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);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback