Index

_

__add__() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) __and__() (logic1.firstorder.formula.Formula method) __annotate_func__() (logic1.theories.Complex.format.ReprFormatter method) __bool__() (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.RCF.atomic.AtomicFormula method) __call__() (logic1.abc.qe.QuantifierElimination method) __eq__() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.ast.SortKey method) (logic1.theories.Complex.normalize.AddSortKey method) (logic1.theories.Complex.normalize.MulSortKey method) (logic1.theories.Complex.term.Term method) (logic1.theories.Complex.term.VariableSet method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.RCF.term.Term method) (logic1.theories.Sets.atomic.Variable method) __ge__() (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) __getitem__() (logic1.firstorder.term.VariableSet method) (logic1.theories.Complex.term.VariableSet method) (logic1.theories.RCF.term.VariableSet method) (logic1.theories.Sets.atomic.VariableSet method) __gt__() (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) __init__() (logic1.firstorder.formula.Formula method) (logic1.theories.Complex.ast._I method) (logic1.theories.Complex.ast.Add method) (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.ast.Conj method) (logic1.theories.Complex.ast.Im method) (logic1.theories.Complex.ast.MonoidalOperation method) (logic1.theories.Complex.ast.Mul method) (logic1.theories.Complex.ast.Neg method) (logic1.theories.Complex.ast.Pow method) (logic1.theories.Complex.ast.Rat method) (logic1.theories.Complex.ast.Re method) (logic1.theories.Complex.ast.UnaryOperation method) (logic1.theories.Complex.ast.Var method) (logic1.theories.Complex.ast.VariableSubstitutor method) (logic1.theories.Complex.atomic.Eq method) (logic1.theories.Complex.atomic.Ge method) (logic1.theories.Complex.atomic.Gt method) (logic1.theories.Complex.atomic.Le method) (logic1.theories.Complex.atomic.Lt method) (logic1.theories.Complex.atomic.Ne method) (logic1.theories.Complex.atomic.RealAtomicFormula method) (logic1.theories.Complex.normalize.AddSortKey method) (logic1.theories.Complex.normalize.MulSortKey method) (logic1.theories.Complex.term.Term method) (logic1.theories.Complex.term.Variable method) (logic1.theories.Complex.term.VariableSet method) (logic1.theories.RCF.term.Term method) __invert__() (logic1.firstorder.formula.Formula method) (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) __iter__() (logic1.theories.RCF.term.Term method) __le__() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.ast.SortKey method) (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.Complex.normalize.AddSortKey method) (logic1.theories.Complex.normalize.MulSortKey method) (logic1.theories.Complex.term.SortKey method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.RCF.term.Term method) (logic1.theories.Sets.atomic.AtomicFormula method)

__lshift__() (logic1.firstorder.formula.Formula method) __lt__() (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) __mul__() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) __ne__() (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) (logic1.theories.Sets.atomic.Variable method) __neg__() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) __new__() (logic1.theories.Complex.ast._I static method) (logic1.theories.Complex.ast.MonoidalOperation static method) (logic1.theories.Complex.ast.Rat static method) __or__() (logic1.firstorder.formula.Formula method) __pow__() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) __radd__() (logic1.theories.RCF.term.Term method) __repr__() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.ast.SortKey method) (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.Complex.term.Term method) (logic1.theories.Complex.term.VariableSet method) __rmul__() (logic1.theories.RCF.term.Term method) __rshift__() (logic1.firstorder.formula.Formula method) __rsub__() (logic1.theories.RCF.term.Term method) __str__() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.RCF.term.Term method) (logic1.theories.Sets.atomic.AtomicFormula method) __sub__() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) __truediv__() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) __xor__() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) _F (class in logic1.firstorder.boolean) _I (class in logic1.theories.Complex.ast) _repr_latex_() (logic1.firstorder.formula.Formula method) _T (class in logic1.firstorder.boolean)

A

