Skip to content

Commit

Permalink
ERROR in array
Browse files Browse the repository at this point in the history
  • Loading branch information
@yangziyiiii
yangziyiiii committed Dec 2, 2024
1 parent c24c84b commit b31b679
Show file tree
Hide file tree
Showing 2 changed files with 98 additions and 19 deletions.
52 changes: 37 additions & 15 deletions apps/idpv/btor_sweeping.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@
#include <chrono>
#include <gmp.h>
#include <gmpxx.h>
#include <iostream>

#include "btor_sweeping.h"
#include "smt-switch/utils.h"
Expand Down Expand Up @@ -65,15 +66,15 @@ class GmpRandStateGuard
mpz_urandomb(rand_num, state, 128);
}

operator gmp_randstate_t &() { return state; }
// operator gmp_randstate_t &() { return state; }
};

std::chrono::time_point<std::chrono::high_resolution_clock> last_time_point;
void print_time() {
auto now = std::chrono::high_resolution_clock::now();
auto elapsed_time = std::chrono::duration_cast<std::chrono::milliseconds>(now - last_time_point).count();
last_time_point = now; // Update last time point
cout << "[" << elapsed_time << " ms] ";
std::cout << "[" << elapsed_time << " ms] ";
}

int main() {
Expand Down Expand Up @@ -126,6 +127,17 @@ int main() {
std::unordered_map<size_t, TermVec> hash_term_map; // hash -> TermVec
std::unordered_map<Term, Term> substitution_map; // term -> term, for substitution

auto array_table_1 = sts1.init();
auto array_table_2 = sts2.init();
// cout << "array_table_1: " << array_table_1->to_string() << endl;
// cout << "array_table_2: " << array_table_2->to_string() << endl;

TermVec out;
std::unordered_map<Term, Term> array_map; //array.index -> array.value
//TODO:
array_conjunctive_partition(array_table_1, out, true, array_map);


//simulation
GmpRandStateGuard rand_guard;
int num_iterations = 10;
Expand Down Expand Up @@ -153,7 +165,10 @@ int main() {

} // end of simulation

cout << "-----node_data_map [a_key_term]size: " << node_data_map[a_input_term].get_simulation_data().size() << endl;
assert(node_data_map[a_key_term].get_simulation_data().size() == num_iterations);
assert(node_data_map[a_input_term].get_simulation_data().size() == num_iterations);
assert(node_data_map[b_key_term].get_simulation_data().size() == num_iterations);
assert(node_data_map[b_input_term].get_simulation_data().size() == num_iterations);

//start post order traversal
std::stack<std::pair<Term,bool>> node_stack;
Expand All @@ -176,13 +191,12 @@ int main() {
visited = true;
} else {
if(current->is_value()) { //constant
//FIXME: use btorbv to store data
auto current_str = current->to_string();
auto current_bv = btor_bv_char_to_bv(current_str.data()); // Btor Bit Vector Type

if(!current_str.empty() && current_str.find("#b") == 0) {
current_str = current_str.substr(2);
}
cout << "current_str: " << current_str << endl;
auto current_bv = btor_bv_char_to_bv(current_str.data());

// auto node_bv_hash = btor_bv_hash(current_bv);
// if(hash_term_map.find(node_bv_hash) == hash_term_map.end()){
Expand All @@ -197,19 +211,17 @@ int main() {
nd.add_data(*current_bv);
}
node_data_map.insert({current, nd});
cout << "node_data_map size: " << node_data_map.size() << endl;
cout << "simulation_data size: " << nd.get_simulation_data().size() << endl;
assert (nd.get_simulation_data().size() == num_iterations);
btor_bv_free(current_bv);

}
else if(current->is_symbol()) { // variants only for leaf nodes
cout << "This is leaf node" << endl;

cout << "current: " << current->to_string() << endl;
cout << node_data_map[current].get_simulation_data().size() << endl;


assert(node_data_map.find(current) != node_data_map.end());

}
else { // compute simulation data for current node
auto op_type = current->get_op();
Expand All @@ -218,19 +230,18 @@ int main() {
auto child_size = children.size();
cout << "children size: " << child_size << endl;

if(child_size == 2 && visited) {
if(child_size == 2 && visited && op_type.prim_op != PrimOp::Select) {
std::cout << "This is a 2-child node." << std::endl;
NodeData nd(current, current->get_sort()->get_width());

for(size_t i = 0; i < num_iterations; i++) {
auto & sim_data_1 = node_data_map[children[0]].get_simulation_data();
auto & sim_data_2 = node_data_map[children[1]].get_simulation_data();

cout << sim_data_1.size() << " " << sim_data_2.size() << endl;
assert(sim_data_1.size() == num_iterations && sim_data_2.size() == num_iterations);

auto btor_child_1 = sim_data_1[i];
auto btor_child_2 = sim_data_2[i];
auto btor_child_2 = sim_data_2[i];

//FIXME: whether to extend bit width or not
auto btor_child_1_fix_width = btor_bv_uext(&btor_child_1, 128 - btor_child_1.width);
Expand All @@ -255,7 +266,7 @@ int main() {
}
node_data_map.insert({current, nd});
}
else if(child_size == 1 && visited) {
else if(child_size == 1 && visited && op_type.prim_op != PrimOp::Select) {
std::cout << "This is a 1-child node." << std::endl;
NodeData nd(current, current->get_sort()->get_width());

Expand Down Expand Up @@ -293,6 +304,17 @@ int main() {
}
node_data_map.insert({current, nd});
}
else if(op_type.prim_op == PrimOp::Select) {
cout << "This is a Array node" << endl;
//TODO:

}

else if(op_type.prim_op == PrimOp::Store) {
cout << "This is a Store node" << endl;
//TODO:
}

else {
throw NotImplementedException("Unsupported operator type2: " + op_type.to_string() + " with child size " + std::to_string(child_size));
}
Expand Down
65 changes: 61 additions & 4 deletions apps/idpv/btor_sweeping.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,15 +3,17 @@
#include <stdint.h>
#include <assert.h>
#include <stdlib.h>
#include <gmp.h>
#include "gmpxx.h"
using namespace smt;
using namespace std;

//----------------CONFIG--------------
//------------------------------------
// #define BTOR_USE_GMP 1

#ifdef BTOR_USE_GMP
#include <gmp.h>
#include "gmpxx.h"
#endif



#define BTOR_BV_TYPE uint32_t
#define BTOR_BV_TYPE_BW (sizeof (BTOR_BV_TYPE) * 8)
Expand Down Expand Up @@ -704,4 +706,59 @@ BtorBitVector *btor_bv_slice (
assert (rem_bits_zero_dbg (res));
#endif
return res;
}

void array_op_partition(smt::PrimOp o, const smt::Term &term, smt::TermVec &out) {
smt::TermVec to_visit({ term });
smt::UnorderedTermSet visited;

smt::Term t;
while (to_visit.size()) {
t = to_visit.back();
to_visit.pop_back();

if(visited.find(t) == visited.end()) {
visited.insert(t);

smt::Op op = t->get_op();
cout << "op : " << op << endl;
if(op.prim_op == o) {
for(auto tt : t) {
to_visit.push_back(tt);
}
} else {
out.push_back(t);
}
}
}
}

void array_conjunctive_partition(const smt::Term &term,
smt::TermVec &out,
bool include_bvand,
std::unordered_map<Term, Term> array_map) {
if (!include_bvand){
array_op_partition(smt::PrimOp::Store, term, out);
}
else {
TermVec tmp;
array_op_partition(smt::PrimOp::BVAnd, term, tmp);
cout << "tmp size " << tmp.size() << endl;

smt::Sort sort;
for(auto tt : tmp) {
sort = tt->get_sort();
if(sort->get_sort_kind() == SortKind::BV && sort->get_width() == 1) {
cout << "BV found: " << tt->to_string() << endl;
array_op_partition(smt::PrimOp::BVAnd, tt, out);
}
else if (sort->get_sort_kind() == SortKind::ARRAY) {
cout << "Array found:" << tt->to_string() << endl;
array_op_partition(smt::PrimOp::Store, tt, out);
}
else {
out.push_back(tt);
}
}
}
}

0 comments on commit b31b679

Please sign in to comment.