Complex

Abstract Syntax Trees

Attention

The classes in this module are not intended to be used directly by the user. Instead, one should use Terms and AtomicFormulas.

ASTs and Visitors

Abstract syntax trees for complex expressions.

class logic1.theories.Complex.ast.AST

Bases: ABC

Abstract base class for all AST nodes that implements basic functionality. AST nodes can be constructed using the constructors of the subclasses or using arithmetic operators.

>>> ast = Re(Add(Var('z'), Mul(Rat(2), _I())))
>>> ast
Re(Add(Var('z'), Mul(Rat(mpq(2,1)), _I())))
>>> print(ast)
Re(z + 2 * i)

>>> z = Var('z')
>>> ast = (Im(z) - I)**2
>>> ast
Pow(Add(Im(Var('z')), Neg(_I())), 2)
>>> print(ast)
(Im(z) - i)^2

See also

Rat, _I, Var, Add, Mul, Neg, Pow, Re, Im, Conj

property op: type[Self]

The operation of this AST node, which is just the class of this node.

>>> z = Var('z')
>>> z.op
<class 'logic1.theories.Complex.ast.Var'>

property args: tuple[object, ...]

The arguments of this AST node. This should be overridden by subclasses to return the appropriate arguments so that self == self.op(*self.args).

>>> z = Var('z')
>>> z.args
('z',)
>>> z.op(*z.args)
Var('z')

__add__(other: int | float | Fraction | mpq | complex | AST) → Add

Construct an addition node from this AST node and another AST node or number.

>>> z = Var('z')
>>> z + 2
Add(Var('z'), Rat(mpq(2,1)))

__eq__(other: object) → bool

Comparison of two AST nodes based on SortKey.

abstractmethod __init__(*args: object) → None

This abstract base class is not supposed to have instances itself.

__invert__() → Conj

Construct a conjugation node from this AST node.

>>> z = Var('z')
>>> ~z
Conj(Var('z'))

__le__(other: AST) → bool

Comparison of two AST nodes based on SortKey.

__mul__(other: int | float | Fraction | mpq | complex | AST) → Mul

Construct a multiplication node from this AST node and another AST node or number.

>>> z = Var('z')
>>> z * 2
Mul(Var('z'), Rat(mpq(2,1)))

__neg__() → Neg

Construct a negation node from this AST node.

>>> z = Var('z')
>>> -z
Neg(Var('z'))

__pow__(other: int) → Pow

Construct a power node from this AST node and an exponent.

>>> z = Var('z')
>>> z ** 2
Pow(Var('z'), 2)

__repr__() → str

Return a string representation of this AST node that can be evaluated to reconstruct the node. For a more human-readable string representation, use __str__() or as_latex().

>>> z = Var('z')
>>> repr(z + 2)
"Add(Var('z'), Rat(mpq(2,1)))"

__str__() → str

Return a human-readable string representation of this AST node.

>>> z = Var('z')
>>> str(Add(z, Rat(mpq(2))))
'z + 2'

__sub__(other: int | float | Fraction | mpq | complex | AST) → Add

Construct an addition node from this AST node and the negation of another AST node or number.

>>> z = Var('z')
>>> z - 2
Add(Var('z'), Neg(Rat(mpq(2,1))))

__truediv__(other: int | float | Fraction | mpq | complex | AST) → AST

Construct an AST node representing the division of this AST node by another AST node or number. Division is defined as multiplication by the inverse. Raise a ValueError if the other AST node is not constant.

>>> z = Var('z')
>>> z / 2
Mul(Var('z'), Rat(mpq(1,2)))
>>> print(z / (1 + I))
z * (1/2 + -1/2 * i)
>>> I / z
Traceback (most recent call last):
  ...
ValueError: Cannot divide by a non-constant AST node

__xor__(other: Never) → AST

Raise a NotImplementedError because the ** operator should be used for constructing power nodes instead. See __pow__().

abstractmethod accept(visitor: ASTVisitor[α]) → α

Accept an AST visitor.

as_latex() → str

Return a LaTeX representation of this AST node.

>>> z = Var('z')
>>> (z + 2 * I).as_latex()
'z + 2 i'

eval() → tuple[mpq, mpq]

Evaluate this AST node as a complex number and return the real and imaginary part. Raise a ValueError if the AST node is not constant.

>>> (2 * I).eval()
(mpq(0,1), mpq(2,1))
>>> z = Var('z')
>>> (z + 1).eval()
Traceback (most recent call last):
  ...
ValueError: Cannot evaluate variable z

factors() → list[AST]

Return a list of factors of this AST node, where each factor is a AST node that is not a multiplication.

>>> z = Var('z')
>>> (2 * z * I).factors()
[Rat(mpq(2,1)), Var('z'), _I()]
>>> (z + 1).factors()
[Add(Var('z'), Rat(mpq(1,1)))]

static from_real_imag(real: mpq, imag: mpq) → AST

Construct an AST node from given real and imaginary parts.

>>> AST.from_real_imag(mpq(2), mpq(-1))
Add(Rat(mpq(2,1)), Neg(_I()))

static from_number(value: int | float | Fraction | mpq | complex) → AST

Construct an AST node from a given Number. Raise a ValueError if the given value is not a number.

