		Search-engine friendly clone of the ACL2 documentation.

Solve

APT solving transformation: directly determine a solution to a specification.

Introduction

Program synthesis, i.e. deriving a program from a specification, can be viewed as a form of constraint solving: the specification expresses the constraints, and the synthesized program is a solution to the constraints. In some cases, this kind of constraint satisfaction problem can be solved directly, e.g. via inference techniques. This transformation attempts to solve a specification directly, producing a satisfying program if successful.

A specification is a predicate over target programs, so that a solution to a specification is indeed a program. The programs may be deeply or shallowly embedded in the ACL2 logic, according to the pop-refinement and shallow pop-refinement approaches, respectively. Currently, this solving transformation operates on specifications over shallowly embedded programs, i.e. second-order predicates in ACL2. Currently, this solving transformation expects these predicates to be expressed using SOFT, but the transformation may be extended, in the future, to operate on second-order predicates expressed via the built-in apply$.

A range of direct solving methods may be employed: rewriting, narrowing (i.e. computing sufficient conditions), witness finding via resolution, SMT solving, SAT solving, etc. Currently this solving transformation only supports (two forms of) rewriting, but there are plans to extend it to additional methods. Note that some of the methods listed above correspond to the sketching approach to program synthesis, which can therefore be a valuable tool in APT's arsenal.

This transformation also supports a manual solving method, in which the user provides the solution, possibly with hints to prove its correctness. While this is not an automatic method like the ones described above, it may be useful when the automatic methods fail, or when the solution happens to be simple to find and to prove. Using this transformation with the manual solving method is generally more convenient than writing out the full refinement step: in particular, this transformation automates the generation and proof of the refinement theorem (i.e. that the new specification implies the old one) from the proof that the manually provided solution satisfies the (old) specification.

Solving methods that require tools that are not part of ACL2 can be modularly and selectively used by including the files in which the callers of such tools reside. This solving transformation, as part of input validation, checks that (the file of) the specified solving method has been loaded (more precisely, it checks that the function symbol of the caller is present in the ACL2 world). The caller is called via reflection by the solving transformation.

The solve design notes, which use this notation, provide the mathematical concepts and template proofs upon which this transformation is based. These notes should be read alongside this reference documentation, which refers to them in some places.

General Form

(solve old
       :method                 ; no default
       :method-rules           ; default nil
       :solution-name          ; default :auto
       :solution-enable        ; default nil
       :solution-guard         ; default t
       :solution-guard-hints   ; default nil
       :solution-body          ; no default
       :solution-hints         ; default nil
       :new-name               ; default :auto
       :new-enable             ; default :auto
       :old-if-new-name        ; default from table
       :old-if-new-enable      ; default from table
       :verify-guards          ; default :auto
       :print                  ; default :result
       :show-only              ; default nil
  )

Inputs

old

