diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index fc17ad4..ab76129 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -74,7 +74,7 @@ jobs: CIBW_SKIP: "*i686 *ppc64le *s390x *win32* *musllinux*" CIBW_MANYLINUX_X86_64_IMAGE: >- ghcr.io/${{ env.REPO_LC }}/manylinux-deps:latest - CIBW_TEST_REQUIRES: pytest + CIBW_TEST_REQUIRES: pytest torch CIBW_TEST_COMMAND: "cd {project} && pytest {project}/tests" - uses: actions/upload-artifact@v4 diff --git a/assets/toy/toy1.cnf b/assets/toy/toy1.cnf new file mode 100644 index 0000000..febe364 --- /dev/null +++ b/assets/toy/toy1.cnf @@ -0,0 +1,5 @@ +p cnf 6 4 +-1 -2 0 +2 3 -2 0 +4 5 0 +4 6 0 diff --git a/include/kompyle/core.h b/include/kompyle/core.h index f4dcc8b..b458dc3 100644 --- a/include/kompyle/core.h +++ b/include/kompyle/core.h @@ -15,10 +15,6 @@ #include #include -NodePtr -compile_from_ganak( - const std::string& cnf_file); - NodePtr compile_from_ganak( Circuit* circ, diff --git a/include/kompyle/field_circuit.h b/include/kompyle/field_circuit.h index 729edfe..3343ead 100644 --- a/include/kompyle/field_circuit.h +++ b/include/kompyle/field_circuit.h @@ -10,62 +10,95 @@ class FCircuit final : public CMSat::Field { public: // NOTE(Ibrahim) // FCircuit does not own the `circ` pointer - FCircuit(NodePtr node, Circuit* circ) - : node_(node), circ_(circ) {} + FCircuit(NodePtr node, Circuit* circ, double count = 1.0) + : node_(node), circ_(circ), count_(count) {} - NodePtr get_node() const { return node_; } + NodePtr get_node() const { return materialise(); } Circuit* get_circuit() const { return circ_; } + double get_count() const { return count_; } + + void add_pending_lit(NodePtr lit) { + pending_lits_.push_back(lit); + } std::unique_ptr dup() const final { - return std::make_unique(node_, circ_); + auto f = std::make_unique(node_, circ_, count_); + f->pending_lits_ = pending_lits_; + return f; } std::unique_ptr add(const Field& other) final { const auto& o = cast(other); - return make(circ_->or_node({ node_, o.node_ })); + return std::make_unique( + circ_->or_node({materialise(), o.materialise()}), + circ_, count_ + o.count_); } Field& operator+=(const Field& other) final { const auto& o = cast(other); - node_ = circ_->or_node({ node_, o.node_ }); + // std::raise(SIGINT); + node_ = circ_->or_node({materialise(), o.materialise()}); + pending_lits_.clear(); + count_ += o.count_; return *this; } Field& operator*=(const Field& other) final { const auto& o = cast(other); - node_ = circ_->and_node({ node_, o.node_ }); + // std::raise(SIGINT); + if (o.node_.get()->is_true() && !o.pending_lits_.empty()) { + for (const auto& l : o.pending_lits_) + pending_lits_.push_back(l); + } else { + node_ = circ_->and_node({materialise(), o.materialise()}); + pending_lits_.clear(); + } + count_ *= o.count_; return *this; } - // NOTE(Ibrahim) - // not needed for circuits, treat as no-op - Field& operator-=(const Field&) final { return *this; } + Field& operator-=(const Field& other) final { + const auto& o = cast(other); + count_ -= o.count_; + return *this; + } - // NOTE(Ibrahim) - // not needed for circuits, treat as no-op - Field& operator/=(const Field&) final { return *this; } + Field& operator/=(const Field& other) final { + const auto& o = cast(other); + if (o.count_ == 0.0) throw std::runtime_error("FCircuit /= division by zero"); + + // std::raise(SIGINT); + assert((o.node_.get()->is_true() && o.pending_lits_.size() == 1)); + const NodePtr& to_remove = o.pending_lits_[0]; + auto it = std::find(pending_lits_.begin(), pending_lits_.end(), to_remove); + assert(it != pending_lits_.end()); + + pending_lits_.erase(it); + count_ /= o.count_; + return *this; + } Field& operator=(const Field& other) final { - node_ = cast(other).node_; - circ_ = cast(other).circ_; + const auto& o = cast(other); + node_ = o.node_; + circ_ = o.circ_; + count_ = o.count_; + pending_lits_ = o.pending_lits_; return *this; } bool operator==(const Field& other) const final { - return node_ == cast(other).node_; + return materialise() == cast(other).materialise(); } bool is_zero() const final { - return node_.get() && node_.get()->is_false(); + return node_.get()->is_false(); } bool is_one() const final { - return node_.get() && node_.get()->is_true(); + return node_.get()->is_true() && pending_lits_.empty(); } - void set_zero() final { node_ = circ_->false_node(); } - void set_one() final { node_ = circ_->true_node(); } - std::ostream& display(std::ostream& os) const final { if (node_.get()) os << node_.get()->get_label(); @@ -74,11 +107,23 @@ class FCircuit final : public CMSat::Field { return os; } + void set_zero() final { + node_ = circ_->false_node(); + pending_lits_.clear(); + count_ = 0.0; + } + uint64_t bytes_used() const final { // NOTE(Ibrahim): Circuit size not included return sizeof(FCircuit); } + void set_one() final { + node_ = circ_->true_node(); + pending_lits_.clear(); + count_ = 1.0; + } + bool parse(const std::string&, const uint32_t) final { // NOTE(Ibrahim): Circuit size not included return false; @@ -89,12 +134,18 @@ class FCircuit final : public CMSat::Field { return static_cast(f); } - std::unique_ptr make(NodePtr n) const { - return std::make_unique(n, circ_); + NodePtr materialise() const { + if (pending_lits_.empty()) return node_; + std::vector children(pending_lits_.begin(), pending_lits_.end()); + if (!node_.get()->is_true()) children.push_back(node_); + if (children.size() == 1) return children[0]; + return circ_->and_node(children); } - NodePtr node_; + NodePtr node_; Circuit* circ_; + double count_; + std::vector pending_lits_; }; class FGenCircuit final : public CMSat::FieldGen { @@ -107,26 +158,21 @@ class FGenCircuit final : public CMSat::FieldGen { std::unique_ptr lit_field(int dimacs_lit) const { - return std::make_unique( - circ_->literal_node(dimacs_lit), circ_); - } - - std::unique_ptr - free_var_field(int var) const { - NodePtr pos = circ_->literal_node(+var); - NodePtr neg = circ_->literal_node(-var); - return std::make_unique( - circ_->or_node({ pos, neg }), circ_); + // auto f = std::make_unique( + // circ_->literal_node(dimacs_lit), circ_, 1.0); + auto f = std::make_unique(circ_->true_node(), circ_, 1.0); + f->add_pending_lit(circ_->literal_node(dimacs_lit)); + return f; } std::unique_ptr zero() const final { return std::make_unique( - circ_->false_node(), circ_); + circ_->false_node(), circ_, 0.0); } std::unique_ptr one() const final { return std::make_unique( - circ_->true_node(), circ_); + circ_->true_node(), circ_, 1.0); } // NOTE(Ibrahim): @@ -144,11 +190,9 @@ class FGenCircuit final : public CMSat::FieldGen { bool larger_than( const CMSat::Field& a, const CMSat::Field& b) const final { - // implied ordering from pointer addresses ? - // const auto& ac = static_cast(a); - // const auto& bc = static_cast(b); - // return ac.get_node().as_int() > bc.get_node().as_int(); - return false; + const auto& ac = static_cast(a); + const auto& bc = static_cast(b); + return ac.get_count() > bc.get_count(); } bool weighted() const final { return true; } diff --git a/pyproject.toml b/pyproject.toml index 290e988..1326a9f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -1,7 +1,7 @@ [build-system] requires = ["scikit-build-core >=0.4.3", "nanobind >=1.3.2", - "klaycircuits @ git+https://github.com/IbrahimElk/klay.git@ref-separation-of-concerns" + "klaycircuits @ git+https://github.com/IbrahimElk/klay.git@feat/sd-dnnf-checker" ] build-backend = "scikit_build_core.build" @@ -13,7 +13,7 @@ readme = "README.md" requires-python = ">=3.10" dependencies = [ "numpy", - "klaycircuits @ git+https://github.com/IbrahimElk/klay.git@ref-separation-of-concerns" + "klaycircuits @ git+https://github.com/IbrahimElk/klay.git@feat/sd-dnnf-checker" ] authors = [ { name = "Ibrahim El Kaddouri" }, @@ -23,6 +23,13 @@ classifiers = [ "License :: OSI Approved :: Apache Software License", ] +[project.optional-dependencies] +dev = ["nanobind >=1.3.2", + "pytest", + "torch", + "jax" +] + [project.urls] Homepage = "https://github.com/ML-KULeuven/kompyle" diff --git a/src/core.cpp b/src/core.cpp index a3e7ff0..dc37d42 100644 --- a/src/core.cpp +++ b/src/core.cpp @@ -15,12 +15,6 @@ cms_to_ganak_cl(const vector& cl) { return ganak_cl; } -NodePtr -compile_from_ganak(const std::string& cnf_file) { - auto circ = std::make_unique(); - return compile_from_ganak(circ.get(), cnf_file); -} - NodePtr compile_from_ganak( Circuit* circ, @@ -55,9 +49,13 @@ compile_from_ganak( GanakInt::CounterConfiguration conf; conf.verb = 0; conf.do_chronobt = 0; - conf.do_use_sat_solver = 0; - conf.first_restart = INT_MAX; - conf.do_buddy = 0; + // conf.first_restart = INT_MAX; + + // FIXME(Ibrahim): + // non chronological backtracking, + // see www.msoos.org/wordpress/wp-content/uploads/2025/05/ganak2.pdf + // isn't compatible yet with circuit building i'm afraid + // issue: Ganak counter(conf, fg); counter.new_vars(cnf.nVars()); diff --git a/src/core_bindings.cpp b/src/core_bindings.cpp index 32da76b..5501db5 100644 --- a/src/core_bindings.cpp +++ b/src/core_bindings.cpp @@ -12,15 +12,6 @@ namespace nb = nanobind; using namespace nb::literals; NB_MODULE(pkompyle, m) { - m.def("compile_from_ganak", - [](const std::string& cnf_file) -> NodePtr { - return compile_from_ganak(cnf_file); - }, - "cnf_file"_a, - "Compile a CNF file into a klay Circuit using Ganak." - //, nb::rv_policy::take_ownership - ); - m.def("compile_from_ganak", [](Circuit* circuit, const std::string& cnf_file) -> NodePtr { return compile_from_ganak(circuit, cnf_file); diff --git a/tests/conftest.py b/tests/conftest.py new file mode 100644 index 0000000..c1f68ff --- /dev/null +++ b/tests/conftest.py @@ -0,0 +1,220 @@ +# Copyright (c) 2026 Ibrahim El Kaddouri +# Licensed under apachev2 + +import os +import pytest + +from util import compile_inline, random_clauses, compile_file + +base_dir = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) +toy_path = os.path.join(base_dir, "assets", "toy") + + +@pytest.fixture +def pair_trivial_sat(): + pair = compile_inline(2, [[1, 2]], "trivial-sat: (x1 OR x2)") + yield pair + pair.cleanup() + + +@pytest.fixture +def pair_trivial_unsat(): + pair = compile_inline(2, [[1], [-1]], "trivial-unsat: x1 AND -x1") + yield pair + pair.cleanup() + + +@pytest.fixture +def pair_tautology(): + pair = compile_inline(3, [], "tautology: no clauses, n=3") + yield pair + pair.cleanup() + + +@pytest.fixture +def pair_xor(): + pair = compile_inline(3, [[1, 2], [-1, -2]], "x1 XOR x2, x3 free") + yield pair + pair.cleanup() + + +@pytest.fixture +def pair_exactly_one(): + clauses = [[1, 2, 3], [-1, -2], [-1, -3], [-2, -3]] + pair = compile_inline(3, clauses, "exactly one of {x1, x2, x3}") + yield pair + pair.cleanup() + + +@pytest.fixture(params=[ + # NOTE(Ibrahim): + # clause-to-variable ratio = 3 + + (1, 3, 0), + (1, 3, 1), + (2, 6, 0), + (2, 6, 1), + (3, 9, 0), + (3, 9, 1), + (4, 12, 0), + (4, 12, 1), + (5, 15, 0), + (5, 15, 1), + (6, 18, 0), + (7, 21, 0), + # (8, 24, 0), + # (9, 27, 0), + # (10, 30, 0), + # (11, 33, 0), + # (12, 36, 0), + # (20, 60, 0), + # (50, 150, 0), + + # NOTE(Ibrahim): + # small debug examples + + # (2, 2, 0), + # (2, 2, 1), + # (30, 26, 0), +]) +def pair_random(request): + n, m, seed = request.param + clauses = random_clauses(n, m, k=3, seed=seed) + pair = compile_inline(n, clauses, f"random-3cnf-n{n}-m{m}-s{seed}") + yield pair + pair.cleanup() + + +@pytest.fixture(params=[ + # NOTE(Ibrahim): + # clause-to-variable ratio = 3 + + (5, 15, 0), + (5, 15, 1), + (6, 18, 0), + (7, 21, 0), + (8, 24, 0), + (9, 27, 0), + (10, 30, 0), + (11, 33, 0), + (12, 36, 0), + (20, 60, 0), + + # # NOTE(Ibrahim): + # # small debug examples + (2, 2, 0), + (2, 2, 1), + (30, 26, 0), + (30, 90, 0), + (40, 120, 0), + (50, 150, 0), +]) +def pair_random_structure(request): + n, m, seed = request.param + clauses = random_clauses(n, m, k=3, seed=seed) + pair = compile_inline(n, clauses, f"random-3cnf-n{n}-m{m}-s{seed}") + yield pair + pair.cleanup() + + + +@pytest.fixture +def pair_toy0(): + path = os.path.join(toy_path, "toy0.cnf") + if not os.path.exists(path): + pytest.skip(f"not found: {path}") + yield compile_file(str(path), "toy0.cnf") + + +@pytest.fixture +def pair_toy1(): + path = os.path.join(toy_path, "toy1.cnf") + if not os.path.exists(path): + pytest.skip(f"not found: {path}") + yield compile_file(str(path), "toy1.cnf") + + +@pytest.fixture +def pair_unit_forced(): + clauses = [ + [1], + [-2], + [1, 2, 3], + ] + pair = compile_inline(3, clauses, "unit-forced: x1=T, x2=F, x3 free") + yield pair + pair.cleanup() + + +@pytest.fixture +def pair_unit_forced_unsat(): + clauses = [ + [1], + [-1], + ] + pair = compile_inline(1, clauses, "unit-forced-unsat: x1=T and x1=F") + yield pair + pair.cleanup() + + +@pytest.fixture +def pair_unit_chain(): + clauses = [ + [1], + [-1, 2], + [-2, 3], + ] + pair = compile_inline(3, clauses, "unit-chain: x1 -> x2 -> x3, all forced T") + yield pair + pair.cleanup() + +@pytest.fixture +def pair_unit_cascade_large(): + clauses = [] + + clauses.append([1]) + for i in range(1, 15): + clauses.append([-i, i + 1]) + + clauses.append([-19]) + clauses.append([20]) + + clauses.append([16, 17, 18]) + + pair = compile_inline(20, clauses, "unit-cascade-large") + yield pair + pair.cleanup() + +@pytest.fixture(params=[ + "pair_trivial_sat", + "pair_tautology", + "pair_xor", + "pair_exactly_one", +]) +def sat_pair(request): + yield request.getfixturevalue(request.param) + + +@pytest.fixture(params=[ + "pair_trivial_unsat", +]) +def unsat_pair(request): + yield request.getfixturevalue(request.param) + + +@pytest.fixture(params=[ + "pair_trivial_sat", + "pair_trivial_unsat", + "pair_tautology", + "pair_xor", + "pair_exactly_one", +]) +def any_pair(request): + yield request.getfixturevalue(request.param) + +@pytest.fixture(params=[ + "pair_toy0", + "pair_toy1", +]) +def pair_any_toy(request): + yield request.getfixturevalue(request.param) diff --git a/tests/test_api.py b/tests/test_api.py index 649a7ab..03609d7 100644 --- a/tests/test_api.py +++ b/tests/test_api.py @@ -1,36 +1,84 @@ -import pytest +# Copyright (c) 2026 Ibrahim El Kaddouri +# Licensed under apachev2 + import kompyle as p import klay as k -@pytest.fixture -def circuit(): - return k.Circuit() - -def test_initial_nb_nodes(circuit): - assert circuit.nb_nodes() == 0 - -def test_compile_from_ganak_into_existing_circuit(circuit): - nptr = p.compile_from_ganak(circuit, "./assets/toy/toy0.cnf") - circuit.set_root(nptr) - assert circuit.nb_nodes() > 0 - -def test_compile_from_ganak_standalone(circuit): - nptr1 = p.compile_from_ganak(circuit, "./assets/toy/toy0.cnf") - nptr2 = p.compile_from_ganak("./assets/toy/toy0.cnf") - circuit.set_root(nptr2) - assert circuit.nb_nodes() > 0 - -def test_or_node(circuit): - nptr1 = p.compile_from_ganak(circuit, "./assets/toy/toy0.cnf") - nptr2 = p.compile_from_ganak("./assets/toy/toy0.cnf") - nptr = circuit.or_node([nptr1, nptr2]) - circuit.set_root(nptr) - assert circuit.nb_nodes() > 0 - -def test_get_indices(circuit): - nptr1 = p.compile_from_ganak(circuit, "./assets/toy/toy0.cnf") - nptr2 = p.compile_from_ganak("./assets/toy/toy0.cnf") - nptr = circuit.or_node([nptr1, nptr2]) - circuit.set_root(nptr) - indices = circuit._get_indices() - assert indices is not None +class TestAPI: + def test_initial_nb_nodes(self): + circuit = k.Circuit() + assert circuit.nb_nodes() == 0 + + def test_compile_from_ganak_toy0(self): + circuit = k.Circuit() + nptr = p.compile_from_ganak(circuit, "./assets/toy/toy0.cnf") + circuit.set_root(nptr) + assert circuit.nb_nodes() > 0 # and circuit.nb_nodes() == 170 + assert circuit.nb_root_nodes() == 1 + + def test_compile_from_ganak_toy1(self): + circuit = k.Circuit() + nptr = p.compile_from_ganak(circuit, "./assets/toy/toy1.cnf") + circuit.set_root(nptr) + assert circuit.nb_nodes() > 0 # and circuit.nb_nodes() == 94 + assert circuit.nb_root_nodes() == 1 + + # NOTE(Ibrahim): + # you have to set_root before recalling + # compile_from_ganak due to arjun! + def test_or_node(self): + circuit = k.Circuit() + + nptr1 = p.compile_from_ganak(circuit, "./assets/toy/toy0.cnf") + circuit.set_root(nptr1) + nbn1 = circuit.nb_nodes() + nbrn1 = circuit.nb_root_nodes() + + nptr2 = p.compile_from_ganak(circuit, "./assets/toy/toy1.cnf") + circuit.set_root(nptr2) + nbn2 = circuit.nb_nodes() + nbrn2 = circuit.nb_root_nodes() + + nptr3 = circuit.or_node([nptr1, nptr2]) + circuit.set_root(nptr3) + nbn3 = circuit.nb_nodes() + nbrn3 = circuit.nb_root_nodes() + + # NOTE(Ibrahim): + # klay/circuit reuses nodes based on hash value! + # doesn't construct a 2nd layer circuit on top! + + assert circuit.nb_nodes() > 0 + assert nbn1 != nbn2 + assert nbn2 != nbn3 + assert nbrn1 + nbrn2 + nbrn3 == 6 + + def test_remove_unused_nodes(self): + circuit = k.Circuit() + + nptr1 = p.compile_from_ganak(circuit, "./assets/toy/toy0.cnf") + nptr2 = p.compile_from_ganak(circuit, "./assets/toy/toy1.cnf") + circuit.or_node([nptr1, nptr2]) + + circuit.remove_unused_nodes() # doesn't remove layer 0 + assert circuit.nb_nodes() == (6 * 2) + 2 + + def test_set_root(self): + circuit = k.Circuit() + + nptr1 = p.compile_from_ganak(circuit, "./assets/toy/toy0.cnf") + nptr2 = p.compile_from_ganak(circuit, "./assets/toy/toy1.cnf") + nptr3 = circuit.or_node([nptr1, nptr2]) + circuit.set_root(nptr3) + + circuit.remove_unused_nodes() # doesn't remove layer 0 + assert circuit.nb_nodes() > (6 * 2) + 2 + + def test_get_indices(self): + circuit = k.Circuit() + nptr1 = p.compile_from_ganak(circuit, "./assets/toy/toy0.cnf") + circuit.set_root(nptr1) + circuit.remove_unused_nodes() + indices = circuit._get_indices() + assert indices is not None + assert len(indices) == 2 diff --git a/tests/test_integration.py b/tests/test_integration.py new file mode 100644 index 0000000..a55ecdf --- /dev/null +++ b/tests/test_integration.py @@ -0,0 +1,35 @@ +# Copyright (c) 2026 Ibrahim El Kaddouri +# Licensed under apachev2 + +from util import assert_exhaustive_equivalence + +class TestExhaustiveEquivalence: + def test_trivial_sat(self, pair_trivial_sat): + assert_exhaustive_equivalence(pair_trivial_sat) + + def test_trivial_unsat(self, pair_trivial_unsat): + assert_exhaustive_equivalence(pair_trivial_unsat) + + def test_tautology(self, pair_tautology): + assert_exhaustive_equivalence(pair_tautology) + + def test_xor(self, pair_xor): + assert_exhaustive_equivalence(pair_xor) + + def test_exactly_one(self, pair_exactly_one): + assert_exhaustive_equivalence(pair_exactly_one) + + def test_random_cnf(self, pair_random): + assert_exhaustive_equivalence(pair_random) + + def test_toy_file(self, pair_toy0): + assert_exhaustive_equivalence(pair_toy0) + + def test_unit_forced(self, pair_unit_forced): + assert_exhaustive_equivalence(pair_unit_forced) + + def test_unit_forced_unsat(self, pair_unit_forced_unsat): + assert_exhaustive_equivalence(pair_unit_forced_unsat) + + def test_unit_chain(self, pair_unit_chain): + assert_exhaustive_equivalence(pair_unit_chain) diff --git a/tests/test_structure.py b/tests/test_structure.py new file mode 100644 index 0000000..66a3c0e --- /dev/null +++ b/tests/test_structure.py @@ -0,0 +1,87 @@ +# Copyright (c) 2026 Ibrahim El Kaddouri +# Licensed under apachev2 + +from util import assert_decomposable_and_smooth, compile_inline + +class TestCircuitStructure: + + def test_trivial_sat(self, pair_trivial_sat): + assert_decomposable_and_smooth(pair_trivial_sat.circuit, + label=pair_trivial_sat.desc) + + def test_trivial_unsat(self, pair_trivial_unsat): + assert_decomposable_and_smooth(pair_trivial_unsat.circuit, + label=pair_trivial_unsat.desc) + + def test_tautology(self, pair_tautology): + assert_decomposable_and_smooth(pair_tautology.circuit, + label=pair_tautology.desc) + + def test_xor(self, pair_xor): + assert_decomposable_and_smooth(pair_xor.circuit, + label=pair_xor.desc) + + def test_exactly_one(self, pair_exactly_one): + assert_decomposable_and_smooth(pair_exactly_one.circuit, + label=pair_exactly_one.desc) + + def test_random_cnf(self, pair_random_structure): + assert_decomposable_and_smooth(pair_random_structure.circuit, + label=pair_random_structure.desc) + + def test_toy_file(self, pair_any_toy): + assert_decomposable_and_smooth(pair_any_toy.circuit, + label=pair_any_toy.desc) + + def test_unit_clause_only(self): + pair = compile_inline(1, [[1]], "unit-clause") + assert_decomposable_and_smooth(pair.circuit, + label=pair.desc) + + # # def test_alarm(self, pair_alarm): + # # assert_decomposable_and_smooth(pair_alarm.circuit, + # # label=pair_alarm.desc) + # # + # # def test_child(self, pair_child): + # # assert_decomposable_and_smooth(pair_child.circuit, + # # label=pair_child.desc) + # # + # # def test_hailfinder(self, pair_hailfinder): + # # assert_decomposable_and_smooth(pair_hailfinder.circuit, + # # label=pair_hailfinder.desc) + # # + # # def test_munin(self, pair_munin): + # # assert_decomposable_and_smooth(pair_munin.circuit, + # # label=pair_munin.desc) + # # + # # def test_pathfinder(self, pair_pathfinder): + # # assert_decomposable_and_smooth(pair_pathfinder.circuit, + # # label=pair_pathfinder.desc) + # # + # # def test_pigs(self, pair_pigs): + # # assert_decomposable_and_smooth(pair_pigs.circuit, + # # label=pair_pigs.desc) + # + # # def test_count124(self, pair_count124): + # # assert_decomposable_and_smooth(pair_count124.circuit, + # # label=pair_count124.desc) + # # + # # def test_count153(self, pair_count153): + # # assert_decomposable_and_smooth(pair_count153.circuit, + # # label=pair_count153.desc) + + def test_unit_forced(self, pair_unit_forced): + assert_decomposable_and_smooth(pair_unit_forced.circuit, + label=pair_unit_forced.desc) + + def test_unit_forced_unsat(self, pair_unit_forced_unsat): + assert_decomposable_and_smooth(pair_unit_forced_unsat.circuit, + label=pair_unit_forced_unsat.desc) + + def test_unit_chain(self, pair_unit_chain): + assert_decomposable_and_smooth(pair_unit_chain.circuit, + label=pair_unit_chain.desc) + + def test_unit_cascade_large(self, pair_unit_cascade_large): + assert_decomposable_and_smooth(pair_unit_cascade_large.circuit, + label=pair_unit_cascade_large.desc) diff --git a/tests/util.py b/tests/util.py new file mode 100644 index 0000000..4f15724 --- /dev/null +++ b/tests/util.py @@ -0,0 +1,187 @@ +# Copyright (c) 2026 Ibrahim El Kaddouri +# Licensed under apachev2 + +import os +import random +import tempfile +import itertools + +from dataclasses import dataclass +from typing import Dict, Generator, List, Tuple + +import klay +import torch +import kompyle as p + +# =================================================================== +# CREATE EXAMPLES +# =================================================================== + +@dataclass +class FormulaCircuitPair: + cnf_path: str + n_vars: int + clauses: List[List[int]] + circuit: klay.Circuit + root: klay.NodePtr + desc: str + _tmp: bool = False + + def cleanup(self): + if self._tmp and os.path.exists(self.cnf_path): + os.unlink(self.cnf_path) + + +def write_cnf(n_vars: int, + clauses: List[List[int]]) -> str: + fd, path = tempfile.mkstemp(suffix=".cnf") + with os.fdopen(fd, "w") as f: + f.write(f"p cnf {n_vars} {len(clauses)}\n") + for cl in clauses: + f.write(" ".join(map(str, cl)) + " 0\n") + return path + + +def parse_cnf(path: str): + n_vars, clauses = 0, [] + with open(path) as f: + for line in f: + line = line.strip() + if not line or line.startswith("c"): + continue + if line.startswith("p"): + n_vars = int(line.split()[2]) + continue + lits = [int(x) for x in line.split() if x != "0"] + if lits: + clauses.append(lits) + return n_vars, clauses + + +def compile_file(cnf_path: str, + desc: str, + tmp: bool = False) -> FormulaCircuitPair: + n_vars, clauses = parse_cnf(cnf_path) + circuit = klay.Circuit() + root = p.compile_from_ganak(circuit, cnf_path) + circuit.set_root(root) + circuit.remove_unused_nodes() + return FormulaCircuitPair( + cnf_path=cnf_path, + n_vars=n_vars, + clauses=clauses, + circuit=circuit, + root=root, + desc=desc, + _tmp=tmp, + ) + + +def compile_inline(n_vars: int, + clauses: List[List[int]], + desc: str) -> FormulaCircuitPair: + path = write_cnf(n_vars, clauses) + return compile_file(path, desc, tmp=True) + + +def random_clauses(n_vars: int, + n_clauses: int, + k: int = 3, + seed: int = 0) -> List[List[int]]: + rng = random.Random(seed) + clauses = [] + for _ in range(n_clauses): + vs = rng.sample(range(1, n_vars + 1), min(k, n_vars)) + clauses.append([v * rng.choice((-1, 1)) for v in vs]) + return clauses + +# =================================================================== +# EVALUATION +# =================================================================== + +Assignment = Dict[int, bool] + +def all_assignments(n_vars: int) -> Generator[Assignment, None, None]: + for values in itertools.product([False, True], repeat=n_vars): + assignment = {} + for i in range(n_vars): + assignment[i + 1] = values[i] + yield assignment + + +def eval_formula(clauses: List[List[int]], alpha: Assignment) -> bool: + for clause in clauses: + clause_satisfied = False + + for literal in clause: + var = abs(literal) + value = alpha[var] if literal > 0 else not alpha[var] + + if value: + clause_satisfied = True + break + + if not clause_satisfied: + return False + return True + + +def eval_circuit(circuit: klay.Circuit, n_vars: int, alpha: Assignment) -> float: + pos_w = torch.tensor([1.0 if alpha[v + 1] else 0.0 for v in range(n_vars)]) + m = circuit.to_torch_module(semiring="real") + + # NOTE(Ibrahim): + # sum because circuits can have multiple roots + return float(m(pos_w).sum()) + + +def assignment_str(alpha: Assignment) -> str: + parts = [] + for v, b in sorted(alpha.items()): + value = "T" if b else "F" + parts.append(f"x{v}={value}") + return "{" + ", ".join(parts) + "}" + + +# =================================================================== +# INTEGRATION (circuit == cnf ?) +# =================================================================== + +def assert_exhaustive_equivalence(pair: FormulaCircuitPair) -> None: + mismatches: List[Tuple[Assignment, bool, bool]] = [] + for alpha in all_assignments(pair.n_vars): + f_sat = eval_formula(pair.clauses, alpha) + c_val = eval_circuit(pair.circuit, pair.n_vars, alpha) + c_sat = c_val > 0.5 + if f_sat != c_sat: + mismatches.append((alpha, f_sat, c_sat)) + + assert not mismatches, ( + f"[{pair.desc}] Exhaustive check found {len(mismatches)} disagreements:\n" + + "\n".join( + f" {assignment_str(a)}: formula={f}, circuit={c}" + for a, f, c in mismatches[:10] + ) + ) + +# =================================================================== +# STRUCTURE (smooth ?, decomposable ?) +# =================================================================== + +def assert_decomposable_and_smooth(circuit: klay.Circuit, + label: str = "") -> klay.SDNNFResult: + result = klay.check_sdnnf(circuit, max_violations=10) + # result = klay.check_decomposability(circuit, max_violations=10) + # result = klay.check_smooth(circuit, max_violations=10) + msg_prefix = f"[{label}] " if (label and ("decomp" in label)) else "" + + assert result.is_decomposable, ( + f"{msg_prefix} circuit is not decomposable.\n{result.summary()}" + ) + assert result.is_smooth, ( + f"{msg_prefix} circuit is not smooth.\n{result.summary()}" + ) + assert len(result.violations) == 0, ( + f"{msg_prefix} unexpected violations:\n{result.summary()}" + ) + return result