Coverage for /usr/lib/python3/dist-packages/sympy/assumptions/ask.py: 41%

1"""Module for querying SymPy objects about assumptions."""

3from sympy.assumptions.assume import (global_assumptions, Predicate,

4 AppliedPredicate)

5from sympy.assumptions.cnf import CNF, EncodedCNF, Literal

6from sympy.core import sympify

7from sympy.core.kind import BooleanKind

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

9from sympy.logic.inference import satisfiable

10from sympy.utilities.decorator import memoize_property

11from sympy.utilities.exceptions import (sympy_deprecation_warning,

12 SymPyDeprecationWarning,

13 ignore_warnings)

16# Memoization is necessary for the properties of AssumptionKeys to

17# ensure that only one object of Predicate objects are created.

18# This is because assumption handlers are registered on those objects.

21class AssumptionKeys:

22 """

23 This class contains all the supported keys by ``ask``.

24 It should be accessed via the instance ``sympy.Q``.

26 """

28 # DO NOT add methods or properties other than predicate keys.

29 # SAT solver checks the properties of Q and use them to compute the

30 # fact system. Non-predicate attributes will break this.

32 @memoize_property

33 def hermitian(self):

34 from .handlers.sets import HermitianPredicate

35 return HermitianPredicate()

37 @memoize_property

38 def antihermitian(self):

39 from .handlers.sets import AntihermitianPredicate

40 return AntihermitianPredicate()

42 @memoize_property

43 def real(self):

44 from .handlers.sets import RealPredicate

45 return RealPredicate()

47 @memoize_property

48 def extended_real(self):

49 from .handlers.sets import ExtendedRealPredicate

50 return ExtendedRealPredicate()

52 @memoize_property

53 def imaginary(self):

54 from .handlers.sets import ImaginaryPredicate

55 return ImaginaryPredicate()

57 @memoize_property

58 def complex(self):

59 from .handlers.sets import ComplexPredicate

60 return ComplexPredicate()

62 @memoize_property

63 def algebraic(self):

64 from .handlers.sets import AlgebraicPredicate

65 return AlgebraicPredicate()

67 @memoize_property

68 def transcendental(self):

69 from .predicates.sets import TranscendentalPredicate

70 return TranscendentalPredicate()

72 @memoize_property

73 def integer(self):

74 from .handlers.sets import IntegerPredicate

75 return IntegerPredicate()

77 @memoize_property

78 def rational(self):

79 from .handlers.sets import RationalPredicate

80 return RationalPredicate()

82 @memoize_property

83 def irrational(self):

84 from .handlers.sets import IrrationalPredicate

85 return IrrationalPredicate()

87 @memoize_property

88 def finite(self):

89 from .handlers.calculus import FinitePredicate

90 return FinitePredicate()

92 @memoize_property

93 def infinite(self):

94 from .handlers.calculus import InfinitePredicate

95 return InfinitePredicate()

97 @memoize_property

98 def positive_infinite(self):

99 from .handlers.calculus import PositiveInfinitePredicate

100 return PositiveInfinitePredicate()

101

102 @memoize_property

103 def negative_infinite(self):

104 from .handlers.calculus import NegativeInfinitePredicate

105 return NegativeInfinitePredicate()

106

107 @memoize_property

108 def positive(self):

109 from .handlers.order import PositivePredicate

110 return PositivePredicate()

111

112 @memoize_property

113 def negative(self):

114 from .handlers.order import NegativePredicate

115 return NegativePredicate()

116

117 @memoize_property

118 def zero(self):

119 from .handlers.order import ZeroPredicate

120 return ZeroPredicate()

121

122 @memoize_property

123 def extended_positive(self):

124 from .handlers.order import ExtendedPositivePredicate

125 return ExtendedPositivePredicate()

126

127 @memoize_property

128 def extended_negative(self):

129 from .handlers.order import ExtendedNegativePredicate

130 return ExtendedNegativePredicate()

131

132 @memoize_property

133 def nonzero(self):

134 from .handlers.order import NonZeroPredicate

135 return NonZeroPredicate()

136

137 @memoize_property

138 def nonpositive(self):

139 from .handlers.order import NonPositivePredicate

140 return NonPositivePredicate()

141

142 @memoize_property

143 def nonnegative(self):

144 from .handlers.order import NonNegativePredicate

145 return NonNegativePredicate()

146

147 @memoize_property

148 def extended_nonzero(self):

149 from .handlers.order import ExtendedNonZeroPredicate

150 return ExtendedNonZeroPredicate()

151

152 @memoize_property

153 def extended_nonpositive(self):

154 from .handlers.order import ExtendedNonPositivePredicate

155 return ExtendedNonPositivePredicate()

156

157 @memoize_property

158 def extended_nonnegative(self):

159 from .handlers.order import ExtendedNonNegativePredicate

160 return ExtendedNonNegativePredicate()

161

162 @memoize_property

163 def even(self):

164 from .handlers.ntheory import EvenPredicate

165 return EvenPredicate()

166

167 @memoize_property

168 def odd(self):

169 from .handlers.ntheory import OddPredicate

170 return OddPredicate()

171

172 @memoize_property

173 def prime(self):

174 from .handlers.ntheory import PrimePredicate

175 return PrimePredicate()

176

177 @memoize_property

178 def composite(self):

179 from .handlers.ntheory import CompositePredicate

180 return CompositePredicate()

181

182 @memoize_property

183 def commutative(self):

184 from .handlers.common import CommutativePredicate

185 return CommutativePredicate()

186

187 @memoize_property

188 def is_true(self):

189 from .handlers.common import IsTruePredicate

190 return IsTruePredicate()

191

192 @memoize_property

193 def symmetric(self):

194 from .handlers.matrices import SymmetricPredicate

195 return SymmetricPredicate()

196

197 @memoize_property

198 def invertible(self):

199 from .handlers.matrices import InvertiblePredicate

200 return InvertiblePredicate()

201

202 @memoize_property

203 def orthogonal(self):

204 from .handlers.matrices import OrthogonalPredicate

205 return OrthogonalPredicate()

206

207 @memoize_property

208 def unitary(self):

209 from .handlers.matrices import UnitaryPredicate

210 return UnitaryPredicate()

211

212 @memoize_property

213 def positive_definite(self):

214 from .handlers.matrices import PositiveDefinitePredicate

215 return PositiveDefinitePredicate()

216

217 @memoize_property

218 def upper_triangular(self):

219 from .handlers.matrices import UpperTriangularPredicate

220 return UpperTriangularPredicate()

221

222 @memoize_property

223 def lower_triangular(self):

224 from .handlers.matrices import LowerTriangularPredicate

225 return LowerTriangularPredicate()

226

227 @memoize_property

228 def diagonal(self):

229 from .handlers.matrices import DiagonalPredicate

230 return DiagonalPredicate()

231

232 @memoize_property

233 def fullrank(self):

234 from .handlers.matrices import FullRankPredicate

235 return FullRankPredicate()

236

237 @memoize_property

238 def square(self):

239 from .handlers.matrices import SquarePredicate

240 return SquarePredicate()

241

242 @memoize_property

243 def integer_elements(self):

244 from .handlers.matrices import IntegerElementsPredicate

245 return IntegerElementsPredicate()

246

247 @memoize_property

248 def real_elements(self):

249 from .handlers.matrices import RealElementsPredicate

250 return RealElementsPredicate()

251

252 @memoize_property

253 def complex_elements(self):

254 from .handlers.matrices import ComplexElementsPredicate

255 return ComplexElementsPredicate()

256

257 @memoize_property

258 def singular(self):

259 from .predicates.matrices import SingularPredicate

260 return SingularPredicate()

261

262 @memoize_property

263 def normal(self):

264 from .predicates.matrices import NormalPredicate

265 return NormalPredicate()

266

267 @memoize_property

268 def triangular(self):

269 from .predicates.matrices import TriangularPredicate

270 return TriangularPredicate()

271

272 @memoize_property

273 def unit_triangular(self):

274 from .predicates.matrices import UnitTriangularPredicate

275 return UnitTriangularPredicate()

276

277 @memoize_property

278 def eq(self):

279 from .relation.equality import EqualityPredicate

280 return EqualityPredicate()

281

282 @memoize_property

283 def ne(self):

284 from .relation.equality import UnequalityPredicate

285 return UnequalityPredicate()

286

287 @memoize_property

288 def gt(self):

289 from .relation.equality import StrictGreaterThanPredicate

290 return StrictGreaterThanPredicate()

291

292 @memoize_property

293 def ge(self):

294 from .relation.equality import GreaterThanPredicate

295 return GreaterThanPredicate()

296

297 @memoize_property

298 def lt(self):

299 from .relation.equality import StrictLessThanPredicate

300 return StrictLessThanPredicate()

301

302 @memoize_property

303 def le(self):

304 from .relation.equality import LessThanPredicate

305 return LessThanPredicate()

306

307

308Q = AssumptionKeys()

309

310def _extract_all_facts(assump, exprs):

311 """

312 Extract all relevant assumptions from *assump* with respect to given *exprs*.

313

314 Parameters

315 ==========

316

317 assump : sympy.assumptions.cnf.CNF

318

319 exprs : tuple of expressions

320

321 Returns

322 =======

323

324 sympy.assumptions.cnf.CNF

325

326 Examples

327 ========

328

329 >>> from sympy import Q

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

331 >>> from sympy.assumptions.ask import _extract_all_facts

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

333 >>> assump = CNF.from_prop(Q.positive(x) & Q.integer(y))

334 >>> exprs = (x,)

335 >>> cnf = _extract_all_facts(assump, exprs)

336 >>> cnf.clauses

337 {frozenset({Literal(Q.positive, False)})}

338

339 """

