From 11f6e8d3403b9315b5e1c8d4397517907eb274e5 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Fri, 27 Oct 2023 03:12:59 -0700 Subject: [PATCH] new decision_proceduret API This changes the API offered by decision_proceduret to solving under assumptions. Solving under assumptions has been popularised by MiniSat, and is a state-less alternative to context stacks. This change mimics the transition from check-sat to check-sat-assuming that SMT-LIB is undergoing. --- src/solvers/decision_procedure.cpp | 10 +++- src/solvers/decision_procedure.h | 21 +++++--- src/solvers/prop/prop_conv_solver.cpp | 14 +++++- src/solvers/prop/prop_conv_solver.h | 2 +- src/solvers/refinement/bv_refinement.h | 2 +- src/solvers/refinement/bv_refinement_loop.cpp | 2 +- src/solvers/smt2/smt2_conv.cpp | 12 ++++- src/solvers/smt2/smt2_conv.h | 2 +- src/solvers/smt2/smt2_dec.cpp | 2 +- src/solvers/smt2/smt2_dec.h | 2 +- .../smt2_incremental_decision_procedure.cpp | 3 +- .../smt2_incremental_decision_procedure.h | 2 +- src/solvers/strings/string_refinement.cpp | 9 ++-- src/solvers/strings/string_refinement.h | 4 +- unit/Makefile | 1 + unit/solvers/flattening/boolbv.cpp | 50 +++++++++++++++++++ .../string_refinement/string_refinement.cpp | 8 +-- 17 files changed, 118 insertions(+), 28 deletions(-) create mode 100644 unit/solvers/flattening/boolbv.cpp diff --git a/src/solvers/decision_procedure.cpp b/src/solvers/decision_procedure.cpp index 0b7bf603e4f8..c0cbacd1ea63 100644 --- a/src/solvers/decision_procedure.cpp +++ b/src/solvers/decision_procedure.cpp @@ -11,13 +11,21 @@ Author: Daniel Kroening, kroening@kroening.com #include "decision_procedure.h" +#include + decision_proceduret::~decision_proceduret() { } decision_proceduret::resultt decision_proceduret::operator()() { - return dec_solve(); + return dec_solve(nil_exprt()); +} + +decision_proceduret::resultt +decision_proceduret::operator()(const exprt &assumption) +{ + return dec_solve(assumption); } void decision_proceduret::set_to_true(const exprt &expr) diff --git a/src/solvers/decision_procedure.h b/src/solvers/decision_procedure.h index 3f8482393963..f80e7392b057 100644 --- a/src/solvers/decision_procedure.h +++ b/src/solvers/decision_procedure.h @@ -17,18 +17,19 @@ Author: Daniel Kroening, kroening@kroening.com class exprt; +/// An interface for a decision procedure for satisfiability problems. class decision_proceduret { public: /// For a Boolean expression \p expr, add the constraint 'expr' if \p value /// is `true`, otherwise add 'not expr' - virtual void set_to(const exprt &expr, bool value) = 0; + virtual void set_to(const exprt &, bool value) = 0; /// For a Boolean expression \p expr, add the constraint 'expr' - void set_to_true(const exprt &expr); + void set_to_true(const exprt &); /// For a Boolean expression \p expr, add the constraint 'not expr' - void set_to_false(const exprt &expr); + void set_to_false(const exprt &); /// Generate a handle, which is an expression that /// has the same value as the argument in any model @@ -37,7 +38,7 @@ class decision_proceduret /// \ref set_to. /// The returned expression may be the expression itself or a more compact /// but solver-specific representation. - virtual exprt handle(const exprt &expr) = 0; + virtual exprt handle(const exprt &) = 0; /// Result of running the decision procedure enum class resultt @@ -48,12 +49,18 @@ class decision_proceduret }; /// Run the decision procedure to solve the problem + /// This corresponds to SMT-LIB's check-sat. resultt operator()(); + /// Run the decision procedure to solve the problem under + /// the given assumption. + /// This corresponds to SMT-LIB's check-sat-assuming. + resultt operator()(const exprt &assumption); + /// Return \p expr with variables replaced by values from satisfying /// assignment if available. /// Return `nil` if not available - virtual exprt get(const exprt &expr) const = 0; + virtual exprt get(const exprt &) const = 0; /// Print satisfying assignment to \p out virtual void print_assignment(std::ostream &out) const = 0; @@ -67,8 +74,8 @@ class decision_proceduret virtual ~decision_proceduret(); protected: - /// Run the decision procedure to solve the problem - virtual resultt dec_solve() = 0; + /// Implementation of the decision procedure. + virtual resultt dec_solve(const exprt &assumption) = 0; }; /// Add Boolean constraint \p src to decision procedure \p dest diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp index 49021dc5e46c..088b17ffbf0d 100644 --- a/src/solvers/prop/prop_conv_solver.cpp +++ b/src/solvers/prop/prop_conv_solver.cpp @@ -439,7 +439,8 @@ void prop_conv_solvert::finish_eager_conversion() { } -decision_proceduret::resultt prop_conv_solvert::dec_solve() +decision_proceduret::resultt +prop_conv_solvert::dec_solve(const exprt &assumption) { // post-processing isn't incremental yet if(!post_processing_done) @@ -459,7 +460,16 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve() log.statistics() << "Solving with " << prop.solver_text() << messaget::eom; - switch(prop.prop_solve()) + if(assumption.is_nil()) + push(); + else + push({literal_exprt(convert(assumption))}); + + auto prop_result = prop.prop_solve(); + + pop(); + + switch(prop_result) { case propt::resultt::P_SATISFIABLE: return resultt::D_SATISFIABLE; diff --git a/src/solvers/prop/prop_conv_solver.h b/src/solvers/prop/prop_conv_solver.h index ba41bc912224..e8b755ceb91f 100644 --- a/src/solvers/prop/prop_conv_solver.h +++ b/src/solvers/prop/prop_conv_solver.h @@ -40,7 +40,7 @@ class prop_conv_solvert : public conflict_providert, virtual void finish_eager_conversion(); // overloading from decision_proceduret - decision_proceduret::resultt dec_solve() override; + decision_proceduret::resultt dec_solve(const exprt &) override; void print_assignment(std::ostream &out) const override; std::string decision_procedure_text() const override; exprt get(const exprt &expr) const override; diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index 0f9b35069183..c26bb556f41f 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -39,7 +39,7 @@ class bv_refinementt:public bv_pointerst explicit bv_refinementt(const infot &info); - decision_proceduret::resultt dec_solve() override; + decision_proceduret::resultt dec_solve(const exprt &) override; std::string decision_procedure_text() const override { diff --git a/src/solvers/refinement/bv_refinement_loop.cpp b/src/solvers/refinement/bv_refinement_loop.cpp index 6db58bf898b2..c7f8678297ed 100644 --- a/src/solvers/refinement/bv_refinement_loop.cpp +++ b/src/solvers/refinement/bv_refinement_loop.cpp @@ -21,7 +21,7 @@ bv_refinementt::bv_refinementt(const infot &info) PRECONDITION(prop.has_is_in_conflict()); } -decision_proceduret::resultt bv_refinementt::dec_solve() +decision_proceduret::resultt bv_refinementt::dec_solve(const exprt &assumption) { // do the usual post-processing log.status() << "BV-Refinement: post-processing" << messaget::eom; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index c9135b23741f..5b7ab53c4ea5 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -317,9 +317,17 @@ void smt2_convt::define_object_size( } } -decision_proceduret::resultt smt2_convt::dec_solve() +decision_proceduret::resultt smt2_convt::dec_solve(const exprt &assumption) { - write_footer(); + if(assumption.is_nil()) + write_footer(); + else + { + assumptions.push_back(literal_exprt(convert(assumption))); + write_footer(); + assumptions.pop_back(); + } + out.flush(); return decision_proceduret::resultt::D_ERROR; } diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h index 2a2e1f3b0980..9f83687f8be9 100644 --- a/src/solvers/smt2/smt2_conv.h +++ b/src/solvers/smt2/smt2_conv.h @@ -106,7 +106,7 @@ class smt2_convt : public stack_decision_proceduret std::size_t number_of_solver_calls = 0; - resultt dec_solve() override; + resultt dec_solve(const exprt &) override; void write_header(); /// Writes the end of the SMT file to the `smt_convt::out` stream. These parts diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp index ddfe31dfb974..55528f80ce77 100644 --- a/src/solvers/smt2/smt2_dec.cpp +++ b/src/solvers/smt2/smt2_dec.cpp @@ -33,7 +33,7 @@ std::string smt2_dect::decision_procedure_text() const // clang-format on } -decision_proceduret::resultt smt2_dect::dec_solve() +decision_proceduret::resultt smt2_dect::dec_solve(const exprt &assumption) { ++number_of_solver_calls; diff --git a/src/solvers/smt2/smt2_dec.h b/src/solvers/smt2/smt2_dec.h index dd9872ffc0ae..ddb499e27fa7 100644 --- a/src/solvers/smt2/smt2_dec.h +++ b/src/solvers/smt2/smt2_dec.h @@ -39,11 +39,11 @@ class smt2_dect : protected smt2_stringstreamt, public smt2_convt { } - resultt dec_solve() override; std::string decision_procedure_text() const override; protected: message_handlert &message_handler; + resultt dec_solve(const exprt &) override; /// Everything except the footer is cached, so that output files can be /// rewritten with varying footers. diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp index 6bc254fde8ce..b1f8ab4825d3 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp @@ -689,7 +689,8 @@ exprt smt2_incremental_decision_proceduret::lower(exprt expression) const return lowered; } -decision_proceduret::resultt smt2_incremental_decision_proceduret::dec_solve() +decision_proceduret::resultt +smt2_incremental_decision_proceduret::dec_solve(const exprt &assumption) { ++number_of_solver_calls; define_object_properties(); diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h index 01ad03ffea0a..4a9cb70274d0 100644 --- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h +++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h @@ -64,7 +64,7 @@ class smt2_incremental_decision_proceduret final protected: // Implementation of protected decision_proceduret member function. - resultt dec_solve() override; + resultt dec_solve(const exprt &) override; /// \brief Defines a function of array sort and asserts the element values /// from `array_exprt` or `array_of_exprt`. /// \details diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp index 155598dac6df..0eada2733090 100644 --- a/src/solvers/strings/string_refinement.cpp +++ b/src/solvers/strings/string_refinement.cpp @@ -603,7 +603,8 @@ output_equations(std::ostream &output, const std::vector &equations) /// \return `resultt::D_SATISFIABLE` if the constraints are satisfiable, /// `resultt::D_UNSATISFIABLE` if they are unsatisfiable, /// `resultt::D_ERROR` if the limit of iteration was reached. -decision_proceduret::resultt string_refinementt::dec_solve() +decision_proceduret::resultt +string_refinementt::dec_solve(const exprt &assumption) { #ifdef DEBUG log.debug() << "dec_solve: Initial set of equations" << messaget::eom; @@ -781,7 +782,8 @@ decision_proceduret::resultt string_refinementt::dec_solve() // Initial try without index set const auto get = [this](const exprt &expr) { return this->get(expr); }; dependencies.clean_cache(); - const decision_proceduret::resultt initial_result = supert::dec_solve(); + const decision_proceduret::resultt initial_result = + supert::dec_solve(nil_exprt()); if(initial_result == resultt::D_SATISFIABLE) { bool satisfied; @@ -822,7 +824,8 @@ decision_proceduret::resultt string_refinementt::dec_solve() while((loop_bound_--) > 0) { dependencies.clean_cache(); - const decision_proceduret::resultt refined_result = supert::dec_solve(); + const decision_proceduret::resultt refined_result = + supert::dec_solve(nil_exprt()); if(refined_result == resultt::D_SATISFIABLE) { diff --git a/src/solvers/strings/string_refinement.h b/src/solvers/strings/string_refinement.h index 613327d1920c..1af64802ea3c 100644 --- a/src/solvers/strings/string_refinement.h +++ b/src/solvers/strings/string_refinement.h @@ -84,7 +84,9 @@ class string_refinementt final : public bv_refinementt exprt get(const exprt &expr) const override; void set_to(const exprt &expr, bool value) override; - decision_proceduret::resultt dec_solve() override; + +protected: + decision_proceduret::resultt dec_solve(const exprt &) override; private: // Base class diff --git a/unit/Makefile b/unit/Makefile index 208c3bc3a362..eb1d2cb3f3f8 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -96,6 +96,7 @@ SRC += analyses/ai/ai.cpp \ path_strategies.cpp \ pointer-analysis/value_set.cpp \ solvers/bdd/miniBDD/miniBDD.cpp \ + solvers/flattening/boolbv.cpp \ solvers/floatbv/float_utils.cpp \ solvers/prop/bdd_expr.cpp \ solvers/sat/external_sat.cpp \ diff --git a/unit/solvers/flattening/boolbv.cpp b/unit/solvers/flattening/boolbv.cpp new file mode 100644 index 000000000000..a3ca65f32f5a --- /dev/null +++ b/unit/solvers/flattening/boolbv.cpp @@ -0,0 +1,50 @@ +/*******************************************************************\ + +Module: Unit tests for boolbvt + +Author: Daniel Kroening + +\*******************************************************************/ + +/// \file +/// Unit tests for boolbvt + +#include +#include +#include +#include +#include +#include + +#include +#include +#include + +SCENARIO("boolbvt", "[core][solvers][flattening][boolbvt]") +{ + console_message_handlert message_handler; + message_handler.set_verbosity(0); + + GIVEN("A satisfiable bit-vector formula f") + { + satcheckt satcheck(message_handler); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + boolbvt boolbv(ns, satcheck, message_handler); + + unsignedbv_typet u32(32); + boolbv << equal_exprt(symbol_exprt("x", u32), from_integer(10, u32)); + + THEN("is indeed satisfiable") + { + REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE); + } + THEN("is unsatisfiable under an inconsistent assumption") + { + auto assumption = + equal_exprt(symbol_exprt("x", u32), from_integer(11, u32)); + REQUIRE( + boolbv(assumption) == decision_proceduret::resultt::D_UNSATISFIABLE); + } + } +} diff --git a/unit/solvers/strings/string_refinement/string_refinement.cpp b/unit/solvers/strings/string_refinement/string_refinement.cpp index b1910e1a5c4a..d86abcec0e5c 100644 --- a/unit/solvers/strings/string_refinement/string_refinement.cpp +++ b/unit/solvers/strings/string_refinement/string_refinement.cpp @@ -100,7 +100,7 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]") solver.set_to( equal_exprt{return_length, from_integer(15, int_type)}, true); - auto result = solver.dec_solve(); + auto result = solver(); THEN("The formula is satisfiable") { REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE); @@ -136,7 +136,7 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]") "The formula is satisfiable and the model of the array should have" "length 10 and end with 'b'") { - auto result = solver.dec_solve(); + auto result = solver(); REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE); const exprt array_model = solver.get(array1); REQUIRE(can_cast_expr(array_model)); @@ -183,7 +183,7 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]") "The model for array1 has length 10 and contains 'c' at " " position 3 and b at position 9") { - auto result = solver.dec_solve(); + auto result = solver(); REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE); const exprt array_model = solver.get(array1); REQUIRE(can_cast_expr(array_model)); @@ -230,7 +230,7 @@ SCENARIO("string refinement", "[core][solvers][strings][string_refinement]") true); THEN("The model for array1 has length 10 and contains 'c' at position 9") { - auto result = solver.dec_solve(); + auto result = solver(); REQUIRE(result == decision_proceduret::resultt::D_SATISFIABLE); const exprt array_model = solver.get(array1); REQUIRE(can_cast_expr(array_model));