>>> AST.from_number(3.5)
Rat(mpq(7,2))
>>> AST.from_number(2 + 3j)
Add(Rat(mpq(2,1)), Mul(Rat(mpq(3,1)), _I()))
>>> AST.from_number("x")
Traceback (most recent call last):
  ...
ValueError: expected one of int, float, Fraction, mpq, complex; x is <class 'str'>

is_constant() → bool

Return True if this AST node is constant.

>>> z = Var('z')
>>> (z + 2).is_constant()
False
>>> (2 * I).is_constant()
True

is_variable() → bool

Return True if this AST node is a variable.

>>> z = Var('z')
>>> (z + 2).is_variable()
False
>>> z.is_variable()
True
>>> I.is_variable()
False

is_zero() → bool

Return True if this AST node is the rational number zero.

>>> z = Var('z')
>>> (z + 2).is_zero()
False
>>> Rat(0).is_zero()
True

sort_key() → SortKey[Self]

A sort key suitable for comparing AST nodes.

>>> z = Var('z')
>>> z.sort_key() < (z + 1).sort_key()
True

subs(sigma: Mapping[Var, int | float | Fraction | mpq | complex | AST]) → AST

Formal substitution of variables in this AST node according to the given mapping.

>>> a, b = Var('a'), Var('b')
>>> (a + 2).subs({a: I})
Add(_I(), Rat(mpq(2,1)))
>>> (a + b).subs({a: 3, b: a})
Add(Rat(mpq(3,1)), Var('a'))

class logic1.theories.Complex.ast.MonoidalOperation

Bases: AST

Abstract base class for monoidal operations, i.e. associative operations with identity element. Implements parts of the abstract class AST for the subclasses Add and Mul.

identity: ClassVar[AST]

The identity element of this operation. This should be overridden by subclasses.

property args: tuple[AST, ...]

The arguments of this AST node.

>>> Add(Rat(1), Rat(2)).args
(Rat(mpq(1,1)), Rat(mpq(2,1)))

abstractmethod __init__(*args: AST) → None

Initialize this monoidal operation with the given arguments. If any of the arguments is itself a monoidal operation of the same type, then the argument is flattened. This abstract class is not supposed to have instances itself.

static __new__(cls, *args: AST)

Create a new instance of this monoidal operation with the given arguments. If no arguments are given, return the identity element. If only one argument is given, return that argument.

>>> x = Var('x')
>>> Add(x)
Var('x')
>>> Add()
Rat(mpq(0,1))

class logic1.theories.Complex.ast.UnaryOperation

Bases: AST

Abstract base class for unary operations, i.e. operations with only one argument. Implements parts of the abstract class AST for the subclasses Neg, Conj, Re and Im.

property args: tuple[AST]

Tuple containing the single argument of this AST node.

abstractmethod __init__(arg: AST) → None

Initialize this unary operation with the given argument. This abstract class is not supposed to have instances itself.

arg: AST

The single argument of this AST node.

class logic1.theories.Complex.ast.Rat

Bases: AST

Non-negative rational number node. Negative rational numbers are automatically represented by a Neg node. Implements the abstract class AST.

>>> Rat(2)
Rat(mpq(2,1))
>>> Rat(1.5)
Rat(mpq(3,2))
>>> Rat(-1)
Neg(Rat(mpq(1,1)))

property args: tuple[mpq]

Tuple containing the value of this node.

>>> Rat(2).args
(mpq(2,1),)

__init__(value: int | float | Fraction | mpq) → None

Initialize this node with the given value. The value must be non-negative, otherwise this node is represented by a negation via __new__().

>>> Rat(2)
Rat(mpq(2,1))

value: mpq

The value of this node.

static __new__(cls, value: int | float | Fraction | mpq)

Create a new instance of Rat from the given value. If the value is negative, create an instance of Neg instead.

>>> Rat(2)
Rat(mpq(2,1))
>>> Rat(-2)
Neg(Rat(mpq(2,1)))

accept(visitor: ASTVisitor[α]) → α

Implements the abstract method AST.accept().

class logic1.theories.Complex.ast._I

Bases: AST

Imaginary unit node. This is a singleton class and the only instance is I. Implements the abstract class AST.

>>> I
_I()

property args: tuple[()]

The imaginary unit has no arguments.

>>> I.args
()

__init__() → None

This class is a singleton, so the constructor is private and should not be called directly.

accept(visitor: ASTVisitor[α]) → α

Implements the abstract method AST.accept().

static __new__(cls)

Create a new instance of _I. This is a singleton class, so this method always returns the same instance.

>>> _I()
_I()
>>> _I() is _I()
True

logic1.theories.Complex.ast.I: Final[_I] = _I()

The singleton instance of the imaginary unit.

class logic1.theories.Complex.ast.Var

Bases: AST

Variable node. Implements the abstract class AST.

>>> z = Var('z')
>>> z
Var('z')

property args: tuple[str]

A tuple containing the name of this variable.

>>> Var('z').args
('z',)

__init__(name: str) → None

Initialize this variable with the given name.

>>> z = Var('z')
>>> z
Var('z')

name: str

The name of this variable.

accept(visitor: ASTVisitor[α]) → α

