Sat Reimplementation #18
Conversation
…at/reimplement
WalkthroughThis update transitions the build and dependency management system from vcpkg/CMake to a Nix-based approach, removing vcpkg-related files, submodules, and workflows. The SAT solver is reimplemented with new backend code, and the previous logic, SAT, and peerboard modules are removed. New CMake targets modularize the build. The CLI and logging infrastructure are refactored, and the test suite is trimmed to reflect these changes. Changes
Sequence Diagram(s)sequenceDiagram
participant User
participant CLI (fabko)
participant Logger
participant SAT CLI Command
participant SAT Model
participant SAT Solver
User->>CLI (fabko): Run with arguments
CLI (fabko)->>Logger: Initialize with log level/file
CLI (fabko)->>SAT CLI Command: Parse and execute command
SAT CLI Command->>Logger: Log execution start
SAT CLI Command->>SAT Model: Load CNF file(s)
SAT Model->>SAT Solver: Instantiate solver
SAT Solver->>SAT Solver: Solve SAT problem(s)
SAT Solver->>SAT CLI Command: Return result(s)
SAT CLI Command->>CLI (fabko): Complete execution
Poem
✨ Finishing Touches
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. 🪧 TipsChatThere are 3 ways to chat with CodeRabbit:
SupportNeed help? Create a ticket on our support page for assistance with any issues or questions. Note: Be mindful of the bot's finite context window. It's strongly recommended to break down tasks such as reading entire modules into smaller chunks. For a focused discussion, use review comments to chat about specific files and their changes, instead of using the PR comments. CodeRabbit Commands (Invoked using PR comments)
Other keywords and placeholders
CodeRabbit Configuration File (
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
There was a problem hiding this comment.
Actionable comments posted: 12
🔭 Outside diff range comments (5)
tests/agent/agent_wanted_interface.cpp (1)
135-142: Lambda signature breaksagentAPI – compilation fails
fabko::agentexpects a callback of the form
std::vector<acl::message>(std::optional<acl::message>),
but the lambda supplied here takes two parameters(fabko::agent&, …).
This will fail substitution of thestd::is_invocable_vrequirement and make the code uncompilable.- my_agent() : fabko::agent( - [](fabko::agent& a, std::optional<fabko::acl::message> input) - -> std::vector<fabko::acl::message> { - auto self = static_cast<my_agent&>(a); - return self.run_logic(input); - }) {} + my_agent() : fabko::agent( + [this](std::optional<fabko::acl::message> input) + -> std::vector<fabko::acl::message> { + return this->run_logic(std::move(input)); + }) {}fabko/agent/protocol/agent_com.hh (1)
48-60: Concept cannot be satisfied – method name mismatch breaks compilation.
c_communicateexpects an instance method namedpropositions(...), but bothp2p::agent_comandlocal::agent_comexposerequest_propositions(...). Any attempt to instantiate the concept with those classes will hard-fail at compile-time.-{ a.propositions(acl::message{}) } -> std::convertible_to<std::future<propositions>>; +{ a.request_propositions(acl::message{}) } -> std::convertible_to<std::future<propositions>>;or rename the concrete methods to
propositions.fabko/agent/protocol/acl.hh (2)
243-250:to_jsonlogic forstd::optionalis inverted – serialises values asnull.When
opt.has_value()is true we should serialise the contained value, notnullptr.- if (opt.has_value()) { - j = nullptr; - } else { - j = opt.value(); - } + if (opt.has_value()) { + j = opt.value(); + } else { + j = nullptr; + }
146-154:from_json(acc&)never fills optional fields.The current guard checks whether the destination already has a value, not whether the JSON contains the field.
- if (obj.reply_with.has_value()) { - obj.reply_with = serializer.at("reply_with").get<std::string>(); - } + if (serializer.contains("reply_with")) { + obj.reply_with = serializer.at("reply_with").get<std::string>(); + } - if (obj.reply_by.has_value()) { - obj.reply_by = serializer.at("reply_by").get<std::string>(); - } + if (serializer.contains("reply_by")) { + obj.reply_by = serializer.at("reply_by").get<std::string>(); + }fabko/agent/blackboard.cpp (1)
21-25:instantiate_black_boarddiscards the visitor result and returns uninitialised data.
std::visit’s return value is ignored anddatais returned without being set. Either capture the return value or forward the call.- std::visit( - overloaded{[&request](auto& b) -> std::string { return b.instantiate_blackboard(request); }}, bc); - return data; + data.blackboard_id = std::visit( + overloaded{[&request](auto& b) { return b.instantiate_blackboard(request); }}, bc); + return data;
🧹 Nitpick comments (17)
fabko/agent/agent.hh (1)
7-11: Typo in license header (“APGL” vs “AGPL”)The project consistently refers to the Affero GPL, yet this header still contains the variant “APGL”. Consider harmonising all headers while you are already touching them.
-// the APGL license is applying. +// the AGPL license applies.tests/agent/agent_wanted_interface.cpp (1)
6-11: Same “APGL”/“AGPL” typo as in other filesSee previous remark about keeping the licence acronym consistent.
tests/agent/test_acl.cpp (1)
7-11: Licence header acronym & contact addressMinor consistency issues:
- “APGL” should be “AGPL”.
- E-mail reads
pronmail.com– likely meantprotonmail.com.Purely cosmetic, but easy to fix while updating headers.
.clang-format (1)
4-90: Style-grid changes look reasonable – be aware of side effectsThe new configuration opts for:
ColumnLimit: 180– improves freedom but hurts diff readability in narrow review tools.BreakFunctionDefinitionParameters: falsetogether withBinPackParameters: BinPack– long function signatures may now overflow the (already wider) column limit.AlignAfterOpenBracket: DontAlign– stops vertical alignment; good for diff-friendliness.No blocker here, just ensure the whole tree is re-formatted once this lands to avoid mixed styles.
fabko/common/exception.hh (1)
7-11: Licence acronym typo (“APGL”)Consistent with other headers, update to “AGPL” for clarity.
VERSION (1)
1-1: Missing trailing newline.Many tooling and POSIX utilities expect text files to end with
\n.-0.1.0 +0.1.0 +fabko/fabko.hh (1)
15-15: Consider removing the empty namespace
namespace fabko {}is still an empty marker. If this header is intended only as a placeholder, consider deleting it or adding at least one meaningful declaration to avoid confusing include-guards that do nothing.fabko/common/logging.cpp (1)
36-36: Minor formatting deviationThe added space after the variable name (
sinks { … }) breaks the existing initializer-brace style used elsewhere (sinks{ … }). Consider reverting for consistency.fabko/compiler/backend/metadata.h (1)
18-18: Consider adding documentation for placeholder class.The
compiler_contextclass is currently empty. Consider adding a comment explaining its intended purpose or adding a TODO marker.-class compiler_context {}; +class compiler_context { + // TODO: Implement compiler context functionality +};fabko/fabko.cpp (1)
17-46: Consider extracting CLI configuration to separate function.The main function is becoming lengthy with the CLI configuration. Consider extracting the command definitions to improve readability.
+fil::sub_command create_test_command() { + return fil::sub_command { + "test", + []() { fmt::print("Command 1 executed\n"); }, + "Test command for verifying fabko functionality", + {}, + { + fil::option {"--option1", "-o1", + []() { fmt::print("Option 1 executed\n"); }, + "Enable verbose output"}, + fil::option {"--option2", "-o2", + []() { fmt::print("Option 2 executed\n"); }, + "Enable debug mode"}, + } + }; +} + int main(int argc, char** argv) { - fil::sub_command command_1 { ... }; + auto command_1 = create_test_command();fabko/compiler/backend/sat/solver_context.cpp (3)
23-23: Usestd::string_viewfor string literals.For compile-time string constants,
std::string_viewis more efficient thanstd::string.-constexpr std::string SECTION = "sat_solver"; //!< logging a section for the SAT solver +constexpr std::string_view SECTION = "sat_solver"; //!< logging a section for the SAT solver
25-32: Incomplete conflict resolution implementation.The
resolve_conflictfunction is stubbed and always returns an empty clause, which will cause the solver to incorrectly report unsatisfiability. The UIP (Unique Implication Point) finding logic needs to be implemented.Would you like me to help implement the conflict resolution algorithm or create an issue to track this TODO?
140-141: Remove redundant lambda capture.When capturing by reference with
&, thethispointer is already implicitly captured.- auto all_clause_ids = std::ranges::fold_right(model_clause, std::vector<var_soa::struct_id> {}, [&, this](const literal& l, auto res) { // + auto all_clause_ids = std::ranges::fold_right(model_clause, std::vector<var_soa::struct_id> {}, [&](const literal& l, auto res) { //fabko/compiler/backend/sat/solver_context.hh (1)
5-6: Consider using#pragma once.Modern C++ projects often prefer
#pragma onceover traditional header guards for simplicity.-#ifndef SOLVER_CONTEXT_HH -#define SOLVER_CONTEXT_HH +#pragma onceAnd remove the corresponding
#endifat the end of the file.fabko/compiler/backend/sat/solver.hh (3)
24-30: Remove redundant absolute value calculation.The constructor already stores the absolute value, so calling
std::abs()again in the getter is redundant.explicit literal(std::int64_t value) : value_(std::abs(value)) {} /** * @return literal value (absolute value that represent the variable) */ - [[nodiscard]] std::int64_t value() const { return std::abs(value_); } + [[nodiscard]] std::int64_t value() const { return value_; }
98-100: Consider making assignment_context members private with getters.Public data members violate encapsulation. Consider providing getter/setter methods instead.
+private: std::int64_t vsids_activity_ {}; std::size_t decision_level_ {}; std::optional<clause_view> clause_propagation_ {}; + +public: + [[nodiscard]] std::int64_t vsids_activity() const { return vsids_activity_; } + [[nodiscard]] std::size_t decision_level() const { return decision_level_; } + [[nodiscard]] const std::optional<clause_view>& clause_propagation() const { return clause_propagation_; }
112-112: Address TODO comment.The TODO indicates missing compiler information for clauses and literals.
Would you like me to help implement the compiler context integration or create an issue to track this TODO?
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
⛔ Files ignored due to path filters (1)
docs/icon_choco.svgis excluded by!**/*.svg
📒 Files selected for processing (68)
.clang-format(3 hunks).github/workflows/ci-linux.yml(1 hunks).github/workflows/ci-macosx.yml(0 hunks).github/workflows/ci-windows.yml(0 hunks).gitmodules(0 hunks).nix/default.nix(1 hunks).nix/fabko.nix(1 hunks).nix/import-from-json.nix(1 hunks).nix/nix-cmake.sh(1 hunks).nix/nix-dep.json(1 hunks).nix/nix-run.sh(1 hunks).nix/shell.nix(2 hunks)CMakeLists.txt(1 hunks)VERSION(1 hunks)default.nix(0 hunks)fabko/CMakeLists.txt(2 hunks)fabko/agent/CMakeLists.txt(1 hunks)fabko/agent/action.hh(1 hunks)fabko/agent/agent.cpp(3 hunks)fabko/agent/agent.hh(1 hunks)fabko/agent/blackboard.cpp(1 hunks)fabko/agent/blackboard.hh(1 hunks)fabko/agent/protocol/acl.hh(1 hunks)fabko/agent/protocol/agent_com.hh(1 hunks)fabko/agent/protocol/agent_com_local.cpp(2 hunks)fabko/agent/protocol/agent_com_p2p.cpp(1 hunks)fabko/agent/protocol/fap_request.hh(1 hunks)fabko/common/exception.hh(1 hunks)fabko/common/logging.cpp(2 hunks)fabko/common/logging.hh(6 hunks)fabko/common/ranges_to.hh(1 hunks)fabko/common/string_utils.hh(1 hunks)fabko/common/visitor_utils.hh(1 hunks)fabko/compiler/CMakeLists.txt(1 hunks)fabko/compiler/backend/metadata.h(1 hunks)fabko/compiler/backend/sat/solver.cpp(1 hunks)fabko/compiler/backend/sat/solver.hh(1 hunks)fabko/compiler/backend/sat/solver_context.cpp(1 hunks)fabko/compiler/backend/sat/solver_context.hh(1 hunks)fabko/core/logic/formula.cpp(0 hunks)fabko/core/logic/formula.hh(0 hunks)fabko/core/logic/sat/assignment_bitset.hh(0 hunks)fabko/core/logic/sat/clause.hh(0 hunks)fabko/core/logic/sat/dimacs_compiler.cpp(0 hunks)fabko/core/logic/sat/helpers.cpp(0 hunks)fabko/core/logic/sat/helpers.hh(0 hunks)fabko/core/logic/sat/solver.cpp(0 hunks)fabko/core/logic/sat/solver.hh(0 hunks)fabko/datastore/kv_rocksdb.cpp(5 hunks)fabko/datastore/kv_rocksdb.hh(2 hunks)fabko/fabko.cpp(1 hunks)fabko/fabko.hh(1 hunks)fabko/peerboard/peerboard.cpp(0 hunks)fabko/peerboard/peerboard.hh(0 hunks)fabko/version.hh(1 hunks)tests/CMakeLists.txt(2 hunks)tests/agent/agent_wanted_interface.cpp(1 hunks)tests/agent/test_acl.cpp(1 hunks)tests/core/common/test_algo_utils.cpp(0 hunks)tests/core/common/test_assignment_bitset.cpp(0 hunks)tests/core/sat/test_basic_sat.cpp(0 hunks)tests/core/sat/test_dimacs_compiler.cpp(0 hunks)tests/core/sat/test_formula.cpp(0 hunks)tests/core/sat/test_sat_coloring.cpp(0 hunks)tests/core/sat/test_set.cpp(0 hunks)tests/peerboard/test_kv_rocksdb.cpp(1 hunks)vcpkg(0 hunks)vcpkg.json(0 hunks)
💤 Files with no reviewable changes (24)
- .gitmodules
- default.nix
- vcpkg
- vcpkg.json
- fabko/core/logic/sat/helpers.cpp
- tests/core/sat/test_formula.cpp
- tests/core/common/test_assignment_bitset.cpp
- fabko/peerboard/peerboard.cpp
- fabko/core/logic/sat/helpers.hh
- tests/core/sat/test_dimacs_compiler.cpp
- tests/core/sat/test_sat_coloring.cpp
- tests/core/sat/test_set.cpp
- .github/workflows/ci-windows.yml
- tests/core/sat/test_basic_sat.cpp
- tests/core/common/test_algo_utils.cpp
- fabko/core/logic/sat/solver.hh
- .github/workflows/ci-macosx.yml
- fabko/peerboard/peerboard.hh
- fabko/core/logic/sat/clause.hh
- fabko/core/logic/formula.hh
- fabko/core/logic/sat/dimacs_compiler.cpp
- fabko/core/logic/sat/assignment_bitset.hh
- fabko/core/logic/sat/solver.cpp
- fabko/core/logic/formula.cpp
🧰 Additional context used
🪛 GitHub Actions: CI Linux Build
CMakeLists.txt
[error] 1-1: CMake Error: Imported target 'fys::fil' includes non-existent path '/build/1z21fyh4lww119rbb77clklhva7nbqs0-source/' in INTERFACE_INCLUDE_DIRECTORIES. Possible reasons: path deleted, renamed, or install/uninstall incomplete or faulty installation package.
fabko/CMakeLists.txt
[error] 1-1: CMake Error: Imported target 'fys::fil' includes non-existent path '/build/1z21fyh4lww119rbb77clklhva7nbqs0-source/' in INTERFACE_INCLUDE_DIRECTORIES. Possible reasons: path deleted, renamed, or install/uninstall incomplete or faulty installation package.
🪛 Shellcheck (0.10.0)
.nix/nix-cmake.sh
[warning] 4-4: cmakeFlags is referenced but not assigned.
(SC2154)
.nix/nix-run.sh
[error] 19-19: Couldn't parse this command expansion. Fix to allow more checks.
(SC1073)
[error] 23-23: Unexpected keyword/token. Fix any mentioned problems and try again.
(SC1072)
🔇 Additional comments (50)
fabko/version.hh (1)
7-7: License year update acknowledgedYear bump to 2025 keeps the header current. No further action required.
fabko/common/string_utils.hh (1)
7-7: License header refreshedConsistent 2025 update; nothing else touched.
fabko/common/visitor_utils.hh (1)
7-7: Header year bump looks goodAlignment with other files confirmed.
fabko/common/ranges_to.hh (1)
7-7: License year sync OKUpdate is correct; no code changes.
fabko/agent/protocol/agent_com_p2p.cpp (1)
7-7: License notice updatedYear range extended to 2025; change approved.
fabko/agent/protocol/agent_com.hh (1)
7-7: License year update looks good.
No additional action required.fabko/agent/action.hh (1)
7-7: License header updated correctly.
No functional code touched.fabko/agent/protocol/acl.hh (1)
7-7: License header update acknowledged.fabko/agent/blackboard.cpp (2)
7-7: License header updated – OK.
38-44: Stub implementations return default-constructed values – functional TODO.Both
request_propositionsandsubmit_decisioncurrently return placeholders; callers will misbehave.Add TODO or implement proper forwarding similar to
instantiate_black_board.fabko/agent/blackboard.hh (1)
7-7: License year bump looks goodHeader update only – no functional impact.
fabko/agent/protocol/fap_request.hh (1)
7-7: License header updated – OKPure metadata change; nothing else to review.
tests/peerboard/test_kv_rocksdb.cpp (1)
7-7: License year updatedNo code modifications in this test file.
fabko/fabko.hh (1)
7-7: License header year update approvedNo functional impact.
fabko/common/logging.cpp (1)
7-7: License header year change acknowledgedNo behavioral change.
.nix/nix-dep.json (1)
1-9: LGTM! Well-structured dependency metadata.The JSON structure correctly defines the "fil" dependency with proper GitHub metadata. The SHA256 hash format and repository information look valid.
CMakeLists.txt (2)
22-28: LGTM! Proper platform-specific library configuration.The uring library setup correctly targets Unix platforms excluding Apple, with appropriate interface properties.
20-20: #!/bin/bashList all CMakeLists.txt files in the repository
fd --hidden --ignore-case --type f CMakeLists.txt
Show root CMakeLists.txt around find_package(fil)
echo "---- Root CMakeLists.txt ----"
sed -n '1,200p' CMakeLists.txtShow fabko/CMakeLists.txt around target_link_libraries
echo "---- fabko/CMakeLists.txt ----"
sed -n '1,200p' fabko/CMakeLists.txt.nix/shell.nix (2)
13-13: LGTM! Ninja addition improves build performance.Adding ninja to the build environment will enable faster parallel builds.
22-22: LGTM! Maintains vcpkg compatibility during transition.Setting VCPKG_ROOT ensures compatibility with existing build scripts during the migration to Nix.
tests/CMakeLists.txt (2)
19-19: LGTM! Consistent with peerboard component removal.Removing the
fabko::peerboardlinkage aligns with the broader refactoring that removes the peerboard component from the codebase.
38-51: Clarify the status of the commented test_core target.The entire
test_coretarget is commented out, which suggests it's temporarily disabled during the refactoring. Consider whether this should be:
- Completely removed if the functionality is no longer needed
- Updated to reflect the new compiler architecture
- Left commented with a TODO explaining when it will be re-enabled
#!/bin/bash # Description: Check if there are any references to test_core or core tests # Expected: Understand if this is temporary or permanent removal # Search for test_core references rg -A 3 -B 3 "test_core" # Search for core test files that might have been removed fd -t f -e cpp -e hpp "test.*core" # Check for compiler test files fd -t f -e cpp -e hpp "test.*compiler"fabko/datastore/kv_rocksdb.cpp (2)
7-7: LGTM! License year update.Routine update of license year to 2022-2025.
39-39: LGTM! Improved code formatting.The reformatting of
fabko_assertcalls to single lines improves readability while maintaining the same functionality and error handling behavior.Also applies to: 57-59, 82-82, 102-102
fabko/agent/protocol/agent_com_local.cpp (5)
6-6: LGTM: License year updated appropriately.The license year extension to 2025 aligns with project maintenance.
11-11: LGTM: Include path reflects modularization.The updated include path
<agent/agent.hh>properly reflects the new modular directory structure mentioned in the PR objectives.
23-27: LGTM: Function formatting improvements.The reformatting to single-line function bodies improves readability while maintaining the same functionality.
29-30: LGTM: Constructor formatting improvement.The multi-line initializer list format improves readability and follows modern C++ style guidelines.
32-32: LGTM: Explicit namespace closing comment.Adding the explicit namespace closing comment improves code documentation and readability.
.nix/default.nix (1)
1-6: LGTM: Well-structured Nix expression.The Nix expression follows standard patterns with proper parameter handling and package exposure. This provides a clean entry point for the new Nix-based build system.
fabko/agent/agent.cpp (4)
7-7: LGTM: License year updated.License year extension to 2025 is appropriate.
16-16: LGTM: Include path reflects new structure.The updated include path
<agent/protocol/acl.hh>aligns with the modular restructuring.
32-38: LGTM: Minor formatting improvements.The spacing and single-line function formatting improve code readability.
41-44: Verify the commented out agent callback logic.The agent callback functionality has been disabled by commenting out the code. This could indicate incomplete refactoring or temporary changes during development.
Please confirm if this is intentional for the current implementation phase or if this functionality should be restored.
#!/bin/bash # Description: Search for any remaining references to _callback_on_action or related callback patterns # Expected: Find other usages or related callback implementations to understand the intended state echo "Searching for callback references..." rg -A 3 -B 3 "_callback_on_action|callback.*action" --type cpp echo "Searching for agent execute patterns..." rg -A 5 -B 2 "agent.*execute|execute.*agent" --type cpp.nix/nix-cmake.sh (1)
1-6: LGTM: Well-implemented cmake wrapper for Nix environment.The script correctly:
- Uses POSIX-compliant shell syntax
- Conditionally applies
cmakeFlagsonly when not using--build- Properly delegates to the
nix-run.shwrapperThe static analysis warning about
cmakeFlagsis a false positive - this variable is provided by the Nix environment, not assigned within the script.fabko/compiler/CMakeLists.txt (4)
1-10: LGTM: Well-organized CMake target structure.The compiler library target is properly structured with appropriate public/private source organization for the SAT solver backend.
11-19: LGTM: Appropriate dependencies and configuration.The RocksDB include directory and library dependencies (fabko::common, nlohmann_json) are appropriate for a compiler backend implementation.
20-20: LGTM: Proper alias creation.The
fabko::compileralias follows CMake best practices for namespaced targets.
15-15: Verify C++26 standard support.C++26 is very recent and may not be supported by all compilers yet. Ensure your target environments support this standard.
What is the current status of C++26 standard support in major compilers like GCC, Clang, and MSVC?fabko/agent/CMakeLists.txt (1)
16-16: Verify include directory path.The include directory is set to
agentbut the target sources use${CMAKE_CURRENT_SOURCE_DIR}/prefixes. This may cause issues if headers try to include each other.#!/bin/bash # Description: Check if header files in the agent directory use relative includes that would be affected by the include directory setting # Search for include statements in agent header files fd -e hh -e hpp . fabko/agent --exec grep -l "#include.*/" {} \; # Check specific include patterns that might break with the current setup rg '#include.*agent/' fabko/agent/ -A 2 -B 2fabko/compiler/backend/metadata.h (1)
13-22: Verify removal of SAT solver interface doesn't break existing code.The transition from
fabko::satnamespace tofabko::compilerrepresents a significant architectural change. Ensure all references to the old SAT solver interface have been updated.#!/bin/bash # Description: Search for any remaining references to the old SAT solver interface # Search for references to the old fabko::sat namespace rg "fabko::sat" --type cpp --type c # Search for references to the removed from_dimacs function rg "from_dimacs" --type cpp --type c # Search for includes of the old solver.hh rg '#include.*solver\.hh' --type cpp --type c.nix/fabko.nix (1)
14-14: Verify VERSION file exists.The derivation reads the version from
../VERSIONfile. Ensure this file exists and contains a valid version string.#!/bin/bash # Description: Check if VERSION file exists and contains valid version # Check if VERSION file exists if [ -f "VERSION" ]; then echo "VERSION file exists" echo "Content: $(cat VERSION)" else echo "ERROR: VERSION file not found" fi # Validate version format (should be semantic versioning) if [ -f "VERSION" ]; then version=$(cat VERSION) if [[ $version =~ ^[0-9]+\.[0-9]+(\.[0-9]+)?(-[a-zA-Z0-9.-]+)?$ ]]; then echo "Version format is valid: $version" else echo "WARNING: Version format may not be standard: $version" fi fifabko/datastore/kv_rocksdb.hh (2)
7-7: LGTM: License year update.The license year update to 2022-2025 is appropriate and consistent with other files in the project.
32-108: LGTM: Formatting consistency improvements.The spacing and formatting changes improve code consistency and align with the updated
.clang-formatconfiguration. No functional changes were made to the API.fabko/compiler/backend/sat/solver.cpp (1)
20-22: Let’s search the entire repo for anysolve_satdefinitions to confirm it’s truly missing.#!/bin/bash # Look for any definitions or usages of solve_sat in the codebase rg "solve_sat" -n ..nix/import-from-json.nix (1)
11-11: Fix string interpolation in error message.The string interpolation syntax in the error message may not work as expected in Nix. Variable substitution in strings needs proper escaping.
- dependencySource = sources.${dependencyName} or (throw "Dependency ${dependencyName} not found in ${sourcesFile}"); + dependencySource = sources.${dependencyName} or (throw "Dependency ${dependencyName} not found in ${toString sourcesFile}");Likely an incorrect or invalid review comment.
.github/workflows/ci-linux.yml (1)
20-20: Verify the nixpkgs channel version.The channel
nixos-25.05may not be available yet or might be unstable. Consider using a stable channel.What is the latest stable NixOS channel version available as of June 2025?fabko/CMakeLists.txt (1)
6-27: LGTM on the library restructuring.The refactoring from
coretocommonand the modularization into separatecompilerandagentcomponents improves the architecture. The dependency simplification also aligns well with the migration strategy.fabko/common/logging.hh (1)
52-94: Excellent use of perfect forwarding!The change from by-value parameters to forwarding references (
Args&&...) improves efficiency by enabling perfect forwarding. Combined withstd::forward<Args>(packs)..., this ensures optimal parameter passing without unnecessary copies.fabko/compiler/backend/sat/solver_context.cpp (1)
69-74: Incorrect while loop condition using count_if result.
std::ranges::count_ifreturns a numeric count, not a boolean. The loop should check if the count is greater than zero.- while (auto propagated_literal = std::ranges::count_if(ctx.clauses_soa_, propagate)) { + while (std::ranges::count_if(ctx.clauses_soa_, propagate) > 0) { if (conflict.has_value()) { break; } - ctx.statistics_.propagations += propagated_literal; + ctx.statistics_.propagations += 1; }Likely an incorrect or invalid review comment.
There was a problem hiding this comment.
Actionable comments posted: 0
🧹 Nitpick comments (4)
README.md (4)
2-3: Add descriptive alt-text for the Tokei badgeThe image in line 3 has an empty alt attribute, which triggers MD045 and hampers accessibility. Provide meaningful alt-text (and optionally wrap the badge in a link for consistency with the other badges).
- +[](https://github.com/FreeYourSoul/Fabko)
12-18: Fix broken grammar & singular/plural mismatchesSeveral phrases read awkwardly and may confuse newcomers skimming the README. Tighten them up and correct the plural forms.
-Fabko is a library that some to make it easy to create agent that interoperates via customizable communication medium ( -peer-to-peer, centralised server based, distributed etc...). - -Those agent will be able to register their capability to an agent node called a "peerboard" node. +Fabko is a library that aims to make it easy to create agents that interoperate via customizable communication media +(peer-to-peer, centralized server-based, distributed, etc.). + +Those agents will be able to register their capabilities with a node called a “peerboard”.
21-24: Prefer “whether” and streamline the sentenceMinor polish for readability and formality.
-It is then possible to produce a request over this compiled graph to define if the agent can do an action or not. +You can then query this compiled graph to determine whether an agent can perform an action.
70-70: Capitalize and clarify the section heading-actor part of FABL +Actor section of FABL
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (7)
README.md(2 hunks)fabko/CMakeLists.txt(1 hunks)fabko/cli_base.hh(1 hunks)fabko/compiler/CMakeLists.txt(1 hunks)fabko/compiler/backend/sat/cli.hh(1 hunks)fabko/fabko.cpp(1 hunks)fabko/fabko.hh(0 hunks)
💤 Files with no reviewable changes (1)
- fabko/fabko.hh
✅ Files skipped from review due to trivial changes (2)
- fabko/compiler/backend/sat/cli.hh
- fabko/cli_base.hh
🚧 Files skipped from review as they are similar to previous changes (3)
- fabko/compiler/CMakeLists.txt
- fabko/fabko.cpp
- fabko/CMakeLists.txt
🧰 Additional context used
🪛 LanguageTool
README.md
[uncategorized] ~12-~12: Possible missing article found.
Context: ...ary that some to make it easy to create agent that interoperates via customizable com...
(AI_HYDRA_LEO_MISSING_AN)
[grammar] ~14-~14: The plural determiner ‘those’ does not agree with the singular noun ‘agent’.
Context: ...sed server based, distributed etc...). Those agent will be able to register their capabili...
(THIS_NNS)
[uncategorized] ~21-~21: Possible missing comma found.
Context: ...Board Language is the base of the FabKo library as it is a declarative language that ma...
(AI_HYDRA_LEO_MISSING_COMMA)
[style] ~25-~25: In contexts where ‘if’ is followed by ‘or’, using ‘whether’ may be more appropriate (and formal).
Context: ...uest over this compiled graph to define if the agent can do an action or not. The ...
(IF_WHETHER)
🪛 markdownlint-cli2 (0.17.2)
README.md
3-3: Images should have alternate text (alt text)
null
(MD045, no-alt-text)
⏰ Context from checks skipped due to timeout of 90000ms (1)
- GitHub Check: Codacy Static Code Analysis
There was a problem hiding this comment.
Actionable comments posted: 0
♻️ Duplicate comments (1)
.nix/fabko.nix (1)
69-69: Fix license specification syntax error.The license specification has a syntax error. License constants must be prefixed with
licenses..- license = [ agpl3Plus unfree ]; + license = [ licenses.agpl3Plus licenses.unfree ];
🧹 Nitpick comments (1)
.nix/fabko.nix (1)
37-37: Remove unnecessary empty line.-
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (2)
.nix/default.nix(1 hunks).nix/fabko.nix(1 hunks)
🚧 Files skipped from review as they are similar to previous changes (1)
- .nix/default.nix
🧰 Additional context used
🪛 GitHub Actions: CI Linux Build
.nix/fabko.nix
[error] 69-69: Nix build error: undefined variable 'agpl3Plus' used in license attribute at line 69.
🔇 Additional comments (6)
.nix/fabko.nix (6)
1-15: LGTM: Well-structured dependency declarations.The dependency parameters and optional build flags are properly structured for a C++ project with conditional testing and coverage support.
17-24: LGTM: Clean version and dependency management.Reading the version from a file and using the import-from-json pattern for external dependencies follows good Nix practices.
31-35: LGTM: Appropriate conditional build inputs.The conditional inclusion of test and coverage tools based on the
execute_testparameter is well-implemented.
38-38: LGTM: Comprehensive coverage compiler flags.The coverage flags are appropriate for generating detailed C++ coverage reports with proper optimization disabling.
57-65: LGTM: Standard C++ dependencies for compiler project.The build inputs include appropriate libraries for a modern C++ compiler with logging, JSON handling, and async I/O support.
40-55: Verifygcovrinvocation in your Nix build environmentI wasn’t able to run
gcovrhere, so please confirm that, in the environment where this postCheck runs, all of the following flags are supported and produce a valid Cobertura XML report:
--filter=".*\.(cpp|hpp|hh)$"--exclude="/nix/store/.*"--gcov-executable=gcov--exclude-unreachable-branches--xml&--xml-pretty--output=$out/coverage/cobertura.xmlYou can verify by running:
gcovr --help | grep -E "(filter|exclude-unreachable-branches|xml)" -A2Adjust any patterns or flags as needed to match the version of
gcovrin your build.
There was a problem hiding this comment.
Actionable comments posted: 4
♻️ Duplicate comments (2)
fabko/compiler/backend/sat/solver.cpp (1)
105-106: Implement the constraint addition logic to prevent duplicate solutions.The TODO comment indicates that logic to disable found solutions is missing. Without this, the solver may return duplicate solutions, making the
expectedparameter meaningless.This is a critical part of the SAT solving algorithm. Would you like me to help implement the constraint addition logic based on the solver context interface?
fabko/compiler/backend/sat/solver.hh (1)
71-71: Critical: Inverted assertion condition.The assertion checks if the clause is empty but the error message indicates it should NOT be empty.
- fabko_assert(clause.vars().empty(), "Cannot make a clause watchers over an empty clause"); + fabko_assert(!clause.vars().empty(), "Cannot make a clause watchers over an empty clause");
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (5)
fabko/common/logging.hh(6 hunks)fabko/compiler/backend/sat/cli.hh(1 hunks)fabko/compiler/backend/sat/solver.cpp(1 hunks)fabko/compiler/backend/sat/solver.hh(1 hunks)fabko/fabko.cpp(1 hunks)
🚧 Files skipped from review as they are similar to previous changes (1)
- fabko/common/logging.hh
🧰 Additional context used
🧬 Code Graph Analysis (2)
fabko/fabko.cpp (1)
fabko/common/logging.cpp (2)
init_logger(30-45)init_logger(30-30)
fabko/compiler/backend/sat/solver.cpp (1)
fabko/compiler/backend/sat/solver_context.cpp (2)
solve_sat(87-119)solve_sat(87-87)
🔇 Additional comments (2)
fabko/fabko.cpp (1)
21-53: LGTM! Well-structured CLI implementation.The main function properly integrates the SAT solver backend with comprehensive logging configuration and error handling. The CLI setup follows good practices with clear option descriptions and proper initialization order.
fabko/compiler/backend/sat/solver.cpp (1)
49-51: Fix capacity check logic.The condition should check if the problem parameters haven't been parsed yet (capacity == 0), not if they have been set (capacity > 0).
- if (clauses.capacity() > 0) { + if (clauses.capacity() != 0) { throw std::runtime_error("Unexpected 'p' is specified twice"); }Likely an incorrect or invalid review comment.
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (1)
fabko/compiler/backend/sat/solver.hh (1)
123-133: Fix documentation: Replace DNF with CNF.The function documentation incorrectly mentions DNF (Disjunctive Normal Form) when it should reference CNF (Conjunctive Normal Form), as evidenced by the function name and parameter name.
/** - * @brief Create a model from a DNF file. + * @brief Create a model from a CNF file. * - * This function reads a DNF (Disjunctive Normal Form) file and constructs a model + * This function reads a CNF (Conjunctive Normal Form) file and constructs a model * that can be used by the SAT solver. The DNF file should contain clauses in the * appropriate format. * - * @param dnf_file Path to the DNF file to be processed. - * @return A model object representing the parsed DNF file. + * @param cnf_file Path to the CNF file to be processed. + * @return A model object representing the parsed CNF file. */ -model make_model_from_cnf_file(const std::filesystem::path& dnf_file); +model make_model_from_cnf_file(const std::filesystem::path& cnf_file);
🧹 Nitpick comments (1)
fabko/compiler/backend/sat/solver.hh (1)
72-80: Simplify the clause_watcher initialization.The immediately invoked lambda expression makes the constructor unnecessarily complex and harder to read.
- explicit clause_watcher(const var_soa& vs, const clause& clause) - : watchers_([&]() -> std::vector<literal> { // - using std::get; - fabko_assert(!clause.vars().empty(), "Cannot make a clause watchers over an empty clause"); - if (clause.vars().size() == 1) { - return {get<soa_literal>(vs[clause.vars().front()])}; - } - return {get<soa_literal>(vs[clause.vars().front()]), get<soa_literal>(vs[clause.vars().back()])}; - }()) {} + explicit clause_watcher(const var_soa& vs, const clause& clause) + : watchers_(initialize_watchers(vs, clause)) {} + +private: + static std::vector<literal> initialize_watchers(const var_soa& vs, const clause& clause) { + using std::get; + fabko_assert(!clause.vars().empty(), "Cannot make a clause watchers over an empty clause"); + if (clause.vars().size() == 1) { + return {get<soa_literal>(vs[clause.vars().front()])}; + } + return {get<soa_literal>(vs[clause.vars().front()]), get<soa_literal>(vs[clause.vars().back()])}; + }
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (4)
fabko/compiler/backend/sat/solver.cpp(1 hunks)fabko/compiler/backend/sat/solver.hh(1 hunks)fabko/compiler/backend/sat/solver_context.cpp(1 hunks)fabko/compiler/backend/sat/solver_context.hh(1 hunks)
🚧 Files skipped from review as they are similar to previous changes (3)
- fabko/compiler/backend/sat/solver_context.cpp
- fabko/compiler/backend/sat/solver.cpp
- fabko/compiler/backend/sat/solver_context.hh
🔇 Additional comments (1)
fabko/compiler/backend/sat/solver.hh (1)
48-49: No missing includes or forward declarations requiredThe
solver.hhheader already brings in both types:
- It includes
solver_context.hh, which in turn:
- Pulls in
<fil/datastructure/soa.hh>(definesvar_soaand its nestedstruct_id).- Includes
compiler/backend/metadata.h(definesfabko::compiler::compiler_context, found by unqualified lookup insidefabko::compiler::sat).No additional includes or forward declarations are needed here.
Likely an incorrect or invalid review comment.
There was a problem hiding this comment.
Actionable comments posted: 4
♻️ Duplicate comments (2)
fabko/compiler/backend/sat/solver.hh (2)
145-153: Fix documentation: Replace DNF with CNF and correct parameter name.The function documentation incorrectly mentions DNF (Disjunctive Normal Form) when it should reference CNF (Conjunctive Normal Form). Also, the parameter name should match the documentation correction.
/** - * @brief Create a model from a DNF file. + * @brief Create a model from a CNF file. * - * This function reads a DNF (Disjunctive Normal Form) file and constructs a model that can be used by the SAT solver. The DNF file should contain clauses in the + * This function reads a CNF (Conjunctive Normal Form) file and constructs a model that can be used by the SAT solver. The CNF file should contain clauses in the * appropriate format. * - * @param dnf_file Path to the DNF file to be processed. - * @return A model object representing the parsed DNF file. + * @param cnf_file Path to the CNF file to be processed. + * @return A model object representing the parsed CNF file. */ -model make_model_from_cnf_file(const std::filesystem::path& dnf_file); +model make_model_from_cnf_file(const std::filesystem::path& cnf_file);
125-127: Consider encapsulation for assignment_context members.The data members are currently public, which breaks encapsulation principles. Consider making them private with appropriate accessor methods.
+private: std::int64_t vsids_activity_ {}; //!< VSIDS (Variable State Independent Decaying Sum) activity value type std::size_t decision_level_ {}; //!< decision level of the literal std::optional<clause_soa::struct_id> clause_propagation_ {}; //!< clause that produced this (nullopt if decision type) + +public: + [[nodiscard]] std::int64_t vsids_activity() const { return vsids_activity_; } + [[nodiscard]] std::size_t decision_level() const { return decision_level_; } + [[nodiscard]] const std::optional<clause_soa::struct_id>& clause_propagation() const { return clause_propagation_; } + + void set_vsids_activity(std::int64_t activity) { vsids_activity_ = activity; } + void set_decision_level(std::size_t level) { decision_level_ = level; } + void set_clause_propagation(const clause_soa::struct_id& clause) { clause_propagation_ = clause; }
🧹 Nitpick comments (1)
fabko/compiler/backend/metadata.hh (1)
10-10: Fix typo in license header.The license name should be "AGPL" not "APGL".
-// the APGL license is applying. +// the AGPL license is applying.
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (5)
fabko/compiler/CMakeLists.txt(1 hunks)fabko/compiler/backend/metadata.hh(1 hunks)fabko/compiler/backend/sat/solver.hh(1 hunks)fabko/compiler/backend/sat/solver_context.cpp(1 hunks)fabko/compiler/backend/sat/solver_context.hh(1 hunks)
✅ Files skipped from review due to trivial changes (1)
- fabko/compiler/CMakeLists.txt
🚧 Files skipped from review as they are similar to previous changes (2)
- fabko/compiler/backend/sat/solver_context.cpp
- fabko/compiler/backend/sat/solver_context.hh
🔇 Additional comments (1)
fabko/compiler/backend/sat/solver.hh (1)
30-31: Review operator implementations for correctness.The equality operator compares absolute values, which means
literal(5)andliteral(-5)would be considered equal. The spaceship operator also compares absolute values. Verify this is the intended behavior for literal comparison.// Current implementation treats positive and negative literals as equal literal(5) == literal(-5); // returns true literal(5) <=> literal(-5); // returns 0 (equal)
There was a problem hiding this comment.
Actionable comments posted: 0
🧹 Nitpick comments (6)
README.md (6)
3-3: Add alt-text to comply with accessibility & markdown-lint (MD045).The Tokei badge lacks alt text, triggering markdownlint warnings and hindering accessibility.
- +[](https://github.com/FreeYourSoul/Fabko)
7-8: Rephrase opening sentence for clarity & grammatical correctness.Current wording is hard to parse and splits a single sentence across two lines.
-Free Agent Board operative is an agent / blackboard library that enables distributed resolution of a problem among -Agents. +Free Agent Board Operative (FabKo) is an agent-based blackboard library that enables the distributed resolution of +problems among agents.
12-17: Fix multiple grammar issues & streamline the paragraph.Language-tool flags missing articles, plural agreement, and awkward phrasing.
-Fabko is a library that some to make it easy to create agent that interoperates via customizable communication medium ( -peer-to-peer, centralised server based, distributed etc...). - -The agent will then be able to communicate through a blackboard generated each time an agent attempts to achieve a new -action. And the agent is going to cooperate to find a solution to resolve that problem. +Fabko aims to make it easy to create agents that interoperate through customizable communication media +(peer-to-peer, centralized server-based, fully distributed, etc.). + +Agents communicate via a blackboard generated each time a new task is initiated, then cooperate to find a solution.
21-27: Polish description of FABL & peerboard for readability.-Free Agent Board Language is the base of the FabKo library as it is a declarative language that makes it possible for an -agent to describe the resources and -the capabilities that it provides. Those can be aggregated among multiple agents to produce complex graphs. It is then -possible to produce a request over this -The compiled graph represents the blackboard on which each node can add their own descriptions of actions. The agent -that holds the peerboard is the agent that aggregates +Free Agent Board Language (FABL) is the foundation of FabKo. It is a declarative language that lets an agent describe +the resources and capabilities it provides. These descriptions can be aggregated across multiple agents to produce +complex graphs, over which queries can determine whether an action can be performed. + +The compiled graph acts as the blackboard where each node can add its own action descriptions. The agent that hosts +the peerboard aggregates all capabilities.
70-70: Upgrade to a proper markdown heading for section discoverability.-actor part of FABL +## Actor part of FABL
144-145: Grammar tweak: plural & typography.-Here is an example of the 9 Queen problems using the actor syntax +Here is an example of the Nine Queens problem using the actor syntax
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
README.md(4 hunks)
🧰 Additional context used
🪛 LanguageTool
README.md
[uncategorized] ~12-~12: You might be missing the article “an” here.
Context: ...ary that some to make it easy to create agent that interoperates via customizable com...
(AI_EN_LECTOR_MISSING_DETERMINER_AN)
[grammar] ~14-~14: The plural determiner ‘those’ does not agree with the singular noun ‘agent’.
Context: ...sed server based, distributed etc...). Those agent will be able to register their capabili...
(THIS_NNS)
[uncategorized] ~21-~21: Possible missing comma found.
Context: ...Board Language is the base of the FabKo library as it is a declarative language that ma...
(AI_HYDRA_LEO_MISSING_COMMA)
[style] ~25-~25: In contexts where ‘if’ is followed by ‘or’, using ‘whether’ may be more appropriate (and formal).
Context: ...uest over this compiled graph to define if the agent can do an action or not. The ...
(IF_WHETHER)
🪛 markdownlint-cli2 (0.17.2)
README.md
3-3: Images should have alternate text (alt text)
(MD045, no-alt-text)
🔇 Additional comments (1)
README.md (1)
57-58: Correct predicate change looks good.Switching
i == jtoi != jcorrectly excludes the same queen from comparison—nice catch.
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (2)
fabko/compiler/backend/sat/solver_context.cpp (2)
40-56: Critical: Incorrect loop condition in backtrack function.The while loop condition is inverted - it should continue while the trail is NOT empty.
- while (ctx.trail_.empty()) { + while (!ctx.trail_.empty()) {
117-118: Fix incorrect usage of unit_propagation return value.The function returns
std::optional<clause_soa::struct_id>, not a boolean. The condition should check if a conflict was found.- if (!unit_propagation(ctx)) - return std::unexpected(sat_error::unsatisfiable); + auto initial_conflict = unit_propagation(ctx); + if (initial_conflict.has_value()) + return std::unexpected(sat_error::unsatisfiable);
🧹 Nitpick comments (2)
fabko/compiler/backend/sat/solver_context.cpp (2)
25-38: TODO: Complete conflict resolution implementation.The conflict resolution function is currently stubbed out and needs proper implementation of the Unique Implication Point (UIP) algorithm and learned clause generation.
Do you want me to help implement the conflict resolution algorithm or open a new issue to track this task?
106-113: TODO: Implement clause learning functionality.The clause learning function is currently stubbed out and needs proper implementation to add learned clauses to the solver's clause database.
Do you want me to help implement the clause learning algorithm or open a new issue to track this task?
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (2)
fabko/compiler/backend/sat/solver.hh(1 hunks)fabko/compiler/backend/sat/solver_context.cpp(1 hunks)
🚧 Files skipped from review as they are similar to previous changes (1)
- fabko/compiler/backend/sat/solver.hh
⏰ Context from checks skipped due to timeout of 90000ms (1)
- GitHub Check: Codacy Static Code Analysis
🔇 Additional comments (3)
fabko/compiler/backend/sat/solver_context.cpp (3)
1-17: LGTM: Appropriate includes and headers.The included headers are well-organized and appropriate for the SAT solver implementation.
58-104: LGTM: Well-implemented unit propagation algorithm.The unit propagation function is well-structured with proper conflict detection and literal assignment logic. The use of modern C++ features like ranges enhances readability.
152-185: LGTM: Well-structured constructor with proper initialization.The constructor effectively initializes the solver context using lambda-based initialization. The mapping of literals to variable IDs and clause construction logic is correct and follows modern C++ practices.
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (4)
fabko/compiler/backend/sat/solver_context.cpp (4)
24-24: Critical: Fix constexpr usage with std::string.This is the same issue previously identified.
std::stringis not a literal type and cannot be used withconstexpr. This will cause compilation errors.-constexpr std::string SECTION = "sat_solver"; //!< logging a section for the SAT solver +constexpr std::string_view SECTION = "sat_solver"; //!< logging a section for the SAT solver
78-89: Critical: Incorrect loop condition in backtrack function.This is the same issue previously identified. The while loop condition is inverted - it should continue while the trail is NOT empty.
- while (ctx.trail_.empty()) { + while (!ctx.trail_.empty()) {
153-154: Critical: Type mismatch - cannot use ! operator on std::optional.The
unit_propagationfunction returnsstd::optional<clause_soa::struct_id>, but the code is using the!operator on it, which is invalid.- if (!unit_propagation(ctx)) - return std::unexpected(sat_error::unsatisfiable); + auto conflict = unit_propagation(ctx); + if (conflict.has_value()) + return std::unexpected(sat_error::unsatisfiable);
157-182: Critical: Potential infinite loop - solution.literals is never populated.This is the same issue previously identified. The while loop condition
solution.literals.empty()could run indefinitely sincesolution.literalsis never populated within the loop. The loop lacks decision-making logic to assign values to variables.You need to implement:
- Decision-making logic to populate solution.literals when no unit propagation is possible
- Proper termination conditions for satisfiable cases
- Logic to extract the solution when all variables are assigned
🧹 Nitpick comments (1)
fabko/compiler/backend/sat/solver_context.cpp (1)
103-113: Performance issue: Inefficient fold_right usage.The
fold_rightoperation is inefficient because it passes the result vector by value in each iteration, causing unnecessary copies.- const auto unassigned = std::ranges::fold_right(clauselit_mapped_varid, - std::vector<std::pair<literal, var_soa::struct_id>> {}, // - [&ctx, &clause_struct](const auto& pair, auto res) { - const auto clause_var_id = pair.second; - const auto& [literal, assignment, assignment_context, meta] = ctx.vars_soa_[clause_var_id]; - if (assignment != assignment::not_assigned) { - return res; - } - res.push_back(pair); - return res; - }); + std::vector<std::pair<literal, var_soa::struct_id>> unassigned; + for (const auto& pair : clauselit_mapped_varid) { + const auto clause_var_id = pair.second; + const auto& [literal, assignment, assignment_context, meta] = ctx.vars_soa_[clause_var_id]; + if (assignment == assignment::not_assigned) { + unassigned.push_back(pair); + } + }
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (2)
fabko/compiler/backend/sat/solver.hh(1 hunks)fabko/compiler/backend/sat/solver_context.cpp(1 hunks)
🚧 Files skipped from review as they are similar to previous changes (1)
- fabko/compiler/backend/sat/solver.hh
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (1)
- GitHub Check: Codacy Static Code Analysis
🔇 Additional comments (1)
fabko/compiler/backend/sat/solver_context.cpp (1)
188-221: Well-implemented constructor with proper initialization.The constructor correctly initializes the solver context by:
- Setting up the SoA structures for variables and clauses
- Mapping model literals to internal variable IDs
- Creating clause watchers for propagation
- Including defensive assertions to ensure data integrity
The initialization logic is comprehensive and handles the complex mapping between the external model and internal solver structures.
There was a problem hiding this comment.
Actionable comments posted: 1
♻️ Duplicate comments (5)
fabko/compiler/backend/sat/solver_context.cpp (5)
24-24: Fix constexpr usage with std::string.This issue was flagged in previous reviews and remains unresolved.
std::stringis not a literal type and cannot be used withconstexpr.-constexpr std::string SECTION = "sat_solver"; +constexpr std::string_view SECTION = "sat_solver";
113-113: Critical: Incorrect loop condition in backtrack function.This critical issue from previous reviews remains unresolved. The while loop condition is inverted - it should continue while the trail is NOT empty.
- while (ctx.trail_.empty()) { + while (!ctx.trail_.empty()) {
179-187: Incomplete implementation: Clause learning is not implemented.The
learn_additional_clausefunction remains stubbed out as identified in previous reviews. This is a critical component of the CDCL algorithm that needs implementation.The function should:
- Add the learned clause to
ctx.clauses_soa_- Set up appropriate watchers for the new clause
- Update solver statistics
Do you want me to help implement the clause learning logic?
195-220: Potential infinite loop: solution.literals is never populated.The while loop condition
solution.literals.empty()could run indefinitely sincesolution.literalsis never populated within the loop, as identified in previous reviews.You need to implement:
- Decision-making logic to populate solution.literals
- Proper termination conditions
- SAT/UNSAT determination logic
- while (solution.literals.empty()) { + while (solution.literals.empty() && /* add termination condition */) {
191-192: Fix return type mismatch in unit_propagation call.The function call expects
std::optional<clause_soa::struct_id>but the conditional check treats it as a bool. This creates a type mismatch.- if (!unit_propagation(ctx)) - return std::unexpected(sat_error::unsatisfiable); + auto conflict = unit_propagation(ctx); + if (conflict.has_value()) + return std::unexpected(sat_error::unsatisfiable);
🧹 Nitpick comments (5)
fabko/common/exception.hh (4)
10-10: Fix typo in license abbreviation."APGL" should be "AGPL" to match the correct license name mentioned earlier.
-// the APGL license is applying. +// the AGPL license is applying.
24-24: Use conventional parameter naming.The parameter name
I(capital i) is unconventional and can be confused withl(lowercase L) in some fonts. Consider using a more descriptive name.- [[nodiscard]] std::string message(int I) const override { return fmt::format("Fabko::Database Exception Category : {} : id {}", name(), I); } + [[nodiscard]] std::string message(int code) const override { return fmt::format("Fabko::Database Exception Category : {} : id {}", name(), code); }And similarly for line 29:
- [[nodiscard]] std::string message(int I) const override { return fmt::format("Fabko Exception Category : {} : id {}", name(), I); } + [[nodiscard]] std::string message(int code) const override { return fmt::format("Fabko Exception Category : {} : id {}", name(), code); }Also applies to: 29-29
39-39: Add const noexcept qualifier to getter method.The
code()method should be markedconst noexceptas it's a simple getter that doesn't modify state or throw exceptions.- [[nodiscard]] int code() const { return _ec.value(); } + [[nodiscard]] int code() const noexcept { return _ec.value(); }
60-60: Replace magic number with named constant.The magic number
42should be replaced with a named constant for better code maintainability and clarity.Consider defining a constant at the namespace level:
namespace { constexpr int DEFAULT_ERROR_CODE = 42; } // anonymous namespaceThen update the usage:
- fabko_assert(assertion, {42, except_cat::fbk {}}, msg); + fabko_assert(assertion, {DEFAULT_ERROR_CODE, except_cat::fbk {}}, msg);fabko/compiler/backend/sat/solver_context.cpp (1)
243-250: Optimize variable lookup in clause construction.The current implementation uses a linear search through
vars_soa_for each literal, which could be expensive for large SAT instances.Consider creating a hash map from literals to variable IDs during initialization:
// Add to constructor initialization std::unordered_map<literal, Vars_Soa::struct_id> literal_to_id; for (const auto& var_struct : vars_soa_) { literal_to_id[get<soa_literal>(var_struct)] = var_struct.struct_id(); } // Then use in clause construction: auto it = literal_to_id.find(l); fabko_assert(it != literal_to_id.end(), "a clause cannot contains a non-defined literal"); res.push_back(it->second);
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (5)
fabko/common/exception.hh(1 hunks)fabko/compiler/backend/sat/cli.hh(1 hunks)fabko/compiler/backend/sat/solver.cpp(1 hunks)fabko/compiler/backend/sat/solver_context.cpp(1 hunks)fabko/compiler/backend/sat/solver_context.hh(1 hunks)
✅ Files skipped from review due to trivial changes (1)
- fabko/compiler/backend/sat/cli.hh
🚧 Files skipped from review as they are similar to previous changes (2)
- fabko/compiler/backend/sat/solver_context.hh
- fabko/compiler/backend/sat/solver.cpp
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (1)
- GitHub Check: Codacy Static Code Analysis
🔇 Additional comments (2)
fabko/compiler/backend/sat/solver_context.cpp (2)
26-109: Verify UIP detection logic correctness.The UIP detection implementation appears more complete than in previous reviews, but the complex logic should be verified for correctness, particularly the clause resolution and backtrack level calculation.
Please verify this implementation against standard CDCL algorithms to ensure:
- Proper UIP identification
- Correct learned clause construction
- Accurate backtrack level calculation
- Proper handling of decision levels
You might want to add unit tests specifically for the conflict resolution logic.
77-77: Fix incorrect usage of structured binding in erase_if.The code attempts to use a structured binding in the erase_if predicate, but
lit_structis a pair, not a structured binding.- std::erase_if(learned_clause, [&trail_lit](const auto& lit_struct) { return get<soa_literal>(lit_struct).value() == trail_lit.value(); }); + std::erase_if(learned_clause, [&trail_lit](const auto& lit_struct) { return lit_struct.first.value() == trail_lit.value(); });Likely an incorrect or invalid review comment.
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (6)
fabko/common/exception.hh (1)
45-58: Make assert functions inline to prevent multiple definition errors.Static functions defined in headers will cause multiple definition errors when included in multiple translation units. These should be marked
inline.fabko/compiler/backend/sat/solver_context.cpp (5)
23-23: Fix constexpr usage with std::string.
std::stringis not a literal type and cannot be used withconstexpr. This will cause compilation errors.
127-127: Critical: Incorrect loop condition in backtrack function.The while loop condition is inverted - it should continue while the trail is NOT empty.
229-229: Potential infinite loop: solution.literals is never populated.The while loop condition
solution.literals.empty()could run indefinitely sincesolution.literalsis never populated within the loop.
191-199: Incomplete implementation: Clause learning is not implemented.The
learn_additional_clausefunction is stubbed out and doesn't actually add learned clauses to the solver state. This is a critical component of the CDCL algorithm.
224-257: Missing solution population logic.The solve function never populates
solution.literalswhen a satisfying assignment is found, leading to an infinite loop.Add logic to populate the solution when all clauses are satisfied:
} else { - make_decision(ctx); + if (!make_decision(ctx)) { + // All variables assigned, check if solution is complete + for (const auto& var_struct : ctx.vars_soa_) { + const auto& [lit, assign, assign_ctx, meta] = var_struct; + if (assign == assignment::on) { + solution.literals.push_back(lit); + } + } + break; + } }
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (5)
fabko/cli_base.hh(1 hunks)fabko/common/exception.hh(1 hunks)fabko/compiler/backend/sat/solver_context.cpp(1 hunks)fabko/compiler/backend/sat/solver_context.hh(1 hunks)fabko/fabko.cpp(1 hunks)
🚧 Files skipped from review as they are similar to previous changes (3)
- fabko/cli_base.hh
- fabko/fabko.cpp
- fabko/compiler/backend/sat/solver_context.hh
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (1)
- GitHub Check: Codacy Static Code Analysis
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (7)
fabko/compiler/backend/sat/solver_context.cpp (4)
31-31: Fix compilation error with constexpr std::string.
std::stringcannot be used withconstexpras it's not a literal type, causing compilation errors.Apply this fix:
-constexpr std::string SECTION = "sat_solver"; //!< logging a section for the SAT solver +constexpr std::string_view SECTION = "sat_solver"; //!< logging a section for the SAT solver
152-152: Critical: Inverted loop condition causes infinite loop.The while loop condition is inverted - it should continue while the trail is NOT empty. This would cause the function to never execute the loop body when there are items to backtrack.
Apply this fix:
- while (ctx.trail_.empty()) { + while (!ctx.trail_.empty()) {
267-304: Critical: Potential infinite loop - solution.literals never populated.The main solving loop condition
solution.literals.empty()could run indefinitely sincesolution.literalsis never populated within the loop. The break statement at line 301 exits the loop but doesn't populate the solution.The loop needs to actually populate
solution.literalswhen a solution is found:if (is_sat_solved) { log_info("solution found"); - break; // @todo remove break and fill-up solution + // Populate solution with current assignments + for (const auto& var_struct : ctx.vars_soa_) { + const auto& [literal, assignment, assignment_context, meta] = var_struct; + if (assignment != assignment::not_assigned) { + solution.literals.push_back(assignment == assignment::on ? literal : Literal(-literal.value())); + } + } + break; }
226-234: Critical: Incomplete clause learning implementation.The
learn_additional_clausefunction is mostly stubbed out and doesn't actually add learned clauses to the solver state, which is essential for the CDCL algorithm.This function should:
- Add the learned clause to
ctx.clauses_soa_- Set up appropriate watchers for the new clause
- Update solver statistics
The current implementation only increments a counter without actually learning the clause.
fabko/compiler/backend/sat/solver.hh (3)
164-172: Fix documentation: Replace DNF with CNF.The function documentation incorrectly mentions DNF (Disjunctive Normal Form) when it should reference CNF (Conjunctive Normal Form), as evidenced by the function name and parameter name.
Apply this fix:
/** - * @brief Create a model from a DNF file. + * @brief Create a model from a CNF file. * - * This function reads a DNF (Disjunctive Normal Form) file and constructs a model that can be used by the SAT solver. The DNF file should contain clauses in the + * This function reads a CNF (Conjunctive Normal Form) file and constructs a model that can be used by the SAT solver. The CNF file should contain clauses in the * appropriate format. * - * @param dnf_file Path to the DNF file to be processed. - * @return A model object representing the parsed DNF file. + * @param cnf_file Path to the CNF file to be processed. + * @return A model object representing the parsed CNF file. */ -model make_model_from_cnf_file(const std::filesystem::path& dnf_file); +model make_model_from_cnf_file(const std::filesystem::path& cnf_file);
144-146: Consider encapsulation for assignment_context members.The data members are currently public, which breaks encapsulation principles. Consider making them private with appropriate accessor methods.
+ private: std::int64_t vsids_activity_ {}; //!< VSIDS (Variable State Independent Decaying Sum) activity value type std::size_t decision_level_ {}; //!< decision level of the literal std::optional<Clauses_Soa::struct_id> clause_propagation_ {}; //!< clause that produced this (std::nullopt if decision type) + + public: + [[nodiscard]] std::int64_t vsids_activity() const { return vsids_activity_; } + [[nodiscard]] std::size_t decision_level() const { return decision_level_; } + [[nodiscard]] const std::optional<Clauses_Soa::struct_id>& clause_propagation() const { return clause_propagation_; }
86-86: Add missing include for metadata.The code references
metadatabut doesn't include the header file.#include "common/exception.hh" #include "solver_context.hh" +#include "metadata.hh"
🧹 Nitpick comments (1)
fabko/compiler/backend/sat/solver.hh (1)
194-194: Clarify the expected parameter purpose.The
solvemethod takes anexpectedparameter with default value -1, but there's no documentation explaining its purpose. This makes the API unclear.Add documentation for the
expectedparameter:- std::vector<result> solve(std::int32_t expected = -1); + /** + * @param expected Maximum number of solutions to find, or -1 for unlimited + */ + std::vector<result> solve(std::int32_t expected = -1);
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (4)
fabko/compiler/backend/sat/solver.cpp(1 hunks)fabko/compiler/backend/sat/solver.hh(1 hunks)fabko/compiler/backend/sat/solver_context.cpp(1 hunks)fabko/compiler/backend/sat/solver_context.hh(1 hunks)
🚧 Files skipped from review as they are similar to previous changes (2)
- fabko/compiler/backend/sat/solver.cpp
- fabko/compiler/backend/sat/solver_context.hh
🧰 Additional context used
🧬 Code Graph Analysis (1)
fabko/compiler/backend/sat/solver_context.cpp (1)
fabko/compiler/backend/sat/solver.cpp (2)
to_string(30-36)to_string(30-30)
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (1)
- GitHub Check: Codacy Static Code Analysis
🔇 Additional comments (1)
fabko/compiler/backend/sat/solver.hh (1)
39-40: Ensure consistent comparison semantics.The equality operator compares absolute values but the spaceship operator also compares absolute values. This means that
Literal(5)andLiteral(-5)would be considered equal, which may not be the intended behavior for literals in SAT solving.Verify if this equality behavior is intentional for the SAT solver logic where positive and negative literals of the same variable should be considered equal for comparison purposes.
sat : add log if sat solution not found
FreeYourSoul
force-pushed
the
sat/reimplement
branch
from
8df2e45 to
de94c0d
Compare
There was a problem hiding this comment.
Actionable comments posted: 0
♻️ Duplicate comments (2)
fabko/compiler/backend/sat/solver_context.cpp (2)
30-30: Fix constexpr usage with std::string.This is the same issue flagged in previous reviews.
std::stringis not a literal type and cannot be used withconstexpr.-constexpr std::string SECTION = "sat_solver"; //!< logging a section for the SAT solver +constexpr std::string_view SECTION = "sat_solver"; //!< logging a section for the SAT solver
128-128: Fix incorrect erase_if predicate.This is the same issue flagged in previous reviews. The predicate uses
get<soa_literal>(lit_struct)butlit_structis astd::pair<Literal, Vars_Soa::struct_id>, not a SoA struct.- std::erase_if(learned_clause, [&trail_lit](const auto& lit_struct) { return get<soa_literal>(lit_struct).value() == trail_lit.value(); }); + std::erase_if(learned_clause, [&trail_lit](const auto& lit_struct) { return lit_struct.first.value() == trail_lit.value(); });
🧹 Nitpick comments (2)
fabko/compiler/backend/sat/solver_context.cpp (2)
61-69: Implement overflow handling for VSIDS activity.The function correctly increases VSIDS activity, but the comment mentions handling numerical overflow which is not implemented.
Consider implementing overflow protection:
void increase_vsids_activity(Solver_Context& ctx, const Clause& clause) { const auto& all_lit = clause.get_literals(); + + // Check if any variable's activity is approaching overflow threshold + constexpr double MAX_ACTIVITY = 1e100; + bool needs_rescale = std::ranges::any_of(all_lit, [&ctx](const auto& lit) { + const auto& [_, varid] = lit; + return get<soa_assignment_ctx>(ctx.vars_soa_[varid]).vsids_activity_ > MAX_ACTIVITY; + }); + + if (needs_rescale) { + // Rescale all variable activities + std::ranges::for_each(ctx.vars_soa_, [](auto& var_struct) { + get<soa_assignment_ctx>(var_struct).vsids_activity_ /= MAX_ACTIVITY; + }); + } + std::for_each(all_lit.begin(), all_lit.end(), [&ctx](const auto& lit) { const auto& [_, varid] = lit; auto varstruct = ctx.vars_soa_[varid]; auto& [literal, assignment, assignment_context, meta] = varstruct; - assignment_context.vsids_activity_ += ctx.config_.vsids_increment; //@todo handle numerical overflow + assignment_context.vsids_activity_ += ctx.config_.vsids_increment; }); }
267-293: Consider polarity heuristic for better performance.The function correctly implements VSIDS-based decision making, but always assigns variables to
assignment::onby default. Consider implementing a polarity heuristic for better performance.Consider implementing a polarity heuristic:
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 ?) +// Use polarity heuristic (e.g., saved polarity from previous assignments) +assignment = assignment_context.saved_polarity.value_or(assignment::on);
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (2)
fabko/compiler/backend/sat/solver.hh(1 hunks)fabko/compiler/backend/sat/solver_context.cpp(1 hunks)
🚧 Files skipped from review as they are similar to previous changes (1)
- fabko/compiler/backend/sat/solver.hh
🧰 Additional context used
🧬 Code Graph Analysis (1)
fabko/compiler/backend/sat/solver_context.cpp (1)
fabko/compiler/backend/sat/solver.cpp (2)
to_string(30-36)to_string(30-30)
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (1)
- GitHub Check: Codacy Static Code Analysis
🔇 Additional comments (6)
fabko/compiler/backend/sat/solver_context.cpp (6)
36-43: LGTM: Correct clause satisfaction check.The function correctly implements clause satisfaction logic by checking if any literal in the clause is assigned to a value that makes the clause true.
45-53: LGTM: Correct conflict detection with planned removal.The function correctly detects conflicts by checking if all literals are assigned in a way that makes the clause false. The TODO comment indicates this will be replaced with watcher-based implementation.
180-196: LGTM: Correct backtracking implementation.The function correctly implements non-linear backtracking by unassigning variables beyond the target decision level and updating the trail.
198-255: LGTM: Correct unit propagation implementation.The function correctly implements unit propagation with proper conflict detection, literal assignment, and trail management.
257-265: LGTM: Correct clause learning implementation.The function correctly learns new clauses, handles empty clauses (unsatisfiable case), and updates solver statistics.
295-349: LGTM: Correct CDCL solving loop implementation.The main solving loop correctly implements the CDCL algorithm with proper restart logic, conflict resolution, clause learning, and solution construction.
There was a problem hiding this comment.
Actionable comments posted: 2
♻️ Duplicate comments (1)
fabko/compiler/backend/sat/solver_context.cpp (1)
30-30: Fix constexpr usage with std::string.
std::stringis not a literal type and cannot be used withconstexpr. This will cause compilation errors.-constexpr std::string SECTION = "sat_solver"; //!< logging a section for the SAT solver +constexpr std::string_view SECTION = "sat_solver"; //!< logging a section for the SAT solver
📜 Review details
Configuration used: CodeRabbit UI
Review profile: CHILL
Plan: Pro
📒 Files selected for processing (1)
fabko/compiler/backend/sat/solver_context.cpp(1 hunks)
🧰 Additional context used
🧬 Code Graph Analysis (1)
fabko/compiler/backend/sat/solver_context.cpp (1)
fabko/compiler/backend/sat/solver.cpp (2)
to_string(30-36)to_string(30-30)
⏰ Context from checks skipped due to timeout of 90000ms. You can increase the timeout in your CodeRabbit configuration to a maximum of 15 minutes (900000ms). (1)
- GitHub Check: Codacy Static Code Analysis
🔇 Additional comments (9)
fabko/compiler/backend/sat/solver_context.cpp (9)
36-43: Function logic is correct.The implementation correctly checks if any literal in the clause satisfies it by matching literal polarity with variable assignment.
45-53: Function logic is correct.The implementation correctly detects conflicts by checking if all literals in the clause are falsified. The todo comment indicates this is temporary until watchers are implemented.
79-174: Conflict resolution implementation is comprehensive.The function correctly implements CDCL conflict analysis with proper UIP detection, learned clause construction, and backtrack level calculation. The implementation addresses the previously incomplete logic.
182-199: Backtracking implementation is correct.The function properly implements non-linear backtracking, correctly unassigning variables beyond the target level and updating the solver state.
201-258: Unit propagation implementation is correct.The function properly implements unit propagation with correct conflict detection and variable assignment logic. The type issues from previous reviews have been resolved.
260-268: Clause learning implementation is correct.The function properly adds learned clauses to the solver state and updates statistics. The previously incomplete implementation has been addressed.
270-296: Decision making implementation is correct.The function properly filters unassigned variables and selects the one with highest VSIDS activity. The previously identified issues with inverted logic and variable filtering have been resolved.
298-352: CDCL solving algorithm implementation is comprehensive.The main solving loop correctly implements the complete CDCL algorithm with proper conflict handling, clause learning, backtracking, decision making, and restart logic. The solution population issue has been resolved.
356-390: Constructor correctly initializes solver state.The Solver_Context constructor properly initializes the SoA structures for variables and clauses, sets up watchers, and initializes VSIDS activities. The implementation correctly transforms the model into the solver's internal representation.
1 participant
Summary by CodeRabbit
New Features
Bug Fixes
Refactor
Chores
Documentation