accept() (logic1.theories.Complex.ast._I method) (logic1.theories.Complex.ast.Add method) (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.ast.Conj method) (logic1.theories.Complex.ast.Im method) (logic1.theories.Complex.ast.Mul method) (logic1.theories.Complex.ast.Neg method) (logic1.theories.Complex.ast.Pow method) (logic1.theories.Complex.ast.Rat method) (logic1.theories.Complex.ast.Re method) (logic1.theories.Complex.ast.Var method) Add (class in logic1.theories.Complex.ast) add() (logic1.abc.simplify.InternalRepresentation method) (logic1.theories.Complex.normalize.ArithmeticEvaluator method) (logic1.theories.Complex.normalize.ConstantEvaluator method) (logic1.theories.Complex.qe.RCF_Evaluator method) (logic1.theories.Complex.simplify.InternalRepresentation method) (logic1.theories.RCF.term.DEFINITE static method) AddSortKey (class in logic1.theories.Complex.normalize) All (class in logic1.firstorder.quantified) ALL (logic1.abc.simplify.RESTART attribute) all() (logic1.firstorder.formula.Formula method) And (class in logic1.firstorder.boolean) append() (logic1.abc.qe.Assumptions method) arg (logic1.firstorder.boolean.Not property) (logic1.firstorder.quantified.QuantifiedFormula property) (logic1.theories.Complex.ast.UnaryOperation attribute) args (logic1.firstorder.formula.Formula property) (logic1.theories.Complex.ast._I property) (logic1.theories.Complex.ast.AST property) (logic1.theories.Complex.ast.MonoidalOperation property) (logic1.theories.Complex.ast.Pow property) (logic1.theories.Complex.ast.Rat property) (logic1.theories.Complex.ast.SortKey property) (logic1.theories.Complex.ast.UnaryOperation property) (logic1.theories.Complex.ast.Var property) (logic1.theories.Complex.normalize.MulSortKey property)

ArithmeticEvaluator (class in logic1.theories.Complex.normalize) as_constant() (logic1.theories.RCF.term.Term method) as_latex() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.firstorder.term.Term method) (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.RCF.term.Term method) (logic1.theories.Sets.atomic.AtomicFormula method) (logic1.theories.Sets.atomic.Variable method) as_redlog() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.theories.RCF.atomic.AtomicFormula method) as_variable() (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) Assumptions (class in logic1.abc.qe) (class in logic1.theories.RCF.node) (class in logic1.theories.Sets.qe) assumptions (logic1.abc.qe.QuantifierElimination property) Assumptions.Inconsistent AST (class in logic1.theories.Complex.ast) ast (logic1.theories.Complex.ast.SortKey attribute) (logic1.theories.Complex.normalize.AddSortKey attribute) (logic1.theories.Complex.normalize.MulSortKey attribute) ASTVisitor (class in logic1.theories.Complex.ast) AtomicFormula (class in logic1.firstorder.atomic) (class in logic1.theories.Complex.atomic) (class in logic1.theories.RCF.atomic) (class in logic1.theories.Sets.atomic) atoms (logic1.abc.qe.Assumptions attribute) atoms() (logic1.firstorder.formula.Formula method)

B

base (logic1.theories.Complex.ast.Pow attribute) blocks (logic1.abc.qe.QuantifierElimination attribute) BooleanFormula (class in logic1.firstorder.boolean) BooleanNormalForm (class in logic1.abc.bnf) (class in logic1.theories.RCF.bnf) (class in logic1.theories.Sets.bnf)

bvars() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.Sets.atomic.AtomicFormula method)

C

C (class in logic1.theories.Sets.atomic) C_ (class in logic1.theories.Sets.atomic) cartesian_normal_form() (in module logic1.theories.Complex.normalize) Clustering (class in logic1.theories.RCF.node) clustering (logic1.theories.RCF.qe.Options attribute) cnf() (in module logic1.theories.RCF.bnf) (in module logic1.theories.Sets.bnf) (logic1.abc.bnf.BooleanNormalForm method) coefficient() (logic1.theories.RCF.term.Term method) complement() (logic1.firstorder.atomic.AtomicFormula class method) (logic1.theories.Complex.atomic.AtomicFormula class method) (logic1.theories.RCF.atomic.AtomicFormula class method) (logic1.theories.Sets.atomic.AtomicFormula class method) Conj (class in logic1.theories.Complex.ast) Conj() (in module logic1.theories.Complex.term)

conjugate() (logic1.theories.Complex.term.Term method) conjugate_normal_form() (in module logic1.theories.Complex.normalize) ConjugateNormalizer (class in logic1.theories.Complex.normalize) constant_coefficient() (logic1.theories.RCF.term.Term method) ConstantEvaluator (class in logic1.theories.Complex.normalize) content() (logic1.theories.RCF.term.Term method) converse() (logic1.theories.Complex.atomic.AtomicFormula class method) (logic1.theories.RCF.atomic.AtomicFormula class method) copy() (logic1.abc.qe.Node method) count_alternations() (logic1.firstorder.formula.Formula method) create_assumptions() (logic1.abc.qe.QuantifierElimination method) create_initial_representation() (logic1.abc.simplify.Simplify method) (logic1.theories.Complex.simplify.Simplify method) create_options() (logic1.abc.qe.QuantifierElimination method) create_root_nodes() (logic1.abc.qe.QuantifierElimination method) create_true_node() (logic1.abc.qe.QuantifierElimination method)

