Z3-Solver（z3.z3types.Z3Exception：Z3 无效替换，需要表达式对。）

Question

我有一个相对复杂的 Z3 布尔公式，当尝试设置特定变量的值时，出现以下错误：
引发 Z3Exception(消息) z3.z3types.Z3Exception：Z3 无效替换，需要表达式对。

我尝试了以下方法：

def create_z3_formula_bdd(dimacs_file):
    variable_names = {
        1: 'inflow1', 2: "inflow1'",
        3: 'inflow2', 4: "inflow2'",
        5: '[email protected]', 6: "[email protected]'",
        7: 'level@1', 8: "level@1'",
        9: 'level@2', 10: "level@2'",
        11: 'level@3', 12: "level@3'",
        13: 'level@4', 14: "level@4'",
        15: 'level@5', 16: "level@5'",
        17: 'level@6', 18: "level@6'",
        19: 'outflow', 20: "outflow'",
        21: '_jx_b0'
    }
    with open(dimacs_file, 'r') as f:
        dimacs_lines = f.readlines()

    # Parse variables and clauses
    variables = set()
    clauses = []
    for line in dimacs_lines:
        tokens = line.split()
        if tokens[0] == 'p':
            num_vars = int(tokens[2])
        elif tokens[0] != 'c' and tokens[0] != '0':
            clause = [int(var) for var in tokens[:-1]]
            variables.update(map(abs, clause))
            clauses.append(clause)

    z3_variables = {var: Bool(variable_names[abs(var)]) for var in variables}

    # Create Z3 clauses
    z3_clauses = [Or([z3_variables[abs(literal)] if literal > 0 else Not(z3_variables[abs(literal)]) for literal in clause]) for clause in clauses]

    return And(z3_clauses)

 formula_bdd = create_z3_formula_bdd('neg_water_reservoir.cnf')
 substitution_map = {variable_names[1]: False}
 formula_with_substitution = substitute(formula_bdd, substitution_map)

Answer 1

您需要发布一个最小可重复的示例；即，您的问题的读者可以自己独立运行的示例。请参阅：https://stackoverflow.com/help/minimal-reproducible-example

话虽如此，z3 的

substitute

方法需要一对值： https://z3prover.github.io/api/html/namespacez3py.html#ae8f9a59a4fcabbb12636c128178c5235

因此，您可以首先将

substitution_map

从 Python 字典转换为对列表。希望这能让你继续前进。如果没有，请发布一个我们可以独立运行的最小代码段。