Expand description
Model Builder for Theory Solvers.
Constructs satisfying assignments by coordinating theory-specific model construction and ensuring cross-theory consistency.
§Architecture
- Theory Model Builders: Each theory provides partial models
- Coordination: Ensure shared variables have consistent values
- Completion: Fill unassigned variables with default values
- Minimization: Optionally produce minimal models
§References
- Z3’s
smt/smt_model_generator.cpp
Structs§
- Model
- Model assignment.
- Model
Builder - Model builder engine.
- Model
Builder Config - Configuration for model builder.
- Model
Builder Stats - Statistics for model builder.
Enums§
- Value
- Value in a model.