<commit_before>#lang racket

(require "eval.rkt" "state.rkt" "../base/assert.rkt" "../base/define.rkt" "cegis.rkt"
         "../config/log.rkt"
         (only-in "../base/reflect.rkt" symbolics)
         (only-in "../base/bool.rkt" || !)
         (only-in "../base/equality.rkt" @equal?)
         (only-in "../base/term.rkt" expression constant? typed? get-type type-deconstruct)
         "../solver/solver.rkt"  "../solver/solution.rkt")

(provide solve solve/evaluate solve+ solve-all verify synthesize symbolics)

(define-syntax-rule (solve/evaluate form)  
  (let-values ([(val asserts) 
                (with-handlers ([exn:fail? (lambda (e) (values #f '(#f)))])
                  (with-asserts form))])
    (send (current-solver) clear)
    (evaluate val (solve-asserts asserts))))

(define-syntax-rule (solve form)  
  (let ([asserts (with-handlers ([exn:fail? always-unsat])
                   (with-asserts-only form))])
    (send (current-solver) clear)
    (solve-asserts asserts)))

(define-syntax-rule (solve+ form)  
  (let ([asserts (with-handlers ([exn:fail? always-unsat])
                   (with-asserts-only form))])
    (solve-asserts asserts)))

(define (solve-asserts asserts)
  (if (andmap passes? asserts)
      (current-solution)
      (begin 
        (send/apply (current-solver) assert asserts)
        (let ([sol (send/handle-breaks (current-solver) solve)])
          (unless (sat? sol) 
            (error 'solve "no satisfying execution found"))
          (current-solution sol)
          sol))))

(define-syntax-rule (solve-all form)  
  (let-values ([(val asserts) (with-asserts form)])
    (send/apply (current-solver) assert asserts)
    (let loop ()
      (let ([sol (send/handle-breaks (current-solver) solve)])
        (cond [(sat? sol) 
               (send (current-solver) 
                     assert
                     (apply || (for/list ([binding (solution->list sol)])
                                 (! (@equal? (car binding) (cdr binding))))))
               (cons sol (loop))]
              [else (send (current-solver) clear)
                    '()])))))

(define-syntax verify
  (syntax-rules ()
    [(_ #:assume assume #:guarantee form)
     (let ([assumes (with-handlers ([exn:fail? always-false]) (with-asserts-only assume))]
           [asserts (with-handlers ([exn:fail? always-false]) (with-asserts-only form))])
       (when (null? asserts) 
         (error 'verify "no counterexample found"))
       (cond [(or (false? assumes) (false? asserts))
              (current-solution (sat (hash)))]
             [(and (andmap passes? assumes) (ormap fails? asserts))
              (void)]
             [else 
              (send/apply (current-solver) assert assumes)
              (send (current-solver) assert (apply || (map ! asserts)))
              (let ([sol (send/handle-breaks (current-solver) solve)])
                (send (current-solver) clear)
                (unless (sat? sol)
                  (error 'verify "no counterexample found"))
                (current-solution sol))])
       (current-solution))]
    [(_ form) (verify #:assume #t #:guarantee form)]))

(define-syntax synthesize 
  (syntax-rules (synthesize)
    [(_ #:forall inputs #:init init #:assume assume #:guarantee spec)
     (let*-values ([(free-vars) (symbolics inputs)]<commit_msg>verify macro bug fix:  forgot to clear solver state<commit_after>#lang racket

(require "eval.rkt" "state.rkt" "../base/assert.rkt" "../base/define.rkt" "cegis.rkt"
         "../config/log.rkt"
         (only-in "../base/reflect.rkt" symbolics)
         (only-in "../base/bool.rkt" || !)
         (only-in "../base/equality.rkt" @equal?)
         (only-in "../base/term.rkt" expression constant? typed? get-type type-deconstruct)
         "../solver/solver.rkt"  "../solver/solution.rkt")

(provide solve solve/evaluate solve+ solve-all verify synthesize symbolics)

(define-syntax-rule (solve/evaluate form)  
  (let-values ([(val asserts) 
                (with-handlers ([exn:fail? (lambda (e) (values #f '(#f)))])
                  (with-asserts form))])
    (send (current-solver) clear)
    (evaluate val (solve-asserts asserts))))

(define-syntax-rule (solve form)  
  (let ([asserts (with-handlers ([exn:fail? always-unsat])
                   (with-asserts-only form))])
    (send (current-solver) clear)
    (solve-asserts asserts)))

(define-syntax-rule (solve+ form)  
  (let ([asserts (with-handlers ([exn:fail? always-unsat])
                   (with-asserts-only form))])
    (solve-asserts asserts)))

(define (solve-asserts asserts)
  (if (andmap passes? asserts)
      (current-solution)
      (begin 
        (send/apply (current-solver) assert asserts)
        (let ([sol (send/handle-breaks (current-solver) solve)])
          (unless (sat? sol) 
            (error 'solve "no satisfying execution found"))
          (current-solution sol)
          sol))))

(define-syntax-rule (solve-all form)  
  (let-values ([(val asserts) (with-asserts form)])
    (send (current-solver) clear)
    (send/apply (current-solver) assert asserts)
    (let loop ()
      (let ([sol (send/handle-breaks (current-solver) solve)])
        (cond [(sat? sol) 
               (send (current-solver) 
                     assert
                     (apply || (for/list ([binding (solution->list sol)])
                                 (! (@equal? (car binding) (cdr binding))))))
               (cons sol (loop))]
              [else (send (current-solver) clear)
                    '()])))))

(define-syntax verify
  (syntax-rules ()
    [(_ #:assume assume #:guarantee form)
     (let ([assumes (with-handlers ([exn:fail? always-false]) (with-asserts-only assume))]
           [asserts (with-handlers ([exn:fail? always-false]) (with-asserts-only form))])
       (when (null? asserts) 
         (error 'verify "no counterexample found"))
       (cond [(or (false? assumes) (false? asserts))
              (current-solution (sat (hash)))]
             [(and (andmap passes? assumes) (ormap fails? asserts))
              (void)]
             [else 
              (send (current-solver) clear)
              (send/apply (current-solver) assert assumes)
              (send (current-solver) assert (apply || (map ! asserts)))
              (let ([sol (send/handle-breaks (current-solver) solve)])
                (send (current-solver) clear)
                (unless (sat? sol)
                  (error 'verify "no counterexample found"))
                (current-solution sol))])
       (current-solution))]
    [(_ form) (verify #:assume #t #:guarantee form)]))

(define-syntax synthesize 
  (syntax-rules (synthesize)
    [(_ #:forall inputs #:init init #:assume assume #:guarantee spec)
     (let*-values ([(free-vars) (symbolics inputs)]
{'fraction_non_alphanumeric': 0.16238179669030733, 'fraction_numerical': 0.0, 'mean_word_length': 2.2294847328244276, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4788116', 'n_tokens_mistral': 2234, 'n_tokens_neox': 2095, 'n_words': 517}