patrick
/
plasp
Archived
1
0
Fork 0
Code Issues 12 Releases 8 Activity

Added mutex groups and variable uniqueness back to the meta encoding.

This commit is contained in:
Patrick Lühne 2016-05-23 16:45:55 +02:00
parent 4c6c739060
commit c90d5b1d72
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
encodings/meta-sequential-incremental.lp
View File

@ -20,6 +20,13 @@ modified(Var, t) :- caused(Var, Val, t).
holds(Var, Val, t) :- caused(Var, Val, t).
holds(Var, Val, t) :- holds(Var, Val, t - 1), not modified(Var, t).
% Check that variables without <none of those> values are unique
:- variable(V), Var = variable(V), not contains(Var, noneValue), not 1 {holds(Var, Val, t) : contains(Var, Val)} 1.
:- contains(Var, noneValue), not {holds(Var, Val, t) : contains(Var, Val)} 1.
% Check mutexes
:- mutexGroup(M), not {holds(Var, Val, t) : contains(M, Var, Val)} 1.
#program check(t).
% Verify that goal is met