<?php
set_time_limit(10);
define('PARO', -1);
define('PARC', -2);
define('VAL_FALSE', 0);
define('VAL_TRUE', 1);
define('OP_NOT', 2);
define('OP_AND', 3);
define('OP_NAND', 4);
define('OP_OR', 5);
define('OP_NOR', 6);
define('OP_XOR', 7);
define('OP_IMPLIES', 8);
define('OP_NOT_IMPLIES',9);
define('OP_IMPLIED', 10);
define('OP_NOT_IMPLIED',11);
define('OP_IFF', 12);
define('OP_MIN', OP_NOT);
define('OP_MAX', OP_IFF);
/**
* Classe définissant une proposition en logique du premier ordre. Vous pouvez
* manipuler la syntaxe acceptée (et produite lors de l'affichage), et appliquer
* des opérations simples sur la formule logique.
*
* Les opérateurs de base sont utilisés (et, ou, non, implication, et leurs
* composés habituels). La syntaxe par défaut est la suivante:
* <ul>
* <li><u>negation</u>: <b style="color:red">!</b></li>
* <li><u>et</u>: <b style="color:red">&</b></li>
* <li><u>non et</u>: <b style="color:red">!&</b></li>
* <li><u>ou</u>: <b style="color:red">|</b></li>
* <li><u>non ou</u>: <b style="color:red">!|</b></li>
* <li><u>ou exclusif</u>: <b style="color:red"><!></b></li>
* <li><u>implication</u>: <b style="color:red">-></b></li>
* <li><u>non implication</u>: <b style="color:red">-!></b></li>
* <li><u>implication gauche</u>: <b style="color:red"><-</b></li>
* <li><u>non implication gauche</u>: <b style="color:red"><!-</b></li>
* <li><u>equivalence</u>: <b style="color:red"><-></b></li>
* </ul>
*
* Les opérateurs suivent cet ordre dans la priorité, c'est-à-dire que
* "(a & b) | c" est strictement equivalent à "a & b | c".
*
* $lang FR
*
* @author hide@address.com
* @version 1.3
* @date 2003-10-07
**/
class FirstOrderLogicProp
{
//-----------------------
// public attributes
//-----------------------
/**
* Masque PCRE (le délimiteur est '/', à ne pas inclure dans ce masque) de
* reconnaissance des variables atomiques.
*
* @type string
* @public
**/
var $PCRE_variable = '[a-z][a-z0-9_]*';
//-----------------------
// #ctor
//-----------------------
/**
* Le constructeur de proposition logique du premier ordre
*
* @type FirstOrderLogicProp
* @param string formula la formule à lire. Si ce paramètre n'est pas spécifié
* on ne lit aucune formule, et il faudra appeler la méthode <i>parse</i> par
* la suite
* @param bool expand si ce paramètre est à TRUE, on appellera la méthode
* <i>expand</i> après lecture.
* @public
**/
function FirstOrderLogicProp ( $formula = NULL , $expand = FALSE )
{
// symbolic syntax
$this->addSyntax ('1', VAL_TRUE);
$this->addSyntax ('0', VAL_FALSE);
$this->addSyntax ('!', OP_NOT);
$this->addSyntax ('&', OP_AND);
$this->addSyntax ('!&', OP_NAND);
$this->addSyntax ('|', OP_OR);
$this->addSyntax ('!|', OP_NOR);
$this->addSyntax ('<!>', OP_XOR);
$this->addSyntax ('->', OP_IMPLIES);
$this->addSyntax ('-!>', OP_NOT_IMPLIES);
$this->addSyntax ('<-', OP_IMPLIED);
$this->addSyntax ('<!-', OP_NOT_IMPLIED);
$this->addSyntax ('<->', OP_IFF);
// parsing formula
if (NULL !== $formula) $this->parse($formula, $expand);
}
//-----------------------
// public functions : operators
//-----------------------
/**
* Effectue l'opération sur l'opérateur passé en paramètre
*
* <b style="color:red">ATTENTION !!</b> dans le cas de l'opérateur unaire NOT,
* ne spécifiez pas d'opérande. L'opérateur est appliqué sur l'objet.
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a & b');
* $a->operate(OP_NOT);
* $a->writeLn(); // affiche "! (a & b)";
* $a->operate(OP_IMPLIES, new FirstOrderLogicProp('a | c'));
* $a->writeLn(); // affiche "(! (a & b)) -> (a | c)"
* </code>
*
* @param int op l'opérateur à appliquer. Utiliser une constante parmi OP_NOT,
* OP_AND, OP_NAND, OP_OR, OP_NOR, OP_XOR, OP_IMPLIES, OP_NOT_IMPLIES,
* OP_IMPLIED, OP_NOT_IMPLIED, OP_IFF
* @param FirstOrderLogic operand la formule sur laquelle appliquer l'opérateur
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon (opérateur invalide, proposition
* non définie).
* @public
**/
function operate ( $op , $operand = NULL )
{
if ($op!==OP_NOT && $op!==OP_OR && $op!==OP_AND && $op!==OP_NOR && $op!==OP_NAND && $op!==OP_XOR
&& $op!==OP_IFF && $op!==OP_IMPLIES && $op!==OP_NOT_IMPLIES && $op!==OP_IMPLIED && $op!==OP_NOT_IMPLIED)
return FALSE;
if (FALSE===$this->__formula) return FALSE;
if ($operand===NULL && $op===OP_NOT) {
$this->__setFormula ($this->__expression($op, NULL, $this->__formula));
}
elseif ($op!==OP_NOT) {
$this->__setFormula ($this->__expression($op, $this->__formula, $operand->__formula));
}
else return FALSE;
return TRUE;
}
/**
* Effectue un OU avec l'opérande
* Equivalent de operate(OP_OR, $operand)
*
* <b style="color:red">ATTENTION !!</b> notez le '_' final dans le nom de la
* méthode, pour éviter le conflit avec une notation réservée de PHP.
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a');
* $b = &new FirstOrderLogicProp('b');
* $a->or_($b);
* $a->writeLn(); // affiche "a | b"
* </code>
*
* @param FirstOrderLogic operand la formule sur laquelle appliquer l'opérateur
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon.
* @public
**/
function or_ ( $operand ) { return $this->operate(OP_OR, $operand); }
/**
* Effectue un ET avec l'opérande
* Equivalent de operate(OP_AND, $operand)
*
* <b style="color:red">ATTENTION !!</b> notez le '_' final dans le nom de la
* méthode, pour éviter le conflit avec une notation réservée de PHP.
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a');
* $b = &new FirstOrderLogicProp('b');
* $a->and_($b);
* $a->writeLn(); // affiche "a & b"
* </code>
*
* @param FirstOrderLogic operand la formule sur laquelle appliquer l'opérateur
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon.
* @public
**/
function and_ ( $operand ) { return $this->operate(OP_AND, $operand); }
/**
* Effectue un NOR avec l'opérande
* Equivalent de operate(OP_NOR, $operand)
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a');
* $b = &new FirstOrderLogicProp('b');
* $a->nor($b);
* $a->writeLn(); // affiche "a !| b"
* </code>
*
* @param FirstOrderLogic operand la formule sur laquelle appliquer l'opérateur
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon.
* @public
**/
function nor ( $operand ) { return $this->operate(OP_NOR, $operand); }
/**
* Effectue un NAND avec l'opérande
* Equivalent de operate(OP_NAND, $operand)
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a');
* $b = &new FirstOrderLogicProp('b');
* $a->nand($b);
* $a->writeLn(); // affiche "a !& b"
* </code>
*
* @param FirstOrderLogic operand la formule sur laquelle appliquer l'opérateur
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon.
* @public
**/
function nand ( $operand ) { return $this->operate(OP_NAND, $operand); }
/**
* Effectue un OU EXCLUSIF avec l'opérande
* Equivalent de operate(OP_XOR, $operand)
*
* <b style="color:red">ATTENTION !!</b> notez le '_' final dans le nom de la
* méthode, pour éviter le conflit avec une notation réservée de PHP.
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a');
* $b = &new FirstOrderLogicProp('b');
* $a->xor_($b);
* $a->writeLn(); // affiche "a <!> b"
* </code>
*
* @param FirstOrderLogic operand la formule sur laquelle appliquer l'opérateur
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon.
* @public
**/
function xor_ ( $operand ) { return $this->operate(OP_XOR, $operand); }
/**
* Effectue un IMPLIQUE avec l'opérande
* Equivalent de operate(OP_IMPLIES, $operand)
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a');
* $b = &new FirstOrderLogicProp('b');
* $a->implies($b);
* $a->writeLn(); // affiche "a -> b"
* </code>
*
* @param FirstOrderLogic operand la formule sur laquelle appliquer l'opérateur
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon.
* @public
**/
function implies ( $operand ) { return $this->operate(OP_IMPLIES, $operand); }
/**
* Effectue un IMPLIQUE GAUCHE avec l'opérande
* Equivalent de operate(OP_IMPLIED, $operand)
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a');
* $b = &new FirstOrderLogicProp('b');
* $a->implied_by($b);
* $a->writeLn(); // affiche "a <- b"
* </code>
*
* @param FirstOrderLogic operand la formule sur laquelle appliquer l'opérateur
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon.
* @public
**/
function implied_by ( $operand ) { return $this->operate(OP_IMPLIED, $operand); }
/**
* Effectue un NON IMPLIQUE avec l'opérande
* Equivalent de operate(OP_NOT_IMPLIES, $operand)
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a');
* $b = &new FirstOrderLogicProp('b');
* $a->not_implies($b);
* $a->writeLn(); // affiche "a -!> b"
* </code>
*
* @param FirstOrderLogic operand la formule sur laquelle appliquer l'opérateur
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon.
* @public
**/
function not_implies ( $operand ) { return $this->operate(OP_NOT_IMPLIES, $operand); }
/**
* Effectue un NON IMPLIQUE GAUCHE avec l'opérande
* Equivalent de operate(OP_NOT_IMPLIED, $operand)
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a');
* $b = &new FirstOrderLogicProp('b');
* $a->not_implied_by($b);
* $a->writeLn(); // affiche "a <!- b"
* </code>
*
* @param FirstOrderLogic operand la formule sur laquelle appliquer l'opérateur
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon.
* @public
**/
function not_implied_by ( $operand ) { return $this->operate(OP_NOT_IMPLIED, $operand); }
/**
* Effectue un EQUIVALENT avec l'opérande
* Equivalent de operate(OP_IFF, $operand)
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a');
* $b = &new FirstOrderLogicProp('b');
* $a->iff($b);
* $a->writeLn(); // affiche "a <-> b"
* </code>
*
* @param FirstOrderLogic operand la formule sur laquelle appliquer l'opérateur
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon.
* @public
**/
function iff ( $operand ) { return $this->operate(OP_IFF, $operand); }
/**
* Effectue un NON
* Equivalent de operate(OP_NOT)
*
* <b style="color:red">ATTENTION !!</b> notez le '_' final dans le nom de la
* méthode, pour éviter le conflit avec une notation réservée de PHP.
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a');
* $a->not_();
* $a->writeLn(); // affiche "! a"
* </code>
*
* @type bool
* @return TRUE si l'opération a réussi, FALSE sinon.
* @public
**/
function not_ ( ) { return $this->operate(OP_NOT); }
//-----------------------
// public functions : others
//-----------------------
/**
* Ajoute une syntaxe pour un opérateur ou une constante. Si la fonction est
* appelée avec succès, la syntaxe introduite est ensuite reconnue, et c'est
* cette syntaxe qui sera utilisée pour l'affichage.
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $prop = &new FirstOrderLogicProp("a & b");
* $prop->write(); // affiche "a & b"
* $prop->addSyntax('AND', OP_AND);
* $prop->write(); // affiche "a AND b"
* $prop->parse('b AND c'); // ceci aurait provoqué
* // une erreur sans l'appel précédent à <i>addSyntax</i>
* </code>
*
* @param string syntax la syntaxe introduite pour l'élément
* @param mixed value l'élément reconnu par la syntaxe. Utiliser une constante
* parmi OP_NOT, OP_AND, OP_NAND, OP_OR, OP_NOR, OP_XOR, OP_IMPLIES, OP_NOT_IMPLIES,
* OP_IMPLIED, OP_NOT_IMPLIED, OP_IFF pour les opérateurs. Utiliser une constante
* parmi VAL_TRUE, VAL_FALSE pour les constantes propositionnelles.
* @type bool
* @return TRUE en cas de succès, FALSE sinon.
* @public
**/
function addSyntax ( $syntax , $value )
{
if ($value !== VAL_TRUE && $value !== VAL_FALSE && ($value > OP_MAX || $value < OP_MIN)) return FALSE;
$syntax = strtoupper($syntax);
if (isset($this->__syntax[$syntax])) return FALSE;
$this->__syntax[$syntax] = $value;
// preparing pcre masks
if ($value === VAL_TRUE || $value === VAL_FALSE) {
$this->__PCRE_vars[] = $syntax;
}
elseif ($value === OP_NOT) {
$this->__PCRE_un_ops[] = $syntax;
}
else {
$this->__PCRE_bin_ops[] = $syntax;
}
$this->__printSyntax[$value] = $syntax;
return TRUE;
}
/**
* lit un fichier de syntaxe pour ajouter la reconnaissance de cette syntaxe
* dans l'objet. Dans ce fichier, les lignes vides sont ignorés, les lignes
* commençant par # sont ignorées également (vous pouvez ainsi mettre des
* commentaires).
* Pour indiquer une syntaxe dans ce fichier, il suffit de mettre une ligne
* de la forme <code style="color:blue">ELEMENT: SYNTAXE</code>.
* <code style="color:blue">ELEMENT</code> peut être FALSE, TRUE, NOT, AND,
* NAND, OR, NOR, XOR, IMPLIES, NOT_IMPLIES, IMPLIED, NOT_IMPLIED, ou IFF.
* <code style="color:blue">SYNTAXE</code> ne doit contenir ni saut de ligne,
* ni caractère d'espacement.
*
* <b style="color:red">ATTENTION !!!</b> S'il y a une erreur dans votre fichier
* toutes les lignes AVANT LA LIGNE ERRONNEE auront été traitées tout de même !
*
* <u>Exemple</u>:
* <pre style="color:darkblue">
* # litteral syntax
*
* TRUE: TRUE
* FALSE: FALSE
* NOT: NOT
* AND: AND
* NAND: NAND
* OR: OR
* NOR: NOR
* XOR: XOR
* IMPLIES: IMPLIES
* NOT_IMPLIES: NOT_IMPLIES
* IMPLIED: IMPLIED_BY
* NOT_IMPLIED: NOT_IMPLIED_BY
* IFF: IF_ONLY_IF
* </pre>
*
* @type bool
* @param string filename le fichier à lire
* @return TRUE si l'ajout a réussi
* @public
**/
function addSyntaxFile ( $filename )
{
$lines = @file($filename);
if (FALSE === $lines) return FALSE;
$ops = array(
'FALSE' => VAL_FALSE,
'TRUE' => VAL_TRUE,
'NOT' => OP_NOT,
'AND' => OP_AND,
'NAND' => OP_NAND,
'OR' => OP_OR,
'NOR' => OP_NOR,
'XOR' => OP_XOR,
'IMPLIES' => OP_IMPLIES,
'NOT_IMPLIES' => OP_NOT_IMPLIES,
'IMPLIED' => OP_IMPLIED,
'NOT_IMPLIED' => OP_NOT_IMPLIED,
'IFF' => OP_IFF
);
foreach ($lines as $line) {
$line = trim($line);
if ($line=='') continue;
if ($line{0}=='#') continue;
foreach ($ops as $op => $val) if (preg_match("/^$op\s*:\s*([^\s]*?)\s*$/i", $line, $m)) {
$this->addSyntax($m[1], $val);
continue 2;
}
return FALSE;
}
return TRUE;
}
/**
* lit une formule dans la syntaxe acceptée.
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $logic = &new FirstOrderLogicProp;
* $formula = '(b & ! a) -> b';
* $logic->parse($formula);
* </code>
*
* En cas d'erreur dans la syntaxe de la formule, des exceptions de niveau
* E_USER_WARNING peuvent être levées.
*
* @type bool
* @param string formula la formule à lire
* @param bool expand si ce paramètre est à TRUE, on appellera la méthode
* <i>expand</i> après lecture.
* @return TRUE en cas de succès, FALSE sinon
* @public
**/
function parse ( $formula , $expand = FALSE )
{
$tree = $this->__parse ($formula);
if (FALSE !== $tree) {
$this->__setFormula ($tree);
if ($expand) $this->expand ();
return TRUE;
}
else {
$this->__setFormula (FALSE);
return FALSE;
}
}
/**
* Développe la formule en effectuant les remplacements des opérateurs par des
* combinaisons de propositions n'utilisant que les opérateurs OU, ET, et NON.
* Si le développement réussit, vous avez une formule équivalente à la précédente
* et n'utilisant que les opérateurs OU, ET, NON.
*
* Les remplacement suivants sont effectués:
* <ul>
* <li><b style="color:red">A -> B</b> deviendra <b style="color:green">(! A) | B</b></li>
* <li><b style="color:red">A <- B</b> deviendra <b style="color:green">(! B) | A</b></li>
* <li><b style="color:red">A -!> B</b> deviendra <b style="color:green">! (A -> B)</b></li>
* <li><b style="color:red">A <!- B</b> deviendra <b style="color:green">! (A <- B)</b></li>
* <li><b style="color:red">A <-> B</b> deviendra <b style="color:green">(A -> B) & (A <- B)</b></li>
* <li><b style="color:red">A !| B</b> deviendra <b style="color:green">! (A | B)</b></li>
* <li><b style="color:red">A !& B</b> deviendra <b style="color:green">! (A & B)</b></li>
* <li><b style="color:red">A <!> B</b> deviendra <b style="color:green">!(A <-> B)</b></li>
* </ul>
* <i>A et B représentent des propositions logiques quelconques</i>
*
* @type bool
* @return TRUE si le développement a réussi, FALSE sinon.
* @public
**/
function expand ( )
{
if (NULL === $this->__expand) {
$formula = $this->__formula;
if (FALSE !== $formula) $formula = $this->__expand ($formula);
if (FALSE !== $formula) $this->__setFormula ($formula);
$this->__expand = FALSE!==$formula;
}
return $this->__expand;
}
/**
* Ecriture de la proposition
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $prop = &new FirstOrderLogicProp('(A & B) | ((C) | (D & E)) | (F<!>G)');
* $prop->write(); // affiche "(A & B) | C | (D & E) | (F <!> G)"
* $prop->write(FALSE); // affiche "A & B | C | D & E | (F <!> G)"
* </code>
*
* @type string
* @param bool strictParenthesis si ce paramètre est à TRUE, on applique le parenthésage
* strict, c'est-à-dire que si une opérande est une formule utilisant un opérateur
* différent, on le parenthèse. Sinon on ne parenthèse que le strict minimum, pour
* respected les priorités.
* @return la formule ecrite avec la derniere syntaxe introduite.
* @public
**/
function toString ( $strictParenthesis = TRUE )
{
if (FALSE === $this->__formula) return FALSE;
if (($strictParenthesis && NULL === $this->__toStringStrict) || (!$strictParenthesis && NULL === $this->__toString)) {
if (FALSE !== $this->__formula) {
if ($strictParenthesis) $this->__toStringStrict = $this->__toString($this->__formula, TRUE);
else $this->__toString = $this->__toString($this->__formula, FALSE);
}
}
return $strictParenthesis ? $this->__toStringStrict : $this->__toString;
}
/**
* Affichage de la proposition
*
* @type void
* @param bool strictParenthesis si ce paramètre est à TRUE, on applique le parenthésage
* strict, c'est-à-dire que si une opérande est une formule utilisant un opérateur
* différent, on le parenthèse. Sinon on ne parenthèse que le strict minimum, pour
* respected les priorités.
* @public
**/
function write ( $strictParenthesis = TRUE )
{
print (FALSE!==($str=$this->toString($strictParenthesis)) ? $str : '');
}
/**
* Affichage de la proposition
* On ajoute un saut de ligne après l'affichage.
*
* @type void
* @param bool strictParenthesis si ce paramètre est à TRUE, on applique le parenthésage
* strict, c'est-à-dire que si une opérande est une formule utilisant un opérateur
* différent, on le parenthèse. Sinon on ne parenthèse que le strict minimum, pour
* respected les priorités.
* @public
**/
function writeLn ( $strictParenthesis = TRUE )
{
$this->write($strictParenthesis);
print ("\n");
}
/**
* "Nettoie" la proposition des éléments trivialement simplifiables.
*
* La proposition sera modifiées par des opérations triviales:
* <ul>
* <li><b style="color:red">A | 1</b> deviendra <b style="color:green">1</b></li>
* <li><b style="color:red">A | 0</b> deviendra <b style="color:green">A</b></li>
* <li><b style="color:red">A | A</b> deviendra <b style="color:green">A</b></li>
* <li><b style="color:red">A & 1</b> deviendra <b style="color:green">A</b></li>
* <li><b style="color:red">A & 0</b> deviendra <b style="color:green">0</b></li>
* <li><b style="color:red">A & A</b> deviendra <b style="color:green">A</b></li>
* <li><b style="color:red">A | !A</b> deviendra <b style="color:green">1</b></li>
* <li><b style="color:red">A & !A</b> deviendra <b style="color:green">0</b></li>
* <li><b style="color:red">!(A | B)</b> deviendra <b style="color:green">!A & !B</b></li>
* <li><b style="color:red">!(A & B)</b> deviendra <b style="color:green">!A | !B</b></li>
* <li><b style="color:red">!!A</b> deviendra <b style="color:green">A</b></li>
* </ul>
* <i>A et B représentent des propositions logiques quelconques</i>
* <b>Pour les opérateur symetriques, les transformations symetriques non explicitées
* ici sont effectuées (par exemple 1|A devient 1) !</b>
*
* Notez qu'en général un <i>clean</i> est toujours précédé automatiquement d'un <i>expand</i>.
*
* @type bool
* @return TRUE si le nettoyage a bien fonctionné, FALSE sinon.
* @public
**/
function clean ( )
{
if (NULL === $this->__clean) {
if (!$this->expand()) return FALSE;
$formula = $this->__formula;
if (FALSE !== $formula) $formula = $this->__clean ($formula);
if (FALSE !== $formula) $this->__setFormula ($formula);
$this->__clean = FALSE !== $formula;
}
return $this->__clean;
}
/**
* Vérifie que deux propositions sont strictement équivalentes.
*
* <b style="color:red">ATTENTION !!</b> on ne vérifie que l'équivalent "visuelle", aucun calcul
* n'est effectué !
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = new &FirstOrderLogicProp('!A & !B');
* $b = new &FirstOrderLogicProp('!(A | B)');
* var_dump($a->equals($b)); // affiche "bool(false)"
* $b->clean();
* var_dump($a->equals($b)); // affiche "bool(true)"
* </code>
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = new &FirstOrderLogicProp('A & B');
* $b = new &FirstOrderLogicProp('B & A)');
* var_dump($a->equals($b)); // affiche "bool(false)"
* </code>
*
* @public
**/
function equals ( $logicFormula )
{
return $this->toString() == $logicFormula->toString();
}
/**
* La proposition est-elle sous sa forme conjonctive ?
*
* La forme conjonctive d'une proposition est la réécriture d'une formule
* sous la forme A<sub>1</sub> & A<sub>2</sub> & ... & A<sub>n</sub>
* Où A<sub>i</sub> = K<sub>i<sub>1</sub></sub> | K<sub>i<sub>2</sub></sub> | ... | K<sub>i<sub>m</sub></sub>
* Où K<sub>i<sub>j</sub></sub> = <i>Variable</i> ou <i>! Variable</i>.
*
* Cette forme conjonctive permet entre autres d'appliquer les algorithmes de
* résolution les plus classiques.
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $formula = 'a <-> b';
* $p = &new FirstOrderLogicProp($formula);
* var_dump($p->isconjunctiveForm()); // affiche "bool(false)"
* $p->clean();
* $p->writeLn(); // affiche "((! A) | B) & ((! B) | A)"
* var_dump($p->isconjunctiveForm()); // affiche "bool(true)"
* </code>
*
* @public
* @type bool
* @return TRUE si la proposition est sous sa forme conjonctive, FALSE sinon.
**/
function isconjunctiveForm ( )
{
if (NULL === $this->__conjunctive) {
$this->__conjunctive = FALSE!==$this->__formula ? $this->__isconjunctiveForm($this->__formula) : FALSE;
}
return $this->__conjunctive;
}
/**
* La proposition est-elle sous sa forme disjonctive ?
*
* La forme disjonctive d'une proposition est la réécriture d'une formule
* sous la forme A<sub>1</sub> | A<sub>2</sub> | ... | A<sub>n</sub>
* Où A<sub>i</sub> = K<sub>i<sub>1</sub></sub> & K<sub>i<sub>2</sub></sub> & ... & K<sub>i<sub>m</sub></sub>
* Où K<sub>i<sub>j</sub></sub> = <i>Variable</i> ou <i>! Variable</i>.
*
* Cette forme conjonctive permet entre autres d'appliquer les algorithmes de
* résolution les plus classiques.
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $formula = 'a <!> b';
* $p = &new FirstOrderLogicProp($formula);
* var_dump($p->isDisjunctiveForm()); // affiche "bool(false)"
* $p->clean();
* $p->writeLn(); // affiche "((! A) & B) | ((! B) & A)"
* var_dump($p->isDisjunctiveForm()); // affiche "bool(true)"
* </code>
*
* @public
* @type bool
* @return TRUE si la proposition est sous sa forme disjonctive, FALSE sinon.
**/
function isDisjunctiveForm ( )
{
if (NULL === $this->__disjunctive) {
return FALSE!==$this->__formula ? $this->__isDisjunctiveForm($this->__formula) : FALSE;
}
return $this->__disjunctive;
}
/**
* La proposition est-elle un atome ?
*
* @type bool
* @return TRUE si la proposition est un atome (une variable, ou une constante
* booléenne), FALSE sinon (<b>ou si la proposition n'est pas définie !!</b>).
* @public
**/
function isAtomic ( )
{
if (NULL === $this->__atom) {
$this->__atom = FALSE!==$this->__formula ? $this->__isAtomic($this->__formula) : FALSE;
}
return $this->__atom;
}
/**
* Affecte une variable dans la proposition
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp ('(a & b)');
* // les deux types d'affectation
* $a->setVariable('a', '0'); // chaine
* $a->setVariable('b', $a->true_()); // objet
* $a->replaceWithValues();
* $a->write(); // affiche "(0 & 1)"
* $a->clean();
* $a->write(); // affiche "0"
* </code>
*
* @param string var le nom de la variable à définir
* @param mixed value une chaine de caractères représentant la proposition à
* affecter à a. Ou bien un objet FirstOrderLogicProp directement.
* @public
* @type void
**/
function setVariable ( $var , $value )
{
$this->__replace = NULL;
$var = strtoupper("$var");
if (is_object($value)) {
$this->__values[$var] = &$value->clone();
}
else {
$c = &$this->clone();
$c->parse($value);
$this->__values[$var] = &$c;
}
}
/**
* Définit une liste de valeurs pour les variables dans la proposition
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp ('(a & b)');
* // les deux types d'affectationss
* $values = array(
* 'a' => '0', // chaine
* 'b' => &FirstOrderLogicProp::true() // objet
* );
* $a->setValues($values);
* $a->replaceWithValues();
* $a->write(); // affiche "0 & 1"
* $a->clean();
* $a->write(); // affiche "0"
* </code>
*
* @param array values un tableau de la forme "VARIABLE" => "VALEUR" (même contraintes
* que <i>setVariable</i> pour la valeur).
* @public
* @type void
**/
function setValues ( $values )
{
foreach ($values as $var => $val) {
$this->setVariable($var, $val);
}
}
/**
* Affecte des variables dans la proposition
* La fonction prend en parametre un nombre pair d'argument: un nom de variable
* suivi d'une valeur (même contraintes que <i>setVariable</i> pour la valeur).
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp ('(a & b)');
* $a->setVariables('a', '0', 'b', &FirstOrderLogicProp::true());
* $a->replaceWithValues();
* $a->write(); // affiche "0 & 1"
* $a->clean();
* $a->write(); // affiche "0"
* </code>
*
* @public
* @type void
**/
function setVariables ( )
{
$args = func_get_args();
$count = count($args);
if ($count%2 != 0) {
trigger_error('setVariable expects an even number of arguments', E_USER_ERROR);
return FALSE;
}
else for ($i=0; $i<$count; $i+=2) {
$var = $args[$i];
$val = $args[$i+1];
$this->setVariable($var, $val);
}
}
/**
* Detruit l'affectation à une variable
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $p = &new FirstOrderLogicProp ('(a & b)');
* $p->setVariables('a', '0', 'b', &FirstOrderLogicProp::true());
* $q = &$p->replacedWithValues();
* $q->write(); // affiche "0 & 1"
* $p->unsetVariable('a');
* $q = &$p->replacedWithValues();
* $q->write(); // affiche "a & 1"
* </code>
*
* @param string var le nom de la variable
* @type void
* @public
**/
function unsetVariable ( $var )
{
$this->__values[strtoupper($var)] = NULL;
}
/**
* Detruit l'affectation de plusieurs variables
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $p = &new FirstOrderLogicProp ('(a & b)');
* $p->setVariables('a', '0', 'b', &FirstOrderLogicProp::true());
* $q = &$p->replacedWithValues();
* $q->write(); // affiche "0 & 1"
* $vars = array('a', 'b');
* $p->unsetVariables($vars);
* $q = &$p->replacedWithValues();
* $q->write(); // affiche "a & b"
* </code>
*
* @param string vars la liste des noms de variables
* @type void
* @public
**/
function unsetVariables ( $vars )
{
foreach ($vars as $var) $this->unsetVariable ($var);
}
/**
* Rend effectif les remplacements par les valeurs des variables dans la proposition
* courante
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $p = &new FirstOrderLogicProp('a & b');
* $p->setVariables('a', '0', 'b', '1');
* // le remplacement n'est pas effectif
* $p->write(); // affiche "a & b"
* $p->replaceWithValues();
* // le remplacement est maintenant effectif
* $p->write(); // affiche "0 & 1"
* $p->setVariable('a', '1');
* $p->replaceWithValues();
* // inutile et sans effet ! la variable 'a' a déja
* // été remplacée et n'existe donc plus dans la proposition
* $p->write(); // affiche "0 & 1"
* </code>
*
* @type void
* @public
**/
function replaceWithValues ( )
{
if (NULL === $this->__replace) {
$formula = $this->__formula;
$this->__replaceWithVariables($formula);
$this->__setFormula($formula);
$this->__replace = TRUE;
}
}
/**
* Retourne une proposition identique à la proposition courante, mais avec les
* remplacements par les valeurs des variables rendus effectifs.
* Cette méthode permet de calculer les remplacements sans pour autant detruire
* la proposition initiale.
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $p = &new FirstOrderLogicProp('a & b');
* $p->setVariables('a', '0', 'b', '1');
* $q = $p->replacedWithValues();
* $p->write(); // affiche "a & b"
* $q->write(); // affiche "0 & 1"
* </code>
*
* @type void
* @public
**/
function replacedWithValues ( )
{
$save = $this->__formula;
$this->replaceWithValues();
$a = &$this->clone();
$this->__formula = $save; // ici on n'appelle pas __setFormula car il
// n'y a pas de réel changement à consigner
return $a;
}
/**
* Clone l'objet
*
* @type FirstOrderLogicProp
* @return un objet identique
* @public
**/
function clone ( )
{
$a = &new FirstOrderLogicProp;
$vars = get_class_vars(get_class($a));
foreach ($vars as $var => $val) {
$a->$var = $this->$var;
}
return $a;
}
/**
* Détruit l'objet
* Appelez cette méthode avant unset sur l'objet pour être sûr que la mémoire
* est bien totalement libérée (ceci n'est utile que dans des versions de php
* inférieure ou égale à 3 théoriquement).s
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = &new FirstOrderLogicProp('a & b | !a');
* $a->write(); // affiche "(a & b) | (! a)"
* var_dump($a); // affiche... beaucoup de choses ;)
* $a->destroy();
* var_dump($a); // affiche "object(firstorderlogicprop)(0) { }"
* unset($a);
* </code>
*
* @type void
* @public
**/
function destroy ( )
{
$vars = get_class_vars(get_class($this));
foreach ($vars as $var => $tmp) {
unset(${'this->'.$var});
}
}
/**
* Liste des variables dans la proposition
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $a = new FirstOrderLogicProp('a & b');
* echo join(', ', $a->variables()); // affiche "A, B"
* </code>
*
* @public
* @type array
* @return la liste des variables dans la proposition
**/
function variables ( )
{
if (NULL === $this->__vars) {
$this->__vars = $this->__variables($this->__formula);
}
return $this->__vars;
}
/**
* Retourne la table des valeurs de la proposition, selon les valeurs de ses
* variables.
* Le retour est un tableau de la forme:
* 'vars' => la liste des variables de la proposition
* 'values' => la liste des valeurs
*
* une valeur est un tableau de la forme:
* 'values' => la liste des affectations
* 'result' => la formule (VRAI ou FAUX) résultat des affectations
*
* une affectation est un couple VARIABLE => VALEUR (VRAI ou FAUX)
*
* @public
* @type array
* @return la table des valeurs
**/
function valuesTable ( )
{
if (NULL === $this->__table) {
$vars = $this->variables();
$res = array(
'vars' => $vars,
'values' => array()
);
$t = &$this->clone();
$t->clean();
$true = &$this->true_();
$false = &$this->false_();
$count = count($vars);
$n = pow(2, $count);
$index = array();
$k = 1;
for ($i=0; $i<$count; ++$i) { $index[$vars[$i]] = $k; $k *= 2; }
$values = array();
for ($i=0; $i<$n; ++$i) {
foreach ($index as $var => $x) $values[$var] = ($i&$x)==$x ? $true->toString() : $false->toString();
$t->setValues($values);
$p = &$t->replacedWithValues();
$p->clean();
$res['values'][] = array(
'values' => $values,
'result' => $p->toString()//equals($true)
);
$p->destroy();
unset($p);
}
$t->destroy();
unset($t);
$this->__table = $res;
}
return $this->__table;
}
/**
* Retourne la proposition correspondant au booléen passée en paramètre.
*
* @type FirstOrderLogicProp
* @public
**/
function fromBoolean ( $bool )
{
$formula = $bool ? $this->__printSyntax[VAL_TRUE] : $this->__printSyntax[VAL_FALSE];
$obj = &new FirstOrderLogicProp($formula);
return $obj;
}
/**
* Retourne la proposition correspondant au booléen VRAI
*
* @type FirstOrderLogicProp
* @public
**/
function true_ ( )
{
return $this->fromBoolean(TRUE);
}
/**
* Retourne la proposition correspondant au booléen FAUX
*
* @type FirstOrderLogicProp
* @public
**/
function false_ ( )
{
return $this->fromBoolean(FALSE);
}
/**
* Met la proposition sous sa forme disjonctive (cf. <i>isDisjunctiveForm</i>).
*
* @type bool
* @public
**/
function disjunctiveForm ( )
{
if (NULL === $this->__disjunctive) {
$res = $this->clean();
if ($res) $this->__setFormula($this->__disjunctiveForm($this->__formula));
$this->__disjunctive = $res;
}
return $this->__disjunctive;
}
/**
* Met la proposition sous sa forme conjonctive (cf. <i>isconjunctiveForm</i>).
*
* @type bool
* @public
**/
function conjunctiveForm ( )
{
if (NULL === $this->__conjunctive) {
$this->__conjunctive = $this->not_()
&& $this->disjunctiveForm()
&& $this->not_()
&& $this->clean();
}
return $this->__conjunctive;
}
/**
* Récupérer l'opérateur de la proposition.
* Si la proposition est atomique, on renvoie FALSE !
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $p = new FirstOrderLogicProp('A & B | C');
* echo $p->operator(); // affiche la valeur de OP_OR
* </code>
*
* @type int
* @return l'opérateur de la proposition
* @public
**/
function operator ()
{
return $this->isAtomic() ? FALSE : $this->__formula['op'];
}
/**
* Récupérer l'opérande gauche de la proposition.
* Si la propostion est atomique, on renvoie FALSE !
* Si l'opérateur est NOT, alors on renvoie FALSE !
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $p = new FirstOrderLogicProp('A & B | C');
* $q = $p->leftOperand();
* $q->write(); // affiche "A & B"
* </code>
*
* @type int
* @return l'opérateur de la proposition
* @public
**/
function leftOperand ()
{
if ($this->isAtomic() || $this->__formula['op']==OP_NOT) {
return FALSE;
}
else {
$p = &$this->clone();
$p->parse($this->__toString($this->__formula[0]));
return $p;
}
}
/**
* Récupérer l'opérande gauche de la proposition.
* Si la propostion est atomique, on renvoie FALSE !
* Si l'opérateur est NOT, alors on renvoie FALSE !
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $p = new FirstOrderLogicProp('A & B | C');
* $q = $p->rightOperand();
* $q->write(); // affiche "C"
* </code>
*
* @type int
* @return l'opérateur de la proposition
* @public
**/
function rightOperand ()
{
if ($this->isAtomic()) {
return FALSE;
}
else {
$p = &$this->clone();
$p->parse($this->__toString($this->__formula[1]));
return $p;
}
}
/**
* Récupérer la valeur atomique de la proposition
* Si la propostion n'est pas atomique, on renvoie FALSE !
*
* Les valeurs retournées peuvent être:
* - la constante VAL_TRUE
* - la constante VAL_FALSE
* - une chaine de caractere (variable atomique)
*
* <b style="color:red">ATTENTION !!</b> dans un cas d'erreur il ne faut pas tester
* directement la valeur de retour, mais la comparer STRICTEMENT avec FALSE (opérateur
* ===).
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* $p = new FirstOrderLogicProp('0');
* $v = $p->atomicValue(); // VAL_FALSE
* if ($v) { echo 'la valeur n'est pas atomique !'; }
* else { echo 'la valeur est: '.$v; }
* </code>
* affiche "la valeur n'est pas atomique !" car VAL_FALSE vaut 0, et 0 est égal (non
* strict) à FALSE.
* Il faut plutot faire le test suivant:
* <code style="color:darkgreen">
* $p = new FirstOrderLogicProp('0');
* $v = $p->atomicValue(); // VAL_FALSE
* if (FALSE!==$v) { echo 'la valeur n'est pas atomique !'; }
* else { echo 'la valeur est: '.$v; }
* </code>
* affiche "la valeur est: 0".
*
* @type int
* @return l'opérateur de la proposition
* @public
**/
function atomicValue ()
{
if ($this->isAtomic()) {
return $this->__formula;
}
else {
return FALSE;
}
}
//-----------------------
// private attributes
//-----------------------
/**
*
* @private
**/
var $__syntax = Array();
/**
*
* @private
**/
var $__formula = NULL;
/**
*
* @private
**/
var $__PCRE_vars = '';
/**
*
* @private
**/
var $__PCRE_bin_ops = '';
/**
*
* @private
**/
var $__PCRE_un_ops = '';
/**
*
* @private
**/
var $__printSyntax = Array();
/**
*
* @private
**/
var $__values = Array();
/**
*
* @private
**/
var $__replace = NULL;
/**
*
* @private
**/
var $__expand = NULL;
/**
*
* @private
**/
var $__clean = NULL;
/**
*
* @private
**/
var $__toStringStrict = NULL;
/**
*
* @private
**/
var $__toString = NULL;
/**
*
* @private
**/
var $__disjunctive = NULL;
/**
*
* @private
**/
var $__conjunctive = NULL;
/**
*
* @private
**/
var $__atom = NULL;
/**
*
* @private
**/
var $__vars = NULL;
/**
*
* @private
**/
var $__table = NULL;
//-----------------------
// private functions
//-----------------------
/**
*
* @private
**/
function __setFormula ( $formula )
{
$this->__formula = $formula;
$this->__expand = NULL;
$this->__clean = NULL;
$this->__toStringStrict = NULL;
$this->__toString = NULL;
$this->__disjunctive = NULL;
$this->__conjunctive = NULL;
$this->__atom = NULL;
$this->__vars = NULL;
$this->__table = NULL;
$this->__replace = NULL;
}
/**
*
* @private
**/
function __parse ( $formula )
{
$len = strlen($formula);
$tokens = $this->__tokens ($formula);
return $this->__parseTokens ($tokens);
}
/**
*
* @private
**/
function __orderSyntax ( $syntax )
{
$vals = array();
$res = array();
$max = 0;
foreach ($syntax as $x) {
$len = strlen("$x");
$vals[$len][] = $x;
if ($max<$len) $max = $len;
}
for ($i=$max; $i>=0; --$i) {
if (isset($vals[$i])) {
foreach ($vals[$i] as $x) $res[] = $x;
}
}
return $res;
}
/**
*
* @private
**/
function __tokens ( $formula )
{
// PCRE masks for parsing
$PCRE_uops = $this->__orderSyntax($this->__PCRE_un_ops);
$PCRE_bops = $this->__orderSyntax($this->__PCRE_bin_ops);
$PCRE_vars = $this->__orderSyntax($this->__PCRE_vars);
$uops = '(?:'; foreach ($PCRE_uops as $x) $uops .= preg_quote($x,'/').')|(?:'; $uops = substr($uops, 0, -4);
$bops = '(?:'; foreach ($PCRE_bops as $x) $bops .= preg_quote($x,'/').')|(?:'; $bops = substr($bops, 0, -4);
$vars = '(?:'; foreach ($PCRE_vars as $x) $vars .= preg_quote($x,'/').')|(?:'; $vars .= $this->PCRE_variable.')';
$PCRE_uops = '/'.$uops.'/Ai';
$PCRE_bops = '/'.$bops.'/Ai';
$PCRE_vars = '/'.$vars.'/Ai';
// starting parsing
$tok = array();
$formula = trim($formula);
while ($formula != '') {
$unary = (bool) preg_match ($PCRE_uops, $formula, $m);
$binary = $unary ? FALSE : (bool) preg_match ($PCRE_bops, $formula, $m);
$variable = $unary || $binary ? FALSE : (bool) preg_match ($PCRE_vars, $formula, $m);
if ($unary || $binary || $variable) {
$token = strtoupper($m[0]);
$formula = substr ($formula, strlen($token));
$tok[] = isset($this->__syntax[$token]) ? $this->__syntax[$token] : $token;
}
elseif ($formula{0}=='(' || $formula{0}==')') {
$tok[] = $formula{0}=='(' ? PARO : PARC;
$formula = substr ($formula, 1);
}
else {
return FALSE;
}
$formula = ltrim($formula);
$token = '';
}
return $tok;
}
/**
*
* @private
**/
function __parseTokens ( $tokens )
{
$tokens = $this->__groupTokens ($tokens);
if (FALSE === $tokens) return FALSE;
$size = sizeof($tokens);
if ($size == 1 && is_array($tokens[0])) {
return $this->__parseTokens($tokens[0]);
}
// a-t-on une simple variable ou constante ?
if ($size == 1 && $this->__isAtomic($tokens[0])) {
return $tokens[0];
}
// trouver l'opérateur le moins prioritaire présent dans tokens
$index = -1;
$op = OP_MIN;
$size = sizeof($tokens);
for ($i=0; $i<$size; ++$i) {
if (is_int($tokens[$i]) && ($tokens[$i]>$op || $index==-1)) {
$op = $tokens[$i];
$index = $i;
}
}
if ($index == -1) {
trigger_error('Operator expected !', E_USER_WARNING);
return FALSE;
}
if ($op == OP_NOT) { // unary
if ($index != 0) {
trigger_error('Unexpected NOT operator', E_USER_WARNING);
return FALSE;
}
$debut = NULL;
array_shift($tokens);
$fin = $this->__parseTokens($tokens);
}
else { // binary
$debut = array();
$fin = $tokens;
for ($i=0; $i<$index; ++$i, $debut[] = array_shift($fin));
array_shift($fin);
$debut = $this->__parseTokens($debut);
$fin = $this->__parseTokens($fin);
}
return $this->__expression ($op, $debut, $fin);
}
/**
*
* @private
**/
function __groupTokens ( $tokens )
{
$res = array();
$len = sizeof($tokens);
for ($i=0; $i<$len; ++$i) {
$tok = $tokens[$i];
if ($tok == PARO) {
$group = array();
$open = 1;
while ($i<$len-1 && $open>0) {
$tok = $tokens[++$i];
if ($tok==PARO) ++$open;
elseif ($tok==PARC) --$open;
$group[] = $tok;
if ($open<0) {
trigger_error('unmatching right parenthesis', E_USER_WARNING);
return FALSE;
}
}
if ($open>0) {
trigger_error('unmatched left parenthesis', E_USER_WARNING);
return FALSE;
}
else {
array_pop($group);
// no recursive call here: we do it in __parseTokens
$tok = $group; // $this->__groupTokens($group);
}
}
$res[] = $tok;
}
return $res;
}
/**
*
* @private
**/
function __expression ( $op , $left , $right )
{
return Array (
'op' => $op,
0 => $left,
1 => $right
);
}
/**
*
* @private
**/
function __expand ( $formula )
{
if ($formula === NULL || $this->__isAtomic($formula)) // variable
return $formula;
// A IMPLIES B = NOT A OR B
// A IMPLIED B = NOT B OR A
// A NOT_IMPLIES B = NOT ( A IMPLIES B )
// A NOT_IMPLIED B = NOT ( A IMPLIED B )
// A IFF B = ( A IMPLIES B ) AND ( A IMPLIED B )
// A NOR B = NOT ( A OR B )
// A NAND B = NOT ( A AND B )
// A XOR B = NOT ( A IFF B)
$op = $formula['op'];
$left = $formula[0];
$right = $formula[1];
switch ($op) {
case OP_IMPLIES:
$op = OP_OR;
$left = $this->__expression(OP_NOT, NULL, $left);
break;
case OP_IMPLIED:
$op = OP_OR;
$l = $this->__expression(OP_NOT, NULL, $right);
$right = $left;
$left = $l;
break;
case OP_NOT_IMPLIES:
$op = OP_NOT;
$right = $this->__expression(OP_IMPLIES, $left, $right);
$left = NULL;
break;
case OP_NOT_IMPLIED:
$op = OP_NOT;
$right = $this->__expression(OP_IMPLIED, $left, $right);
$left = NULL;
break;
case OP_NOR:
$op = OP_NOT;
$right = $this->__expression(OP_OR, $left, $right);
$left = NULL;
break;
case OP_NAND:
$op = OP_NOT;
$right = $this->__expression(OP_AND, $left, $right);
$left = NULL;
break;
case OP_IFF:
$op = OP_AND;
$l = $this->__expression(OP_IMPLIES, $left, $right);
$right = $this->__expression(OP_IMPLIED, $left, $right);
$left = $l;
break;
case OP_XOR:
$op = OP_NOT;
$right = $this->__expression(OP_IFF, $left, $right);
$left = NULL;
break;
}
return $this->__expression($op, $this->__expand($left), $this->__expand($right));
}
/**
*
* @private
**/
function __toString ( $formula , $strictPar = TRUE )
{
if ($formula === NULL) {
return '';
}
elseif (is_string($formula)) {
return $formula;
}
elseif ($formula === VAL_TRUE || $formula === VAL_FALSE) {
return $this->__printSyntax[$formula];
}
else {
$o = $this->__printSyntax[$op = $formula['op']] . ' ';
if ($op!=OP_NOT) $o = ' '.$o;
$l = $this->__toString($left = $formula[0], $strictPar);
$r = $this->__toString($right = $formula[1], $strictPar);
if (!$this->__isAtomic($left) && isset($left['op']) && (($left['op']!=$op && $strictPar) || ($left['op']>$op))) $l = '(' . $l . ')';
if (!$this->__isAtomic($right) && isset($right['op']) && (($right['op']!=$op && $strictPar) || ($right['op']>$op))) $r = '(' . $r . ')';
return $l . $o . $r;
}
}
/**
*
* @private
**/
function __clean ( $formula )
{
// A OR 1 = 1
// A OR 0 = A
// A OR A = A
// A AND A = A
// A AND 1 = A
// A AND 0 = 0
// A OR NOT A = 1
// A AND NOT A = 0
// NOT ( A AND B ) = NOT A OR NOT B
// NOT ( A OR B ) = NOT A AND NOT B
// NOT NOT A = A
if ($formula === NULL || $this->__isAtomic($formula))
return $formula;
else {
$op = $formula['op'];
$left = $this->__clean($formula[0]);
$right = $this->__clean($formula[1]);
if ($op == OP_OR) {
if ($left === VAL_TRUE) return VAL_TRUE;
elseif ($right === VAL_TRUE) return VAL_TRUE;
elseif ($left === VAL_FALSE) return $right;
elseif ($right === VAL_FALSE) return $left;
else {
$l = $this->__toString($left);
$r = $this->__toString($right);
if ($l==$r) return $left;
elseif (
(isset($left['op']) && $left['op']==OP_NOT && $this->__toString($left[1])==$r)
||
(isset($right['op']) && $right['op']==OP_NOT && $this->__toString($right[1])==$l)
)
return VAL_TRUE;
}
}
elseif ($op == OP_AND) {
if ($left === VAL_TRUE) return $right;
elseif ($right === VAL_TRUE) return $left;
elseif ($left === VAL_FALSE) return VAL_FALSE;
elseif ($right === VAL_FALSE) return VAL_TRUE;
else {
$l = $this->__toString($left);
$r = $this->__toString($right);
if ($l==$r) return $left;
elseif (
(isset($left['op']) && $left['op']==OP_NOT && $this->__toString($left[1])==$r)
||
(isset($right['op']) && $right['op']==OP_NOT && $this->__toString($right[1])==$l)
)
return VAL_FALSE;
}
}
elseif ($op == OP_NOT) {
if ($right === VAL_TRUE) return VAL_FALSE;
elseif ($right === VAL_FALSE) return VAL_TRUE;
elseif (isset($right['op']) && ($right['op']==OP_OR || $right['op']==OP_AND)) {
$l = $this->__expression(OP_NOT, NULL, $right[0]);
$r = $this->__expression(OP_NOT, NULL, $right[1]);
return $this->__clean($this->__expression($right['op']==OP_AND ? OP_OR : OP_AND, $l, $r));
}
elseif (isset($right['op']) && $right['op']==OP_NOT) {
return $right[1];
}
}
return $this->__expression($op, $left, $right);
}
}
/**
*
* @private
**/
function __isAtomic ( $formula )
{
return is_string($formula) || $formula===VAL_TRUE || $formula===VAL_FALSE;
}
/**
*
* @private
**/
function __isconjunctiveForm ( $formula )
{
if ($this->__isconjunctiveAtom($formula)) {
return TRUE;
}
else {
return $formula['op']==OP_AND
&& $this->__isconjunctiveForm($formula[0])
&& $this->__isconjunctiveForm($formula[1]);
}
}
/**
*
* @private
**/
function __isDisjunctiveForm ( $formula )
{
if ($this->__isDisjunctiveAtom($formula)) {
return TRUE;
}
else {
return $formula['op']==OP_OR
&& $this->__isDisjunctiveForm($formula[0])
&& $this->__isDisjunctiveForm($formula[1]);
}
}
/**
*
* @private
**/
function __isconjunctiveAtom ( $formula )
{
return $this->__isAtomic($formula)
|| ($formula['op']==OP_NOT && $this->__isAtomic($formula[1]))
|| ($formula['op']==OP_OR && $this->__isconjunctiveAtom($formula[0]) && $this->__isconjunctiveAtom($formula[1]));
}
/**
*
* @private
**/
function __isDisjunctiveAtom ( $formula )
{
return $this->__isAtomic($formula)
|| ($formula['op']==OP_NOT && $this->__isAtomic($formula[1]))
|| ($formula['op']==OP_AND && $this->__isDisjunctiveAtom($formula[0]) && $this->__isDisjunctiveAtom($formula[1]));
}
/**
*
* @private
**/
function __replaceWithVariables ( &$formula )
{
if (is_string($formula)) {
if (isset($this->__values[$formula])) $formula = $this->__values[$formula]->__formula;
}
elseif (isset($formula['op'])) {
$this->__replaceWithVariables($formula[0]);
$this->__replaceWithVariables($formula[1]);
}
}
/**
*
* @private
**/
function __variables ($formula)
{
if (is_string($formula)) {
return array(strtoupper($formula));
}
elseif (isset($formula['op'])) {
$a = array_unique(array_merge($this->__variables($formula[0]), $this->__variables($formula[1])));
sort($a);
return $a;
}
return array();
}
/**
*
* @private
**/
function __disjunctiveForm ( $formula )
{
$formula = $this->__clean($formula);
if (is_array($formula) && isset($formula['op'])) {
$op = $formula['op'];
$left = $this->__disjunctiveForm($formula[0]);
$right = $this->__disjunctiveForm($formula[1]);
if ($op==OP_AND && is_array($left) && isset($left['op']) && $left['op']==OP_OR) {
// (left1 OR left2) AND right == (left1 AND right) OR (left2 AND right) == l1 OR l2
$l1 = $this->__expression(OP_AND, $left[0], $right);
$l2 = $this->__expression(OP_AND, $left[1], $right);
$op = OP_OR;
$left = $l1;
$right = $l2;
}
elseif ($op==OP_AND && is_array($right) && isset($right['op']) && $right['op']==OP_OR) {
// left AND (right1 OR right2) == (left AND right1) OR (left AND right2) == r1 OR r2
$r1 = $this->__expression(OP_AND, $left, $right[0]);
$r2 = $this->__expression(OP_AND, $left, $right[1]);
$op = OP_OR;
$left = $r1;
$right = $r2;
}
//$formula = $this->__disjunctiveForm($this->__expression($op, $left, $right));
$formula = $this->__expression($op, $this->__disjunctiveForm($left), $this->__disjunctiveForm($right));
}
return $formula;
}
}
/**
* Permet la vérification de formules.
* cf. <i>check()</i>
*
* $lang FR
*
* @author hide@address.com
* @version 1.0
* @date 2003-10-04
**/
class FOLPChecker extends FirstOrderLogicProp
{
/**
* Attribut en lecture seule
*
* Après un appel à check, cet attribut vaut TRUE si la proposition est un theroeme
* et FALSE sinon. Dans le cas FALSE, l'attribut <i>counterexample</i> reprend les
* affectations de variables qui ont permis d'arriver à la conclusion (le contre-
* exemple).
*
* Si <i>check()</i> n'a pas encore été appelée, l'attribut vaut NULL
*
* @type bool
* @public
**/
var $theorem = NULL;
/**
* Attribut en lecture seule
*
* Après un appel à check, cet attribut vaut NULL s'il n'y a aucun contre-exemple
* trouvé à la proposition (c'est un theoreme). Sinon il indique une des affectations
* permettant de rendre fausse la proposition.
*
* Cet attribut est alors un tableau de couples ( VARIABLE , VALEUR ). VARIABLE est une
* chaine de caracteres (le nom de la variable) et VALEUR est un objet FirstOrderLogicProp
* (<i>true_()</i> ou <i>false_()</i>)
*
* @type bool
* @public
**/
var $counterexample = NULL;
/**
* Effectue la vérifications de la proposition logique.
* L'algorithme utilisé est l'algorithme classique:
* - mise sous forme disjonctive de la négation de la formule
* - recherche d'une opérande conjonctive vraie (qui rendrait donc toute la négation vraie)
* - si on a trouvé une opérande vraie: l'affectation qui y a conduit est un contre-exemple
* - sinon la proposition est un théorème
*
* <u>Exemple</u>:
* <code style="color:darkgreen">
* function checkFormula ( $formula )
* {
* $p = &new FOLPChecker($formula);
* echo 'checking <b>'.htmlentities($formula).'</b>...<br>';
* $p->check();
* if ($p->theorem) {
* echo 'This is a theorem !';
* }
* else {
* echo 'This is not a theorem. Here is a counterexample:<br>';
* echo 'If you affect ';
* foreach ($p->counterexample as $aff) {
* $var = $aff[0];
* $val = $aff[1]->toString();
* echo $val.' to "'.$var.'", ';
* }
* echo 'then the proposition becomes false.';
* }
* }
*
* checkFormula ( '((a->b)&(b->c)) -> (a->c)'); // it's a theorem
* </code>
*
* @public
**/
function check ( )
{
$p = &$this->clone();
$p->not_();
$p->disjunctiveForm();
$this->theorem = TRUE;
$this->__findDisjunctiveOperandsUntilTrue($p);
}
/**
*
* @private
**/
function __findDisjunctiveOperandsUntilTrue( $p )
{
if (FALSE === $this->theorem) return;
if ($p->isAtomic()) {
$val = $p->atomicValue();
if ($val===VAL_FALSE || $val===VAL_TRUE) {
return NULL;
}
else return array(array($val, $p->true_()));
}
else {
if ($p->operator() == OP_OR) {
$l = &$p->leftOperand();
$r = &$p->rightOperand();
$left = $this->__findDisjunctiveOperandsUntilTrue($l);
$right = $this->__findDisjunctiveOperandsUntilTrue($r);
if ($l->isAtomic() || $l->operator()==OP_AND) $left = array($left);
if ($r->isAtomic() || $r->operator()==OP_AND) $right = array($right);
if ($left!==NULL) foreach ($left as $l) if ($l!==NULL && !$this->__contradiction($l)) { $this->theorem = FALSE; $this->counterexample = $l; return; }
if ($right!==NULL) foreach ($right as $r) if ($r!==NULL && !$this->__contradiction($r)) { $this->theorem = FALSE; $this->counterexample = $r; return; }
return array_merge($left, $right);
}
elseif ($p->operator() == OP_NOT) {
$var = &$p->rightOperand();
$var = $var->atomicValue();
return array(array($var, $p->false_()));
}
elseif ($p->operator() == OP_AND) {
$left = $this->__findDisjunctiveOperandsUntilTrue($p->leftOperand());
$right = $this->__findDisjunctiveOperandsUntilTrue($p->rightOperand());
return array_merge($left, $right);
}
else die('woooops');
}
}
/**
*
* @private
**/
function __contradiction ( $affect )
{
$values = array();
foreach ($affect as $aff) if (is_array($aff)) {
$var = $aff[0];
$val = $aff[1];
if (isset($values[$var]) && $values[$var]!=$val) return TRUE;
$values[$var] = $val;
}
return FALSE;
}
}
?>