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