Location: PHPKode > scripts > First Order Logic Prop > first-order-logic-prop/FirstOrderLogicProp.inc.php
<?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">&amp;</b></li>
*     <li><u>non et</u>: <b style="color:red">!&amp;</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">&lt;!&gt;</b></li>
*     <li><u>implication</u>: <b style="color:red">-&gt;</b></li>
*     <li><u>non implication</u>: <b style="color:red">-!&gt;</b></li>
*     <li><u>implication gauche</u>: <b style="color:red">&lt;-</b></li>
*     <li><u>non implication gauche</u>: <b style="color:red">&lt;!-</b></li>
*     <li><u>equivalence</u>: <b style="color:red">&lt;-&gt;</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 -&gt; B</b> deviendra <b style="color:green">(! A) | B</b></li>
    *     <li><b style="color:red">A &lt;- B</b> deviendra <b style="color:green">(! B) | A</b></li>
    *     <li><b style="color:red">A -!&gt; B</b> deviendra <b style="color:green">! (A -&gt; B)</b></li>
    *     <li><b style="color:red">A &lt;!- B</b> deviendra <b style="color:green">! (A &lt;- B)</b></li>
    *     <li><b style="color:red">A &lt;-&gt; B</b> deviendra <b style="color:green">(A -&gt; 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 &lt;!&gt; B</b> deviendra <b style="color:green">!(A &lt;-&gt; 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' =&gt; la liste des variables de la proposition
    * 'values' =&gt; la liste des valeurs
    *
    * une valeur est un tableau de la forme:
    * 'values' =&gt; la liste des affectations
    * 'result' =&gt; la formule (VRAI ou FAUX) résultat des affectations
    *
    * une affectation est un couple VARIABLE =&gt; 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;
    }



}







?>
Return current item: First Order Logic Prop