I'm trying to run the following Blockworld Planning Program in python:
#include <incmode>.
#program base.
% Define
location(table).
location(X) :- block(X).
holds(F,0) :- init(F).
#program step(t).
% Generate
{ move(X,Y,t) : block(X), location(Y), X != Y } = 1.
% Test
:- move(X,Y,t), holds(on(A,X),t-1).
:- move(X,Y,t), holds(on(B,Y),t-1), B != X, Y != table.
% Define
moved(X,t) :- move(X,Y,t).
holds(on(X,Y),t) :- move(X,Y,t).
holds(on(X,Z),t) :- holds(on(X,Z),t-1), not moved(X,t).
#program check(t).
% Test
:- query(t), goal(F), not holds(F,t).
% Display
#show move/3.
#program base.
% Sussman Anomaly
%
block(b0).
block(b1).
block(b2).
%
% initial state:
%
% 2
% 0 1
% -------
%
init(on(b1,table)).
init(on(b2,b0)).
init(on(b0,table)).
%
% goal state:
%
% 2
% 1
% 0
% -------
%
goal(on(b1,b0)).
goal(on(b2,b1)).
goal(on(b0,table)).
I do this by making use of the following simple function
def print_answer_sets(program):
control = clingo.Control()
control.add("base", [], program)
control.ground([("base", [])])
control.configuration.solve.models = 0
for model in control.solve(yield_=True):
sorted_model = [str(atom) for atom in model.symbols(shown=True)]
sorted_model.sort()
print("Answer set: {{{}}}".format(", ".join(sorted_model)))
To which I pass a long triple-quote string of the program above. I.e.
print_answer_sets("""
#include <incmode>.
#program base.
% Define
location(table).
location(X) :- bl
...etc.
""")
This has generally worked with other clingo programs.
However, I can't seem to produce an answer set, and I get an error
no atoms over signature occur in program:
move/3
Note that running this same program directly with clingo in the terminal or on their web interface works fine.
I believe this is because this string makes use of multiple "#program" statements and an "#include" statement, which I might not be parsing correctly (or at all) in print_answer_sets. Is there a way to properly handle program parts in python? I've tried looking at the docs and the user manual but its a bit dense.
Thanks!
I got help from my professor who managed to find a solution. I added some comments for myself and others and am posting below:
import clingo
asp_code_base = """
#include <incmode>.
% Define
location(table).
location(X) :- block(X).
holds(F,0) :- init(F).
block(b0).
block(b1).
block(b2).
init(on(b1,table)).
init(on(b2,b0)).
init(on(b0,table)).
goal(on(b1,b0)).
goal(on(b2,b1)).
goal(on(b0,table)).
#show move/3.
"""
asp_code_step = """
% Generate
{ move(X,Y,t) : block(X), location(Y), X != Y } = 1.
% Test
:- move(X,Y,t), holds(on(A,X),t-1).
:- move(X,Y,t), holds(on(B,Y),t-1), B != X, Y != table.
% Define
moved(X,t) :- move(X,Y,t).
holds(on(X,Y),t) :- move(X,Y,t).
holds(on(X,Z),t) :- holds(on(X,Z),t-1), not moved(X,t).
"""
asp_code_check = """
#external query(t).
% Test
:- query(t), goal(F), not holds(F,t).
"""
def on_model(model):
print("Found solution:", model)
# this is an arbitrary upper limit set to ensure process terminates
max_step = 5
control = clingo.Control()
control.configuration.solve.models = 1 # find one answer only
# add each #program
control.add("base", [], asp_code_base)
control.add("step", ["t"], asp_code_step)
control.add("check", ["t"], asp_code_check)
# for grounding, we make use of a parts array
parts = []
parts.append(("base", []))
control.ground(parts)
ret, step = None, 1
# try solving until max number of steps or until solved
while step <= max_step and (step == 1 or not ret.satisfiable):
parts = []
# handle #external call
control.release_external(clingo.Function("query", [clingo.Number(step - 1)]))
parts.append(("step", [clingo.Number(step)]))
parts.append(("check", [clingo.Number(step)]))
control.cleanup() # cleanup previous grounding call, so we can ground again
control.ground(parts)
# finish handling #external call
control.assign_external(clingo.Function("query", [clingo.Number(step)]), True)
print(f"Solving step: t={step}")
ret = control.solve(on_model=on_model)
print(f"Returned: {ret}")
step += 1
This outputs, as expected (omitting warning)
Solving step: t=1
Returned: UNSAT
Solving step: t=2
Returned: UNSAT
Solving step: t=3
Found solution: move(b2,table,1) move(b1,b0,2) move(b2,b1,3)
Returned: SAT