ksmt-core/io.ksmt.expr.rewrite.simplify/KBoolExprSimplifier/transform

transform

open override fun transform(expr: KAndExpr): KExpr<KBoolSort>
open override fun transform(expr: KOrExpr): KExpr<KBoolSort>
open override fun transform(expr: KNotExpr): KExpr<KBoolSort>
open override fun transform(expr: KImpliesExpr): KExpr<KBoolSort>
open override fun transform(expr: KXorExpr): KExpr<KBoolSort>

open override fun <T : KSort> transform(expr: KIteExpr<T>): KExpr<T>

Simplify ite expression in two stages:

  1. Simplify condition only SimplifierStagedIteCondition. If condition is true/false only one branch simplification is required.

  2. Simplify ite branches SimplifierStagedIteBranches.