Implements the abstract method AST.accept().

class logic1.theories.Complex.ast.Add

Bases: MonoidalOperation

Addition node. Implements the abstract class MonoidalOperation.

>>> z = Var('z')
>>> z + 1 + I
Add(Var('z'), Rat(mpq(1,1)), _I())

identity: ClassVar[Rat] = Rat(mpq(0,1))

The identity element of addition, which is the rational number \(0\).

__init__(*args: AST) → None

Initialize this addition node with the given arguments. If any of the arguments is itself an addition node, then the argument is flattened. If zero or one argument is given, the identity element or the argument itself is returned by MonoidalOperation.__new__().

>>> z = Var('z')
>>> Add(z, Rat(1), I)
Add(Var('z'), Rat(mpq(1,1)), _I())
>>> Add(z, Add(Rat(1), I))
Add(Var('z'), Rat(mpq(1,1)), _I())
>>> Add(z)
Var('z')
>>> Add()
Rat(mpq(0,1))

accept(visitor: ASTVisitor[α]) → α

Implements the abstract method AST.accept().

class logic1.theories.Complex.ast.Mul

Bases: MonoidalOperation

Multiplication node. Implements the abstract class MonoidalOperation.

>>> z = Var('z')
>>> z * I * 2
Mul(Var('z'), _I(), Rat(mpq(2,1)))

identity: ClassVar[Rat] = Rat(mpq(1,1))

The identity element of multiplication, which is the rational number $1$.

__init__(*args: AST) → None

Initialize this multiplication node with the given arguments. If any of the arguments is itself a multiplication node, then the argument is flattened. If zero or one argument is given, the identity element or the argument itself is returned by MonoidalOperation.__new__().

>>> z = Var('z')
>>> Mul(z, Rat(2), I)
Mul(Var('z'), Rat(mpq(2,1)), _I())
>>> Mul(z, Mul(Rat(2), I))
Mul(Var('z'), Rat(mpq(2,1)), _I())
>>> Mul(z)
Var('z')
>>> Mul()
Rat(mpq(1,1))

accept(visitor: ASTVisitor[α]) → α

Implements the abstract method AST.accept().

class logic1.theories.Complex.ast.Pow

Bases: AST

Power node. Implements the abstract class AST.

>>> z = Var('z')
>>> z ** 2
Pow(Var('z'), 2)

property args: tuple[AST, int]

Tuple containing the base and the exponent of this power node.

>>> (I ** 2).args
(_I(), 2)

__init__(base: AST, exponent: int) → None

Initialize this power node with the given base and exponent. Raise a TypeError if the exponent is negative.

>>> z = Var('z')
>>> Pow(z, 2)
Pow(Var('z'), 2)
>>> Pow(z, -1)
Traceback (most recent call last):
  ...
TypeError: Exponent must be a non-negative integer

base: AST

The base of this power node.

exponent: int

The exponent of this power node. Must be a non-negative integer.

accept(visitor: ASTVisitor[α]) → α

Implements the abstract method AST.accept().

class logic1.theories.Complex.ast.Neg

Bases: UnaryOperation

Negation node. Implements the abstract class UnaryOperation.

>>> z = Var('z')
>>> -z
Neg(Var('z'))

__init__(arg: AST) → None

Initialize this negation node with the given argument.

>>> z = Var('z')
>>> Neg(z)
Neg(Var('z'))

accept(visitor: ASTVisitor[α]) → α

Implements the abstract method AST.accept().

class logic1.theories.Complex.ast.Conj

Bases: UnaryOperation

Complex conjugation node. Implements the abstract class UnaryOperation.

>>> z = Var('z')
>>> ~z
Conj(Var('z'))

__init__(arg: AST) → None

Initialize this conjugation node with the given argument.

>>> z = Var('z')
>>> Conj(z)
Conj(Var('z'))

accept(visitor: ASTVisitor[α]) → α

Implements the abstract method AST.accept().

class logic1.theories.Complex.ast.Re

Bases: UnaryOperation

Real part node. Implements the abstract class UnaryOperation.

>>> z = Var('z')
>>> Re(z)
Re(Var('z'))

__init__(arg: AST) → None

Initialize this real part node with the given argument.

>>> z = Var('z')
>>> Re(z)
Re(Var('z'))

accept(visitor: ASTVisitor[α]) → α

Implements the abstract method AST.accept().

class logic1.theories.Complex.ast.Im

Bases: UnaryOperation

Imaginary part node. Implements the abstract class UnaryOperation.

>>> z = Var('z')
>>> Im(z)
Im(Var('z'))

__init__(arg: AST) → None

Initialize this imaginary part node with the given argument.

>>> z = Var('z')
>>> Im(z)
Im(Var('z'))

accept(visitor: ASTVisitor[α]) → α

Implements the abstract method AST.accept().

class logic1.theories.Complex.ast.ASTVisitor

Bases: ABC, Generic[α]

Abstract visitor for AST nodes used to implement various operations on AST nodes.

See also

• IdentityASTVisitor, VariableSubstitutor,

• normalize.ArithmeticEvaluator, normalize.ConstantEvaluator, normalize.WeakNormalizer, normalize.Normalizer, normalize.ConjugateNormalizer

