Ar Table

Implementing Algebraic Reasoning (AR).

class ARTable

Bases: object

The coefficient matrix.

expr_delta(vc)

There is only constant delta between vc and the system

Return type:: bool

substitute_in_existing_expressions(vc)

Return type:: Expr

add_expr(expression, predicate)

Add a new equality (sum cv = 0), represented by the list of tuples vc=[(v, c), ..]. Return True iff the equality can already be deduced by the internal system

Return type:: bool

why_expr(vc)

AR traceback == MILP.

Return type:: tuple[Circumcenter | Cong | Coll | NColl | Cyclic | ConstantAngle | ACompute | LCompute | ConstantLength | ConstantRatio | EqAngle | Diff | RCompute | ObtuseAngle | MidPoint | EqRatio | Perp | NPerp | Para | NPara | SameClock | SameSide | NSameSide | PythagoreanPremises | PythagoreanConclusions | SquaredConstantLength | SquaredConstantRatio | SimtriClock | SimtriReflect | ContriClock | ContriReflect | AngleEquation | LengthEquation, ...]