-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy path5value.py
111 lines (81 loc) · 3.58 KB
/
5value.py
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
103
104
105
106
from util import *
from z3 import *
import math
########
n = 5 # number of truth values in logic
fs = [] # formulas
### Variables ###
# Implication: nxn-matrix of integer variables
I = NAME(tuple( tuple( Int("%s->%s" % (i, j)) for j in range(n) ) for i in range(n) ), 'I')
# Designated set: n-vector of bools
D = NAME(tuple( Bool("?%s" % i) for i in range(n) ), 'D')
### Operations ###
# ints always correspond to object-level/non-classical truth values
# bools always correspond to meta-level/classical truth values
# these all accept either variables or values, and return variables
# int -> bool
def TRUE (p, name=None): return ind(D, p, fs=fs, name=name or "?%s" % p, Type=Bool)
def FALSE(p, name=None): return Not(TRUE(p, name=name))
# int+ -> int
def IMP(p, q, name=None): return ind(I, p, q, fs=fs, name=name or "(%s->%s)" % (p, q))
def NOT(p, name=None): return IMP(p, 0, name=name or "-%s" % p)
def OR (p, q, name=None): return IMP(IMP(p, q), q, name=name or "(%s||%s)" % (p, q))
def AND(p, q, name=None): return NOT(IMP(p, NOT(q)), name=name or "(%s&&%s)" % (p, q))
N = tuple(NOT(i) for i in range(n))
O = tuple(tuple(OR (j,i) for i in range(n)) for j in range(n)) # bug: not sure why I had to transpose these
A = tuple(tuple(AND(j,i) for i in range(n)) for j in range(n)) # bug: not sure why I had to transpose these
### Formulas ###
# in range
fs += [ And(0 <= NOT(i), NOT(i) < n) for i in range(n) ]
fs += [ And(0 <= IMP(i, j), IMP(i, j) < n) for i in range(n) for j in range(n) ]
# not true isn't true
fs += [ Implies(TRUE(i), FALSE(NOT(i))) for i in range(n) ]
# not not true is true
fs += [ Implies(TRUE(i), TRUE(NOT(NOT((i))))) for i in range(n) ]
# |== (not not p) -> p
fs += [ TRUE(IMP(NOT(NOT(i)), i)) for i in range(n) ]
# |=/= p or (not p)
fs.append(Not(And(*[ TRUE(OR(i, NOT(i))) for i in range(n) ])))
# |=/= p -> (p and p)
fs.append(Not(And(*[ TRUE(IMP(i, AND(i, i))) for i in range(n) ])))
# MP
fs += [ Implies(And(TRUE(IMP(i, j)), TRUE(i)), TRUE(j)) for i in range(n) for j in range(n) ]
# Cases
fs += [ Implies(TRUE(OR(i, j)), TRUE(k)) == And(Implies(TRUE(i), TRUE(k)), Implies(TRUE(j), TRUE(k)))
for i in range(n) for j in range(n) for k in range(n) ]
# Left Conj
fs += [ Implies(And(TRUE(i), TRUE(j)), TRUE(k)) == Implies(TRUE(AND(i, j)), TRUE(k))
for i in range(n) for j in range(n) for k in range(n) ]
# Right Conj
fs += [ TRUE(AND(i, j)) == And(TRUE(i), TRUE(j)) for i in range(n) for j in range(n) ]
### Domain Restriction ###
# specify truth designation
fs += [TRUE(i) == (i>=n-2) for i in range(n)]
# monotonicity of negation
fs += [NOT(i) >= NOT(i+1) for i in range(n-1)] + [D[-1]]
# specify negation
fs += [NOT(i) == n-1-i for i in range(n)]
# symmetry over antidiagonal
fs += [IMP(i,j) == IMP(n-1-j,n-1-i) for i in range(n) for j in range(n)]
# specify corners
# fs += [IMP(0,0) == n-1, IMP(0,-1) == n-1, IMP(-1,0) == 0, IMP(-1,-1) == n-1]
# specify edges
fs += [IMP(0,i) == n-1 for i in range(n)]
fs += [IMP(-1,i) == i for i in range(n)]
fs += [IMP(i,0) == n-1-i for i in range(n)]
fs += [IMP(i,-1) == n-1 for i in range(n)]
# monotonicity of implication
fs += [IMP(i,j) <= IMP(i,j+1) for i in range(n) for j in range(n-1)]
fs += [IMP(i,j) >= IMP(i+1,j) for i in range(n-1) for j in range(n)]
### Solve ###
pp("%s Formulas\n" % len(fs))
M = 50 # number of models to generate
V = None #N + D # set of variables of which to avoid full repeats ("None" for all)
for i, m in enumerate(get_models(fs, M, V)):
print("--- Model %s ---" % (i+1))
pp( meval(m, I) )
pp( meval(m, N) )
pp( meval(m, D) )
pp( meval(m, O) )
pp( meval(m, A) )
print()