• format.ReprFormatter, format.StrFormatter, format.LatexFormatter

• qe.RCF_Evaluator

abstractmethod visit_rat(num: Rat) → α

Visit a rational number.

abstractmethod visit_i(i: _I) → α

Visit the imaginary unit.

abstractmethod visit_var(var: Var) → α

Visit a variable.

abstractmethod visit_add(add: Add) → α

Visit an addition node.

abstractmethod visit_mul(mul: Mul) → α

Visit a multiplication node.

abstractmethod visit_pow(pow: Pow) → α

Visit a power node.

abstractmethod visit_neg(neg: Neg) → α

Visit a negation node.

abstractmethod visit_conj(conj: Conj) → α

Visit a conjugation node.

abstractmethod visit_re(re: Re) → α

Visit a real part node.

abstractmethod visit_im(im: Im) → α

Visit an imaginary part node.

class logic1.theories.Complex.ast.IdentityASTVisitor

Bases: ASTVisitor[AST]

Visitor that returns the same AST node, but with all children visited. Useful as a base class for other visitors.

>>> z = Var('z')
>>> (z + 1).accept(IdentityASTVisitor())
Add(Var('z'), Rat(mpq(1,1)))

visit_rat(num: Rat) → AST

Return the same rational number. Implements the abstract method ASTVisitor.visit_rat().

>>> IdentityASTVisitor().visit_rat(Rat(mpq(2,1)))
Rat(mpq(2,1))

visit_i(i: _I) → AST

Return the imaginary unit. Implements the abstract method ASTVisitor.visit_i().

>>> IdentityASTVisitor().visit_i(I)
_I()

visit_var(var: Var) → AST

Return the same variable. Implements the abstract method ASTVisitor.visit_var().

>>> IdentityASTVisitor().visit_var(Var('x'))
Var('x')

visit_add(add: Add) → AST

Return the same addition node, but with all arguments visited. Implements the abstract method ASTVisitor.visit_add().

>>> x = Var('x')
>>> IdentityASTVisitor().visit_add(x + 2)
Add(Var('x'), Rat(mpq(2,1)))

visit_mul(mul: Mul) → AST

Return the same multiplication node, but with all arguments visited. Implements the abstract method ASTVisitor.visit_mul().

>>> x = Var('x')
>>> IdentityASTVisitor().visit_mul(x * 2)
Mul(Var('x'), Rat(mpq(2,1)))

visit_pow(pow: Pow) → AST

Return the same power node, but with the base visited. Implements the abstract method ASTVisitor.visit_pow().

>>> x = Var('x')
>>> IdentityASTVisitor().visit_pow(x ** 2)
Pow(Var('x'), 2)

visit_neg(neg: Neg) → AST

Return the same negation node, but with the argument visited. Implements the abstract method ASTVisitor.visit_neg().

>>> x = Var('x')
>>> IdentityASTVisitor().visit_neg(Neg(x))
Neg(Var('x'))

visit_conj(conj: Conj) → AST

Return the same conjugation node, but with the argument visited. Implements the abstract method ASTVisitor.visit_conj().

>>> x = Var('x')
>>> IdentityASTVisitor().visit_conj(Conj(x))
Conj(Var('x'))

visit_re(re: Re) → AST

Return the same real part node, but with the argument visited. Implements the abstract method ASTVisitor.visit_re().

>>> x = Var('x')
>>> IdentityASTVisitor().visit_re(Re(x))
Re(Var('x'))

visit_im(im: Im) → AST

Return the same imaginary part node, but with the argument visited. Implements the abstract method ASTVisitor.visit_im().

>>> x = Var('x')
>>> IdentityASTVisitor().visit_im(Im(x))
Im(Var('x'))

class logic1.theories.Complex.ast.VariableSubstitutor

Bases: IdentityASTVisitor

Visitor that substitutes variables according to a given mapping. See also AST.subs().

>>> x = Var('x')
>>> (x + 2).accept(VariableSubstitutor({x: I}))
Add(_I(), Rat(mpq(2,1)))

__init__(mapping: Mapping[Var, int | float | Fraction | mpq | complex | AST]) → None

Initialize the substitutor with a given mapping.

visit_var(var: Var) → AST

Return the substituted AST node for the given variable, or the variable itself if not found in the mapping.

>>> x = Var('x')
>>> visitor = VariableSubstitutor({x: I})
>>> visitor.visit_var(x)
_I()
>>> y = Var('y')
>>> visitor.visit_var(y)
Var('y')

Printing

String and LaTeX formatters for complex ASTs.

class logic1.theories.Complex.format.ReprFormatter

Bases: ASTVisitor[str]

Formatter for AST nodes that produces a more human-readable string representation that is valid Python code and allows for the reconstruction of the original expression.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> (z**3 + 2 * I).accept(ReprFormatter())
'z**3 + 2 * I'

symbols: ClassVar[dict[type[AST], str]] = {}

Mapping of AST node types to their corresponding symbols used in the string representation. This mapping can be overridden in subclasses to customize the symbols.

visit_rat(num: Rat) → str

Return the string representation of a rational number.

>>> from logic1.theories.Complex.ast import *
>>> ReprFormatter().visit_rat(Rat(mpq(3, 4)))
'3/4'

