1#script (python)
2
3import sys
4from clingo import Function, Tuple_, Number, String
5
6class Observer:
7    def __init__(self):
8        self.__delayed = []
9        self.__symbols = {}
10        self.__reified = []
11        self.__terms   = {}
12        self.__elems   = {}
13
14    def __getattr__(self, name):
15        assert(not name.startswith("_"))
16        def caller(*args):
17            self.__delayed.append((name, args))
18        return caller
19
20    def __map(self, lit):
21        sign = False
22        if lit < 0:
23            sign = True
24            lit = -lit
25        ret = self.__symbols.get(lit, Function("__aux"))
26        if sign:
27            ret = Function("neg", [ret])
28        return ret
29
30    def init_program(self, incremental):
31        self.__reified.append(Function("init_program", [Number(incremental)]))
32
33    def begin_step(self):
34        self.__reified.append(Function("begin_step", []))
35
36    def _rule(self, choice, head, body):
37        head = sorted(set([ self.__map(atm) for atm in head ]))
38        body = sorted(set([ self.__map(lit) for lit in body ]))
39        self.__reified.append(Function("rule", [Number(choice), Tuple_(head), Tuple_(body)]))
40
41    def _weight_rule(self, choice, head, lower_bound, body):
42        head = sorted(set([ self.__map(atm) for atm in head ]))
43        body = sorted(set([ Tuple_([self.__map(lit), Number(weight)]) for lit, weight in body ]))
44        self.__reified.append(Function("weight_rule", [Number(choice), Tuple_(head), Number(lower_bound), Tuple_(body)]))
45
46    def _minimize(self, priority, literals):
47        literals = sorted(set([ Tuple_([self.__map(lit), Number(weight)]) for lit, weight in literals ]))
48        self.__reified.append(Function("minimize", [Number(priority), Tuple_(literals)]))
49
50    def _project(self, atoms):
51        atoms = sorted(set([ self.__map(atm) for atm in atoms ]))
52        self.__reified.append(Function("project", [Tuple_(atoms)]))
53
54    def output_atom(self, symbol, atom):
55        self.__symbols[atom] = symbol
56        self.__reified.append(Function("output_atom", [symbol]))
57
58    def _output_term(self, symbol, condition):
59        condition = sorted(set([ self.__map(lit) for lit in condition ]))
60        self.__reified.append(Function("output_term", [symbol, Tuple_(condition)]))
61
62    def _output_csp(self, symbol, value, condition):
63        condition = sorted(set([ self.__map(lit) for lit in condition ]))
64        self.__reified.append(Function("output_csp", [symbol, Number(value), Tuple_(condition)]))
65
66    def _external(self, atom, value):
67        self.__reified.append(Function("external", [self.__map(atom), String(str(value).replace('TruthValue.', ''))]))
68
69    def _assume(self, literals):
70        literals = sorted(set([ self.__map(lit) for lit in literals ]))
71        self.__reified.append(Function("assume", [Tuple_(literals)]))
72
73    def _heuristic(self, atom, type, bias, priority, condition):
74        condition = sorted(set([ self.__map(lit) for lit in condition ]))
75        self.__reified.append(Function("heuristic", [self.__map(atom), String(str(type).replace('HeuristicType.', '')), Number(bias), Tuple_(condition)]))
76
77    def _acyc_edge(self, node_u, node_v, condition):
78        condition = sorted(set([ self.__map(lit) for lit in condition ]))
79        self.__reified.append(Function("acyc_edge", [Number(node_u), Number(node_v), Tuple_(condition)]))
80
81    def theory_term_number(self, term_id, number):
82        self.__terms[term_id] = lambda: Number(number)
83
84    def theory_term_string(self, term_id, name):
85        self.__terms[term_id] = lambda: Function(name)
86
87    def theory_term_compound(self, term_id, name_id_or_type, arguments):
88        self.__terms[term_id] = lambda: Function(self.__terms[name_id_or_type]().name, [self.__terms[i]() for i in arguments])
89
90    def theory_element(self, element_id, terms, condition):
91        self.__elems[element_id] = lambda: Function("elem", [Tuple_([self.__terms[i]() for i in terms]), Tuple_(sorted(set([ self.__map(lit) for lit in condition ])))])
92
93    def _theory_atom(self, atom_id_or_zero, term_id, elements):
94        self.__symbols[atom_id_or_zero] = Function("theory", [self.__terms[term_id](), Tuple_(sorted(set([ self.__elems[e]() for e in elements ])))]);
95
96    def _theory_atom_with_guard(self, atom_id_or_zero, term_id, elements, operator_id, right_hand_side_id):
97        self.__symbols[atom_id_or_zero] = Function("theory", [self.__terms[term_id](), Tuple_(sorted(set([ self.__elems[e]() for e in elements ]))), self.__terms[operator_id](), self.__terms[right_hand_side_id]()]);
98
99    def end_step(self):
100        self.__reified.append(Function("end_step", []))
101
102    def finalize(self):
103        for name, args in self.__delayed:
104            if name.startswith("theory_atom"):
105                getattr(self, "_" + name)(*args)
106        for name, args in self.__delayed:
107            if not name.startswith("theory_atom"):
108                getattr(self, "_" + name)(*args)
109        return Context(self.__reified)
110
111class Context:
112    def __init__(self, reified):
113        self.__reified = reified[:]
114
115    def get(self):
116        return self.__reified
117
118def main(prg):
119    obs = Observer()
120    prg.register_observer(obs, True)
121    prg.ground([("base", [])])
122    prg.solve(assumptions=[(Function("b"), False)])
123    ctx = obs.finalize()
124    print ("Solving...")
125    print ("Answer: 1")
126    print (" ".join([str(x) for x in ctx.get()]))
127    sys.stdout.flush()
128
129#end.
130
131$x $= 1.
132$y $= 2.
133
1341 {a; b}.
135#minimize {1:a; 2:b}.
136#project a.
137#show x : a, b.
138#external a.
139#heuristic a : b. [1@2,sign]
140#edge (a,b) : a, b.
141
142#theory t {
143  term   { + : 1, binary, left };
144  &a/0 : term, any;
145  &b/1 : term, {=}, term, any
146}.
147a :- &a { 1+2,"test": a, b }.
148b :- &b(3) { } = 17.
149