v1.4

CHANGELOG.md

@@ -4,6 +4,14 @@ All notable changes to this project will be documented in this file.
 The format is based on [Keep a Changelog](http://keepachangelog.com/en/1.0.0/)
 and this project adheres to [Semantic Versioning](http://semver.org/spec/v2.0.0.html).
 
+## v1.4.0 - 2023-11-20
+### Added
+- `get_conjuncts(p: HplPredicate | HplExpression)` function to `hpl.rewrite` module.
+- `get_disjuncts(p: HplPredicate | HplExpression)` function to `hpl.rewrite` module.
+
+### Changed
+- Small improvement in `hpl.rewrite.simplify`.
+
 ## v1.3.0 - 2023-10-04
 ### Added
 - `split_and(p: HplPredicate | HplExpression)` function to `hpl.rewrite` module.

src/hpl/rewrite.py

@@ -127,6 +127,42 @@ def simplify(predicate_or_expression: P) -> P:
     return _simplify(predicate_or_expression)
 
 
+@typechecked
+def get_conjuncts(predicate_or_expression: P) -> List[HplExpression]:
+    if predicate_or_expression.is_predicate:
+        assert isinstance(predicate_or_expression, HplPredicate)
+        predicate_or_expression = predicate_or_expression.condition
+    assert isinstance(predicate_or_expression, HplExpression)
+    conjuncts: List[HplExpression] = []
+    stack = [predicate_or_expression]
+    while stack:
+        phi = stack.pop()
+        if isinstance(phi, HplBinaryOperator) and phi.operator.is_and:
+            stack.append(phi.operand1)
+            stack.append(phi.operand2)
+        else:
+            conjuncts.append(phi)
+    return conjuncts
+
+
+@typechecked
+def get_disjuncts(predicate_or_expression: P) -> List[HplExpression]:
+    if predicate_or_expression.is_predicate:
+        assert isinstance(predicate_or_expression, HplPredicate)
+        predicate_or_expression = predicate_or_expression.condition
+    assert isinstance(predicate_or_expression, HplExpression)
+    disjuncts: List[HplExpression] = []
+    stack = [predicate_or_expression]
+    while stack:
+        phi = stack.pop()
+        if isinstance(phi, HplBinaryOperator) and phi.operator.is_or:
+            stack.append(phi.operand1)
+            stack.append(phi.operand2)
+        else:
+            disjuncts.append(phi)
+    return disjuncts
+
+
 ###############################################################################
 # Formula Rewriting - Helper Functions
 ###############################################################################
@@ -611,6 +647,18 @@ def _simplify_conjunction(phi: HplBinaryOperator) -> HplExpression:
     # p & ~p == F
     if _obviously_different(p, q):
         return false()
+    # p & (q & p) == p & q
+    conjuncts = get_conjuncts(p)
+    conjuncts.extend(get_conjuncts(q))
+    unique = set(conjuncts)
+    if len(conjuncts) != len(unique):
+        if len(unique) == 1:
+            return conjuncts[0]
+        conjuncts = list(unique)
+        psi = And(conjuncts[0], conjuncts[1])
+        for i in range(2, len(conjuncts)):
+            psi = And(conjuncts[i], psi)
+        return psi
     return phi if p is phi.operand1 and q is phi.operand2 else And(p, q)
 
 
@@ -637,6 +685,18 @@ def _simplify_disjunction(phi: HplBinaryOperator) -> HplExpression:
     # p | ~p == T
     if _obviously_different(p, q):
         return true()
+    # p | (q | p) == p | q
+    disjuncts = get_disjuncts(p)
+    disjuncts.extend(get_disjuncts(q))
+    unique = set(disjuncts)
+    if len(disjuncts) != len(unique):
+        if len(unique) == 1:
+            return disjuncts[0]
+        disjuncts = list(unique)
+        psi = Or(disjuncts[0], disjuncts[1])
+        for i in range(2, len(disjuncts)):
+            psi = Or(disjuncts[i], psi)
+        return psi
     return phi if p is phi.operand1 and q is phi.operand2 else Or(p, q)
 
 

tests/test_logic_rewrite.py

@@ -5,10 +5,12 @@
 # Imports
 ###############################################################################
 
-from hpl.ast.expressions import HplBinaryOperator, HplExpression, HplFieldAccess, HplLiteral
+from hpl.ast.expressions import HplBinaryOperator, HplExpression
 from hpl.ast.predicates import HplContradiction, HplPredicate, HplPredicateExpression, HplVacuousTruth
 from hpl.parser import condition_parser, expression_parser
 from hpl.rewrite import (
+    get_conjuncts,
+    get_disjuncts,
     is_true,
     refactor_reference,
     replace_this_with_var,
@@ -277,6 +279,19 @@ def test_simplify_and():
     q = simplify(p)
     assert isinstance(q, HplPredicateExpression)
     assert q == a
+    p = parser.parse('a and (b and (c and a))')
+    q = simplify(p)
+    assert isinstance(q, HplPredicateExpression)
+    assert sorted([ref.field for ref in get_conjuncts(q.condition)]) == ['a', 'b', 'c']
+    x = q.condition
+    assert isinstance(x, HplBinaryOperator)
+    assert x.operator.is_and
+    assert not isinstance(x.operand1, HplBinaryOperator)
+    assert isinstance(x.operand2, HplBinaryOperator)
+    x = x.operand2
+    assert x.operator.is_and
+    assert not isinstance(x.operand1, HplBinaryOperator)
+    assert not isinstance(x.operand2, HplBinaryOperator)
 
 
 def test_simplify_or():
@@ -311,6 +326,19 @@ def test_simplify_or():
     q = simplify(p)
     assert isinstance(q, HplPredicateExpression)
     assert q == a
+    p = parser.parse('a or (b or (c or a))')
+    q = simplify(p)
+    assert isinstance(q, HplPredicateExpression)
+    x = q.condition
+    assert isinstance(x, HplBinaryOperator)
+    assert sorted([ref.field for ref in get_disjuncts(q.condition)]) == ['a', 'b', 'c']
+    assert x.operator.is_or
+    assert not isinstance(x.operand1, HplBinaryOperator)
+    assert isinstance(x.operand2, HplBinaryOperator)
+    x = x.operand2
+    assert x.operator.is_or
+    assert not isinstance(x.operand1, HplBinaryOperator)
+    assert not isinstance(x.operand2, HplBinaryOperator)
 
 
 def test_simplify_comparison():