summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2011-10-17 03:12:17 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2011-10-17 03:12:17 +0000
commitbb59480a36fb0f799af53676c07b8fca43c2fff4 (patch)
tree555fb1210e2e94ba09bb9dd447cac30a6ad2ab70 /src/theory/bv
parent5cb65d8beac0f06fcafbef99d109c09ad029b14d (diff)
Sharing work
Diffstat (limited to 'src/theory/bv')
-rw-r--r--src/theory/bv/theory_bv_rewriter.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 20da74ce8..11a55ca61 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -42,6 +42,10 @@ public:
return RewriteResponse(REWRITE_DONE, node);
}
+ static inline Node rewriteEquality(TNode node) {
+ return postRewrite(node).node;
+ }
+
static void init();
static void shutdown();
};/* class TheoryBVRewriter */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback