parent
b46a40452f
commit
42fb856148
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
@ -1,3 +1,3 @@
|
||||
Start testing: Jun 25 08:28 CST
|
||||
Start testing: Jun 26 13:14 CST
|
||||
----------------------------------------------------------
|
||||
End testing: Jun 25 08:28 CST
|
||||
End testing: Jun 26 13:14 CST
|
||||
|
||||
Binary file not shown.
Binary file not shown.
@ -1,3 +1,4 @@
|
||||
#include "z3++.h"
|
||||
|
||||
void recordBranches(z3::expr_vector &OldVec);
|
||||
void searchStrategy(z3::expr_vector &OldVec);
|
||||
|
||||
@ -1,6 +1,68 @@
|
||||
#include "Strategy.h"
|
||||
#include <iostream>
|
||||
|
||||
/*
|
||||
static const char *NOT = "not";
|
||||
std::vector<std::string> Branches;
|
||||
/**
|
||||
* Implement your search strategy.
|
||||
*/
|
||||
void searchStrategy(z3::expr_vector &OldVec) { /* Add your code here */ }
|
||||
|
||||
void recordBranches(z3::expr_vector &OldVec){
|
||||
for (auto && E : OldVec) {
|
||||
if(E.to_string().find('X') == std::string::npos){
|
||||
continue;
|
||||
}
|
||||
if(std::find(Branches.begin(), Branches.end(),E.to_string()) == Branches.end()){
|
||||
Branches.push_back(E.to_string().c_str());
|
||||
}
|
||||
}
|
||||
/*
|
||||
for(const auto &E : Branches){
|
||||
printf("%s\n", E.c_str());
|
||||
}
|
||||
*/
|
||||
}
|
||||
|
||||
void searchStrategy(z3::expr_vector &OldVec) {
|
||||
int i = OldVec.size()-1;
|
||||
if(i<0){
|
||||
return;
|
||||
}
|
||||
auto e = OldVec[i];
|
||||
if(e.to_string().find('X') == std::string::npos){
|
||||
OldVec.pop_back();
|
||||
searchStrategy(OldVec);
|
||||
return;
|
||||
}
|
||||
//printf("e%d:%s\n\n",i, e.to_string().c_str());
|
||||
if(e.to_string().substr(1, 3) != NOT){
|
||||
std::string newExpr = e.to_string();
|
||||
//printf("expr0:%s\n", newExpr.c_str());
|
||||
if(newExpr.find("false") != std::string::npos){
|
||||
newExpr = newExpr.replace(newExpr.end()-6, newExpr.end()-1,"true");
|
||||
} else{
|
||||
newExpr = newExpr.replace(newExpr.end()-5, newExpr.end()-1,"false");
|
||||
}
|
||||
//printf("expr1:%s\n", newExpr.c_str());
|
||||
if(std::find(Branches.begin(), Branches.end(), newExpr) == Branches.end()){
|
||||
//printf("newpath\n");
|
||||
OldVec.pop_back();
|
||||
OldVec.push_back(not e);
|
||||
//printf("new\n");
|
||||
/*
|
||||
for(auto EX : OldVec){
|
||||
printf("%s\n", EX.to_string().c_str());
|
||||
}
|
||||
*/
|
||||
} else{
|
||||
//printf("back\n");
|
||||
OldVec.pop_back();
|
||||
searchStrategy(OldVec);
|
||||
}
|
||||
}
|
||||
else {
|
||||
//printf("unsat\n");
|
||||
OldVec.pop_back();
|
||||
searchStrategy(OldVec);
|
||||
}
|
||||
}
|
||||
|
||||
@ -1 +1,11 @@
|
||||
B5
|
||||
(= (< 0 X0) true)
|
||||
(= (< (+ 0 1) X0) true)
|
||||
(= (< (+ 0 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1 1 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1 1 1 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1 1 1 1 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1 1 1 1 1 1 1) X0) false)
|
||||
(= (= (mod (* 1 2 2 2 2 2 2 2 2 2) 1022) 2) false)
|
||||
|
||||
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file not shown.
@ -1 +1 @@
|
||||
X0,2
|
||||
X0,10
|
||||
|
||||
@ -1,23 +1,53 @@
|
||||
=== Inputs ===
|
||||
X0 : 1850737439
|
||||
X1 : 1423391991
|
||||
X2 : 1736296805
|
||||
X0 : 9
|
||||
|
||||
=== Symbolic Memory ===
|
||||
140723196736720 : X2
|
||||
140723196736724 : X1
|
||||
140723196736728 : X0
|
||||
140723196736732 : 0
|
||||
R0 : 1270725261
|
||||
140722793318076 : (+ 0 1 1 1 1 1 1 1 1 1)
|
||||
140722793318080 : (* 1 2 2 2 2 2 2 2 2 2)
|
||||
140722793318084 : 1022
|
||||
140722793318088 : X0
|
||||
140722793318092 : 0
|
||||
R0 : 2124147437
|
||||
R1 : 32764
|
||||
R2 : (- 1406716656)
|
||||
R3 : X0
|
||||
R4 : (= X0 1)
|
||||
R5 : (= (= X0 1) true)
|
||||
R6 : (= (= X0 1) false)
|
||||
R2 : (- 1810135296)
|
||||
R3 : 32764
|
||||
R5 : (+ 0 1 1 1 1 1 1 1 1 1)
|
||||
R6 : X0
|
||||
R7 : (< (+ 0 1 1 1 1 1 1 1 1 1) X0)
|
||||
R8 : (= (< (+ 0 1 1 1 1 1 1 1 1 1) X0) true)
|
||||
R9 : (= (< (+ 0 1 1 1 1 1 1 1 1 1) X0) false)
|
||||
R10 : (* 1 2 2 2 2 2 2 2 2)
|
||||
R11 : (* 1 2 2 2 2 2 2 2 2 2)
|
||||
R13 : (+ 0 1 1 1 1 1 1 1 1)
|
||||
R14 : (+ 0 1 1 1 1 1 1 1 1 1)
|
||||
R15 : (* 1 2 2 2 2 2 2 2 2 2)
|
||||
R16 : 1022
|
||||
R17 : (mod (* 1 2 2 2 2 2 2 2 2 2) 1022)
|
||||
R18 : (= (mod (* 1 2 2 2 2 2 2 2 2 2) 1022) 2)
|
||||
R19 : (= (= (mod (* 1 2 2 2 2 2 2 2 2 2) 1022) 2) true)
|
||||
R20 : (= (= (mod (* 1 2 2 2 2 2 2 2 2 2) 1022) 2) false)
|
||||
|
||||
=== Path Condition ===
|
||||
B5 : (= (= X0 1) false)
|
||||
B1 : (= (< 0 X0) true)
|
||||
B1 : (= (< (+ 0 1) X0) true)
|
||||
B1 : (= (< (+ 0 1 1) X0) true)
|
||||
B1 : (= (< (+ 0 1 1 1) X0) true)
|
||||
B1 : (= (< (+ 0 1 1 1 1) X0) true)
|
||||
B1 : (= (< (+ 0 1 1 1 1 1) X0) true)
|
||||
B1 : (= (< (+ 0 1 1 1 1 1 1) X0) true)
|
||||
B1 : (= (< (+ 0 1 1 1 1 1 1 1) X0) true)
|
||||
B1 : (= (< (+ 0 1 1 1 1 1 1 1 1) X0) true)
|
||||
B3 : (= (< (+ 0 1 1 1 1 1 1 1 1 1) X0) false)
|
||||
B5 : (= (= (mod (* 1 2 2 2 2 2 2 2 2 2) 1022) 2) false)
|
||||
|
||||
=== New Path Condition ===
|
||||
(= (= X0 1) false)
|
||||
(= (< 0 X0) true)
|
||||
(= (< (+ 0 1) X0) true)
|
||||
(= (< (+ 0 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1 1 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1 1 1 1 1) X0) true)
|
||||
(= (< (+ 0 1 1 1 1 1 1 1 1) X0) true)
|
||||
(not (= (< (+ 0 1 1 1 1 1 1 1 1 1) X0) false))
|
||||
|
||||
Loading…
Reference in new issue