diff --git a/hipaasat/__init__.py b/hipaasat/__init__.py index b794fd4..f2bceb7 100644 --- a/hipaasat/__init__.py +++ b/hipaasat/__init__.py @@ -1 +1,5 @@ +"""""" + __version__ = '0.1.0' + +from . import cnf diff --git a/hipaasat/cnf.py b/hipaasat/cnf.py new file mode 100644 index 0000000..7c7af6f --- /dev/null +++ b/hipaasat/cnf.py @@ -0,0 +1,277 @@ +from collections import OrderedDict +from enum import Enum + +from typing import Any, Dict, Iterable, Iterator, List, Optional, Set + +__all__ = [ + "check_clause_consistency", + "check_at_most_one_clause_consistency", + "check_consistency", + "check_or_clause_consistency", + "Clause", + "ClauseType", + "CNF", + "Literal", + "simplify", +] + +class Literal(object): + def __init__(self, name: str, negated: bool = False, assignment: bool = None) -> None: + self._name = name + self._negated = negated + self._assignment = assignment + + def __eq__(self, other: Any) -> bool: + if isinstance(self, Literal): + return ( + self.name == other.name and + self.negated == other.negated and + self.assignment == other.assignment + ) + return NotImplemented + + @property + def name(self) -> str: + return self._name + + @property + def negated(self) -> bool: + return self._negated + + @property + def assignment(self) -> Optional[bool]: + return self._assignment + + @property + def value(self) -> Optional[bool]: + if self.assignment is None: + return None + return self.negated ^ self.assignment + + def assign(self, value: bool, inplace: bool = False) -> "Literal": + if inplace: + self._assignment = value + ret = self + else: + ret = Literal(self.name, self.negated, value) + return ret + + def copy(self) -> "Literal": + return Literal(self.name, self.negated, self.assignment) + + def is_assigned(self) -> bool: + return self._assignment is not None + + def make_false(self, inplace: bool = False) -> "Literal": + return self.assign(self.negated & True, inplace=inplace) + + def make_true(self, inplace: bool = False) -> "Literal": + return self.assign(self.negated ^ True, inplace=inplace) + +class ClauseType(Enum): + AT_MOST_ONE = "AtMostOne" + OR = "OR" + +class Clause(object): + def __init__(self, clause_type: ClauseType, literals: Iterable[Literal]) -> None: + seen: Set[str] = set() + for lit in literals: + if lit.name in seen: + raise ValueError("Two or more literals with the same name") + seen.add(lit.name) + + self._clause_type = clause_type + self._literals = OrderedDict([(lit.name, lit) for lit in literals]) + self._assigned: Dict[str, Literal] = {lit.name: lit for lit in self._literals.values() if lit.is_assigned()} + self._unassigned: Dict[str, Literal] = {lit.name: lit for lit in self._literals.values() if not lit.is_assigned()} + + def __eq__(self, other: Any) -> bool: + if isinstance(other, Clause): + equal = self.type == other.type + for lit in self: + other_lit = other.get_literal(lit.name) + equal &= lit == other_lit + return equal + return NotImplemented + + def __iter__(self) -> Iterator[Literal]: + return iter(self._literals.values()) + + def __len__(self) -> int: + return len(self._literals) + + @property + def type(self) -> ClauseType: + return self._clause_type + + def assign(self, name: str, value: bool, inplace: bool = False) -> "Clause": + if inplace: + lit = self._literals.get(name) + if lit: + lit.assign(value, inplace=True) + if lit.name in self._unassigned: + del self._unassigned[lit.name] + self._assigned[lit.name] = lit + ret = self + else: + literals = (lit.assign(value, inplace=False) if lit.name == name else lit for lit in self._literals.values()) + ret = Clause(self.type, literals) + return ret + + def assigned_literal_count(self) -> int: + return len(self._assigned) + + def copy(self) -> "Clause": + return Clause(self.type, self._literals.values()) + + def get_literal(self, name: str) -> Optional[Literal]: + return self._literals.get(name) + + def get_assigned_literals(self) -> List[Literal]: + return list(self._assigned.values()) + + def get_unassigned_literals(self) -> List[Literal]: + return list(self._unassigned.values()) + + def remove_literal(self, name: str, inplace: bool = False) -> "Clause": + if inplace: + self._literals.pop(name, None) + self._assigned.pop(name, None) + self._unassigned.pop(name, None) + ret = self + else: + literals = (lit for lit in self._literals.values() if lit.name != name) + ret = Clause(self.type, literals) + return ret + + def unassigned_literal_count(self) -> int: + return len(self._unassigned) + +def check_clause_consistency(clause: Clause) -> Optional[bool]: + if clause.type == ClauseType.AT_MOST_ONE: + return check_at_most_one_clause_consistency(clause) + elif clause.type == ClauseType.OR: + return check_or_clause_consistency(clause) + else: + raise ValueError("unknown clause type {}".format(clause.type)) + +def check_at_most_one_clause_consistency(clause: Clause) -> Optional[bool]: + if clause.type != ClauseType.AT_MOST_ONE: + raise ValueError("clause must be of type {}".format(ClauseType.AT_MOST_ONE)) + count = 0 + incomplete = False + for lit in clause: + if lit.value is None: + incomplete = True + else: + count += lit.value + if count > 1: + return False + return None if incomplete else True + +def check_or_clause_consistency(clause: Clause) -> Optional[bool]: + if clause.type != ClauseType.OR: + raise ValueError("clause must be of type {}".format(ClauseType.OR)) + incomplete = False + for lit in clause: + if lit.value is None: + incomplete = True + elif lit.value: + return True + return None if incomplete else False + +class CNF(object): + def __init__(self, clauses: Iterable[Clause]) -> None: + self._clauses = list(clauses) + + def __iter__(self) -> Iterator[Clause]: + return iter(self._clauses) + + def __len__(self) -> int: + return len(self._clauses) + + def assign(self, name: str, value: bool, inplace: bool = False) -> "CNF": + if inplace: + for c in self: + c.assign(name, value, inplace=True) + ret = self + else: + clone = self.copy() + clone.assign(name, value, inplace=True) + ret = clone + return ret + + def assigned_literal_count(self) -> int: + names: Set[str] = set() + for c in self: + for lit in c.get_assigned_literals(): + names.add(lit.name) + return len(names) + + def copy(self) -> "CNF": + return CNF(self._clauses) + + def get_literal(self, name: str) -> Optional[Literal]: + duplicates: List[Literal] = [] + for c in self: + lit = c.get_literal(name) + if lit: + duplicates.append(lit) + + exemplar = duplicates.pop() + while duplicates: + for lit in duplicates: + assert exemplar.assignment == lit.assignment + exemplar = duplicates.pop() + + return exemplar + + def unique_literal_count(self) -> int: + names: Set[str] = set() + for c in self: + for lit in c: + names.add(lit.name) + return len(names) + +def check_consistency(cnf: CNF) -> Optional[bool]: + result = True + incomplete = False + for c in cnf: + r = check_clause_consistency(c) + if r is None: + incomplete = True + else: + result &= r + if not result: + # no need to check any of the remaining clauses as this clause is empty + # and thus the whole statement is inconsistent + return False + return None if incomplete else True + +def simplify(cnf: CNF, inplace: bool = False) -> Optional[CNF]: + if inplace: + ret = _simplify_inplace(cnf) + else: + clone = cnf.copy() + ret = _simplify_inplace(clone) + return ret + +def _simplify_inplace(cnf: CNF) -> Optional[CNF]: + unit_clauses = [c for c in cnf if c.unassigned_literal_count() == 1] + while unit_clauses: + clause = unit_clauses.pop(0) + literals = clause.get_unassigned_literals() + assert len(literals) == 1 + + literal = literals[0] + literal.make_true(inplace=True) + + assert literal.assignment is not None + for c in cnf: + c.assign(literal.name, literal.assignment, inplace=True) + consistent = check_consistency(cnf) + if consistent == False: + return None + + unit_clauses = [c for c in cnf if c.unassigned_literal_count() == 1] + return cnf diff --git a/pyproject.lock b/pyproject.lock index adebb66..9d9825e 100644 --- a/pyproject.lock +++ b/pyproject.lock @@ -1,3 +1,21 @@ +[[package]] +category = "dev" +description = "An abstract syntax tree for Python with inference support." +name = "astroid" +optional = false +platform = "*" +python-versions = ">=3.4.*" +version = "2.0.4" + +[package.dependencies] +lazy-object-proxy = "*" +six = "*" +wrapt = "*" + +[package.dependencies.typed-ast] +python = "<3.7" +version = "*" + [[package]] category = "dev" description = "Atomic file writes." @@ -28,6 +46,33 @@ version = "0.3.9" [package.requirements] platform = "win32" +[[package]] +category = "dev" +description = "A Python utility / library to sort Python imports." +name = "isort" +optional = false +platform = "*" +python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*" +version = "4.3.4" + +[[package]] +category = "dev" +description = "A fast and thorough lazy object proxy." +name = "lazy-object-proxy" +optional = false +platform = "*" +python-versions = "*" +version = "1.3.1" + +[[package]] +category = "dev" +description = "McCabe checker, plugin for flake8" +name = "mccabe" +optional = false +platform = "*" +python-versions = "*" +version = "0.6.1" + [[package]] category = "dev" description = "More routines for operating on iterables, beyond itertools" @@ -85,6 +130,24 @@ platform = "unix" python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*" version = "1.6.0" +[[package]] +category = "dev" +description = "python code static checker" +name = "pylint" +optional = false +platform = "*" +python-versions = ">=3.4.*" +version = "2.1.1" + +[package.dependencies] +astroid = ">=2.0.0" +isort = ">=4.2.5" +mccabe = "*" + +[package.dependencies.colorama] +platform = "win32" +version = "*" + [[package]] category = "dev" description = "pytest: simple powerful testing with Python" @@ -138,21 +201,36 @@ platform = "*" python-versions = "*" version = "3.6.6" +[[package]] +category = "dev" +description = "Module for decorators, wrappers and monkey patching." +name = "wrapt" +optional = false +platform = "*" +python-versions = "*" +version = "1.10.11" + [metadata] -content-hash = "1344a8a8baed479c70c20d350281038cc233461884bf33e812f387237f75e185" +content-hash = "aa4883df225e0afd3ff4dac8c53e587577165056ea6688f1a6ab5c7899725ba8" platform = "*" python-versions = "^3.5" [metadata.hashes] +astroid = ["292fa429e69d60e4161e7612cb7cc8fa3609e2e309f80c224d93a76d5e7b58be", "c7013d119ec95eb626f7a2011f0b63d0c9a095df9ad06d8507b37084eada1a8d"] atomicwrites = ["0312ad34fcad8fac3704d441f7b317e50af620823353ec657a53e981f92920c0", "ec9ae8adaae229e4f8446952d204a3e4b5fdd2d099f9be3aaf556120135fb3ee"] attrs = ["10cbf6e27dbce8c30807caf056c8eb50917e0eaafe86347671b57254006c3e69", "ca4be454458f9dec299268d472aaa5a11f67a4ff70093396e1ceae9c76cf4bbb"] colorama = ["463f8483208e921368c9f306094eb6f725c6ca42b0f97e313cb5d5512459feda", "48eb22f4f8461b1df5734a074b57042430fb06e1d61bd1e11b078c0fe6d7a1f1"] +isort = ["1153601da39a25b14ddc54955dbbacbb6b2d19135386699e2ad58517953b34af", "b9c40e9750f3d77e6e4d441d8b0266cf555e7cdabdcff33c4fd06366ca761ef8", "ec9ef8f4a9bc6f71eec99e1806bfa2de401650d996c59330782b89a5555c1497"] +lazy-object-proxy = ["0ce34342b419bd8f018e6666bfef729aec3edf62345a53b537a4dcc115746a33", "1b668120716eb7ee21d8a38815e5eb3bb8211117d9a90b0f8e21722c0758cc39", "209615b0fe4624d79e50220ce3310ca1a9445fd8e6d3572a896e7f9146bbf019", "27bf62cb2b1a2068d443ff7097ee33393f8483b570b475db8ebf7e1cba64f088", "27ea6fd1c02dcc78172a82fc37fcc0992a94e4cecf53cb6d73f11749825bd98b", "2c1b21b44ac9beb0fc848d3993924147ba45c4ebc24be19825e57aabbe74a99e", "2df72ab12046a3496a92476020a1a0abf78b2a7db9ff4dc2036b8dd980203ae6", "320ffd3de9699d3892048baee45ebfbbf9388a7d65d832d7e580243ade426d2b", "50e3b9a464d5d08cc5227413db0d1c4707b6172e4d4d915c1c70e4de0bbff1f5", "5276db7ff62bb7b52f77f1f51ed58850e315154249aceb42e7f4c611f0f847ff", "61a6cf00dcb1a7f0c773ed4acc509cb636af2d6337a08f362413c76b2b47a8dd", "6ae6c4cb59f199d8827c5a07546b2ab7e85d262acaccaacd49b62f53f7c456f7", "7661d401d60d8bf15bb5da39e4dd72f5d764c5aff5a86ef52a042506e3e970ff", "7bd527f36a605c914efca5d3d014170b2cb184723e423d26b1fb2fd9108e264d", "7cb54db3535c8686ea12e9535eb087d32421184eacc6939ef15ef50f83a5e7e2", "7f3a2d740291f7f2c111d86a1c4851b70fb000a6c8883a59660d95ad57b9df35", "81304b7d8e9c824d058087dcb89144842c8e0dea6d281c031f59f0acf66963d4", "933947e8b4fbe617a51528b09851685138b49d511af0b6c0da2539115d6d4514", "94223d7f060301b3a8c09c9b3bc3294b56b2188e7d8179c762a1cda72c979252", "ab3ca49afcb47058393b0122428358d2fbe0408cf99f1b58b295cfeb4ed39109", "bd6292f565ca46dee4e737ebcc20742e3b5be2b01556dafe169f6c65d088875f", "cb924aa3e4a3fb644d0c463cad5bc2572649a6a3f68a7f8e4fbe44aaa6d77e4c", "d0fc7a286feac9077ec52a927fc9fe8fe2fabab95426722be4c953c9a8bede92", "ddc34786490a6e4ec0a855d401034cbd1242ef186c20d79d2166d6a4bd449577", "e34b155e36fa9da7e1b7c738ed7767fc9491a62ec6af70fe9da4a057759edc2d", "e5b9e8f6bda48460b7b143c3821b21b452cb3a835e6bbd5dd33aa0c8d3f5137d", "e81ebf6c5ee9684be8f2c87563880f93eedd56dd2b6146d8a725b50b7e5adb0f", "eb91be369f945f10d3a49f5f9be8b3d0b93a4c2be8f8a5b83b0571b8123e0a7a", "f460d1ceb0e4a5dcb2a652db0904224f367c9b3c1470d5a7683c0480e582468b"] +mccabe = ["ab8a6258860da4b6677da4bd2fe5dc2c659cff31b3ee4f7f5d64e79735b80d42", "dd8d182285a0fe56bace7f45b5e7d1a6ebcbf524e8f3bd87eb0f125271b8831f"] more-itertools = ["c187a73da93e7a8acc0001572aebc7e3c69daf7bf6881a2cea10650bd4420092", "c476b5d3a34e12d40130bc2f935028b5f636df8f372dc2c1c01dc19681b2039e", "fcbfeaea0be121980e15bc97b3817b5202ca73d0eae185b4550cbfce2a3ebb3d"] mypy = ["673ea75fb750289b7d1da1331c125dc62fc1c3a8db9129bb372ae7b7d5bf300a", "c770605a579fdd4a014e9f0a34b6c7a36ce69b08100ff728e96e27445cef3b3c"] pathlib2 = ["8eb170f8d0d61825e09a95b38be068299ddeda82f35e96c3301a8a5e7604cb83", "d1aa2a11ba7b8f7b21ab852b1fb5afb277e1bb99d5dfc663380b5015c0d80c5a"] pluggy = ["6e3836e39f4d36ae72840833db137f7b7d35105079aee6ec4a62d9f80d594dd1", "95eb8364a4708392bae89035f45341871286a333f749c3141c20573d2b3876e1"] py = ["06a30435d058473046be836d3fc4f27167fd84c45b99704f2fb5509ef61f9af1", "50402e9d1c9005d759426988a492e0edaadb7f4e68bcddfea586bc7432d009c6"] +pylint = ["1d6d3622c94b4887115fe5204982eee66fdd8a951cf98635ee5caee6ec98c3ec", "31142f764d2a7cd41df5196f9933b12b7ee55e73ef12204b648ad7e556c119fb"] pytest = ["2d7c49e931316cc7d1638a3e5f54f5d7b4e5225972b3c9838f3584788d27f349", "ad0c7db7b5d4081631e0155f5c61b80ad76ce148551aaafe3a718d65a7508b18"] six = ["70e8a77beed4562e7f14fe23a786b54f6296e34344c23bc42f07b15018ff98e9", "832dc0e10feb1aa2c68dcc57dbb658f1c7e65b9b61af69048abc87a2db00a0eb"] typed-ast = ["0948004fa228ae071054f5208840a1e88747a357ec1101c17217bfe99b299d58", "10703d3cec8dcd9eef5a630a04056bbc898abc19bac5691612acba7d1325b66d", "1f6c4bd0bdc0f14246fd41262df7dfc018d65bb05f6e16390b7ea26ca454a291", "25d8feefe27eb0303b73545416b13d108c6067b846b543738a25ff304824ed9a", "29464a177d56e4e055b5f7b629935af7f49c196be47528cc94e0a7bf83fbc2b9", "2e214b72168ea0275efd6c884b114ab42e316de3ffa125b267e732ed2abda892", "3e0d5e48e3a23e9a4d1a9f698e32a542a4a288c871d33ed8df1b092a40f3a0f9", "519425deca5c2b2bdac49f77b2c5625781abbaf9a809d727d3a5596b30bb4ded", "57fe287f0cdd9ceaf69e7b71a2e94a24b5d268b35df251a88fef5cc241bf73aa", "668d0cec391d9aed1c6a388b0d5b97cd22e6073eaa5fbaa6d2946603b4871efe", "68ba70684990f59497680ff90d18e756a47bf4863c604098f10de9716b2c0bdd", "6de012d2b166fe7a4cdf505eee3aaa12192f7ba365beeefaca4ec10e31241a85", "79b91ebe5a28d349b6d0d323023350133e927b4de5b651a8aa2db69c761420c6", "8550177fa5d4c1f09b5e5f524411c44633c80ec69b24e0e98906dd761941ca46", "898f818399cafcdb93cbbe15fc83a33d05f18e29fb498ddc09b0214cdfc7cd51", "94b091dc0f19291adcb279a108f5d38de2430411068b219f41b343c03b28fb1f", "a26863198902cda15ab4503991e8cf1ca874219e0118cbf07c126bce7c4db129", "a8034021801bc0440f2e027c354b4eafd95891b573e12ff0418dec385c76785c", "bc978ac17468fe868ee589c795d06777f75496b1ed576d308002c8a5756fb9ea", "c05b41bc1deade9f90ddc5d988fe506208019ebba9f2578c622516fd201f5863", "c9b060bd1e5a26ab6e8267fd46fc9e02b54eb15fffb16d112d4c7b1c12987559", "edb04bdd45bfd76c8292c4d9654568efaedf76fe78eb246dde69bdb13b2dad87", "f19f2a4f547505fe9072e15f6f4ae714af51b5a681a97f187971f50c283193b6"] typing = ["4027c5f6127a6267a435201981ba156de91ad0d1d98e9ddc2aa173453453492d", "57dcf675a99b74d64dacf6fba08fb17cf7e3d5fdff53d4a30ea2a5e7e52543d4", "a4c8473ce11a65999c8f59cb093e70686b6c84c98df58c1dae9b3b196089858a"] +wrapt = ["d4d560d479f2c21e1b5443bbd15fe7ec4b37fe7e53d335d3b9b0a7b1226fe3c6"] diff --git a/pyproject.toml b/pyproject.toml index b083c3a..f59ef7f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -6,9 +6,10 @@ authors = ["Miller Wilt "] readme = "README.md" [tool.poetry.dependencies] -python = "^3.5" +python = "^3.6" typing = "^3.6" [tool.poetry.dev-dependencies] pytest = "^3.0" mypy = "^0.620.0" +pylint = "^2.1" diff --git a/tests/test_cnf.py b/tests/test_cnf.py new file mode 100644 index 0000000..9291d72 --- /dev/null +++ b/tests/test_cnf.py @@ -0,0 +1,191 @@ +import pytest + +from hipaasat.cnf import check_consistency, check_clause_consistency, Clause, ClauseType, CNF, Literal + +def test_or_clause_consistency_single_literal(): + oc = Clause(ClauseType.OR, [ + Literal("test") + ]) + assert check_clause_consistency(oc) is None + + oc = Clause(ClauseType.OR, [ + Literal("test", assignment=True) + ]) + assert check_clause_consistency(oc) + + oc = Clause(ClauseType.OR, [ + Literal("test", assignment=False) + ]) + assert check_clause_consistency(oc) == False + + oc = Clause(ClauseType.OR, [ + Literal("test", negated=True, assignment=False) + ]) + assert check_clause_consistency(oc) + + oc = Clause(ClauseType.OR, [ + Literal("test", negated=True, assignment=True) + ]) + assert check_clause_consistency(oc) == False + +def test_or_clause_consistency_multiple_literals(): + oc = Clause(ClauseType.OR, [ + Literal("1"), Literal("2") + ]) + assert check_clause_consistency(oc) is None + + oc = Clause(ClauseType.OR, [ + Literal("1", assignment=True), Literal("2") + ]) + assert check_clause_consistency(oc) + + oc = Clause(ClauseType.OR, [ + Literal("1", assignment=False), Literal("2", assignment=True) + ]) + assert check_clause_consistency(oc) + + oc = Clause(ClauseType.OR, [ + Literal("1", negated=True, assignment=False), Literal("2", assignment=True) + ]) + assert check_clause_consistency(oc) + + oc = Clause(ClauseType.OR, [ + Literal("1", negated=True, assignment=False), Literal("2", assignment=False), Literal("3", assignment=False) + ]) + assert check_clause_consistency(oc) + + oc = Clause(ClauseType.OR, [ + Literal("1", assignment=False), Literal("2", assignment=False), Literal("3", assignment=False) + ]) + assert check_clause_consistency(oc) == False + + lits = [Literal(str(i), assignment=False) for i in range(100)] + lits.append(Literal(name="100", negated=True, assignment=False)) + oc = Clause(ClauseType.OR, lits) + assert check_clause_consistency(oc) + +def test_at_most_one_single_literal(): + amo = Clause(ClauseType.AT_MOST_ONE, [ + Literal("1") + ]) + assert check_clause_consistency(amo) is None + + amo = Clause(ClauseType.AT_MOST_ONE, [ + Literal("1", assignment=True) + ]) + assert check_clause_consistency(amo) + + amo = Clause(ClauseType.AT_MOST_ONE, [ + Literal("1", assignment=False) + ]) + assert check_clause_consistency(amo) + +def test_at_most_one_multiple_literals(): + amo = Clause(ClauseType.AT_MOST_ONE, [ + Literal("1"), Literal("2", assignment=True), Literal("3") + ]) + assert check_clause_consistency(amo) is None + + amo = Clause(ClauseType.AT_MOST_ONE, [ + Literal("1", assignment=False), Literal("2", assignment=False), Literal("3", assignment=False) + ]) + assert check_clause_consistency(amo) + + amo = Clause(ClauseType.AT_MOST_ONE, [ + Literal("1", assignment=False), Literal("2", assignment=False), Literal("3", assignment=True) + ]) + assert check_clause_consistency(amo) + + amo = Clause(ClauseType.AT_MOST_ONE, [ + Literal("1", assignment=False), Literal("2", assignment=True), Literal("3", assignment=True) + ]) + assert check_clause_consistency(amo) == False + + amo = Clause(ClauseType.AT_MOST_ONE, [ + Literal("1", assignment=True), Literal("2", assignment=True), Literal("3", assignment=True) + ]) + assert check_clause_consistency(amo) == False + +def test_cnf_single_clause(): + oc = Clause(ClauseType.OR, [ + Literal("1"), Literal("2") + ]) + cnf = CNF([oc]) + assert check_consistency(cnf) is None + + oc = Clause(ClauseType.OR, [ + Literal("test", assignment=True) + ]) + cnf = CNF([oc]) + assert check_consistency(cnf) + + oc = Clause(ClauseType.OR, [ + Literal("test", assignment=False) + ]) + cnf = CNF([oc]) + assert check_consistency(cnf) == False + + oc = Clause(ClauseType.OR, [ + Literal("test", negated=True, assignment=False) + ]) + cnf = CNF([oc]) + assert check_consistency(cnf) + + oc = Clause(ClauseType.OR, [ + Literal("test", negated=True, assignment=True) + ]) + cnf = CNF([oc]) + assert check_consistency(cnf) == False + +def test_cnf_multiple_clauses(): + cnf = CNF([ + Clause(ClauseType.OR, [ + Literal("1"), Literal("2") + ]), + Clause(ClauseType.OR, [ + Literal("2", assignment=True), Literal("3", assignment=True) + ]), + Clause(ClauseType.OR, [ + Literal("4", assignment=True), Literal("5", assignment=True) + ]) + ]) + assert check_consistency(cnf) is None + + cnf = CNF([ + Clause(ClauseType.OR, [ + Literal("1", assignment=True), Literal("2", assignment=True) + ]), + Clause(ClauseType.OR, [ + Literal("2", assignment=True), Literal("3", assignment=True) + ]), + Clause(ClauseType.OR, [ + Literal("4", assignment=True), Literal("5", assignment=True) + ]) + ]) + assert check_consistency(cnf) + + cnf = CNF([ + Clause(ClauseType.OR, [ + Literal("1", assignment=False), Literal("2", assignment=False) + ]), + Clause(ClauseType.OR, [ + Literal("2", assignment=False), Literal("3", assignment=True) + ]), + Clause(ClauseType.OR, [ + Literal("4", assignment=True), Literal("5", assignment=True) + ]) + ]) + assert check_consistency(cnf) == False + + cnf = CNF([ + Clause(ClauseType.OR, [ + Literal("1"), Literal("2", assignment=True) + ]), + Clause(ClauseType.OR, [ + Literal("2", assignment=False), Literal("3", assignment=False) + ]), + Clause(ClauseType.OR, [ + Literal("4", assignment=True), Literal("5", assignment=True) + ]) + ]) + assert check_consistency(cnf) == False