From 6554ac787a5cd53e60801f9df739da2cf87e0e60 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 24 Sep 2013 05:13:11 +0300
Subject: [PATCH] add test case for substitution

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/test/expr_substitution.cpp | 50 ++++++++++++++++++++++++++++++++++
 src/test/main.cpp              |  1 +
 2 files changed, 51 insertions(+)
 create mode 100644 src/test/expr_substitution.cpp

diff --git a/src/test/expr_substitution.cpp b/src/test/expr_substitution.cpp
new file mode 100644
index 000000000..915ac96f3
--- /dev/null
+++ b/src/test/expr_substitution.cpp
@@ -0,0 +1,50 @@
+#include "expr_substitution.h"
+#include "smt_params.h"
+#include "substitution.h"
+#include "unifier.h"
+#include "bv_decl_plugin.h"
+#include "ast_pp.h"
+#include "arith_decl_plugin.h"
+#include "reg_decl_plugins.h"
+#include "th_rewriter.h"
+
+expr* mk_bv_xor(bv_util& bv, expr* a, expr* b) {
+    expr* args[2];
+    args[0] = a;
+    args[1] = b;
+    return bv.mk_bv_xor(2, args);
+}
+
+expr* mk_bv_and(bv_util& bv, expr* a, expr* b) {
+    expr* args[2];
+    args[0] = a;
+    args[1] = b;
+    ast_manager& m = bv.get_manager();
+    return m.mk_app(bv.get_family_id(), OP_BAND, 2, args);
+}
+
+void tst_expr_substitution() {
+    memory::initialize(0);
+    ast_manager m;
+    reg_decl_plugins(m);
+    bv_util bv(m);
+
+    expr_ref a(m), b(m), c(m);
+    expr_ref x(m);
+    x = m.mk_const(symbol("x"), bv.mk_sort(8));
+    a = mk_bv_and(bv, mk_bv_xor(bv, x,bv.mk_numeral(8,8)), mk_bv_xor(bv,x,x));
+    b = x;
+    c = bv.mk_bv_sub(x, bv.mk_numeral(4, 8));
+
+    expr_substitution subst(m);
+    subst.insert(b, c);
+    th_rewriter   rw(m);
+    rw.set_substitution(&subst);
+    
+    expr_ref   new_a(m);
+    proof_ref  pr(m);
+    rw(a, new_a, pr);
+
+    std::cout << mk_pp(new_a, m) << "\n";
+    
+}
diff --git a/src/test/main.cpp b/src/test/main.cpp
index 333456369..bc7e04124 100644
--- a/src/test/main.cpp
+++ b/src/test/main.cpp
@@ -215,6 +215,7 @@ int main(int argc, char ** argv) {
     TST(rcf);
     TST(polynorm);
     TST(qe_arith);
+    TST(expr_substitution);
 }
 
 void initialize_mam() {}