<commit_before>#lang racket
(require "z3o.rkt" "common.rkt" "spec/utils.rkt")
(provide z3-prepare z3-clean z3-namelines cassius-check-sat)

(define to-resolve
  (append
   '(get/elt &box &pelt &velt &nelt &felt &lelt)
   '(get/box &elt &pbox &vbox &nbox &fbox &lbox)
   '(&pbflow &ppflow &vflow &nflow &flt &flt-up)
   '(fid)
   (for/list ([(name p) (in-dict (extra-pointers))] [i (in-naturals)])
     (sformat "&~a" i))))

(define to-expand
  (append
   '(link-element link-box)
   '(match-element-box match-anon-box match-anon-element)
   '(link-flow-simple link-flow-root link-flow-block)
   '(float position box-in-flow box-positioned)
   '(compute-style)
   '(pelt velt nelt felt lelt)
   '(pbox fbox lbox vbox nbox)
   '(pflow fflow lflow nflow vflow)
   '(ppflow pbflow flt)
   '(box-elt elt-box)))

(define to-expand-2
  (append
   '(an-inline-box a-text-box a-line-box a-block-box)
   '(a-block-flow-box a-block-float-box a-block-positioned-box an-anon-block-box a-view-box)
   '(positioned-horizontal-layout positioned-vertical-layout)))

(define ((unless-debug f) cmds)
  (if (*debug*)
      cmds
      (f cmds)))

(define *emitter-passes*
  (list
   (z3-ground-quantifiers 'Box)
   z3-fix-rational
   z3-unlet ; LETs are weirdly slow for some reason
   (z3-resolve-fns)
   #;z3-dco
   (z3-expand to-expand)
   (z3-expand to-expand-2)
   z3-unlet
   ;z3-simplif
   z3-assert-and
   ;(apply z3-resolve-fns to-resolve)
   ;(z3-sink-fields-and 'get/box 'get/elt 'is-box 'is-no-box 'is-elt 'is-no-elt)
   ;(z3-expand to-expand-2 #:clear true)<commit_msg>Stop expanding ppflow<commit_after>#lang racket
(require "z3o.rkt" "common.rkt" "spec/utils.rkt")
(provide z3-prepare z3-clean z3-namelines cassius-check-sat)

(define to-resolve
  (append
   '(get/elt &box &pelt &velt &nelt &felt &lelt)
   '(get/box &elt &pbox &vbox &nbox &fbox &lbox)
   '(&pbflow &vflow &nflow)
   '(fid)
   (for/list ([(name p) (in-dict (extra-pointers))] [i (in-naturals)])
     (sformat "&~a" i))))

(define to-expand
  (append
   '(link-element link-box)
   '(match-element-box match-anon-box)
   '(link-flow-root link-flow-simple link-flow-block)
   '(float position box-in-flow box-positioned)
   '(compute-style)
   '(pelt velt nelt felt lelt)
   '(pbox fbox lbox vbox nbox)
   '(pflow fflow lflow nflow vflow)
   '(ppflow pbflow flt)
   '(box-elt)))

(define to-expand-2
  (append
   '(an-inline-box a-text-box a-line-box a-block-box)
   '(a-block-flow-box a-block-float-box a-block-positioned-box an-anon-block-box a-view-box)
   '(positioned-horizontal-layout positioned-vertical-layout)))

(define ((unless-debug f) cmds)
  (if (*debug*)
      cmds
      (f cmds)))

(define *emitter-passes*
  (list
   (z3-ground-quantifiers 'Box)
   z3-fix-rational
   z3-unlet ; LETs are weirdly slow for some reason
   (z3-resolve-fns)
   #;z3-dco
   (z3-expand to-expand)
   (z3-expand to-expand-2)
   z3-unlet
   ;z3-simplif
   z3-assert-and
   ;(apply z3-resolve-fns to-resolve)
   ;(z3-sink-fields-and 'get/box 'get/elt 'is-box 'is-no-box 'is-elt 'is-no-elt)
   ;(z3-expand to-expand-2 #:clear true)
{'fraction_non_alphanumeric': 0.1709928617780662, 'fraction_numerical': 0.012978585334198572, 'mean_word_length': 3.223287671232877, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '568011', 'n_tokens_mistral': 1332, 'n_tokens_neox': 1284, 'n_words': 278}