340 facts = set()

341

342 for clause in assump.clauses:

343 args = []

344 for literal in clause:

345 if isinstance(literal.lit, AppliedPredicate) and len(literal.lit.arguments) == 1:

346 if literal.lit.arg in exprs:

347 # Add literal if it has matching in it

348 args.append(Literal(literal.lit.function, literal.is_Not))

349 else:

350 # If any of the literals doesn't have matching expr don't add the whole clause.

351 break

352 else:

353 if args:

354 facts.add(frozenset(args))

355 return CNF(facts)

356

357

358def ask(proposition, assumptions=True, context=global_assumptions):

359 """

360 Function to evaluate the proposition with assumptions.

361

362 Explanation

363 ===========

364

365 This function evaluates the proposition to ``True`` or ``False`` if

366 the truth value can be determined. If not, it returns ``None``.

367

368 It should be discerned from :func:`~.refine()` which, when applied to a

369 proposition, simplifies the argument to symbolic ``Boolean`` instead of

370 Python built-in ``True``, ``False`` or ``None``.

371

372 **Syntax**

373

374 * ask(proposition)

375 Evaluate the *proposition* in global assumption context.

376

377 * ask(proposition, assumptions)

378 Evaluate the *proposition* with respect to *assumptions* in

379 global assumption context.

380

381 Parameters

382 ==========

383

384 proposition : Boolean

385 Proposition which will be evaluated to boolean value. If this is

386 not ``AppliedPredicate``, it will be wrapped by ``Q.is_true``.

387

388 assumptions : Boolean, optional

389 Local assumptions to evaluate the *proposition*.

390

391 context : AssumptionsContext, optional

392 Default assumptions to evaluate the *proposition*. By default,

393 this is ``sympy.assumptions.global_assumptions`` variable.

394

395 Returns

396 =======

397

398 ``True``, ``False``, or ``None``

399

400 Raises

401 ======

402

403 TypeError : *proposition* or *assumptions* is not valid logical expression.

404

405 ValueError : assumptions are inconsistent.

406

407 Examples

408 ========

409

410 >>> from sympy import ask, Q, pi

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

412 >>> ask(Q.rational(pi))

413 False

414 >>> ask(Q.even(x*y), Q.even(x) & Q.integer(y))

415 True

416 >>> ask(Q.prime(4*x), Q.integer(x))

417 False

418

419 If the truth value cannot be determined, ``None`` will be returned.

420

421 >>> print(ask(Q.odd(3*x))) # cannot determine unless we know x

422 None

423

424 ``ValueError`` is raised if assumptions are inconsistent.

425

426 >>> ask(Q.integer(x), Q.even(x) & Q.odd(x))

427 Traceback (most recent call last):

428 ...

429 ValueError: inconsistent assumptions Q.even(x) & Q.odd(x)

430

431 Notes

432 =====

433

434 Relations in assumptions are not implemented (yet), so the following

435 will not give a meaningful result.

436

437 >>> ask(Q.positive(x), x > 0)

438

439 It is however a work in progress.

440

441 See Also

442 ========

443

444 sympy.assumptions.refine.refine : Simplification using assumptions.

445 Proposition is not reduced to ``None`` if the truth value cannot

446 be determined.

447 """

448 from sympy.assumptions.satask import satask

449

450 proposition = sympify(proposition)

451 assumptions = sympify(assumptions)

452

453 if isinstance(proposition, Predicate) or proposition.kind is not BooleanKind:

454 raise TypeError("proposition must be a valid logical expression")

455

456 if isinstance(assumptions, Predicate) or assumptions.kind is not BooleanKind:

457 raise TypeError("assumptions must be a valid logical expression")

458

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

460 if isinstance(proposition, AppliedPredicate):

461 key, args = proposition.function, proposition.arguments

462 elif proposition.func in binrelpreds:

463 key, args = binrelpreds[type(proposition)], proposition.args

464 else:

465 key, args = Q.is_true, (proposition,)

466

467 # convert local and global assumptions to CNF

468 assump_cnf = CNF.from_prop(assumptions)

469 assump_cnf.extend(context)

470

471 # extract the relevant facts from assumptions with respect to args

472 local_facts = _extract_all_facts(assump_cnf, args)

473

474 # convert default facts and assumed facts to encoded CNF

475 known_facts_cnf = get_all_known_facts()

476 enc_cnf = EncodedCNF()

477 enc_cnf.from_cnf(CNF(known_facts_cnf))

