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