D

DEFINITE (class in logic1.theories.RCF.term) definite() (logic1.firstorder.boolean.And class method) (logic1.firstorder.boolean.Or class method) definite_element() (logic1.firstorder.boolean.And class method) (logic1.firstorder.boolean.Or class method) degree (logic1.theories.Complex.normalize.MulSortKey attribute) degree() (logic1.theories.RCF.term.Term method) DeltaTimeFormatter (class in logic1.support.logging) depth() (logic1.firstorder.formula.Formula method) derivative() (logic1.theories.RCF.term.Term method)

dnf() (in module logic1.theories.RCF.bnf) (in module logic1.theories.Sets.bnf) (logic1.abc.bnf.BooleanNormalForm method) dual() (logic1.firstorder.boolean._F class method) (logic1.firstorder.boolean._T class method) (logic1.firstorder.boolean.And class method) (logic1.firstorder.boolean.Or class method) (logic1.firstorder.quantified.All class method) (logic1.firstorder.quantified.Ex class method) (logic1.theories.RCF.atomic.AtomicFormula class method)

E

elimination_order (logic1.theories.RCF.qe.Options attribute) Eq (class in logic1.theories.Complex.atomic) (class in logic1.theories.RCF.atomic) (class in logic1.theories.Sets.atomic) Equivalent (class in logic1.firstorder.boolean) eval() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.Complex.term.Term method)

Ex (class in logic1.firstorder.quantified) ex() (logic1.firstorder.formula.Formula method) explode_always (logic1.theories.RCF.simplify.Options attribute) exponent (logic1.theories.Complex.ast.Pow attribute) extend() (logic1.abc.qe.Assumptions method) extract() (logic1.abc.simplify.InternalRepresentation method) (logic1.theories.Complex.simplify.InternalRepresentation method)

F

F (in module logic1.firstorder.boolean) factor() (logic1.theories.RCF.term.Term method) factors (logic1.theories.Complex.normalize.AddSortKey attribute) factors() (logic1.theories.Complex.ast.AST method) failure_nodes (logic1.abc.qe.QuantifierElimination attribute) final_simplify() (logic1.abc.bnf.BooleanNormalForm method) (logic1.abc.qe.QuantifierElimination method) Formula (class in logic1.firstorder.formula) (in module logic1.theories.Complex.types) (in module logic1.theories.RCF.types) (in module logic1.theories.Sets.types) formula (logic1.abc.qe.Node attribute) formula_to_complex() (in module logic1.theories.Complex.qe) formula_to_rcf() (in module logic1.theories.Complex.qe) fresh() (logic1.firstorder.term.Variable method) (logic1.theories.Complex.term.Variable method) (logic1.theories.Complex.term.VariableSet method) (logic1.theories.RCF.term.Variable method) (logic1.theories.RCF.term.VariableSet method) (logic1.theories.Sets.atomic.Variable method) (logic1.theories.Sets.atomic.VariableSet method)

from_constant() (logic1.theories.RCF.term.DEFINITE static method) from_number() (logic1.theories.Complex.ast.AST static method) from_real_imag() (logic1.theories.Complex.ast.AST static method) (logic1.theories.Complex.term.Term static method) FULL (logic1.theories.RCF.node.Clustering attribute) (logic1.theories.RCF.node.Generic attribute) fvars() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.Sets.atomic.AtomicFormula method)

G

Ge (class in logic1.theories.Complex.atomic) (class in logic1.theories.RCF.atomic) Generic (class in logic1.theories.RCF.node) generic (logic1.theories.RCF.qe.Options attribute) get() (logic1.firstorder.term.VariableSet method) (logic1.support.logging.Timer method)

get_reference_time() (logic1.support.logging.DeltaTimeFormatter method) gqe() (in module logic1.theories.RCF.redlog) Gt (class in logic1.theories.Complex.atomic) (class in logic1.theories.RCF.atomic)

I

