products/sources/formale Sprachen/PVS/ACCoRD/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: Lisp

Original von: PVS©
(wedge_optimum_2D
 (intersects_segment_fun?_TCC1 0
  (intersects_segment_fun?_TCC1-1 nil 3530552207
   ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (* const-decl "real" vectors_2D "vectors/")
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (intersects_segment_fun?_TCC2 0
  (intersects_segment_fun?_TCC2-1 nil 3530552207
   ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (intersects_segment_fun?_TCC3 0
  (intersects_segment_fun?_TCC3-1 nil 3530552207
   ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (intersects_segment_fun?_TCC4 0
  (intersects_segment_fun?_TCC4-1 nil 3530552207
   ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (intersects_segment_fun_def 0
  (intersects_segment_fun_def-3 nil 3530552296
   (""
    (case "FORALL (p,w,v,a,b,e1,e2): intersects_segment_fun?(p,w,v,a,b,e1,e2) = intersects_segment?(p,w,v,a,b,e1,e2)")
    (("1" (decompose-equality) nil nil)
     ("2" (hide 2)
      (("2" (skeep)
        (("2" (expand "intersects_segment_fun?")
          (("2"
            (name "tlow1" "IF v * e1 > 0 THEN ((p - w) * e1) / (v * e1)
                                         ELSIF v * e1 = 0 AND (w - p) * e1 < 0 THEN 1 + b
                                         ELSE a
                                         ENDIF")
            (("1" (replace -1)
              (("1"
                (name "thigh1"
                      "IF v * e1 < 0 THEN ((p - w) * e1) / (v * e1)
                                                 ELSIF v * e1 = 0 AND (w - p) * e1 < 0 THEN a - 1
                                                 ELSE b
                                                 ENDIF")
                (("1" (replace -1)
                  (("1"
                    (name "tlow2"
                          "IF v * e2 > 0 THEN ((p - w) * e2) / (v * e2)
                                                     ELSIF v * e2 = 0 AND (w - p) * e2 < 0 THEN 2 + b
                                                     ELSE a
                                                     ENDIF")
                    (("1" (replace -1)
                      (("1"
                        (name "thigh2"
                              "IF v * e2 < 0 THEN ((p - w) * e2) / (v * e2)
                                                             ELSIF v * e2 = 0 AND (w - p) * e2 < 0 THEN a - 2
                                                             ELSE b
                                                             ENDIF")
                        (("1" (replace -1)
                          (("1" (name "tlow" "max(max(tlow1,tlow2),a)")
                            (("1" (replace -1)
                              (("1"
                                (name
                                 "thigh"
                                 "min(min(thigh1,thigh2),b)")
                                (("1"
                                  (replace -1)
                                  (("1"
                                    (case
                                     "NOT (FORALL (t:real): (a<=t AND t<=b AND (w+t*v-p)*e1>=0 AND (w+t*v-p)*e2>=0) IFF (tlow <= t AND t<=thigh))")
                                    (("1"
                                      (hide-all-but 1)
                                      (("1"
                                        (skeep)
                                        (("1"
                                          (ground)
                                          (("1"
                                            (expand "tlow")
                                            (("1"
                                              (case
                                               "t>=tlow1 AND t>=tlow2")
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (expand "max")
                                                  (("1"
                                                    (lift-if)
                                                    (("1"
                                                      (lift-if)
                                                      (("1"
                                                        (lift-if)
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide 2)
                                                (("2"
                                                  (split +)
                                                  (("1"
                                                    (expand "tlow1")
                                                    (("1"
                                                      (lift-if)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (ground)
                                                          (("1"
                                                            (cross-mult
                                                             1)
                                                            (("1"
                                                              (hide-all-but
                                                               (-4 1))
                                                              (("1"
                                                                (grind)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide-all-but
                                                             (-1
                                                              -2
                                                              -5))
                                                            (("2"
                                                              (grind)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (expand "tlow2")
                                                    (("2"
                                                      (lift-if)
                                                      (("2"
                                                        (assert)
                                                        (("2"
                                                          (ground)
                                                          (("1"
                                                            (cross-mult
                                                             1)
                                                            (("1"
                                                              (hide-all-but
                                                               (-5 1))
                                                              (("1"
                                                                (grind)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide-all-but
                                                             (-1
                                                              -2
                                                              -6))
                                                            (("2"
                                                              (grind)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("3"
                                                (assert)
                                                (("3"
                                                  (flatten)
                                                  (("3"
                                                    (expand "tlow2" 1)
                                                    (("3"
                                                      (ground)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "thigh")
                                            (("2"
                                              (case
                                               "t<=thigh1 AND t<=thigh2")
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (expand "min")
                                                  (("1"
                                                    (lift-if)
                                                    (("1"
                                                      (lift-if)
                                                      (("1"
                                                        (lift-if)
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide 2)
                                                (("2"
                                                  (split +)
                                                  (("1"
                                                    (expand "thigh1")
                                                    (("1"
                                                      (lift-if)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (ground)
                                                          (("1"
                                                            (cross-mult
                                                             1)
                                                            (("1"
                                                              (hide-all-but
                                                               (-4 1))
                                                              (("1"
                                                                (grind)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide-all-but
                                                             (-1
                                                              -2
                                                              -5))
                                                            (("2"
                                                              (grind)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (expand "thigh2")
                                                    (("2"
                                                      (lift-if)
                                                      (("2"
                                                        (assert)
                                                        (("2"
                                                          (ground)
                                                          (("1"
                                                            (cross-mult
                                                             1)
                                                            (("1"
                                                              (hide-all-but
                                                               (-5 1))
                                                              (("1"
                                                                (grind)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (hide-all-but
                                                             (-1
                                                              -2
                                                              -6))
                                                            (("2"
                                                              (grind)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("3"
                                                (flatten)
                                                (("3"
                                                  (hide 2)
                                                  (("3"
                                                    (expand "thigh2" 1)
                                                    (("3"
                                                      (ground)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("3"
                                            (expand "tlow")
                                            (("3"
                                              (expand "thigh")
                                              (("3"
                                                (case
                                                 "t>=tlow1 AND t<=thigh1")
                                                (("1"
                                                  (hide (-2 -3))
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (expand "thigh1")
                                                      (("1"
                                                        (expand
                                                         "tlow1")
                                                        (("1"
                                                          (lift-if)
                                                          (("1"
                                                            (split -)
                                                            (("1"
                                                              (flatten)
                                                              (("1"
                                                                (cross-mult
                                                                 -2)
                                                                (("1"
                                                                  (hide-all-but
                                                                   (-2
                                                                    1))
                                                                  (("1"
                                                                    (grind)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (flatten)
                                                              (("2"
                                                                (split
                                                                 -)
                                                                (("1"
                                                                  (flatten)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (flatten)
                                                                  (("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (split
                                                                       -)
                                                                      (("1"
                                                                        (flatten)
                                                                        (("1"
                                                                          (cross-mult
                                                                           -2)
                                                                          (("1"
                                                                            (hide-all-but
                                                                             (-2
                                                                              3))
                                                                            (("1"
                                                                              (grind)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (flatten)
                                                                        (("2"
                                                                          (assert)
                                                                          (("2"
                                                                            (split
                                                                             -)
                                                                            (("1"
                                                                              (propax)
                                                                              nil
                                                                              nil)
                                                                             ("2"
                                                                              (case
                                                                               "v*e1 = 0")
                                                                              (("1"
                                                                                (mult-by
                                                                                 -1
                                                                                 "t")
                                                                                (("1"
                                                                                  (hide-all-but
                                                                                   (-1
                                                                                    1
                                                                                    5))
                                                                                  (("1"
                                                                                    (grind)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (expand "min")
                                                  (("2"
                                                    (expand "max")
                                                    (("2"
                                                      (lift-if)
                                                      (("2"
                                                        (lift-if)
                                                        (("2"
                                                          (lift-if)
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (ground)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (flatten)
                                                  (("3"
                                                    (expand "thigh1" +)
                                                    (("3"
                                                      (ground)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("4"
                                            (expand "thigh")
                                            (("4"
                                              (expand "tlow")
                                              (("4"
                                                (case
                                                 "tlow2 <= t AND t<=thigh2")
                                                (("1"
                                                  (hide (-2 -3))
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (expand "thigh2")
                                                      (("1"
                                                        (expand
                                                         "tlow2")
                                                        (("1"
                                                          (lift-if)
                                                          (("1"
                                                            (split -)
                                                            (("1"
                                                              (flatten)
                                                              (("1"
                                                                (cross-mult
                                                                 -2)
                                                                (("1"
                                                                  (hide-all-but
                                                                   (-2
                                                                    1))
                                                                  (("1"
                                                                    (grind)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (flatten)
                                                              (("2"
                                                                (split
                                                                 -)
                                                                (("1"
                                                                  (flatten)
                                                                  (("1"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (flatten)
                                                                  (("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (split
                                                                       -)
                                                                      (("1"
                                                                        (flatten)
                                                                        (("1"
                                                                          (cross-mult
                                                                           -2)
                                                                          (("1"
                                                                            (hide-all-but
                                                                             (-2
                                                                              3))
                                                                            (("1"
                                                                              (grind)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (flatten)
                                                                        (("2"
                                                                          (ground)
                                                                          (("2"
                                                                            (case
                                                                             "v*e2 = 0")
                                                                            (("1"
                                                                              (mult-by
                                                                               -1
                                                                               "t")
                                                                              (("1"
                                                                                (hide-all-but
                                                                                 (-1
                                                                                  1
                                                                                  5))
                                                                                (("1"
                                                                                  (grind)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (assert)
                                                                              nil
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (expand "min")
                                                  (("2"
                                                    (expand "max")
                                                    (("2"
                                                      (lift-if)
                                                      (("2"
                                                        (lift-if)
                                                        (("2"
                                                          (lift-if)
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (ground)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("3"
                                                  (flatten)
                                                  (("3"
                                                    (expand "thigh2" +)
                                                    (("3"
                                                      (ground)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide-all-but (-1 1))
                                      (("2"
                                        (iff)
                                        (("2"
                                          (ground)
                                          (("1"
                                            (inst - "tlow")
                                            (("1"
                                              (expand
                                               "intersects_segment?")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (inst + "tlow")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand
                                             "intersects_segment?")
                                            (("2"
                                              (skeep -1)
                                              (("2"
                                                (inst - "t")
                                                (("2"
                                                  (assert)
                                                  (("2"
                                                    (ground)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide-all-but 1)
                                  (("2"
                                    (expand "thigh2")
                                    (("2" (ground) nil nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (hide-all-but 1)
                                  (("3"
                                    (expand "thigh1")
                                    (("3" (ground) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (hide-all-but 1)
                              (("2"
                                (expand "tlow2")
                                (("2" (ground) nil nil))
                                nil))
                              nil)
                             ("3" (hide-all-but 1)
                              (("3"
                                (expand "tlow1")
                                (("3" (ground) nil nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide-all-but 1) (("2" (ground) nil nil))
                          nil))
                        nil))
                      nil)
                     ("2" (hide-all-but 1) (("2" (ground) nil nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but 1) (("2" (ground) nil nil)) nil))
                nil))
              nil)
             ("2" (hide-all-but 1) (("2" (ground) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (div_mult_pos_ge2 formula-decl nil real_props nil)
    (tlow1 skolem-const-decl "numfield" wedge_optimum_2D nil)
    (tlow2 skolem-const-decl "numfield" wedge_optimum_2D nil)
    (tlow skolem-const-decl
     "{p: real | p >= max(tlow1, tlow2) AND p >= a}" wedge_optimum_2D
     nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (div_mult_neg_le2 formula-decl nil real_props nil)
    (thigh1 skolem-const-decl "numfield" wedge_optimum_2D nil)
    (thigh2 skolem-const-decl "numfield" wedge_optimum_2D nil)
    (thigh skolem-const-decl
     "{p: real | p <= min(thigh1, thigh2) AND p <= b}" wedge_optimum_2D
     nil)
    (both_sides_times1_imp formula-decl nil extra_real_props nil)
    (v skolem-const-decl "Vect2" wedge_optimum_2D nil)
    (e1 skolem-const-decl "Nz_vect2" wedge_optimum_2D nil)
    (e2 skolem-const-decl "Nz_vect2" wedge_optimum_2D nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (* const-decl "Vector" vectors_2D "vectors/")
    (+ const-decl "Vector" vectors_2D "vectors/")
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (<= const-decl "bool" reals nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (>= const-decl "bool" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (> const-decl "bool" reals nil)
    (* const-decl "real" vectors_2D "vectors/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (intersects_segment_fun? const-decl "bool" wedge_optimum_2D nil)
    (intersects_segment? const-decl "bool" wedge_optimum_2D nil))
   nil)
  (intersects_segment_fun_def-2 nil 3530552265
   ("" (skeep)
    ((""
      (name "mspis"
            "max_segment_point_in_slice(p, w, v, a, b, e1, e2)")
      (("" (label "mspisdef" -1)
        (("" (replace -1)
          (("" (assert)
            (("" (expand "max_segment_point_in_slice")
              ((""
                (name "tlow1"
                      "IF v * e1 > 0 THEN ((p - w) * e1) / (v * e1)
                                  ELSIF v * e1 = 0 AND (w - p) * e1 < 0 THEN 1 + b
                                  ELSE a
                                  ENDIF")
                (("1" (replace -1)
                  (("1"
                    (name "thigh1"
                          "IF v * e1 < 0 THEN ((p - w) * e1) / (v * e1)
                                        ELSIF v * e1 = 0 AND (w - p) * e1 < 0 THEN a - 1
                                        ELSE b
                                        ENDIF")
                    (("1" (replace -1)
                      (("1"
                        (name "tlow2"
                              "IF v * e2 > 0 THEN ((p - w) * e2) / (v * e2)
                                          ELSIF v * e2 = 0 AND (w - p) * e2 < 0 THEN 2 + b
                                          ELSE a
                                          ENDIF")
                        (("1" (replace -1)
                          (("1"
                            (name "thigh2"
                                  "IF v * e2 < 0 THEN ((p - w) * e2) / (v * e2)
                                                ELSIF v * e2 = 0 AND (w - p) * e2 < 0 THEN a - 2
                                                ELSE b
                                                ENDIF")
                            (("1" (replace -1)
                              (("1"
                                (case "v = zero")
                                (("1"
                                  (replace -1)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (replace "mspisdef" :dir rl)
                                      (("1"
                                        (split +)
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (expand
                                             "on_segment_in_wedge?")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (expand
                                                 "intersects_segment?")
                                                (("1"
                                                  (skeep -1)
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (inst + "t")
                                                      (("1"
                                                        (assert)
                                                        nil)))))))))))))))
                                         ("2"
                                          (skeep)
                                          (("2"
                                            (expand
                                             "on_segment_in_wedge?")
                                            (("2"
                                              (skeep -1)
                                              (("2"
                                                (assert)
                                                nil)))))))))))))))
                                 ("2"
                                  (label "vnz" 1)
                                  (("2"
                                    (hide "vnz")
                                    (("2"
                                      (name
                                       "tlow"
                                       "max(max(tlow1,tlow2),a)")
                                      (("1"
                                        (replace -1)
                                        (("1"
                                          (name
                                           "thigh"
                                           "min(min(thigh1,thigh2),b)")
                                          (("1"
                                            (replace -1)
                                            (("1"
                                              (name "aa" "sqv(v)")
                                              (("1"
                                                (replace -1)
                                                (("1"
                                                  (name
                                                   "bb"
                                                   "2*(v*(w-p))")
                                                  (("1"
                                                    (copy -1)
                                                    (("1"
                                                      (mult-by
                                                       -1
                                                       "tlow")
                                                      (("1"
                                                        (replace -1)
                                                        (("1"
                                                          (copy -2)
                                                          (("1"
                                                            (mult-by
                                                             -1
                                                             "thigh")
                                                            (("1"
                                                              (replace
                                                               -1)
                                                              (("1"
                                                                (hide
                                                                 (-1
                                                                  -2))
                                                                (("1"
                                                                  (name
                                                                   "cc"
                                                                   "sqv(w-p)")
                                                                  (("1"
                                                                    (case
                                                                     "NOT (FORALL (t:real): (a<=t AND t<=b AND (w+t*v-p)*e1>=0 AND (w+t*v-p)*e2>=0) IFF (tlow <= t AND t<=thigh))")
                                                                    (("1"
                                                                      (hide-all-but
                                                                       1)
                                                                      (("1"
                                                                        (skeep)
                                                                        (("1"
                                                                          (ground)
                                                                          (("1"
                                                                            (expand
                                                                             "tlow")
                                                                            (("1"
                                                                              (case
                                                                               "t>=tlow1 AND t>=tlow2")
                                                                              (("1"
                                                                                (flatten)
                                                                                (("1"
                                                                                  (expand
                                                                                   "max")
                                                                                  (("1"
                                                                                    (lift-if)
                                                                                    (("1"
                                                                                      (lift-if)
                                                                                      (("1"
                                                                                        (lift-if)
                                                                                        (("1"
                                                                                          (assert)
                                                                                          nil)))))))))))
                                                                               ("2"
                                                                                (hide
                                                                                 2)
                                                                                (("2"
                                                                                  (split
                                                                                   +)
                                                                                  (("1"
                                                                                    (expand
                                                                                     "tlow1")
                                                                                    (("1"
                                                                                      (lift-if)
                                                                                      (("1"
                                                                                        (assert)
                                                                                        (("1"
                                                                                          (ground)
                                                                                          (("1"
                                                                                            (cross-mult
                                                                                             1)
                                                                                            (("1"
                                                                                              (hide-all-but
                                                                                               (-4
                                                                                                1))
                                                                                              (("1"
                                                                                                (grind)
                                                                                                nil)))))
                                                                                           ("2"
                                                                                            (hide-all-but
                                                                                             (-1
                                                                                              -2
                                                                                              -5))
                                                                                            (("2"
                                                                                              (grind)
                                                                                              nil)))))))))))
                                                                                   ("2"
                                                                                    (expand
                                                                                     "tlow2")
                                                                                    (("2"
                                                                                      (lift-if)
                                                                                      (("2"
                                                                                        (assert)
                                                                                        (("2"
                                                                                          (ground)
                                                                                          (("1"
                                                                                            (cross-mult
                                                                                             1)
                                                                                            (("1"
                                                                                              (hide-all-but
                                                                                               (-5
                                                                                                1))
                                                                                              (("1"
                                                                                                (grind)
                                                                                                nil)))))
                                                                                           ("2"
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.95 Sekunden  (vorverarbeitet)  ¤



zum Wurzelverzeichnis wechseln
Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln
sprechenden Kalenders

in der Quellcodebibliothek suchen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff