From e043fe288ddfa5f5cf93ffe3aa7ddc5e8bf15439 Mon Sep 17 00:00:00 2001 From: Valentyn Sobol Date: Fri, 17 Feb 2023 21:40:09 +0300 Subject: [PATCH] Custom expression documentation (#72) * Basic example * Custom expression docs * Update version --- README.md | 19 +- Requirements.md | 64 +++-- .../main/kotlin/org.ksmt.ksmt-base.gradle.kts | 2 +- docs/custom-expressions.md | 272 ++++++++++++++++++ docs/getting-started.md | 6 +- examples/build.gradle.kts | 4 +- examples/src/main/kotlin/CustomExpressions.kt | 246 ++++++++++++++++ 7 files changed, 569 insertions(+), 44 deletions(-) create mode 100644 docs/custom-expressions.md create mode 100644 examples/src/main/kotlin/CustomExpressions.kt diff --git a/README.md b/README.md index 318f69a99..a652119be 100644 --- a/README.md +++ b/README.md @@ -14,9 +14,9 @@ repositories { } // core -implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.2") +implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.0") // z3 solver -implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.2") +implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.0") ``` ## Usage @@ -30,16 +30,17 @@ Currently, KSMT supports the following SMT solvers: |--------------------------------------------------|:------------------:|:------------------:|:------------------:| | [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | | [Bitwuzla](https://github.com/bitwuzla/bitwuzla) | :heavy_check_mark: | :heavy_check_mark: | | +| [Yices2](https://github.com/SRI-CSL/yices2) | :heavy_check_mark: | :heavy_check_mark: | | KSMT can express formulas in the following theories: -| Theory | Z3 | Bitwuzla | -|-------------------------|:------------------:|:------------------:| -| Bitvectors | :heavy_check_mark: | :heavy_check_mark: | -| Arrays | :heavy_check_mark: | :heavy_check_mark: | -| IEEE Floats | :heavy_check_mark: | :heavy_check_mark: | -| Uninterpreted Functions | :heavy_check_mark: | :heavy_check_mark: | -| Arithmetic | :heavy_check_mark: | | +| Theory | Z3 | Bitwuzla | Yices2 | +|-------------------------|:------------------:|:------------------:|--------------------| +| Bitvectors | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | +| Arrays | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | +| IEEE Floats | :heavy_check_mark: | :heavy_check_mark: | | +| Uninterpreted Functions | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | +| Arithmetic | :heavy_check_mark: | | :heavy_check_mark: | Check out our [roadmap](Requirements.md) for detailed description of features and future plans. diff --git a/Requirements.md b/Requirements.md index 2bd1ea5f8..42990e685 100644 --- a/Requirements.md +++ b/Requirements.md @@ -1,31 +1,32 @@ -| Feature | Status | -|-----------------------------------------------------------------------------------|-----------------| -| [Rich expression system](#rich-expression-system) | Done | -| [Expression interning](#expression-interning) | Done | -| [Basic theories support](#basic-theories-support) | Done | -| [SMT-LIB2 parser](#smt-lib2-parser) | Done partially | -| [SMT-LIB2 serializer](#smt-lib2-serializer) | TODO | -| [Unsupported features handling](#unsupported-features-handling) | Done partially | -| [SMT solver support](#smt-solver-support) | Done | -| [Z3 solver support](#z3-solver-support) | Done | -| [Bitwuzla solver support](#bitwuzla-solver-support) | Done | -| [Yices2 solver support](#yices2-solver-support) | In progress | -| [CVC5 solver support](#cvc5-solver-support) | TODO | -| [External process runner](#external-process-runner) | Done | -| [Portfolio solver](#portfolio-solver) | TODO | -| [Solver configuration API](#solver-configuration-api) | Done | -| [Deployment](#deployment) | Done partially | -| [Expression simplification / evaluation](#expression-simplification--evaluation) | Done partially | -| [Performance tests](#performance-tests) | TODO | -| [Better Z3 API](#better-z3-api) | Done partially | -| [Better Bitwuzla bindings](#better-bitwuzla-bindings) | TODO | -| [Solver specific features API](#solver-specific-features-api) | TODO | -| [Quantifier elimination](#quantifier-elimination) | TODO | -| [Interpolation](#interpolation) | TODO | -| [Model based projection](#model-based-projection) | TODO | -| [Support more theories](#support-more-theories) | TODO | -| [Solver proofs](#solver-proofs) | TODO | -| ... | - | +| Feature | Status | +|----------------------------------------------------------------------------------|----------------| +| [Rich expression system](#rich-expression-system) | Done | +| [Expression interning](#expression-interning) | Done | +| [Basic theories support](#basic-theories-support) | Done | +| [SMT-LIB2 parser](#smt-lib2-parser) | Done partially | +| [SMT-LIB2 serializer](#smt-lib2-serializer) | TODO | +| [Unsupported features handling](#unsupported-features-handling) | Done partially | +| [SMT solver support](#smt-solver-support) | Done | +| [Z3 solver support](#z3-solver-support) | Done | +| [Bitwuzla solver support](#bitwuzla-solver-support) | Done | +| [Yices2 solver support](#yices2-solver-support) | Done | +| [CVC5 solver support](#cvc5-solver-support) | In progress | +| [External process runner](#external-process-runner) | Done | +| [Portfolio solver](#portfolio-solver) | In progress | +| [Solver configuration API](#solver-configuration-api) | Done | +| [Deployment](#deployment) | Done partially | +| [Expression simplification / evaluation](#expression-simplification--evaluation) | Done | +| [Performance tests](#performance-tests) | TODO | +| [Better Z3 API](#better-z3-api) | Done partially | +| [Better Bitwuzla bindings](#better-bitwuzla-bindings) | Done | +| [Solver specific features API](#solver-specific-features-api) | TODO | +| [Quantifier elimination](#quantifier-elimination) | TODO | +| [Interpolation](#interpolation) | TODO | +| [Model based projection](#model-based-projection) | TODO | +| [Support more theories](#support-more-theories) | TODO | +| [Solver proofs](#solver-proofs) | TODO | +| [SymFpu](#symfpu) | In progress | +| ... | - | ### Rich expression system @@ -293,7 +294,12 @@ Some solvers provide native support for theories above, e.g. Z3 and CVC5. ### Solver proofs -In case of UNSAT many solvers can produce proof. +In case of UNSAT many solvers can produce proof. Provide a universal representation of proof in KSMT and implement conversion from solver native proof. +### SymFpu + +Support for Fp theory in SMT solvers that support Bv (e.g. Yices2). +The [SymFpu](https://github.com/martin-cs/symfpu) approach proposes to rewrite all +FP expressions over BV terms. diff --git a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts index 4f3486de1..167ffca2a 100644 --- a/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts +++ b/buildSrc/src/main/kotlin/org.ksmt.ksmt-base.gradle.kts @@ -9,7 +9,7 @@ plugins { } group = "org.ksmt" -version = "0.3.2" +version = "0.4.0" repositories { mavenCentral() diff --git a/docs/custom-expressions.md b/docs/custom-expressions.md new file mode 100644 index 000000000..f757fa25b --- /dev/null +++ b/docs/custom-expressions.md @@ -0,0 +1,272 @@ +# Custom expressions + +In some cases, it is convenient to extend the KSMT expression +system with user defined (custom) expressions. +Here we will describe the key points of creating custom expressions. + +See [CustomExpressions.kt](/examples/src/main/kotlin/CustomExpressions.kt) for a complete example. + +### Expressions definition + +As an example, we will consider the following custom expressions structure: +a base `CustomExpr` expression and two custom expressions. +The `CustomAndExpr` expression that acts like `n-ary logical and` +and `CustomBvAddExpr` that acts like `n-ary bvadd`. + +#### Base expression and transformer + +The important thing is that we must not only define our new custom expression, +but also define an extended `KTransformer`, because KSMT transformers are +unaware of our custom expressions. + +```kotlin +interface CustomTransformer : KTransformer { + fun transform(expr: CustomAndExpr): KExpr + fun transform(expr: CustomBvAddExpr): KExpr +} +``` + +For the base expression, we can override accept with our `CustomTransformer`, +since all of our custom expressions can only be correctly transformed with this transformer. + +```kotlin +abstract class CustomExpr(ctx: KContext) : KExpr(ctx) { + override fun accept(transformer: KTransformerBase): KExpr { + /** + * Since KSMT transformers are unaware of our custom expressions + * we must use our own extended transformer. + * + * Note: it's a good idea to throw an exception when our + * custom expression is visited by non our transformer, + * because this usually means that our custom expression + * has leaked into KSMT core and will be processed incorrectly. + * */ + transformer as? CustomTransformer ?: error("Leaked custom expression") + return accept(transformer) + } + + abstract fun accept(transformer: CustomTransformer): KExpr +} +``` + +#### Custom expressions + +Important notes on defining custom expressions are provided as comments in the examples. +Also, see [expression management](#expressions-management) for the details about `equals`, `hashCode`, +`internEquals` and `internHashCode`. + +```kotlin +class CustomAndExpr( + val args: List>, + ctx: KContext +) : CustomExpr(ctx) { + override val sort: KBoolSort + get() = ctx.boolSort + + /** + * Expression printer, suitable for deeply nested expressions. + * Mainly used in toString. + * */ + override fun print(printer: ExpressionPrinter) { + printer.append("(customAnd") + args.forEach { + printer.append(" ") + + /** + * Note the use of append with KExpr argument. + * */ + printer.append(it) + } + printer.append(")") + } + + /** + * Analogues of equals and hashCode. + * */ + override fun internHashCode(): Int = hash(args) + + /** + * Note the use of [structurallyEqual] utility, which check + * that types are the same and all fields specified in `{ }` are equal. + * */ + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { args } + + /** + * The expression is visited by the transformer. + * Normally, we should invoke the corresponding transform + * method of the transformer and return the invocation result. + * + * It is usually a bad idea to return something without transform + * invocation, or to invoke transform on some other expression. + * It is better to perform any expression transformation with the + * corresponding transformer. + * */ + override fun accept(transformer: CustomTransformer): KExpr = + transformer.transform(this) +} +``` + +The definition of `CustomBvAddExpr` is actually the same as for `CustomAndExpr`. + +```kotlin +class CustomBvAddExpr( + val args: List>, + ctx: KContext +) : CustomExpr(ctx) { + + /** + * The sort of this expression is parametric and + * depends on the sorts of arguments. + * */ + override val sort: T by lazy { args.first().sort } + + override fun print(printer: ExpressionPrinter) { + printer.append("(customBvAdd") + args.forEach { + printer.append(" ") + printer.append(it) + } + printer.append(")") + } + + override fun internHashCode(): Int = hash(args) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { args } + + override fun accept(transformer: CustomTransformer): KExpr = + transformer.transform(this) +} +``` + +### Expressions rewriting + +Since KSMT is unaware of our custom expressions, +we must ensure that the expressions that will be processed +by the various KSMT facilities do not contain any custom parts. +For such purposes we can define a transformer for our custom expressions that rewrites +them with the appropriate KSMT expressions. + +```kotlin +class CustomExprRewriter( + override val ctx: KContext +) : KNonRecursiveTransformer(ctx), CustomTransformer { + /** + * Here we use [transformExprAfterTransformed] function of [KNonRecursiveTransformer] + * that implements bottom-up transformation (transform arguments first). + * */ + override fun transform(expr: CustomBvAddExpr): KExpr = + transformExprAfterTransformed(expr, expr.args) { transformedArgs -> + transformedArgs.reduce { acc, e -> ctx.mkBvAddExpr(acc, e) } + } + + override fun transform(expr: CustomAndExpr): KExpr = + transformExprAfterTransformed(expr, expr.args) { transformedArgs -> + ctx.mkAnd(transformedArgs) + } +} + +``` + +Note the use of `KNonRecursiveTransformer` that allows transformation of deeply nested expressions without recursion. + +### Expressions management + +In KSMT we use expression interning and guarantee that any +two equal expressions are equal by reference (same object). +We use `internEquals` and `internHashCode` as a replacement for `equals` and `hashCode`, +and we use reference equality for the `equals` method. +To apply interning for custom expressions you need to create an interner and ensure that +all created expressions are managed by this interner. +For such purposes it is convenient to define an extended context that manages all custom expressions. + +```kotlin +class CustomContext : KContext() { + // Interners for custom expressions. + private val customAndInterner = mkAstInterner() + private val customBvInterner = mkAstInterner>() + + // Expression builder, that performs interning of created expression + fun mkCustomAnd(args: List>): CustomAndExpr = + customAndInterner.createIfContextActive { + CustomAndExpr(args, this) + } + + fun mkCustomBvAdd(args: List>): CustomBvAddExpr = + customBvInterner.createIfContextActive { + CustomBvAddExpr(args, this) + }.uncheckedCast() // Unchecked cast is used here because [customBvInterner] has erased sort. +} +``` + +### Misc: wrappers + +Since it is required to eliminate all our custom expressions +before interaction with any KSMT feature, +it is convenient to create wrappers. + +For example, we can wrap `KSolver` and eliminate custom expressions on each query. + +```kotlin +class CustomSolver( + private val solver: KSolver, + private val transformer: CustomExprRewriter +) : KSolver { + + // expr can contain custom expressions -> rewrite + override fun assert(expr: KExpr) = + solver.assert(transformer.apply(expr)) + + // expr can contain custom expressions -> rewrite + override fun assertAndTrack(expr: KExpr): KExpr = + solver.assertAndTrack(transformer.apply(expr)) + + // assumptions can contain custom expressions -> rewrite + override fun checkWithAssumptions(assumptions: List>, timeout: Duration): KSolverStatus = + solver.checkWithAssumptions(assumptions.map { transformer.apply(it) }, timeout) + + // wrap model for correct handling of eval method + override fun model(): KModel = CustomModel(solver.model(), transformer) + + // Other methods don't suffer from custom expressions + + override fun check(timeout: Duration): KSolverStatus = + solver.check(timeout) + + override fun pop(n: UInt) = solver.pop(n) + override fun push() = solver.push() + + override fun reasonOfUnknown(): String = solver.reasonOfUnknown() + override fun unsatCore(): List> = solver.unsatCore() + + override fun close() = solver.close() + override fun configure(configurator: C.() -> Unit) = solver.configure(configurator) +} +``` + +Also, we can wrap `KModel` and eliminate custom expressions before eval. + +```kotlin +class CustomModel( + private val model: KModel, + private val transformer: CustomExprRewriter +) : KModel { + // expr can contain custom expressions -> rewrite + override fun eval(expr: KExpr, isComplete: Boolean): KExpr = + model.eval(transformer.apply(expr), isComplete) + + // Other methods don't suffer from custom expressions + + override val declarations: Set> + get() = model.declarations + + override val uninterpretedSorts: Set + get() = model.uninterpretedSorts + + override fun interpretation(decl: KDecl): KModel.KFuncInterp? = + model.interpretation(decl) + + override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set>? = + model.uninterpretedSortUniverse(sort) + + override fun detach(): KModel = CustomModel(model.detach(), transformer) +} +``` diff --git a/docs/getting-started.md b/docs/getting-started.md index f9eab3a67..7955709ec 100644 --- a/docs/getting-started.md +++ b/docs/getting-started.md @@ -18,7 +18,7 @@ repositories { ```kotlin dependencies { // core - implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.2") + implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.0") } ``` @@ -26,9 +26,9 @@ dependencies { ```kotlin dependencies { // z3 - implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.2") + implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.0") // bitwuzla - implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.3.2") + implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.4.0") } ``` SMT solver specific packages are provided with solver native binaries. diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts index ad992a522..43f1605a6 100644 --- a/examples/build.gradle.kts +++ b/examples/build.gradle.kts @@ -10,9 +10,9 @@ repositories { dependencies { // core - implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.3.2") + implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.4.0") // z3 solver - implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.3.2") + implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.4.0") } java { diff --git a/examples/src/main/kotlin/CustomExpressions.kt b/examples/src/main/kotlin/CustomExpressions.kt new file mode 100644 index 000000000..e197edcb5 --- /dev/null +++ b/examples/src/main/kotlin/CustomExpressions.kt @@ -0,0 +1,246 @@ +import org.ksmt.KContext +import org.ksmt.cache.hash +import org.ksmt.cache.structurallyEqual +import org.ksmt.decl.KDecl +import org.ksmt.expr.KExpr +import org.ksmt.expr.printer.ExpressionPrinter +import org.ksmt.expr.transformer.KNonRecursiveTransformer +import org.ksmt.expr.transformer.KTransformer +import org.ksmt.expr.transformer.KTransformerBase +import org.ksmt.solver.KModel +import org.ksmt.solver.KSolver +import org.ksmt.solver.KSolverConfiguration +import org.ksmt.solver.KSolverStatus +import org.ksmt.sort.KBoolSort +import org.ksmt.sort.KBvSort +import org.ksmt.sort.KSort +import org.ksmt.sort.KUninterpretedSort +import org.ksmt.utils.uncheckedCast +import kotlin.time.Duration + +/** + * Base expression for all our custom expressions. + * */ +abstract class CustomExpr(ctx: KContext) : KExpr(ctx) { + override fun accept(transformer: KTransformerBase): KExpr { + /** + * Since KSMT transformers are unaware of our custom expressions + * we must use our own extended transformer. + * + * Note: it's a good idea to throw an exception when our + * custom expression is visited by non our transformer, + * because this usually means that our custom expression + * has leaked into KSMT core and will be processed incorrectly. + * */ + transformer as? CustomTransformer ?: error("Leaked custom expression") + return accept(transformer) + } + + abstract fun accept(transformer: CustomTransformer): KExpr +} + +/** + * Extended transformer for our expressions. + * */ +interface CustomTransformer : KTransformer { + fun transform(expr: CustomAndExpr): KExpr + fun transform(expr: CustomBvAddExpr): KExpr +} + +/** + * Example: custom expression that acts like n-ary logical and. + * */ +class CustomAndExpr( + val args: List>, + ctx: KContext +) : CustomExpr(ctx) { + override val sort: KBoolSort + get() = ctx.boolSort + + /** + * Expression printer, suitable for deeply nested expressions. + * Mainly used in toString. + * */ + override fun print(printer: ExpressionPrinter) { + printer.append("(customAnd") + args.forEach { + printer.append(" ") + + /** + * Note the use of append with KExpr argument. + * */ + printer.append(it) + } + printer.append(")") + } + + /** + * Analogues of equals and hashCode. + * */ + override fun internHashCode(): Int = hash(args) + + /** + * Note the use of [structurallyEqual] utility, which check + * that types are the same and all fields specified in `{ }` are equal. + * */ + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { args } + + /** + * The expression is visited by the transformer. + * Normally, we should invoke the corresponding transform + * method of the transformer and return the invocation result. + * + * It is usually a bad idea to return something without transform + * invocation, or to invoke transform on some other expression. + * It is better to perform any expression transformation with the + * corresponding transformer. + * */ + override fun accept(transformer: CustomTransformer): KExpr = + transformer.transform(this) +} + +/** + * Example: custom expression that acts like n-ary bvadd. + * */ +class CustomBvAddExpr( + val args: List>, + ctx: KContext +) : CustomExpr(ctx) { + + /** + * The sort of this expression is parametric and + * depends on the sorts of arguments. + * */ + override val sort: T by lazy { args.first().sort } + + override fun print(printer: ExpressionPrinter) { + printer.append("(customBvAdd") + args.forEach { + printer.append(" ") + printer.append(it) + } + printer.append(")") + } + + override fun internHashCode(): Int = hash(args) + override fun internEquals(other: Any): Boolean = structurallyEqual(other) { args } + + override fun accept(transformer: CustomTransformer): KExpr = + transformer.transform(this) +} + +/** + * Rewriter: a transformer for our custom expressions that rewrites + * them with the appropriate KSMT expressions. Such a transformer is required + * to interact with KSolver and other KSMT features. + * + * Note the use of [KNonRecursiveTransformer] that allows transformation + * of deeply nested expressions without recursion. + * */ +class CustomExprRewriter( + override val ctx: KContext +) : KNonRecursiveTransformer(ctx), CustomTransformer { + /** + * Here we use [transformExprAfterTransformed] function of [KNonRecursiveTransformer] + * that implements bottom-up transformation (transform arguments first). + * */ + override fun transform(expr: CustomBvAddExpr): KExpr = + transformExprAfterTransformed(expr, expr.args) { transformedArgs -> + transformedArgs.reduce { acc, e -> ctx.mkBvAddExpr(acc, e) } + } + + override fun transform(expr: CustomAndExpr): KExpr = + transformExprAfterTransformed(expr, expr.args) { transformedArgs -> + ctx.mkAnd(transformedArgs) + } +} + +/** + * Since it is required to eliminate all + * our custom expressions before interaction with any + * KSMT feature, it is convenient to create wrappers + * + * KSolver wrapper which eliminates custom expressions. + * */ +class CustomSolver( + private val solver: KSolver, + private val transformer: CustomExprRewriter +) : KSolver { + + // expr can contain custom expressions -> rewrite + override fun assert(expr: KExpr) = + solver.assert(transformer.apply(expr)) + + // expr can contain custom expressions -> rewrite + override fun assertAndTrack(expr: KExpr): KExpr = + solver.assertAndTrack(transformer.apply(expr)) + + // assumptions can contain custom expressions -> rewrite + override fun checkWithAssumptions(assumptions: List>, timeout: Duration): KSolverStatus = + solver.checkWithAssumptions(assumptions.map { transformer.apply(it) }, timeout) + + // wrap model for correct handling of eval method + override fun model(): KModel = CustomModel(solver.model(), transformer) + + // Other methods don't suffer from custom expressions + + override fun check(timeout: Duration): KSolverStatus = + solver.check(timeout) + + override fun pop(n: UInt) = solver.pop(n) + override fun push() = solver.push() + + override fun reasonOfUnknown(): String = solver.reasonOfUnknown() + override fun unsatCore(): List> = solver.unsatCore() + + override fun close() = solver.close() + override fun configure(configurator: C.() -> Unit) = solver.configure(configurator) +} + +/** + * KModel wrapper which eliminates custom expressions. + * */ +class CustomModel( + private val model: KModel, + private val transformer: CustomExprRewriter +) : KModel { + // expr can contain custom expressions -> rewrite + override fun eval(expr: KExpr, isComplete: Boolean): KExpr = + model.eval(transformer.apply(expr), isComplete) + + // Other methods don't suffer from custom expressions + + override val declarations: Set> + get() = model.declarations + + override val uninterpretedSorts: Set + get() = model.uninterpretedSorts + + override fun interpretation(decl: KDecl): KModel.KFuncInterp? = + model.interpretation(decl) + + override fun uninterpretedSortUniverse(sort: KUninterpretedSort): Set>? = + model.uninterpretedSortUniverse(sort) + + override fun detach(): KModel = CustomModel(model.detach(), transformer) +} + +/** + * Extended context for our custom expressions. + * */ +class CustomContext : KContext() { + // Interners for custom expressions. + private val customAndInterner = mkAstInterner() + private val customBvInterner = mkAstInterner>() + + // Expression builder, that performs interning of created expression + fun mkCustomAnd(args: List>): CustomAndExpr = + customAndInterner.createIfContextActive { + CustomAndExpr(args, this) + } + + fun mkCustomBvAdd(args: List>): CustomBvAddExpr = + customBvInterner.createIfContextActive { + CustomBvAddExpr(args, this) + }.uncheckedCast() // Unchecked cast is used here because [customBvInterner] has erased sort. +}