unit tests watcher side

FreeYourSoul · FreeYourSoul · commit bd69b7ab4990 · 2025-07-21T17:41:38.000+02:00
diff --git a/CMakeLists.txt b/CMakeLists.txt
@@ -36,10 +36,10 @@ set(nlohmann-json_IMPLICIT_CONVERSIONS OFF)
 
 add_subdirectory(fabko)
 
-if (IS_BUILT_FROM_SOURCE AND BUILD_TESTING)
-    message(STATUS "Tests will be built")
-    add_subdirectory(tests)
-endif ()
+#if (BUILD_TESTING)
+message(STATUS "Tests will be built")
+add_subdirectory(tests)
+#endif ()
 
 #
 # Installation
diff --git a/docs/cnf/README.md b/docs/cnf/README.md
@@ -1,6 +1,8 @@
 # CNF
 
-Those are CNF files representing probles that must be runneable from the CLI.
+https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html : link to benchmarks to be downloaded.
+
+Those are CNF files representing problems that must be runnable from the CLI.
 Those are used for testing purposes and validation of the SAT solver which is part of the fabko solution
 
 ## Simple Straightforward formula
diff --git a/docs/cnf/pigeon-hole.cnf b/docs/cnf/pigeon-hole.cnf
@@ -0,0 +1,85 @@
+p cnf 20 75
+
+c Each pigeon must be in at least one hole
+1 2 3 4         0
+5 6 7 8         0
+9 10 11 12      0
+13 14 15 16     0
+17 18 19 20     0
+
+c Each pigeon can be in at most one hole
+-1 -2     0
+-1 -3     0
+-1 -4     0
+-2 -3     0
+-2 -4     0
+-3 -4     0
+-5 -6     0
+-5 -7     0
+-5 -8     0
+-6 -7     0
+-6 -8     0
+-7 -8     0
+-9 -10    0
+-9 -11    0
+-9 -12    0
+-10 -11   0
+-10 -12   0
+-11 -12   0
+-13 -14   0
+-13 -15   0
+-13 -16   0
+-14 -15   0
+-14 -16   0
+-15 -16   0
+-17 -18   0
+-17 -19   0
+-17 -20   0
+-18 -19   0
+-18 -20   0
+-19 -20   0
+
+c No two pigeons in the same hole
+-1 -5    0
+-1 -9    0
+-1 -13   0
+-1 -17   0
+-5 -9    0
+-5 -13   0
+-5 -17   0
+-9 -13   0
+-9 -17   0
+-13 -17  0
+
+-2 -6    0
+-2 -10   0
+-2 -14   0
+-2 -18   0
+-6 -10   0
+-6 -14   0
+-6 -18   0
+-10 -14  0
+-10 -18  0
+-14 -18  0
+
+-3 -7    0
+-3 -11   0
+-3 -15   0
+-3 -19   0
+-7 -11   0
+-7 -15   0
+-7 -19   0
+-11 -15  0
+-11 -19  0
+-15 -19  0
+
+-4 -8    0
+-4 -12   0
+-4 -16   0
+-4 -20   0
+-8 -12   0
+-8 -16   0
+-8 -20   0
+-12 -16  0
+-12 -20  0
+-16 -20  0
diff --git a/fabko/compiler/backend/sat/solver.cpp b/fabko/compiler/backend/sat/solver.cpp
@@ -98,8 +98,8 @@ Model make_model_from_cnf_file(const std::filesystem::path& cnf_file) {
 
             std::istringstream iss(line);
             std::string p, cnf;
-            std::size_t num_variables;
-            std::size_t num_clauses;
+            int num_variables = 0;
+            int num_clauses   = 0;
 
             iss >> p >> cnf >> num_variables >> num_clauses;
             if (p != "p" || cnf != "cnf") {
@@ -143,10 +143,12 @@ std::vector<solver::result> solver::solve(std::int32_t expected) {
 
     for (auto i = 0; i < expected; ++i) {
         auto r = impl_details::solve_sat(context_, model_);
+
         if (!r.has_value()) {
             auto error = r.error();
             if (error == sat_error::unsatisfiable) {
-                log_error("SAT solver cannot find solution for mode : UNSATISFIABLE");
+                if (i == 0)
+                    log_info("SAT solver cannot find solution for mode : UNSATISFIABLE");
             } else {
                 log_error("SAT solver : an error occurred");
             }
diff --git a/fabko/compiler/backend/sat/solver.hh b/fabko/compiler/backend/sat/solver.hh
@@ -104,26 +104,36 @@ class Clause_Watcher {
      */
     explicit Clause_Watcher(const Vars_Soa& vs, const Clause& clause)
         : watchers_([&]() -> std::array<std::optional<Vars_Soa::struct_id>, 2> { //
-            using std::get;
             fabko_assert(!clause.get_literals().empty(), "Cannot make a clause watchers over an empty clause");
-            if (clause.get_literals().size() == 1) {
-                return {vs[clause.get_literals().front().second].struct_id(), std::nullopt};
-            }
+
             auto filtered = std::ranges::views::filter(
                                 clause.get_literals(), [&vs](const auto& lit_id_pair) { return get<soa_assignment>(vs[lit_id_pair.second]) == assignment::not_assigned; }) //
                           | std::views::transform([&vs](const auto& lit_id_pair) { return vs[lit_id_pair.second].struct_id(); });                                          //
 
             auto it = filtered.begin();
             if (it == filtered.end())
-                return {std::nullopt, std::nullopt}; // no watched literals, clause is satisfied
-            ++it;
-            if (it == filtered.end())
-                return {*it, std::nullopt};          // no watched literals, clause is satisfied
+                return {std::nullopt, std::nullopt};      // no watched literals, clause is satisfied
+            if (++it == filtered.end())
+                return {*filtered.begin(), std::nullopt}; // no watched literals, clause is satisfied
 
             return {std::make_optional(*filtered.begin()), std::make_optional(*it)};
         }()) {}
 
-    [[nodiscard]] std::size_t size() const { return (watchers_[0].has_value() ? 1 : 0) + watchers_[1].has_value() ? 1 : 0; }
+    [[nodiscard]] std::size_t size() const { return (watchers_[0].has_value() ? 1 : 0) + (watchers_[1].has_value() ? 1 : 0); }
+
+    /**
+     * @return variable ids that are currently under watch
+     */
+    [[nodiscard]] std::vector<Vars_Soa::struct_id> get_watched() const {
+        std::vector<Vars_Soa::struct_id> res;
+        if (watchers_[0].has_value()) {
+            res.push_back(watchers_[0].value());
+        }
+        if (watchers_[1].has_value()) {
+            res.push_back(watchers_[1].value());
+        }
+        return res;
+    }
 
   private:
     std::array<std::optional<Vars_Soa::struct_id>, 2> watchers_; //!< The watched literals (1 for unit clauses, 2 for other clauses)
diff --git a/fabko/compiler/backend/sat/solver_impl.cpp b/fabko/compiler/backend/sat/solver_impl.cpp
@@ -12,19 +12,16 @@
 
 #include <algorithm>
 #include <expected>
+#include <numeric>
 #include <optional>
 #include <ranges>
 
-#include "common/exception.hh"
 #include "common/logging.hh"
 #include "solver.hh"
 
 #include "solver_context.hh"
 
-#include <numeric>
-
-namespace fabko::compiler::sat {
-namespace impl_details {
+namespace fabko::compiler::sat::impl_details {
 
 namespace {
 constexpr std::string SECTION = "sat_solver"; //!< logging a section for the SAT solver
@@ -127,7 +124,7 @@ conflict_resolution_result resolve_conflict(Solver_Context& ctx, Clauses_Soa::so
             const auto& trail_assign_ctx = get<soa_assignment_ctx>(trail_node);
 
             if (!trail_assign_ctx.is_decision() && trail_assign_ctx.decision_level_ == ctx.current_decision_level_) {
-                if (std::ranges::any_of(current_level_vars, [trail_var](const auto& ss) { return get<soa_literal>(ss).value() == trail_var; })) {
+                if (std::ranges::any_of(current_level_vars, [trail_var](const auto& current_var) { return get<soa_literal>(current_var).value() == trail_var; })) {
                     break;
                 }
             }
@@ -155,15 +152,18 @@ conflict_resolution_result resolve_conflict(Solver_Context& ctx, Clauses_Soa::so
 
             // add literals from the propagation clause (except current trail literal)
             for (const auto [prop_lit, prop_varid] : propagation_vars) {
+                const auto prop_node        = ctx.vars_soa_[prop_varid];
+                const auto& prop_assign_ctx = get<soa_assignment_ctx>(prop_node);
+
                 if (prop_lit.value() == trail_lit.value()
                     || std::ranges::any_of(learned_clause, [&prop_lit](const auto& lit_map) { return prop_lit.value() == lit_map.first.value(); }))
                     continue;
 
                 learned_clause.emplace_back(prop_lit, prop_varid);
-                if (trail_assign_ctx.decision_level_ == ctx.current_decision_level_) {
-                    current_level_vars.push_back(ctx.vars_soa_[prop_varid]);
-                } else if (trail_assign_ctx.decision_level_ > backtrack_level) {
-                    backtrack_level = trail_assign_ctx.decision_level_;
+                if (prop_assign_ctx.decision_level_ == ctx.current_decision_level_) {
+                    current_level_vars.push_back(prop_node);
+                } else if (prop_assign_ctx.decision_level_ > backtrack_level) {
+                    backtrack_level = prop_assign_ctx.decision_level_;
                 }
             }
         }
@@ -305,7 +305,7 @@ bool make_decision(Solver_Context& ctx) {
     auto& [lit, assignment, assignment_context, meta] = s;
 
     assignment_context.decision_level_ = ctx.current_decision_level_;
-    assignment                         = assignment::on; // always set at on by default. Off will be set by propagation (@incomplete : really ?)
+    assignment                         = assignment::on;
 
     log_debug("make decision: level({}) :: {} -> {}", ctx.current_decision_level_, lit.value(), to_string(assignment));
     ctx.trail_.push_back((*var_highest_vsids).struct_id());
@@ -314,9 +314,6 @@ bool make_decision(Solver_Context& ctx) {
 }
 
 std::expected<solver::result, sat_error> solve_sat(Solver_Context& ctx, const Model& model) {
-    if (unit_propagation(ctx).has_value())
-        return std::unexpected(sat_error::unsatisfiable);
-
     solver::result solution;
     while (solution.literals.empty()) {
         if (ctx.conflict_count_since_last_restart_ >= ctx.config_.restart_threshold) {
@@ -330,12 +327,16 @@ std::expected<solver::result, sat_error> solve_sat(Solver_Context& ctx, const Mo
             ctx.config_.restart_threshold *= static_cast<int>(ctx.config_.restart_multiplier);
         }
 
-        const auto conflict = unit_propagation(ctx);
-        if (conflict.has_value()) {
+        if (const auto conflict = unit_propagation(ctx); conflict.has_value()) {
             ++ctx.conflict_count_since_last_restart_;
             ++ctx.statistics_.conflicts;
             const auto& [learned_clause, backtrack_level] = resolve_conflict(ctx, ctx.clauses_soa_[conflict.value()]);
 
+            if (ctx.current_decision_level_ == 0 && backtrack_level == 0) {
+                log_info("Conflict found on level 0, unsatisfiable");
+                return std::unexpected(sat_error::unsatisfiable);
+            }
+
             if (learned_clause.is_empty()) {
                 log_info("Conflict resolved into an empty clause, unsatisfiable");
                 return std::unexpected(sat_error::unsatisfiable);
@@ -367,5 +368,4 @@ std::expected<solver::result, sat_error> solve_sat(Solver_Context& ctx, const Mo
     return solution;
 }
 
-} // namespace impl_details
-} // namespace fabko::compiler::sat
+} // namespace fabko::compiler::sat::impl_details
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
@@ -7,33 +7,31 @@ find_package(Catch2 3 CONFIG REQUIRED)
 include(CTest)
 include(Catch)
 
+#
 # Test of the Agent
 #
+#add_executable(test_agent)
+#target_sources(test_agent
+#        PRIVATE
+#        ${CMAKE_CURRENT_SOURCE_DIR}/agent/test_acl.cpp
+#)
+#target_compile_features(test_agent PUBLIC cxx_std_26)
+#target_link_libraries(test_agent
+#        PRIVATE Catch2::Catch2WithMain fabko::agent)
 #
-add_executable(test_agent)
-target_sources(test_agent
-        PRIVATE
-        agent/test_acl.cpp
-)
-target_compile_features(test_agent PUBLIC cxx_std_26)
-target_link_libraries(test_agent
-        PRIVATE Catch2::Catch2WithMain fabko::agent)
-
-catch_discover_tests(test_agent)
+#catch_discover_tests(test_agent)
 
-
-# Test of the compiler
 #
-#add_executable(test_core)
-#target_sources(test_core
-#        PRIVATE
-#
-#)
-#target_compile_features(test_core PUBLIC cxx_std_26)
-#target_compile_features(test_core
-#        PRIVATE -DTEST_ASSETS_PATH="${CMAKE_CURRENT_SOURCE_DIR}/_assets")
-#target_link_libraries(test_core
-#        PRIVATE fabko::core Catch2::Catch2WithMain)
+# Test of the compiler
 #
-#catch_discover_tests(test_core)
+add_executable(test_compiler)
+target_sources(test_compiler
+        PRIVATE
+        ${CMAKE_CURRENT_SOURCE_DIR}/compiler/soa/watcher_testcase.cpp
+)
+target_compile_features(test_compiler PUBLIC cxx_std_26)
+target_link_libraries(test_compiler
+        PRIVATE fabko::compiler Catch2::Catch2WithMain)
+
+catch_discover_tests(test_compiler)
 
diff --git a/tests/compiler/soa/watcher_testcase.cpp b/tests/compiler/soa/watcher_testcase.cpp