I (in module logic1.theories.Complex.ast) (in module logic1.theories.Complex.term) identity (logic1.theories.Complex.ast.Add attribute) (logic1.theories.Complex.ast.MonoidalOperation attribute) (logic1.theories.Complex.ast.Mul attribute) IdentityASTVisitor (class in logic1.theories.Complex.ast) Im (class in logic1.theories.Complex.ast) Im() (in module logic1.theories.Complex.term) imaginary_part() (logic1.theories.Complex.term.Term method) imp() (logic1.firstorder.term.VariableSet method) implicit_ranges (logic1.theories.RCF.simplify.Options attribute) Implies (class in logic1.firstorder.boolean) Index (in module logic1.theories.Sets.atomic) index (logic1.theories.Sets.atomic.C_ property) init_env() (logic1.abc.qe.QuantifierElimination class method) init_env_arg() (logic1.abc.qe.QuantifierElimination method) InternalRepresentation (class in logic1.abc.simplify) (class in logic1.theories.Complex.simplify) (class in logic1.theories.RCF.simplify) (class in logic1.theories.Sets.simplify) InternalRepresentation.Inconsistent involutive_not() (in module logic1.firstorder.boolean) is_all() (logic1.firstorder.formula.Formula static method) is_and() (logic1.firstorder.formula.Formula static method) is_atomic() (logic1.firstorder.formula.Formula static method) is_boolean_formula() (logic1.firstorder.formula.Formula static method) is_constant() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method)

is_definite() (logic1.theories.RCF.term.Term method) is_equivalent() (logic1.firstorder.formula.Formula static method) is_ex() (logic1.firstorder.formula.Formula static method) is_false() (logic1.firstorder.formula.Formula static method) is_imaginary() (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.Complex.term.Term method) is_implies() (logic1.firstorder.formula.Formula static method) is_monomial() (logic1.theories.RCF.term.Term method) is_not() (logic1.firstorder.formula.Formula static method) is_or() (logic1.firstorder.formula.Formula static method) is_quantified_formula() (logic1.firstorder.formula.Formula static method) is_real() (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.Complex.term.Term method) is_term() (logic1.firstorder.formula.Formula static method) is_true() (logic1.firstorder.formula.Formula static method) is_valid() (in module logic1.theories.Complex.simplify) (in module logic1.theories.RCF.simplify) (in module logic1.theories.Sets.simplify) (logic1.abc.simplify.Simplify method) is_variable() (logic1.firstorder.formula.Formula static method) (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) is_weakly_parametric_linear() (logic1.theories.RCF.term.Term method) is_zero() (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method)

L

LatexFormatter (class in logic1.theories.Complex.format) lc() (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) Le (class in logic1.theories.Complex.atomic) (class in logic1.theories.RCF.atomic) lhs (logic1.firstorder.boolean.Equivalent property) (logic1.firstorder.boolean.Implies property) (logic1.theories.Complex.atomic.AtomicFormula property) (logic1.theories.RCF.atomic.AtomicFormula property) (logic1.theories.Sets.atomic.Ne property) lift (logic1.theories.RCF.simplify.Options attribute) log_level (logic1.abc.qe.Options attribute) (logic1.theories.RCF.qe.Options attribute) log_rate (logic1.abc.qe.Options attribute) (logic1.theories.RCF.qe.Options attribute) logic1.abc module logic1.abc.bnf module logic1.abc.qe module logic1.abc.simplify module logic1.firstorder module logic1.firstorder.atomic module logic1.firstorder.boolean module logic1.firstorder.formula module logic1.firstorder.quantified module logic1.firstorder.term module logic1.interactive.Complex module logic1.interactive.RCF module logic1.interactive.Sets module logic1.support.excepthook module logic1.support.logging module logic1.theories.Complex module

logic1.theories.Complex.ast module logic1.theories.Complex.atomic module logic1.theories.Complex.format module logic1.theories.Complex.normalize module logic1.theories.Complex.qe module logic1.theories.Complex.simplify module logic1.theories.Complex.term module logic1.theories.Complex.types module logic1.theories.RCF module logic1.theories.RCF.atomic module logic1.theories.RCF.bnf module logic1.theories.RCF.qe module logic1.theories.RCF.redlog module logic1.theories.RCF.simplify module logic1.theories.RCF.term module logic1.theories.RCF.types module logic1.theories.Sets module logic1.theories.Sets.atomic module logic1.theories.Sets.bnf module logic1.theories.Sets.qe module logic1.theories.Sets.simplify module logic1.theories.Sets.types module Lt (class in logic1.theories.Complex.atomic) (class in logic1.theories.RCF.atomic)

M