visit_i(_: _I) → str

Return the string representation of the imaginary unit.

>>> from logic1.theories.Complex.ast import *
>>> ReprFormatter().visit_i(I)
'I'

visit_var(var: Var) → str

Return the string representation of a variable.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> ReprFormatter().visit_var(z)
'z'

visit_add(add: Add) → str

Return the string representation of an addition.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> ReprFormatter().visit_add(z + 1 - I)
'z + 1 - I'

visit_mul(mul: Mul) → str

Return the string representation of a multiplication.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> ReprFormatter().visit_mul(z * (z + 1))
'z * (z + 1)'

visit_pow(pow: Pow) → str

Return the string representation of a power.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> ReprFormatter().visit_pow(z**2)
'z**2'

visit_neg(neg: Neg) → str

Return the string representation of a negation.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> ReprFormatter().visit_neg(-z)
'-z'

visit_conj(conj: Conj) → str

Return the string representation of a conjugation.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> ReprFormatter().visit_conj(~z)
'~z'

visit_re(re: Re) → str

Return the string representation of a real part.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> ReprFormatter().visit_re(Re(z))
'Re(z)'

visit_im(im: Im) → str

Return the string representation of an imaginary part.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> ReprFormatter().visit_im(Im(z))
'Im(z)'

__annotate_func__()

The type of the None singleton.

class logic1.theories.Complex.format.StrFormatter

Bases: ReprFormatter

Formatter for AST nodes that produces a more human-readable string representation but does not necessarily allow the reconstruction of the original expression.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> (z**3 + 2 * I).accept(StrFormatter())
'z^3 + 2 * i'

symbols: ClassVar[dict[type[AST], str]] = {<class 'logic1.theories.Complex.ast.Pow'>: '^', <class 'logic1.theories.Complex.ast._I'>: 'i'}

Custom mapping of AST node types to their corresponding symbols.

class logic1.theories.Complex.format.LatexFormatter

Bases: ReprFormatter

Formatter for AST nodes that produces a LaTeX representation.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> (z**3 + 2 * I).accept(LatexFormatter())
'z^{3} + 2 i'

symbols: ClassVar[dict[type[AST], str]] = {<class 'logic1.theories.Complex.ast.Im'>: '\\Im', <class 'logic1.theories.Complex.ast.Mul'>: '\\cdot', <class 'logic1.theories.Complex.ast.Re'>: '\\Re', <class 'logic1.theories.Complex.ast._I'>: 'i'}

Custom mapping of AST node types to their corresponding symbols.

visit_rat(num: Rat) → str

Return the LaTeX representation of a rational number as integer or fraction.

>>> from logic1.theories.Complex.ast import *
>>> LatexFormatter().visit_rat(Rat(mpq(2)))
'2'
>>> LatexFormatter().visit_rat(Rat(mpq(3, 4)))
'\\frac{3}{4}'

visit_var(var: Var) → str

Return the LaTeX representation of a variable.

>>> from logic1.theories.Complex.ast import *
>>> LatexFormatter().visit_var(Var('z'))
'z'
>>> LatexFormatter().visit_var(Var('z1'))
'z_{1}'
>>> LatexFormatter().visit_var(Var('z_re'))
'z_{re}'

visit_conj(conj: Conj) → str

Return the LaTeX representation of a conjugation.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> LatexFormatter().visit_conj(~z)
'\\overline{z}'

visit_pow(pow: Pow) → str

Return the LaTeX representation of a power.

>>> from logic1.theories.Complex.ast import *
>>> z = Var('z')
>>> LatexFormatter().visit_pow(z**2)
'z^{2}'

Normalization

Visitors and functions for evaluating and normalizing complex ASTs.

class logic1.theories.Complex.normalize.ArithmeticEvaluator

Bases: ASTVisitor[α]

Abstract visitor that evaluates an AST to an element of α, given implementations of addition, negation and multiplication.

See also

ConstantEvaluator, qe.RCF_Evaluator

abstractmethod add(a: α, b: α) → α

Add two elements. Must be implemented by subclasses.

abstractmethod neg(a: α) → α

Negate an element. Must be implemented by subclasses.

abstractmethod mul(a: α, b: α) → α

Multiply two elements. Must be implemented by subclasses.

visit_add(add: Add) → α

Evaluate a sum by using the add() method.

visit_mul(mul: Mul) → α

Evaluate a product by using the mul() method.

visit_neg(neg: Neg) → α

Evaluate a negation by using the neg() method.

visit_pow(pow: Pow) → α

Evaluate a power using the mul() method.

class logic1.theories.Complex.normalize.ConstantEvaluator

Bases: ArithmeticEvaluator[tuple[mpq, mpq]]

Visitor based on ArithmeticEvaluator that evaluates an AST to a constant. The result is a complex number represented as a pair of real and imaginary parts. Raises a ValueError if the AST contains variables.

>>> (1 + 2 * I).accept(ConstantEvaluator())
(mpq(1,1), mpq(2,1))

add(a: tuple[mpq, mpq], b: tuple[mpq, mpq]) → tuple[mpq, mpq]

