From c90d5b1d72ac30f384c887fee7d5bdbdb16e00f4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Patrick=20L=C3=BChne?= <patrick-github@luehne.de>
Date: Mon, 23 May 2016 16:45:55 +0200
Subject: [PATCH] Added mutex groups and variable uniqueness back to the meta
 encoding.

---
 encodings/meta-sequential-incremental.lp | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/encodings/meta-sequential-incremental.lp b/encodings/meta-sequential-incremental.lp
index 2345c16..be12e91 100644
--- a/encodings/meta-sequential-incremental.lp
+++ b/encodings/meta-sequential-incremental.lp
@@ -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