|
| 1 | + |
| 2 | +max_vars(7). |
| 3 | +max_body(20). |
| 4 | + |
| 5 | +non_datalog. |
| 6 | + |
| 7 | +:- not body_var(_,1). |
| 8 | +:- not body_var(_,2). |
| 9 | + |
| 10 | + |
| 11 | +head_pred(out,3). |
| 12 | +body_pred(in,3). |
| 13 | +body_pred(my_succ,2). |
| 14 | +body_pred(add,3). |
| 15 | +body_pred(lt,2). |
| 16 | +body_pred(empty,2). |
| 17 | +body_pred(C,1):-constant(C,_). |
| 18 | + |
| 19 | +pred_task_specific(in). |
| 20 | +pred_task_specific(empty). |
| 21 | + |
| 22 | +constant(v0, value). |
| 23 | +constant(v1, value). |
| 24 | +constant(v2, value). |
| 25 | +constant(v3, value). |
| 26 | +constant(v4, value). |
| 27 | +constant(v5, value). |
| 28 | +constant(v6, value). |
| 29 | +constant(v7, value). |
| 30 | +constant(v8, value). |
| 31 | +constant(v9, value). |
| 32 | + |
| 33 | +constant(c0, position). |
| 34 | +constant(c1, position). |
| 35 | +constant(c2, position). |
| 36 | +constant(c3, position). |
| 37 | +constant(c4, position). |
| 38 | +constant(c5, position). |
| 39 | +constant(c6, position). |
| 40 | +constant(c7, position). |
| 41 | +constant(c8, position). |
| 42 | +constant(c9, position). |
| 43 | + |
| 44 | +type(empty,(ex,position)). |
| 45 | +type(out,(ex,position,value)). |
| 46 | +type(in,(ex,position,value)). |
| 47 | +type(my_succ,(position,position)). |
| 48 | +type(add,(position,position,position)). |
| 49 | +type(lt,(position,position)). |
| 50 | +type(C,(T,)):- constant(C,T). |
| 51 | + |
| 52 | +%% %% BECAUSE WE DO NOT LEARN FROM INTERPRETATIONS |
| 53 | +bad_body(in, Vars):- |
| 54 | + vars(_, Vars), |
| 55 | + Vars = (V0,_,_), |
| 56 | + V0 != 0. |
| 57 | + |
| 58 | +bad_body(empty, Vars):- |
| 59 | + vars(_, Vars), |
| 60 | + Vars = (V0,_), |
| 61 | + V0 != 0. |
| 62 | + |
| 63 | +%:- body_literal(Rule,add,_,(A,B,C)), body_literal(Rule,lt,_,(B,C)). |
| 64 | +%:- body_literal(Rule,add,_,(A,B,C)), body_literal(Rule,lt,_,(A,C)). |
| 65 | + |
| 66 | +% SOUND! add/3 must be used with a non-const argument [reducer discovers it] |
| 67 | +:- body_literal(Rule,add,_,(A,B,C)), body_literal(Rule,P,_,(A,)), body_literal(Rule,Q,_,(B,)), constant(P,position), constant(Q,position), P != Q. |
| 68 | +:- body_literal(Rule,add,_,(A,B,C)), body_literal(Rule,P,_,(A,)), body_literal(Rule,Q,_,(C,)), constant(P,position), constant(Q,position), P != Q. |
| 69 | +:- body_literal(Rule,add,_,(A,B,C)), body_literal(Rule,P,_,(B,)), body_literal(Rule,Q,_,(C,)), constant(P,position), constant(Q,position), P != Q. |
| 70 | + |
| 71 | +% SOUND! lt/3 must be used with a non-const argument [reducer discovers it] |
| 72 | +:- body_literal(Rule,lt,_,(A,B)), body_literal(Rule,P,_,(A,)), body_literal(Rule,Q,_,(B,)), constant(P,position), constant(Q,position), P != Q. |
| 73 | + |
| 74 | +% SOUND! succ/2 cannot be used with a const argument [reducer discovers it] |
| 75 | +:- body_literal(Rule,my_succ,_,(A,B)), body_literal(Rule,P,_,(A,)), constant(P,position). |
| 76 | +:- body_literal(Rule,my_succ,_,(A,B)), body_literal(Rule,P,_,(B,)), constant(P,position). |
| 77 | + |
| 78 | +%% SOUND! no point having in(A,B,C) where both B and C are not used [shrinker discovers it] |
| 79 | +%:- body_literal(R, in, 3, (A,B,C)), singleton(B), singleton(C). |
| 80 | + |
| 81 | +:- body_literal(Rule,add,_,(A,_,_)), body_literal(Rule,c0,_,(A,)). |
| 82 | +:- body_literal(Rule,add,_,(_,B,_)), body_literal(Rule,c0,_,(B,)). |
| 83 | +:- body_literal(Rule,add,_,(_,_,C)), body_literal(Rule,c0,_,(C,)). |
| 84 | + |
| 85 | +:- body_literal(Rule,add,_,(A,_,_)), body_literal(Rule,c1,_,(A,)). |
| 86 | +:- body_literal(Rule,add,_,(_,B,_)), body_literal(Rule,c1,_,(B,)). |
| 87 | +:- body_literal(Rule,add,_,(_,_,C)), body_literal(Rule,c1,_,(C,)). |
0 commit comments