matrix (logic1.abc.qe.QuantifierElimination attribute) matrix() (logic1.firstorder.formula.Formula method) memorize() (logic1.abc.qe.Node method) module logic1.abc logic1.abc.bnf logic1.abc.qe logic1.abc.simplify logic1.firstorder logic1.firstorder.atomic logic1.firstorder.boolean logic1.firstorder.formula logic1.firstorder.quantified logic1.firstorder.term logic1.interactive.Complex logic1.interactive.RCF logic1.interactive.Sets logic1.support.excepthook logic1.support.logging logic1.theories.Complex logic1.theories.Complex.ast logic1.theories.Complex.atomic logic1.theories.Complex.format logic1.theories.Complex.normalize logic1.theories.Complex.qe logic1.theories.Complex.simplify logic1.theories.Complex.term logic1.theories.Complex.types logic1.theories.RCF logic1.theories.RCF.atomic logic1.theories.RCF.bnf logic1.theories.RCF.qe logic1.theories.RCF.redlog logic1.theories.RCF.simplify logic1.theories.RCF.term logic1.theories.RCF.types logic1.theories.Sets logic1.theories.Sets.atomic logic1.theories.Sets.bnf logic1.theories.Sets.qe logic1.theories.Sets.simplify logic1.theories.Sets.types

MonoidalOperation (class in logic1.theories.Complex.ast) MONOMIAL (logic1.theories.RCF.node.Generic attribute) monomial_coefficient() (logic1.theories.RCF.term.Term method) monomials() (logic1.theories.RCF.term.Term method) MPolynomial (class in logic1.theories.RCF.types) Mul (class in logic1.theories.Complex.ast) mul() (logic1.theories.Complex.normalize.ArithmeticEvaluator method) (logic1.theories.Complex.normalize.ConstantEvaluator method) (logic1.theories.Complex.qe.RCF_Evaluator method) (logic1.theories.RCF.term.DEFINITE static method) MulSortKey (class in logic1.theories.Complex.normalize)

N

name (logic1.theories.Complex.ast.Var attribute) (logic1.theories.Complex.term.Variable property) Ne (class in logic1.theories.Complex.atomic) (class in logic1.theories.RCF.atomic) (class in logic1.theories.Sets.atomic) Neg (class in logic1.theories.Complex.ast) neg() (logic1.theories.Complex.normalize.ArithmeticEvaluator method) (logic1.theories.Complex.normalize.ConstantEvaluator method) (logic1.theories.Complex.qe.RCF_Evaluator method) negated (logic1.abc.qe.QuantifierElimination attribute) NEGATIVE (logic1.theories.RCF.term.DEFINITE attribute) NEGATIVE_SEMI (logic1.theories.RCF.term.DEFINITE attribute) neutral() (logic1.firstorder.boolean.And class method) (logic1.firstorder.boolean.Or class method) neutral_element() (logic1.firstorder.boolean.And class method) (logic1.firstorder.boolean.Or class method)

next_() (logic1.abc.simplify.InternalRepresentation method) (logic1.theories.Complex.simplify.InternalRepresentation method) Node (class in logic1.abc.qe) (class in logic1.theories.RCF.node) (class in logic1.theories.Sets.qe) NodeList (class in logic1.abc.qe) NONE (logic1.abc.simplify.RESTART attribute) (logic1.theories.RCF.node.Clustering attribute) (logic1.theories.RCF.node.Generic attribute) normal_ast (logic1.theories.Complex.term.Term property) normalize() (logic1.theories.RCF.term.Term method) Normalizer (class in logic1.theories.Complex.normalize) Not (class in logic1.firstorder.boolean) NoTraceException Number (in module logic1.theories.Complex.types)

O

off() (logic1.support.logging.RateFilter method) on() (logic1.support.logging.RateFilter method) oo (in module logic1.theories.Sets.atomic) op (logic1.firstorder.formula.Formula property) (logic1.theories.Complex.ast.AST property) (logic1.theories.Complex.ast.SortKey property) Options (class in logic1.abc.qe) (class in logic1.abc.simplify) (class in logic1.theories.Complex.simplify) (class in logic1.theories.RCF.qe) (class in logic1.theories.RCF.simplify)

options (logic1.abc.qe.QuantifierElimination attribute) Or (class in logic1.firstorder.boolean) ORDER (logic1.theories.Complex.ast.SortKey attribute) OTHERS (logic1.abc.simplify.RESTART attribute)

P

pop() (logic1.firstorder.term.VariableSet method) (logic1.theories.Complex.term.VariableSet method) (logic1.theories.RCF.term.VariableSet method) (logic1.theories.Sets.atomic.VariableSet method) POSITIVE (logic1.theories.RCF.term.DEFINITE attribute) POSITIVE_SEMI (logic1.theories.RCF.term.DEFINITE attribute) Pow (class in logic1.theories.Complex.ast) prefer_order (logic1.theories.RCF.simplify.Options attribute) prefer_weak (logic1.theories.RCF.simplify.Options attribute)

