itest-ithm

(defun itest?-fn1
  (form hints
    override-defaults
    state)
  (declare (xargs :mode :program :stobjs (state)))
  (b* ((ctx 'itest?) (debug-enable (f-get-global 'debugger-enable state))
      (state (f-put-global 'debugger-enable :never state))
      (cgen-state (make-cgen-state-fn form
          (cons :user-defined ctx)
          override-defaults
          (w state)))
      (vl (cget verbosity-level))
      (pts? (cget print-cgen-summary))
      (timeout (cget cgen-timeout))
      (hints (append 'nil
          (add-string-val-pair-to-string-val-alist "Goal"
            :do-not (list 'quote '(generalize fertilize))
            (add-string-val-pair-to-string-val-alist "Goal"
              :do-not-induct t
              hints))))
      ((mv res cgen-state state) (with-time-limit timeout
          (prove/cgen form
            hints
            cgen-state
            state)))
      ((er &) (cond ((not (cgen-state-p cgen-state)) (value nil))
          ((and (<= (access gcs% (cget gcs) :cts) 0)
             (not pts?)) (value nil))
          (t (print-testing-summary cgen-state
              ctx
              state))))
      ((mv cgen-err cts-found? state) (cond ((eq res :falsifiable) (prog2$ (cw? (normal-output-flag vl)
                "~%Itest? found a counterexample.~%")
              (mv nil t state)))
          ((eq res t) (prog2$ (cw? (and pts? (normal-output-flag vl))
                "~|Itest? failed (probably due to a hard error).~%")
              (mv t nil state)))
          ((eq res nil) (prog2$ (cw? (and pts? (normal-output-flag vl))
                "~%Itest? proved the conjecture under consideration~s0. ~
Therefore, no counterexamples exist. ~%"
                (if hints
                  ""
                  " (without induction)"))
              (mv nil nil state)))
          (t (prog2$ (cw? (and pts? (normal-output-flag vl))
                "~%Itest? succeeded. No counterexamples were found.~%")
              (mv nil nil state)))))
      ((er counterexamples) (if cgen-err
          (mv t nil state)
          (extract-cgen cgen-state state)))
      (state (f-put-global 'debugger-enable
          debug-enable
          state)))
    (mv cgen-err
      (list cts-found?
        (cons res counterexamples))
      state)))

(defun itest?-fn
  (form hints
    override-defaults
    state)
  (declare (xargs :mode :program :stobjs (state)))
  (revert-world (itest?-fn1 form
      hints
      override-defaults
      state)))

(defun itest?-fn-simple
  (form state)
  (declare (xargs :mode :program :stobjs (state)))
  (itest?-fn form nil nil state))