Module dev.civl.sarl
Package dev.civl.sarl.simplify.IF

Interface ContextPartition

public interface ContextPartition

Provides a partition of the set of conjunctive clauses of a BooleanExpression (the context) and a method to use that partition for context minimization. Given a predicate (a BooleanExpression to check for validity or to be simplified), method minimizeFor(SymbolicExpression, PreUniverse) produces a new context which is possibly weaker than the original one, but which is guaranteed to produce an equivalent result when used as the context for validity or simplification.

Let pc be the context, and say pc is the conjunction over some set C of clauses. Define an equivalence relation on C as follows: if two clauses have a free (not bound) symbolic constant in common, they are equivalent; complete by taking the transitive closure to an equivalence relation. Say C is the disjoint union of P1, P2, ..., where the Pi are the equivalence classes.

Given any symbolic constant X that occurs in the path condition, there is a unique i such that X occurs in at least one clause in Pi. Let P(X) denote this Pi.

Give any boolean symbolic expression q, let T(q) be the set of all clauses P(X) where X ranges over all symbolic constants occurring in q for which X also occurs in pc. Let subpc(pc, q) be the conjunction of these P(X). The expression subpc(pc, q) can be used for the context when attempting to determine the validity of q, and the result will be equivalent to using the full path condition pc.

It is possible that the context pc is unsatisfiable, yet pc(q) is satisfiable. However in this case any result can be returned for a validity request, since the contract for a prover leaves unspecified what is returned by TheoremProver.valid(BooleanExpression) when the context is unsatisfiable.

The main method (after construction) is minimizeFor(SymbolicExpression, PreUniverse). The results are cached.

  • Method Summary

    Modifier and Type
    Method
    Description
    List<BooleanExpression>
    minimizeFor(SymbolicExpression expr, PreUniverse universe)
    Returns a formula equivalent to or weaker than the original context but which can be used as the context for check validity or simplifying expr.

  • Method Details

    • minimizeFor

      List<BooleanExpression> minimizeFor(SymbolicExpression expr, PreUniverse universe)
      Returns a formula equivalent to or weaker than the original context but which can be used as the context for check validity or simplifying expr.
      Parameters:
      expr - any non-null boolean expression
      universe - the symbolic universe used to construct new symbolic expressions and which produced the context and expr
      Returns:
      the reduced context