478 enc_cnf.add_from_cnf(local_facts)

479

480 # check the satisfiability of given assumptions

481 if local_facts.clauses and satisfiable(enc_cnf) is False:

482 raise ValueError("inconsistent assumptions %s" % assumptions)

483

484 # quick computation for single fact

485 res = _ask_single_fact(key, local_facts)

486 if res is not None:

487 return res

488

489 # direct resolution method, no logic

490 res = key(*args)._eval_ask(assumptions)

491 if res is not None:

492 return bool(res)

493

494 # using satask (still costly)

495 res = satask(proposition, assumptions=assumptions, context=context)

496 return res

497

498

499def _ask_single_fact(key, local_facts):

500 """

501 Compute the truth value of single predicate using assumptions.

502

503 Parameters

504 ==========

505

506 key : sympy.assumptions.assume.Predicate

507 Proposition predicate.

508

509 local_facts : sympy.assumptions.cnf.CNF

510 Local assumption in CNF form.

511

512 Returns

513 =======

514

515 ``True``, ``False`` or ``None``

516

517 Examples

518 ========

519

520 >>> from sympy import Q

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

522 >>> from sympy.assumptions.ask import _ask_single_fact

523

524 If prerequisite of proposition is rejected by the assumption,

525 return ``False``.

526

527 >>> key, assump = Q.zero, ~Q.zero

528 >>> local_facts = CNF.from_prop(assump)

529 >>> _ask_single_fact(key, local_facts)

530 False

531 >>> key, assump = Q.zero, ~Q.even

532 >>> local_facts = CNF.from_prop(assump)

533 >>> _ask_single_fact(key, local_facts)

534 False

535

536 If assumption implies the proposition, return ``True``.

537

538 >>> key, assump = Q.even, Q.zero

539 >>> local_facts = CNF.from_prop(assump)

540 >>> _ask_single_fact(key, local_facts)

541 True

542

543 If proposition rejects the assumption, return ``False``.

544

545 >>> key, assump = Q.even, Q.odd

546 >>> local_facts = CNF.from_prop(assump)

547 >>> _ask_single_fact(key, local_facts)

548 False

549 """

550 if local_facts.clauses:

551

552 known_facts_dict = get_known_facts_dict()

553

554 if len(local_facts.clauses) == 1:

555 cl, = local_facts.clauses

556 if len(cl) == 1:

557 f, = cl

558 prop_facts = known_facts_dict.get(key, None)

559 prop_req = prop_facts[0] if prop_facts is not None else set()

560 if f.is_Not and f.arg in prop_req:

561 # the prerequisite of proposition is rejected

562 return False

563

564 for clause in local_facts.clauses:

565 if len(clause) == 1:

566 f, = clause

567 prop_facts = known_facts_dict.get(f.arg, None) if not f.is_Not else None

568 if prop_facts is None:

569 continue

570

571 prop_req, prop_rej = prop_facts

572 if key in prop_req:

573 # assumption implies the proposition

574 return True

575 elif key in prop_rej:

576 # proposition rejects the assumption

577 return False

578

579 return None

580

581

582def register_handler(key, handler):

583 """

584 Register a handler in the ask system. key must be a string and handler a

585 class inheriting from AskHandler.

586

587 .. deprecated:: 1.8.

588 Use multipledispatch handler instead. See :obj:`~.Predicate`.

589

590 """

591 sympy_deprecation_warning(

592 """

593 The AskHandler system is deprecated. The register_handler() function

594 should be replaced with the multipledispatch handler of Predicate.

595 """,

596 deprecated_since_version="1.8",

597 active_deprecations_target='deprecated-askhandler',

598 )

599 if isinstance(key, Predicate):

600 key = key.name.name

601 Qkey = getattr(Q, key, None)

602 if Qkey is not None:

603 Qkey.add_handler(handler)

604 else:

605 setattr(Q, key, Predicate(key, handlers=[handler]))

606

607

608def remove_handler(key, handler):

609 """

610 Removes a handler from the ask system.

611

612 .. deprecated:: 1.8.

613 Use multipledispatch handler instead. See :obj:`~.Predicate`.

614

615 """

616 sympy_deprecation_warning(

617 """

618 The AskHandler system is deprecated. The remove_handler() function

619 should be replaced with the multipledispatch handler of Predicate.

620 """,

621 deprecated_since_version="1.8",

622 active_deprecations_target='deprecated-askhandler',

623 )

624 if isinstance(key, Predicate):

625 key = key.name.name

626 # Don't show the same warning again recursively

627 with ignore_warnings(SymPyDeprecationWarning):

628 getattr(Q, key).remove_handler(handler)

629

630

631from sympy.assumptions.ask_generated import (get_all_known_facts,

632 get_known_facts_dict)