Request a model

Enable model production before set-logic, then request the model after a successful check-sat:

(set-option :produce-models true)
(set-logic QF_LRA)
(declare-const x Real)
(assert (= x (/ 1 3)))
(check-sat)
(get-model)
(exit)

./build/primo --quiet --check-model docs/examples/model.smt2

Expected output for this fixed-value example:

sat
(model
  (define-fun x () Real (/ 1 3))
)

The interpretation assigns x the exact value one third. In a less constrained problem, different satisfying assignments are equally valid; do not require a particular arbitrary value or function-table order in an application.

--check-model asks Primo to evaluate the original assertions against its own constructed model. In the default rebuild engine it requires model production to be enabled separately. The opt-in assumptions engine constructs a model internally when checking is requested, but get-model still requires :produce-models true. This is not independent validation by another solver. The separate Dolmen workflow is used when qualifying experiment results.

When a model is available

The capability map identifies routes with model support. get-model requires all of the following:

• :produce-models true was set in start mode;

• the most recent query returned sat and constructed a model;

• the context has not changed since that query.

Adding an assertion or declaration, changing the scope, or resetting the session invalidates the previous query result. Run check-sat again before requesting another model. A model is not available after unsat or unknown. Quantified formulas do not support model requests.

For example, docs/examples/stale-model.smt2 obtains SAT, pushes a scope and then calls get-model without a fresh query. It produces:

sat
(error "get-model requires a current SAT model")

This is a command-state error; it does not mean the assertions became inconsistent. See Repeated queries and scopes for scoped use.

Representation and source

Printed models contain typed SMT-LIB definitions. Values for uninterpreted sorts and function entries are solver-chosen interpretations, not additional constraints on future solves. The maintained model must assign one result to each function and evaluated argument tuple.

The session interpreter enforces model availability. The implementation’s ownership, reconstruction and evaluation contracts remain in Finalized model interpretations, with the owning model in src/core/model.hpp. That implementation chapter will be separated from its development history in the next rewrite batches.