|
|
|---|
|
|
|
|---|
Try to prove a goal using GL symbolic simulation.
Usage, as a
(gl-hint my-gl-clause-processor :bindings `((a ,(g-number (list (mk-number-list 1 1 9)))) (b ,(g-boolean 0))) :hyp '(bvecp a 8) :coverage-hints ('(:expand ((bvecp a 8)))))
The above hint causes an attempt to apply the clause processor
my-gl-clause-processor to the current clause. Such a clause processor must be
created using def-gl-clause-processor. One such clause processor,
The full interface is as follows, with default values and brief descriptions of each keyword argument:
(gl-hint clause-processor-name ;; bindings of variables to symbolic object specs :bindings <required> ;; maximum recursion depth :clk 1000000 ;; hypothesis of the theorem :hyp t ;; conclusion of the theorem :concl nil ;; hints for proving coverage :cov-hints nil :cov-hints-position nil :cov-theory-add nil :do-not-expand nil ;; number of counterexamples to print :n-counterexamples 3 ;; abort if symbolic simulation yields a result with ;; indeterminate truth value. :abort-indeterminate t ;; abort as soon as a counterexample is discovered. :abort-ctrex t ;; execute the conclusion on each counterexample (turn off if non-executable) :exec-ctrex t ;; abort if a hypothesis is discovered to be unsatisfiable. :abort-vacuous t ;; enable accumulated-persistence-like rule profiling :prof-enabledp nil ;; To perform case-splitting, set this argument: :param-bindings nil ;; Ignored unless case-splitting: :param-hyp nil :run-before-cases nil :run-after-cases nil)
The keyword arguments to