Raw constructor for honsed incremental-extremize-config-p structures.
Syntax:
(honsed-incremental-extremize-config numerator denominator direction sat-config obj progress-term final-term unsat-term sat-term error-term bad-ctrex-term interpolate-factor)
This is identical to incremental-extremize-config, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by defaggregate.
Function:
(defun honsed-incremental-extremize-config (numerator denominator direction sat-config obj progress-term final-term unsat-term sat-term error-term bad-ctrex-term interpolate-factor) (declare (xargs :guard (and))) (mbe :logic (incremental-extremize-config numerator denominator direction sat-config obj progress-term final-term unsat-term sat-term error-term bad-ctrex-term interpolate-factor) :exec (hons (hons 'numerator numerator) (hons (hons 'denominator denominator) (hons (hons 'direction direction) (hons (hons 'sat-config sat-config) (hons (hons 'obj obj) (hons (hons 'progress-term progress-term) (hons (hons 'final-term final-term) (hons (hons 'unsat-term unsat-term) (hons (hons 'sat-term sat-term) (hons (hons 'error-term error-term) (hons (hons 'bad-ctrex-term bad-ctrex-term) (hons (hons 'interpolate-factor interpolate-factor) nil))))))))))))))