%% Uso: 
%% - rinominare il file dandogli estensione .php, eliminando ".txt"
%% - Eseguire: php schursLemma.ott.php <n>

%% Schur's lemma in FOL (model expansion)

<?php
	$n = (int)$argv[1];
	if ($n == "" || !is_numeric($n) || ($n <= 0)) {
		echo("% Syntax: php schursLemma.ott.php <n> | mace2 -p -n <n>\n");
		exit;
	};
	echo("% Generating FO formula whose models are solutions of the Schur's Lemma problem instance with n=$n\n");
?>

%Sono date <?php echo($n); ?> biglie, ognuna delle quali etichettata con un numero tra 1 ed <?php echo($n); ?>
%(in particolare, esiste una biiezione tra le biglie e l’intervallo [1, <?php echo($n); ?>]), e
%3 urne. 
%Il problema consiste nell’inserire le biglie nelle tre urne in modo tale che
%per ogni tripla di biglie (x, y, z ) tale che x + y = z , queste non siano
%tutte nella stessa urna. 




%SP = { int/1, urna/1, in(int, urna) }

set(auto).
formula_list(usable).

% CDA: Ci sono 3 urne
all u (urna(u) <-> (u=0 | u=1 | u=2 )).

% CDA: Ci sono <?php echo($n); ?> biglie
all b (int(b) <-> 
    (<?php for($i=0; $i<$n-1; $i++) {echo("b=$i | "); } echo("b=".($n-1)); ?>)).



%% in() e' una funzione totale  BIGLIE --> URNE
all b u (in(b,u) -> (int(b) & urna(u))).  %% tipizzazione
all b exists u ( in(b,u) ).  %% relazione totale
all b u v  ((in(b,u) & in(b,v)) -> u=v).  %% relazione monovalore (funzione)


%% vincolo
all b1 b2 b3 u ( ( int(b1) & int(b2) & int(b3) & 
				   urna(u) & 
				   b1 != b2 & b1 != b3 & b2 != b3 &
				   somma(b1,b2,b3)  ) -> 
						-( in(b1,u) & in(b2,u) & in(b3,u) )
).



%% pre-int della somma tra interi in 0..<?php echo($n-1); ?>

<?php
for($x=0; $x<$n; $x++) {  // Mooolto inefficiente!
	for($y=0; $y<$n; $y++) {
		for($z=0; $z<$n; $z++) {
			
			if ($x+$y == $z) {
				echo(" somma($x,$y,$z). %LR\n");
			} else {
				echo("    -somma($x,$y,$z). %CWA\n");
			}
		}
	}
}
?>

end_of_list.