#!/usr/bin/php
<?php 

error_reporting(E_ALL|E_STRICT); 
ini_set('display_errors', true);

require_once('TarskiTheorems.php');

 $TarskiReserved = array("ext","ip","e5","alpha", "beta", "gamma");
  $Numbers = array("$0$", "$1$", "$2$", "$3$", "$4$","$5$");

foreach($TarskiTheorems as $t)
  { if($t->SkolemSymbols != "")
	    { foreach($t->SkolemSymbols as $ell)
		    { $TarskiReserved[] = $ell;
			  $Numbers[] = "$" . count($Numbers) . "$";
			}
		}
  }
foreach($TarskiDefinitions as $t)
	{ $TarskiReserved[] = $t->definiens;
	  $Numbers[] = "$" . count($Numbers) . "$";
	}
function get_vars($t, $ss)
// $t is a string,  $ss is the skolem symbols
// return a string that is a comma-separated list of the members of $vars that occur in $t 
// in the right order for the arguments of the elements of $ss.
{ $flag = 0;
  $ans = ""; 
  $allvars1 = array("xa", "xb", "xp", "xq", "xc", "xd", "xa1", "xb1","xc1","xd1", 
                   "xe","xf", "xm",  "xr",  
                   "xcs", "xt", "xA", "xB", "xC", "xD"
                  );
  if($ss[0] == "crossbar" || $ss[0] == "triangle")
     $allvars = array("xa","xb","xc","xa1","xb1","xp");
  else if($ss[0] == "constructAngle")
    $allvars = array("xa","xb","xc", "xd", "xe","xp");
  else if($ss[0] == "ins")
     $allvars = array("xc", "xd", "xa", "xb");  
  else if ($ss[0] == "c63")
	 $allvars = array("xa", "xp", "xb");
  else if ($ss[0] == "insert")
     $allvars = array("xb", "xc", "xa", "xr");
  else if ($ss[0] == "op")
     $allvars = array("xq","xb","xp","xc","xa");
  else if ($ss[0] == "erectsameside")
     $allvars = array("xb","xc","xa","xq");
  else if ( $ss[0] == "c12112" || 
			$ss[0] == "b12121" ||
			$ss[0] == "c12111" || 
			$ss[0] == "b12121" ||
			$ss[0] == "c1211"  || 
			$ss[0] == "b1211" 
		  )
		{ $allvars = array("xt","xq","xr","xcs","xp1","xp2","xa");
		}
  else
     $allvars = $allvars1;
  foreach($allvars as $x)
	{  if(strpos($t,$x) === false)
		  { if($ss[0] == "erect" && $x == "xc")
			  $allvars[] = $x;
			else
			  continue;
	  	  }
	  if($flag == 0)
			{ $flag = 1;
			  $ans = $x;
			}
	  else
		    { $ans =   $ans . "," . $x;
			}
	}
  return $ans;
} 

