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
|
#script (lua)
function main(prg)
local step = 0
local check = false
while true do
parts = {}
if step > 0 then
parts[#parts+1] = {"trans", {step}}
else
parts[#parts+1] = {"base", {}}
end
parts[#parts+1] = {"state", {step}}
if check then
parts[#parts+1] = {"check", {step}}
end
prg:ground(parts)
prg:release_external(gringo.Fun("vol", {step-1}))
prg:assign_external(gringo.Fun("vol", {step}), true)
local ret = prg:solve()
if ret == gringo.SolveResult.SAT then
if not check and prg:get_const("nocheck") == nil then
check = true
parts = {}
parts[#parts+1] = {"check", {step}}
prg:ground(parts)
ret = prg:solve()
if ret == gringo.SolveResult.SAT then
break
end
else
break
end
end
step = step+1
end
end
#end.
|
