如何提取Z3Py两模型中赋值不同的自由变量列表（排除全称量词变量）

To solve your problem of comparing two Z3 models and identifying differing free variables (while ignoring bound variables from ForAll quantifiers) plus unexpected variables in the models, here's a practical, step-by-step solution:

Key Insights #

• Free vs. Bound Variables: Variables used only in ForAll are bound, so they won't appear in the set of free variables extracted from your formulas. We use Z3's built-in free_vars() method to isolate exactly the variables we care about.
• Model Comparison Goals: We need to check two critical things:
  1. Free variables that have different values (or are missing in one model)
  2. Variables present in either model that aren't free variables (these are unexpected and worth debugging)

Complete Solution Code #

import z3

def compare_z3_models(old_model, new_model, input_formulas):
    # Collect all free variables from the input formulas
    free_variables = set()
    for formula in input_formulas:
        free_variables.update(formula.free_vars())
    
    # Helper function to safely get a variable's value from a model
    def get_variable_value(model, var):
        return model[var] if var in model else None
    
    # Identify free variables with differing assignments
    differing_free_vars = []
    for var in free_variables:
        old_val = get_variable_value(old_model, var)
        new_val = get_variable_value(new_model, var)
        if old_val != new_val:
            differing_free_vars.append({
                "name": var.name(),
                "old_value": old_val,
                "new_value": new_val
            })
    
    # Identify unexpected variables (present in model but not free variables)
    old_model_decls = set(old_model.decls())
    new_model_decls = set(new_model.decls())
    
    unexpected_vars = {
        "in_old_model": [var.name() for var in old_model_decls - free_variables],
        "in_new_model": [var.name() for var in new_model_decls - free_variables]
    }
    
    return {
        "differing_free_variables": differing_free_vars,
        "unexpected_variables": unexpected_vars
    }

# Example Usage
if __name__ == "__main__":
    # Define variables and formulas
    x = z3.Int('x')
    y = z3.Int('y')
    z = z3.Int('z')  # Bound variable (only used in ForAll)
    
    formulas = [
        x > 3,
        z3.ForAll(z, z < y)
    ]
    
    # Get first model
    solver = z3.Solver()
    solver.add(formulas)
    solver.check()
    old_model = solver.model()
    
    # Get second model with an additional constraint
    solver.add(y == 7)
    solver.check()
    new_model = solver.model()
    
    # Run comparison
    comparison_result = compare_z3_models(old_model, new_model, formulas)
    
    # Print results
    print("=== Differing Free Variables ===")
    for var in comparison_result["differing_free_variables"]:
        print(f"- {var['name']}: Old={var['old_value']}, New={var['new_value']}")
    
    print("\n=== Unexpected Variables ===")
    if comparison_result["unexpected_variables"]["in_old_model"]:
        print(f"Old model has unexpected variables: {', '.join(comparison_result['unexpected_variables']['in_old_model'])}")
    else:
        print("Old model has no unexpected variables.")
    
    if comparison_result["unexpected_variables"]["in_new_model"]:
        print(f"New model has unexpected variables: {', '.join(comparison_result['unexpected_variables']['in_new_model'])}")
    else:
        print("New model has no unexpected variables.")

How It Works #

1. Collect Free Variables: We iterate through all your input formulas and gather every free variable using formula.free_vars(). This automatically excludes variables that are only bound in ForAll quantifiers.
2. Compare Free Variables: For each free variable, we check its value in both models. If values differ (or one model doesn't assign it), we flag it as differing.
3. Detect Unexpected Variables: We compare the variables present in each model against the free variables. Any variable in the model that isn't a free variable is marked as unexpected—this helps catch mistakes like accidentally including bound variables or unused variables in your solver setup.

Notes #

• Unassigned Variables: If a free variable isn't assigned in one model (Z3 might skip variables that don't affect satisfiability), this counts as a difference since the models don't agree on its value.
• Flexibility: The code returns variable names for readability, but you can easily modify it to return the actual Z3 variable objects if needed.

内容的提问来源于stack exchange，提问作者Johan