diff --git a/src/trans-netlist/Makefile b/src/trans-netlist/Makefile index 6eb346c38..ea43689dc 100644 --- a/src/trans-netlist/Makefile +++ b/src/trans-netlist/Makefile @@ -9,6 +9,7 @@ SRC = aig.cpp \ ldg.cpp \ map_aigs.cpp \ netlist.cpp \ + netlist_boolbv.cpp \ smv_netlist.cpp \ trans_to_netlist.cpp \ trans_trace.cpp \ diff --git a/src/trans-netlist/instantiate_netlist.cpp b/src/trans-netlist/instantiate_netlist.cpp index 2543080f8..cfd3a832f 100644 --- a/src/trans-netlist/instantiate_netlist.cpp +++ b/src/trans-netlist/instantiate_netlist.cpp @@ -13,48 +13,15 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include #include +#include "netlist_boolbv.h" + #include #include -/*******************************************************************\ - - Class: instantiate_var_mapt - - Purpose: - -\*******************************************************************/ - -class instantiate_var_mapt:public boolbvt -{ -public: - instantiate_var_mapt(const namespacet &_ns, propt &solver, - message_handlert &message_handler, - const var_mapt &_var_map) - : boolbvt(_ns, solver, message_handler), var_map(_var_map) {} - - typedef boolbvt SUB; - - // overloading - using boolbvt::get_literal; - - virtual literalt convert_bool(const exprt &expr); - virtual literalt get_literal(const std::string &symbol, const unsigned bit); - virtual bvt convert_bitvector(const exprt &expr); - -protected: - // disable smart variable allocation, - // we already have literals for all variables - virtual bool boolbv_set_equality_to_true(const equal_exprt &expr) { return true; } - virtual bool set_equality_to_true(const equal_exprt &expr) { return true; } - - const var_mapt &var_map; -}; - /*******************************************************************\ Function: instantiate_constraint @@ -74,7 +41,7 @@ void instantiate_constraint( const namespacet &ns, message_handlert &message_handler) { - instantiate_var_mapt i(ns, solver, message_handler, var_map); + netlist_boolbvt i(ns, solver, message_handler, var_map); try { @@ -113,7 +80,7 @@ literalt instantiate_convert( const namespacet &ns, message_handlert &message_handler) { - instantiate_var_mapt i(ns, solver, message_handler, var_map); + netlist_boolbvt i(ns, solver, message_handler, var_map); try { @@ -153,7 +120,7 @@ void instantiate_convert( message_handlert &message_handler, bvt &bv) { - instantiate_var_mapt i(ns, solver, message_handler, var_map); + netlist_boolbvt i(ns, solver, message_handler, var_map); try { @@ -175,107 +142,6 @@ void instantiate_convert( /*******************************************************************\ -Function: instantiate_var_mapt::convert_bool - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -literalt instantiate_var_mapt::convert_bool(const exprt &expr) -{ - if(expr.id()==ID_symbol || expr.id()==ID_next_symbol) - { - bvt result=convert_bitvector(expr); - - if(result.size()!=1) - throw "expected one-bit result"; - - return result[0]; - } - else if(expr.id()==ID_sva_overlapped_implication) - { - // same as regular implication - auto &sva_overlapped_implication = to_sva_overlapped_implication_expr(expr); - return prop.limplies( - convert_bool(sva_overlapped_implication.lhs()), - convert_bool(sva_overlapped_implication.rhs())); - } - else if(expr.id() == ID_verilog_past) - { - throw ebmc_errort().with_location(expr.source_location()) - << "no support for $past when using AIG backends"; - } - - return SUB::convert_bool(expr); -} - -/*******************************************************************\ - -Function: instantiate_var_mapt::convert_bitvector - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -bvt instantiate_var_mapt::convert_bitvector(const exprt &expr) -{ - if(expr.id()==ID_symbol || expr.id()==ID_next_symbol) - { - bool next=(expr.id()==ID_next_symbol); - const irep_idt &identifier=expr.get(ID_identifier); - - std::size_t width=boolbv_width(expr.type()); - - if(width!=0) - { - bvt bv; - bv.resize(width); - - for(std::size_t i=0; i +#include + +/*******************************************************************\ + +Function: netlist_boolbvt::convert_bool + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +literalt netlist_boolbvt::convert_bool(const exprt &expr) +{ + if(expr.id() == ID_symbol || expr.id() == ID_next_symbol) + { + bvt result = convert_bitvector(expr); + + if(result.size() != 1) + throw "expected one-bit result"; + + return result[0]; + } + else if(expr.id() == ID_sva_overlapped_implication) + { + // same as regular implication + auto &sva_overlapped_implication = to_sva_overlapped_implication_expr(expr); + return prop.limplies( + convert_bool(sva_overlapped_implication.lhs()), + convert_bool(sva_overlapped_implication.rhs())); + } + else if(expr.id() == ID_verilog_past) + { + throw ebmc_errort().with_location(expr.source_location()) + << "no support for $past when using AIG backends"; + } + + return SUB::convert_bool(expr); +} + +/*******************************************************************\ + +Function: netlist_boolbvt::convert_bitvector + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bvt netlist_boolbvt::convert_bitvector(const exprt &expr) +{ + if(expr.id() == ID_symbol || expr.id() == ID_next_symbol) + { + bool next = (expr.id() == ID_next_symbol); + const irep_idt &identifier = expr.get(ID_identifier); + + std::size_t width = boolbv_width(expr.type()); + + if(width != 0) + { + bvt bv; + bv.resize(width); + + for(std::size_t i = 0; i < width; i++) + bv[i] = next ? var_map.get_next(identifier, i) + : var_map.get_current(identifier, i); + + return bv; + } + } + else if(expr.id() == ID_verilog_past) + { + throw ebmc_errort().with_location(expr.source_location()) + << "no support for $past when using AIG backends"; + } + + return SUB::convert_bitvector(expr); +} + +/*******************************************************************\ + +Function: netlist_boolbvt::get_literal + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +literalt +netlist_boolbvt::get_literal(const std::string &symbol, const unsigned bit) +{ + return var_map.get_current(symbol, bit); +} diff --git a/src/trans-netlist/netlist_boolbv.h b/src/trans-netlist/netlist_boolbv.h new file mode 100644 index 000000000..a6fd036e3 --- /dev/null +++ b/src/trans-netlist/netlist_boolbv.h @@ -0,0 +1,60 @@ +/*******************************************************************\ + +Module: boolbvt for Netlists + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_TRANS_NETLIST_NETLIST_BOOLBV_H +#define CPROVER_TRANS_NETLIST_NETLIST_BOOLBV_H + +#include + +#include "var_map.h" + +/*******************************************************************\ + + Class: netlist_boolbvt + + Purpose: + +\*******************************************************************/ + +class netlist_boolbvt : public boolbvt +{ +public: + netlist_boolbvt( + const namespacet &_ns, + propt &solver, + message_handlert &message_handler, + const var_mapt &_var_map) + : boolbvt(_ns, solver, message_handler), var_map(_var_map) + { + } + + typedef boolbvt SUB; + + // overloading + literalt convert_bool(const exprt &) override; + bvt convert_bitvector(const exprt &expr) override; + + using boolbvt::get_literal; + literalt get_literal(const std::string &symbol, const unsigned bit); + +protected: + // disable smart variable allocation, + // we already have literals for all variables + bool boolbv_set_equality_to_true(const equal_exprt &) override + { + return true; + } + bool set_equality_to_true(const equal_exprt &expr) override + { + return true; + } + + const var_mapt &var_map; +}; + +#endif // CPROVER_TRANS_NETLIST_NETLIST_BOOLBV_H