Raw constructor for incremental-extremize-config-p structures.
Syntax:
(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 the lowest-level constructor for incremental-extremize-config-p structures. It simply conses together a structure with the specified fields.
Note: It's generally better to use macros like make-incremental-extremize-config or change-incremental-extremize-config instead. These macros lead to more readable and robust code, because you don't have to remember the order of the fields.
The incremental-extremize-config-p structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see honsed-incremental-extremize-config instead.
This is an ordinary constructor function introduced by defaggregate.
Function:
(defun 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))) (cons (cons 'numerator numerator) (cons (cons 'denominator denominator) (cons (cons 'direction direction) (cons (cons 'sat-config sat-config) (cons (cons 'obj obj) (cons (cons 'progress-term progress-term) (cons (cons 'final-term final-term) (cons (cons 'unsat-term unsat-term) (cons (cons 'sat-term sat-term) (cons (cons 'error-term error-term) (cons (cons 'bad-ctrex-term bad-ctrex-term) (cons (cons 'interpolate-factor interpolate-factor) nil)))))))))))))