From 5e93c9d3e419f30eaa040fb8fbbd1a741a563340 Mon Sep 17 00:00:00 2001 From: Hendrik 'Henk' Bierlee Date: Fri, 31 Oct 2025 09:21:24 +0000 Subject: [PATCH 1/6] Expand `to_cnf` transformation using pindakaas back-end --- cpmpy/solvers/pindakaas.py | 28 ++++---- cpmpy/tools/dimacs.py | 2 +- cpmpy/transformations/to_cnf.py | 119 ++++++++++++------------------- tests/test_tocnf.py | 122 +++++++++++++++++--------------- 4 files changed, 126 insertions(+), 145 deletions(-) diff --git a/cpmpy/solvers/pindakaas.py b/cpmpy/solvers/pindakaas.py index 20540903a..9bb05bf40 100755 --- a/cpmpy/solvers/pindakaas.py +++ b/cpmpy/solvers/pindakaas.py @@ -121,6 +121,20 @@ def __init__(self, cpm_model=None, subsolver=None): def native_model(self): return self.pdk_solver + def _int2bool_user_vars(self): + # ensure all vars are known to solver + self.solver_vars(list(self.user_vars)) + + # the user vars are only the Booleans (e.g. to ensure solveAll behaves consistently) + user_vars = set() + for x in self.user_vars: + if isinstance(x, _BoolVarImpl): + user_vars.add(x) + else: + # extends set with encoding variables of `x` + user_vars.update(self.ivarmap[x.name].vars()) + return user_vars + def solve(self, time_limit=None, assumptions=None): """ Solve the encoded CPMpy model given optional time limit and assumptions, returning whether a solution was found. @@ -135,19 +149,7 @@ def solve(self, time_limit=None, assumptions=None): if time_limit is not None and time_limit <= 0: raise ValueError("Time limit must be positive") - # ensure all vars are known to solver - self.solver_vars(list(self.user_vars)) - - # the user vars are only the Booleans (e.g. to ensure solveAll behaves consistently) - user_vars = set() - for x in self.user_vars: - if isinstance(x, _BoolVarImpl): - user_vars.add(x) - else: - # extends set with encoding variables of `x` - user_vars.update(self.ivarmap[x.name].vars()) - - self.user_vars = user_vars + self.user_vars = self._int2bool_user_vars() if time_limit is not None: time_limit = timedelta(seconds=time_limit) diff --git a/cpmpy/tools/dimacs.py b/cpmpy/tools/dimacs.py index 4a3ef0d2c..1e50b9b62 100644 --- a/cpmpy/tools/dimacs.py +++ b/cpmpy/tools/dimacs.py @@ -38,7 +38,7 @@ def write_dimacs(model, fname=None): """ constraints = toplevel_list(model.constraints) - constraints = to_cnf(constraints) + constraints, _ = to_cnf(constraints) vars = get_variables(constraints) mapping = {v : i+1 for i, v in enumerate(vars)} diff --git a/cpmpy/transformations/to_cnf.py b/cpmpy/transformations/to_cnf.py index 5a03f28e2..999a32ad8 100644 --- a/cpmpy/transformations/to_cnf.py +++ b/cpmpy/transformations/to_cnf.py @@ -1,82 +1,51 @@ """ - Meta-transformation for obtaining a CNF from a list of constraints. - - Converts the logical constraints into disjuctions using the tseitin transform, - including flattening global constraints that are :func:`~cpmpy.expressions.core.Expression.is_bool()` and not in `supported`. - - .. note:: - The transformation is no longer used by the SAT solvers, and may be outdated. - Check :meth:`CPM_pysat.transform ` for an up-to-date alternative. - - Other constraints are copied verbatim so this transformation - can also be used in non-pure CNF settings. - - The implementation first converts the list of constraints - to **Flat Normal Form**, this already flattens subexpressions using - auxiliary variables. - - What is then left to do is to tseitin encode the following into CNF: - - - ``BV`` with BV a ``BoolVar`` (or ``NegBoolView``) - - ``or([BV])`` constraint - - ``and([BV])`` constraint - - ``BE != BV`` with ``BE :: BV|or()|and()|BV!=BV|BV==BV|BV->BV`` - - ``BE == BV`` - - ``BE -> BV`` - - ``BV -> BE`` +Transform constraints to **Conjunctive Normal Form** (i.e. an `and` of `or`s of literals, i.e. Boolean variables or their negation, e.g. from `x xor y` to `(x or ~y) and (~x or y)`) using a back-end encoding library and its transformation pipeline. """ -from ..expressions.core import Operator -from ..expressions.variables import _BoolVarImpl -from .reification import only_implies -from .flatten_model import flatten_constraint -def to_cnf(constraints, csemap=None): - """ - Converts all logical constraints into **Conjunctive Normal Form** +import itertools +import cpmpy as cp +import pindakaas as pdk +from ..solvers.pindakaas import CPM_pindakaas - Arguments: - constraints: list[Expression] or Operator - supported: (frozen)set of global constraint names that do not need to be decomposed - """ - fnf = flatten_constraint(constraints, csemap=csemap) - fnf = only_implies(fnf, csemap=csemap) - return flat2cnf(fnf) -def flat2cnf(constraints): +def to_cnf(constraints, csemap=None, ivarmap=None): """ - Converts from **Flat Normal Form** all logical constraints into **Conjunctive Normal Form**, - including flattening global constraints that are :func:`~cpmpy.expressions.core.Expression.is_bool()` and not in `supported`. - - What is now left to do is to tseitin encode: - - - ``BV`` with BV a ``BoolVar`` (or ``NegBoolView``) - - ``or([BV])`` constraint - - ``and([BV])`` constraint - - ``BE != BV`` with ``BE :: BV|or()|and()|BV!=BV|BV==BV|BV->BV`` - - ``BE == BV`` - - ``BE -> BV`` - - ``BV -> BE`` - - We do it in a principled way for each of the cases. (in)equalities - get transformed into implications, everything is modular. - - Arguments: - constraints: list[Expression] or Operator + Converts all constraints into **Conjunctive Normal Form** + + Arguments: + constraints: list[Expression] or Operator + csemap: `dict()` used for CSE + ivarmap: `dict()` used to map integer variables to their encoding (usefull for finding the values of the now-encoded integer variables) + Returns: + Equivalent CPMpy constraints in CNF, and the updated `ivarmap` """ - cnf = [] - for expr in constraints: - # BE -> BE - if expr.name == '->': - a0,a1 = expr.args - - # BoolVar() -> BoolVar() - if isinstance(a1, _BoolVarImpl) or \ - (isinstance(a1, Operator) and a1.name == 'or'): - cnf.append(~a0 | a1) - continue - - # all other cases added as is... - # TODO: we should raise here? is not really CNF... - cnf.append(expr) - - return cnf + slv = CPM_pindakaas() + slv.pdk_solver = pdk.CNF() + if ivarmap is not None: + slv.ivarmap = ivarmap + slv._csemap = csemap + slv += constraints + return to_cpmpy_cnf(slv), slv.ivarmap + + +def to_cpmpy_cnf(slv): + # from pdk var to cpmpy var + cpmpy_vars = {str(slv.solver_var(x).var()): x for x in slv._int2bool_user_vars()} + + def to_cpmpy_clause(clause): + for lit in clause: + x = str(lit.var()) + if x not in cpmpy_vars: + cpmpy_vars[x] = cp.boolvar() + y = cpmpy_vars[x] + if lit.is_negated(): + yield ~y + else: + yield y + + return list( + itertools.chain( + (x | ~x for x in cpmpy_vars.values()), # ensure all vars are "known" in the CNF + (cp.any(to_cpmpy_clause(clause)) for clause in slv.pdk_solver.clauses()), + ) + ) diff --git a/tests/test_tocnf.py b/tests/test_tocnf.py index eefef07bb..912eb31ae 100644 --- a/tests/test_tocnf.py +++ b/tests/test_tocnf.py @@ -1,76 +1,86 @@ import unittest -import numpy as np -from cpmpy import * -from cpmpy.solvers import CPM_ortools +import cpmpy as cp + +from cpmpy.expressions.variables import _BoolVarImpl +from cpmpy.expressions.utils import is_bool, argvals from cpmpy.transformations.to_cnf import to_cnf from cpmpy.transformations.get_variables import get_variables -from cpmpy.expressions.core import Operator from cpmpy.expressions.globalconstraints import Xor + class TestToCnf(unittest.TestCase): def test_tocnf(self): - a,b,c = boolvar(shape=3) + a, b, clause = cp.boolvar(shape=3) + x = cp.intvar(1, 2) + y, z = cp.intvar(0, 1, shape=2) - cases = [a, - a|b, - a&b, - a!=b, - a==b, - a.implies(b), - a.implies(b|c), - a.implies(b&c), - a.implies(b!=c), - a.implies(b==c), - a.implies(b.implies(c)), - (b|c).implies(a), - (b&c).implies(a), - (b!=c).implies(a), - (b==c).implies(a), - (b.implies(c)).implies(a), - Xor([a,b]), - ] + bvs = cp.boolvar(shape=3) + cases = [ + a, + a | b, + a & b, + a != b, + a == b, + a.implies(b), + a.implies(b | clause), + a.implies(b & clause), + a.implies(b != clause), + a.implies(b == clause), + a.implies(b.implies(clause)), + (b | clause).implies(a), + (b & clause).implies(a), + (b != clause).implies(a), + (b == clause).implies(a), + (b.implies(clause)).implies(a), + Xor([a, b]), + cp.sum([2 * x + 3 * y]) <= 4, + cp.sum([2 * x + 3 * y + 5 * z]) <= 6, + cp.sum([2 * cp.intvar(1, 2) + 3 * cp.intvar(0, 1)]) <= 4, + cp.sum([ 3 * cp.intvar(0,1) ]) <= 4, + (a + b + clause) == 1, + # a * b == 1, # TODO in linearization! + # a * b != 1, + (a + b + clause) != 1, + a + b + clause > 2, + a + b + clause <= 2, + cp.sum(cp.intvar(lb=2, ub=3, shape=3)) <= 3, + ] # test for equivalent solutions with/without to_cnf for case in cases: - vs = cpm_array(get_variables(case)) + vs = cp.cpm_array(get_variables(case)) s1 = self.allsols([case], vs) - s1.sort(axis=0) - s2 = self.allsols(to_cnf(case), vs) - s2.sort(axis=0) - for ss1,ss2 in zip(s1,s2): - self.assertTrue(np.all(ss1 == ss2), (case, s1, s2)) + cnf, ivarmap = to_cnf(case) - # test for errors in edge cases of to_cnf - bvs = boolvar(shape=3) - ivs = intvar(lb=2, ub=3, shape=3) - edge_cases = [ - # do not consider object as a double implcation, but as a sum - (a + b + c) == 1, - a * b == 1, - a * b != 1, - (a + b + c) != 1, - sum(bvs) > 2, - sum(bvs) <= 2, - sum(ivs) <= 3 - ] + # TODO + # assert ( + # cnf is False + # or isinstance(cnf, _BoolVarImpl) + # or cnf.name == "and" + # and all( + # clause.name == "or" + # and all([is_bool(lit) or isinstance(lit, _BoolVarImpl) for lit in clause.args]) + # for clause in cnf.args + # ) + # ), f"The following was not CNF: {cnf}" - # check for error in edge cases - for case in edge_cases: - cnf = to_cnf(case) - # Expressions should not be decomposed at the to_cnf level! - self.assertEqual(len(cnf), 1) + s2 = self.allsols(cnf, vs, ivarmap=ivarmap) + assert s1 == s2, f"The equivalence check failed for translaton from {case} to {cnf}" - def allsols(self, cons, vs): - sols = [] + def allsols(self, cons, vs, ivarmap=None): + m = cp.Model(cons) + sols = set() - m = CPM_ortools(Model(cons)) - while m.solve(): - sols.append(vs.value()) - m += ~all(vs == vs.value()) + def display(): + if ivarmap: + for x_enc in ivarmap.values(): + x_enc._x._value = x_enc.decode() + sols.add(tuple(argvals(vs))) - return np.array(sols) + m.solveAll(solver="ortools", display=display, solution_limit=100) + assert len(sols) < 100, sols + return sols -if __name__ == '__main__': +if __name__ == "__main__": unittest.main() - From 29513e6582e1056ece57253115038899cf7787fd Mon Sep 17 00:00:00 2001 From: Hendrik 'Henk' Bierlee Date: Fri, 31 Oct 2025 09:52:52 +0000 Subject: [PATCH 2/6] Minimize number of free var clauses (x | ~x) --- cpmpy/transformations/to_cnf.py | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/cpmpy/transformations/to_cnf.py b/cpmpy/transformations/to_cnf.py index 999a32ad8..3743aa3bc 100644 --- a/cpmpy/transformations/to_cnf.py +++ b/cpmpy/transformations/to_cnf.py @@ -31,6 +31,7 @@ def to_cnf(constraints, csemap=None, ivarmap=None): def to_cpmpy_cnf(slv): # from pdk var to cpmpy var cpmpy_vars = {str(slv.solver_var(x).var()): x for x in slv._int2bool_user_vars()} + free_vars = set(cpmpy_vars.values()) def to_cpmpy_clause(clause): for lit in clause: @@ -38,14 +39,15 @@ def to_cpmpy_clause(clause): if x not in cpmpy_vars: cpmpy_vars[x] = cp.boolvar() y = cpmpy_vars[x] + try: + free_vars.remove(y) + except KeyError: + pass if lit.is_negated(): yield ~y else: yield y - return list( - itertools.chain( - (x | ~x for x in cpmpy_vars.values()), # ensure all vars are "known" in the CNF - (cp.any(to_cpmpy_clause(clause)) for clause in slv.pdk_solver.clauses()), - ) - ) + clauses = [cp.any(to_cpmpy_clause(clause)) for clause in slv.pdk_solver.clauses()] + free_vars = [ (x | ~x) for x in free_vars ] # add free variables so they are "known" in the CNF + return clauses + free_vars From bca800124309c320db5cafccfadf3f79dad83936 Mon Sep 17 00:00:00 2001 From: Hendrik 'Henk' Bierlee Date: Fri, 31 Oct 2025 11:03:24 +0000 Subject: [PATCH 3/6] Bypass `pindakaas` for simple clauses --- cpmpy/solvers/pindakaas.py | 23 ++++++++++++++++++----- cpmpy/transformations/to_cnf.py | 28 +++++++++++++++++++--------- tests/test_tool_dimacs.py | 3 ++- 3 files changed, 39 insertions(+), 15 deletions(-) diff --git a/cpmpy/solvers/pindakaas.py b/cpmpy/solvers/pindakaas.py index 9bb05bf40..051731513 100755 --- a/cpmpy/solvers/pindakaas.py +++ b/cpmpy/solvers/pindakaas.py @@ -265,22 +265,33 @@ def add(self, cpm_expr_orig): __add__ = add # avoid redirect in superclass + def _add_clause(self, cpm_expr): + if not isinstance(cpm_expr, list): + raise TypeError + + self.pdk_solver.add_clause(self.solver_vars(cpm_expr)) + def _post_constraint(self, cpm_expr, conditions=[]): + if not isinstance(conditions, list): + raise TypeError + """Add a single, *transformed* constraint, implied by conditions.""" if isinstance(cpm_expr, BoolVal): # base case: Boolean value if cpm_expr.args[0] is False: - self.pdk_solver.add_clause(conditions) + self._add_clause(conditions) elif isinstance(cpm_expr, _BoolVarImpl): # (implied) literal - self.pdk_solver.add_clause(conditions + [self.solver_var(cpm_expr)]) + self._add_clause(conditions + [cpm_expr]) elif cpm_expr.name == "or": # (implied) clause - self.pdk_solver.add_clause(conditions + self.solver_vars(cpm_expr.args)) + self._add_clause(conditions + cpm_expr.args) elif cpm_expr.name == "->": # implication a0, a1 = cpm_expr.args - self._post_constraint(a1, conditions=conditions + [~self.solver_var(a0)]) + if not isinstance(a0, _BoolVarImpl): + raise TypeError + self._post_constraint(a1, conditions=conditions + [~a0]) elif isinstance(cpm_expr, Comparison): # Bool linear assert cpm_expr.name in {"<=", ">=", "=="}, ( @@ -302,7 +313,9 @@ def _post_constraint(self, cpm_expr, conditions=[]): lhs = sum(c * l for c, l in zip(coefficients, self.solver_vars(literals))) - self.pdk_solver.add_encoding(eval_comparison(cpm_expr.name, lhs, rhs), conditions=conditions) + self.pdk_solver.add_encoding( + eval_comparison(cpm_expr.name, lhs, rhs), conditions=self.solver_vars(conditions) + ) else: raise NotSupportedError(f"{self.name}: Unsupported constraint {cpm_expr}") diff --git a/cpmpy/transformations/to_cnf.py b/cpmpy/transformations/to_cnf.py index 3743aa3bc..9efa28e15 100644 --- a/cpmpy/transformations/to_cnf.py +++ b/cpmpy/transformations/to_cnf.py @@ -6,6 +6,7 @@ import cpmpy as cp import pindakaas as pdk from ..solvers.pindakaas import CPM_pindakaas +from ..transformations.get_variables import get_variables def to_cnf(constraints, csemap=None, ivarmap=None): @@ -20,20 +21,28 @@ def to_cnf(constraints, csemap=None, ivarmap=None): Equivalent CPMpy constraints in CNF, and the updated `ivarmap` """ slv = CPM_pindakaas() - slv.pdk_solver = pdk.CNF() if ivarmap is not None: slv.ivarmap = ivarmap slv._csemap = csemap - slv += constraints - return to_cpmpy_cnf(slv), slv.ivarmap + # the encoded constraints (i.e. `PB`s) will be added to this `pdk.CNF` object + slv.pdk_solver = pdk.CNF() + + # however, we bypass `pindakaas` for simple clauses + clauses = [] + slv._add_clause = lambda cpm_expr: clauses.append(cp.any(cpm_expr)) -def to_cpmpy_cnf(slv): - # from pdk var to cpmpy var + # add, transform, and encode constraints into CNF/clauses + slv += constraints + + # now we read the pdk.CNF back to cpmpy constraints by mapping from `pdk.Lit` to CPMpy lit cpmpy_vars = {str(slv.solver_var(x).var()): x for x in slv._int2bool_user_vars()} - free_vars = set(cpmpy_vars.values()) + + # if a user variable `x` does not occur in any clause, they should be added as `x | ~x` + free_vars = set(cpmpy_vars.values()) - set(get_variables(clauses)) def to_cpmpy_clause(clause): + """Lazily convert `pdk.CNF` to CPMpy.""" for lit in clause: x = str(lit.var()) if x not in cpmpy_vars: @@ -48,6 +57,7 @@ def to_cpmpy_clause(clause): else: yield y - clauses = [cp.any(to_cpmpy_clause(clause)) for clause in slv.pdk_solver.clauses()] - free_vars = [ (x | ~x) for x in free_vars ] # add free variables so they are "known" in the CNF - return clauses + free_vars + clauses += (cp.any(to_cpmpy_clause(clause)) for clause in slv.pdk_solver.clauses()) + clauses += ((x | ~x) for x in free_vars) # add free variables so they are "known" by the CNF + + return clauses, slv.ivarmap diff --git a/tests/test_tool_dimacs.py b/tests/test_tool_dimacs.py index 57e43f587..bc44f998f 100644 --- a/tests/test_tool_dimacs.py +++ b/tests/test_tool_dimacs.py @@ -60,7 +60,8 @@ def test_write_cnf(self): m += a <= 0 cnf_txt = write_dimacs(m) - gt_cnf = "p cnf 3 3\n1 2 3 0\n-2 -3 0\n-1 0\n" + # TODO note the order is slightly unexpected, because of an optimization in `to_cnf` which puts simple clauses before encoded constraints (i.e.) sums + gt_cnf = "p cnf 3 3\n1 2 3 0\n-1 0\n-2 -3 0\n" self.assertEqual(cnf_txt, gt_cnf) From d2c65329e3fa940d50960a46836afcb52076570e Mon Sep 17 00:00:00 2001 From: Hendrik 'Henk' Bierlee Date: Fri, 31 Oct 2025 11:16:22 +0000 Subject: [PATCH 4/6] Handle pindakaas dependency --- cpmpy/transformations/to_cnf.py | 9 +++++++-- tests/test_tocnf.py | 8 +++++--- tests/test_tool_dimacs.py | 4 ++++ 3 files changed, 16 insertions(+), 5 deletions(-) diff --git a/cpmpy/transformations/to_cnf.py b/cpmpy/transformations/to_cnf.py index 9efa28e15..41db5fa97 100644 --- a/cpmpy/transformations/to_cnf.py +++ b/cpmpy/transformations/to_cnf.py @@ -2,9 +2,7 @@ Transform constraints to **Conjunctive Normal Form** (i.e. an `and` of `or`s of literals, i.e. Boolean variables or their negation, e.g. from `x xor y` to `(x or ~y) and (~x or y)`) using a back-end encoding library and its transformation pipeline. """ -import itertools import cpmpy as cp -import pindakaas as pdk from ..solvers.pindakaas import CPM_pindakaas from ..transformations.get_variables import get_variables @@ -20,6 +18,13 @@ def to_cnf(constraints, csemap=None, ivarmap=None): Returns: Equivalent CPMpy constraints in CNF, and the updated `ivarmap` """ + if not CPM_pindakaas.supported(): + raise ImportError( + f"Install the Pindakaas python library `pindakaas` (e.g. `pip install pindakaas`) package to use the `to_cnf` transformation" + ) + + import pindakaas as pdk + slv = CPM_pindakaas() if ivarmap is not None: slv.ivarmap = ivarmap diff --git a/tests/test_tocnf.py b/tests/test_tocnf.py index 912eb31ae..bba40e322 100644 --- a/tests/test_tocnf.py +++ b/tests/test_tocnf.py @@ -1,13 +1,15 @@ import unittest import cpmpy as cp -from cpmpy.expressions.variables import _BoolVarImpl -from cpmpy.expressions.utils import is_bool, argvals from cpmpy.transformations.to_cnf import to_cnf from cpmpy.transformations.get_variables import get_variables from cpmpy.expressions.globalconstraints import Xor +from cpmpy.solvers.pindakaas import CPM_pindakaas +import pytest + +@pytest.mark.skipif(not CPM_pindakaas.supported(), reason="Pindakaas (required for `to_cnf`) not installed") class TestToCnf(unittest.TestCase): def test_tocnf(self): a, b, clause = cp.boolvar(shape=3) @@ -36,7 +38,7 @@ def test_tocnf(self): cp.sum([2 * x + 3 * y]) <= 4, cp.sum([2 * x + 3 * y + 5 * z]) <= 6, cp.sum([2 * cp.intvar(1, 2) + 3 * cp.intvar(0, 1)]) <= 4, - cp.sum([ 3 * cp.intvar(0,1) ]) <= 4, + cp.sum([3 * cp.intvar(0, 1)]) <= 4, (a + b + clause) == 1, # a * b == 1, # TODO in linearization! # a * b != 1, diff --git a/tests/test_tool_dimacs.py b/tests/test_tool_dimacs.py index bc44f998f..8b7c28944 100644 --- a/tests/test_tool_dimacs.py +++ b/tests/test_tool_dimacs.py @@ -7,7 +7,11 @@ from cpmpy.tools.dimacs import read_dimacs, write_dimacs from cpmpy.transformations.get_variables import get_variables_model from cpmpy.solvers.solver_interface import ExitStatus +from cpmpy.solvers.pindakaas import CPM_pindakaas + + +@pytest.mark.skipif(not CPM_pindakaas.supported(), reason="Pindakaas (required for `to_cnf`) not installed") class CNFTool(unittest.TestCase): def setUp(self) -> None: From eff0cabbb47df0f8b2c502130c822a592b37ced9 Mon Sep 17 00:00:00 2001 From: Hendrik 'Henk' Bierlee Date: Fri, 31 Oct 2025 13:14:59 +0000 Subject: [PATCH 5/6] Fix import --- tests/test_tocnf.py | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/test_tocnf.py b/tests/test_tocnf.py index bba40e322..208714242 100644 --- a/tests/test_tocnf.py +++ b/tests/test_tocnf.py @@ -1,9 +1,11 @@ import unittest import cpmpy as cp + from cpmpy.transformations.to_cnf import to_cnf from cpmpy.transformations.get_variables import get_variables from cpmpy.expressions.globalconstraints import Xor +from cpmpy.expressions.utils import argvals from cpmpy.solvers.pindakaas import CPM_pindakaas import pytest From 9635d8f7efdfac68a3ec1e0b53cfea6dd3b732e5 Mon Sep 17 00:00:00 2001 From: Hendrik 'Henk' Bierlee Date: Fri, 31 Oct 2025 18:35:15 +0000 Subject: [PATCH 6/6] Remove return of `ivarmap` --- cpmpy/tools/dimacs.py | 2 +- cpmpy/transformations/to_cnf.py | 2 +- tests/test_tocnf.py | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/cpmpy/tools/dimacs.py b/cpmpy/tools/dimacs.py index 1e50b9b62..4a3ef0d2c 100644 --- a/cpmpy/tools/dimacs.py +++ b/cpmpy/tools/dimacs.py @@ -38,7 +38,7 @@ def write_dimacs(model, fname=None): """ constraints = toplevel_list(model.constraints) - constraints, _ = to_cnf(constraints) + constraints = to_cnf(constraints) vars = get_variables(constraints) mapping = {v : i+1 for i, v in enumerate(vars)} diff --git a/cpmpy/transformations/to_cnf.py b/cpmpy/transformations/to_cnf.py index 41db5fa97..66cb3314b 100644 --- a/cpmpy/transformations/to_cnf.py +++ b/cpmpy/transformations/to_cnf.py @@ -65,4 +65,4 @@ def to_cpmpy_clause(clause): clauses += (cp.any(to_cpmpy_clause(clause)) for clause in slv.pdk_solver.clauses()) clauses += ((x | ~x) for x in free_vars) # add free variables so they are "known" by the CNF - return clauses, slv.ivarmap + return clauses diff --git a/tests/test_tocnf.py b/tests/test_tocnf.py index 208714242..efdd1048c 100644 --- a/tests/test_tocnf.py +++ b/tests/test_tocnf.py @@ -54,7 +54,8 @@ def test_tocnf(self): for case in cases: vs = cp.cpm_array(get_variables(case)) s1 = self.allsols([case], vs) - cnf, ivarmap = to_cnf(case) + ivarmap = dict() + cnf = to_cnf(case, ivarmap=ivarmap) # TODO # assert (