From c113f41688b6b98a090b382a86dbcd39722720ee Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 31 Oct 2024 14:55:42 -0400 Subject: [PATCH] BMC: push negation into conjunction This pushes the negation into the conjunction of the property constraint for BMC. This yields a constraint that is a disjunction, which is CNF-friendly. --- src/ebmc/bmc.cpp | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp index 68f93133a..018423f28 100644 --- a/src/ebmc/bmc.cpp +++ b/src/ebmc/bmc.cpp @@ -17,6 +17,15 @@ Author: Daniel Kroening, dkr@amazon.com #include #include +static exprt::operandst vector_negation(const exprt::operandst &src) +{ + exprt::operandst result; + result.reserve(src.size()); + for(auto &expr : src) + result.push_back(not_exprt{expr}); + return result; +} + void bmc( std::size_t bound, bool convert_only, @@ -79,7 +88,11 @@ void bmc( for(const auto &property : properties.properties) { if(!property.is_disabled()) - solver.set_to_false(conjunction(property.timeframe_handles)); + { + // one of them must be false + solver.set_to_true( + disjunction(vector_negation((property.timeframe_handles)))); + } } // Call decision_proceduret::dec_solve to finish the conversion @@ -106,7 +119,9 @@ void bmc( message.status() << "Checking " << property.name << messaget::eom; - auto assumption = not_exprt{conjunction(property.timeframe_handles)}; + // one of them must be false + auto assumption = + disjunction(vector_negation(property.timeframe_handles)); decision_proceduret::resultt dec_result = solver(assumption);