forked from microsoft/mcBV
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Rules.fs
224 lines (198 loc) · 8.61 KB
/
Rules.fs
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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
module Rules
open GlobalOptions
open Util
open BooleanValuation
open Clause
open Trail
open State
open RLEBVTheory
open BoundsTheory
open InitializationRules
open PropagationRules
open DecisionRules
open ConflictRules
open Explain
let CheckTDB (s:State) =
let mutable res = true
for i in 0 .. (!s.theoryDB).count - 1 do
let tRel = (!s.theoryDB).getThRelationByIndex i
let tHolds = tHolds tRel s.bvVal s.numeralDB
let tbndsHolds = tbndsHolds tRel s.bounds s.numeralDB
let valueB = (!s.bVal).getValueB tRel.getBoolVar
let valueT = (!s.bVal).getValueT tRel.getBoolVar
match (tHolds, tbndsHolds, valueB, valueT) with
| (Undefined, Undefined, _, Undefined)
| (False, False, False, False)
| (False, Undefined, False, False)
| (True, True, True, True)
| (True, Undefined, True, True) ->
// That's alright, ignore.
()
| (True, _, False, _)
| (True, _, _, False)
| (False, _, True, _)
| (False, _, _, True)
| (_, _, True, False)
| (_, _, False, True) ->
let mutable is_propagated = false
for c in (!s.trail).getTrailPtr .. (!s.trail).getCount - 1 do
match (!s.trail).trail.[c] with
| BoolDecision l
| Imp (_,l) ->
if abs l = tRel.getBoolVar then
is_propagated <- true
| MAssgnmnt (bv,_,_) -> if (List.exists (fun x -> x = bv) tRel.variableArguments) then
is_propagated <- true
| BAssgnmnt (bv,_,_) -> ()
if not is_propagated then
printfn "Invariant violation; disagreement: %s -> (RLE:%s,Bnds:%s) x (B:%s,T:%s)"
(tRel.ToString(s.numeralDB))
(tHolds.ToString())
(tbndsHolds.ToString())
(valueB.ToString())
(valueT.ToString())
res <- false
| (True, _, Undefined, _)
| (False, _, Undefined, _) ->
let mutable is_propagated = false
for c in (!s.trail).getTrailPtr .. (!s.trail).getCount - 1 do
match (!s.trail).trail.[c] with
| BoolDecision l
| Imp (_,l) ->
if abs l = tRel.getBoolVar then
is_propagated <- true
| MAssgnmnt (bv,_,_) -> if (List.exists (fun x -> x = bv) tRel.variableArguments) then
is_propagated <- true
| BAssgnmnt (bv,_,_) -> ()
if not is_propagated then
// tRel holds, but that fact has not been propagated into the according
// Boolean variable that represents tRel (tRel.getBoolVar)
printfn "Not propagated to valueB %s" (tRel.ToString())
res <- false
| (True, _, _, Undefined)
| (False, _, _, Undefined) ->
() // OK
| (Undefined, True, _, _)
| (Undefined, False, _, _) ->
() // OK, bounds can be stronger
| (Undefined, _, _, False)
| (Undefined, _, _, True) ->
printfn "Theory value assigned, but %s does not evaluate" (tRel.ToString())
res <- false
| _ ->
printfn "Theory DB check not implemented for tHolds=%s tbndsHolds=%s valueB=%s valueT=%s" (tHolds.ToString()) (tbndsHolds.ToString()) (valueB.ToString()) (valueT.ToString())
NOT_YET_IMPLEMENTED("th-rel check")
if not res then
printfn "Trail at the failure: "
let mutable lvl = 0
printfn "L%d====================================" lvl
for i in 0 .. (!s.trail).getCount - 1 do
let e = (!s.trail).trail.[i]
match e with
| BoolDecision v ->
lvl <- lvl + 1
printfn "L%d====================================" lvl
printf "BoolDecision %d :" v
| Imp (c,l) ->
printf "(%s) -> %d : " (clauseToString !c) l
| _ -> ()
printfn "%s" (s.trailElemToString e)
res
let paranoia (s:State) =
let mutable res = true
if not s.IsConflicted then
res <- res && ((!s.clauseDB).Check s.bVal)
res <- res && (CheckTDB s)
res
let PropagateWithLimitedBounds (s:State) (trail:Trail) =
let mutable cnt = 0
let limit = (!s.variableDB).highestVarInUse / 2
while not s.IsConflicted && trail.hasPropagationsPending do
Propagate s trail.nextPropagation
cnt <- cnt + 1
if cnt > limit then
s.boundsEnabled <- false
s.boundsEnabled <- true
let checkSat (s:State) (sandbox:State) =
let mutable trail = !s.trail
// Initial propagation and watchlist construction
pushUnits s
// printfn "Stats: "
// printfn "Vars : %d" (!s.varDB).highestVarInUse
// printfn "BoolVars: %d" ((Array.sumBy (fun x -> if x = 0 then 1 else 0) (!s.varDB).sorts) - 1)
// printfn "BvVars : %d" (Array.sumBy (fun x -> if x > 0 then 1 else 0) (!s.varDB).sorts)
// printfn "Clauses : %d" (!s.clauseDB).count
// printfn "Units : %d" (Array.sumBy (fun x ->
// match x with
// |Imp (cls,_) -> if getSize !cls = 1 then 1 else 0
// | _ -> 0 ) (!s.trail).trail)
dbg <| (lazy sprintf "%s" ((!s.clauseDB).ToString()))
if DBG then
printfn "Occurrence & watchlists: "
let wm = (!s.watchManager)
for v in 1 .. (!s.variableDB).highestVarInUse do
if ((!s.variableDB).isBoolean v) then
(wm.printBoolWatch s.clauseDB v)
else
(wm.printThWatch s.numeralDB s.theoryDB v)
if s.IsConflicted then
dbg <| (lazy sprintf "Conflict in initial clause database; trivially unsat.")
dbg <| (lazy sprintf "Conflict clause: %s" (clauseToString !(s.GetConflictClause)))
s.MarkUNSAT
verbose <| (lazy sprintf "L 00 ===========================================================================")
while not s.IsSolved do
if s.IsConflicted then
if (!s.trail).getNumDecisions = 0 then
s.MarkUNSAT
elif GENERALIZE then
let pre_cnflct = !s.GetConflictClause
xTExplanationGeneralization s sandbox
if s.IsConflicted then
let aft_cnflct = !s.GetConflictClause
if pre_cnflct <> aft_cnflct then
s.ShowFancyConflict(pre_cnflct, "[pre-generalization]")
s.ShowFancyConflict(aft_cnflct, "[generalized]")
else
s.ShowFancyConflict(pre_cnflct, "[no generalization]")
resolveConflict s
//else
//Otherwise Backjump-Decide resolved a conflict.
else
s.ShowFancyConflict(!s.GetConflictClause, "")
resolveConflict s
else
// Propagation
PropagateWithLimitedBounds s trail
if DBG then assert(paranoia s)
if s.IsSearch then
if s.IsComplete then
// Everything is assigned, so we're done.
if not DBG then
s.MarkSAT
else
if (paranoia s) then s.MarkSAT
else
// Decision time <- no propagagtions but search is incomplete,
// i.e., at least one variable is still unassigned.
let nd = trail.getNumDecisions + 1
verbose <| (lazy sprintf "L %02d ===========================================================================" nd)
decide s
verbose <| (lazy sprintf "== Done ========================================================================")
if VRB then
if s.IsSatisfiable then
printfn "SATISFIABLE"
printfn "------------------"
printfn "FINAL TRAIL:"
(!s.trail).forcePrint("", s.bvVal, s.bounds)
printfn "------------------"
printfn "Model:"
for v in 1 .. (!s.variableDB).highestVarInUse do
if (!s.variableDB).sorts.[v] = 0 then
printfn "%d -> %s" v (((!s.bVal).getValueB v).ToString())
else
printfn "%d -> %s" v (((!s.bvVal).getValue v).ToString())
else if s.IsUnsatisfiable then
(!s.trail).print("", s.bvVal, s.bounds)
else
verbose <| (lazy "UNKNOWN")
s