Module completion 

Model Completion.

Fills in values for unassigned variables to produce a complete model that satisfies all constraints.

Strategies

• Default values: Assign default values based on sort
• Witness completion: Use witness terms from theory solving
• Optimal completion: Minimize model size or maximize interpretability

References

• Z3’s model/model_evaluator.cpp

Structs

CompletionConfig

Configuration for model completion.

CompletionStats

Statistics for model completion.

ModelCompleter

Model completion engine.

Enums

CompletionStrategy

Strategy for completing missing values.