Coverage for /usr/lib/python3/dist-packages/sympy/assumptions/cnf.py: 27%

1"""

2The classes used here are for the internal use of assumptions system

3only and should not be used anywhere else as these do not possess the

4signatures common to SymPy objects. For general use of logic constructs

5please refer to sympy.logic classes And, Or, Not, etc.

6"""

7from itertools import combinations, product, zip_longest

8from sympy.assumptions.assume import AppliedPredicate, Predicate

9from sympy.core.relational import Eq, Ne, Gt, Lt, Ge, Le

10from sympy.core.singleton import S

11from sympy.logic.boolalg import Or, And, Not, Xnor

12from sympy.logic.boolalg import (Equivalent, ITE, Implies, Nand, Nor, Xor)

15class Literal:

16 """

17 The smallest element of a CNF object.

19 Parameters

20 ==========

22 lit : Boolean expression

24 is_Not : bool

26 Examples

27 ========

29 >>> from sympy import Q

30 >>> from sympy.assumptions.cnf import Literal

31 >>> from sympy.abc import x

32 >>> Literal(Q.even(x))

33 Literal(Q.even(x), False)

34 >>> Literal(~Q.even(x))

35 Literal(Q.even(x), True)

36 """

38 def __new__(cls, lit, is_Not=False):

39 if isinstance(lit, Not):

40 lit = lit.args[0]

41 is_Not = True

42 elif isinstance(lit, (AND, OR, Literal)):

43 return ~lit if is_Not else lit

44 obj = super().__new__(cls)

45 obj.lit = lit

46 obj.is_Not = is_Not

47 return obj

49 @property

50 def arg(self):

51 return self.lit

53 def rcall(self, expr):

54 if callable(self.lit):

55 lit = self.lit(expr)

56 else:

57 try:

58 lit = self.lit.apply(expr)

59 except AttributeError:

60 lit = self.lit.rcall(expr)

61 return type(self)(lit, self.is_Not)

63 def __invert__(self):

64 is_Not = not self.is_Not

65 return Literal(self.lit, is_Not)

67 def __str__(self):

68 return '{}({}, {})'.format(type(self).__name__, self.lit, self.is_Not)

70 __repr__ = __str__

72 def __eq__(self, other):

73 return self.arg == other.arg and self.is_Not == other.is_Not

75 def __hash__(self):

76 h = hash((type(self).__name__, self.arg, self.is_Not))

77 return h

80class OR:

81 """

82 A low-level implementation for Or

83 """

84 def __init__(self, *args):

85 self._args = args

87 @property

88 def args(self):

89 return sorted(self._args, key=str)

91 def rcall(self, expr):

92 return type(self)(*[arg.rcall(expr)

93 for arg in self._args

94 ])

96 def __invert__(self):

97 return AND(*[~arg for arg in self._args])

99 def __hash__(self):

100 return hash((type(self).__name__,) + tuple(self.args))

101

102 def __eq__(self, other):

103 return self.args == other.args

104

105 def __str__(self):

106 s = '(' + ' | '.join([str(arg) for arg in self.args]) + ')'

107 return s

108

109 __repr__ = __str__

110

111

112class AND:

113 """

114 A low-level implementation for And

115 """

116 def __init__(self, *args):

117 self._args = args

118

119 def __invert__(self):

120 return OR(*[~arg for arg in self._args])

121

122 @property

123 def args(self):

124 return sorted(self._args, key=str)

125

126 def rcall(self, expr):

127 return type(self)(*[arg.rcall(expr)

128 for arg in self._args

129 ])

130

131 def __hash__(self):

132 return hash((type(self).__name__,) + tuple(self.args))

133

134 def __eq__(self, other):

135 return self.args == other.args

136

137 def __str__(self):

138 s = '('+' & '.join([str(arg) for arg in self.args])+')'

139 return s

140

141 __repr__ = __str__

142

143

144def to_NNF(expr, composite_map=None):

145 """

146 Generates the Negation Normal Form of any boolean expression in terms

147 of AND, OR, and Literal objects.

148

149 Examples

150 ========

151

152 >>> from sympy import Q, Eq

153 >>> from sympy.assumptions.cnf import to_NNF

154 >>> from sympy.abc import x, y

155 >>> expr = Q.even(x) & ~Q.positive(x)

156 >>> to_NNF(expr)

157 (Literal(Q.even(x), False) & Literal(Q.positive(x), True))

158

159 Supported boolean objects are converted to corresponding predicates.

160

161 >>> to_NNF(Eq(x, y))

162 Literal(Q.eq(x, y), False)

163

164 If ``composite_map`` argument is given, ``to_NNF`` decomposes the

165 specified predicate into a combination of primitive predicates.

166

167 >>> cmap = {Q.nonpositive: Q.negative | Q.zero}

168 >>> to_NNF(Q.nonpositive, cmap)

169 (Literal(Q.negative, False) | Literal(Q.zero, False))

170 >>> to_NNF(Q.nonpositive(x), cmap)

171 (Literal(Q.negative(x), False) | Literal(Q.zero(x), False))

172 """