Prefix (class in logic1.firstorder.quantified) (in module logic1.theories.RCF.types) (in module logic1.theories.Sets.types) primitive_part() (logic1.theories.RCF.term.Term method) process() (logic1.abc.qe.Node method) pseudo_quo_rem() (logic1.theories.RCF.term.Term method) push() (logic1.firstorder.term.VariableSet method) (logic1.theories.Complex.term.VariableSet method) (logic1.theories.RCF.term.VariableSet method) (logic1.theories.Sets.atomic.VariableSet method)

Q

qe() (in module logic1.theories.Complex.qe) (in module logic1.theories.RCF.qe) (in module logic1.theories.RCF.redlog) (in module logic1.theories.Sets.qe) qea() (in module logic1.theories.RCF.redlog)

QuantifiedFormula (class in logic1.firstorder.quantified) QuantifierElimination (class in logic1.abc.qe) (class in logic1.theories.Sets.qe) quantify() (logic1.firstorder.formula.Formula method) quo_rem() (logic1.theories.RCF.term.Term method) qvars() (logic1.firstorder.formula.Formula method)

R

Rat (class in logic1.theories.Complex.ast) RateFilter (class in logic1.support.logging) RationalNumber (in module logic1.theories.Complex.types) RCF_Evaluator (class in logic1.theories.Complex.qe) Re (class in logic1.theories.Complex.ast) Re() (in module logic1.theories.Complex.term) real_formula_to_rcf() (in module logic1.theories.Complex.qe) real_normal_form() (in module logic1.theories.Complex.qe) (logic1.theories.Complex.atomic.AtomicFormula method) real_part() (logic1.theories.Complex.term.Term method) RealAtomicFormula (class in logic1.theories.Complex.atomic) reduce() (logic1.theories.RCF.term.Term method)

ReprFormatter (class in logic1.theories.Complex.format) reset() (logic1.support.logging.Timer method) (logic1.theories.Complex.term.VariableSet method) RESTART (class in logic1.abc.simplify) restart() (logic1.abc.simplify.InternalRepresentation method) result (logic1.abc.qe.QuantifierElimination attribute) rhs (logic1.firstorder.boolean.Equivalent property) (logic1.firstorder.boolean.Implies property) (logic1.theories.Complex.atomic.AtomicFormula property) (logic1.theories.RCF.atomic.AtomicFormula property) (logic1.theories.Sets.atomic.Ne property) root_nodes (logic1.abc.qe.QuantifierElimination attribute)

S

set_normal_form() (logic1.theories.Complex.term.Term class method) set_rate() (logic1.support.logging.RateFilter method) set_reference_time() (logic1.support.logging.DeltaTimeFormatter method) simpl_at() (logic1.abc.simplify.Simplify method) (logic1.theories.Complex.simplify.Simplify method) Simplify (class in logic1.abc.simplify) (class in logic1.theories.Complex.simplify) (class in logic1.theories.RCF.simplify) (class in logic1.theories.Sets.simplify) simplify() (in module logic1.theories.Complex.simplify) (in module logic1.theories.RCF.redlog) (in module logic1.theories.RCF.simplify) (in module logic1.theories.Sets.simplify) (logic1.abc.bnf.BooleanNormalForm method) (logic1.abc.qe.Assumptions method) (logic1.abc.simplify.Simplify method) (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.Sets.atomic.AtomicFormula method) sort_key() (logic1.firstorder.term.Term method) (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) (logic1.theories.Sets.atomic.Variable method)

SortKey (class in logic1.theories.Complex.ast) (class in logic1.theories.Complex.term) (class in logic1.theories.RCF.term) square() (logic1.theories.RCF.term.DEFINITE static method) stack (logic1.firstorder.term.VariableSet property) (logic1.theories.Complex.term.VariableSet property) (logic1.theories.RCF.term.VariableSet property) (logic1.theories.Sets.atomic.VariableSet property) StrFormatter (class in logic1.theories.Complex.format) strict_part() (logic1.theories.RCF.atomic.AtomicFormula class method) subs() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.theories.Complex.ast.AST method) (logic1.theories.Complex.atomic.AtomicFormula method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.RCF.term.Term method) (logic1.theories.Sets.atomic.AtomicFormula method) (logic1.theories.Sets.atomic.Variable method) subs_linear_solution() (logic1.theories.RCF.term.Term method) substitute (logic1.theories.RCF.simplify.Options attribute) success_nodes (logic1.abc.qe.QuantifierElimination attribute) summands() (logic1.theories.RCF.term.Term method) symbols (logic1.theories.Complex.format.LatexFormatter attribute) (logic1.theories.Complex.format.ReprFormatter attribute) (logic1.theories.Complex.format.StrFormatter attribute)

