Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.Util

Returns true if the variables in the given polynomial are sorted in decreasing order.

Equations
Instances For

    Returns true if the cutsat state is inconsistent.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[extern lean_grind_cutsat_mk_var]

      Creates a new variable in the cutsat module.

      Returns true if e is already associated with a cutsat variable.

      Equations
      Instances For

        Returns true if x has been eliminated using an equality constraint.

        Equations
        Instances For
          @[extern lean_grind_cutsat_assert_eq]

          Resets the assignment of any variable bigger or equal to x.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            Equations
            Instances For
              Equations
              Instances For
                Equations
                Instances For
                  Equations
                  Instances For
                    Equations
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        Equations
                        Instances For
                          Equations
                          Instances For
                            Equations
                            Instances For
                              @[extern lean_grind_cutsat_assert_le]
                              Equations
                              Instances For
                                Equations
                                Instances For
                                  Equations
                                  Instances For
                                    Equations
                                    Instances For
                                      Equations
                                      Instances For
                                        Equations
                                        Instances For
                                          Equations
                                          Instances For
                                            Equations
                                            Instances For

                                              Returns occurrences of x.

                                              Equations
                                              Instances For

                                                Adds y as an occurrence of x. That is, x occurs in lowers[y], uppers[y], or dvdCnstrs[y].

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For

                                                  Given p a polynomial being inserted into lowers, uppers, or dvdCnstrs, get its leading variable y, and adds y as an occurrence for the remaining variables in p.

                                                  Equations
                                                  Instances For

                                                    Tries to evaluate the polynomial p using the partial model/assignment built so far. The result is none if the polynomial contains variables that have not been assigned.

                                                    Equations
                                                    Instances For
                                                      @[reducible, inline]
                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]
                                                        Equations
                                                        Instances For

                                                          Returns .true if c is satisfied by the current partial model, .undef if c contains unassigned variables, and .false otherwise.

                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            Equations
                                                            Instances For

                                                              Returns .true if c is satisfied by the current partial model, .undef if c contains unassigned variables, and .false otherwise.

                                                              Equations
                                                              Instances For

                                                                Returns .true if c is satisfied by the current partial model, .undef if c contains unassigned variables, and .false otherwise.

                                                                Equations
                                                                Instances For

                                                                  Given a polynomial p, returns some (x, k, c) if p contains the monomial k*x, and x has been eliminated using the equality c.

                                                                  Equations
                                                                  Instances For
                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For