From 93651cf27e51059dc449e1dd2d74a01ef05d8e32 Mon Sep 17 00:00:00 2001 From: Aman Goel Date: Sun, 25 Aug 2024 19:28:01 +0000 Subject: [PATCH] Temp changes --- src/reach/avr_config.cpp | 14 +++++++------- src/reach/avr_config.h | 4 ++-- src/reach/avr_word_netlist.cpp | 20 ++++++++++++++++++++ src/reach/avr_word_netlist.h | 1 + src/reach/reach_bt.cpp | 8 ++++---- src/reach/reach_cegar.cpp | 4 ++-- src/reach/reach_core.h | 6 +++--- src/reach/reach_m5.cpp | 4 ++-- src/reach/reach_y2.cpp | 4 ++-- 9 files changed, 43 insertions(+), 22 deletions(-) diff --git a/src/reach/avr_config.cpp b/src/reach/avr_config.cpp index 53390b7..7823a0b 100644 --- a/src/reach/avr_config.cpp +++ b/src/reach/avr_config.cpp @@ -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; @@ -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) @@ -287,11 +287,11 @@ 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") @@ -299,7 +299,7 @@ void Config::set_abstraction(string& name) { << ((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":"") diff --git a/src/reach/avr_config.h b/src/reach/avr_config.h index 9bb4bae..270ab87 100644 --- a/src/reach/avr_config.h +++ b/src/reach/avr_config.h @@ -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" @@ -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; diff --git a/src/reach/avr_word_netlist.cpp b/src/reach/avr_word_netlist.cpp index 04c9586..49af034 100644 --- a/src/reach/avr_word_netlist.cpp +++ b/src/reach/avr_word_netlist.cpp @@ -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); diff --git a/src/reach/avr_word_netlist.h b/src/reach/avr_word_netlist.h index ac0f07c..0635596 100644 --- a/src/reach/avr_word_netlist.h +++ b/src/reach/avr_word_netlist.h @@ -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; diff --git a/src/reach/reach_bt.cpp b/src/reach/reach_bt.cpp index df98c5c..5220fb9 100644 --- a/src/reach/reach_bt.cpp +++ b/src/reach/reach_bt.cpp @@ -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) { @@ -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) { @@ -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) { diff --git a/src/reach/reach_cegar.cpp b/src/reach/reach_cegar.cpp index 8ca0ae4..eb2d0fa 100644 --- a/src/reach/reach_cegar.cpp +++ b/src/reach/reach_cegar.cpp @@ -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) @@ -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)) { diff --git a/src/reach/reach_core.h b/src/reach/reach_core.h index c3c398a..26462dc 100644 --- a/src/reach/reach_core.h +++ b/src/reach/reach_core.h @@ -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; @@ -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; diff --git a/src/reach/reach_m5.cpp b/src/reach/reach_m5.cpp index 42089f0..93054ba 100644 --- a/src/reach/reach_m5.cpp +++ b/src/reach/reach_m5.cpp @@ -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) { @@ -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) { diff --git a/src/reach/reach_y2.cpp b/src/reach/reach_y2.cpp index 6d15df5..7d20406 100644 --- a/src/reach/reach_y2.cpp +++ b/src/reach/reach_y2.cpp @@ -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) @@ -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)