z3/dpll_wrong.py at master · SalvatoreZagaria/z3 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
from z3 import *
'''
The formula has to be written as a list of lists.
Allowed operators: AND, OR, NOT, IMPLIES, BI-IMPLIES
'''

formula_list = ["AND", "x = y", ["OR", ["AND", "y = z", ["NOT", "x = z"]], "x = z"]]


def get_operator(operator):
    if operator == "NOT":
        return Not
    elif operator == "AND":
        return And
    elif operator == "OR":
        return Or
    elif operator == "IMPLIES":
        return Implies
    elif operator == "BI-IMPLIES":
        return operator
    else:
        return False


def get_inner_most(f_list, to_avoid=None):
    last_one = None
    while True:
        if to_avoid == f_list:
            return last_one
        if all(type(i) == str for i in f_list):
            return f_list
        for i in f_list:
            if type(i) == list:
                last_one = f_list
                f_list = i
                break


def get_sat_formula(sat_formula, operator_str, variables):
    if sat_formula is None:
        if operator_str == "BI-IMPLIES":
            return variables[0] == variables[1]
        elif operator_str == "NOT":
            return Not(variables[0])
        else:
            operator = get_operator(operator_str)
            if operator:
                return operator(variables)
            else:
                print("{}: operator not valid.".format(operator_str))
                return False
    else:
        if operator_str == "BI-IMPLIES":
            return variables[0] == sat_formula
        elif operator_str == "NOT":
            return Not(sat_formula)
        else:
            operator = get_operator(operator_str)
            if operator:
                variables.append(sat_formula)
                return operator(variables)
            else:
                print("{}: operator not valid.".format(operator_str))
                return False


def sat_solver(f_list):
    sat_formula = None
    inner_most = get_inner_most(f_list)
    while True:
        variables = []
        if inner_most is None:
            break
        else:
            for i in inner_most[1:]:
                if type(i) == str:
                    variables.append(Bool(i))
            sat_formula = get_sat_formula(sat_formula, inner_most[0], variables)
        inner_most = get_inner_most(f_list, to_avoid=inner_most)

    return sat_formula


if __name__ == "__main__":
    sat_formula = sat_solver(formula_list)
    s = Solver()
    s.add(sat_formula)
    s.check()
    m = s.model()
    variables_for_dtp = []
    for d in m.decls():
        if m[d]:
            variables_for_dtp.append(d)
        else:
            variables_for_dtp.append(Not(d))
    dtp = And(variables_for_dtp)
    solve(dtp)


#
# dpt = And(x == y, y == z, Not(x == z))
# solve(dpt)