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