diff --git a/regression/cbmc/hex_trace/test.desc b/regression/cbmc/hex_trace/test.desc
index 45811a0756c..b3ff75981ab 100644
--- a/regression/cbmc/hex_trace/test.desc
+++ b/regression/cbmc/hex_trace/test.desc
@@ -4,7 +4,6 @@ main.c
^EXIT=10$
^SIGNAL=0$
a=0 \s*\(0x0\)
-b=0ul? \s*\(0x0\)
a=-100 \s*\(0xFFFFFF9C\)
a=2147483647 \s*\(0x7FFFFFFF\)
b=4294967294ul? \s*\(0xFFFFFFFE\)
diff --git a/src/solvers/decision_procedure.cpp b/src/solvers/decision_procedure.cpp
index 0b7bf603e4f..c0cbacd1ea6 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 <util/std_expr.h>
+
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 3f848239396..f80e7392b05 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 7ca6632f1f5..804ed91ce6d 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(assumption_stack))
+ if(assumption.is_nil())
+ push();
+ else
+ push({literal_exprt(convert(assumption))});
+
+ auto prop_result = prop.prop_solve(assumption_stack);
+
+ 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 a32ce943188..f8bcb40fda1 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 0f9b3506918..c26bb556f41 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 9d193280855..da418cf0329 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 c9135b23741..5b7ab53c4ea 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 2a2e1f3b098..9f83687f8be 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 ddfe31dfb97..55528f80ce7 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 dd9872ffc0a..ddb499e27fa 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 df00c264c93..bc78dfc171d 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -687,7 +687,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 911dae5491a..4bd6b21eba8 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.h
@@ -67,7 +67,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 45cd53fffba..d9e682ae64c 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<exprt> &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 613327d1920..1af64802ea3 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 af2afbb0207..1b1b5af3878 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 00000000000..a3ca65f32f5
--- /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 <util/arith_tools.h>
+#include <util/bitvector_types.h>
+#include <util/cout_message.h>
+#include <util/namespace.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+#include <solvers/flattening/boolbv.h>
+#include <solvers/sat/satcheck.h>
+#include <testing-utils/use_catch.h>
+
+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/flattening/module_dependencies.txt b/unit/solvers/flattening/module_dependencies.txt
new file mode 100644
index 00000000000..7de7a55e4cc
--- /dev/null
+++ b/unit/solvers/flattening/module_dependencies.txt
@@ -0,0 +1,4 @@
+solvers/flattening
+solvers/sat
+testing-utils
+util
diff --git a/unit/solvers/strings/string_refinement/string_refinement.cpp b/unit/solvers/strings/string_refinement/string_refinement.cpp
index b1910e1a5c4..d86abcec0e5 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_exprt>(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_exprt>(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_exprt>(array_model));