1#script (lua) 2 3function table.shallow_copy(t) 4 local t2 = {} 5 for k,v in pairs(t) do 6 t2[k] = v 7 end 8 return t2 9end 10 11function table.append(t, val) 12 t[#t + 1] = val 13end 14 15function table.get(t, key, def) 16 local val = t[key] 17 if val ~= nil then 18 return val 19 else 20 return def 21 end 22end 23 24function table.sort_unique(t) 25 local set = {} 26 for k, v in ipairs(t) do 27 set[tostring(v)] = v 28 end 29 local ret = {} 30 for k, v in pairs(set) do 31 table.append(ret, v) 32 end 33 table.sort(ret) 34 return ret 35end 36 37function table.map(t, f) 38 for k, v in ipairs(t) do 39 t[k] = f(v) 40 end 41 return t 42end 43 44function string.startswith(str, pre) 45 return string.sub(str, 1, string.len(pre)) == pre 46end 47 48function bool_to_num(var) 49 return var and 1 or 0 50end 51 52Function = clingo.Function 53Tuple = clingo.Tuple 54 55local Context = { } 56function Context:__index(key) 57 return Context[key] 58end 59 60function Context.new(reified) 61 local self = setmetatable({}, Context) 62 self.__reified = table.shallow_copy(reified) 63 return self 64end 65 66function Context:get() 67 return self.__reified 68end 69 70local Observer = { } 71 72function Observer.new() 73 local self = setmetatable({}, Observer) 74 self.__delayed = {} 75 self.__symbols = {} 76 self.__reified = {} 77 self.__terms = {} 78 self.__elems = {} 79 return self 80end 81 82function Observer:__index(name) 83 f = Observer[name] 84 if f == nil then 85 assert(not string.startswith(name, "_")) 86 return function (...) 87 table.append(self.__delayed, {name, {...}}) 88 end 89 else 90 return f 91 end 92end 93 94function Observer:__map(lit) 95 local sign = false 96 if lit < 0 then 97 sign = true 98 lit = -lit 99 end 100 local ret = table.get(self.__symbols, lit, Function("__aux")) 101 if sign then 102 ret = Function("neg", {ret}) 103 end 104 return ret 105end 106 107function Observer:__map_lits(t) 108 for k, v in ipairs(t) do 109 t[k] = self:__map(v) 110 end 111 return t 112end 113 114function Observer:__map_wlits(t) 115 for k, v in ipairs(t) do 116 t[k] = Tuple({self:__map(v[1]), v[2]}) 117 end 118 return t 119end 120 121function Observer:init_program(incremental) 122 table.append(self.__reified, Function("init_program", {bool_to_num(incremental)})) 123end 124 125function Observer:begin_step() 126 table.append(self.__reified, Function("begin_step", {})) 127end 128 129function Observer:_rule(choice, head, body) 130 head = table.sort_unique(self:__map_lits(head)) 131 body = table.sort_unique(self:__map_lits(body)) 132 table.append(self.__reified, Function("rule", {bool_to_num(choice), Tuple(head), Tuple(body)})) 133end 134 135function Observer:_weight_rule(choice, head, lower_bound, body) 136 head = table.sort_unique(self:__map_lits(head)) 137 body = table.sort_unique(self:__map_wlits(body)) 138 table.append(self.__reified, Function("weight_rule", {bool_to_num(choice), Tuple(head), lower_bound, Tuple(body)})) 139end 140 141function Observer:_minimize(priority, literals) 142 literals = table.sort_unique(self:__map_wlits(literals)) 143 table.append(self.__reified, Function("minimize", {priority, Tuple(literals)})) 144end 145 146function Observer:_project(atoms) 147 atoms = table.sort_unique(self:__map_lits(atoms)) 148 table.append(self.__reified, Function("project", {Tuple(atoms)})) 149end 150 151function Observer:output_atom(symbol, atom) 152 self.__symbols[atom] = symbol 153 table.append(self.__reified, Function("output_atom", {symbol})) 154end 155 156function Observer:_output_term(symbol, condition) 157 condition = table.sort_unique(self:__map_lits(condition)) 158 table.append(self.__reified, Function("output_term", {symbol, Tuple(condition)})) 159end 160 161function Observer:_output_csp(symbol, value, condition) 162 condition = table.sort_unique(self:__map_lits(condition)) 163 table.append(self.__reified, Function("output_csp", {symbol, value, Tuple(condition)})) 164end 165 166function Observer:_external(atom, value) 167 table.append(self.__reified, Function("external", {self:__map(atom), tostring(value)})) 168end 169 170function Observer:_assume(literals) 171 literals = table.sort_unique(self:__map_lits(literals)) 172 table.append(self.__reified, Function("assume", {Tuple(literals)})) 173end 174 175function Observer:_heuristic(atom, type, bias, priority, condition) 176 condition = table.sort_unique(self:__map_lits(condition)) 177 table.append(self.__reified, Function("heuristic", {self:__map(atom), tostring(type), bias, Tuple(condition)})) 178end 179 180function Observer:_acyc_edge(node_u, node_v, condition) 181 condition = table.sort_unique(self:__map_lits(condition)) 182 table.append(self.__reified, Function("acyc_edge", {node_u, node_v, Tuple(condition)})) 183end 184 185function Observer:theory_term_number(term_id, number) 186 self.__terms[term_id] = function() return number end 187end 188 189function Observer:theory_term_string(term_id, name) 190 self.__terms[term_id] = function() return Function(name) end 191end 192 193function Observer:theory_term_compound(term_id, name_id_or_type, arguments) 194 self.__terms[term_id] = function () 195 return Function(self.__terms[name_id_or_type]().name, table.map(arguments, function (i) 196 return self.__terms[i]() 197 end)) 198 end 199end 200 201function Observer:theory_element(element_id, terms, condition) 202 self.__elems[element_id] = function () 203 condition = table.sort_unique(self:__map_lits(condition)) 204 return Function("elem", {Tuple(table.map(terms, function (i) 205 return self.__terms[i]() 206 end)), Tuple(condition)}) 207 end 208end 209 210function Observer:_theory_atom(atom_id_or_zero, term_id, elements) 211 elements = table.sort_unique(table.map(elements, function (e) 212 return self.__elems[e]() 213 end)) 214 self.__symbols[atom_id_or_zero] = Function("theory", {self.__terms[term_id](), Tuple(elements)}); 215end 216 217function Observer:_theory_atom_with_guard(atom_id_or_zero, term_id, elements, operator_id, right_hand_side_id) 218 elements = table.sort_unique(table.map(elements, function (e) 219 return self.__elems[e]() 220 end)) 221 self.__symbols[atom_id_or_zero] = Function("theory", {self.__terms[term_id](), Tuple(elements), self.__terms[operator_id](), self.__terms[right_hand_side_id]()}); 222end 223 224function Observer:end_step() 225 table.append(self.__reified, Function("end_step", {})) 226end 227 228function Observer:finalize() 229 if unpack == nil then 230 unpack = table.unpack 231 end 232 for _, v in ipairs(self.__delayed) do 233 local name, args 234 name, args = v[1], v[2] 235 if string.startswith(name, "theory_atom") then 236 self["_" .. name](unpack(args)) 237 end 238 end 239 for _, v in ipairs(self.__delayed) do 240 local name, args 241 name, args = v[1], v[2] 242 if not string.startswith(name, "theory_atom") then 243 self["_" .. name](unpack(args)) 244 end 245 end 246 return Context.new(self.__reified) 247end 248 249function main(prg) 250 obs = Observer.new() 251 prg:register_observer(obs, true) 252 prg:ground({{"base", {}}}) 253 prg:solve{assumptions={{Function("b"), false}}} 254 ctx = obs:finalize() 255 prg:add("q", {}, "q(@get()).") 256 prg:ground({{"q", {}}}, ctx) 257 prg:solve() 258 print "Solving..." 259 print "Answer: 1" 260 print (table.concat(table.map(ctx:get(), tostring), " ")) 261 io.flush() 262end 263 264#end. 265 266$x $= 1. 267$y $= 2. 268 2691 {a; b}. 270#minimize {1:a; 2:b}. 271#project a. 272#show x : a, b. 273#external a. 274#heuristic a : b. [1@2,sign] 275#edge (a,b) : a, b. 276 277#theory t { 278 term { + : 1, binary, left }; 279 &a/0 : term, any; 280 &b/1 : term, {=}, term, any 281}. 282a :- &a { 1+2,"test": a, b }. 283b :- &b(3) { } = 17. 284