Documentation

Lean.Meta.Tactic.Grind.Arith.Cutsat.Search

Asserts constraints implied by a CooperSplit.

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

      Assuming all variables smaller than x have already been assigned, returns the best lower bound for x using the given partial assignment and inequality constraints where x is the maximal variable.

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

        Assuming all variables smaller than x have already been assigned, returns the best upper bound for x using the given partial assignment and inequality constraints where x is the maximal variable.

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

          Returns values we cannot assign x because of disequality constraints.

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

            Solution space for a divisibility constraint of the form d ∣ a*x + b See DvdCnstr.getSolutions? to understand how it is computed.

            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

                  Given a divisibility constraint solution space s := { b, d }, and a candidate assignment v, we want to find an assignment w such that w ≥ v such that exists k, w = k*d + b Thus,

                  • k*d + b ≥ v
                  • k ≥ cdiv (v - b) d So, we take w = (cdiv (v - b) d)*d + b
                  Equations
                  Instances For

                    Given a divisibility constraint solution space s := { b, d }, and a candidate assignment v, we want to find an assignment w such that w ≤ v such that exists k, w = k*d + b Thus,

                    • k*d + b ≤ v
                    • k ≤ (v - b) / d So, we take w = ((v - b) / d)*d + b
                    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

                          Tries to find an integer v s.t. lower ≤ v ≤ upper, v ∉ dvals, and v ∈ s. Returns .found v if result was found, .dvd if it failed because of the divisibility constraint, and .diseq c because of the disequality constraint c.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            partial def Lean.Meta.Grind.Arith.Cutsat.findRatVal (lower upper : Rat) (diseqVals : Array (Rat × DiseqCnstr)) :
                            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
                                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
                                    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

                                        Given c₁ of the form a₁*x + p₁ ≠ 0, and c₂ of the form b*x + p ≤ 0 splits c₁ and resolve with c₂.

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

                                          Given c₁ of the form -a₁*x + p₁ ≤ 0, and c of the form b*x + p ≠ 0, splits c and resolve with c₁.

                                          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

                                              Returns true if we already have a complete assignment / model.

                                              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
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For