<?php

class knowledgeBase {
	//This class represents the knowledge base of the inference engine
	//facts and rules can be added or subtracted or the knowledge base
	//can be asked to infer what it can from the existing knowledge base
	
	var $facts;
	var $rules;
	var $jtms;
	
	function register_jtms(&$jtms){
		$this->jtms =& $jtms;
		$this->jtms->test();
		//$jtms =& $this->jtms;
		//$jtms->test();
	}
	
	function knowledgeBase(){
		//creates a new empty knowledge base
		$this->rules = array();
		$this->facts = array();
	}
	
	function add_rule($rule){
		//adds a rule to the knowledge base
		//if it doesn't exist return true
		if(!in_o_array($rule, $this->rules)){
			array_push($this->rules, $rule);
			return true;
		}
		return false;
	}
	
	function add_fact($fact){
		//adds a fact to the knowledge base
		//if it doesn't exist return true
		//echo("\nAdding fact:");
		//		print_r($fact);
		if(!in_o_array($fact, $this->facts)){
		if($this->jtms){
			$this->jtms->jtms_add_justification_set($fact, "true");
		}
		}
		if(!in_o_array($fact, $this->facts)){
			$this->facts[] = $fact;
			return true;
		}
		return false;
	}
	
	function add_fact_and_justify($fact, $justifications){
		//adds a fact to the knowledge base
		//if it doesn't exist return true
		if($this->jtms){
			$this->jtms->jtms_add_justification_set($fact, $justifications);
		}
		if(!in_o_array($fact, $this->facts)){
			array_push($this->facts, $fact);
			return true;
		}
		return false;
	}
	
	
	function retract_rule($rule){
		//removes a rule if it exists from the knowledgebase
		if(in_o_array($rule, $this->rules)){
			foreach($this->rules as $existingRule){
				if($existingRule != $rule){
					$remainingRules[] = $existingRule;
				}
			}
			$this->rules = $remainingRules;
			return true;
		}
		return false;
	}
	
	function retract_fact($fact){
		//removes a fact if it exists from the knowledgebase
		if(in_o_array($fact, $this->facts)){
			if(isset($this->facts)){
			foreach($this->facts as $existingFact){
				if($existingFact != $fact){
					$remainingFacts[] = $existingFact;
				}
			}
			}
			$this->facts = $remainingFacts;
			if($this->jtms){
				$retractions = $this->jtms->jtms_retract($fact);
				if(isset($retractions)){
				foreach($retractions as $retractMe){
					if(isset($retractMe)){
					$this->retract_fact($retractMe);	
					}
				}
				}
			}
			return true;
		}
		return false;
	}
	
	function modus_ponens(){
		//performs modus ponens
		$changed = true;
		while($changed){
			$changed = false;
			foreach($this->rules as $rule){
				$unifications = $this->unify_rule($rule);
				if($unifications != false){
					foreach($unifications as $uSet){
						$head = NULL;
						$justifications = array();
						foreach($uSet as $key => $value){
							if($key === "head"){
								$head = $value;	
							}
							else{
								$justifications[] = $value;	
							}	
						}
						if($this->add_fact_and_justify($head, $justifications)){
							$changed = true;	
						}
					}	
				}	
			}	
		}	
	}
	
	function unify_rule($rule, $matches = array()){
		if(count($rule->horns) == 0){
			//base case, there are no more horns to unify
			$matches2 = array();
			foreach($matches as $match){
				$match["head"] = $rule->head;
				$matches2[] = $match;
			}
			return $matches2;
		}
		else{
			$found = array();
			$subs = array();
			foreach($this->facts as $fact){
				//cycle through to find each match
				$test = $this->unify($rule->horns[0], $fact);
				if(get_class($test) == "match"){
					$found[] = $test->arg2;
					$subs[] = $test->substitutions;
				}
			}
			if(count($found) == 0){
				return false;
			}
			else{
				$answer = array();
				for($i = 0; $i < count($found); $i++){
					$sofar = array();
					$recRule = new rule($rule->head, array_slice($rule->horns, 1));
					foreach($subs[$i] as $key => $value){
						$recRule->apply_subs($key, $value);
					}
					//sort out the matches array
					if(count($matches) == 0){
							$sofar[] = array($found[$i]);
					}
					else{
						foreach($matches as $match){
							$match[] = $found[$i];
							$sofar[] = $match;
						}
					}
					$testAnswer = $this->unify_rule($recRule, $sofar);
					if($testAnswer != false){
						foreach($testAnswer as $ansKey => $cand){
							$answer[] = $cand;
						}
					}
				}
				return $answer;
			}
		}
	}
	
	function unify($one, $two){
		$class = get_class($one);
		$class2 = get_class($two);
		//echo("**$class**$class2**");
		if(get_class($one) == "atom" && get_class($two) == "atom" && $one == $two){
			return new match($one, $two);
		}
		elseif(get_class($one) == "variable" && get_class($two) == "atom"){
			$match = new match($one, $two);
			$match->add_substitution($one->name, $two);
			return $match;
		}
		elseif(get_class($one) == "fact" && get_class($two) == "fact"){
			//echo("<br>Two facts identified</br>");
			if(sizeof($one->arguments) != sizeof($two->arguments)){
				return false;
			}
			elseif($one->name != $two->name){
				return false;
			}
			else{
				$match = new match($one, $two);
				$flag = true;
				for($i = 0; $i < sizeof($one->arguments); $i++){
					$onearg = $one->arguments[$i];
					$twoarg = $two->arguments[$i];
					$S = $this->unify($onearg, $twoarg);
					if($S === false){
						return false;
					}
					elseif(get_class($S) == "match"){
						foreach($S->substitutions as $key => $value){
							if(isset($match->substitutions["$key"])	&& $match->substitutions["$key"] != $value){
							}
							else{
								$match->add_substitution($key, $value);
							}
						}
					}
				}
				$match->propogate_instantiations();
				return $match;
			}
		}
		else{
			return false;
		}
	}
	
}
?>