Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

experiment with z3 tactics #64

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

experiment with z3 tactics #64

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 9 additions & 5 deletions dev-clean/benchmarks/demo_benchmarks/nqueen.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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++)
Expand All @@ -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++) {
Expand All @@ -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();
Expand Down
24 changes: 21 additions & 3 deletions dev-clean/headers/llsc/smt_z3.hpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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);
Expand Down
2 changes: 2 additions & 0 deletions dev-clean/src/test/scala/sai/llsc/TestLLSC.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)))

Expand Down