#!/usr/bin/php
<?php 
require_once("TarskiTheorems.php");
require_once("GenerateInputFiles.php");
require_once("FinalResults.php");

 
$chapter = "10";
// $test_only = "Lemma12.11-case2";
$only_unproved = false;   // if true, only tries so-far-unproved theorems, i.e. with 'false' result.
$skip_unproved = false;     //  only check theorems that have some result already listed
$check_level = 7;    //  1,  check only theorems with numerical results, not using   diagrams or hints.
                     //  2,  check only theorems with array(number,"diagram")  values, using diagrams but not hints
                     //  3,  check both the above two, using diagrams if $diagrams is set to true, otherwise
                     //  only for theorems with array(number, "diagrams") values
                     //  4,  check theorems with array(number, "hints")  values.  Use diagrams too.
                     //  combine these as bit flags, so e.g. 7 checks everything. 
                     
$diagrams = false;   //  but it will be set to true if the result is already array(number, "diagrams")
$hints = "default";   // set to true or false to override what's already in TarskiFinalResults
$cases = false;
$default_max_seconds = 120;
$hint_max_seconds = 30;
$default_max_weight = 20; 
$default_ratio = 4;
$hint_max_weight = $chapter == 9 ? 9 : 8;   


$sos = false;
$directory = "Inputs";
$OldProofDir = "Proofs";

function get_settings($max_weight, $max_seconds, $ratio = 4)
{ 
$settings = array(
"set(hyper_res).",
"set(para_into).",
"set(para_from).",
"set(binary_res).",
"set(ur_res).",
"set(order_history).",
"assign(max_seconds,$max_seconds).",
"assign(max_mem,2000000).",
"clear(print_kept).",
"set(input_sos_first).",
"set(back_sub).",
"assign(bsub_hint_wt,-1).",
"set(keep_hint_subsumers).",
"assign(max_weight,$max_weight).",
"assign(max_distinct_vars,4).",
"assign(pick_given_ratio,$ratio).",
"assign(max_proofs,1)."
);
return $settings;
}

$theorems = TheoremsByChapter($chapter);
$hints_in = $hints;
$diagrams_in = $diagrams;
$ratio_in = $default_ratio;

foreach($theorems as $t)
	{   // if($t->name != $test_only) continue; 
		$hints = $hints_in;
		$ratio = $ratio_in;
		$diagrams = $diagrams_in;
		$result = $TarskiFinalResults[$t->name];
		if(! is_array($result) && trim($result) == "skip")
		    continue;
		if(($check_level & 1) == 0 && is_numeric($result))
		    continue;
		if(($check_level & 1) == 0 && is_array($result) && count($result) == 2  && is_numeric($result[0]) && strstr($result[1],"="))
		   { //example, $result = array(11, "max_seconds = 140")
			 continue;
		   }	   
		if(is_array($result) && $result[1] == "subformula")
		    continue;  // use TestSubformulaStrategy.php instead 
		if(is_array($result) && $result[1] == "diagram" && ($check_level & 2) == 0)
		    continue;
		if($result === false && $skip_unproved)
		    continue; 
		if(!$only_unproved || $result ===false)
		 {  if($hints == "default")
				{ if(is_array($result) && $result[1] == "diagram")
					 { $hints = false;
					   $diagrams = true;
					 }
				  else if(is_array($result) && $result[1] == "hints")
			    	 { $hints = true;
					   $diagrams = true;  // always use the diagram with hints.
					 }
				  else
					 { $hints = false;
					   // don't change the value of $diagrams from what was specified at the top of the file.
					 }
		    	}
			$cases = $hints;  // use cases if and only if using hints
			if($hints && $check_level < 4)
				continue;
			if($hints)
				{ $max_weight = $hint_max_weight;
				  $max_seconds = $hint_max_seconds;
				}
			else
				{ $max_weight = $default_max_weight;
				  $max_seconds = $default_max_seconds;
				}	
			//  we may need to adjust max_seconds or max_weights based on stored results		
			if (is_array($result) && count($result) > 1)  
			    { $weightflag = 0;
				  $timeflag = 0;
				  foreach($result as $line)
					{ if(strstr($line, "max_weight"))
						{ $temp = explode("=", $line);
						  $max_weight = trim($temp[1]);
						  $weightflag = 1;
						}
					  if(strstr($line, "max_seconds"))
						{ $temp = explode("=", $line);
						  $max_seconds = trim($temp[1]);
						  $timeflag = 1;
					    }
					  if(strstr($line, "ratio"))
							{ $temp = explode("=", $line);
							  $ratio = trim($temp[1]);
							  $timeflag = 1;
						    }
					}
				}	
			$settings = get_settings($max_weight, $max_seconds, $ratio);
			WriteInputFile($t, $directory, $diagrams, $settings, $sos, $cases);
			$theorem_name = $t->name;
			if($hints)
				InsertHintsIntoInputFile($theorem_name,$OldProofDir, $directory);
			$infile = $directory . "/" . $theorem_name . ".in";
			$outfile = $directory . "/" . $theorem_name . ".out";
			
			echo "Trying to prove $theorem_name ";
			if($hints)
			   echo "with hints";
			else
			   echo "without hints";
			if($diagrams && !$hints)
			   echo " but with diagrams";
			else if(!$hints)
			   echo " and without diagrams";
			echo " and with max_weight = $max_weight and max_seconds = $max_seconds.";
			exec( "otter < $infile > $outfile");
		 }
	}
?>