Add two complex numbers represented as pairs of real and imaginary parts. Implements the abstract method ArithmeticEvaluator.add().

>>> ConstantEvaluator().add((mpq(1), mpq(2)), (mpq(3), mpq(4)))
(mpq(4,1), mpq(6,1))

neg(a: tuple[mpq, mpq]) → tuple[mpq, mpq]

Negate a complex number represented as a pair of real and imaginary parts. Implements the abstract method ArithmeticEvaluator.neg().

>>> ConstantEvaluator().neg((mpq(1), mpq(2)))
(mpq(-1,1), mpq(-2,1))

mul(a: tuple[mpq, mpq], b: tuple[mpq, mpq]) → tuple[mpq, mpq]

Multiply two complex numbers represented as pairs of real and imaginary parts. Implements the abstract method ArithmeticEvaluator.mul().

>>> ConstantEvaluator().mul((mpq(1), mpq(2)), (mpq(3), mpq(4)))
(mpq(-5,1), mpq(10,1))

visit_rat(num: Rat) → tuple[mpq, mpq]

Evaluate a rational number. Implements the abstract method ASTVisitor.visit_rat().

>>> ConstantEvaluator().visit_rat(Rat(mpq(1, 2)))
(mpq(1,2), mpq(0,1))

visit_i(i: _I) → tuple[mpq, mpq]

Evaluate the imaginary unit. Implements the abstract method ASTVisitor.visit_i().

>>> ConstantEvaluator().visit_i(I)
(mpq(0,1), mpq(1,1))

visit_var(var: Var) → tuple[mpq, mpq]

Raise a ValueError since variables cannot be evaluated to constants. Implements the abstract method ASTVisitor.visit_var().

>>> x = Var('x')
>>> ConstantEvaluator().visit_var(x)
Traceback (most recent call last):
  ...
ValueError: Cannot evaluate variable x

visit_conj(conj: Conj) → tuple[mpq, mpq]

Evaluate a complex conjugation. Implements the abstract method ASTVisitor.visit_conj().

>>> ConstantEvaluator().visit_conj(Conj(1 + 2 * I))
(mpq(1,1), mpq(-2,1))

visit_re(re: Re) → tuple[mpq, mpq]

Evaluate a real part. Implements the abstract method ASTVisitor.visit_re().

>>> ConstantEvaluator().visit_re(Re(1 + 2 * I))
(mpq(1,1), mpq(0,1))

visit_im(im: Im) → tuple[mpq, mpq]

Evaluate an imaginary part. Implements the abstract method ASTVisitor.visit_im().

>>> ConstantEvaluator().visit_im(Im(1 + 2 * I))
(mpq(2,1), mpq(0,1))

class logic1.theories.Complex.normalize.WeakNormalizer

Bases: IdentityASTVisitor

Visitor that normalizes an AST by rearranging sums and products, and applying local simplifications, but not expanding any nodes.

visit_add(add: Add) → AST

Normalize a sum by collecting constant terms and rearranging non-constant terms in a canonical order according to AddSortKey.

>>> x, y, z = Var('x'), Var('y'), Var('z')
>>> print(WeakNormalizer().visit_add(y + x + z + x - z))
2 * x + y
>>> print(WeakNormalizer().visit_add(2 + x - 3))
x - 1

visit_mul(mul: Mul) → AST

Normalize a product by collecting constant factors and rearranging non-constant factors in a canonical order according to MulSortKey.

>>> x, y = Var('x'), Var('y')
>>> print(WeakNormalizer().visit_mul(y * x * y))
x * y^2
>>> print(WeakNormalizer().visit_mul(2 * x * -I))
-2 * i * x
>>> print(WeakNormalizer().visit_mul(x * Re(x) * Im(x) * Conj(x)))
x * ~x * Re(x) * Im(x)
>>> print(WeakNormalizer().visit_mul(Re(x) * Re(y) * (x + y)))
Re(x) * Re(y) * (x + y)
>>> print(WeakNormalizer().visit_mul(0 * x))
0
>>> print(WeakNormalizer().visit_mul(1 * x))
x
>>> print(WeakNormalizer().visit_mul(-1 * x))
-x

visit_pow(pow: Pow) → AST

Normalize a power by evaluating it if the base is constant, and simplifying if the exponent is 0 or 1. Note that 0 ** 0 is defined to be 1 as for gmpy2.mpq.

>>> x, y = Var('x'), Var('y')
>>> print(WeakNormalizer().visit_pow((x + y)**0))
1
>>> print(WeakNormalizer().visit_pow((x + y)**1))
x + y
>>> print(WeakNormalizer().visit_pow((x + y)**2))
(x + y)^2
>>> print(WeakNormalizer().visit_pow(I**2))
-1
>>> print(WeakNormalizer().visit_pow((I - I)**0))
1

visit_neg(neg: Neg) → AST

Normalize a negation by evaluating constants, simplifying double negations and moving the negation inside products.

>>> x, y = Var('x'), Var('y')
>>> print(WeakNormalizer().visit_neg(-(1 + I)))
-1 - i
>>> print(WeakNormalizer().visit_neg(-(-x)))
x
>>> print(WeakNormalizer().visit_neg(-(x * y)))
-x * y

visit_conj(conj: Conj) → AST

