anchor.diff:    ;;         Prove correctness of clause processor
     ;;
   
  -;; -----------------------------------------------------------------
  -;;       Define evaluators
  +  ;; -----------------------------------------------------------------
  +  ;;       Define evaluators
   
  -(defevaluator ev-process-hint ev-lst-process-hint
  -  ((not x) (if x y z) (hint-please hint tag)))
  +  (defevaluator ev-process-hint ev-lst-process-hint
  +    ((not x) (if x y z) (hint-please hint tag)))
   
  -(def-join-thms ev-process-hint)
  +  (def-join-thms ev-process-hint)
   
     (defthm correctness-of-process-hint
       (implies (and (pseudo-term-listp cl)
  
positive.code: (include-book "SMT-hint-interface")
  (include-book "SMT-verified-cps")
  
  (defsection Smtlink-process-user-hint
    :parents (Smtlink)
    :short "Functionalities for processing user hints given to Smtlink. User
    hints will be merged with (smt-hint)."
  
  ;; --------------------------------------------------------
  
  ;; Example:
  ;; (defthm ...
  ;;   ...
  ;;   :hints (("Goal"
  ;;            :clause-processor
  ;;            (SMT::smtlink clause
  ;;                          '(:functions ()
  ;;                            :hypotheses ()
  ;;                            :main-hint ()
  ;;                            :int-to-rat nil
  ;;                            :smt-fname ""
  ;;                            :rm-file t
  ;;                            :smt-solver-params ()
  ;;                            :smt-cnf ())))))
  
    (define true-list-fix ((lst t))
      :returns (true-listp)
      (if (true-listp lst)
          lst
        nil))
  
negative.code:       (:smt-solver-params . listp)
        (:smt-cnf . listp)))
  
    (define eval-type ((type symbolp) (content t))
      :short "Evaluate if a content is of the given type."
      :returns (type-correct? booleanp)
      (cond ((equal type 'booleanp) (booleanp content))
            ((equal type 'stringp) (stringp content))
            ((equal type 'listp) (listp content))
            (t (symbolp content))))
  
    (define check-syntax ((hint-lst true-listp) (used true-listp))
      :short "Main function for checking the syntax of a Smtlink hint list."
      :returns (syntax-good? booleanp)
      :hints (("Goal" :in-theory (enable true-list-fix)))
      (b* ((hint-lst (true-list-fix hint-lst))
           ((if (endp hint-lst)) t)
           ((cons first rest) hint-lst)
           ((cons second rest-of-second) rest)
           ((if (member-equal first used))
            (er hard? 'Smtlink=>check-syntax "Already defined ~p0.~%" first))
           (exist? (assoc-equal first *syntax-lst*))
           ((unless exist?) nil)
           (type (cdr exist?))
           (type-correct? (eval-type type second))
           ((unless type-correct?) nil))
        (check-syntax rest-of-second (cons first used))))
  
    (define smtlink-hint-syntax-p ((hint-lst t))
      :short "Syntax check for Smtlink hint."
      :returns (syntax-good? booleanp)
      (b* (;; hint-lst should be a listp
           ((unless (true-listp hint-lst)) nil)
           ;; hint-lst should not exceed a length of 16 elements
           ((unless (<= (len hint-lst) 16)) nil))
        (check-syntax hint-lst nil)))
  
    (define smtlink-hint-syntax-fix ((hint-lst smtlink-hint-syntax-p))
      :short "Fixing function for Smtlink hint syntax."
      :returns (fixed-syntax smtlink-hint-syntax-p)
      :ignore-ok t
      :irrelevant-formals-ok t
      (if (smtlink-hint-syntax-p hint-lst) hint-lst nil))
  
    (define combine-hints ((raw-user-hints smtlink-hint-syntax-p)
                           (hint smtlink-hint-p))
      :returns (combined-hint smtlink-hint-p)
      :ignore-ok t
      (b* ((user-hints (smtlink-hint-syntax-fix raw-user-hints))
           (- (cw "Warning (Smtlink=>combine-hints): Smtlink hint syntax
      violated~% ~q0Therefore user provided Smtlink hint ignored.~%" raw-user-hints))
           (hint (smtlink-hint-fix hint)))
        hint))
  
    (define process-hint ((cl pseudo-term-listp) (user-hint t))
      :returns (subgoal-lst pseudo-term-list-listp)
      :enabled t
      (b* ((cl (pseudo-term-list-fix cl))
           ((unless (smtlink-hint-syntax-p user-hint)) (list cl))
           (- (cw "user-hint: ~q0" user-hint))
           (combined-hint (combine-hints user-hint (smt-hint)))
           (cp-hint `(:clause-processor (Smt-verified-cp clause ',combined-hint)))
           (subgoal-lst (cons `(hint-please ',cp-hint 'process-hint) cl)))
  