Fix exporting abstract states as linear constraint systems

Three related defects, all reachable from any domain built as
array_adaptive(flat_boolean_numerical(...)).

1. flat_boolean_numerical_domain::to_disjunctive_linear_constraint_system
   added its two components to a disjunctive system with operator+=, which is
   *disjunction* ("c1 or ... or cn += d ==> c1 or ... or cn or d"). A product
   denotes the conjunction of its components, so this returned a much weaker
   system than the state it was exporting -- and terminated the process with
   "cannot add true" whenever a component was top, which is the common case
   since most program points carry no boolean information. The boolean
   component is a conjunction, so it is now distributed into each disjunct of
   the numerical component. The sibling to_linear_constraint_system was
   already correct; only the disjunctive version was wrong.

2. flat_boolean_domain::to_linear_constraint_system returned a system
   *containing a tautology* for top, whereas the convention elsewhere (e.g.
   split_dbm) is that top is the empty system and only bottom is represented
   by a constraint. Consumers therefore never recognized it as top, and
   conjoining it contributed a redundant `true`.

3. array_adaptive and array_smashing range-iterated the base domain's
   disjunctive system without checking for bottom, and begin() raises an error
   on a bottom system. This was unreachable only while (1) never reported
   bottom. powerset_domain and value_partitioning_domain already guarded it.

tests/domains/unittests-lincst-export.cc covers all three. Against the
unfixed code the suite reports two assertion failures and then dies with
"cannot add true".

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: caballa

include/crab/domains/array_adaptive.hpp