T

T (in module logic1.firstorder.boolean) Term (class in logic1.firstorder.term) (class in logic1.theories.Complex.term) (class in logic1.theories.RCF.term) term (logic1.theories.Complex.term.SortKey attribute) term_to_complex() (in module logic1.theories.Complex.qe) time_final_simplification (logic1.abc.qe.QuantifierElimination attribute) time_import_failure_nodes (logic1.abc.qe.QuantifierElimination attribute) time_import_success_nodes (logic1.abc.qe.QuantifierElimination attribute) time_import_working_nodes (logic1.abc.qe.QuantifierElimination attribute) time_multiprocessing (logic1.abc.qe.QuantifierElimination attribute) time_start_all_workers (logic1.abc.qe.QuantifierElimination attribute)

time_start_first_worker (logic1.abc.qe.QuantifierElimination attribute) time_syncmanager_enter (logic1.abc.qe.QuantifierElimination attribute) time_syncmanager_exit (logic1.abc.qe.QuantifierElimination attribute) time_total (logic1.abc.qe.QuantifierElimination attribute) Timer (class in logic1.support.logging) to_complement() (logic1.firstorder.atomic.AtomicFormula method) to_nnf() (logic1.firstorder.formula.Formula method) to_pnf() (logic1.firstorder.formula.Formula method) total_degree (logic1.theories.Complex.normalize.AddSortKey attribute) traditional_guards (logic1.theories.RCF.qe.Options attribute) transform_atom() (logic1.abc.simplify.InternalRepresentation method) traverse() (logic1.firstorder.formula.Formula method)

U

UnaryOperation (class in logic1.theories.Complex.ast)

UNKNOWN (logic1.theories.RCF.term.DEFINITE attribute) UPolynomial (class in logic1.theories.RCF.types)

V

value (logic1.theories.Complex.ast.Rat attribute) Var (class in logic1.theories.Complex.ast) var (logic1.firstorder.quantified.QuantifiedFormula property) Variable (class in logic1.firstorder.term) (class in logic1.theories.Complex.term) (class in logic1.theories.RCF.term) (class in logic1.theories.Sets.atomic) variables (logic1.abc.qe.Node attribute) VariableSet (class in logic1.firstorder.term) (class in logic1.theories.Complex.term) (class in logic1.theories.RCF.term) (class in logic1.theories.Sets.atomic) VariableSubstitutor (class in logic1.theories.Complex.ast) vars() (logic1.firstorder.term.Term method) (logic1.theories.Complex.term.Term method) (logic1.theories.RCF.term.Term method) (logic1.theories.Sets.atomic.Variable method) VirtualSubstitution (class in logic1.theories.RCF.qe) visit_add() (logic1.theories.Complex.ast.ASTVisitor method) (logic1.theories.Complex.ast.IdentityASTVisitor method) (logic1.theories.Complex.format.ReprFormatter method) (logic1.theories.Complex.normalize.ArithmeticEvaluator method) (logic1.theories.Complex.normalize.WeakNormalizer method) visit_conj() (logic1.theories.Complex.ast.ASTVisitor method) (logic1.theories.Complex.ast.IdentityASTVisitor method) (logic1.theories.Complex.format.LatexFormatter method) (logic1.theories.Complex.format.ReprFormatter method) (logic1.theories.Complex.normalize.ConstantEvaluator method) (logic1.theories.Complex.normalize.Normalizer method) (logic1.theories.Complex.normalize.WeakNormalizer method) (logic1.theories.Complex.qe.RCF_Evaluator method) visit_i() (logic1.theories.Complex.ast.ASTVisitor method) (logic1.theories.Complex.ast.IdentityASTVisitor method) (logic1.theories.Complex.format.ReprFormatter method) (logic1.theories.Complex.normalize.ConstantEvaluator method) (logic1.theories.Complex.qe.RCF_Evaluator method) visit_im() (logic1.theories.Complex.ast.ASTVisitor method) (logic1.theories.Complex.ast.IdentityASTVisitor method) (logic1.theories.Complex.format.ReprFormatter method) (logic1.theories.Complex.normalize.ConjugateNormalizer method) (logic1.theories.Complex.normalize.ConstantEvaluator method) (logic1.theories.Complex.normalize.Normalizer method) (logic1.theories.Complex.normalize.WeakNormalizer method) (logic1.theories.Complex.qe.RCF_Evaluator method)