function negate_literal($clause, $ss = "")
// $ss is either ""  or an array of Skolem symbols
{   global $Numbers, $TarskiReserved;
   if($clause[0] == '-')
		$temp = substr($clause,1);
   else if (strstr($clause, "!="))
        $temp = str_replace("!=","=",$clause);
   else if (strstr($clause, "="))
        $temp = str_replace("=", "!=", $clause);
   else
        $temp = "-" . $clause;
   $constants = array("a", "b", "c", "d", "e", "f", "m", "p", "r", "q", "cs", "t", "A", "B", "C", "D", "cu", "cv");
   $vars =      array("xa", "xb", "xc", "xd", "xe","xf", "xm","xp", "xr", "xq", "xcs", "xt", "xA", "xB", "xC", "xD","u", "v");
   $temp = str_replace("ext", "#85#", $temp);
 //  Maybe there are Skolem symbols
   if(is_array($ss) && count($ss) == 1)
     { $temp = str_replace("x","$ss[0]" . "()", $temp);
	 }
   else if(is_array($ss))
     { if($ss[0] == "f113a")
	      $skolemvars = array("xa1", "xc1", "xd1", "xf1");
	   else if ($ss[0] == "c12111" || $ss[0] == "c12112" || $ss[0] == "c1211")
	      $skolemvars = array("xc", "xb");
	   else
	     $skolemvars = array("x","y","z");
	   for($i = 0; $i < count($ss); $i++)
	      { $temp = str_replace($skolemvars[$i],$ss[$i] . "()", $temp);
		  }
	 }
   $q = str_replace("samesideline", "#1#", $temp);
   $q = str_replace("sameside", "#2#", $q);
   $q = str_replace("opposite", "#3#", $q);
   $q = str_replace(array("cu", "cv","cw"),array("#4#", "#5#","#6#"), $q);
   $q = str_replace(array("congruent", "parallel", "insert","erectAux21a","erectAux","perpAt", "constructAngle","ext"),
                    array("#7#", "#8#", "#9#","#10#", "#11#", "#12","#13#","#14#"),$q);
   $q = str_replace($TarskiReserved, $Numbers, $q);
   $r = str_replace($constants, $vars, $q);
   $ans = str_replace($Numbers, $TarskiReserved, $r);
   $ans = str_replace("#85#","ext", $ans);
   $ans = str_replace (array("#1#","#2#","#3#","#4#","#5#","#6#","#7#","#8#","#9#","#10#","#11#","#12","#13#","#14#"),
                       array("samesideline", "sameside", "opposite", "u", "v", "w",
                             "congruent", "parallel", "insert","erectAux21a","erectAux", "perpAt", "constructAngle", "ext"), 
                       $ans);

   return $ans;  // leaving the arguments of the Skolem term empty 
}
/*_________________________________________________________*/
function equality_axiom($p)
// in Satz 4.6 a particular equality axiom is in list(sos) and is needed.
//  So we have to ignore it when Skolemizing.
{ $q = explode('|', $p);
   if(! is_array($q) || count($q) != 3 )
      return false;
   $one = trim($q[0]);
   $r = explode("!=", $one);
   if(!is_array($r) || count($r) != 2)
      return false;
   if(trim($r[0]) != "x" || trim($r[1]) != "y")
      return false;
   $two = trim($q[1]);
   $three = trim($q[2]);
   if($two[0] != '-' || strlen($two) != 1+strlen($three))
      return false;
   for($i=0;$i<count($three);$i++)
      { if($three[i] != ($two[i-1] == 'x' ? 'y' : $two[i-1]))
	         return false;
	  }
   return true;
}
  
 
/*_________________________________________________________*/


function negate_theorem($p,$ss)
// p is the negative form of a theorem, as an array of clauses
// ss is an array of Skolem symbols or an empty string
{   $flag = 0;
	$ans = "";
	if(!is_array($p))
	    { echo "error in negate_theorem\n";
		  echo "$p\n";
		  die();
		}
    foreach($p as $clause)
	{  if(equality_axiom($clause))
		   continue;  // ignore.  This happens only in Satz 4.6
	   if($flag == 0)
	  	{ $ans = $ans . negate_literal($clause, $ss);
		  $flag = 1;
	  	}
   	   else 
	  	 { $ans = $ans . " | ";
		   $ans = $ans . negate_literal($clause, $ss);
	  	 }
	}
	if($ss != "")
	 	{ // put in arguments of Skolem functions
		 $parameters = get_vars($ans, $ss);
		 $ans = str_replace("()","(" . $parameters . ")", $ans);
		}
    return $ans;
}
/*__________________________________________________________*/
function strip_disjunction($clauselist)
// clauselist should be an array of clauses, 
// containing just one disjunction.
// Return an array of elements, each of which is an 
// array of clauses, obtained from clauselist by substituting
// one disjunct for the disjunction in clauselist.