Normalize a conjugation by evaluating constants and by simplifying double conjugations and conjugations of real and imaginary parts.

>>> x, y = Var('x'), Var('y')
>>> print(WeakNormalizer().visit_conj(Conj(1 + I)))
1 - i
>>> print(WeakNormalizer().visit_conj(Conj(Conj(x))))
x
>>> print(WeakNormalizer().visit_conj(Conj(Re(x))))
Re(x)
>>> print(WeakNormalizer().visit_conj(Conj(Im(x))))
Im(x)

visit_re(re: Re) → AST

Normalize a real part by evaluating constants and by simplifying real parts of real parts, imaginary parts and conjugates.

>>> x = Var('x')
>>> print(WeakNormalizer().visit_re(Re(1 + I)))
1
>>> print(WeakNormalizer().visit_re(Re(Re(x))))
Re(x)
>>> print(WeakNormalizer().visit_re(Re(Im(x))))
Im(x)
>>> print(WeakNormalizer().visit_re(Re(Conj(x))))
Re(x)

visit_im(im: Im) → AST

Normalize an imaginary part by evaluating constants and by simplifying imaginary parts of real parts, imaginary parts and conjugates.

>>> x = Var('x')
>>> print(WeakNormalizer().visit_im(Im(1 + I)))
1
>>> print(WeakNormalizer().visit_im(Im(Re(x))))
0
>>> print(WeakNormalizer().visit_im(Im(Im(x))))
0
>>> print(WeakNormalizer().visit_im(Im(Conj(x))))
-Im(x)

class logic1.theories.Complex.normalize.Normalizer

Bases: WeakNormalizer

Visitor based on WeakNormalizer that also expands sums and products, and propagates ast.Re, ast.Im and ast.Conj.

visit_mul(mul: Mul) → AST

Expand a product by distributing it over sums and normalizing the factors recursively.

>>> x, y, z = Var('x'), Var('y'), Var('z')
>>> print(Normalizer().visit_mul(x * (y + z)))
x * y + x * z

visit_pow(pow: Pow) → AST

Expand powers of sums and products, and normalize them recursively.

>>> x, y = Var('x'), Var('y')
>>> print(Normalizer().visit_pow((x + y)**2))
x^2 + 2 * x * y + y^2
>>> print(Normalizer().visit_pow((x * y)**2))
x^2 * y^2
>>> print(Normalizer().visit_pow((-x)**3))
-x^3

visit_neg(neg: Neg) → AST

Expand a negation by distributing it over sums and normalizing the argument recursively.

>>> x, y = Var('x'), Var('y')
>>> print(Normalizer().visit_neg(-(x + y)))
-x - y

visit_conj(conj: Conj) → AST

Propagate a conjugation by distributing it over sums and products, and normalizing the argument recursively.

>>> x, y = Var('x'), Var('y')
>>> print(Normalizer().visit_conj(Conj(x + y)))
~x + ~y
>>> print(Normalizer().visit_conj(Conj(x * y)))
~x * ~y
>>> print(Normalizer().visit_conj(Conj(-x)))
-~x
>>> print(Normalizer().visit_conj(Conj(x**2)))
(~x)^2

visit_re(re: Re) → AST

Propagate a real part by distributing it over sums and products, and normalizing the argument recursively.

>>> x, y = Var('x'), Var('y')
>>> print(Normalizer().visit_re(Re(x + y)))
Re(x) + Re(y)
>>> print(Normalizer().visit_re(Re(x * y)))
Re(x) * Re(y) - Im(x) * Im(y)
>>> print(Normalizer().visit_re(Re(-x)))
-Re(x)
>>> print(Normalizer().visit_re(Re(x**2)))
Re(x)^2 - Im(x)^2

visit_im(im: Im) → AST

Propagate an imaginary part by distributing it over sums and products, and normalizing the argument recursively.

>>> x, y = Var('x'), Var('y')
>>> print(Normalizer().visit_im(Im(x + y)))
Im(x) + Im(y)
>>> print(Normalizer().visit_im(Im(x * y)))
Re(x) * Im(y) + Re(y) * Im(x)
>>> print(Normalizer().visit_im(Im(-x)))
-Im(x)
>>> print(Normalizer().visit_im(Im(x**2)))
2 * Re(x) * Im(x)

class logic1.theories.Complex.normalize.ConjugateNormalizer

Bases: Normalizer

Visitor based on Normalizer that additionally replaces all occurrences of Re and Im. This yields a unique normal form.

>>> z = Var('z')
>>> normalizer = ConjugateNormalizer()
>>> print((Re(z) + I * Im(z)).accept(normalizer))
z
>>> print((Re(z)**2 + Im(z)**2).accept(normalizer))
z * ~z

visit_re(re: Re) → AST

Replace a real part with its equivalent expression in terms of its argument and its conjugate.

>>> z = Var('z')
>>> print(ConjugateNormalizer().visit_re(Re(z)))
1/2 * z + 1/2 * ~z

visit_im(im: Im) → AST

Replace an imaginary part with its equivalent expression in terms of its argument and its conjugate.

>>> z = Var('z')
>>> print(ConjugateNormalizer().visit_im(Im(z)))
-1/2 * i * z + 1/2 * i * ~z