173 from sympy.assumptions.ask import Q

174

175 if composite_map is None:

176 composite_map = {}

177

178

179 binrelpreds = {Eq: Q.eq, Ne: Q.ne, Gt: Q.gt, Lt: Q.lt, Ge: Q.ge, Le: Q.le}

180 if type(expr) in binrelpreds:

181 pred = binrelpreds[type(expr)]

182 expr = pred(*expr.args)

183

184 if isinstance(expr, Not):

185 arg = expr.args[0]

186 tmp = to_NNF(arg, composite_map) # Strategy: negate the NNF of expr

187 return ~tmp

188

189 if isinstance(expr, Or):

190 return OR(*[to_NNF(x, composite_map) for x in Or.make_args(expr)])

191

192 if isinstance(expr, And):

193 return AND(*[to_NNF(x, composite_map) for x in And.make_args(expr)])

194

195 if isinstance(expr, Nand):

196 tmp = AND(*[to_NNF(x, composite_map) for x in expr.args])

197 return ~tmp

198

199 if isinstance(expr, Nor):

200 tmp = OR(*[to_NNF(x, composite_map) for x in expr.args])

201 return ~tmp

202

203 if isinstance(expr, Xor):

204 cnfs = []

205 for i in range(0, len(expr.args) + 1, 2):

206 for neg in combinations(expr.args, i):

207 clause = [~to_NNF(s, composite_map) if s in neg else to_NNF(s, composite_map)

208 for s in expr.args]

209 cnfs.append(OR(*clause))

210 return AND(*cnfs)

211

212 if isinstance(expr, Xnor):

213 cnfs = []

214 for i in range(0, len(expr.args) + 1, 2):

215 for neg in combinations(expr.args, i):

216 clause = [~to_NNF(s, composite_map) if s in neg else to_NNF(s, composite_map)

217 for s in expr.args]

218 cnfs.append(OR(*clause))

219 return ~AND(*cnfs)

220

221 if isinstance(expr, Implies):

222 L, R = to_NNF(expr.args[0], composite_map), to_NNF(expr.args[1], composite_map)

223 return OR(~L, R)

224

225 if isinstance(expr, Equivalent):

226 cnfs = []

227 for a, b in zip_longest(expr.args, expr.args[1:], fillvalue=expr.args[0]):

228 a = to_NNF(a, composite_map)

229 b = to_NNF(b, composite_map)

230 cnfs.append(OR(~a, b))

231 return AND(*cnfs)

232

233 if isinstance(expr, ITE):

234 L = to_NNF(expr.args[0], composite_map)

235 M = to_NNF(expr.args[1], composite_map)

236 R = to_NNF(expr.args[2], composite_map)

237 return AND(OR(~L, M), OR(L, R))

238

239 if isinstance(expr, AppliedPredicate):

240 pred, args = expr.function, expr.arguments

241 newpred = composite_map.get(pred, None)

242 if newpred is not None:

243 return to_NNF(newpred.rcall(*args), composite_map)

244

245 if isinstance(expr, Predicate):

246 newpred = composite_map.get(expr, None)

247 if newpred is not None:

248 return to_NNF(newpred, composite_map)

249

250 return Literal(expr)

251

252

253def distribute_AND_over_OR(expr):

254 """

255 Distributes AND over OR in the NNF expression.

256 Returns the result( Conjunctive Normal Form of expression)

257 as a CNF object.

258 """

259 if not isinstance(expr, (AND, OR)):

260 tmp = set()

261 tmp.add(frozenset((expr,)))

262 return CNF(tmp)

263

264 if isinstance(expr, OR):

265 return CNF.all_or(*[distribute_AND_over_OR(arg)

266 for arg in expr._args])

267

268 if isinstance(expr, AND):

269 return CNF.all_and(*[distribute_AND_over_OR(arg)

270 for arg in expr._args])

271

272

273class CNF:

274 """

275 Class to represent CNF of a Boolean expression.

276 Consists of set of clauses, which themselves are stored as

277 frozenset of Literal objects.

278

279 Examples

280 ========

281

282 >>> from sympy import Q

283 >>> from sympy.assumptions.cnf import CNF

284 >>> from sympy.abc import x

285 >>> cnf = CNF.from_prop(Q.real(x) & ~Q.zero(x))

286 >>> cnf.clauses

287 {frozenset({Literal(Q.zero(x), True)}),

288 frozenset({Literal(Q.negative(x), False),

289 Literal(Q.positive(x), False), Literal(Q.zero(x), False)})}

290 """