{   $t = array();
	if(!is_array($clauselist))
	    { echo "error in strip_disjunction\n";
		  die();
		}
	foreach($clauselist as $clause)
		{ if(strchr($clause,"|"))
			{ $disjuncts = explode("|", $clause);
			  $n = count($disjuncts);
			  break;
			}
		}
	for($i=0;$i< $n;$i++)
		{ $t[] = array();
		} 
	foreach($clauselist as $clause)	
	   {  if(strchr($clause,"|"))
			{ for($i=0;$i< $n; $i++)
				{ $t[$i][] =  trim($disjuncts[$i]);
				}
			}
		  else
		    { for($i=0;$i< $n; $i++)
				{ $t[$i][] =  $clause;
				}
		    }
	    }

	return $t;
}
/*__________________________________________________________*/
function symbols_in($x)
// return a pair of arrays, one containing the atoms in $x and 
// the second containing the function symbols in $x.
// $x can be an array of strings or a string.
{ $atoms = array();
  $functions = array();
  $allowed = array("T", "E", "ext", "ip", "insert", "alpha", "beta", "gamma");
  global $TarskiDefinitions;
  foreach($TarskiDefinitions as $d)
    { $allowed[] = $d->definiens;
	}
  if(is_array($x))
	{ foreach($x as $y)
		{ $temp = symbols_in($y);
		  $a = $temp[0];
		  $b = $temp[1];
		  foreach($a as $z)
		      { if(! in_array($z, $a))
					$atoms[] = $z;
			  }
		  foreach($b as $z)
			  { if(! in_array($z, $b))
					$functions[] = $z;
			  }
		}
	  return array($atoms,$functions);
    }
  // Now $x$ is a string
  if(strstr($x, "|"))
     return symbols_in(explode("|", $x));
  if(strstr($x, "!="))
     return symbols_in(explode("!=", $x));
  if(strstr($x, "="))
     return symbols_in(explode("=", $x));
  $pieces = array_filter(preg_split( "/[,\(\)\.]/", $x), "strlen");
  foreach($pieces as $piece)
     { $piece = trim($piece);
	   if($piece == "")
	      continue;
	   if(in_array($piece, $allowed))
	      continue;
	   $j = strpos($x,  $piece . "(");
	   if($j===0 || ($j > 0  && !ctype_alpha($x[$j-1])))  // must use ===, not just == 
	      { // echo "$x $temp33\n";
		    $functions[] = $piece;
			$ell = strstr($x, $piece . ",");
			$m = strstr($x, $piece . ")");
			if( 
				($ell === 0 || ($ell > 0 && !ctype_alpha($x[$ell-1]))) ||
				($m === 0 || ($m > 0 && !ctype_alpha($x[$m-1])))
			  )
		        echo "$x contains $piece both as function symbol and constant.\n";
		  }
	   else if (strstr($x, $piece . ",") || strstr($x, $piece . ")") || trim($x) == $piece)
	      {  $atoms[] = $piece;
		  }
	   else  
	      {  echo "Trouble: $piece seems ungrammatically used in $x\n.";
		  }
	}
  $ans = array($atoms,$functions);
  return $ans;
}
/*__________________________________________________________*/
function atoms_in($x)
{  $s = symbols_in($x);
   return $s[0];
}
/*__________________________________________________________*/
function functors_in($x)
{  $s = symbols_in($x);
   return $s[1];
}
	   
/*__________________________________________________________*/
function TestDiagram($t, $SkolemSymbols)
// $t should be a member of $TarskiTheorems. 
// $SkolemSymbols should be an array containing all the Skolem symbols 
// of theorems occurring earlier in the master list $TarskiTheorems.
// Check each line $line of $t->Diagram and report any violations of the 
// following rules:  $line must be an equation, introducing a new constant
// on the left, and on the right must occur only variables and constants from
// $t->NegatedForm and Skolem symbols from $SkolemSymbols, plus ip, ext, and insert.
{  if(!is_array($t->Diagram))
		return;
   $atoms = atoms_in($t->NegatedForm);
   $theorem_name = $t->name;
   foreach($t->Diagram as $line)
		{ if(strstr($line, "!="))
			 { echo "Diagram of $theorem_name contains an inequality\n";
			   continue;
			 }
		  $sides = explode("=", $line);
		  if(count($sides) != 2)
			 { echo "Diagram of $theorem_name is not an equation.\n";
			   continue;
			 }
		  $left = trim($sides[0]);
		  $right = trim($sides[1]);
		  if(in_array($left,$atoms))
			 { echo "Left side of the diagram of $theorem_name is not a new constant: it is already used.\n";
			   continue;  //  with the next line of the diagram
			 }
		  $c = $left[0];
		  if(!strchr("abcdepqrtfmkjoPQR",$c))
			 { echo "Left side of the diagram of $theorem_name begins with an unrecognized letter $c for a constant.\n";
			   continue;
		     }
		  $permitted = array("cx", "cy", "cs", "ca", "cb", "cu", "cv", "cstar", "bstar", "cz", "cx1", "m", "j","aone","cone", "one", "tt", "rr");
		  if(strlen($left) == 3 && is_numeric($left[2]))
		     { $left = substr($left,0,2);
			 }
		  if(strlen($left) > 1 && ! in_array($left, $permitted) && !is_numeric(substr($left,1)))
		     { echo "Left side of the diagram of $theorem_name, which is $left, has a suspicious form, please check it.\n";
			 }
		  // Now turning to the right side of $line
		  $right_atoms = atoms_in($line);
		  // everything in $right_atoms must already be in $atoms
		  foreach($right_atoms as $atom)
			 { if(!in_array($atom, $atoms))  // atoms_in does not count alpha, beta, and gamma
				  { echo "Right side of the diagram of $theorem_name introduces a new symbol, which is illegal.\n";
					break;
				  }
			 }
		 $atoms[] = $left; // subsequent lines of the diagram are allowed to use this constant.
		 $functions = functors_in($line);
		 if(!is_array($functions))
			continue;
		 // every member of $functions must already occur in $SkolemSymbols.  Functors_in omits ext, ip, insert.
		 foreach($functions as $f)
			{ if (!in_array($f,$SkolemSymbols))
					echo "Diagram of $theorem_name introduces a new functions symbol, which is illegal.\n";
			}
		}
}		  
/*__________________________________________________________*/
function is_tautology($line)
// return true or false according as $line is a tautology.
{   if(! is_string($line))
		return false;
	$r = explode('|', $line);
	if(count($r) != 2)
	   return false;
	$a = str_replace(' ', '', trim($r[0]));
	$b = str_replace(' ', '', trim($r[1]));
	if($a[0] == '-' && substr($a,1) == $b)
	   return true;
	if($b[0] == '-' && substr($b,1) == $a)
	   return true;
	if(strstr($a, "!=") && str_replace("!=", "=", $a) == $b)
	   return true;
	if(strstr($b, "!=") && str_replace("!=", "=", $b) == $a)
	   return true;
	return false;
}
/*__________________________________________________________*/
// Following is the main loop that tests the master list.
// It checks whether each theorem has been correctly Skolemized,
// whether there are any duplicate Skolem symbols, and 
// whether the diagram of each theorem has the allowed form.
// See TestDiagram for the definition of "allowed form".
// If there is a Cases field in the theorem, its contents should be tautologies.

