From 8157016daa172d6de22d53067617f3177fa10ebd Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 29 Aug 2024 08:52:00 -0700 Subject: [PATCH] move bdd engine invocation into property_checker(...) This moves the invocation of the BDD engine into the property_checker(...) function. --- src/ebmc/bdd_engine.cpp | 39 +++++++++++++++------------------ src/ebmc/bdd_engine.h | 10 +++++++-- src/ebmc/ebmc_parse_options.cpp | 4 ---- src/ebmc/property_checker.cpp | 7 +++++- 4 files changed, 32 insertions(+), 28 deletions(-) diff --git a/src/ebmc/bdd_engine.cpp b/src/ebmc/bdd_engine.cpp index df2f9bea1..ddf1c2c42 100644 --- a/src/ebmc/bdd_engine.cpp +++ b/src/ebmc/bdd_engine.cpp @@ -10,8 +10,6 @@ Author: Daniel Kroening, daniel.kroening@inf.ethz.ch #include -#include -#include #include #include #include @@ -42,19 +40,27 @@ class bdd_enginet public: bdd_enginet( const cmdlinet &_cmdline, - ui_message_handlert &_ui_message_handler) - : cmdline(_cmdline), message(_ui_message_handler) + transition_systemt &_transition_system, + ebmc_propertiest &_properties, + message_handlert &_message_handler) + : cmdline(_cmdline), + transition_system(_transition_system), + properties(_properties), + message(_message_handler), + ns(transition_system.symbol_table) { } int operator()(); protected: + using propertiest = ebmc_propertiest; using propertyt = ebmc_propertiest::propertyt; const cmdlinet &cmdline; + transition_systemt &transition_system; + propertiest &properties; messaget message; - transition_systemt transition_system; - ebmc_propertiest properties; + const namespacet ns; netlistt netlist; // the Manager must appear before any BDDs @@ -171,12 +177,6 @@ int bdd_enginet::operator()() { try { - transition_system = - get_transition_system(cmdline, message.get_message_handler()); - - properties = ebmc_propertiest::from_command_line( - cmdline, transition_system, message.get_message_handler()); - const auto property_map = properties.make_property_map(); message.status() << "Building netlist" << messaget::eom; @@ -229,7 +229,6 @@ int bdd_enginet::operator()() for(propertyt &p : properties.properties) check_property(p); - const namespacet ns(transition_system.symbol_table); report_results(cmdline, properties, ns, message.get_message_handler()); return properties.exit_code(); } @@ -429,8 +428,6 @@ void bdd_enginet::compute_counterexample( throw "unexpected result from SAT solver"; } - const namespacet ns(transition_system.symbol_table); - property.witness_trace = compute_trans_trace(property.timeframe_literals, bmc_map, solver, ns); } @@ -901,8 +898,6 @@ void bdd_enginet::get_atomic_propositions(const exprt &expr) aig_prop_constraintt aig_prop(netlist, message.get_message_handler()); - const namespacet ns(transition_system.symbol_table); - literalt l = instantiate_convert( aig_prop, netlist.var_map, expr, ns, message.get_message_handler()); @@ -997,7 +992,7 @@ void bdd_enginet::build_BDDs() /*******************************************************************\ -Function: do_bdd +Function: bdd_engine Inputs: @@ -1007,10 +1002,12 @@ Function: do_bdd \*******************************************************************/ -int do_bdd( +int bdd_engine( const cmdlinet &cmdline, - ui_message_handlert &ui_message_handler) + transition_systemt &transition_system, + ebmc_propertiest &properties, + message_handlert &message_handler) { - return bdd_enginet(cmdline, ui_message_handler)(); + return bdd_enginet{cmdline, transition_system, properties, message_handler}(); } diff --git a/src/ebmc/bdd_engine.h b/src/ebmc/bdd_engine.h index 217f4a087..d333a1e7d 100644 --- a/src/ebmc/bdd_engine.h +++ b/src/ebmc/bdd_engine.h @@ -10,8 +10,14 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_EBMC_BDD_ENGINE_H #include -#include +#include -int do_bdd(const cmdlinet &, ui_message_handlert &); +#include "ebmc_properties.h" + +int bdd_engine( + const cmdlinet &, + transition_systemt &, + ebmc_propertiest &, + message_handlert &); #endif diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 79c7dddba..24f2558e4 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include "bdd_engine.h" #include "diatest.h" #include "ebmc_base.h" #include "ebmc_error.h" @@ -170,9 +169,6 @@ int ebmc_parse_optionst::doit() if(cmdline.isset("ranking-function")) return do_ranking_function(cmdline, ui_message_handler); - if(cmdline.isset("bdd") || cmdline.isset("show-bdds")) - return do_bdd(cmdline, ui_message_handler); - if(cmdline.isset("interpolation-word")) { throw ebmc_errort() << "This option is currently disabled"; diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp index d4fc20505..0bcc9c6cd 100644 --- a/src/ebmc/property_checker.cpp +++ b/src/ebmc/property_checker.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, dkr@amazon.com #include #include +#include "bdd_engine.h" #include "bmc.h" #include "dimacs_writer.h" #include "ebmc_error.h" @@ -378,7 +379,11 @@ int property_checker( ebmc_propertiest &properties, message_handlert &message_handler) { - if(cmdline.isset("aig") || cmdline.isset("dimacs")) + if(cmdline.isset("bdd") || cmdline.isset("show-bdds")) + { + return bdd_engine(cmdline, transition_system, properties, message_handler); + } + else if(cmdline.isset("aig") || cmdline.isset("dimacs")) { return bit_level_bmc( cmdline, transition_system, properties, message_handler);