291 def __init__(self, clauses=None):

292 if not clauses:

293 clauses = set()

294 self.clauses = clauses

295

296 def add(self, prop):

297 clauses = CNF.to_CNF(prop).clauses

298 self.add_clauses(clauses)

299

300 def __str__(self):

301 s = ' & '.join(

302 ['(' + ' | '.join([str(lit) for lit in clause]) +')'

303 for clause in self.clauses]

304 )

305 return s

306

307 def extend(self, props):

308 for p in props:

309 self.add(p)

310 return self

311

312 def copy(self):

313 return CNF(set(self.clauses))

314

315 def add_clauses(self, clauses):

316 self.clauses |= clauses

317

318 @classmethod

319 def from_prop(cls, prop):

320 res = cls()

321 res.add(prop)

322 return res

323

324 def __iand__(self, other):

325 self.add_clauses(other.clauses)

326 return self

327

328 def all_predicates(self):

329 predicates = set()

330 for c in self.clauses:

331 predicates |= {arg.lit for arg in c}

332 return predicates

333

334 def _or(self, cnf):

335 clauses = set()

336 for a, b in product(self.clauses, cnf.clauses):

337 tmp = set(a)

338 for t in b:

339 tmp.add(t)

340 clauses.add(frozenset(tmp))

341 return CNF(clauses)

342

343 def _and(self, cnf):

344 clauses = self.clauses.union(cnf.clauses)

345 return CNF(clauses)

346

347 def _not(self):

348 clss = list(self.clauses)

349 ll = set()

350 for x in clss[-1]:

351 ll.add(frozenset((~x,)))

352 ll = CNF(ll)

353

354 for rest in clss[:-1]:

355 p = set()

356 for x in rest:

357 p.add(frozenset((~x,)))

358 ll = ll._or(CNF(p))

359 return ll

360

361 def rcall(self, expr):

362 clause_list = []

363 for clause in self.clauses:

364 lits = [arg.rcall(expr) for arg in clause]

365 clause_list.append(OR(*lits))

366 expr = AND(*clause_list)

367 return distribute_AND_over_OR(expr)

368

369 @classmethod

370 def all_or(cls, *cnfs):

371 b = cnfs[0].copy()

372 for rest in cnfs[1:]:

373 b = b._or(rest)

374 return b

375

376 @classmethod

377 def all_and(cls, *cnfs):

378 b = cnfs[0].copy()

379 for rest in cnfs[1:]:

380 b = b._and(rest)

381 return b

382

383 @classmethod

384 def to_CNF(cls, expr):

385 from sympy.assumptions.facts import get_composite_predicates

386 expr = to_NNF(expr, get_composite_predicates())

387 expr = distribute_AND_over_OR(expr)

388 return expr

389

390 @classmethod

391 def CNF_to_cnf(cls, cnf):

392 """

393 Converts CNF object to SymPy's boolean expression

394 retaining the form of expression.

395 """

396 def remove_literal(arg):

397 return Not(arg.lit) if arg.is_Not else arg.lit

398

399 return And(*(Or(*(remove_literal(arg) for arg in clause)) for clause in cnf.clauses))

400

401

402class EncodedCNF:

403 """

404 Class for encoding the CNF expression.

405 """

406 def __init__(self, data=None, encoding=None):

407 if not data and not encoding:

408 data = []

409 encoding = {}

410 self.data = data

411 self.encoding = encoding

412 self._symbols = list(encoding.keys())

413

414 def from_cnf(self, cnf):

415 self._symbols = list(cnf.all_predicates())

416 n = len(self._symbols)

417 self.encoding = dict(zip(self._symbols, range(1, n + 1)))

418 self.data = [self.encode(clause) for clause in cnf.clauses]

419

420 @property

421 def symbols(self):

422 return self._symbols

423

424 @property

425 def variables(self):

426 return range(1, len(self._symbols) + 1)

427

428 def copy(self):

429 new_data = [set(clause) for clause in self.data]

430 return EncodedCNF(new_data, dict(self.encoding))

431

432 def add_prop(self, prop):

433 cnf = CNF.from_prop(prop)

434 self.add_from_cnf(cnf)

435

436 def add_from_cnf(self, cnf):

437 clauses = [self.encode(clause) for clause in cnf.clauses]

438 self.data += clauses

439

440 def encode_arg(self, arg):

441 literal = arg.lit

442 value = self.encoding.get(literal, None)

443 if value is None:

444 n = len(self._symbols)

445 self._symbols.append(literal)

446 value = self.encoding[literal] = n + 1

447 if arg.is_Not:

448 return -value

449 else:

450 return value

451

452 def encode(self, clause):

453 return {self.encode_arg(arg) if not arg.lit == S.false else 0 for arg in clause}