Skip to content

Commit

Permalink
Temp changes
Browse files Browse the repository at this point in the history
  • Loading branch information
@aman-goel
aman-goel committed Aug 25, 2024
1 parent e891d9b commit 93651cf
Show file tree
Hide file tree
Showing 9 changed files with 43 additions and 22 deletions.
14 changes: 7 additions & 7 deletions src/reach/avr_config.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ int Config::g_fineness = 0;
int Config::g_lazy_assume = 0;

bool Config::g_uf_unordered = false;
bool Config::g_uf_mult_only = false;
bool Config::g_uf_heavy_only = false;
bool Config::g_uf_no_bitwise = false;
bool Config::g_uf_no_sext = false;
bool Config::g_uf_no_shift = false;
Expand Down Expand Up @@ -249,8 +249,8 @@ void Config::set_abstraction(string& name) {
{
if (name.find(NAME_UF_UNORDERED) != string::npos)
g_uf_unordered = !g_uf_unordered;
if (name.find(NAME_UF_MULT_ONLY) != string::npos)
g_uf_mult_only = !g_uf_mult_only;
if (name.find(NAME_UF_HEAVY_ONLY) != string::npos)
g_uf_heavy_only = !g_uf_heavy_only;
if (name.find(NAME_UF_NO_BITWISE) != string::npos)
g_uf_no_bitwise = !g_uf_no_bitwise;
if (name.find(NAME_UF_NO_SEXT) != string::npos)
Expand Down Expand Up @@ -287,19 +287,19 @@ void Config::set_abstraction(string& name) {
}
}

if (g_uf_mult_only) {
if (g_uf_heavy_only) {
g_ab_interpret = true;
g_ab_interpret_limit = 0;
g_ab_interpret_excc = LEVEL_EXCC_ALL;
g_uf_unordered = true;
// g_ab_interpret_excc = LEVEL_EXCC_NONE;
// g_uf_unordered = false;
}

cerr << "\t(abstraction: " << (g_ab_interpret?"sa":"sa+uf")
<< (g_ab_interpret_limit == 0?"":to_string(g_ab_interpret_limit))
<< ((g_ab_interpret_excc != LEVEL_EXCC_DEFAULT)?"+ec"+to_string(g_ab_interpret_excc):"")
<< (g_fineness != FINENESS_DEFAULT?"+l"+to_string(g_fineness):"")
<< (g_uf_unordered?"+unordered":"")
<< (g_uf_mult_only?"+mult":"")
<< (g_uf_heavy_only?"+heavy":"")
<< (g_uf_no_bitwise?"+nobitwise":"")
<< (g_uf_no_sext?"+nosignex":"")
<< (g_uf_no_shift?"+noshift":"")
Expand Down
4 changes: 2 additions & 2 deletions src/reach/avr_config.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -176,7 +176,7 @@
#define NAME_EXCC "ec"

#define NAME_UF_UNORDERED "+unordered"
#define NAME_UF_MULT_ONLY "+mult"
#define NAME_UF_HEAVY_ONLY "+heavy"
#define NAME_UF_NO_BITWISE "+nobitwise"
#define NAME_UF_NO_SEXT "+nosignex"
#define NAME_UF_NO_SHIFT "+noshift"
Expand Down Expand Up @@ -264,7 +264,7 @@ class Config {
static int g_fineness;
static int g_lazy_assume;
static bool g_uf_unordered;
static bool g_uf_mult_only;
static bool g_uf_heavy_only;
static bool g_uf_no_bitwise;
static bool g_uf_no_sext;
static bool g_uf_no_shift;
Expand Down
20 changes: 20 additions & 0 deletions src/reach/avr_word_netlist.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1882,6 +1882,26 @@ bool OpInst::is_unordered_uf() {
}
#endif

bool OpInst::is_heavy_uf() {
bool result = false;
switch (m_op) {
case Mult:
case Div:
case SDiv:
case Rem:
case SRem:
case SMod:
// case ArrayConst:
// case ArraySelect:
case ArrayStore:
result = (get_size() > 4);
break;
default:
;
}
return result;
}

Inst* OpInst::create(OpType op, Inst* exp1, Inst* exp2, Inst* exp3, int o_size, bool to_simplify, Inst* wire, SORT sort) {
if (op == OpInst::LogNot) {
OpInst* opt = OpInst::as(exp1);
Expand Down
1 change: 1 addition & 0 deletions src/reach/avr_word_netlist.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2560,6 +2560,7 @@ class OpInst: public Inst {
int get_simple_version();
bool is_unordered_uf();
#endif
bool is_heavy_uf();

protected:
OpType m_op;
Expand Down
8 changes: 4 additions & 4 deletions src/reach/reach_bt.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1691,7 +1691,7 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) {

#ifdef INTERPRET_EX_CC
if (m_allow_ex_cc) {
if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
(m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) {
Inst* simplified = e->t_simple;
if (OpInst::as(e) && e != simplified) {
Expand Down Expand Up @@ -2323,11 +2323,11 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) {
InstL::const_iterator ve_it = ch->begin(), ve_it2 = ch->begin();
ve_it2++;
NumInst* num = NumInst::as(*ve_it2);
cout << "Rotate: " << *e << endl;
// cout << "Rotate: " << *e << endl;
if (num != 0)
{
int rotate_amount = num->get_mpz()->get_si() % e->get_size();
cout << "rotate_amount: " << rotate_amount << endl;
// cout << "rotate_amount: " << rotate_amount << endl;
if (rotate_amount != 0) {
if (o == OpInst::RotateL)
{
Expand Down Expand Up @@ -2682,7 +2682,7 @@ void bt_API::inst2yices(Inst*e, bool bvAllConstraints) {

#ifdef INTERPRET_EX_CC
if (m_allow_ex_cc) {
if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
(m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) {
Inst* simplified = e->t_simple;
if (e != simplified) {
Expand Down
4 changes: 2 additions & 2 deletions src/reach/reach_cegar.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ void Reach::retrieve_ab_sol(Solver* solver, Inst* e, InstS& relSig, InstS& relCo

#ifdef INTERPRET_EX_CC
if (solver->m_allow_ex_cc) {
if (Config::g_uf_mult_only || (_abstract_mapper->fetch_op(e) == Solver::TheoryMapper::EUF_OP) ||
if (Config::g_uf_heavy_only || (_abstract_mapper->fetch_op(e) == Solver::TheoryMapper::EUF_OP) ||
(_abstract_mapper->fetch_op(e->t_simple) == Solver::TheoryMapper::EUF_OP)) {
Inst* simplified = e->t_simple;
if (e != simplified)
Expand Down Expand Up @@ -170,7 +170,7 @@ void Reach::retrieve_cex_val(Inst* e, Solver*solver, bool abstract, bool init_vi
e->set_visit();

#ifdef INTERPRET_EX_CC
if (Config::g_uf_mult_only || solver->m_allow_ex_cc && abstract && evalSimple)
if (Config::g_uf_heavy_only || solver->m_allow_ex_cc && abstract && evalSimple)
{
if ((_abstract_mapper->fetch_op(e) == Solver::TheoryMapper::EUF_OP) ||
(_abstract_mapper->fetch_op(e->t_simple) == Solver::TheoryMapper::EUF_OP)) {
Expand Down
6 changes: 3 additions & 3 deletions src/reach/reach_core.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -683,10 +683,10 @@ class UFBV_Mapper: public Solver::TheoryMapper {
if (e) {
e = e->get_port();

if (Config::g_uf_mult_only) {
if (Config::g_uf_heavy_only) {
if (e->get_type() == Op) {
OpInst* op = OpInst::as(e);
if (op->get_op() == OpInst::Mult)
if (op->is_heavy_uf())
return Solver::TheoryMapper::EUF_OP;
}
return Solver::TheoryMapper::BV_OP;
Expand All @@ -709,7 +709,7 @@ class UFBV_Mapper: public Solver::TheoryMapper {
return Solver::TheoryMapper::EUF_OP;
}
virtual Solver::TheoryMapper::VarType fetch_var(Inst*e) {
if (Config::g_uf_mult_only)
if (Config::g_uf_heavy_only)
return Solver::TheoryMapper::BV_VAR;
else if (Config::g_ab_interpret_excc >= LEVEL_EXCC_ALL)
return Solver::TheoryMapper::BV_VAR;
Expand Down
4 changes: 2 additions & 2 deletions src/reach/reach_m5.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2416,7 +2416,7 @@ void m5_API::inst2yices(Inst*e, bool bvAllConstraints) {

#ifdef INTERPRET_EX_CC
if (m_allow_ex_cc) {
if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
(m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) {
Inst* simplified = e->t_simple;
if (OpInst::as(e) && e != simplified) {
Expand Down Expand Up @@ -3508,7 +3508,7 @@ void m5_API::inst2yices(Inst*e, bool bvAllConstraints) {

#ifdef INTERPRET_EX_CC
if (m_allow_ex_cc) {
if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
(m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) {
Inst* simplified = e->t_simple;
if (e != simplified) {
Expand Down
4 changes: 2 additions & 2 deletions src/reach/reach_y2.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6191,7 +6191,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints)
#ifdef INTERPRET_EX_CC
if (m_allow_ex_cc)
{
if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
(m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) {
Inst* simplified = e->t_simple;
if (OpInst::as(e) && e != simplified)
Expand Down Expand Up @@ -7820,7 +7820,7 @@ void y2_API::inst2yices(Inst*e, bool bvAllConstraints)
#ifdef INTERPRET_EX_CC
if (m_allow_ex_cc)
{
if (Config::g_uf_mult_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
if (Config::g_uf_heavy_only || (m_mapper->fetch_op(e) == TheoryMapper::EUF_OP) ||
(m_mapper->fetch_op(e->t_simple) == TheoryMapper::EUF_OP)) {
Inst* simplified = e->t_simple;
if (e != simplified)
Expand Down

0 comments on commit 93651cf

Please sign in to comment.