visit_mul() (logic1.theories.Complex.ast.ASTVisitor method) (logic1.theories.Complex.ast.IdentityASTVisitor method) (logic1.theories.Complex.format.ReprFormatter method) (logic1.theories.Complex.normalize.ArithmeticEvaluator method) (logic1.theories.Complex.normalize.Normalizer method) (logic1.theories.Complex.normalize.WeakNormalizer method) visit_neg() (logic1.theories.Complex.ast.ASTVisitor method) (logic1.theories.Complex.ast.IdentityASTVisitor method) (logic1.theories.Complex.format.ReprFormatter method) (logic1.theories.Complex.normalize.ArithmeticEvaluator method) (logic1.theories.Complex.normalize.Normalizer method) (logic1.theories.Complex.normalize.WeakNormalizer method) visit_pow() (logic1.theories.Complex.ast.ASTVisitor method) (logic1.theories.Complex.ast.IdentityASTVisitor method) (logic1.theories.Complex.format.LatexFormatter method) (logic1.theories.Complex.format.ReprFormatter method) (logic1.theories.Complex.normalize.ArithmeticEvaluator method) (logic1.theories.Complex.normalize.Normalizer method) (logic1.theories.Complex.normalize.WeakNormalizer method) visit_rat() (logic1.theories.Complex.ast.ASTVisitor method) (logic1.theories.Complex.ast.IdentityASTVisitor method) (logic1.theories.Complex.format.LatexFormatter method) (logic1.theories.Complex.format.ReprFormatter method) (logic1.theories.Complex.normalize.ConstantEvaluator method) (logic1.theories.Complex.qe.RCF_Evaluator method) visit_re() (logic1.theories.Complex.ast.ASTVisitor method) (logic1.theories.Complex.ast.IdentityASTVisitor method) (logic1.theories.Complex.format.ReprFormatter method) (logic1.theories.Complex.normalize.ConjugateNormalizer method) (logic1.theories.Complex.normalize.ConstantEvaluator method) (logic1.theories.Complex.normalize.Normalizer method) (logic1.theories.Complex.normalize.WeakNormalizer method) (logic1.theories.Complex.qe.RCF_Evaluator method) visit_var() (logic1.theories.Complex.ast.ASTVisitor method) (logic1.theories.Complex.ast.IdentityASTVisitor method) (logic1.theories.Complex.ast.VariableSubstitutor method) (logic1.theories.Complex.format.LatexFormatter method) (logic1.theories.Complex.format.ReprFormatter method) (logic1.theories.Complex.normalize.ConstantEvaluator method) (logic1.theories.Complex.qe.RCF_Evaluator method) VV (in module logic1.theories.Complex.term) (in module logic1.theories.RCF.term) (in module logic1.theories.Sets.atomic)

W

WeakNormalizer (class in logic1.theories.Complex.normalize) workers (logic1.abc.qe.Options attribute) (logic1.theories.RCF.qe.Options attribute)

working_nodes (logic1.abc.qe.QuantifierElimination attribute) WorkingNodeList (class in logic1.abc.qe)

X

xopt (logic1.theories.RCF.qe.Options attribute)

Z

ZERO (logic1.theories.RCF.term.DEFINITE attribute)

Α

α (class in logic1.theories.Complex.types) (in module logic1.abc.bnf) (in module logic1.abc.qe) (in module logic1.abc.simplify) (in module logic1.firstorder.atomic) (in module logic1.firstorder.formula)

Η

η (class in logic1.theories.Complex.types)

Ι

ι (in module logic1.abc.qe)

Κ

κ (in module logic1.firstorder.atomic)

Λ

λ (in module logic1.abc.qe)

Μ

μ (in module logic1.abc.qe)

Ν

ν (in module logic1.abc.qe)

Ρ

ρ (in module logic1.abc.simplify)

Σ

σ (in module logic1.abc.bnf) (in module logic1.abc.qe) (in module logic1.abc.simplify) (in module logic1.firstorder.atomic) (in module logic1.firstorder.formula)

Τ

τ (class in logic1.theories.Complex.types) (in module logic1.abc.bnf) (in module logic1.abc.qe) (in module logic1.abc.simplify) (in module logic1.firstorder.atomic) (in module logic1.firstorder.formula) (in module logic1.theories.RCF.term.term_sage)

Χ

χ (in module logic1.abc.bnf) (in module logic1.abc.qe) (in module logic1.abc.simplify) (in module logic1.firstorder.atomic) (in module logic1.firstorder.formula)

Ω

ω (in module logic1.abc.qe) (in module logic1.abc.simplify)