From e55c8b01a5f8f9be2948cbdcf8ead34ae981ee2c Mon Sep 17 00:00:00 2001
From: Guannan Wei <guannanwei@outlook.com>
Date: Thu, 3 Mar 2022 00:01:20 -0800
Subject: [PATCH] some experiment

---
 dev-clean/benchmarks/demo_benchmarks/nqueen.c | 14 +++++++----
 dev-clean/headers/llsc/smt_z3.hpp             | 24 ++++++++++++++++---
 .../src/test/scala/sai/llsc/TestLLSC.scala    |  2 ++
 3 files changed, 32 insertions(+), 8 deletions(-)

diff --git a/dev-clean/benchmarks/demo_benchmarks/nqueen.c b/dev-clean/benchmarks/demo_benchmarks/nqueen.c
index ab73c45a..2fa82716 100644
--- a/dev-clean/benchmarks/demo_benchmarks/nqueen.c
+++ b/dev-clean/benchmarks/demo_benchmarks/nqueen.c
@@ -1,12 +1,13 @@
 #ifdef KLEE
 #include "klee/klee.h"
 #endif
+#include "../../headers/llsc_client.h"
 
 // https://www.geeksforgeeks.org/n-queen-problem-backtracking-3/
 #define N 5
 #include <stdbool.h>
 #include <stdio.h>
-  
+
 bool isSafe(int board[N][N], int row, int col) {
     int i, j;
     for (i = 0; i < col; i++)
@@ -20,7 +21,7 @@ bool isSafe(int board[N][N], int row, int col) {
             return false;
     return true;
 }
-  
+
 bool solveNQUtil(int board[N][N], int col) {
     if (col >= N) return true;
     for (int i = 0; i < N; i++) {
@@ -39,15 +40,18 @@ bool solveNQ() {
 #ifdef KLEE
     klee_make_symbolic(board, sizeof(int) * N * N, "board");
 #else
-    make_symbolic(board, sizeof(int) * N * N);
+    for (int i = 0; i < N*N; i++) {
+      make_symbolic_whole(((int*)board)+i, sizeof(int));
+    }
+    //make_symbolic(board, sizeof(int) * N * N);
 #endif
     if (solveNQUtil(board, 0) == false) {
         return false;
     }
-  
+
     return true;
 }
-  
+
 int main()
 {
     solveNQ();
diff --git a/dev-clean/headers/llsc/smt_z3.hpp b/dev-clean/headers/llsc/smt_z3.hpp
index 987d5da3..21f72120 100644
--- a/dev-clean/headers/llsc/smt_z3.hpp
+++ b/dev-clean/headers/llsc/smt_z3.hpp
@@ -14,11 +14,24 @@ class CheckerZ3 : public Checker {
     solver* s = new solver(*c);
     return std::make_tuple(c, s);
   }
+
   context* g_ctx;
+  params* pr;
+  tactic* t;
   solver* g_solver;
 public:
   CheckerZ3() {
     std::cout << "Use Z3 " << Z3_get_full_version() << "\n";
+    g_ctx = new context;
+    pr = new params(*g_ctx);
+    pr->set("mul2concat", true);
+    t = new tactic(with(tactic(*g_ctx, "qfbv"), *pr) &
+               //tactic(*g_ctx, "solve-eqs") &
+               //tactic(*g_ctx, "qfbv") &
+               tactic(*g_ctx, "bit-blast") &
+               //tactic(*g_ctx, "aig") &
+               tactic(*g_ctx, "sat"));
+    g_solver = new solver(t->mk_solver());
   }
   ~CheckerZ3() { destroy_solvers(); }
   void init_solvers() override {
@@ -35,15 +48,20 @@ class CheckerZ3 : public Checker {
     }
   }
   instance get_my_thread_local_instance() {
-    return checker_map[std::this_thread::get_id()];
+    return {g_ctx, g_solver};
+    //return checker_map[std::this_thread::get_id()];
   }
   solver_result make_query(PC pc) override {
     auto pc_set = pc.get_path_conds();
     auto start = steady_clock::now();
+
     context* c; solver* s;
     std::tie(c, s) = get_my_thread_local_instance();
-    for (auto& e: pc_set)
-      s->add(construct_z3_expr(c, e));
+    for (auto& e: pc_set) {
+      auto t = construct_z3_expr(c, e);
+      s->add(t);
+    }
+    //std::cout << s->to_smt2() << "\n";
     auto result = s->check();
     auto end = steady_clock::now();
     solver_time += duration_cast<microseconds>(end - start);
diff --git a/dev-clean/src/test/scala/sai/llsc/TestLLSC.scala b/dev-clean/src/test/scala/sai/llsc/TestLLSC.scala
index 4e1ad3d7..5769c308 100644
--- a/dev-clean/src/test/scala/sai/llsc/TestLLSC.scala
+++ b/dev-clean/src/test/scala/sai/llsc/TestLLSC.scala
@@ -249,6 +249,8 @@ class TestImpCPSLLSC extends TestLLSC {
 class Playground extends TestLLSC {
   //testLLSC(new PureCPSLLSC, TestPrg(mp1048576, "mp1mTest_CPS", "@f", symArg(20), "--disable-solver", nPath(1048576)))
   val llsc = new PureCPSLLSC_Z3
+  //testLLSC(llsc, TestPrg(nqueen, "nQueens", "@main", noArg, None, nPath(1363)))
+  testLLSC(new PureCPSLLSC, TestPrg(nqueen, "nQueens_STP", "@main", noArg, None, nPath(1363)))
   //testLLSC(llsc, TestPrg(bubbleSort2Ground, "bubbleSort2Ground", "@main", 0, None, status(255)))
   //testLLSC(llsc, TestPrg(bubbleSortGround2, "bubbleSortGround2", "@main", 0, None, status(255)))