PHP code example of d3lph1 / boollet

    
        
<?php
require_once('vendor/autoload.php');

/* Start to develop here. Best regards https://php-download.com/ */

    

d3lph1 / boollet example snippets

use D3lph1\Boollet\Structure\Expression\{Variable, UnaryExpression, BinaryExpression};
use D3lph1\Boollet\Structure\Operator\{UnaryOperators, BinaryOperators};

$expr = new BinaryExpression(
    new UnaryExpression(UnaryOperators::NOT, new Variable(false)),
    BinaryOperators::AND,
    new BinaryExpression(new Variable(true), BinaryOperators::OR, new Variable(false, label: 'Z'))
);

echo $expr; // (!A ⋀ (B ⋁ Z))

$val = $expr->evaluate(); // true

$val = $expr->evaluate(['A' => true, 'B' => true, 'Z' => true]) // false

use D3lph1\Boollet\ValueBinder;

$a = new Variable(false);
$b = new Variable(true);
$z = new Variable(false, label: 'Z');

$expr = new BinaryExpression(
    new UnaryExpression(UnaryOperators::NOT, $a),
    BinaryOperators::AND,
    new BinaryExpression($b, BinaryOperators::OR, $z)
);

$binder = new ValueBinder();
$binder->bind($a);
$binder->bindAll([$b, $z]);

$binder->set([
    'A' => true,
    'B' => true,
    'Z' => true
])

$expr->evaluate(); // true

use D3lph1\Boollet\Parser\{Lexer, Reader\StringInputReader, ShuntingYardParser};

$lexer = Lexer::default();
$input = new StringInputReader('X ⊕ Y → (X ⋀ Z)');
$parser = new ShuntingYardParser($lexer);

$expr = $parser->parse($input);

echo $expr; // ((X ⊕ Y) → (X ⋀ Z))

use D3lph1\Boollet\TruthTable;

$table = TruthTable::tabulate($expr);
$table->setLabel('f(X ⊕ Y → (X ⋀ Z))');

echo $table;

use D3lph1\Boollet\NormalForm\NormalForms;

// $expr ~ ((X ⊕ Y) → (X ⋀ Z))

$ccnf = NormalForms::calculateCompleteConjunctive($expr); // ((X ⋁ (!Y ⋁ Z)) ⋀ ((X ⋁ (!Y ⋁ !Z)) ⋀ (!X ⋁ (Y ⋁ Z))))
$cdnf = NormalForms::calculateCompleteDisjunctive($expr); // ((!X ⋀ (!Y ⋀ !Z)) ⋁ ((!X ⋀ (!Y ⋀ Z)) ⋁ ((X ⋀ (!Y ⋀ Z)) ⋁ ((X ⋀ (Y ⋀ !Z)) ⋁ (X ⋀ (Y ⋀ Z))))))

use \D3lph1\Boollet\ZhegalkinPolynomial;

// $expr ~ (!X → ((!Y ⊕ X) ⋀ !Z))

$polynomial = ZhegalkinPolynomial::calculate($expr);

echo $polynomial; // ((Z ⋀ (Y ⋀ X)) ⊕ ((Y ⋀ X) ⊕ ((Z ⋀ X) ⊕ ((Z ⋀ Y) ⊕ (Y ⊕ (Z ⊕ 1))))))

use \D3lph1\Boollet\SAT\CompleteDisjunctiveNormalFormSATSolver;
// $expr ~ X ⋁ (Y ⋀ Z)

$y->set(false);

$cdnf = NormalForms::calculateCompleteDisjunctive($expr);

$sat = new CompleteDisjunctiveNormalFormSATSolver();
$solutions = $sat->findAllPossibleSolutions($cdnf, ['X', 'Z']);
$solutions = $sat->findAllPossibleSolutions($cdnf, ['X', 'Z']);

^ array:2 [▼
  0 => array:2 [▼
    "X" => true
    "Z" => false
  ]
  1 => array:2 [▼
    "X" => true
    "Z" => true
  ]
]

use D3lph1\Boollet\Constraints\Constraints;

$solutions = $sat->findAllPossibleSolutionsWithConstraints($cdnf, ['X', 'Z'], new class() implements Constraints {
    public function isSatisfy(array $values): bool
    {
        return $values['X'];
    }
});

^ array:1 [▼
  0 => array:2 [▼
    "X" => true
    "Z" => false
  ]
]