$SkolemSymbols = array();
foreach ($TarskiTheorems as $t)
{	$n = count($t->PositiveForm);
	$Neg = $t->NegatedForm;
	$count = 0;
	foreach($Neg as $clause)
		{ if(strchr($clause,"|"))
			++$count;
		}
	if($count == 1 && $t->name != "Satz4.6")  // Satz 4.6 has an equality axiom, which will be ignored.
		{ // just one disjunction in sos
		  $distributed = strip_disjunction($t->NegatedForm);
		  $n = count($distributed);
		  $error = 0;
		  if($n != count($t->PositiveForm))
			{ echo "error in "; echo $t->name; echo " $n\n"; 
			  die();
			}
		  for($i = 0; $i< $n; $i++)
		     { $test1 =  str_replace(' ', '', $t->PositiveForm[$i]);
			   $test2 =  str_replace(' ', '', negate_theorem($distributed[$i], $t->SkolemSymbols));	
			   if($test1 != $test2)
			    	{ echo "There's trouble with $t->name line $i:\n";
					  echo "     $test1\n";
				  	  echo "     $test2\n";
					  ++$error;
					}
			}
		  if(!$error)
			echo "$t->name OK\n";
		}
	else if($count == 0)
	  { $test1 =  str_replace(' ', '', $t->PositiveForm[0]);
		$test2 =  str_replace(' ', '', negate_theorem($t->NegatedForm, $t->SkolemSymbols));
		if($test1 == $test2)
	    	{ echo "$t->name OK\n";
			}
		else
	    	{ echo "There's trouble with $t->name\n";
			  echo "     $test1\n";
		  	  echo "     $test2\n";
			}
	  }
	else if($t->name != "Satz4.6") 
	  { echo $t->name;  echo " has more than one disjunction.\n";
	  }
	$functions = functors_in($t->NegatedForm);
	foreach($functions as $f)
		{ if( !in_array($SkolemSymbols,$f))
			 echo "t->name", " introduces a new function symbol, which is illegal.\n";
		}
	if(is_array($t->Diagram))
		TestDiagram($t,$SkolemSymbols);  
	if($t->Cases != "")
	    { if(!is_array($t->Cases))
			 { echo $t->name; 
			   echo " Cases field must be an empty string or an array.\n";
			 }
		  else
		     { $theorem_name = $t->name;
			   foreach($t->Cases as $line)
				  { // check whether $line is a tautology
					if(! is_string($line))
						{ echo "Cases field of $theorem_name must contain an array of strings defining tautologies.\n";
						  continue;
						}
					if(!is_tautology($line))
						echo "Cases field of $theorem_name contains a non-tautology, namely $line.\n";
				  }
			  }
		 }	   
	if(is_array($t->SkolemSymbols))
	  { foreach($t->SkolemSymbols as $f)
			{ if(in_array($f, $SkolemSymbols))
				{ echo "Duplicate Skolem symbol $f in "; echo "$t->name\n";
				}
			  else
				$SkolemSymbols[] = $f;
			}
	  }
}

 

?>