basics

(in-package "SMT")

(include-book "xdoc/top" :dir :system)

(include-book "std/util/defval" :dir :system)

(include-book "std/strings/decimal" :dir :system)

(include-book "std/strings/case-conversion" :dir :system)

(defxdoc smt-basics
  :parents (verified)
  :short "Basic functions and types in Smtlink.")

(defval *smt-basics*
  :parents (smt-basics)
  :short "Basic ACL2 functions supported in Smtlink."
  (append '(magic-fix)
    '(rationalp realp booleanp integerp symbolp)
    '(binary-+ binary-*
      unary-/
      unary--
      equal
      <
      implies
      if
      not
      lambda)))

(defval *smt-functions*
  :parents (smt-functions)
  :short "ACL2 functions and their corresponding Z3 functions."
  `((binary-+ "_SMT_.plus" . 1) (binary-* "_SMT_.times" . 1)
    (unary-/ "_SMT_.reciprocal" . 1)
    (unary-- "_SMT_.negate" . 1)
    (equal "_SMT_.equal" . 2)
    (< "_SMT_.lt" . 2)
    (if "_SMT_.ifx" . 3)
    (not "_SMT_.notx" . 1)
    (lambda "lambda" . 2)
    (implies "_SMT_.implies" . 2)))

(defval *smt-types*
  :parents (smt-basics)
  :short "ACL2 type functions and their corresponding Z3 type declarations."
  `((realp . "_SMT_.RealSort()") (rationalp . "_SMT_.RealSort()")
    (integerp . "_SMT_.IntSort()")
    (booleanp . "_SMT_.BoolSort()")
    (symbolp . "Symbol_z3.z3Sym")))

(defval *smt-uninterpreted-types*
  :parents (smt-basics)
  :short "ACL2 type functions and their corresponding Z3 uninterpreted function
    type declarations."
  `((realp . "_SMT_.RealSort()") (rationalp . "_SMT_.RealSort()")
    (real/rationalp . "_SMT_.RealSort()")
    (integerp . "_SMT_.IntSort()")
    (booleanp . "_SMT_.BoolSort()")
    (symbolp . "Symbol_z3.z3Sym")))

(defval *smt-architecture*
  '((process-hint . add-hypo-cp) (add-hypo . expand-cp)
    (expand . type-extract-cp)
    (type-extract . uninterpreted-fn-cp)
    (uninterpreted . smt-trusted-cp)
    (uninterpreted-custom . smt-trusted-cp-custom)))

(encapsulate nil
  (local (defun falist-to-xdoc-aux
      (falist acc)
      (b* (((when (atom falist)) acc) ((cons facl2 (cons fsmt nargs)) (car falist))
          (facl2-str (if (equal facl2 'hint-please)
              (list (downcase-string (symbol-name facl2)))
              `("@(see " ,(SYMBOL-NAME SMT::FACL2) ")")))
          (entry `("<tr><td>" ,@SMT::FACL2-STR
              "</td><td>"
              ,SMT::FSMT
              "</td><td>"
              ,(SMT::NAT-TO-DEC-STRING SMT::NARGS)
              "</td></tr> ")))
        (falist-to-xdoc-aux (cdr falist)
          (revappend entry acc)))))
  (local (defun falist-to-xdoc
      nil
      (declare (xargs :mode :program))
      (string-append-lst `("<p></p>
<table>
<tr><th>ACL2 function</th><th>Z3 function</th><th>Nargs</th></tr>
" ,@(REVERSE (SMT::FALIST-TO-XDOC-AUX SMT::*SMT-FUNCTIONS* NIL))
          "</table>"))))
  (make-event `(defxdoc smt-functions
      :parents (smt-basics)
      :short "SMT functions"
      :long ,(SMT::FALIST-TO-XDOC))))

(encapsulate nil
  (local (defun alist-to-xdoc-aux
      (alist acc)
      (b* (((when (atom alist)) acc) ((cons facl2 fsmt) (car alist))
          (facl2-str (if (equal facl2 'realp)
              (list (downcase-string (symbol-name facl2)))
              `("@(see " ,(SYMBOL-NAME SMT::FACL2) ")")))
          (entry `("<tr><td>" ,@SMT::FACL2-STR
              "</td><td>"
              ,SMT::FSMT
              "</td></tr> ")))
        (alist-to-xdoc-aux (cdr alist)
          (revappend entry acc)))))
  (local (defun talist-to-xdoc
      nil
      (declare (xargs :mode :program))
      (string-append-lst `("<p></p>
<table>
<tr><th>ACL2 type functions</th><th>Z3 type declarations</th></tr>
" ,@(REVERSE (SMT::ALIST-TO-XDOC-AUX SMT::*SMT-TYPES* NIL))
          "</table>"))))
  (make-event `(defxdoc smt-types
      :parents (smt-basics)
      :short "SMT types"
      :long ,(SMT::TALIST-TO-XDOC)))
  (local (defun ualist-to-xdoc
      nil
      (declare (xargs :mode :program))
      (string-append-lst `("<p></p>
<table>
<tr><th>ACL2 type functions</th><th>Z3 uninterpreted function type declarations</th></tr>
" ,@(REVERSE (SMT::ALIST-TO-XDOC-AUX SMT::*SMT-UNINTERPRETED-TYPES* NIL))
          "</table>"))))
  (make-event `(defxdoc smt-uninterpreted-types
      :parents (smt-basics)
      :short "SMT uninterpreted function types"
      :long ,(SMT::UALIST-TO-XDOC))))