acl2s-parameter

(in-package "ACL2S")

(include-book "acl2s/utilities" :dir :system)

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

(defun keywordify
  (sym)
  (declare (xargs :guard (symbolp sym)))
  (fix-intern-in-pkg-of-sym (symbol-name sym)
    :a))

(def-const *acl2s-parameters*
  '(:testing-enabled :num-trials :verbosity-level :num-counterexamples :num-print-counterexamples :num-witnesses :num-print-witnesses :search-strategy :sampling-method :backtrack-limit :cgen-timeout :cgen-local-timeout :cgen-single-test-timeout :print-cgen-summary :backtrack-bad-generalizations :use-fixers :recursively-fix :defdata-aliasing-enabled))

(table acl2s-defaults-table)

(defrec acl2s-param-info%
  (value guard setter)
  nil)

(defmacro add-acl2s-parameter
  (name default
    &key
    (setter 'nil)
    (guard 't)
    short
    long)
  "Add a new user-defined parameter.
   Put it in the acl2s-defaults-table as a key,
   using the value of :default. 
:guard is a term that checks for legal values of the
   parameter (It uses symbol 'value for variable capture).
getter and setter specify macro names that will be used by
the actual getter/setter mechanism to delegate its function.
Note that setter should be a macro that expands to a state changing
embedded event form, this this is called from inside an make-event.
You have to see the code in acl2s-defaults to understand whats going
on with getter and setter, the situation is assymmetric and I am
being lazy about documentation.
short and long are keyword arguments to defxdoc. 
"
  (b* (((unless (symbolp name)) (er hard
         'add-acl2s-parameter
         "Name must be a symbol, but is ~x0."
         name)))
    `(progn (table acl2s-defaults-table
        ',(ACL2S::KEYWORDIFY ACL2S::NAME)
        ',(MAKE ACL2S::ACL2S-PARAM-INFO% :GUARD ACL2S::GUARD :VALUE ACL2S::DEFAULT
       :SETTER ACL2S::SETTER)
        :put)
      ,@(AND ACL2S::SHORT
       `((ACL2S::DEFXDOC ,ACL2S::NAME :PARENTS (CGEN ACL2S-DEFAULTS) :SHORT
          ,ACL2S::SHORT :LONG ,ACL2S::LONG))))))

(defxdoc acl2s-defaults
  :parents (acl2-sedan cgen)
  :short "Getting and setting defaults for various parameters in Cgen (ACL2 Sedan)"
  :long "
<h3>Examples</h3>
@({
  (acl2s-defaults :set num-trials 1000)
  (acl2s-defaults :get cgen-local-timeout)
  (acl2s-defaults :get testing-enabled)
  (acl2s-defaults :set num-counterexamples 3)
})

<p>
The following parameters are available for control via @('acl2s-defaults').
These are stored in the constant @('*acl2s-parameters*') and are package-agnostic.

@({
                  num-trials
                  verbosity-level
                  num-counterexamples
                  num-witnesses
                  sampling-method
                  backtrack-limit
                  search-strategy
                  testing-enabled
                  cgen-timeout
                  cgen-local-timeout
                  cgen-single-test-timeout
                  print-cgen-summary
                  use-fixers
                  num-print-counterexamples
                  num-print-witnesses

})
</p>
")

(def-const *testing-enabled-values*
  '(t nil :naive :on-failure))

(add-acl2s-parameter testing-enabled
  :naive :short "Testing enable/disable flag"
  :long " <p>Testing can be enabled or disabled using this parameter.
  The default value is <tt>:naive</tt> (unless you are in the usual
  ACL2 Sedan session modes, where default is @('t')).  Setting this
  parameter to @('nil') amounts to disabling the testing
  mechanism. Setting this parameter to <tt>:on-failure</tt> is similar to
  setting it to @('t'), except for some undocumented behavior related
  to redefined versions of @('defthm'). Setting this parameter to
  <tt>:naive</tt> leads to top-level testing without any theorem
  prover support.</p> <code> Usage:
   (acl2s-defaults :set testing-enabled :naive)
   (acl2s-defaults :get testing-enabled)
   :doc testing-enabled
  </code>
   "
  :guard (member-eq value
    *testing-enabled-values*)
  :setter set-acl2s-random-testing-enabled)

(add-acl2s-parameter num-trials
  1000
  :short "Max number of tries to find counterexamples"
  :long " Maximum number of tries (attempts) to construct 
  counterexamples and witnesses.
  By default this parameter is set to 4000. Can be set to
  any natural number <tt>n</tt>. If set to 0, it is similar
  to setting testing-enabled parameter to @('nil').

  <code>
   Usage:
   (acl2s-defaults :set num-trials 4000)
   (acl2s-defaults :get num-trials)
   :doc num-trials
   </code>"
  :guard (and (natp value) (< value 1000000000)))

(add-acl2s-parameter verbosity-level
  1
  :short "Control verbosity of Cgen"
  :long "
 <p>Control amount of output printed by Cgen.</p>

<dl>
<dt>Levels</dt>
<dd>   0 - All Cgen output is turned off      </dd> 
<dd>   1 - Normal output (default)            </dd> 
<dd>   2 - Verbose output                     </dd> 
<dd>   3 - More verbose with Cgen statistics  </dd>  
<dd>   4 - For Debug by normal users          </dd>  
<dd>   5 and above - System level debug by developers </dd>
</dl>

  <code>
    Usage:
    (acl2s-defaults :set verbosity-level 1)
    (acl2s-defaults :get verbosity-level)
    :doc verbosity-level
  </code>"
  :guard (natp value))

(add-acl2s-parameter num-counterexamples
  3
  :short "Number of Counterexamples to be searched"
  :long "
  Set the number of counterexamples desired to be searched.
  By default this parameter is set to 3. Can be set to
  any natural number n. Setting this number to 0 implies
  the user is not interested in searching for counterexamples.
  <code>
  Usage:
  (acl2s-defaults :set num-counterexamples 3)
  (acl2s-defaults :get num-counterexamples)
  :doc num-counterexamples
  </code>"
  :guard (natp value))

(add-acl2s-parameter num-print-counterexamples
  3
  :short "Number of Counterexamples to be printed"
  :long "
  Set the number of counterexamples desired to be printed.
  By default this parameter is set to 3. Can be set to
  any natural number n. Setting this number to 0 implies
  the user is not interested in seeing counterexamples, and
  thus none will be printed in the testing output.
  
  <code>
  Usage:
  (acl2s-defaults :set num-print-counterexamples 3)
  (acl2s-defaults :get num-print-counterexamples)
  :doc num-counterexamples
  </code>"
  :guard (natp value))

(add-acl2s-parameter num-witnesses
  3
  :short "Number of Witnesses to be shown"
  :long "
  Set the number of witnesses desired to be shown
  By default this parameter is set to 3. Can be set to
  any natural number. Setting this number to 0 implies
  the user is not interested in seeing witnesses, and
  thus none will be printed in the testing output.
  
  <code>
  Usage:
  (acl2s-defaults :set num-witnesses 3)
  (acl2s-defaults :get num-witnesses)
  :doc num-witnesses
  </code>"
  :guard (natp value))

(add-acl2s-parameter num-print-witnesses
  3
  :short "Number of Witnesses to be printed"
  :long "
  Set the number of witnesses desired to be printed.
  By default this parameter is set to 3. Can be set to
  any natural number. Setting this number to 0 implies
  the user is not interested in seeing witnesses, and
  thus none will be printed in the testing output.
  
  <code>
  Usage:
  (acl2s-defaults :set num-print-witnesses 3)
  (acl2s-defaults :get num-print-witnesses)
  :doc num-print-witnesses
  </code>"
  :guard (natp value))

(def-const *search-strategy-values*
  '(:simple :incremental :hybrid))

(add-acl2s-parameter search-strategy
  :simple :short "Specify the search strategy to be used."
  :long "
  Specify which of the following strategies to
  use for instantiating free variables of the conjecture
  under test: @(':simple') or  @(':incremental').
  @(':incremental') uses a dpll-like algorithm to search
  for counterexamples (and is currently much slower).
  By default this parameter is set to @(':simple').
   <code>
    Usage:
    (acl2s-defaults :set search-strategy :simple)
    (acl2s-defaults :get search-strategy)
    :doc search-strategy
   </code>
   "
  :guard (member-eq value
    *search-strategy-values*))

(def-const *sampling-method-values*
  '(:random :uniform-random :be :mixed))

(add-acl2s-parameter sampling-method
  :random :short "Specify sampling method to be used to instantiate variables "
  :long "
  Specify which of the following methods to
  use for instantiating free variables of the conjecture
  under test: @(':be') or @(':random') or @(':uniform-random') or @(':mixed')
  By default this parameter is set to the symbol @(':random')
   <code>
    Usage:
    (acl2s-defaults :set sampling-method :random)
    (acl2s-defaults :get sampling-method)
    :doc sampling-method
   </code>
   "
  :guard (member-eq value
    *sampling-method-values*))

(add-acl2s-parameter backtrack-limit
  3
  :short "Maximum number of backtracks allowed (per variable)"
  :long "
   Maximum number of backtracks allowed by a variable.
   The default backtrack limit is set to 3. Setting this 
   parameter to 0 disables the backtracking.
   <code>
    Usage:
    (acl2s-defaults :set backtrack-limit 3)
    (acl2s-defaults :get backtrack-limit)
    :doc backtrack-limit
   </code>
   "
  :guard (natp value))

(add-acl2s-parameter cgen-timeout
  60
  :short "test?/prover timeout (in seconds)"
  :long "Maximum allowed time (in seconds) to be spent
  in the ACL2 prover on behalf of Cgen/test? macro.
  This value is used as the first argument of the
  with-timeout macro around the call to 
  prove/cgen.

  The default timeout limit is set to 60 sec.
  Guard : Timeout should be a non-negative rational.
   <code>
    Usage:
    (acl2s-defaults :set cgen-timeout 60)
    (acl2s-defaults :get cgen-timeout)
    :doc cgen-timeout
   </code>
   "
  :guard (and (rationalp value) (<= 0 value)))

(add-acl2s-parameter cgen-local-timeout
  10
  :short "Cgen/Testing timeout (in seconds)"
  :long "Maximum allowed time (in seconds) for Cgen to
  search for counterexamples to a particular form/subgoal.
  The default timeout limit is set to 10 sec.
  Setting this parameter to 0 amounts to disabling
  the timeout mechanism, i.e. its a no-op.
  Guard : Timeout should be a non-negative rational.
   <code>
    Usage:
    (acl2s-defaults :set cgen-local-timeout 10)
    (acl2s-defaults :get cgen-local-timeout)
    :doc cgen-local-timeout
   </code>
   "
  :guard (and (rationalp value) (<= 0 value)))

(add-acl2s-parameter cgen-single-test-timeout
  1/100
  :short "Cgen/Testing timeout for single, individual tests (in seconds)"
  :long "Maximum allowed time (in seconds) for Cgen to check a single test. 
  The default timeout limit is set to 1/100 sec. This is useful if
  you have functions that are very slow on some inputs. A simple
  example is the naive definition of the fibonnaci function.
  Setting this parameter to 0 amounts to disabling the timeout. 
  Guard : Timeout should be a non-negative rational.
   <code>
    Usage:
    (acl2s-defaults :set cgen-single-test-timeout 10)
    (acl2s-defaults :get cgen-single-test-timeout)
    :doc cgen-single-test-timeout
   </code>
   "
  :guard (and (rationalp value) (<= 0 value)))

(add-acl2s-parameter print-cgen-summary
  t
  :short "Print summary for Cgen"
  :long " <p>Print summary of cgen/testing done in course of test? form (and
  other forms). The default is set to @('T'). Setting this parameter to
  @('NIL'), means that no summary is printed.</p>

   <code>
    Usage:
    (acl2s-defaults :set print-cgen-summary t)
    (acl2s-defaults :get print-cgen-summary)
    :doc print-cgen-summary
   </code>
   "
  :guard (booleanp value))

(add-acl2s-parameter backtrack-bad-generalizations
  t
  :short "Specify whether to check for and then backtrack from bad generalizations."
  :long "
  By default this parameter is set to <tt>t</tt>.
   <code>
    Usage:
    (acl2s-defaults :set backtrack-bad-generalizations t)
    (acl2s-defaults :get backtrack-bad-generalizations)
    :doc backtrack-bad-generalizations
   </code>
   "
  :guard (booleanp value))

(add-acl2s-parameter use-fixers
  nil
  :short "Specify whether fixers are to be used."
  :long "
  By default this parameter is set to <tt>nil</tt>.
   <code>
    Usage:
    (acl2s-defaults :set use-fixers t)
    (acl2s-defaults :get use-fixers)
    :doc use-fixers
   </code>
   "
  :guard (booleanp value))

(add-acl2s-parameter recursively-fix
  t
  :short "Specify whether unsatisfied but fixable constraints are to be recursively fixed."
  :long "Specify whether unsatisfied but fixable constraints are to be
  recursively fixed. The resulting solution substitutions are stacked in the
  reverse order. 
  By default this parameter is set to <tt>t</tt>.
   "
  :guard (booleanp value))

(add-acl2s-parameter defdata-aliasing-enabled
  t
  :short "Enable Defdata aliasing"
  :long " <p>Defdata will try and determine if proposed data definitions are
  equivalent to existing data definitions and if so, Defdata will
  create alias types. The advantage is that any existing theorems can
  be used to reason about the new type. Defdata will generate macros
  for the recognizers and enumerators, which means that during proofs,
  you will see the recognizer for the base type. If you turn this off,
  then you can still use defdata-alias to explicitly tell ACL2s to
  alias types.</p>
 <code> Usage:
   (acl2s-defaults :get defdata-aliasing-enabled)
   (acl2s-defaults :set defdata-aliasing-enabled t)
   :doc defdata-aliasing-enabled
  </code>
   "
  :guard (booleanp value))

(defun mem-tree
  (x tree)
  (declare (xargs :guard (symbolp x)))
  (if (atom tree)
    (eq x tree)
    (or (mem-tree x (car tree))
      (mem-tree x (cdr tree)))))

(defun get-acl2s-random-testing-hints-flag-fn
  (state)
  (declare (xargs :mode :program :stobjs (state)))
  (and (mem-tree 'test-checkpoint
      (override-hints (w state)))
    t))

(defmacro get-acl2s-random-testing-hints-enabled
  nil
  `(get-acl2s-random-testing-hints-flag-fn state))

(defun set-acl2s-random-testing-flag-fn
  (flg mode state)
  (declare (xargs :mode :program :stobjs (state)))
  (let ((flg (if (eq flg :naive)
         nil
         flg)))
    (if (get-acl2s-random-testing-hints-enabled)
      (if flg
        '(value-triple :redundant)
        (if (eq mode :program)
          '(progn (logic)
            (disable-acl2s-random-testing)
            (program))
          '(disable-acl2s-random-testing)))
      (if flg
        (if (eq mode :program)
          '(progn (logic)
            (enable-acl2s-random-testing)
            (program))
          '(enable-acl2s-random-testing))
        '(value-triple :redundant)))))

(defmacro set-acl2s-random-testing-enabled
  (v forms)
  (declare (xargs :guard (member-eq v *testing-enabled-values*)))
  `(make-event (let ((mode (cdr (assoc-eq :defun-mode (table-alist 'acl2-defaults-table
               (w state))))))
      (let ((forms ',ACL2S::FORMS))
        (value `(progn ,(ACL2S::SET-ACL2S-RANDOM-TESTING-FLAG-FN ,ACL2S::V ACL2S::MODE ACL2S::STATE)
            ,@ACL2S::FORMS))))))

(defun get-acl2s-defaults
  (param wrld)
  (declare (xargs :verify-guards nil
      :guard (and (symbolp param)
        (plist-worldp wrld))))
  (b* ((kparam (keywordify param)) (param-rec-pair (assoc-eq kparam
          (table-alist 'acl2s-defaults-table
            wrld)))
      ((unless (consp param-rec-pair)) (er hard
          'acl2s-defaults
          "~|Parameter ~x0 not found in acl2s defaults!~%"
          param))
      (r (cdr param-rec-pair))
      (val (access acl2s-param-info% r :value)))
    val))

(defmacro acl2s-defaults
  (&rest rst)
  (b* (((unless (consp (cdr rst))) (er hard
         'acl2s-defaults
         "~|At least 2 arguments, but given ~x0~%"
         rst)) (param (second rst))
      (op (car rst))
      ((unless (or (eq :get op)
           (and (eq :set op) (consp (cddr rst))))) (er hard
          'acl2s-defaults
          "~|Invalid arguments supplied, given ~x0~%"
          rst)))
    (if (eq :get op)
      `(get-acl2s-defaults ',ACL2S::PARAM
        (w state))
      `(with-output :off summary
        :summary-off :all (make-event (b* ((param-rec-pair (assoc-eq ',(ACL2S::KEYWORDIFY ACL2S::PARAM)
                 (table-alist 'acl2s-defaults-table
                   (w state)))) ((unless (consp param-rec-pair)) (er hard
                  'acl2s-defaults
                  "~|Parameter ~x0 not found in acl2s-defaults!~%"
                  ',ACL2S::PARAM))
              (r (cdr param-rec-pair))
              (guard (access acl2s-param-info% r :guard))
              (setter (access acl2s-param-info% r :setter))
              (v (third ',ACL2S::RST)))
            `(make-event (if (not ,(SUBST ACL2S::V 'ACL2S::VALUE ACL2S::GUARD))
                (er soft
                  'acl2s-defaults-table
                  "Guard ~x0 for ~x1 in table failed for VALUE ~x2"
                  ',ACL2S::GUARD
                  ',',ACL2S::PARAM
                  ',ACL2S::V)
                (if ',ACL2S::SETTER
                  (let ((table-update-form `(table acl2s-defaults-table
                         ',',',(ACL2S::KEYWORDIFY ACL2S::PARAM)
                         ',(CHANGE ACL2S::ACL2S-PARAM-INFO% ',ACL2S::R :VALUE ',ACL2S::V))))
                    (value `(,',ACL2S::SETTER ,',ACL2S::V (,ACL2S::TABLE-UPDATE-FORM))))
                  (value `(progn (table acl2s-defaults-table
                        ',',',(ACL2S::KEYWORDIFY ACL2S::PARAM)
                        ',(CHANGE ACL2S::ACL2S-PARAM-INFO% ',ACL2S::R :VALUE ',ACL2S::V))
                      (value-triple ',',ACL2S::V))))))))))))

(defun assoc-eq/pkg-agnostic
  (s al)
  "If symbol name of s equals a key, return that entry in al"
  (declare (xargs :guard (and (symbolp s) (symbol-alistp al))))
  (if (endp al)
    'nil
    (if (equal (symbol-name (caar al))
        (symbol-name s))
      (car al)
      (assoc-eq/pkg-agnostic s (cdr al)))))

(defun acl2s-defaults-value-alist.
  (defaults override-alist ans.)
  (declare (xargs :verify-guards nil
      :guard (and (symbol-alistp defaults)
        (symbol-alistp override-alist)
        (symbol-alistp ans.))))
  (if (endp defaults)
    ans.
    (b* (((cons param rec-val) (car defaults)) (val (access acl2s-param-info% rec-val :value))
        (override (assoc-eq/pkg-agnostic param
            override-alist))
        (val (if override
            (cdr override)
            val)))
      (acl2s-defaults-value-alist. (cdr defaults)
        override-alist
        (cons (cons param val) ans.)))))

(defmacro acl2s-defaults-alist
  (&optional override-alist)
  "return alist mapping acl2s-parameters to their default values
overridden by entries in override-alist"
  `(acl2s-defaults-value-alist. (table-alist 'acl2s-defaults-table
      (w state))
    ,ACL2S::OVERRIDE-ALIST
    'nil))

(defun acl2s-parameter-p
  (key)
  (declare (xargs :guard t))
  (and (symbolp key)
    (member-eq (keywordify key)
      *acl2s-parameters*)))