From 67f360b2c605ab64efd6c37f00ff2d2004f0ab5f Mon Sep 17 00:00:00 2001 From: Jk Xu <54522439+Dousir9@users.noreply.github.com> Date: Wed, 29 May 2024 16:40:19 +0800 Subject: [PATCH] chore(planner): remove z3 (#15663) * chore: remove z3 * chore: improve can filter null --- .gitignore | 3 - Cargo.lock | 31 - Cargo.toml | 3 - Makefile | 2 +- docker/build-tool/musl/Dockerfile | 7 - src/binaries/Cargo.toml | 3 +- src/query/constraint/Cargo.toml | 25 - src/query/constraint/benches/bench.rs | 143 - src/query/constraint/src/declare.rs | 440 - src/query/constraint/src/lib.rs | 18 - src/query/constraint/src/mir.rs | 392 - src/query/constraint/src/problem.rs | 104 - src/query/constraint/src/simplify.rs | 60 - src/query/constraint/tests/it/declare.rs | 446 - src/query/constraint/tests/it/main.rs | 20 - src/query/constraint/tests/it/parser.rs | 234 - src/query/constraint/tests/it/problem.rs | 68 - src/query/constraint/tests/it/simplify.rs | 173 - .../constraint/tests/it/testdata/simplify.txt | 7495 ----------------- src/query/expression/src/expression.rs | 10 + src/query/service/Cargo.toml | 3 +- src/query/sql/Cargo.toml | 2 - .../planner/optimizer/property/constraint.rs | 192 - .../sql/src/planner/optimizer/property/mod.rs | 5 - .../sql/src/planner/optimizer/rule/factory.rs | 2 +- .../outer_join_to_inner_join.rs | 136 +- .../rewrite/rule_push_down_filter_join.rs | 17 +- .../sql/src/planner/plans/scalar_expr.rs | 35 + .../explain/eliminate_outer_join.test | 56 +- 29 files changed, 149 insertions(+), 9976 deletions(-) delete mode 100644 src/query/constraint/Cargo.toml delete mode 100644 src/query/constraint/benches/bench.rs delete mode 100644 src/query/constraint/src/declare.rs delete mode 100644 src/query/constraint/src/lib.rs delete mode 100644 src/query/constraint/src/mir.rs delete mode 100644 src/query/constraint/src/problem.rs delete mode 100644 src/query/constraint/src/simplify.rs delete mode 100644 src/query/constraint/tests/it/declare.rs delete mode 100644 src/query/constraint/tests/it/main.rs delete mode 100644 src/query/constraint/tests/it/parser.rs delete mode 100644 src/query/constraint/tests/it/problem.rs delete mode 100644 src/query/constraint/tests/it/simplify.rs delete mode 100644 src/query/constraint/tests/it/testdata/simplify.txt delete mode 100644 src/query/sql/src/planner/optimizer/property/constraint.rs diff --git a/.gitignore b/.gitignore index ec4d621ac995..70c2442408e2 100644 --- a/.gitignore +++ b/.gitignore @@ -73,8 +73,5 @@ benchmark/clickbench/results # direnv test files .envrc -# z3 -**/.z3-trace - # lychee .lycheecache diff --git a/Cargo.lock b/Cargo.lock index 41027680f1b5..b09a50df8e7c 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2922,16 +2922,6 @@ dependencies = [ "strum 0.24.1", ] -[[package]] -name = "databend-common-constraint" -version = "0.1.0" -dependencies = [ - "criterion", - "databend-common-ast", - "goldenfile", - "z3", -] - [[package]] name = "databend-common-datavalues" version = "0.1.0" @@ -3738,7 +3728,6 @@ dependencies = [ "databend-common-catalog", "databend-common-compress", "databend-common-config", - "databend-common-constraint", "databend-common-exception", "databend-common-expression", "databend-common-functions", @@ -15775,26 +15764,6 @@ version = "1.0.0-rc.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1367295b8f788d371ce2dbc842c7b709c73ee1364d30351dd300ec2203b12377" -[[package]] -name = "z3" -version = "0.12.1" -source = "git+https://github.com/prove-rs/z3.rs?rev=247d308#247d308f27d8b59152ad402e2d8b13d617a1a6a1" -dependencies = [ - "log", - "num", - "z3-sys", -] - -[[package]] -name = "z3-sys" -version = "0.8.1" -source = "git+https://github.com/prove-rs/z3.rs?rev=247d308#247d308f27d8b59152ad402e2d8b13d617a1a6a1" -dependencies = [ - "bindgen 0.69.4", - "cmake", - "pkg-config", -] - [[package]] name = "z85" version = "3.0.5" diff --git a/Cargo.toml b/Cargo.toml index 3bec3cb0da77..e840359fba4a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -35,7 +35,6 @@ members = [ "src/query/async_functions", "src/query/codegen", "src/query/config", - "src/query/constraint", "src/query/catalog", "src/query/sharing", "src/query/sharing_endpoint", @@ -306,6 +305,4 @@ arrow-format = { git = "https://github.com/Xuanwo/arrow-format", rev = "be633a0" icelake = { git = "https://github.com/icelake-io/icelake", rev = "be8b2c2" } ethnum = { git = "https://github.com/ariesdevil/ethnum-rs", rev = "4cb05f1" } async-backtrace = { git = "https://github.com/zhang2014/async-backtrace.git", rev = "dea4553" } -z3 = { git = "https://github.com/prove-rs/z3.rs", rev = "247d308" } -z3-sys = { git = "https://github.com/prove-rs/z3.rs", rev = "247d308" } # proj = { git = "https://github.com/ariesdevil/proj", rev = "51e1c60" } diff --git a/Makefile b/Makefile index 4fe4ae6b3089..fbf18a5d3353 100644 --- a/Makefile +++ b/Makefile @@ -110,7 +110,7 @@ clean: rm -f ./nohup.out ./tests/suites/0_stateless/*.stdout-e rm -rf ./_meta*/ ./_logs*/ ./src/query/service_logs*/ ./src/meta/service/_logs*/ ./stateless_test_data/ rm -rf ./src/common/base/_logs*/ ./src/meta/raft-store/_logs*/ ./src/meta/sled-store/_logs*/ - find . \( -type f -name '.z3-trace' -o -type d -name '.databend' \) | xargs rm -rf + rm -rf ./.databend ./query/service/.databend ./meta/service/.databend genproto: python -m grpc_tools.protoc -Isrc/common/cloud_control/proto/ --python_out=tests/cloud_control_server/ --grpc_python_out=tests/cloud_control_server/ src/common/cloud_control/proto/task.proto diff --git a/docker/build-tool/musl/Dockerfile b/docker/build-tool/musl/Dockerfile index 8d1e26917565..f4e1e53f7d26 100644 --- a/docker/build-tool/musl/Dockerfile +++ b/docker/build-tool/musl/Dockerfile @@ -20,13 +20,6 @@ RUN ln -s ${MUSL_TARGET}-gcc /usr/local/bin/musl-gcc RUN rustup target add ${MUSL_RUST_TARGET} -# needed by z3 -RUN ln -s ${MUSL_TARGET}-g++ /usr/local/bin/musl-g++ -RUN ln -s ${MUSL_TARGET}-ar /usr/local/bin/musl-ar - -# HACK: something wrong with python detection in cmake for z3 -RUN ln -s python3.9 /usr/bin/python3.10 - # HACK: to link with libstdc++ statically # ref: https://github.com/rust-lang/rust/issues/36710#issuecomment-364623950 COPY linker.sh /usr/local/bin/linker diff --git a/src/binaries/Cargo.toml b/src/binaries/Cargo.toml index 416e18cd1807..9b96cdb7e257 100644 --- a/src/binaries/Cargo.toml +++ b/src/binaries/Cargo.toml @@ -8,7 +8,7 @@ publish = { workspace = true } edition = { workspace = true } [features] -default = ["simd", "jemalloc", "z3-prove"] +default = ["simd", "jemalloc"] memory-profiling = [ "databend-meta/memory-profiling", "databend-query/memory-profiling", @@ -16,7 +16,6 @@ memory-profiling = [ ] python-udf = ["databend-query/python-udf"] simd = ["databend-meta/simd", "databend-query/simd"] -z3-prove = ["databend-query/z3-prove"] jemalloc = ["databend-common-base/jemalloc"] io-uring = [ "databend-meta/io-uring", diff --git a/src/query/constraint/Cargo.toml b/src/query/constraint/Cargo.toml deleted file mode 100644 index 6113a74d4cfe..000000000000 --- a/src/query/constraint/Cargo.toml +++ /dev/null @@ -1,25 +0,0 @@ -[package] -name = "databend-common-constraint" -version = { workspace = true } -authors = { workspace = true } -license = { workspace = true } -publish = { workspace = true } -edition = { workspace = true } - -[lib] -test = true - -[dependencies] # In alphabetical order -# Workspace dependencies - -# Crates.io dependencies -z3 = { version = "0.12.1", features = ["bundled"] } - -[dev-dependencies] -criterion = { workspace = true } -databend-common-ast = { path = "../ast" } -goldenfile = "1.4" - -[[bench]] -name = "bench" -harness = false diff --git a/src/query/constraint/benches/bench.rs b/src/query/constraint/benches/bench.rs deleted file mode 100644 index 1a3f597bf45f..000000000000 --- a/src/query/constraint/benches/bench.rs +++ /dev/null @@ -1,143 +0,0 @@ -// Copyright 2021 Datafuse Labs -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -#[macro_use] -extern crate criterion; - -use criterion::black_box; -use criterion::Criterion; -use databend_common_constraint::mir::MirBinaryOperator; -use databend_common_constraint::mir::MirConstant; -use databend_common_constraint::mir::MirDataType; -use databend_common_constraint::mir::MirExpr; -use databend_common_constraint::problem::variable_must_not_null; -use databend_common_constraint::simplify::simplify; - -fn bench(c: &mut Criterion) { - let mut group = c.benchmark_group("bench_solver"); - group.sample_size(10); - - group.bench_function("solve_variable_not_null", |b| { - b.iter(|| { - // a > 0 and a < 1 => a is not null - let assertion = MirExpr::BinaryOperator { - op: MirBinaryOperator::And, - left: Box::new(MirExpr::BinaryOperator { - op: MirBinaryOperator::Gt, - left: Box::new(MirExpr::Variable { - name: "a".to_string(), - data_type: MirDataType::Int, - }), - right: Box::new(MirExpr::Constant(MirConstant::Int(0))), - }), - right: Box::new(MirExpr::BinaryOperator { - op: MirBinaryOperator::Lt, - left: Box::new(MirExpr::Variable { - name: "a".to_string(), - data_type: MirDataType::Int, - }), - right: Box::new(MirExpr::Constant(MirConstant::Int(1))), - }), - }; - let result = variable_must_not_null(&assertion, "a"); - black_box(result); - }); - }); - - group.bench_function("solve_variable_not_null_multiple_variables", |b| { - b.iter(|| { - // (a > 0 and b > 0) or (a < 0 and b < 0) => a is not null - let assertion = MirExpr::BinaryOperator { - op: MirBinaryOperator::Or, - left: Box::new(MirExpr::BinaryOperator { - op: MirBinaryOperator::And, - left: Box::new(MirExpr::BinaryOperator { - op: MirBinaryOperator::Gt, - left: Box::new(MirExpr::Variable { - name: "a".to_string(), - data_type: MirDataType::Int, - }), - right: Box::new(MirExpr::Constant(MirConstant::Int(0))), - }), - right: Box::new(MirExpr::BinaryOperator { - op: MirBinaryOperator::Gt, - left: Box::new(MirExpr::Variable { - name: "b".to_string(), - data_type: MirDataType::Int, - }), - right: Box::new(MirExpr::Constant(MirConstant::Int(0))), - }), - }), - right: Box::new(MirExpr::BinaryOperator { - op: MirBinaryOperator::And, - left: Box::new(MirExpr::BinaryOperator { - op: MirBinaryOperator::Lt, - left: Box::new(MirExpr::Variable { - name: "a".to_string(), - data_type: MirDataType::Int, - }), - right: Box::new(MirExpr::Constant(MirConstant::Int(0))), - }), - right: Box::new(MirExpr::BinaryOperator { - op: MirBinaryOperator::Lt, - left: Box::new(MirExpr::Variable { - name: "b".to_string(), - data_type: MirDataType::Int, - }), - right: Box::new(MirExpr::Constant(MirConstant::Int(0))), - }), - }), - }; - let result = variable_must_not_null(&assertion, "a"); - black_box(result); - }); - }); - - group.bench_function("simplify", |b| { - b.iter(|| { - // a + b < 1 and a >= 0 - let expr = MirExpr::BinaryOperator { - op: MirBinaryOperator::And, - left: Box::new(MirExpr::BinaryOperator { - op: MirBinaryOperator::Lt, - left: Box::new(MirExpr::BinaryOperator { - op: MirBinaryOperator::Plus, - left: Box::new(MirExpr::Variable { - name: "a".to_string(), - data_type: MirDataType::Int, - }), - right: Box::new(MirExpr::Variable { - name: "b".to_string(), - data_type: MirDataType::Int, - }), - }), - right: Box::new(MirExpr::Constant(MirConstant::Int(1))), - }), - right: Box::new(MirExpr::BinaryOperator { - op: MirBinaryOperator::Gte, - left: Box::new(MirExpr::Variable { - name: "a".to_string(), - data_type: MirDataType::Int, - }), - right: Box::new(MirExpr::Constant(MirConstant::Int(0))), - }), - }; - let simplified = simplify(&expr).unwrap(); - black_box(simplified); - }); - }); -} - -criterion_group!(benches, bench); -criterion_main!(benches); diff --git a/src/query/constraint/src/declare.rs b/src/query/constraint/src/declare.rs deleted file mode 100644 index 712aca06e840..000000000000 --- a/src/query/constraint/src/declare.rs +++ /dev/null @@ -1,440 +0,0 @@ -// Copyright 2021 Datafuse Labs -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -use std::ops::Add; -use std::ops::Mul; -use std::ops::Sub; - -use z3::ast::Ast; -use z3::ast::Bool; -use z3::ast::Datatype; -use z3::ast::Dynamic; -use z3::ast::Int; -use z3::Context; -use z3::DatatypeAccessor; -use z3::DatatypeBuilder; -use z3::DatatypeSort; -use z3::Sort; - -/// Get the Z3 sort of Nullable Boolean type. -pub fn nullable_bool_sort(ctx: &Context) -> DatatypeSort { - DatatypeBuilder::new(ctx, "Nullable(Boolean)") - .variant("TRUE_BOOL", vec![]) - .variant("FALSE_BOOL", vec![]) - .variant("NULL_BOOL", vec![]) - .finish() -} - -/// Construct a TRUE value of Nullable Boolean type. -pub fn true_bool(ctx: &Context) -> Dynamic { - nullable_bool_sort(ctx).variants[0].constructor.apply(&[]) -} - -/// Construct a FALSE value of Nullable Boolean type. -pub fn false_bool(ctx: &Context) -> Dynamic { - nullable_bool_sort(ctx).variants[1].constructor.apply(&[]) -} - -/// Construct a NULL value of Nullable Boolean type. -pub fn null_bool(ctx: &Context) -> Dynamic { - nullable_bool_sort(ctx).variants[2].constructor.apply(&[]) -} - -/// Check if a Nullable Boolean value is true. -pub fn is_true<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>) -> Bool<'ctx> { - debug_assert!(a.get_sort() == nullable_bool_sort(ctx).sort); - a._eq(&true_bool(ctx)) -} - -/// Check if a Nullable Boolean value is false. -pub fn is_false<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>) -> Bool<'ctx> { - debug_assert!(a.get_sort() == nullable_bool_sort(ctx).sort); - a._eq(&false_bool(ctx)) -} - -/// Construct a Nullable Boolean value from a bool constant. -pub fn const_bool(ctx: &Context, a: bool) -> Dynamic<'_> { - if a { true_bool(ctx) } else { false_bool(ctx) } -} - -/// Construct a variable of Nullable Boolean type. -pub fn var_bool<'ctx>(ctx: &'ctx Context, name: &str) -> Dynamic<'ctx> { - Dynamic::from_ast(&Datatype::new_const( - ctx, - name, - &nullable_bool_sort(ctx).sort, - )) -} - -/// Construct a Nullable Boolean value from a Boolean value. -pub fn from_bool<'ctx>(ctx: &'ctx Context, a: &Bool<'ctx>) -> Dynamic<'ctx> { - a.ite(&true_bool(ctx), &false_bool(ctx)) -} - -pub fn nullable_int_sort(ctx: &Context) -> DatatypeSort { - DatatypeBuilder::new(ctx, "Nullable(Int)") - .variant("NULL_INT", vec![]) - .variant("JUST_INT", vec![( - "unwrap-int", - DatatypeAccessor::Sort(Sort::int(ctx)), - )]) - .finish() -} - -/// Construct a NULL value of Nullable(Int) type. -pub fn null_int(ctx: &Context) -> Dynamic<'_> { - nullable_int_sort(ctx).variants[0].constructor.apply(&[]) -} - -/// Construct a const Nullable(Int) from an i64. -pub fn const_int(ctx: &Context, a: i64) -> Dynamic<'_> { - from_int(ctx, &Int::from_i64(ctx, a)) -} - -/// Construct a variable of Nullable(Int) type. -pub fn var_int<'ctx>(ctx: &'ctx Context, name: &str) -> Dynamic<'ctx> { - Dynamic::from_ast(&Datatype::new_const( - ctx, - name, - &nullable_int_sort(ctx).sort, - )) -} - -/// Construct a const value of Int type. -pub fn from_int<'ctx>(ctx: &'ctx Context, a: &Int<'ctx>) -> Dynamic<'ctx> { - nullable_int_sort(ctx).variants[1].constructor.apply(&[a]) -} - -/// Equality check for Nullable(Int) type. -/// The table below shows the result of `eq_int`: -/// -/// | a | b | result | -/// |---|---|--------| -/// | NULL | NULL | NULL | -/// | NULL | 1 | NULL | -/// | 1 | NULL | NULL | -/// | 1 | 1 | TRUE | -/// | 1 | 2 | FALSE | -pub fn eq_int<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>, b: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); - debug_assert!(b.get_sort() == nullable_int_sort(ctx).sort); - - // IF(a IS NULL OR b IS NULL, NULL, a = b) - Bool::or(ctx, &[&is_null_int(ctx, a), &is_null_int(ctx, b)]) - .ite(&null_bool(ctx), &from_bool(ctx, &a._eq(b))) -} - -// /// Inequality check for Nullable(Int) type. -// /// The table below shows the result of `ne_int`: -// /// -// /// | a | b | result | -// /// |---|---|--------| -// /// | NULL | NULL | NULL | -// /// | NULL | 1 | NULL | -// /// | 1 | NULL | NULL | -// /// | 1 | 1 | FALSE | -// /// | 1 | 2 | TRUE | -// pub fn ne_int<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>, b: &Dynamic<'ctx>) -> Dynamic<'ctx> { -// debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); -// debug_assert!(b.get_sort() == nullable_int_sort(ctx).sort); - -// // IF(a IS NULL OR b IS NULL, NULL, a != b) -// Bool::or(ctx, &[&is_null_int(ctx, a), &is_null_int(ctx, b)]).ite( -// &null_bool(ctx), -// &a._eq(b).ite(&false_bool(ctx), &true_bool(ctx)), -// ) -// } - -/// Greater than check for Nullable(Int) type. -/// The table below shows the result of `gt_int`: -/// -/// | a | b | result | -/// |---|---|--------| -/// | NULL | NULL | NULL | -/// | NULL | 1 | NULL | -/// | 1 | NULL | NULL | -/// | 1 | 1 | FALSE | -/// | 1 | 2 | FALSE | -/// | 2 | 1 | TRUE | -pub fn gt_int<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>, b: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); - debug_assert!(b.get_sort() == nullable_int_sort(ctx).sort); - - // IF(a IS NULL OR b IS NULL, NULL, a > b) - Bool::or(ctx, &[&is_null_int(ctx, a), &is_null_int(ctx, b)]).ite( - &null_bool(ctx), - &from_bool(ctx, &unwrap_int(ctx, a).gt(&unwrap_int(ctx, b))), - ) -} - -/// Less than check for Nullable(Int) type. -/// The table below shows the result of `lt_int`: -/// -/// | a | b | result | -/// |---|---|--------| -/// | NULL | NULL | NULL | -/// | NULL | 1 | NULL | -/// | 1 | NULL | NULL | -/// | 1 | 1 | FALSE | -/// | 1 | 2 | TRUE | -/// | 2 | 1 | FALSE | -pub fn lt_int<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>, b: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); - debug_assert!(b.get_sort() == nullable_int_sort(ctx).sort); - - // IF(a IS NULL OR b IS NULL, NULL, a < b) - Bool::or(ctx, &[&is_null_int(ctx, a), &is_null_int(ctx, b)]).ite( - &null_bool(ctx), - &from_bool(ctx, &unwrap_int(ctx, a).lt(&unwrap_int(ctx, b))), - ) -} - -/// Greater than or equal check for Nullable(Int) type. -/// The table below shows the result of `ge_int`: -/// -/// | a | b | result | -/// |---|---|--------| -/// | NULL | NULL | NULL | -/// | NULL | 1 | NULL | -/// | 1 | NULL | NULL | -/// | 1 | 1 | TRUE | -/// | 1 | 2 | FALSE | -/// | 2 | 1 | TRUE | -pub fn ge_int<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>, b: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); - debug_assert!(b.get_sort() == nullable_int_sort(ctx).sort); - - // IF(a IS NULL OR b IS NULL, NULL, a >= b) - Bool::or(ctx, &[&is_null_int(ctx, a), &is_null_int(ctx, b)]).ite( - &null_bool(ctx), - &from_bool(ctx, &unwrap_int(ctx, a).ge(&unwrap_int(ctx, b))), - ) -} - -/// Less than or equal check for Nullable(Int) type. -/// The table below shows the result of `le_int`: -/// -/// | a | b | result | -/// |---|---|--------| -/// | NULL | NULL | NULL | -/// | NULL | 1 | NULL | -/// | 1 | NULL | NULL | -/// | 1 | 1 | TRUE | -/// | 1 | 2 | TRUE | -/// | 2 | 1 | FALSE | -pub fn le_int<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>, b: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); - debug_assert!(b.get_sort() == nullable_int_sort(ctx).sort); - - // IF(a IS NULL OR b IS NULL, NULL, a <= b) - Bool::or(ctx, &[&is_null_int(ctx, a), &is_null_int(ctx, b)]).ite( - &null_bool(ctx), - &from_bool(ctx, &unwrap_int(ctx, a).le(&unwrap_int(ctx, b))), - ) -} - -/// Plus operation for Nullable(Int) type. -/// The table below shows the result of `plus_int`: -/// -/// | a | b | result | -/// |---|---|--------| -/// | NULL | NULL | NULL | -/// | NULL | 1 | NULL | -/// | 1 | NULL | NULL | -/// | 1 | 1 | 2 | -pub fn plus_int<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>, b: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); - debug_assert!(b.get_sort() == nullable_int_sort(ctx).sort); - - // IF(a IS NULL OR b IS NULL, NULL, a + b) - Bool::or(ctx, &[&is_null_int(ctx, a), &is_null_int(ctx, b)]).ite( - &null_int(ctx), - &from_int(ctx, &unwrap_int(ctx, a).add(unwrap_int(ctx, b))), - ) -} - -/// Minus operation for Nullable(Int) type. -/// The table below shows the result of `minus_int`: -/// -/// | a | b | result | -/// |---|---|--------| -/// | NULL | NULL | NULL | -/// | NULL | 1 | NULL | -/// | 1 | NULL | NULL | -/// | 1 | 1 | 0 | -pub fn minus_int<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>, b: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); - debug_assert!(b.get_sort() == nullable_int_sort(ctx).sort); - - // IF(a IS NULL OR b IS NULL, NULL, a - b) - Bool::or(ctx, &[&is_null_int(ctx, a), &is_null_int(ctx, b)]).ite( - &null_int(ctx), - &from_int(ctx, &unwrap_int(ctx, a).sub(unwrap_int(ctx, b))), - ) -} - -/// Multiply operation for Nullable(Int) type. -/// The table below shows the result of `multiply_int`: -/// -/// | a | b | result | -/// |---|---|--------| -/// | NULL | NULL | NULL | -/// | NULL | 1 | NULL | -/// | 1 | NULL | NULL | -/// | 2 | 2 | 4 | -pub fn multiply_int<'ctx>( - ctx: &'ctx Context, - a: &Dynamic<'ctx>, - b: &Dynamic<'ctx>, -) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); - debug_assert!(b.get_sort() == nullable_int_sort(ctx).sort); - - // IF(a IS NULL OR b IS NULL, NULL, a * b) - Bool::or(ctx, &[&is_null_int(ctx, a), &is_null_int(ctx, b)]).ite( - &null_int(ctx), - &from_int(ctx, &unwrap_int(ctx, a).mul(unwrap_int(ctx, b))), - ) -} - -/// Minus operation for Nullable(Int) type. -/// The table below shows the result of `minus_int`: -/// -/// | a | result | -/// |---|--------| -/// | NULL | NULL | -/// | 1 | -1 | -pub fn unary_minus_int<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); - - // IF(a IS NULL, NULL, -a) - is_null_int(ctx, a).ite( - &null_int(ctx), - &from_int(ctx, &unwrap_int(ctx, a).unary_minus()), - ) -} - -/// Logical AND operation for Nullable Boolean type. -/// The table below shows the result of `and_bool`: -/// -/// | a | b | result | -/// |---|---|--------| -/// | NULL | NULL | NULL | -/// | NULL | TRUE | NULL | -/// | NULL | FALSE | FALSE | -/// | TRUE | NULL | NULL | -/// | TRUE | TRUE | TRUE | -/// | TRUE | FALSE | FALSE | -/// | FALSE | NULL | FALSE | -/// | FALSE | TRUE | FALSE | -/// | FALSE | FALSE | FALSE | -pub fn and_bool<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>, b: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_bool_sort(ctx).sort); - debug_assert!(b.get_sort() == nullable_bool_sort(ctx).sort); - - // IF(is_false(a) OR is_false(b), FALSE, IF(a IS NULL OR b IS NULL, NULL, TRUE)) - Bool::or(ctx, &[&is_false(ctx, a), &is_false(ctx, b)]).ite( - &false_bool(ctx), - &Bool::or(ctx, &[&is_null_bool(ctx, a), &is_null_bool(ctx, b)]) - .ite(&null_bool(ctx), &true_bool(ctx)), - ) -} - -/// Logical OR operation for Nullable Boolean type. -/// The table below shows the result of `or_bool`: -/// -/// | a | b | result | -/// |---|---|--------| -/// | NULL | NULL | NULL | -/// | NULL | TRUE | TRUE | -/// | NULL | FALSE | NULL | -/// | TRUE | NULL | TRUE | -/// | TRUE | TRUE | TRUE | -/// | TRUE | FALSE | TRUE | -/// | FALSE | NULL | NULL | -/// | FALSE | TRUE | TRUE | -/// | FALSE | FALSE | FALSE | -pub fn or_bool<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>, b: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_bool_sort(ctx).sort); - debug_assert!(b.get_sort() == nullable_bool_sort(ctx).sort); - - // IF(is_true(a) OR is_true(b), TRUE, IF(a IS NULL OR b IS NULL, NULL, FALSE)) - Bool::or(ctx, &[&is_true(ctx, a), &is_true(ctx, b)]).ite( - &true_bool(ctx), - &Bool::or(ctx, &[&is_null_bool(ctx, a), &is_null_bool(ctx, b)]) - .ite(&null_bool(ctx), &false_bool(ctx)), - ) -} - -/// Equality check for Nullable Boolean type. -/// The table below shows the result of `eq_bool`: -/// -/// | a | b | result | -/// |---|---|--------| -/// | NULL | NULL | NULL | -/// | NULL | TRUE | NULL | -/// | NULL | FALSE | NULL | -/// | TRUE | NULL | NULL | -/// | TRUE | TRUE | TRUE | -/// | TRUE | FALSE | FALSE | -/// | FALSE | NULL | NULL | -/// | FALSE | TRUE | FALSE | -/// | FALSE | FALSE | TRUE | -pub fn eq_bool<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>, b: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_bool_sort(ctx).sort); - debug_assert!(b.get_sort() == nullable_bool_sort(ctx).sort); - - // IF(a IS NULL OR b IS NULL, NULL, a = b) - Bool::or(ctx, &[&is_null_bool(ctx, a), &is_null_bool(ctx, b)]) - .ite(&null_bool(ctx), &from_bool(ctx, &a._eq(b))) -} - -/// Logical NOT operation for Nullable Boolean type. -/// The table below shows the result of `not_bool`: -/// -/// | a | result | -/// |---|--------| -/// | NULL | NULL | -/// | TRUE | FALSE | -/// | FALSE | TRUE | -pub fn not_bool<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>) -> Dynamic<'ctx> { - debug_assert!(a.get_sort() == nullable_bool_sort(ctx).sort); - - // IF(a IS NULL, NULL, NOT a) - is_null_bool(ctx, a).ite( - &null_bool(ctx), - &is_true(ctx, a).ite(&false_bool(ctx), &true_bool(ctx)), - ) -} - -pub fn is_null_bool<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>) -> Bool<'ctx> { - debug_assert!(a.get_sort() == nullable_bool_sort(ctx).sort); - - a._eq(&null_bool(ctx)) -} - -pub fn is_null_int<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>) -> Bool<'ctx> { - debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); - - a._eq(&null_int(ctx)) -} - -pub fn unwrap_int<'ctx>(ctx: &'ctx Context, a: &Dynamic<'ctx>) -> Int<'ctx> { - debug_assert!(a.get_sort() == nullable_int_sort(ctx).sort); - - nullable_int_sort(ctx).variants[1].accessors[0] - .apply(&[a]) - .as_int() - .unwrap() -} diff --git a/src/query/constraint/src/lib.rs b/src/query/constraint/src/lib.rs deleted file mode 100644 index 7b95d57b0f43..000000000000 --- a/src/query/constraint/src/lib.rs +++ /dev/null @@ -1,18 +0,0 @@ -// Copyright 2021 Datafuse Labs -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -pub mod declare; -pub mod mir; -pub mod problem; -pub mod simplify; diff --git a/src/query/constraint/src/mir.rs b/src/query/constraint/src/mir.rs deleted file mode 100644 index bbacab71c869..000000000000 --- a/src/query/constraint/src/mir.rs +++ /dev/null @@ -1,392 +0,0 @@ -// Copyright 2021 Datafuse Labs -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -use std::collections::HashMap; - -use z3::ast::Ast; -use z3::ast::Dynamic; -use z3::Context; -use z3::DeclKind; - -use crate::declare::*; - -#[derive(Debug, Clone, PartialEq, Eq)] -pub enum MirExpr { - Constant(MirConstant), - Variable { - name: String, - data_type: MirDataType, - }, - UnaryOperator { - op: MirUnaryOperator, - arg: Box, - }, - BinaryOperator { - op: MirBinaryOperator, - left: Box, - right: Box, - }, -} - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum MirConstant { - Bool(bool), - Int(i64), - Null, -} - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum MirDataType { - Bool, - Int, -} - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum MirUnaryOperator { - Minus, - Not, - IsNull, - RemoveNullable, -} - -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -pub enum MirBinaryOperator { - Plus, - Minus, - Multiply, - And, - Or, - Eq, - Lt, - Lte, - Gt, - Gte, -} - -#[derive(Debug, Clone, Copy)] -pub struct WrongType; - -impl MirExpr { - pub fn variables(&self) -> HashMap { - fn walk(expr: &MirExpr, buf: &mut HashMap) { - match expr { - MirExpr::Constant { .. } => {} - MirExpr::Variable { name, data_type } => { - buf.insert(name.clone(), *data_type); - } - MirExpr::UnaryOperator { arg, .. } => { - walk(arg, buf); - } - MirExpr::BinaryOperator { left, right, .. } => { - walk(left, buf); - walk(right, buf); - } - } - } - - let mut buf = HashMap::new(); - walk(self, &mut buf); - buf - } - - pub fn as_z3_ast<'ctx>( - &self, - ctx: &'ctx Context, - required_type: MirDataType, - ) -> Result, WrongType> { - let (ast, ty) = match self { - MirExpr::Constant(c) => match c { - MirConstant::Bool(x) => Ok((const_bool(ctx, *x), MirDataType::Bool)), - MirConstant::Int(x) => Ok((const_int(ctx, *x), MirDataType::Int)), - MirConstant::Null => match required_type { - MirDataType::Bool => Ok((null_bool(ctx), MirDataType::Bool)), - MirDataType::Int => Ok((null_int(ctx), MirDataType::Int)), - }, - }, - MirExpr::Variable { name, data_type } => match data_type { - MirDataType::Bool => Ok((var_bool(ctx, name), MirDataType::Bool)), - MirDataType::Int => Ok((var_int(ctx, name), MirDataType::Int)), - }, - MirExpr::UnaryOperator { op, arg } => match op { - MirUnaryOperator::Minus => Ok(( - unary_minus_int(ctx, &arg.as_z3_ast(ctx, MirDataType::Int)?), - MirDataType::Int, - )), - MirUnaryOperator::Not => Ok(( - not_bool(ctx, &arg.as_z3_ast(ctx, MirDataType::Bool)?), - MirDataType::Bool, - )), - MirUnaryOperator::IsNull => match arg.as_z3_ast(ctx, MirDataType::Bool) { - Ok(arg) => Ok((from_bool(ctx, &is_null_bool(ctx, &arg)), MirDataType::Bool)), - Err(_) => match arg.as_z3_ast(ctx, MirDataType::Int) { - Ok(arg) => Ok((from_bool(ctx, &is_null_int(ctx, &arg)), MirDataType::Bool)), - Err(_) => Err(WrongType), - }, - }, - MirUnaryOperator::RemoveNullable => unreachable!( - "RemoveNullable is a hint returned by the solver, \ - therefore it should not be used as an input" - ), - }, - MirExpr::BinaryOperator { op, left, right } => match op { - MirBinaryOperator::Plus => Ok(( - plus_int( - ctx, - &left.as_z3_ast(ctx, MirDataType::Int)?, - &right.as_z3_ast(ctx, MirDataType::Int)?, - ), - MirDataType::Int, - )), - MirBinaryOperator::Minus => Ok(( - minus_int( - ctx, - &left.as_z3_ast(ctx, MirDataType::Int)?, - &right.as_z3_ast(ctx, MirDataType::Int)?, - ), - MirDataType::Int, - )), - MirBinaryOperator::Multiply => Ok(( - multiply_int( - ctx, - &left.as_z3_ast(ctx, MirDataType::Int)?, - &right.as_z3_ast(ctx, MirDataType::Int)?, - ), - MirDataType::Int, - )), - MirBinaryOperator::And => Ok(( - and_bool( - ctx, - &left.as_z3_ast(ctx, MirDataType::Bool)?, - &right.as_z3_ast(ctx, MirDataType::Bool)?, - ), - MirDataType::Bool, - )), - MirBinaryOperator::Or => Ok(( - or_bool( - ctx, - &left.as_z3_ast(ctx, MirDataType::Bool)?, - &right.as_z3_ast(ctx, MirDataType::Bool)?, - ), - MirDataType::Bool, - )), - MirBinaryOperator::Lt => Ok(( - lt_int( - ctx, - &left.as_z3_ast(ctx, MirDataType::Int)?, - &right.as_z3_ast(ctx, MirDataType::Int)?, - ), - MirDataType::Bool, - )), - MirBinaryOperator::Lte => Ok(( - le_int( - ctx, - &left.as_z3_ast(ctx, MirDataType::Int)?, - &right.as_z3_ast(ctx, MirDataType::Int)?, - ), - MirDataType::Bool, - )), - MirBinaryOperator::Gt => Ok(( - gt_int( - ctx, - &left.as_z3_ast(ctx, MirDataType::Int)?, - &right.as_z3_ast(ctx, MirDataType::Int)?, - ), - MirDataType::Bool, - )), - MirBinaryOperator::Gte => Ok(( - ge_int( - ctx, - &left.as_z3_ast(ctx, MirDataType::Int)?, - &right.as_z3_ast(ctx, MirDataType::Int)?, - ), - MirDataType::Bool, - )), - MirBinaryOperator::Eq => match ( - left.as_z3_ast(ctx, MirDataType::Bool), - right.as_z3_ast(ctx, MirDataType::Bool), - ) { - (Ok(left), Ok(right)) => Ok((eq_bool(ctx, &left, &right), MirDataType::Bool)), - _ => match ( - left.as_z3_ast(ctx, MirDataType::Int), - right.as_z3_ast(ctx, MirDataType::Int), - ) { - (Ok(left), Ok(right)) => { - Ok((eq_int(ctx, &left, &right), MirDataType::Bool)) - } - _ => Err(WrongType), - }, - }, - }, - }?; - - if ty != required_type { - return Err(WrongType); - } - - Ok(ast) - } - - pub fn from_z3_ast(ast: &Dynamic, variables: &HashMap) -> Option { - let decl = ast.safe_decl().ok()?; - match (decl.kind(), decl.name().as_str()) { - (DeclKind::DT_CONSTRUCTOR, "TRUE_BOOL") | (DeclKind::TRUE, _) => { - Some(MirExpr::Constant(MirConstant::Bool(true))) - } - (DeclKind::DT_CONSTRUCTOR, "FALSE_BOOL") | (DeclKind::FALSE, _) => { - Some(MirExpr::Constant(MirConstant::Bool(false))) - } - (DeclKind::DT_CONSTRUCTOR, "NULL_BOOL") => Some(MirExpr::Constant(MirConstant::Null)), - (DeclKind::DT_CONSTRUCTOR, "NULL_INT") => Some(MirExpr::Constant(MirConstant::Null)), - (DeclKind::DT_CONSTRUCTOR, "JUST_INT") => { - Self::from_z3_ast(&ast.children()[0], variables) - } - (DeclKind::AND, _) => Some(MirExpr::BinaryOperator { - op: MirBinaryOperator::And, - left: Box::new(Self::from_z3_ast(&ast.children()[0], variables)?), - right: Box::new(Self::from_z3_ast(&ast.children()[1], variables)?), - }), - (DeclKind::OR, _) => Some(MirExpr::BinaryOperator { - op: MirBinaryOperator::Or, - left: Box::new(Self::from_z3_ast(&ast.children()[0], variables)?), - right: Box::new(Self::from_z3_ast(&ast.children()[1], variables)?), - }), - (DeclKind::NOT, _) => { - let arg = Self::from_z3_ast(&ast.children()[0], variables)?; - match arg.clone() { - MirExpr::BinaryOperator { op, left, right } => { - let op = match op { - MirBinaryOperator::Gt => MirBinaryOperator::Lte, - MirBinaryOperator::Gte => MirBinaryOperator::Lt, - MirBinaryOperator::Lt => MirBinaryOperator::Gte, - MirBinaryOperator::Lte => MirBinaryOperator::Gt, - _ => { - return Some(MirExpr::UnaryOperator { - op: MirUnaryOperator::Not, - arg: Box::new(arg), - }); - } - }; - Some(MirExpr::BinaryOperator { op, left, right }) - } - _ => Some(MirExpr::UnaryOperator { - op: MirUnaryOperator::Not, - arg: Box::new(arg), - }), - } - } - (DeclKind::GT, _) => Some(MirExpr::BinaryOperator { - op: MirBinaryOperator::Gt, - left: Box::new(Self::from_z3_ast(&ast.children()[0], variables)?), - right: Box::new(Self::from_z3_ast(&ast.children()[1], variables)?), - }), - (DeclKind::GE, _) => Some(MirExpr::BinaryOperator { - op: MirBinaryOperator::Gte, - left: Box::new(Self::from_z3_ast(&ast.children()[0], variables)?), - right: Box::new(Self::from_z3_ast(&ast.children()[1], variables)?), - }), - (DeclKind::LT, _) => Some(MirExpr::BinaryOperator { - op: MirBinaryOperator::Lt, - left: Box::new(Self::from_z3_ast(&ast.children()[0], variables)?), - right: Box::new(Self::from_z3_ast(&ast.children()[1], variables)?), - }), - (DeclKind::LE, _) => Some(MirExpr::BinaryOperator { - op: MirBinaryOperator::Lte, - left: Box::new(Self::from_z3_ast(&ast.children()[0], variables)?), - right: Box::new(Self::from_z3_ast(&ast.children()[1], variables)?), - }), - (DeclKind::ADD, _) => { - let left = Self::from_z3_ast(&ast.children()[0], variables)?; - let right = Self::from_z3_ast(&ast.children()[1], variables)?; - match right { - MirExpr::UnaryOperator { - op: MirUnaryOperator::Minus, - arg, - } => Some(MirExpr::BinaryOperator { - op: MirBinaryOperator::Minus, - left: Box::new(left), - right: arg, - }), - _ => Some(MirExpr::BinaryOperator { - op: MirBinaryOperator::Plus, - left: Box::new(Self::from_z3_ast(&ast.children()[0], variables)?), - right: Box::new(Self::from_z3_ast(&ast.children()[1], variables)?), - }), - } - } - (DeclKind::SUB, _) => Some(MirExpr::BinaryOperator { - op: MirBinaryOperator::Minus, - left: Box::new(Self::from_z3_ast(&ast.children()[0], variables)?), - right: Box::new(Self::from_z3_ast(&ast.children()[1], variables)?), - }), - (DeclKind::UMINUS, _) => { - let arg = Self::from_z3_ast(&ast.children()[0], variables)?; - match arg { - MirExpr::Constant(MirConstant::Int(x)) => { - Some(MirExpr::Constant(MirConstant::Int(-x))) - } - _ => Some(MirExpr::UnaryOperator { - op: MirUnaryOperator::Minus, - arg: Box::new(arg), - }), - } - } - (DeclKind::MUL, _) => { - let left = Self::from_z3_ast(&ast.children()[0], variables)?; - let right = Self::from_z3_ast(&ast.children()[1], variables)?; - match left { - MirExpr::Constant(MirConstant::Int(1)) => Some(right), - MirExpr::Constant(MirConstant::Int(-1)) => Some(MirExpr::UnaryOperator { - op: MirUnaryOperator::Minus, - arg: Box::new(right), - }), - _ => Some(MirExpr::BinaryOperator { - op: MirBinaryOperator::Multiply, - left: Box::new(left), - right: Box::new(right), - }), - } - } - (DeclKind::EQ, _) => { - let left = Self::from_z3_ast(&ast.children()[0], variables)?; - let right = Self::from_z3_ast(&ast.children()[1], variables)?; - match (left, right) { - (MirExpr::Constant(MirConstant::Null), other) - | (other, MirExpr::Constant(MirConstant::Null)) => { - Some(MirExpr::UnaryOperator { - op: MirUnaryOperator::IsNull, - arg: Box::new(other), - }) - } - (left, right) => Some(MirExpr::BinaryOperator { - op: MirBinaryOperator::Eq, - left: Box::new(left), - right: Box::new(right), - }), - } - } - (DeclKind::ANUM, _) => Some(MirExpr::Constant(MirConstant::Int( - ast.as_int().unwrap().as_i64()?, - ))), - (DeclKind::DT_ACCESSOR, "unwrap-int") => Some(MirExpr::UnaryOperator { - op: MirUnaryOperator::RemoveNullable, - arg: Box::new(Self::from_z3_ast(&ast.children()[0], variables)?), - }), - (DeclKind::UNINTERPRETED, name) => Some(MirExpr::Variable { - name: name.to_string(), - data_type: variables[name], - }), - _ => None, - } - } -} diff --git a/src/query/constraint/src/problem.rs b/src/query/constraint/src/problem.rs deleted file mode 100644 index db9e93a6b673..000000000000 --- a/src/query/constraint/src/problem.rs +++ /dev/null @@ -1,104 +0,0 @@ -// Copyright 2021 Datafuse Labs -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -use z3::ast::forall_const; -use z3::ast::Ast; -use z3::Config; -use z3::Context; -use z3::SatResult; -use z3::Solver; - -use crate::declare::is_true; -use crate::declare::var_bool; -use crate::declare::var_int; -use crate::mir::MirDataType; -use crate::mir::MirExpr; -use crate::mir::MirUnaryOperator; - -/// Given the assertions are true, try to prove that a certain variable mut be not null. -/// -/// Basically, this function tries to prove the following proposition: -/// -/// ∀x. assertion(x) -> x is not null -/// -/// ``` -/// use databend_common_constraint::mir::*; -/// use databend_common_constraint::problem::variable_must_not_null; -/// -/// // a > 0 -/// let assertion = MirExpr::BinaryOperator { -/// op: MirBinaryOperator::Gt, -/// left: Box::new(MirExpr::Variable { -/// name: "a".to_string(), -/// data_type: MirDataType::Int, -/// }), -/// right: Box::new(MirExpr::Constant(MirConstant::Int(0))), -/// }; -/// -/// // a > 0 => a is not null -/// assert!(variable_must_not_null(&assertion, "a")); -/// ``` -pub fn variable_must_not_null(assertion: &MirExpr, variable: &str) -> bool { - let ctx = &Context::new(&Config::new()); - - let variables = assertion.variables(); - let for_all_free_vars = variables - .iter() - .map(|(name, data_type)| match data_type { - MirDataType::Bool => var_bool(ctx, name), - MirDataType::Int => var_int(ctx, name), - }) - .collect::>(); - - let assertion = if let Ok(assertion) = assertion.as_z3_ast(ctx, MirDataType::Bool) { - is_true(ctx, &assertion) - } else { - return false; - }; - - let variable_is_not_null = MirExpr::UnaryOperator { - op: MirUnaryOperator::Not, - arg: Box::new(MirExpr::UnaryOperator { - op: MirUnaryOperator::IsNull, - arg: Box::new(MirExpr::Variable { - name: variable.to_string(), - data_type: variables[variable], - }), - }), - }; - let variable_is_not_null = - if let Ok(variable_is_not_null) = variable_is_not_null.as_z3_ast(ctx, MirDataType::Bool) { - is_true(ctx, &variable_is_not_null) - } else { - return false; - }; - - let p = forall_const( - ctx, - for_all_free_vars - .iter() - .map(|v| v as &dyn Ast) - .collect::>() - .as_slice(), - &[], - &assertion.implies(&variable_is_not_null), - ); - - let solver = Solver::new(ctx); - solver.push(); - solver.assert(&p); - let result = solver.check(); - - result == SatResult::Sat -} diff --git a/src/query/constraint/src/simplify.rs b/src/query/constraint/src/simplify.rs deleted file mode 100644 index eddec326ed6f..000000000000 --- a/src/query/constraint/src/simplify.rs +++ /dev/null @@ -1,60 +0,0 @@ -// Copyright 2021 Datafuse Labs -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -use z3::ast::Bool; -use z3::ast::Dynamic; -use z3::Config; -use z3::Context; -use z3::Goal; -use z3::Tactic; - -use crate::declare::is_true; -use crate::mir::MirDataType; -use crate::mir::MirExpr; - -pub fn simplify(expr: &MirExpr) -> Option> { - let ctx = &Context::new(&Config::new()); - let variables = expr.variables(); - let ast = mir_to_z3_assertion(ctx, expr)?; - let simplified = simplify_z3_ast(ctx, &ast)?; - simplified - .iter() - .map(|formula| MirExpr::from_z3_ast(formula, &variables)) - .collect() -} - -pub fn mir_to_z3_assertion<'ctx>(ctx: &'ctx Context, expr: &MirExpr) -> Option> { - Some(is_true(ctx, &expr.as_z3_ast(ctx, MirDataType::Bool).ok()?)) -} - -pub fn simplify_z3_ast<'ctx>(ctx: &'ctx Context, ast: &Bool<'ctx>) -> Option>> { - let goal = Goal::new(ctx, false, false, false); - goal.assert(ast); - - let formulas = Tactic::repeat( - ctx, - &Tactic::new(ctx, "simplify") - .and_then(&Tactic::new(ctx, "ctx-solver-simplify")) - .and_then(&Tactic::new(ctx, "propagate-values")) - .and_then(&Tactic::new(ctx, "propagate-ineqs")), - 5, - ) - .apply(&goal, None) - .ok()? - .list_subgoals() - .next()? - .get_formulas::(); - - Some(formulas) -} diff --git a/src/query/constraint/tests/it/declare.rs b/src/query/constraint/tests/it/declare.rs deleted file mode 100644 index ad56028f5d3f..000000000000 --- a/src/query/constraint/tests/it/declare.rs +++ /dev/null @@ -1,446 +0,0 @@ -// Copyright 2023 Datafuse Labs. -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -use databend_common_constraint::declare::*; -use z3::Config; -use z3::Context; -use z3::SatResult; -use z3::Solver; - -#[test] -fn test_bool_is_true() { - // Test is_true function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - // is_true(TRUE) => true - solver.assert(&is_true(ctx, &true_bool(ctx))); - // is_true(FALSE) => false - solver.assert(&is_true(ctx, &false_bool(ctx)).not()); - // is_true(NULL) => false - solver.assert(&is_true(ctx, &null_bool(ctx)).not()); - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_bool_logical_and() { - // Test logical AND function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - // TRUE AND TRUE => TRUE - solver.assert(&is_true( - ctx, - &and_bool(ctx, &true_bool(ctx), &true_bool(ctx)), - )); - // TRUE AND FALSE => FALSE - solver.assert(&is_true(ctx, &and_bool(ctx, &true_bool(ctx), &false_bool(ctx))).not()); - // FALSE AND TRUE => FALSE - solver.assert(&is_true(ctx, &and_bool(ctx, &false_bool(ctx), &true_bool(ctx))).not()); - // TRUE AND NULL => NULL - solver.assert(&is_null_bool( - ctx, - &and_bool(ctx, &true_bool(ctx), &null_bool(ctx)), - )); - // NULL AND TRUE => NULL - solver.assert(&is_null_bool( - ctx, - &and_bool(ctx, &null_bool(ctx), &true_bool(ctx)), - )); - // FALSE AND FALSE => FALSE - solver.assert(&is_true(ctx, &and_bool(ctx, &false_bool(ctx), &false_bool(ctx))).not()); - // FALSE AND NULL => FALSE - solver.assert(&is_true(ctx, &and_bool(ctx, &false_bool(ctx), &null_bool(ctx))).not()); - // NULL AND FALSE => FALSE - solver.assert(&is_true(ctx, &and_bool(ctx, &null_bool(ctx), &false_bool(ctx))).not()); - // NULL AND NULL => NULL - solver.assert(&is_null_bool( - ctx, - &and_bool(ctx, &null_bool(ctx), &null_bool(ctx)), - )); - - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_bool_logical_or() { - // Test logical OR function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - // TRUE OR TRUE => TRUE - solver.assert(&is_true( - ctx, - &or_bool(ctx, &true_bool(ctx), &true_bool(ctx)), - )); - // TRUE OR FALSE => TRUE - solver.assert(&is_true( - ctx, - &or_bool(ctx, &true_bool(ctx), &false_bool(ctx)), - )); - // FALSE OR TRUE => TRUE - solver.assert(&is_true( - ctx, - &or_bool(ctx, &false_bool(ctx), &true_bool(ctx)), - )); - // TRUE OR NULL => TRUE - solver.assert(&is_true( - ctx, - &or_bool(ctx, &true_bool(ctx), &null_bool(ctx)), - )); - // NULL OR TRUE => TRUE - solver.assert(&is_true( - ctx, - &or_bool(ctx, &null_bool(ctx), &true_bool(ctx)), - )); - // FALSE OR FALSE => FALSE - solver.assert(&is_true(ctx, &or_bool(ctx, &false_bool(ctx), &false_bool(ctx))).not()); - // FALSE OR NULL => NULL - solver.assert(&is_null_bool( - ctx, - &or_bool(ctx, &false_bool(ctx), &null_bool(ctx)), - )); - // NULL OR FALSE => NULL - solver.assert(&is_null_bool( - ctx, - &or_bool(ctx, &null_bool(ctx), &false_bool(ctx)), - )); - // NULL OR NULL => NULL - solver.assert(&is_null_bool( - ctx, - &or_bool(ctx, &null_bool(ctx), &null_bool(ctx)), - )); - - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_bool_logical_not() { - // Test logical NOT function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - // NOT TRUE => FALSE - solver.assert(&is_true(ctx, ¬_bool(ctx, &true_bool(ctx))).not()); - // NOT FALSE => TRUE - solver.assert(&is_true(ctx, ¬_bool(ctx, &false_bool(ctx)))); - // NOT NULL => NULL - solver.assert(&is_null_bool(ctx, ¬_bool(ctx, &null_bool(ctx)))); - - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_int_eq() { - // Test int equality function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - // 1 == 1 => TRUE - solver.assert(&is_true( - ctx, - &eq_int(ctx, &const_int(ctx, 1), &const_int(ctx, 1)), - )); - // 1 == 2 => FALSE - solver.assert(&is_true(ctx, &eq_int(ctx, &const_int(ctx, 1), &const_int(ctx, 2))).not()); - // 1 == NULL => NULL - solver.assert(&is_null_bool( - ctx, - &eq_int(ctx, &const_int(ctx, 1), &null_int(ctx)), - )); - // NULL == 1 => NULL - solver.assert(&is_null_bool( - ctx, - &eq_int(ctx, &null_int(ctx), &const_int(ctx, 1)), - )); - // NULL == NULL => NULL - solver.assert(&is_null_bool( - ctx, - &eq_int(ctx, &null_int(ctx), &null_int(ctx)), - )); - - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_int_lt() { - // Test int less than function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - // 1 < 2 => TRUE - solver.assert(&is_true( - ctx, - <_int(ctx, &const_int(ctx, 1), &const_int(ctx, 2)), - )); - // 2 < 1 => FALSE - solver.assert(&is_true(ctx, <_int(ctx, &const_int(ctx, 2), &const_int(ctx, 1))).not()); - // 1 < NULL => NULL - solver.assert(&is_null_bool( - ctx, - <_int(ctx, &const_int(ctx, 1), &null_int(ctx)), - )); - // NULL < 1 => NULL - solver.assert(&is_null_bool( - ctx, - <_int(ctx, &null_int(ctx), &const_int(ctx, 1)), - )); - // NULL < NULL => NULL - solver.assert(&is_null_bool( - ctx, - <_int(ctx, &null_int(ctx), &null_int(ctx)), - )); - - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_int_le() { - // Test int less than or equal function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - // 1 <= 2 => TRUE - solver.assert(&is_true( - ctx, - &le_int(ctx, &const_int(ctx, 1), &const_int(ctx, 2)), - )); - // 2 <= 1 => FALSE - solver.assert(&is_true(ctx, &le_int(ctx, &const_int(ctx, 2), &const_int(ctx, 1))).not()); - // 1 <= 1 => TRUE - solver.assert(&is_true( - ctx, - &le_int(ctx, &const_int(ctx, 1), &const_int(ctx, 1)), - )); - // 1 <= NULL => NULL - solver.assert(&is_null_bool( - ctx, - &le_int(ctx, &const_int(ctx, 1), &null_int(ctx)), - )); - // NULL <= 1 => NULL - solver.assert(&is_null_bool( - ctx, - &le_int(ctx, &null_int(ctx), &const_int(ctx, 1)), - )); - // NULL <= NULL => NULL - solver.assert(&is_null_bool( - ctx, - &le_int(ctx, &null_int(ctx), &null_int(ctx)), - )); - - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_int_gt() { - // Test int greater than function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - // 2 > 1 => TRUE - solver.assert(&is_true( - ctx, - >_int(ctx, &const_int(ctx, 2), &const_int(ctx, 1)), - )); - // 1 > 2 => FALSE - solver.assert(&is_true(ctx, >_int(ctx, &const_int(ctx, 1), &const_int(ctx, 2))).not()); - // 1 > NULL => NULL - solver.assert(&is_null_bool( - ctx, - >_int(ctx, &const_int(ctx, 1), &null_int(ctx)), - )); - // NULL > 1 => NULL - solver.assert(&is_null_bool( - ctx, - >_int(ctx, &null_int(ctx), &const_int(ctx, 1)), - )); - // NULL > NULL => NULL - solver.assert(&is_null_bool( - ctx, - >_int(ctx, &null_int(ctx), &null_int(ctx)), - )); - - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_int_ge() { - // Test int greater than or equal function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - // 2 >= 1 => TRUE - solver.assert(&is_true( - ctx, - &ge_int(ctx, &const_int(ctx, 2), &const_int(ctx, 1)), - )); - // 1 >= 2 => FALSE - solver.assert(&is_true(ctx, &ge_int(ctx, &const_int(ctx, 1), &const_int(ctx, 2))).not()); - // 1 >= 1 => TRUE - solver.assert(&is_true( - ctx, - &ge_int(ctx, &const_int(ctx, 1), &const_int(ctx, 1)), - )); - // 1 >= NULL => NULL - solver.assert(&is_null_bool( - ctx, - &ge_int(ctx, &const_int(ctx, 1), &null_int(ctx)), - )); - // NULL >= 1 => NULL - solver.assert(&is_null_bool( - ctx, - &ge_int(ctx, &null_int(ctx), &const_int(ctx, 1)), - )); - // NULL >= NULL => NULL - solver.assert(&is_null_bool( - ctx, - &ge_int(ctx, &null_int(ctx), &null_int(ctx)), - )); - - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_int_plus() { - // Test int plus function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - // 1 + 2 = 3 => TRUE - solver.assert(&is_true( - ctx, - &eq_int( - ctx, - &plus_int(ctx, &const_int(ctx, 1), &const_int(ctx, 2)), - &const_int(ctx, 3), - ), - )); - // 1 + NULL = 3 => NULL - solver.assert(&is_null_bool( - ctx, - &eq_int( - ctx, - &plus_int(ctx, &const_int(ctx, 1), &null_int(ctx)), - &const_int(ctx, 3), - ), - )); - // NULL + 1 = 3 => NULL - solver.assert(&is_null_bool( - ctx, - &eq_int( - ctx, - &plus_int(ctx, &null_int(ctx), &const_int(ctx, 1)), - &const_int(ctx, 3), - ), - )); - // NULL + NULL = 3 => NULL - solver.assert(&is_null_bool( - ctx, - &eq_int( - ctx, - &plus_int(ctx, &null_int(ctx), &null_int(ctx)), - &const_int(ctx, 3), - ), - )); - - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_int_minus() { - // Test int minus function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - // 3 - 2 = 1 => TRUE - solver.assert(&is_true( - ctx, - &eq_int( - ctx, - &minus_int(ctx, &const_int(ctx, 3), &const_int(ctx, 2)), - &const_int(ctx, 1), - ), - )); - // 1 - NULL = 3 => NULL - solver.assert(&is_null_bool( - ctx, - &eq_int( - ctx, - &minus_int(ctx, &const_int(ctx, 1), &null_int(ctx)), - &const_int(ctx, 3), - ), - )); - // NULL - 1 = 3 => NULL - solver.assert(&is_null_bool( - ctx, - &eq_int( - ctx, - &minus_int(ctx, &null_int(ctx), &const_int(ctx, 1)), - &const_int(ctx, 3), - ), - )); - // NULL - NULL = 3 => NULL - solver.assert(&is_null_bool( - ctx, - &eq_int( - ctx, - &minus_int(ctx, &null_int(ctx), &null_int(ctx)), - &const_int(ctx, 3), - ), - )); - - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_int_unary_minus() { - // Test int minus function - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - // - 0 => 0 - solver.assert(&is_true( - ctx, - &eq_int( - ctx, - &unary_minus_int(ctx, &const_int(ctx, 0)), - &const_int(ctx, 0), - ), - )); - // - 2 => -2 - solver.assert(&is_true( - ctx, - &eq_int( - ctx, - &unary_minus_int(ctx, &const_int(ctx, 2)), - &const_int(ctx, -2), - ), - )); - // - NULL => NULL - solver.assert(&is_null_int(ctx, &unary_minus_int(ctx, &null_int(ctx)))); - - assert_eq!(solver.check(), SatResult::Sat); -} - -#[test] -fn test_int_nullability() { - // Test int nullability - let ctx = &Context::new(&Config::new()); - let solver = Solver::new(ctx); - - let int = const_int(ctx, 1); - solver.assert(&is_null_int(ctx, &int).not()); - solver.assert(&is_null_int(ctx, &null_int(ctx))); - - assert_eq!(solver.check(), SatResult::Sat); -} diff --git a/src/query/constraint/tests/it/main.rs b/src/query/constraint/tests/it/main.rs deleted file mode 100644 index c5230733c012..000000000000 --- a/src/query/constraint/tests/it/main.rs +++ /dev/null @@ -1,20 +0,0 @@ -// Copyright 2023 Datafuse Labs. -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -#![feature(try_blocks)] - -mod declare; -mod parser; -mod problem; -mod simplify; diff --git a/src/query/constraint/tests/it/parser.rs b/src/query/constraint/tests/it/parser.rs deleted file mode 100644 index 41ccc9225136..000000000000 --- a/src/query/constraint/tests/it/parser.rs +++ /dev/null @@ -1,234 +0,0 @@ -// Copyright 2023 Datafuse Labs. -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -use std::collections::HashMap; - -use databend_common_ast::ast::BinaryOperator as ASTBinaryOperator; -use databend_common_ast::ast::ColumnID; -use databend_common_ast::ast::ColumnRef; -use databend_common_ast::ast::Expr as ASTExpr; -use databend_common_ast::ast::FunctionCall; -use databend_common_ast::ast::Identifier; -use databend_common_ast::ast::Literal; -use databend_common_ast::ast::UnaryOperator as ASTUnaryOperator; -use databend_common_ast::parser::parse_expr; -use databend_common_ast::parser::tokenize_sql; -use databend_common_ast::parser::Dialect; -use databend_common_constraint::mir::MirBinaryOperator; -use databend_common_constraint::mir::MirConstant; -use databend_common_constraint::mir::MirDataType; -use databend_common_constraint::mir::MirExpr; -use databend_common_constraint::mir::MirUnaryOperator; - -pub fn parse_mir_expr(text: &str, variables: &HashMap) -> MirExpr { - let tokens = tokenize_sql(text).unwrap(); - let expr = parse_expr(&tokens, Dialect::PostgreSQL).unwrap(); - sql_ast_to_mir(expr, variables).unwrap() -} - -pub fn pretty_mir_expr(expr: &MirExpr) -> String { - let ast = mir_to_sql_ast(expr); - ast.to_string() -} - -fn sql_ast_to_mir(ast: ASTExpr, variables: &HashMap) -> Option { - match ast { - ASTExpr::Literal { value, .. } => { - let constant = match value { - Literal::Boolean(x) => MirConstant::Bool(x), - Literal::UInt64(x) => MirConstant::Int(x as i64), - Literal::Null => MirConstant::Null, - _ => return None, - }; - Some(MirExpr::Constant(constant)) - } - ASTExpr::ColumnRef { - column: - ColumnRef { - database: None, - table: None, - column: - ColumnID::Name(Identifier { - name, quote: None, .. - }), - }, - .. - } => Some(MirExpr::Variable { - data_type: variables[&name], - name, - }), - ASTExpr::IsNull { - expr, not: false, .. - } => Some(MirExpr::UnaryOperator { - op: MirUnaryOperator::IsNull, - arg: Box::new(sql_ast_to_mir(*expr, variables)?), - }), - ASTExpr::IsNull { - expr, not: true, .. - } => Some(MirExpr::UnaryOperator { - op: MirUnaryOperator::Not, - arg: Box::new(MirExpr::UnaryOperator { - op: MirUnaryOperator::IsNull, - arg: Box::new(sql_ast_to_mir(*expr, variables)?), - }), - }), - ASTExpr::BinaryOp { - op, left, right, .. - } => { - let op = match op { - ASTBinaryOperator::Plus => MirBinaryOperator::Plus, - ASTBinaryOperator::Minus => MirBinaryOperator::Minus, - ASTBinaryOperator::Multiply => MirBinaryOperator::Multiply, - ASTBinaryOperator::And => MirBinaryOperator::And, - ASTBinaryOperator::Or => MirBinaryOperator::Or, - ASTBinaryOperator::Eq => MirBinaryOperator::Eq, - ASTBinaryOperator::Lt => MirBinaryOperator::Lt, - ASTBinaryOperator::Lte => MirBinaryOperator::Lte, - ASTBinaryOperator::Gt => MirBinaryOperator::Gt, - ASTBinaryOperator::Gte => MirBinaryOperator::Gte, - ASTBinaryOperator::NotEq => { - return sql_ast_to_mir( - ASTExpr::UnaryOp { - span: None, - op: ASTUnaryOperator::Not, - expr: Box::new(ASTExpr::BinaryOp { - span: None, - op: ASTBinaryOperator::Eq, - left, - right, - }), - }, - variables, - ); - } - _ => return None, - }; - let left = sql_ast_to_mir(*left, variables)?; - let right = sql_ast_to_mir(*right, variables)?; - Some(MirExpr::BinaryOperator { - op, - left: Box::new(left), - right: Box::new(right), - }) - } - ASTExpr::UnaryOp { op, expr, .. } => { - let op = match op { - ASTUnaryOperator::Minus => MirUnaryOperator::Minus, - ASTUnaryOperator::Not => MirUnaryOperator::Not, - _ => return None, - }; - let expr = sql_ast_to_mir(*expr, variables)?; - Some(MirExpr::UnaryOperator { - op, - arg: Box::new(expr), - }) - } - _ => None, - } -} - -fn mir_to_sql_ast(expr: &MirExpr) -> ASTExpr { - match expr { - MirExpr::Constant(constant) => { - let value = match constant { - MirConstant::Bool(x) => Literal::Boolean(*x), - MirConstant::Int(x) if *x >= 0 => Literal::UInt64(*x as u64), - MirConstant::Int(x) => { - return ASTExpr::UnaryOp { - span: None, - op: ASTUnaryOperator::Minus, - expr: Box::new(ASTExpr::Literal { - span: None, - value: Literal::UInt64(x.wrapping_neg() as u64), - }), - }; - } - MirConstant::Null => Literal::Null, - }; - ASTExpr::Literal { span: None, value } - } - MirExpr::Variable { name, .. } => ASTExpr::ColumnRef { - span: None, - column: ColumnRef { - database: None, - table: None, - column: ColumnID::Name(Identifier::from_name(None, name.clone())), - }, - }, - MirExpr::UnaryOperator { op, arg } => { - let op = match op { - MirUnaryOperator::Minus => ASTUnaryOperator::Minus, - MirUnaryOperator::Not => { - if let MirExpr::UnaryOperator { - op: MirUnaryOperator::IsNull, - arg, - } = &**arg - { - return ASTExpr::IsNull { - span: None, - expr: Box::new(mir_to_sql_ast(arg)), - not: true, - }; - }; - ASTUnaryOperator::Not - } - MirUnaryOperator::IsNull => { - return ASTExpr::IsNull { - span: None, - expr: Box::new(mir_to_sql_ast(arg)), - not: false, - }; - } - MirUnaryOperator::RemoveNullable => { - return ASTExpr::FunctionCall { - span: None, - func: FunctionCall { - distinct: false, - name: Identifier::from_name(None, "remove_nullable"), - args: vec![mir_to_sql_ast(arg)], - params: vec![], - window: None, - lambda: None, - }, - }; - } - }; - ASTExpr::UnaryOp { - span: None, - op, - expr: Box::new(mir_to_sql_ast(arg)), - } - } - MirExpr::BinaryOperator { op, left, right } => { - let op = match op { - MirBinaryOperator::Plus => ASTBinaryOperator::Plus, - MirBinaryOperator::Minus => ASTBinaryOperator::Minus, - MirBinaryOperator::Multiply => ASTBinaryOperator::Multiply, - MirBinaryOperator::And => ASTBinaryOperator::And, - MirBinaryOperator::Or => ASTBinaryOperator::Or, - MirBinaryOperator::Eq => ASTBinaryOperator::Eq, - MirBinaryOperator::Lt => ASTBinaryOperator::Lt, - MirBinaryOperator::Lte => ASTBinaryOperator::Lte, - MirBinaryOperator::Gt => ASTBinaryOperator::Gt, - MirBinaryOperator::Gte => ASTBinaryOperator::Gte, - }; - ASTExpr::BinaryOp { - span: None, - op, - left: Box::new(mir_to_sql_ast(left)), - right: Box::new(mir_to_sql_ast(right)), - } - } - } -} diff --git a/src/query/constraint/tests/it/problem.rs b/src/query/constraint/tests/it/problem.rs deleted file mode 100644 index 959b0964921e..000000000000 --- a/src/query/constraint/tests/it/problem.rs +++ /dev/null @@ -1,68 +0,0 @@ -// Copyright 2023 Datafuse Labs. -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -use databend_common_constraint::mir::MirDataType; -use databend_common_constraint::problem::variable_must_not_null; - -use crate::parser::parse_mir_expr; - -#[test] -fn test_assert_int_not_null() { - let variables = &[("a".to_string(), MirDataType::Int)].into_iter().collect(); - - assert!(variable_must_not_null( - &parse_mir_expr("a is not null", variables), - "a", - )); - assert!(variable_must_not_null( - &parse_mir_expr("a > 0", variables), - "a", - )); - assert!(variable_must_not_null( - &parse_mir_expr("a > 0 or a < 0", variables), - "a", - )); - assert!(variable_must_not_null( - &parse_mir_expr("a > 0 and a < 1", variables), - "a", - )); - - assert!(!variable_must_not_null( - &parse_mir_expr("a > 0 or true", variables), - "a", - )); - assert!(!variable_must_not_null( - &parse_mir_expr("a is null", variables), - "a", - )); -} - -#[test] -fn test_assert_int_is_not_null_multiple_variable() { - let variables = &[ - ("a".to_string(), MirDataType::Int), - ("b".to_string(), MirDataType::Int), - ] - .into_iter() - .collect(); - - assert!(variable_must_not_null( - &parse_mir_expr("a > 0 and b > 0", variables), - "a", - )); - assert!(variable_must_not_null( - &parse_mir_expr("a > 0 and b > 0", variables), - "b", - )); -} diff --git a/src/query/constraint/tests/it/simplify.rs b/src/query/constraint/tests/it/simplify.rs deleted file mode 100644 index e31e5b0ce41c..000000000000 --- a/src/query/constraint/tests/it/simplify.rs +++ /dev/null @@ -1,173 +0,0 @@ -// Copyright 2023 Datafuse Labs. -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -use std::collections::HashMap; -use std::io::Write; - -use databend_common_constraint::mir::MirDataType; -use databend_common_constraint::mir::MirExpr; -use databend_common_constraint::simplify::mir_to_z3_assertion; -use databend_common_constraint::simplify::simplify_z3_ast; -use goldenfile::Mint; -use z3::Config; -use z3::Context; - -use crate::parser; - -pub fn simplify_ast( - file: &mut impl Write, - variables: &HashMap, - text: impl AsRef, -) { - let ctx = &Context::new(&Config::new()); - - let text = text.as_ref(); - - let mir_expr = parser::parse_mir_expr(text, variables); - let z3_ast = mir_to_z3_assertion(ctx, &mir_expr); - let output_z3_ast = z3_ast - .as_ref() - .and_then(|z3_ast| simplify_z3_ast(ctx, z3_ast)); - let output_mir_expr = output_z3_ast.as_ref().and_then(|output_z3_ast| { - output_z3_ast - .iter() - .map(|formula| MirExpr::from_z3_ast(formula, variables)) - .collect::>>() - }); - let ouput_sql_ast = output_mir_expr.as_ref().map(|output_mir_expr| { - output_mir_expr - .iter() - .map(parser::pretty_mir_expr) - .collect::>() - }); - - writeln!(file, "{:-^80}", " Input ").unwrap(); - writeln!(file, "{}", text).unwrap(); - writeln!(file, "{:-^80}", " Output ").unwrap(); - - if let Some(ouput_sql_ast) = ouput_sql_ast { - for conjunction in ouput_sql_ast { - writeln!(file, "{}", conjunction).unwrap(); - } - } else { - writeln!(file, "UNCHANGED").unwrap(); - } - - writeln!(file, "{:-^80}", " Input MIR ").unwrap(); - writeln!(file, "{:#?}", mir_expr).unwrap(); - - if let Some(z3_ast) = z3_ast { - writeln!(file, "{:-^80}", " Input Z3 AST ").unwrap(); - writeln!(file, "{:#?}", z3_ast).unwrap(); - } - - if let Some(output_z3_ast) = output_z3_ast { - writeln!(file, "{:-^80}", " Output Z3 AST ").unwrap(); - writeln!(file, "{:#?}", output_z3_ast).unwrap(); - } - - if let Some(output_mir_expr) = output_mir_expr { - writeln!(file, "{:-^80}", " Output MIR ").unwrap(); - writeln!(file, "{:#?}", output_mir_expr).unwrap(); - } - - writeln!(file, "\n").unwrap(); -} - -#[test] -fn test_simplify() { - let mut mint = Mint::new("tests/it/testdata"); - let file = &mut mint.new_goldenfile("simplify.txt").unwrap(); - - let variables = &[ - ("a".to_string(), MirDataType::Int), - ("b".to_string(), MirDataType::Int), - ("p".to_string(), MirDataType::Bool), - ("q".to_string(), MirDataType::Bool), - ] - .into_iter() - .collect(); - - simplify_ast(file, variables, "a > 0 or true"); - simplify_ast(file, variables, "a = 1 and a = 1"); - simplify_ast(file, variables, "a = 1 and a = 2"); - simplify_ast(file, variables, "a = 1 and a != 1"); - simplify_ast(file, variables, "a = 1 and a != 2"); - simplify_ast(file, variables, "a = 1 and a < 2 "); - simplify_ast(file, variables, "a = 1 and a < 1"); - simplify_ast(file, variables, "a = 1 and a <= 2"); - simplify_ast(file, variables, "a = 1 and a <= 1"); - simplify_ast(file, variables, "a = 1 and a > 0"); - simplify_ast(file, variables, "a = 1 and a > 1"); - simplify_ast(file, variables, "a = 1 and a >= 0"); - simplify_ast(file, variables, "a = 1 and a >= 1"); - simplify_ast(file, variables, "a != 1 and a = 1"); - simplify_ast(file, variables, "a != 1 and a = 2"); - simplify_ast(file, variables, "a != 1 and a != 1"); - simplify_ast(file, variables, "a != 1 and a != 2"); - simplify_ast(file, variables, "a != 1 and a < 1 "); - simplify_ast(file, variables, "a != 1 and a < 2"); - simplify_ast(file, variables, "a != 1 and a <= 1"); - simplify_ast(file, variables, "a != 1 and a <= 2"); - simplify_ast(file, variables, "a != 1 and a > 1"); - simplify_ast(file, variables, "a != 1 and a > 0"); - simplify_ast(file, variables, "a != 1 and a >= 1"); - simplify_ast(file, variables, "a != 1 and a >= 0"); - simplify_ast(file, variables, "a < 5 and a = 10"); - simplify_ast(file, variables, "a < 5 and a = 2"); - simplify_ast(file, variables, "a < 5 and a != 10"); - simplify_ast(file, variables, "a < 5 and a != 2"); - simplify_ast(file, variables, "a < 5 and a <= 10 "); - simplify_ast(file, variables, "a < 5 and a > 10"); - simplify_ast(file, variables, "a < 5 and a > 2"); - simplify_ast(file, variables, "a <= 1 and a >= 1"); - simplify_ast(file, variables, "a = 1 or a = 1"); - simplify_ast(file, variables, "a = 1 or a = 2"); - simplify_ast(file, variables, "a = 1 or a != 1"); - simplify_ast(file, variables, "a = 1 or a != 2"); - simplify_ast(file, variables, "a = 1 or a < 2 "); - simplify_ast(file, variables, "a = 1 or a < 1"); - simplify_ast(file, variables, "a = 1 or a <= 2"); - simplify_ast(file, variables, "a = 1 or a <= 1"); - simplify_ast(file, variables, "a = 1 or a > 0"); - simplify_ast(file, variables, "a = 1 or a > 1"); - simplify_ast(file, variables, "a = 1 or a >= 0"); - simplify_ast(file, variables, "a = 1 or a >= 1"); - simplify_ast(file, variables, "a != 1 or a = 1"); - simplify_ast(file, variables, "a != 1 or a = 2"); - simplify_ast(file, variables, "a != 1 or a != 1"); - simplify_ast(file, variables, "a != 1 or a != 2"); - simplify_ast(file, variables, "a != 1 or a < 1 "); - simplify_ast(file, variables, "a != 1 or a < 2"); - simplify_ast(file, variables, "a != 1 or a <= 1"); - simplify_ast(file, variables, "a != 1 or a <= 2"); - simplify_ast(file, variables, "a != 1 or a > 1"); - simplify_ast(file, variables, "a != 1 or a > 0"); - simplify_ast(file, variables, "a != 1 or a >= 1"); - simplify_ast(file, variables, "a != 1 or a >= 0"); - simplify_ast(file, variables, "a < 5 or a = 10"); - simplify_ast(file, variables, "a < 5 or a = 2"); - simplify_ast(file, variables, "a < 5 or a != 10"); - simplify_ast(file, variables, "a < 5 or a != 2"); - simplify_ast(file, variables, "a < 5 or a <= 10 "); - simplify_ast(file, variables, "a < 5 or a > 10"); - simplify_ast(file, variables, "a < 5 or a > 2"); - simplify_ast(file, variables, "a <= 1 or a >= 1"); - simplify_ast(file, variables, "a + b < 1 and a >= 0"); - simplify_ast(file, variables, "a + b < 1 and a - b >= 0"); - simplify_ast(file, variables, "a < a + b"); - simplify_ast(file, variables, "1 - 30 * a < 20 * a + b"); - simplify_ast(file, variables, "a > 0 and b > 0"); - simplify_ast(file, variables, "a > 0 and b > 0 and a * b = 0"); -} diff --git a/src/query/constraint/tests/it/testdata/simplify.txt b/src/query/constraint/tests/it/testdata/simplify.txt deleted file mode 100644 index 7515a791cffb..000000000000 --- a/src/query/constraint/tests/it/testdata/simplify.txt +++ /dev/null @@ -1,7495 +0,0 @@ ------------------------------------- Input ------------------------------------- -a > 0 or true ------------------------------------- Output ------------------------------------ ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, - right: Constant( - Bool( - true, - ), - ), -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - (= TRUE_BOOL TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= TRUE_BOOL NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[] ----------------------------------- Output MIR ---------------------------------- -[] - - ------------------------------------- Input ------------------------------------- -a = 1 and a = 1 ------------------------------------- Output ------------------------------------ -a = 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (= a (JUST_INT 1)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 and a = 2 ------------------------------------- Output ------------------------------------ -FALSE ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - false, -] ----------------------------------- Output MIR ---------------------------------- -[ - Constant( - Bool( - false, - ), - ), -] - - ------------------------------------- Input ------------------------------------- -a = 1 and a != 1 ------------------------------------- Output ------------------------------------ -FALSE ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - false, -] ----------------------------------- Output MIR ---------------------------------- -[ - Constant( - Bool( - false, - ), - ), -] - - ------------------------------------- Input ------------------------------------- -a = 1 and a != 2 ------------------------------------- Output ------------------------------------ -a = 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (= a (JUST_INT 1)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 and a < 2 ------------------------------------- Output ------------------------------------ -a = 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (= a (JUST_INT 1)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 and a < 1 ------------------------------------- Output ------------------------------------ -FALSE ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - false, -] ----------------------------------- Output MIR ---------------------------------- -[ - Constant( - Bool( - false, - ), - ), -] - - ------------------------------------- Input ------------------------------------- -a = 1 and a <= 2 ------------------------------------- Output ------------------------------------ -a = 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (= a (JUST_INT 1)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 and a <= 1 ------------------------------------- Output ------------------------------------ -a = 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (= a (JUST_INT 1)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 and a > 0 ------------------------------------- Output ------------------------------------ -a = 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (= a (JUST_INT 1)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 and a > 1 ------------------------------------- Output ------------------------------------ -FALSE ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - false, -] ----------------------------------- Output MIR ---------------------------------- -[ - Constant( - Bool( - false, - ), - ), -] - - ------------------------------------- Input ------------------------------------- -a = 1 and a >= 0 ------------------------------------- Output ------------------------------------ -a = 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (= a (JUST_INT 1)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 and a >= 1 ------------------------------------- Output ------------------------------------ -a = 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (= a (JUST_INT 1)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a = 1 ------------------------------------- Output ------------------------------------ -FALSE ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - false, -] ----------------------------------- Output MIR ---------------------------------- -[ - Constant( - Bool( - false, - ), - ), -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a = 2 ------------------------------------- Output ------------------------------------ -a = 2 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (= a (JUST_INT 2)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a != 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 1))), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a != 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 1 -NOT a = 2 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 1))), - (not (= a (JUST_INT 2))), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a < 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 1 -remove_nullable(a) <= 0 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 1))), - (<= (unwrap-int a) 0), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 0, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a < 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 1 -remove_nullable(a) <= 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 1))), - (<= (unwrap-int a) 1), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a <= 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 1 -remove_nullable(a) <= 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 1))), - (<= (unwrap-int a) 1), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a <= 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 1 -remove_nullable(a) <= 2 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 1))), - (<= (unwrap-int a) 2), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 2, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a > 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 1 -remove_nullable(a) >= 2 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 1))), - (>= (unwrap-int a) 2), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 2, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a > 0 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 1 -remove_nullable(a) >= 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 1))), - (>= (unwrap-int a) 1), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a >= 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 1 -remove_nullable(a) >= 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Gte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 1))), - (>= (unwrap-int a) 1), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 and a >= 0 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 1 -remove_nullable(a) >= 0 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Gte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 1))), - (>= (unwrap-int a) 0), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 0, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 and a = 10 ------------------------------------- Output ------------------------------------ -FALSE ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 10, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - false, -] ----------------------------------- Output MIR ---------------------------------- -[ - Constant( - Bool( - false, - ), - ), -] - - ------------------------------------- Input ------------------------------------- -a < 5 and a = 2 ------------------------------------- Output ------------------------------------ -a = 2 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (= a (JUST_INT 2)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 and a != 10 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 10 -remove_nullable(a) <= 4 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 10, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 10))), - (<= (unwrap-int a) 4), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 10, - ), - ), - }, - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 4, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 and a != 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -NOT a = 2 -remove_nullable(a) <= 4 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= a (JUST_INT 2))), - (<= (unwrap-int a) 4), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 4, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 and a <= 10 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -remove_nullable(a) <= 4 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 10, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 10))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 10))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (<= (unwrap-int a) 4), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 4, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 and a > 10 ------------------------------------- Output ------------------------------------ -FALSE ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 10, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 10))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 10))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - false, -] ----------------------------------- Output MIR ---------------------------------- -[ - Constant( - Bool( - false, - ), - ), -] - - ------------------------------------- Input ------------------------------------- -a < 5 and a > 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -remove_nullable(a) >= 3 -remove_nullable(a) <= 4 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (>= (unwrap-int a) 3), - (<= (unwrap-int a) 4), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 3, - ), - ), - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 4, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a <= 1 and a >= 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -remove_nullable(a) = 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (= (unwrap-int a) 1), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Eq, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a = 1 ------------------------------------- Output ------------------------------------ -a = 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (= a (JUST_INT 1)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a = 2 ------------------------------------- Output ------------------------------------ -a = 1 OR a = 2 -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (or (= a (JUST_INT 1)) (= a (JUST_INT 2))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a != 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a != 2 ------------------------------------- Output ------------------------------------ -NOT a = 2 -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a (JUST_INT 2))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a < 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -remove_nullable(a) <= 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (<= (unwrap-int a) 1), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a < 1 ------------------------------------- Output ------------------------------------ -a = 1 OR 1 > remove_nullable(a) -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (or (= a (JUST_INT 1)) (not (<= 1 (unwrap-int a)))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: Constant( - Int( - 1, - ), - ), - right: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a <= 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -remove_nullable(a) <= 2 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (<= (unwrap-int a) 2), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 2, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a <= 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -remove_nullable(a) <= 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (<= (unwrap-int a) 1), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a > 0 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -remove_nullable(a) >= 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (>= (unwrap-int a) 1), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a > 1 ------------------------------------- Output ------------------------------------ -a = 1 OR remove_nullable(a) > 1 -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (or (= a (JUST_INT 1)) (not (<= (unwrap-int a) 1))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a >= 0 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -remove_nullable(a) >= 0 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (>= (unwrap-int a) 0), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 0, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a = 1 or a >= 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -remove_nullable(a) >= 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (>= (unwrap-int a) 1), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a = 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a = 2 ------------------------------------- Output ------------------------------------ -NOT a = 1 OR a = 2 -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (or (not (= a (JUST_INT 1))) (= a (JUST_INT 2))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a != 1 ------------------------------------- Output ------------------------------------ -NOT a = 1 -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a (JUST_INT 1))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a != 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a < 1 ------------------------------------- Output ------------------------------------ -NOT a = 1 OR 1 > remove_nullable(a) -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (or (not (= a (JUST_INT 1))) (not (<= 1 (unwrap-int a)))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Gt, - left: Constant( - Int( - 1, - ), - ), - right: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a < 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a <= 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a <= 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a > 1 ------------------------------------- Output ------------------------------------ -NOT a = 1 -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a (JUST_INT 1))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a > 0 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a >= 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Gte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a != 1 or a >= 0 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - }, - right: BinaryOperator { - op: Gte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 1)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 or a = 10 ------------------------------------- Output ------------------------------------ -5 > remove_nullable(a) OR a = 10 -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 10, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (or (not (<= 5 (unwrap-int a))) (= a (JUST_INT 10))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Or, - left: BinaryOperator { - op: Gt, - left: Constant( - Int( - 5, - ), - ), - right: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 10, - ), - ), - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 or a = 2 ------------------------------------- Output ------------------------------------ -5 > remove_nullable(a) OR a = 2 -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (or (not (<= 5 (unwrap-int a))) (= a (JUST_INT 2))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Or, - left: BinaryOperator { - op: Gt, - left: Constant( - Int( - 5, - ), - ), - right: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - right: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 or a != 10 ------------------------------------- Output ------------------------------------ -NOT a = 10 -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 10, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 10)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a (JUST_INT 10))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 10, - ), - ), - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 or a != 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: UnaryOperator { - op: Not, - arg: BinaryOperator { - op: Eq, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) TRUE_BOOL FALSE_BOOL)) - NULL_BOOL) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) - (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (= a (JUST_INT 2)) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - FALSE_BOOL - TRUE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 or a <= 10 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -remove_nullable(a) <= 10 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 10, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 10))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 10))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (<= (unwrap-int a) 10), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 10, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 or a > 10 ------------------------------------- Output ------------------------------------ -5 > remove_nullable(a) OR remove_nullable(a) > 10 -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 10, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 10))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 10) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 10))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (or (not (<= 5 (unwrap-int a))) (not (<= (unwrap-int a) 10))), - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - BinaryOperator { - op: Or, - left: BinaryOperator { - op: Gt, - left: Constant( - Int( - 5, - ), - ), - right: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - right: BinaryOperator { - op: Gt, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 10, - ), - ), - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a < 5 or a > 2 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 5, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 2, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 5) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) (unwrap-int (JUST_INT 5))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 2) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 2))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a <= 1 or a >= 1 ------------------------------------- Output ------------------------------------ -a IS NOT NULL ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Or, - left: BinaryOperator { - op: Lte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 1, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL)) - TRUE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (<= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, -] - - ------------------------------------- Input ------------------------------------- -a + b < 1 and a >= 0 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -b IS NOT NULL -remove_nullable(a) + remove_nullable(b) <= 0 -remove_nullable(a) >= 0 -remove_nullable(b) <= 0 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Lt, - left: BinaryOperator { - op: Plus, - left: Variable { - name: "a", - data_type: Int, - }, - right: Variable { - name: "b", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gte, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int a) (unwrap-int b)))) - NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int a) - (unwrap-int b))))) - (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int a) (unwrap-int b)))) - NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int (ite (or (= a NULL_INT) - (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int a) - (unwrap-int b))))) - (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= b NULL_INT)), - (<= (+ (unwrap-int a) (unwrap-int b)) 0), - (>= (unwrap-int a) 0), - (<= (unwrap-int b) 0), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Lte, - left: BinaryOperator { - op: Plus, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - }, - right: Constant( - Int( - 0, - ), - ), - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 0, - ), - ), - }, - BinaryOperator { - op: Lte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - right: Constant( - Int( - 0, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a + b < 1 and a - b >= 0 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -b IS NOT NULL -remove_nullable(a) - remove_nullable(b) >= 0 -remove_nullable(a) + remove_nullable(b) <= 0 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Lt, - left: BinaryOperator { - op: Plus, - left: Variable { - name: "a", - data_type: Int, - }, - right: Variable { - name: "b", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, - right: BinaryOperator { - op: Gte, - left: BinaryOperator { - op: Minus, - left: Variable { - name: "a", - data_type: Int, - }, - right: Variable { - name: "b", - data_type: Int, - }, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int a) (unwrap-int b)))) - NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int a) - (unwrap-int b))))) - (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (- (unwrap-int a) (unwrap-int b)))) - NULL_INT) - (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (- (unwrap-int a) - (unwrap-int b))))) - (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int a) (unwrap-int b)))) - NULL_INT) - (= (JUST_INT 1) NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int (ite (or (= a NULL_INT) - (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int a) - (unwrap-int b))))) - (unwrap-int (JUST_INT 1))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (- (unwrap-int a) (unwrap-int b)))) - NULL_INT) - (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (>= (unwrap-int (ite (or (= a NULL_INT) - (= b NULL_INT)) - NULL_INT - (JUST_INT (- (unwrap-int a) - (unwrap-int b))))) - (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= b NULL_INT)), - (>= (+ (unwrap-int a) (* (- 1) (unwrap-int b))) 0), - (<= (+ (unwrap-int a) (unwrap-int b)) 0), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Gte, - left: BinaryOperator { - op: Minus, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - }, - right: Constant( - Int( - 0, - ), - ), - }, - BinaryOperator { - op: Lte, - left: BinaryOperator { - op: Plus, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - }, - right: Constant( - Int( - 0, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a < a + b ------------------------------------- Output ------------------------------------ -a IS NOT NULL -b IS NOT NULL -remove_nullable(b) >= 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Lt, - left: Variable { - name: "a", - data_type: Int, - }, - right: BinaryOperator { - op: Plus, - left: Variable { - name: "a", - data_type: Int, - }, - right: Variable { - name: "b", - data_type: Int, - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= a NULL_INT) - (= (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int a) (unwrap-int b)))) - NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int a) - (unwrap-int (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int a) (unwrap-int b)))))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= b NULL_INT)), - (>= (unwrap-int b) 1), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -1 - 30 * a < 20 * a + b ------------------------------------- Output ------------------------------------ -a IS NOT NULL -b IS NOT NULL -50 * remove_nullable(a) + remove_nullable(b) >= 2 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: Lt, - left: BinaryOperator { - op: Minus, - left: Constant( - Int( - 1, - ), - ), - right: BinaryOperator { - op: Multiply, - left: Constant( - Int( - 30, - ), - ), - right: Variable { - name: "a", - data_type: Int, - }, - }, - }, - right: BinaryOperator { - op: Plus, - left: BinaryOperator { - op: Multiply, - left: Constant( - Int( - 20, - ), - ), - right: Variable { - name: "a", - data_type: Int, - }, - }, - right: Variable { - name: "b", - data_type: Int, - }, - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= (JUST_INT 1) NULL_INT) - (= (ite (or (= (JUST_INT 30) NULL_INT) (= a NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int (JUST_INT 30)) - (unwrap-int a)))) - NULL_INT)) - NULL_INT - (JUST_INT (- (unwrap-int (JUST_INT 1)) - (unwrap-int (ite (or (= (JUST_INT 30) NULL_INT) - (= a NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int (JUST_INT 30)) - (unwrap-int a)))))))) - NULL_INT) - (= (ite (or (= (ite (or (= (JUST_INT 20) NULL_INT) (= a NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int (JUST_INT 20)) - (unwrap-int a)))) - NULL_INT) - (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int (ite (or (= (JUST_INT 20) NULL_INT) - (= a NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int (JUST_INT 20)) - (unwrap-int a))))) - (unwrap-int b)))) - NULL_INT)) - NULL_BOOL - (ite (< (unwrap-int (ite (or (= (JUST_INT 1) NULL_INT) - (= (ite (or (= (JUST_INT 30) NULL_INT) - (= a NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int (JUST_INT 30)) - (unwrap-int a)))) - NULL_INT)) - NULL_INT - (JUST_INT (- (unwrap-int (JUST_INT 1)) - (unwrap-int (ite (or (= (JUST_INT 30) - NULL_INT) - (= a - NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int (JUST_INT 30)) - (unwrap-int a))))))))) - (unwrap-int (ite (or (= (ite (or (= (JUST_INT 20) NULL_INT) - (= a NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int (JUST_INT 20)) - (unwrap-int a)))) - NULL_INT) - (= b NULL_INT)) - NULL_INT - (JUST_INT (+ (unwrap-int (ite (or (= (JUST_INT 20) - NULL_INT) - (= a - NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int (JUST_INT 20)) - (unwrap-int a))))) - (unwrap-int b)))))) - TRUE_BOOL - FALSE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= b NULL_INT)), - (>= (+ (* 50 (unwrap-int a)) (unwrap-int b)) 2), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Gte, - left: BinaryOperator { - op: Plus, - left: BinaryOperator { - op: Multiply, - left: Constant( - Int( - 50, - ), - ), - right: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - right: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - }, - right: Constant( - Int( - 2, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a > 0 and b > 0 ------------------------------------- Output ------------------------------------ -a IS NOT NULL -b IS NOT NULL -remove_nullable(a) >= 1 -remove_nullable(b) >= 1 ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "b", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= b NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int b) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= b NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int b) (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - (not (= a NULL_INT)), - (not (= b NULL_INT)), - (>= (unwrap-int a) 1), - (>= (unwrap-int b) 1), -] ----------------------------------- Output MIR ---------------------------------- -[ - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - }, - UnaryOperator { - op: Not, - arg: UnaryOperator { - op: IsNull, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "a", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, - BinaryOperator { - op: Gte, - left: UnaryOperator { - op: RemoveNullable, - arg: Variable { - name: "b", - data_type: Int, - }, - }, - right: Constant( - Int( - 1, - ), - ), - }, -] - - ------------------------------------- Input ------------------------------------- -a > 0 and b > 0 and a * b = 0 ------------------------------------- Output ------------------------------------ -FALSE ----------------------------------- Input MIR ----------------------------------- -BinaryOperator { - op: And, - left: BinaryOperator { - op: And, - left: BinaryOperator { - op: Gt, - left: Variable { - name: "a", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, - right: BinaryOperator { - op: Gt, - left: Variable { - name: "b", - data_type: Int, - }, - right: Constant( - Int( - 0, - ), - ), - }, - }, - right: BinaryOperator { - op: Eq, - left: BinaryOperator { - op: Multiply, - left: Variable { - name: "a", - data_type: Int, - }, - right: Variable { - name: "b", - data_type: Int, - }, - }, - right: Constant( - Int( - 0, - ), - ), - }, -} ---------------------------------- Input Z3 AST --------------------------------- -(= (ite (or (= (ite (or (= (ite (or (= a NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) - (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= b NULL_INT) (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int b) - (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) - (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) - (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= b NULL_INT) - (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int b) - (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - FALSE_BOOL) - (= (ite (or (= (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int a) (unwrap-int b)))) - NULL_INT) - (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int a) (unwrap-int b)))) - (JUST_INT 0)) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= (ite (or (= a NULL_INT) - (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) - (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL) - (= (ite (or (= b NULL_INT) - (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int b) - (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - FALSE_BOOL)) - FALSE_BOOL - (ite (or (= (ite (or (= a NULL_INT) - (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int a) - (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL) - (= (ite (or (= b NULL_INT) - (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (> (unwrap-int b) - (unwrap-int (JUST_INT 0))) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - NULL_BOOL) - (= (ite (or (= (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int a) (unwrap-int b)))) - NULL_INT) - (= (JUST_INT 0) NULL_INT)) - NULL_BOOL - (ite (= (ite (or (= a NULL_INT) (= b NULL_INT)) - NULL_INT - (JUST_INT (* (unwrap-int a) - (unwrap-int b)))) - (JUST_INT 0)) - TRUE_BOOL - FALSE_BOOL)) - NULL_BOOL)) - NULL_BOOL - TRUE_BOOL)) - TRUE_BOOL) --------------------------------- Output Z3 AST --------------------------------- -[ - false, -] ----------------------------------- Output MIR ---------------------------------- -[ - Constant( - Bool( - false, - ), - ), -] - - diff --git a/src/query/expression/src/expression.rs b/src/query/expression/src/expression.rs index c0e6de4ba489..6396635cdda8 100644 --- a/src/query/expression/src/expression.rs +++ b/src/query/expression/src/expression.rs @@ -530,6 +530,16 @@ impl Expr { } } } + + pub fn contains_column_ref(&self) -> bool { + match self { + Expr::ColumnRef { .. } => true, + Expr::Constant { .. } => false, + Expr::Cast { expr, .. } => expr.contains_column_ref(), + Expr::FunctionCall { args, .. } => args.iter().any(Expr::contains_column_ref), + Expr::LambdaFunctionCall { args, .. } => args.iter().any(Expr::contains_column_ref), + } + } } impl RemoteExpr { diff --git a/src/query/service/Cargo.toml b/src/query/service/Cargo.toml index ca9ec64a5cbb..f44ca421aeac 100644 --- a/src/query/service/Cargo.toml +++ b/src/query/service/Cargo.toml @@ -12,10 +12,9 @@ doctest = false test = true [features] -default = ["simd", "z3-prove"] +default = ["simd"] simd = ["databend-common-arrow/simd"] python-udf = ["arrow-udf-python"] -z3-prove = ["databend-common-sql/z3-prove"] disable_initial_exec_tls = ["databend-common-base/disable_initial_exec_tls"] memory-profiling = ["databend-common-base/memory-profiling", "databend-common-http/memory-profiling"] diff --git a/src/query/sql/Cargo.toml b/src/query/sql/Cargo.toml index 0cb1ba2998e2..d24b3a6ae0a5 100644 --- a/src/query/sql/Cargo.toml +++ b/src/query/sql/Cargo.toml @@ -13,7 +13,6 @@ test = true [features] default = [] storage-hdfs = ["databend-common-config/storage-hdfs"] -z3-prove = ["databend-common-constraint"] [dependencies] # In alphabetical order # Workspace dependencies @@ -23,7 +22,6 @@ databend-common-base = { path = "../../common/base" } databend-common-catalog = { path = "../catalog" } databend-common-compress = { path = "../../common/compress" } databend-common-config = { path = "../config" } -databend-common-constraint = { path = "../constraint", optional = true } databend-common-exception = { path = "../../common/exception" } databend-common-expression = { path = "../expression" } databend-common-functions = { path = "../functions" } diff --git a/src/query/sql/src/planner/optimizer/property/constraint.rs b/src/query/sql/src/planner/optimizer/property/constraint.rs deleted file mode 100644 index 5eba241b847a..000000000000 --- a/src/query/sql/src/planner/optimizer/property/constraint.rs +++ /dev/null @@ -1,192 +0,0 @@ -// Copyright 2021 Datafuse Labs -// -// Licensed under the Apache License, Version 2.0 (the "License"); -// you may not use this file except in compliance with the License. -// You may obtain a copy of the License at -// -// http://www.apache.org/licenses/LICENSE-2.0 -// -// Unless required by applicable law or agreed to in writing, software -// distributed under the License is distributed on an "AS IS" BASIS, -// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -// See the License for the specific language governing permissions and -// limitations under the License. - -use databend_common_constraint::mir::MirBinaryOperator; -use databend_common_constraint::mir::MirConstant; -use databend_common_constraint::mir::MirDataType; -use databend_common_constraint::mir::MirExpr; -use databend_common_constraint::mir::MirUnaryOperator; -use databend_common_constraint::problem::variable_must_not_null; -use databend_common_expression::cast_scalar; -use databend_common_expression::types::DataType; -use databend_common_expression::types::NumberDataType; -use databend_common_expression::types::NumberScalar; -use databend_common_expression::Scalar; -use databend_common_functions::BUILTIN_FUNCTIONS; - -use crate::plans::FunctionCall; -use crate::IndexType; -use crate::ScalarExpr; - -#[derive(Debug)] -pub struct ConstraintSet { - constraints: Vec<(ScalarExpr, MirExpr)>, - #[allow(dead_code)] - unsupported_constraints: Vec, -} - -impl ConstraintSet { - /// Build a `ConstraintSet` with conjunctions - pub fn new(constraints: &[ScalarExpr]) -> Self { - let mut supported_constraints = Vec::new(); - let mut unsupported_constraints = Vec::new(); - - for constraint in constraints { - let mir_expr = as_mir(constraint); - if let Some(mir_expr) = mir_expr { - supported_constraints.push((constraint.clone(), mir_expr)); - } else { - unsupported_constraints.push(constraint.clone()); - } - } - - Self { - constraints: supported_constraints, - unsupported_constraints, - } - } - - /// Check if the given variable is null-rejected with current constraints. - /// For example, with a constraint `a > 1`, the variable `a` must not be null. - /// - /// NOTICE: this check is false-positive, which means it may return `false` even - /// if the variable is null-rejected. But it can ensure not returning `true` for - /// the variable is not null-rejected. - pub fn is_null_reject(&self, variable: &IndexType) -> bool { - if !self - .constraints - .iter() - .any(|(scalar, _)| scalar.used_columns().contains(variable)) - { - // The variable isn't used by any constraint, therefore it's unconstrained. - return false; - } - - let conjunctions = self - .constraints - .iter() - .map(|(_, mir)| mir.clone()) - .reduce(|left, right| MirExpr::BinaryOperator { - op: MirBinaryOperator::And, - left: Box::new(left), - right: Box::new(right), - }) - .unwrap(); - - variable_must_not_null(&conjunctions, &variable.to_string()) - } -} - -/// Transform a logical expression into a MIR expression. -pub fn as_mir(scalar: &ScalarExpr) -> Option { - match scalar { - ScalarExpr::FunctionCall(func) => { - if let Some(unary_op) = match func.func_name.as_str() { - "minus" => Some(MirUnaryOperator::Minus), - "not" => Some(MirUnaryOperator::Not), - "is_null" => Some(MirUnaryOperator::IsNull), - "is_not_null" => { - return Some(MirExpr::UnaryOperator { - op: MirUnaryOperator::Not, - arg: Box::new(as_mir(&ScalarExpr::FunctionCall(FunctionCall { - func_name: "is_null".to_string(), - ..func.clone() - }))?), - }); - } - _ => None, - } { - let arg = as_mir(&func.arguments[0])?; - return Some(MirExpr::UnaryOperator { - op: unary_op, - arg: Box::new(arg), - }); - } - - if let Some(binary_op) = match func.func_name.as_str() { - "plus" => Some(MirBinaryOperator::Plus), - "minus" => Some(MirBinaryOperator::Minus), - "multiply" => Some(MirBinaryOperator::Multiply), - "and" => Some(MirBinaryOperator::And), - "or" => Some(MirBinaryOperator::Or), - "lt" => Some(MirBinaryOperator::Lt), - "lte" => Some(MirBinaryOperator::Lte), - "gt" => Some(MirBinaryOperator::Gt), - "gte" => Some(MirBinaryOperator::Gte), - "eq" => Some(MirBinaryOperator::Eq), - "noteq" => { - return Some(MirExpr::UnaryOperator { - op: MirUnaryOperator::Not, - arg: Box::new(as_mir(&ScalarExpr::FunctionCall(FunctionCall { - func_name: "eq".to_string(), - ..func.clone() - }))?), - }); - } - _ => None, - } { - let left = as_mir(&func.arguments[0])?; - let right = as_mir(&func.arguments[1])?; - return Some(MirExpr::BinaryOperator { - op: binary_op, - left: Box::new(left), - right: Box::new(right), - }); - } - - None - } - ScalarExpr::ConstantExpr(constant) => { - let value = match &constant.value { - Scalar::Number(scalar) if scalar.data_type().is_integer() => { - MirConstant::Int(parse_int_literal(*scalar)?) - } - Scalar::Boolean(value) => MirConstant::Bool(*value), - Scalar::Null => MirConstant::Null, - Scalar::Timestamp(value) => MirConstant::Int(*value), - _ => return None, - }; - Some(MirExpr::Constant(value)) - } - ScalarExpr::BoundColumnRef(column_ref) => { - let name = column_ref.column.index.to_string(); - let data_type = match column_ref.column.data_type.remove_nullable() { - DataType::Boolean => MirDataType::Bool, - DataType::Number(num_ty) if num_ty.is_integer() => MirDataType::Int, - DataType::Timestamp => MirDataType::Int, - _ => return None, - }; - Some(MirExpr::Variable { name, data_type }) - } - _ => None, - } -} - -/// Parse a scalar value into a i64 if possible. -/// This is used to parse a constant expression into z3 ast. -fn parse_int_literal(lit: NumberScalar) -> Option { - Some( - cast_scalar( - None, - Scalar::Number(lit), - DataType::Number(NumberDataType::Int64), - &BUILTIN_FUNCTIONS, - ) - .ok()? - .into_number() - .unwrap() - .into_int64() - .unwrap(), - ) -} diff --git a/src/query/sql/src/planner/optimizer/property/mod.rs b/src/query/sql/src/planner/optimizer/property/mod.rs index c35ae88f587f..e4fc73909b48 100644 --- a/src/query/sql/src/planner/optimizer/property/mod.rs +++ b/src/query/sql/src/planner/optimizer/property/mod.rs @@ -15,9 +15,6 @@ mod builder; mod column_stat; -#[cfg(feature = "z3-prove")] -mod constraint; - mod enforcer; mod histogram; #[allow(clippy::module_inception)] @@ -28,8 +25,6 @@ pub use builder::RelExpr; pub use column_stat::ColumnStat; pub use column_stat::ColumnStatSet; pub use column_stat::NewStatistic; -#[cfg(feature = "z3-prove")] -pub use constraint::ConstraintSet; pub use enforcer::require_property; pub use enforcer::DistributionEnforcer; pub use enforcer::Enforcer; diff --git a/src/query/sql/src/planner/optimizer/rule/factory.rs b/src/query/sql/src/planner/optimizer/rule/factory.rs index 2284e4619637..c1f9dca75509 100644 --- a/src/query/sql/src/planner/optimizer/rule/factory.rs +++ b/src/query/sql/src/planner/optimizer/rule/factory.rs @@ -59,7 +59,7 @@ impl RuleFactory { RuleID::EliminateEvalScalar => Ok(Box::new(RuleEliminateEvalScalar::new())), RuleID::PushDownFilterUnion => Ok(Box::new(RulePushDownFilterUnion::new())), RuleID::PushDownFilterEvalScalar => Ok(Box::new(RulePushDownFilterEvalScalar::new())), - RuleID::PushDownFilterJoin => Ok(Box::new(RulePushDownFilterJoin::new())), + RuleID::PushDownFilterJoin => Ok(Box::new(RulePushDownFilterJoin::new(metadata))), RuleID::PushDownFilterScan => Ok(Box::new(RulePushDownFilterScan::new(metadata))), RuleID::PushDownFilterSort => Ok(Box::new(RulePushDownFilterSort::new())), RuleID::PushDownFilterProjectSet => Ok(Box::new(RulePushDownFilterProjectSet::new())), diff --git a/src/query/sql/src/planner/optimizer/rule/rewrite/push_down_filter_join/outer_join_to_inner_join.rs b/src/query/sql/src/planner/optimizer/rule/rewrite/push_down_filter_join/outer_join_to_inner_join.rs index f9193afb2857..0db88ee0f4a8 100644 --- a/src/query/sql/src/planner/optimizer/rule/rewrite/push_down_filter_join/outer_join_to_inner_join.rs +++ b/src/query/sql/src/planner/optimizer/rule/rewrite/push_down_filter_join/outer_join_to_inner_join.rs @@ -12,10 +12,14 @@ // See the License for the specific language governing permissions and // limitations under the License. +use std::collections::HashMap; use std::sync::Arc; use databend_common_exception::Result; +use databend_common_expression::types::DataType; +use databend_common_expression::ConstantFolder; use databend_common_expression::DataBlock; +use databend_common_expression::DataField; use databend_common_expression::DataSchema; use databend_common_expression::Evaluator; use databend_common_expression::Expr; @@ -33,10 +37,11 @@ use crate::plans::Filter; use crate::plans::Join; use crate::plans::JoinType; use crate::ColumnSet; +use crate::MetadataRef; use crate::ScalarExpr; use crate::TypeCheck; -pub fn outer_join_to_inner_join(s_expr: &SExpr) -> Result<(SExpr, bool)> { +pub fn outer_join_to_inner_join(s_expr: &SExpr, metadata: MetadataRef) -> Result<(SExpr, bool)> { let mut join: Join = s_expr.child(0)?.plan().clone().try_into()?; if !join.join_type.is_outer_join() { return Ok((s_expr.clone(), false)); @@ -57,7 +62,8 @@ pub fn outer_join_to_inner_join(s_expr: &SExpr) -> Result<(SExpr, bool)> { if can_filter_null( predicate, &left_prop.output_columns, - &right_prop.output_columns, + &join.join_type, + metadata.clone(), )? => { can_filter_left_null = true; @@ -65,45 +71,35 @@ pub fn outer_join_to_inner_join(s_expr: &SExpr) -> Result<(SExpr, bool)> { JoinPredicate::Right(_) if can_filter_null( predicate, - &left_prop.output_columns, &right_prop.output_columns, + &join.join_type, + metadata.clone(), )? => { can_filter_right_null = true; } - JoinPredicate::Both { .. } + JoinPredicate::Both { .. } | JoinPredicate::Other(_) => { if can_filter_null( predicate, &left_prop.output_columns, + &join.join_type, + metadata.clone(), + )? { + can_filter_left_null = true; + } + if can_filter_null( + predicate, &right_prop.output_columns, - )? => - { - can_filter_left_null = true; - can_filter_right_null = true; + &join.join_type, + metadata.clone(), + )? { + can_filter_right_null = true; + } } _ => (), } } - #[cfg(feature = "z3-prove")] - { - let constraint_set = crate::optimizer::ConstraintSet::new(&filter.predicates); - let left_columns = join_rel_expr - .derive_relational_prop_child(0)? - .output_columns - .clone(); - let right_columns = join_rel_expr - .derive_relational_prop_child(1)? - .output_columns - .clone(); - can_filter_left_null |= left_columns - .iter() - .any(|col| constraint_set.is_null_reject(col)); - can_filter_right_null |= right_columns - .iter() - .any(|col| constraint_set.is_null_reject(col)); - } - let original_join_type = join.join_type.clone(); join.join_type = eliminate_outer_join_type(join.join_type, can_filter_left_null, can_filter_right_null); @@ -156,33 +152,35 @@ fn eliminate_outer_join_type( pub fn can_filter_null( predicate: &ScalarExpr, - left_output_columns: &ColumnSet, - right_output_columns: &ColumnSet, + columns_can_be_replaced: &ColumnSet, + join_type: &JoinType, + metadata: MetadataRef, ) -> Result { + if !matches!(join_type, JoinType::Left | JoinType::Right | JoinType::Full) { + return Ok(true); + } + struct ReplaceColumnBindingsNull<'a> { can_replace: bool, - left_output_columns: &'a ColumnSet, - right_output_columns: &'a ColumnSet, + columns_can_be_replaced: &'a ColumnSet, } impl<'a> ReplaceColumnBindingsNull<'a> { - fn replace( - &mut self, - expr: &mut ScalarExpr, - column_set: &mut Option, - ) -> Result<()> { + fn replace(&mut self, expr: &mut ScalarExpr) -> Result<()> { if !self.can_replace { return Ok(()); } match expr { ScalarExpr::BoundColumnRef(column_ref) => { - if let Some(column_set) = column_set { - column_set.insert(column_ref.column.index); + if self + .columns_can_be_replaced + .contains(&column_ref.column.index) + { + *expr = ScalarExpr::ConstantExpr(ConstantExpr { + span: None, + value: Scalar::Null, + }); } - *expr = ScalarExpr::ConstantExpr(ConstantExpr { - span: None, - value: Scalar::Null, - }); Ok(()) } ScalarExpr::FunctionCall(func) => { @@ -196,40 +194,13 @@ pub fn can_filter_null( return Ok(()); } - if func.func_name != "or" { - for expr in &mut func.arguments { - self.replace(expr, column_set)?; - } - return Ok(()); - } - - let mut children_columns_set = Some(ColumnSet::new()); for expr in &mut func.arguments { - self.replace(expr, &mut children_columns_set)?; - } - - let mut has_left = false; - let mut has_right = false; - let children_columns_set = children_columns_set.unwrap(); - for column in children_columns_set.iter() { - if self.left_output_columns.contains(column) { - has_left = true; - } else if self.right_output_columns.contains(column) { - has_right = true; - } - } - if has_left && has_right { - self.can_replace = false; - return Ok(()); - } - - if let Some(column_set) = column_set { - *column_set = column_set.union(&children_columns_set).cloned().collect(); + self.replace(expr)?; } Ok(()) } - ScalarExpr::CastExpr(cast) => self.replace(&mut cast.argument, column_set), + ScalarExpr::CastExpr(cast) => self.replace(&mut cast.argument), ScalarExpr::ConstantExpr(_) => Ok(()), _ => { self.can_replace = false; @@ -242,14 +213,18 @@ pub fn can_filter_null( // Replace the column bindings of predicate with `Scalar::Null` and evaluate the result. let mut replace = ReplaceColumnBindingsNull { can_replace: true, - left_output_columns, - right_output_columns, + columns_can_be_replaced, }; let mut null_scalar_expr = predicate.clone(); - replace.replace(&mut null_scalar_expr, &mut None).unwrap(); + replace.replace(&mut null_scalar_expr).unwrap(); if replace.can_replace { - let expr = convert_scalar_expr_to_expr(null_scalar_expr)?; + let columns = null_scalar_expr.columns_and_data_types(metadata); + let expr = convert_scalar_expr_to_expr(null_scalar_expr, columns)?; let func_ctx = &FunctionContext::default(); + let (expr, _) = ConstantFolder::fold(&expr, func_ctx, &BUILTIN_FUNCTIONS); + if expr.contains_column_ref() { + return Ok(false); + } let data_block = DataBlock::empty(); let evaluator = Evaluator::new(&data_block, func_ctx, &BUILTIN_FUNCTIONS); if let Value::Scalar(scalar) = evaluator.run(&expr)? { @@ -263,8 +238,15 @@ pub fn can_filter_null( } // Convert `ScalarExpr` to `Expr`. -fn convert_scalar_expr_to_expr(scalar_expr: ScalarExpr) -> Result { - let schema = Arc::new(DataSchema::new(vec![])); +fn convert_scalar_expr_to_expr( + scalar_expr: ScalarExpr, + columns: HashMap, +) -> Result { + let fields = columns + .into_iter() + .map(|(index, data_type)| DataField::new(index.to_string().as_str(), data_type)) + .collect(); + let schema = Arc::new(DataSchema::new(fields)); let remote_expr = scalar_expr .type_check(schema.as_ref())? .project_column_ref(|index| schema.index_of(&index.to_string()).unwrap()) diff --git a/src/query/sql/src/planner/optimizer/rule/rewrite/rule_push_down_filter_join.rs b/src/query/sql/src/planner/optimizer/rule/rewrite/rule_push_down_filter_join.rs index 3bddc292c3a4..566876967f29 100644 --- a/src/query/sql/src/planner/optimizer/rule/rewrite/rule_push_down_filter_join.rs +++ b/src/query/sql/src/planner/optimizer/rule/rewrite/rule_push_down_filter_join.rs @@ -39,14 +39,16 @@ use crate::plans::JoinType; use crate::plans::Operator; use crate::plans::RelOp; use crate::plans::ScalarExpr; +use crate::MetadataRef; pub struct RulePushDownFilterJoin { id: RuleID, matchers: Vec, + metadata: MetadataRef, } impl RulePushDownFilterJoin { - pub fn new() -> Self { + pub fn new(metadata: MetadataRef) -> Self { Self { id: RuleID::PushDownFilterJoin, // Filter @@ -62,6 +64,7 @@ impl RulePushDownFilterJoin { children: vec![Matcher::Leaf, Matcher::Leaf], }], }], + metadata, } } } @@ -73,7 +76,7 @@ impl Rule for RulePushDownFilterJoin { fn apply(&self, s_expr: &SExpr, state: &mut TransformResult) -> Result<()> { // First, try to convert outer join to inner join - let (s_expr, outer_to_inner) = outer_join_to_inner_join(s_expr)?; + let (s_expr, outer_to_inner) = outer_join_to_inner_join(s_expr, self.metadata.clone())?; // Second, check if can convert mark join to semi join let (s_expr, mark_to_semi) = convert_mark_to_semi_join(&s_expr)?; @@ -88,7 +91,7 @@ impl Rule for RulePushDownFilterJoin { } // Finally, push down filter to join. - let (need_push, mut result) = try_push_down_filter_join(&s_expr)?; + let (need_push, mut result) = try_push_down_filter_join(&s_expr, self.metadata.clone())?; if !need_push && !outer_to_inner && !mark_to_semi { return Ok(()); } @@ -104,7 +107,7 @@ impl Rule for RulePushDownFilterJoin { } } -pub fn try_push_down_filter_join(s_expr: &SExpr) -> Result<(bool, SExpr)> { +pub fn try_push_down_filter_join(s_expr: &SExpr, metadata: MetadataRef) -> Result<(bool, SExpr)> { // Extract or predicates from Filter to push down them to join. // For example: `select * from t1, t2 where (t1.a=1 and t2.b=2) or (t1.a=2 and t2.b=1)` // The predicate will be rewritten to `((t1.a=1 and t2.b=2) or (t1.a=2 and t2.b=1)) and (t1.a=1 or t1.a=2) and (t2.b=2 or t2.b=1)` @@ -142,7 +145,8 @@ pub fn try_push_down_filter_join(s_expr: &SExpr) -> Result<(bool, SExpr)> { if can_filter_null( &predicate, &left_prop.output_columns, - &right_prop.output_columns, + &join.join_type, + metadata.clone(), )? { left_push_down.push(predicate); } else { @@ -159,8 +163,9 @@ pub fn try_push_down_filter_join(s_expr: &SExpr) -> Result<(bool, SExpr)> { ) { if can_filter_null( &predicate, - &left_prop.output_columns, &right_prop.output_columns, + &join.join_type, + metadata.clone(), )? { right_push_down.push(predicate); } else { diff --git a/src/query/sql/src/planner/plans/scalar_expr.rs b/src/query/sql/src/planner/plans/scalar_expr.rs index 810479ed87d1..582715230b3a 100644 --- a/src/query/sql/src/planner/plans/scalar_expr.rs +++ b/src/query/sql/src/planner/plans/scalar_expr.rs @@ -12,6 +12,7 @@ // See the License for the specific language governing permissions and // limitations under the License. +use std::collections::HashMap; use std::hash::Hash; use std::hash::Hasher; @@ -34,6 +35,7 @@ use crate::binder::ColumnBinding; use crate::optimizer::ColumnSet; use crate::optimizer::SExpr; use crate::IndexType; +use crate::MetadataRef; #[derive(Clone, Debug, PartialEq, Eq, Hash)] pub enum ScalarExpr { @@ -180,6 +182,39 @@ impl ScalarExpr { Ok(()) } + pub fn columns_and_data_types(&self, metadata: MetadataRef) -> HashMap { + struct UsedColumnsVisitor { + columns: HashMap, + metadata: MetadataRef, + } + + impl<'a> Visitor<'a> for UsedColumnsVisitor { + fn visit_bound_column_ref(&mut self, col: &'a BoundColumnRef) -> Result<()> { + self.columns + .insert(col.column.index, *col.column.data_type.clone()); + Ok(()) + } + + fn visit_subquery(&mut self, subquery: &'a SubqueryExpr) -> Result<()> { + for idx in subquery.outer_columns.iter() { + self.columns + .insert(*idx, self.metadata.read().column(*idx).data_type()); + } + if let Some(child_expr) = subquery.child_expr.as_ref() { + self.visit(child_expr)?; + } + Ok(()) + } + } + + let mut visitor = UsedColumnsVisitor { + columns: HashMap::new(), + metadata, + }; + visitor.visit(self).unwrap(); + visitor.columns + } + pub fn has_one_column_ref(&self) -> bool { struct BoundColumnRefVisitor { has_column_ref: bool, diff --git a/tests/sqllogictests/suites/mode/standalone/explain/eliminate_outer_join.test b/tests/sqllogictests/suites/mode/standalone/explain/eliminate_outer_join.test index 73a91d195b6f..2dc8d30f7d27 100644 --- a/tests/sqllogictests/suites/mode/standalone/explain/eliminate_outer_join.test +++ b/tests/sqllogictests/suites/mode/standalone/explain/eliminate_outer_join.test @@ -614,33 +614,37 @@ Filter query T explain select * from t left join t t1 on t.a = t1.a where t1.a <= 1 or (t.a > 1 and t.a < 2) ---- -HashJoin +Filter ├── output columns: [t.a (#0), t1.a (#1)] -├── join type: INNER -├── build keys: [t1.a (#1)] -├── probe keys: [t.a (#0)] -├── filters: [t1.a (#1) <= 1 OR t.a (#0) > 1 AND t.a (#0) < 2] -├── estimated rows: 10.00 -├── TableScan(Build) -│ ├── table: default.eliminate_outer_join.t -│ ├── output columns: [a (#1)] -│ ├── read rows: 10 -│ ├── read size: < 1 KiB -│ ├── partitions total: 1 -│ ├── partitions scanned: 1 -│ ├── pruning stats: [segments: , blocks: ] -│ ├── push downs: [filters: [], limit: NONE] -│ └── estimated rows: 10.00 -└── TableScan(Probe) - ├── table: default.eliminate_outer_join.t - ├── output columns: [a (#0)] - ├── read rows: 10 - ├── read size: < 1 KiB - ├── partitions total: 1 - ├── partitions scanned: 1 - ├── pruning stats: [segments: , blocks: ] - ├── push downs: [filters: [], limit: NONE] - └── estimated rows: 10.00 +├── filters: [is_true(t1.a (#1) <= 1 OR t.a (#0) > 1 AND t.a (#0) < 2)] +├── estimated rows: 4.05 +└── HashJoin + ├── output columns: [t.a (#0), t1.a (#1)] + ├── join type: LEFT OUTER + ├── build keys: [t1.a (#1)] + ├── probe keys: [t.a (#0)] + ├── filters: [] + ├── estimated rows: 10.00 + ├── TableScan(Build) + │ ├── table: default.eliminate_outer_join.t + │ ├── output columns: [a (#1)] + │ ├── read rows: 10 + │ ├── read size: < 1 KiB + │ ├── partitions total: 1 + │ ├── partitions scanned: 1 + │ ├── pruning stats: [segments: , blocks: ] + │ ├── push downs: [filters: [], limit: NONE] + │ └── estimated rows: 10.00 + └── TableScan(Probe) + ├── table: default.eliminate_outer_join.t + ├── output columns: [a (#0)] + ├── read rows: 10 + ├── read size: < 1 KiB + ├── partitions total: 1 + ├── partitions scanned: 1 + ├── pruning stats: [segments: , blocks: ] + ├── push downs: [filters: [], limit: NONE] + └── estimated rows: 10.00 statement ok create table time_table(a timestamp)