logic1.theories.Complex.normalize.conjugate_normal_form(ast: AST) → AST

Return the conjugate normal form of an AST which is a polynomial expression in the variables and their conjugates. It is a unique normal form.

>>> z = Var('z')
>>> print(conjugate_normal_form(z))
z
>>> print(conjugate_normal_form(Re(z)))
1/2 * z + 1/2 * ~z

logic1.theories.Complex.normalize.cartesian_normal_form(ast: AST) → AST

Return the Cartesian normal form of an AST which is of the form f + I * g where f and g are polynomial expressions in the real and imaginary parts of variables. It is a unique normal form.

>>> z = Var('z')
>>> print(cartesian_normal_form(z))
Re(z) + i * Im(z)
>>> print(cartesian_normal_form(z**2))
Re(z)^2 - Im(z)^2 + i * 2 * Re(z) * Im(z)

SortKeys

class logic1.theories.Complex.ast.SortKey

Bases: Generic[η]

Default sort key for comparing AST nodes.

>>> z = Var('z')
>>> SortKey(z) < SortKey(z + 1)
True

See also

AST.sort_key()

ORDER: ClassVar[tuple[type[AST], ...]] = (<class 'logic1.theories.Complex.ast.Rat'>, <class 'logic1.theories.Complex.ast._I'>, <class 'logic1.theories.Complex.ast.Var'>, <class 'logic1.theories.Complex.ast.Conj'>, <class 'logic1.theories.Complex.ast.Re'>, <class 'logic1.theories.Complex.ast.Im'>, <class 'logic1.theories.Complex.ast.Pow'>, <class 'logic1.theories.Complex.ast.Neg'>, <class 'logic1.theories.Complex.ast.Mul'>, <class 'logic1.theories.Complex.ast.Add'>)

The order of AST node types for sorting.

ast: η

The AST node for which this is a sort key.

property op: type[AST]

The operation of the underlying AST node.

>>> z = Var('z')
>>> SortKey(z).op
<class 'logic1.theories.Complex.ast.Var'>

property args: tuple[object, ...]

The arguments of the underlying AST node, where each argument that is itself an AST node is replaced by its sort key.

>>> z = Var('z')
>>> SortKey(z + 1).args
(SortKey(Var('z')), SortKey(Rat(mpq(1,1))))

__eq__(other: object) → bool

Return True if the underlying AST nodes are equal, i.e. have the same operation and the same arguments.

>>> z = Var('z')
>>> SortKey(z) == SortKey(z)
True
>>> SortKey(z) == SortKey(z + 1)
False

__le__(other: SortKey) → bool

Comparison of the underlying AST nodes first by their operation according to ORDER, then recursively by their arguments. The remaining comparison operators are derived from this using functools.total_ordering().

>>> z = Var('z')
>>> SortKey(z) <= SortKey(z + 1)
True

__repr__() → str

Return a string representation of this sort key that can be evaluated to reconstruct the sort key.

>>> z = Var('z')
>>> repr(SortKey(z))
"SortKey(Var('z'))"

class logic1.theories.Complex.normalize.AddSortKey

Bases: object

A sort key for canonically ordering sums in WeakNormalizer. It compares two AST nodes first by their total degree and then lexicographically by their factors.

>>> x, y = Var('x'), Var('y')
>>> AddSortKey(x * y) <= AddSortKey(x**2)
True

__init__(ast: AST) → None

Initialize the sort key of an AST node.

ast: AST

The AST node for which this is a sort key.

total_degree: int

The total degree of the AST node.

factors: list[tuple[AST, int]]

The factors of the AST node, each represented as a tuple of the factor and its degree.

__le__(other: Self) → bool

Compare the underlying AST nodes first by their total degree and then lexicographically by their factors using MulSortKey. The remaining comparison operators are derived from this using functools.total_ordering().

>>> x, y, z = Var('x'), Var('y'), Var('z')
>>> AddSortKey(x * y) <= AddSortKey(x**2)
True
>>> AddSortKey(x**2) <= AddSortKey(x * y)
False

__eq__(other)

Return self==value.

class logic1.theories.Complex.normalize.MulSortKey

Bases: object

A sort key for canonically ordering AST nodes inside products in WeakNormalizer. It compares two AST nodes first by their operator and then by their arguments and exponent.

>>> z = Var('z')
>>> MulSortKey(z**2) <= MulSortKey(z)
False
>>> MulSortKey(z) <= MulSortKey(Re(z))
True

property args: tuple[object, ...]

Return the arguments of the AST node, replacing any AST nodes with their corresponding sort keys.

__init__(ast: AST) → None

Initialize the sort key of an AST node. The AST node must not be a constant, a negation or a product.

ast: AST

The AST node for which this is a sort key.

degree: int = 1

The exponent of the AST node.

__le__(other: Self) → bool

Compare the underlying AST nodes first by their operator and then by their arguments and exponent. The remaining comparison operators are derived from this using functools.total_ordering().

>>> z = Var('z')
>>> MulSortKey(z**2) <= MulSortKey(z)
False
>>> MulSortKey(z) <= MulSortKey(Re(z))
True

__eq__(other)

Return self==value.