potassco / ngo

Non Ground Optimizer for logic programs.
MIT License
4 stars 0 forks source link

Symmetry trait: Unsafe variables, removed too much #74

Closed MaxOstrowski closed 1 year ago

MaxOstrowski commented 1 year ago
 #program base.
  executionTime(J,M,T) :- duration(J,M,T).
  %comment removed
  task(T) :- executionTime(T,_,_).
  machine(M) :- executionTime(_,M,_).
  %comment removed
  %comment removed
  maxtime(T,T1) :- task(T); executionTime(T,R1,T1); 0 <= { executionTime(T,R2,T2): R2 != R1, T2 > T1 } <= 0.
  time((0..(Max-1))) :- Max = #sum { T1,T,R1: executionTime(T,R1,T1) }.
  %comment removed
  { before(T1,T2,M) } :- sequence(T1,M,ST1); sequence(T2,M,ST2); T1 < T2.
  before(T2,T1,M) :- sequence(T1,M,ST1); sequence(T2,M,ST2); T1 < T2; not before(T1,T2,M).
  seq(T,M,0) :- sequence(T,M,1).
  seq(T,M2,(S+Time)) :- sequence(T,M1,ST); sequence(T,M2,(ST+1)); executionTime(T,M1,Time); seq(T,M1,S); time((S+Time)).
  seq(T2,M,(S+Time)) :- before(T1,T2,M); executionTime(T1,M,Time); seq(T1,M,S); time((S+Time)).
  #false :- before(T1,T2,M); executionTime(T1,M,Time); seq(T1,M,S); not time((S+Time)).
  aux(T,M,S) :- seq(T,M,S).
  aux(T,M,(S-1)) :- aux(T,M,S); time((S-1)).
  bind(T,M,S) :- aux(T,M,S); not aux(T,M,(S+1)).
  %comment removed
  #show.
  #show perm(T,M,(P+1)) : bind(T,M,S); P = #count { TT: bind(TT,M,SS), SS < S }.
  %comment removed
  aux((Time+Exec)) :- bind(T,M,Time); executionTime(T,M,Exec).
  %comment removed
  aux((T-1)) :- aux(T); T > 0.
  latency(T) :- aux(T); not aux((T+1)).
  %:~ latency(T). [T@0]
  :~ aux(T). [1@0,T]

becomes

#program base.
%comment removed
%comment removed
%comment removed
time((0..(Max-1))) :- Max = #sum { T1,T,R1: duration(T,R1,T1) }.
%comment removed
{ before(T1,T2,M) } :- sequence(_,M,_); 2 <= #count { T1: sequence(T1,M,_) }.
before(T2,T1,M) :- sequence(T1,M,_); sequence(T2,M,_); T1 < T2; not before(T1,T2,M).
seq(T,M,0) :- sequence(T,M,1).
seq(T,M2,(S+Time)) :- sequence(T,M1,ST); sequence(T,M2,(ST+1)); duration(T,M1,Time); seq(T,M1,S); time((S+Time)).
seq(T2,M,(S+Time)) :- before(T1,T2,M); duration(T1,M,Time); seq(T1,M,S); time((S+Time)).
#false :- before(T1,_,M); duration(T1,M,Time); seq(T1,M,S); not time((S+Time)).
aux(T,M,S) :- seq(T,M,S).
aux(T,M,(S-1)) :- aux(T,M,S); time((S-1)). 
bind(T,M,S) :- aux(T,M,S); not aux(T,M,(S+1)).
%comment removed
#show.
#show perm(T,M,(P+1)) : bind(T,M,S); P = #count { TT: bind(TT,M,SS), SS < S }.
%comment removed 
aux((Time+Exec)) :- bind(T,M,Time); duration(T,M,Exec).
%comment removed
aux((T-1)) :- aux(T); T > 0.
%:~ latency(T). [T@0]
:~ aux(T). [1@0,T] 
%comment removed

on default settings, rule: { before(T1,T2,M) } :- sequence(_,M,_); 2 <= #count { T1: sequence(T1,M,_) }. is definitely wrong