summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorlianah <lianahady@gmail.com>2013-04-30 16:43:09 -0400
committerlianah <lianahady@gmail.com>2013-04-30 16:43:09 -0400
commitdb93834744ae5e1c93404e6236e1b46348037770 (patch)
tree6387d38e2034150522c44004278c09a2d3e6ff80
parent2d9b058a6a5c977f2806965526320e6d5fed18fe (diff)
parent07c2ba8ec0fba4e63620ea4861a2c79ceb9d8507 (diff)
fixed merge conflicts
-rw-r--r--src/theory/bv/theory_bv.cpp2
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp8
2 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 9c64cbf77..b2f91e070 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -180,7 +180,7 @@ void TheoryBV::check(Effort e)
while (!done()) {
TNode fact = get().assertion;
- // checkForLemma(fact);
+ checkForLemma(fact);
for (unsigned i = 0; i < d_subtheories.size(); ++i) {
d_subtheories[i]->assertFact(fact);
}
diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index 5a43e2c57..0775cb1f8 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -106,16 +106,16 @@ RewriteResponse TheoryBVRewriter::RewriteUle(TNode node, bool preregister){
RewriteRule<UleMax>,
RewriteRule<ZeroUle>,
RewriteRule<UleZero>,
- RewriteRule<UleSelf>//,
- // RewriteRule<UleEliminate>
+ RewriteRule<UleSelf>,
+ RewriteRule<UleEliminate>
>::apply(node);
return RewriteResponse(resultNode == node ? REWRITE_DONE : REWRITE_AGAIN, resultNode);
}
RewriteResponse TheoryBVRewriter::RewriteSle(TNode node, bool preregister){
Node resultNode = LinearRewriteStrategy
- < RewriteRule <EvalSle>//,
- // RewriteRule <SleEliminate>
+ < RewriteRule <EvalSle>,
+ RewriteRule <SleEliminate>
>::apply(node);
return RewriteResponse(resultNode == node? REWRITE_DONE : REWRITE_AGAIN, resultNode);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback