Please wait ...

Benchmark(s) have been added to cart.

Tag has been added.

• Login
• Links
• FAQs
• Contact

Navigation

• Instance
  • Show Instances
• Problem
  • Show Problems
• Show Tags
• Search
• Cart

Encoding gbie_chk.bingo

Name	gbie_chk.bingo
Class Tree	[Root]    Miscellaneous (45)    ASP Contest 09 (45)    Verification and Evaluation Encodings and Tools (38)
Submitter	Martin Gebser
Author	Martin Gebser and Roland Kaminski
Description	As Bingo is still a prototype, please make sure that it reads an instance along with a solution candidate before the encoding by calling: - Input from <instance> and <solution> files: bingo <instance> <solution> gbie_chk.bingo - Solution from standard input: bingo - <instance> gbie_chk.bingo
Created	2009-05-13 08:12
Modified	2009-05-13 08:14
Languages	Bingo (alpha)
Language Features
Compatible Instance Classes
Input Predicates
Output Predicates
Encoding Parameter
Standalone	No
Tags
Attributes
Content	#hide. #show values/4. #show sol/0. char_to_digit(0, 0). char_to_digit(1, 1). char_to_digit(2, 2). char_to_digit(3, 3). char_to_digit(4, 4). char_to_digit(5, 5). char_to_digit(6, 6). char_to_digit(7, 7). char_to_digit(8, 8). char_to_digit(9, 9). digit(X, Y, D) :- char(C, Y), char_to_digit(C, D), X = Y - 1, X >= 0. dig(X) :- digit(_, X, _). % tell the grounder that dig/1 is complete because no dependency checking or % statement ordering is done % Note: this also implies that the instance has to be given FIRST! #complete dig/1. sign(X, 1) :- char(p, X). sign(X, Y) :- char(m, X), Y = 0 - 1. num_1(X, Y, Val) :- digit(X, Y, Val), not dig(X). num_1(X, Z, NewVal) :- num_1(X, Y, Val_1), digit(Y, Z, Val_2), NewVal_1 = 10 * Val_1, NewVal = NewVal_1 + Val_2. num(X, Y, Val) :- num_1(X, Y, Val), Z = Y + 1, not dig(Z). par_expr(X, W, Val) :- char(o, Y), expr(Y, Z, Val), W = Z + 1, char(c, W), X = Y - 1, X >= 0. sing_term(X, Z, Val) :- par_expr(Y, Z, Val1), sign(Y, S), Val = Val1 * S, X = Y - 1, X >= 0. sing_term(X, Z, Val) :- num(Y, Z, Val1), sign(Y, S), Val = Val1 * S, X = Y - 1, X >= 0. expr(X, Y, Val) :- char(o, X), num(X, Y, Val). expr(0, Y, Val) :- num(0, Y, Val). expr(X, Y, Val) :- par_expr(X, Y, Val). expr(X, Y, Val) :- sing_term(X, Y, Val). expr(X, Z, Val) :- expr(X, Y, Val_1), sing_term(Y, Z, Val_2), Val = Val_1 + Val_2. cmp(X, W, Val) :- char(g, Y), num(Y, W, Val), X = Y - 1, X >= 0. cmp(X, W, Val) :- char(g, Y), Z = Y + 1, sign(Z, S), num(Z, W, Val1), Val = S * Val1, X = Y - 1, X >= 0. ssol :- expr(0, Y, Val1), cmp(Y, Z, Val2), Val1 > Val2. val1(Y, p, V) :- expr(0, Y, V), V >= 0. val1(Y, m, V) :- expr(0, Y, V1), V1 < 0, V = 0 - V1. val2(Y, p, V) :- val1(Y, _, _), cmp(Y, Z, V), V >= 0. val2(Y, m, V) :- val1(Y, _, _), cmp(Y, Z, V1), V1 < 0, V = 0 - V1. vvalues(S1, V1, S2, V2) :- val1(Y, S1, V1), val2(Y, S2, V2). :- not ssol. #complete values/4. #complete vvalues/4. :- values(S1, V1, S2, V2), not vvalues(S1, V1, S2, V2). :- vvalues(S1, V1, S2, V2), not values(S1, V1, S2, V2). :- not sol.