Index _ | A | B | C | D | E | F | G | I | L | M | N | O | P | Q | R | S | T | V | W | Α | Ι | Λ | Ν | Ρ | Σ | Τ | Φ | Χ | Ω _ __add__() (logic1.theories.RCF.atomic.Term method) __and__() (logic1.firstorder.formula.Formula method) __bool__() (logic1.theories.RCF.atomic.AtomicFormula method) __call__() (logic1.abc.qe.QuantifierElimination method) __eq__() (logic1.theories.RCF.atomic.Term method) (logic1.theories.Sets.atomic.Variable method) __ge__() (logic1.theories.RCF.atomic.Term method) __getitem__() (logic1.firstorder.atomic.VariableSet method) (logic1.theories.RCF.atomic.VariableSet method) (logic1.theories.Sets.atomic.VariableSet method) __gt__() (logic1.theories.RCF.atomic.Term method) __init__() (logic1.firstorder.formula.Formula method) __invert__() (logic1.firstorder.formula.Formula method) __iter__() (logic1.theories.RCF.atomic.Term method) __le__() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.RCF.atomic.Term method) (logic1.theories.Sets.atomic.AtomicFormula method) __lshift__() (logic1.firstorder.formula.Formula method) __lt__() (logic1.theories.RCF.atomic.Term method) __mul__() (logic1.theories.RCF.atomic.Term method) __ne__() (logic1.theories.RCF.atomic.Term method) (logic1.theories.Sets.atomic.Variable method) __neg__() (logic1.theories.RCF.atomic.Term method) __or__() (logic1.firstorder.formula.Formula method) __pow__() (logic1.theories.RCF.atomic.Term method) __radd__() (logic1.theories.RCF.atomic.Term method) __rmul__() (logic1.theories.RCF.atomic.Term method) __rshift__() (logic1.firstorder.formula.Formula method) __rsub__() (logic1.theories.RCF.atomic.Term method) __str__() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.Sets.atomic.AtomicFormula method) __sub__() (logic1.theories.RCF.atomic.Term method) __truediv__() (logic1.theories.RCF.atomic.Term method) _F (class in logic1.firstorder.boolean) _repr_latex_() (logic1.firstorder.formula.Formula method) _T (class in logic1.firstorder.boolean) A add() (logic1.abc.simplify.InternalRepresentation method) All (class in logic1.firstorder.quantified) 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) args (logic1.firstorder.formula.Formula property) as_latex() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.atomic.Term method) (logic1.firstorder.formula.Formula method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.RCF.atomic.Term method) (logic1.theories.Sets.atomic.AtomicFormula method) (logic1.theories.Sets.atomic.Variable method) Assumptions (class in logic1.abc.qe) (class in logic1.theories.RCF.qe) (class in logic1.theories.Sets.qe) assumptions (logic1.abc.qe.QuantifierElimination property) Assumptions.Inconsistent (class in logic1.abc.qe.Assumptions) AtomicFormula (class in logic1.firstorder.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 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.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) CLUSTERING (class in logic1.theories.RCF.qe) 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.atomic.Term method) complement() (logic1.firstorder.atomic.AtomicFormula class method) (logic1.theories.RCF.atomic.AtomicFormula class method) (logic1.theories.Sets.atomic.AtomicFormula class method) constant_coefficient() (logic1.theories.RCF.atomic.Term method) content() (logic1.theories.RCF.atomic.Term method) converse() (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) 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() (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.RCF.atomic.Term method) DeltaTimeFormatter (class in logic1.support.logging) depth() (logic1.firstorder.formula.Formula method) derivative() (logic1.theories.RCF.atomic.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 Eq (class in logic1.theories.RCF.atomic) (class in logic1.theories.Sets.atomic) Equivalent (class in logic1.firstorder.boolean) Ex (class in logic1.firstorder.quantified) ex() (logic1.firstorder.formula.Formula method) extend() (logic1.abc.qe.Assumptions method) extract() (logic1.abc.simplify.InternalRepresentation method) F F (in module logic1.firstorder.boolean) factor() (logic1.theories.RCF.atomic.Term method) failure_nodes (logic1.abc.qe.QuantifierElimination attribute) final_simplify() (logic1.abc.qe.QuantifierElimination method) Formula (class in logic1.firstorder.formula) formula (logic1.abc.qe.Node attribute) fresh() (logic1.firstorder.atomic.Variable method) (logic1.theories.RCF.atomic.Variable method) (logic1.theories.RCF.atomic.VariableSet method) (logic1.theories.Sets.atomic.Variable method) (logic1.theories.Sets.atomic.VariableSet method) FULL (logic1.theories.RCF.qe.CLUSTERING attribute) (logic1.theories.RCF.qe.GENERIC attribute) fvars() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.Sets.atomic.AtomicFormula method) G Ge (class in logic1.theories.RCF.atomic) GENERIC (class in logic1.theories.RCF.qe) generic (logic1.theories.RCF.qe.Options attribute) get() (logic1.firstorder.atomic.VariableSet method) (logic1.support.logging.Timer method) get_reference_time() (logic1.support.logging.DeltaTimeFormatter method) Gt (class in logic1.theories.RCF.atomic) I imp() (logic1.firstorder.atomic.VariableSet method) 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.RCF.simplify) (class in logic1.theories.Sets.simplify) 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.RCF.atomic.Term method) is_definite() (logic1.theories.RCF.atomic.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_implies() (logic1.firstorder.formula.Formula static 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_term() (logic1.firstorder.formula.Formula static method) is_true() (logic1.firstorder.formula.Formula static method) is_valid() (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) is_zero() (logic1.theories.RCF.atomic.Term method) L lc() (logic1.theories.RCF.atomic.Term method) Le (class in logic1.theories.RCF.atomic) lhs (logic1.firstorder.boolean.Equivalent property) (logic1.firstorder.boolean.Implies property) (logic1.theories.RCF.atomic.AtomicFormula property) (logic1.theories.Sets.atomic.Ne property) log_level (logic1.abc.qe.Options attribute) log_rate (logic1.abc.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.support.excepthook module logic1.support.logging module logic1.theories.RCF module logic1.theories.RCF.atomic module logic1.theories.RCF.bnf module logic1.theories.RCF.qe module logic1.theories.RCF.simplify 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 Lt (class in logic1.theories.RCF.atomic) M matrix (logic1.abc.qe.QuantifierElimination attribute) matrix() (logic1.firstorder.formula.Formula 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.support.excepthook logic1.support.logging logic1.theories.RCF logic1.theories.RCF.atomic logic1.theories.RCF.bnf logic1.theories.RCF.qe logic1.theories.RCF.simplify logic1.theories.Sets logic1.theories.Sets.atomic logic1.theories.Sets.bnf logic1.theories.Sets.qe logic1.theories.Sets.simplify MONOMIAL (logic1.theories.RCF.qe.GENERIC attribute) monomials() (logic1.theories.RCF.atomic.Term method) N Ne (class in logic1.theories.RCF.atomic) (class in logic1.theories.Sets.atomic) negated (logic1.abc.qe.QuantifierElimination 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) Node (class in logic1.abc.qe) (class in logic1.theories.RCF.qe) (class in logic1.theories.Sets.qe) NONE (logic1.theories.RCF.atomic.TSQ attribute) (logic1.theories.RCF.qe.CLUSTERING attribute) (logic1.theories.RCF.qe.GENERIC attribute) Not (class in logic1.firstorder.boolean) NoTraceException 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) Options (class in logic1.abc.qe) (class in logic1.theories.RCF.qe) options (logic1.abc.qe.QuantifierElimination attribute) Or (class in logic1.firstorder.boolean) P pop() (logic1.firstorder.atomic.VariableSet method) (logic1.theories.RCF.atomic.VariableSet method) (logic1.theories.Sets.atomic.VariableSet method) Prefix (class in logic1.firstorder.quantified) process() (logic1.abc.qe.Node method) pseudo_quo_rem() (logic1.theories.RCF.atomic.Term method) push() (logic1.firstorder.atomic.VariableSet method) (logic1.theories.RCF.atomic.VariableSet method) (logic1.theories.Sets.atomic.VariableSet method) Q qe() (in module logic1.theories.RCF.qe) (in module logic1.theories.Sets.qe) 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.atomic.Term method) qvars() (logic1.firstorder.formula.Formula method) R RateFilter (class in logic1.support.logging) reset() (logic1.support.logging.Timer method) result (logic1.abc.qe.QuantifierElimination attribute) rhs (logic1.firstorder.boolean.Equivalent property) (logic1.firstorder.boolean.Implies property) (logic1.theories.RCF.atomic.AtomicFormula property) (logic1.theories.Sets.atomic.Ne property) root_nodes (logic1.abc.qe.QuantifierElimination attribute) S set_rate() (logic1.support.logging.RateFilter method) set_reference_time() (logic1.support.logging.DeltaTimeFormatter method) simpl_at() (logic1.abc.simplify.Simplify method) Simplify (class in logic1.abc.simplify) (class in logic1.theories.RCF.simplify) (class in logic1.theories.Sets.simplify) simplify() (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.RCF.atomic.AtomicFormula method) (logic1.theories.Sets.atomic.AtomicFormula method) sort_key() (logic1.firstorder.atomic.Term static method) (logic1.theories.RCF.atomic.Term static method) (logic1.theories.Sets.atomic.Variable static method) STRICT (logic1.theories.RCF.atomic.TSQ attribute) strict_part() (logic1.theories.RCF.atomic.AtomicFormula class method) subs() (logic1.firstorder.atomic.AtomicFormula method) (logic1.firstorder.formula.Formula method) (logic1.theories.RCF.atomic.AtomicFormula method) (logic1.theories.RCF.atomic.Term method) (logic1.theories.Sets.atomic.AtomicFormula method) (logic1.theories.Sets.atomic.Variable method) success_nodes (logic1.abc.qe.QuantifierElimination attribute) T T (in module logic1.firstorder.boolean) Term (class in logic1.firstorder.atomic) (class in logic1.theories.RCF.atomic) 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) traditional_guards (logic1.theories.RCF.qe.Options attribute) transform_atoms() (logic1.firstorder.formula.Formula method) TSQ (class in logic1.theories.RCF.atomic) V var (logic1.firstorder.quantified.QuantifiedFormula property) Variable (class in logic1.firstorder.atomic) (class in logic1.theories.RCF.atomic) (class in logic1.theories.Sets.atomic) variables (logic1.abc.qe.Node attribute) VariableSet (class in logic1.firstorder.atomic) (class in logic1.theories.RCF.atomic) (class in logic1.theories.Sets.atomic) vars() (logic1.firstorder.atomic.Term method) (logic1.theories.RCF.atomic.Term method) (logic1.theories.Sets.atomic.Variable method) VirtualSubstitution (class in logic1.theories.RCF.qe) VV (in module logic1.theories.RCF.atomic) (in module logic1.theories.Sets.atomic) W WEAK (logic1.theories.RCF.atomic.TSQ attribute) workers (logic1.abc.qe.QuantifierElimination attribute) working_nodes (logic1.abc.qe.QuantifierElimination attribute) Α α (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.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) Τ τ (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.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)