/
types.go
95 lines (81 loc) · 1.98 KB
/
types.go
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
package solver
// Describes basic types and constants that are used in the solver
// Status is the status of a given problem or clause at a given moment.
type Status byte
const (
// Indet means the problem is not proven sat or unsat yet.
Indet = Status(iota)
// Sat means the problem or clause is satisfied.
Sat
// Unsat means the problem or clause is unsatisfied.
Unsat
// Unit is a constant meaning the clause contains only one unassigned literal.
Unit
// Many is a constant meaning the clause contains at least 2 unassigned literals.
Many
)
func (s Status) String() string {
switch s {
case Indet:
return "INDETERMINATE"
case Sat:
return "SAT"
case Unsat:
return "UNSAT"
case Unit:
return "UNIT"
case Many:
return "MANY"
default:
panic("invalid status")
}
}
// Var start at 0 ; thus the CNF variable 1 is encoded as the Var 0.
type Var int32
// Lit start at 0 and are positive ; the sign is the last bit.
// Thus the CNF literal -3 is encoded as 2 * (3-1) + 1 = 5.
type Lit int32
// IntToLit converts a CNF literal to a Lit.
func IntToLit(i int32) Lit {
if i < 0 {
return Lit(2*(-i-1) + 1)
}
return Lit(2 * (i - 1))
}
// IntToVar converts a CNF variable to a Var.
func IntToVar(i int32) Var {
return Var(i - 1)
}
// Lit returns the positive Lit associated to v.
func (v Var) Lit() Lit {
return Lit(v * 2)
}
// SignedLit returns the Lit associated to v, negated if 'signed', positive else.
func (v Var) SignedLit(signed bool) Lit {
if signed {
return Lit(v*2) + 1
}
return Lit(v * 2)
}
// Var returns the variable of l.
func (l Lit) Var() Var {
return Var(l / 2)
}
// Int returns the equivalent CNF literal.
func (l Lit) Int() int32 {
sign := l&1 == 1
res := int32((l / 2) + 1)
if sign {
return -res
}
return res
}
// IsPositive is true iff l is > 0
func (l Lit) IsPositive() bool {
return l%2 == 0
}
// Negation returns -l, i.e the positive version of l if it is negative,
// or the negative version otherwise.
func (l Lit) Negation() Lit {
return l ^ 1
}