		Search-engine friendly clone of the ACL2 documentation.

Solve-event-generation

Solve-gen-solution-from-rewritten-term

Attempt to determine a solution from a rewritten term.

Signature
(solve-gen-solution-from-rewritten-term matrix rewritten-term ?f x1...xn ctx state) → (mv erp f-body state)
Arguments: matrix — Guard (pseudo-termp matrix).; rewritten-term — Guard (pseudo-termp rewritten-term).; ?f — Guard (symbolp ?f).; x1...xn — Guard (symbol-listp x1...xn).
Returns: f-body — A pseudo-termp.

This function is called after calling a rewriter (currently, the ACL2 and Axe rewriters are supported) on the matrix of the specification. The obtained rewritten term is passed to this function, which attempts to extract a solution from it. This extraction process does not depend on the particular rewriter, and thus it is factored in this function, which is always part of the transformation (unlike the functions to call the rewriters, which are in separately includable files. The matrix of the specification is passed to this function just for the purpose of being used in error messages.

The extraction process is as explained in the user documentation. We collect the leaves of the if tree, and remove all the t ones from the list, since they do not contribute any constraints. If there are no more terms left, they were all t, and thus we return nil as the solution; anything else would be fine as well, but nil is simple. If there is exactly one term left and it has the form (equal (?f x1 ... xn) term<x1,...,xn>), we return term<x1,...,xn> as the solution.

The current strategy is somewhat restrictive; there are clearly (easy) ways to extract solutions from a wider range of forms of rewritten terms. There are plans to do that.

In the final error message, we use no evisceration so that the terms can always be seen in full. We do not expect these terms to be too large in the near future. If this changes, we may use some evisceration.

Definitions and Theorems

Function: solve-gen-solution-from-rewritten-term

(defun solve-gen-solution-from-rewritten-term
       (matrix rewritten-term ?f x1...xn ctx state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (pseudo-termp matrix)
                             (pseudo-termp rewritten-term)
                             (symbolp ?f)
                             (symbol-listp x1...xn))))
 (let ((__function__ 'solve-gen-solution-from-rewritten-term))
  (declare (ignorable __function__))
  (b* ((leaf-terms (if-tree-leaf-terms rewritten-term))
       (leaf-terms (remove-equal *t* leaf-terms))
       ((when (not leaf-terms)) (value *nil*))
       (leaf-term (car leaf-terms))
       ((when (and (not (cdr leaf-terms))
                   (nvariablep leaf-term)
                   (not (fquotep leaf-term))
                   (eq (ffn-symb leaf-term) 'equal)
                   (= (len (fargs leaf-term)) 2)
                   (equal (fargn leaf-term 1)
                          (fcons-term ?f x1...xn))))
        (value (fargn leaf-term 2))))
   (er-soft+
    ctx t nil
    "The rewriter has rewritten the term ~X10 to ~X20, ~
               which does not determine a solution for ~x3 ~
               according to the user documentation. ~
               This transformation may be extended in the future ~
               to determine solutions in more cases than now."
    nil matrix rewritten-term ?f))))