Denotes the target function to transform.
It must be the name of a function, or a numbered name with a wildcard index that resolves to the name of a function. In the rest of this documentation page, for expository convenience, it is assumed that old is the name of the denoted function.
old must be a SOFT quantifier function (see `Classification' section in soft::defsoft) that depends on one function variable (let it be ?f), that has no parameters, and whose body has the form
(forall (x1 ... xn) matrix<(?f x1 ... xn)>)
where x1, ..., xn are 0 or more variables and matrix<(?f x1 ... xn)> is a term that contains a single call of ?f on x1, ..., xn (after translation and let expansion).
The transformation attempts to solve for ?f, i.e. to determine an n-ary function that satisfies the constraints that old puts on ?f.
In the solve design notes, old is denoted by S, ?f is denoted by f, x0, ..., xn are denoted by the single variable x (the generalization to multiple variables is straighforward in the design notes), and matrix<(?f x1 ... xn)> is denoted by R(x,f(x)).

:method — no default

Specifies the solving method to use.
It must be one of the following:
:acl2-rewriter, to use the ACL2 rewriter. This method is made available by including community book kestrel/apt/solve-method-acl2-rewriter.lisp.
:axe-rewriter, to use the Axe rewriter. This method is available by including community book kestrel/apt/solve-method-axe-rewriter.lisp.
:manual, to manually supply a solution.
Support for more methods is planned.

:method-rules — nil

Specifies the ACL2 or Axe rewrite rules to use when :method is :acl2-rewriter or :axe-rewriter.
It must be a list of symbols that are names of ACL2 theorems usable as ACL2 or Axe rewrite rules.
For the ACL2 rewriter, these rules are added to the current theory, and the rewriter operates in the so-augmented theory. For the Axe rewriter, these rules define the theory that the rewriter operates on.
This input may be present only if :method is :acl2-rewriter or :axe-rewriter.

:solution-name — default :auto

Determines the name of the solution function for ?f, and whether the function is generated or not.
It must be one of the following:
:auto, which may only be used when the name of ?f starts with a ?. In this case, the function is generated, and its name is the symbol obtained by removing the initial ? from the name of ?f.
A symbol that names an existing function. In this case, the function is not generated: the existing function is used instead. This is allowed only if :method is :manual.
Any other symbol, to use as the name of the solution function, which is generated in this case.
If this input is the name of an existing function, then the inputs :solution-enable, :solution-guard, :solution-guard-hints, and :solution-body must be all absent. If any of these inputs are present, then the :solution-name input must not be the name of an existing function.
If this input is the name of an existing function, it must be in logic mode and it must be defined. Its arity must be the same as ?f. It must return a single result. If guards must be verified (as determined by the :verify-guards input), then the function must be guard-verified.
In the rest of the documentation page, let f be the name of this function, whether it already exists or is generated.

:solution-enable — default nil

Determines whether f is enabled, when this function is generated.
It must be one of the following:
t, to enable it.
nil, to disable it.
This input must be absent if f already exists.

:solution-guard — default t

Determines the guard of f, when this function is generated.
It must be an untranslated term whose free variables are among x1, ..., xn. The term must return a single (i.e. non-mv) result.
See Section `Solution Determination' below for a discussion about this input.
This input must be absent if f already exists.

:solution-guard-hints — default nil

Determines the hints to verify the guards of f, when this function is generated.
See Section `Solution Determination' below for a discussion about this input.
This input may be present only if guards are to be verified, as determined by the :verify-guards input.
This input must be absent if f already exists.

:solution-body — no default

Specifies the body of the solution function, when :method is :manual and f is generated.
It must be an untranslated term whose free variables are among x1, ..., xn. The term must return a single (i.e. non-mv) result.
See Section `Solution Determination' below for a discussion about this input.
This input must be present if :method is :manual and f is generated; otherwise, this input must be absent.

:solution-hints — nil

Specifies the hints to prove the correctness of the solution, when :method is :manual.
This input may be present only if :method is :manual.

:new-name — default :auto

Determines the name of the generated new function.
It must be one of the following:
:auto, to generate the name automatically as described in function-name-generation.
Any other symbol, to use as the name of the function.
In the rest of this documentation page, let new be the name of this function.

:new-enable — default :auto

Determines whether new is enabled.
It must be one of the following:
t, to enable it.
nil, to disable it.
:auto, to enable it iff old is enabled.

:old-if-new-name — default from table

Determines the name of the theorem asserting that the old function is implied by the old function.
It must be one of the following:
A keyword, to use as separator between the names of old and new. A keyword :kwd specifies the theorem name oldkwdnew, in the same package as new.
Any other symbol, to use as the name of the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-old-if-new-name.
In the rest of this documentation page, let old-if-new be the name of this theorem.

:old-if-new-enable — default from table

Determines whether the old-if-new theorem is enabled.
It must be one of the following:
t, to enable the theorem.
nil, to disable the theorem.
Absent, to use the value from the APT defaults table, which is set via set-default-input-old-if-new-enable.
If this input is t, the :new-to-old-enable input must be nil. At most one of these two inputs may be t at any time.

:verify-guards — default :auto

Determines whether the guards of the generated functions are verified or not.
It must be one of the following:
t, to verify the guards.
nil, to not verify guards.
:auto, to verify the guards if and only if the guards of the target function old are verified.

:print — default :result

Specifies what is printed on the screen (see screen printing).
It must be one of the following:
nil, to print nothing (not even error output).
:error, to print only error output (if any).
:result, to print, besides any error output, also the results of solve. This is the default value of the :print input.
:info, to print, besides any error output and the results, also some additional information about the internal operations of solve.
:all, to print, besides any error output, the results, and the additional information, also ACL2's output in response to all the submitted events.
If the call of solve is redundant, an indication to that effect is printed on the screen, unless :print is nil.

:show-only — default nil

Determines whether the event expansion of solve is submitted to ACL2 or just printed on the screen:
nil, to submit it.
t, to just print it. In this case: the event expansion is printed even if :print is nil (because the user has explicitly asked to show the event expansion); the resulting events are not re-printed separately (other than their appearance in the printed event expansion) even if :print is :result or :info or :all; no ACL2 output is printed for the event expansion even if :print is :all (because the event expansion is not submitted). If the call of solve is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

Solution Determination

The transformation attempts to find a solution for ?f according to the chosen method, as explained below. A solution may or may not be found. If no solution is found, the transformation fails with an informative error message.

Rewriting

When the :method input is :acl2-rewriter or :axe-rewriter, the transformation calls the ACL2 or Axe rewriter on the term matrix<(?f x1 ... xn)>, obtaining a rewritten term result.

Consider the outer if tree structure of result, and collect all the leaves of such a tree:

If result is not a call of if, then result is the only leaf.
If result has the form (if a b c), recursively collect the leaves of b of c, and join them into a list.

For instance, if result is (if a (if b c d) e), the collected leaves are c, d, and e.

There are three cases to consider.

The first case is the one where all the collected leaves are t. In this case, the transformation is successful, and the determined solution is

(defun f (x1 ... xn)
  nil)

The fact that matrix<(?f x1 ... xn)> rewrote to t (under all the conditions in the if tree) means that any ?f satisfies the constraints. So anything can be used as the solution f. We use the function that always returns nil for simplicity. While this may seem an unlikely case, it may arise under certain conditions, e.g. for some boundary cases.

The second case is the one where one collected leaf has the form

(equal (?f x1 ... xn) term<x1,...,xn>)

where term<x1,...,xn> is a term that may depend on x1, ..., xn and that does not contain ?f, and all the other collected leaves are t. In this case, the transformation is successful, and the determined solution is

(defun f (x1 ... xn)
  term<x1,...,xn>)

The conditions under which the rewritten term is t put no constraints on the solution, which can be therefore entirely determined by the only equality leaf.

The third case is the one where the two cases above do not apply. In this case, the transformation fails. No solution has been determined.

Support for determining solutions in more cases may be added in the future.

Note that, in the second case above, there is no general guarantee that term<x1,...,xn> can be guard-verified without assumptions on x1, ..., xn. The :solution-guard input may be used to add such assumptions, and :solution-guard-hints input may be used to verify guards, but there is no general guarantee that suitable inputs always exist: the ACL2 or Axe rewriter may produce a logically valid term that cannot be guard-verified under any hypotheses on its variables. Future extensions of this transformation may address this issue, e.g. by limiting rewriting so that only guard-verifiable terms are produced.

When the transformation is successful, the ACL2 or Axe rewriting provides an ACL2 or Axe proof of correctness of the solution. This should suffice to generate an ACL2 proof of the old-if-new refinement theorem in principle, but in practice there may be technical difficulties in some cases. Difficulties seem less likely to happen when using the ACL2 rewriter, because the same rewrites should apply during the generated proof. Difficulties may be more likely when using the Axe rewriter, because its rewriting may not exactly correspond to ACL2's rewriting. Future extensions of this transformation may address this issue, e.g. by having the Axe rewriter produce an ACL2 proof that this transformation may use to prove the refinement theorem.

In any case, the transformation attempts to prove a theorem to confirm the correctness of ACL2's or Axe's rewriting in ACL2. If that theorem is successful, the transformation internally generates a theorem of the form

(implies (equal (?f x1 ... xn)
                term<x1,...,xn>)
         matrix<(?f x1 ... xn)>)

which essentially says that the matrix of old holds if we replace (?f x1 ... xn) with term<x1,...,xn>, i.e. that the inferred solution body satisfies the initial specification. It is the latter theorem that is used to prove old-if-new. Its formulation is equivalent to matrix<term<x1,...,xn>>, but the formulation used is more convenient for generating the proof of old-if-new.

Manual

When the :method input is :manual, the transformation calls no inference tool. Instead, the generated or existing function f is the (purported) solution.

If f exists, it must have the same number of arguments as ?f. It must be the case that

(implies (equal (?f x1 ... xn)
                (f x1 ... xn))
         matrix<(?f x1 ... xn)>)

This proof is attempted via the :solution-hints input.

If f is generated, it has the form

(defun f (x1 ... xn)
  term<x1,...,xn>)

where term<x1,...,xn> is the :solution-body input; it is a term whose free variables are among x1, ..., xn.

It must be the case that

(implies (equal (?f x1 ... xn)
                term<x1,...,xn>)
         matrix<(?f x1 ... xn)>)

This proof is attempted via the :solution-hints input.

The guard of f is determined by :solution-guard. If guards are to be verified, the verification of the guards of f is attempted using :solution-guard-hints.

Generated Events

The solution for ?f.
(defun f (x1 ... xn)
  (declare (xargs :guard ...)) ; from :solution-guard input
  ...) ; see section 'Solution Determination' above
This is not generated if :method is :manual and :solution-name names an existing function.
In the solve design notes, f is denoted by f_0.

new

Specification strengthened by choosing the solution, i.e. equality between ?f and f:
(soft::defun-sk2 new ()
  (forall (x1 ... xn)
          (equal (?f x1 ... xn)
                 (f x1 ... xn))))
In the solve design notes, new is denoted by S'.

old-if-new

Theorem asserting that new implies old (i.e. a refinement relation):
(defthm old-if-new
  (implies (new)
           (old))
In the solve design notes, old-if-new is denoted by SS'.

Subtopics

Solve-implementation: Implementation of solve.