@@ -2980,6 +2980,11 @@ class array_adaptive_domain final
   to_disjunctive_linear_constraint_system() const override {
     disjunctive_linear_constraint_system_t res;
     auto disj_csts = m_base_dom.to_disjunctive_linear_constraint_system();
+    if (disj_csts.is_false()) {
+      // begin() raises an error on a bottom system, so bottom must be
+      // propagated rather than iterated.
+      return disjunctive_linear_constraint_system_t(true /*is_false*/);
+    }
     for (auto &csts : disj_csts) {
       auto filtered_csts = filter_nonscalar_vars(std::move(csts));
       if (!filtered_csts.is_true()) {

include/crab/domains/array_smashing.hpp

@@ -724,6 +724,11 @@ class array_smashing final
     disjunctive_linear_constraint_system_t res;
 
     auto disj_csts = m_base_dom.to_disjunctive_linear_constraint_system();
+    if (disj_csts.is_false()) {
+      // begin() raises an error on a bottom system, so bottom must be
+      // propagated rather than iterated.
+      return disjunctive_linear_constraint_system_t(true /*is_false*/);
+    }
     for (auto &csts : disj_csts) {
       auto filtered_csts = filter_ghost_vars(std::move(csts));
       if (!filtered_csts.is_true()) {

include/crab/domains/flat_boolean_domain.hpp

@@ -400,7 +400,11 @@ class flat_boolean_domain final
       return linear_constraint_t::get_false();
 
     if (is_top())
-      return linear_constraint_t::get_true();
+      // Top is the empty system: linear_constraint_system::is_true() is
+      // "no constraints". Returning a system holding a tautology instead would
+      // not be recognized as top by consumers, and would add a redundant `true`
+      // to any conjunction this is combined with.
+      return linear_constraint_system_t();
 
     linear_constraint_system_t res;
     for (auto kv : m_env) {
@@ -1751,9 +1755,42 @@ class flat_boolean_numerical_domain final
 
   disjunctive_linear_constraint_system_t
   to_disjunctive_linear_constraint_system() const override {
-    disjunctive_linear_constraint_system_t res;
-    res += m_product.first().to_disjunctive_linear_constraint_system();
-    res += m_product.second().to_disjunctive_linear_constraint_system();
+    // A product denotes the *conjunction* of its components, but operator+= on
+    // a disjunctive constraint system is disjunction (see its documentation:
+    // "c1 or ... or cn += d ==> c1 or ... or cn or d"). Adding each component
+    // in turn would therefore compute `bool_part OR num_part`, which is much
+    // weaker than the product, and is an outright error ("cannot add true")
+    // whenever a component is top.
+    //
+    // The boolean component is always a conjunction of constraints over 0/1
+    // variables, so the product is obtained by distributing those constraints
+    // into every disjunct of the numerical component.
+    linear_constraint_system_t bool_csts =
+        m_product.first().to_linear_constraint_system();
+    disjunctive_linear_constraint_system_t num_csts =
+        m_product.second().to_disjunctive_linear_constraint_system();
+
+    if (bool_csts.is_false() || num_csts.is_false()) {
+      return disjunctive_linear_constraint_system_t(true /*is_false*/);
+    }
+    if (num_csts.is_true()) {
+      // No numerical information: the product is just the boolean part.
+      if (bool_csts.is_true()) {
+        return disjunctive_linear_constraint_system_t(false /*is_false*/);
+      }
+      return disjunctive_linear_constraint_system_t(bool_csts);
+    }
+
+    disjunctive_linear_constraint_system_t res(true /*is_false*/);
+    for (const linear_constraint_system_t &disjunct : num_csts) {
+      linear_constraint_system_t conj(disjunct);
+      conj += bool_csts;
+      if (conj.is_true()) {
+        // A top disjunct makes the whole disjunction top.
+        return disjunctive_linear_constraint_system_t(false /*is_false*/);
+      }
+      res += conj;
+    }
     return res;
   }
 

tests/domains/unittests-lincst-export.cc

@@ -0,0 +1,254 @@
+// Unit tests for exporting abstract states as linear constraint systems,
+// organized as Boost.Test suites:
+//
+//   flat_bool_export     to_linear_constraint_system on the 3-valued boolean
+//                        domain: top is the empty system, bottom carries a
+//                        contradiction, known values become 0/1 equalities
+//   product_export       to_disjunctive_linear_constraint_system on
+//                        flat_boolean_numerical_domain: a product denotes the
+//                        *conjunction* of its components
+//   array_export         to_disjunctive_linear_constraint_system on the array
+//                        wrappers, which must propagate a bottom base domain
+//                        rather than iterating it
+//
+// The product and array suites are regression tests: exporting a state whose
+// boolean component was top used to terminate the process ("cannot add true"),
+// and a state with both boolean and numerical information used to be exported
+// as their disjunction instead of their conjunction.
+//
+// Nothing is printed to standard output: the whole Boost.Test log is routed
+// to stderr (tests/run_tests.sh diffs stdout against a golden file) and
+// ctest checks the exit code.
+#define BOOST_TEST_MODULE unittests_lincst_export
+#define BOOST_TEST_ALTERNATIVE_INIT_API
+#define BOOST_TEST_NO_MAIN
+#include <boost/test/included/unit_test.hpp>
+
+#include "../common.hpp"
+
+#include <crab/support/debug.hpp>
+
+#include <set>
+#include <string>
+#include <vector>
+
+using namespace crab::cfg_impl;
+using namespace crab::domain_impl;
+
+using flat_bool_domain_t =
+    crab::domains::flat_boolean_domain<ikos::z_number, varname_t>;
+using product_domain_t = z_bool_interval_domain_t;
+using z_lin_cst_sys_t = ikos::linear_constraint_system<ikos::z_number, varname_t>;
+using z_disj_lin_cst_sys_t =
+    ikos::disjunctive_linear_constraint_system<ikos::z_number, varname_t>;
+
+namespace {
+
+/** The constraints of a system, as strings, so they can be compared by set. */
+std::set<std::string> constraints_of(const z_lin_cst_sys_t &csts) {
+  std::set<std::string> res;
+  for (auto const &c : csts) {
+    crab::crab_string_os os;
+    os << c;
+    res.insert(os.str());
+  }
+  return res;
+}
+
+/** The disjuncts of a disjunctive system. Must not be called on bottom. */
+std::vector<std::set<std::string>>
+disjuncts_of(const z_disj_lin_cst_sys_t &dcsts) {
+  std::vector<std::set<std::string>> res;
+  for (auto const &csts : dcsts) {
+    res.push_back(constraints_of(csts));
+  }
+  return res;
+}
+
+} // namespace
+
+// ---------------------------------------------------------------------------
+BOOST_AUTO_TEST_SUITE(flat_bool_export)
+
+// Top is the empty system, matching the convention of the numerical domains
+// (e.g. split_dbm): is_true() is "no constraints". Returning a system that
+// *contains* a tautology instead would not be recognized as top, and would add
+// a redundant `true` to any conjunction it took part in.
+BOOST_AUTO_TEST_CASE(top_exports_the_empty_system) {
+  flat_bool_domain_t dom;
+  auto csts = dom.to_linear_constraint_system();
+  BOOST_CHECK_MESSAGE(csts.is_true(), "top must export as the empty system");
+  BOOST_CHECK_EQUAL(csts.size(), 0u);
+}
+
+// Bottom, by contrast, *is* represented by a constraint, so that is_false()
+// can detect it.
+BOOST_AUTO_TEST_CASE(bottom_exports_a_contradiction) {
+  flat_bool_domain_t dom;
+  dom.set_to_bottom();
+  auto csts = dom.to_linear_constraint_system();
+  BOOST_CHECK(csts.is_false());
+}
+
+BOOST_AUTO_TEST_CASE(known_booleans_export_as_zero_one_equalities) {
+  variable_factory_t vfac;
+  z_var b(vfac["b"], crab::BOOL_TYPE, 1);
+  z_var c(vfac["c"], crab::BOOL_TYPE, 1);
+
+  flat_bool_domain_t dom;
+  dom.assume_bool(b, false /*not negated*/); // b is true
+  dom.assume_bool(c, true /*negated*/);      // c is false
+
+  auto csts = constraints_of(dom.to_linear_constraint_system());
+  BOOST_CHECK_EQUAL(csts.count("b = 1"), 1u);
+  BOOST_CHECK_EQUAL(csts.count("c = 0"), 1u);
+}
+
+BOOST_AUTO_TEST_SUITE_END()
+
+// ---------------------------------------------------------------------------
+BOOST_AUTO_TEST_SUITE(product_export)
+
+BOOST_AUTO_TEST_CASE(top_exports_as_top) {
+  product_domain_t dom;
+  auto dcsts = dom.to_disjunctive_linear_constraint_system();
+  BOOST_CHECK(!dcsts.is_false());
+  BOOST_CHECK_MESSAGE(dcsts.is_true(), "a top product must export as top");
+}
+
+BOOST_AUTO_TEST_CASE(bottom_exports_as_bottom) {
+  product_domain_t dom;
+  dom.set_to_bottom();
+  auto dcsts = dom.to_disjunctive_linear_constraint_system();
+  BOOST_CHECK_MESSAGE(dcsts.is_false(),
+                      "a bottom product must export as bottom");
+}
+
+// Regression: with a top boolean component, exporting used to reach
+// `operator+=(true)` on a disjunctive system, which terminates the process.
+// Most program points have no boolean information, so this was the common case.
+BOOST_AUTO_TEST_CASE(numerical_only_survives_a_top_boolean_component) {
+  variable_factory_t vfac;
+  z_var y(vfac["y"], crab::INT_TYPE, 32);
+
+  product_domain_t dom;
+  dom += z_lin_cst_t(z_lin_exp_t(y) >= ikos::z_number(1));
+  dom += z_lin_cst_t(z_lin_exp_t(y) <= ikos::z_number(10));
+
+  auto dcsts = dom.to_disjunctive_linear_constraint_system();
+  BOOST_REQUIRE(!dcsts.is_false());
+  BOOST_CHECK_MESSAGE(!dcsts.is_true(),
+                      "numerical information must not be exported as top");
+
+  auto disjuncts = disjuncts_of(dcsts);
+  BOOST_REQUIRE_EQUAL(disjuncts.size(), 1u);
+  BOOST_CHECK_EQUAL(disjuncts[0].count("-y <= -1"), 1u);
+  BOOST_CHECK_EQUAL(disjuncts[0].count("y <= 10"), 1u);
+  // No stray tautology from the top boolean component.
+  BOOST_CHECK_EQUAL(disjuncts[0].count("true"), 0u);
+}
+
+BOOST_AUTO_TEST_CASE(boolean_only_is_exported) {
+  variable_factory_t vfac;
+  z_var b(vfac["b"], crab::BOOL_TYPE, 1);
+
+  product_domain_t dom;
+  dom.assume_bool(b, false /*not negated*/);
+
+  auto dcsts = dom.to_disjunctive_linear_constraint_system();
+  BOOST_REQUIRE(!dcsts.is_false());
+  BOOST_REQUIRE(!dcsts.is_true());
+  auto disjuncts = disjuncts_of(dcsts);
+  BOOST_REQUIRE_EQUAL(disjuncts.size(), 1u);
+  BOOST_CHECK_EQUAL(disjuncts[0].count("b = 1"), 1u);
+}
+
+// Regression, and the reason this file exists: a product denotes the
+// conjunction of its components. Adding each component to a disjunctive system
+// in turn computes their *disjunction* instead, which is far weaker -- here it
+// would yield `(b = 1) OR (1 <= y <= 10)` as two disjuncts rather than one
+// disjunct holding both facts.
+BOOST_AUTO_TEST_CASE(components_are_conjoined_not_disjoined) {
+  variable_factory_t vfac;
+  z_var b(vfac["b"], crab::BOOL_TYPE, 1);
+  z_var y(vfac["y"], crab::INT_TYPE, 32);
+
+  product_domain_t dom;
+  dom.assume_bool(b, false /*not negated*/);
+  dom += z_lin_cst_t(z_lin_exp_t(y) >= ikos::z_number(1));
+  dom += z_lin_cst_t(z_lin_exp_t(y) <= ikos::z_number(10));
+
+  auto dcsts = dom.to_disjunctive_linear_constraint_system();
+  BOOST_REQUIRE(!dcsts.is_false());
+  BOOST_REQUIRE(!dcsts.is_true());
+
+  auto disjuncts = disjuncts_of(dcsts);
+  BOOST_REQUIRE_MESSAGE(disjuncts.size() == 1u,
+                        "the two components must be conjoined into a single "
+                        "disjunct, not unioned into two");
+  BOOST_CHECK_EQUAL(disjuncts[0].count("b = 1"), 1u);
+  BOOST_CHECK_EQUAL(disjuncts[0].count("-y <= -1"), 1u);
+  BOOST_CHECK_EQUAL(disjuncts[0].count("y <= 10"), 1u);
+}
+
+BOOST_AUTO_TEST_SUITE_END()
+
+// ---------------------------------------------------------------------------
+BOOST_AUTO_TEST_SUITE(array_export)
+
+// Regression: the array wrappers range-iterate the base domain's disjunctive
+// system, and begin() raises an error on a bottom system. This was unreachable
+// only while the product never reported bottom.
+BOOST_AUTO_TEST_CASE(array_adaptive_propagates_bottom) {
+  z_aa_bool_int_t dom;
+  dom.set_to_bottom();
+  auto dcsts = dom.to_disjunctive_linear_constraint_system();
+  BOOST_CHECK(dcsts.is_false());
+}
+
+BOOST_AUTO_TEST_CASE(array_smashing_propagates_bottom) {
+  z_as_bool_num_t dom;
+  dom.set_to_bottom();
+  auto dcsts = dom.to_disjunctive_linear_constraint_system();
+  BOOST_CHECK(dcsts.is_false());
+}
+
+BOOST_AUTO_TEST_CASE(array_adaptive_exports_scalar_facts) {
+  variable_factory_t vfac;
+  z_var y(vfac["y"], crab::INT_TYPE, 32);
+
+  z_aa_bool_int_t dom;
+  dom += z_lin_cst_t(z_lin_exp_t(y) >= ikos::z_number(1));
+  dom += z_lin_cst_t(z_lin_exp_t(y) <= ikos::z_number(10));
+
+  auto dcsts = dom.to_disjunctive_linear_constraint_system();
+  BOOST_REQUIRE(!dcsts.is_false());
+  BOOST_REQUIRE(!dcsts.is_true());
+  auto disjuncts = disjuncts_of(dcsts);
+  BOOST_REQUIRE_EQUAL(disjuncts.size(), 1u);
+  BOOST_CHECK_EQUAL(disjuncts[0].count("-y <= -1"), 1u);
+  BOOST_CHECK_EQUAL(disjuncts[0].count("y <= 10"), 1u);
+}
+
+BOOST_AUTO_TEST_SUITE_END()
+
+// Keep stdout empty: the golden-output harness (tests/run_tests.sh) diffs
+// the standard output of every test binary, so the whole Boost.Test log is
+// routed to stderr.  ctest passes --disable-warnings, which Boost.Test would
+// reject, so it is translated into the crab flag it stands for.
+int main(int argc, char **argv) {
+  std::vector<char *> args;
+  for (int idx = 0; idx < argc; ++idx) {
+    if (std::string(argv[idx]) == "--disable-warnings") {
+      crab::CrabEnableWarningMsg(false);
+      continue;
+    }
+    args.push_back(argv[idx]);
+  }
+  char log_sink[] = "--log_sink=stderr";
+  char report_sink[] = "--report_sink=stderr";
+  args.push_back(log_sink);
+  args.push_back(report_sink);
+  return boost::unit_test::unit_test_main(
+      &init_unit_test, static_cast<int>(args.size()), args.data());
+}