From f3ccba2f2dc66f4cd9e4bc6759114e30f09a3e69 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Wed, 19 Apr 2023 11:50:36 +0200 Subject: [PATCH 01/12] ADT-CHC: initial commit, automated test run and added a failing test to brainstorm ADT-CHC: handling OP_DT_ACCESSOR ad a constructor Handle accessor as a variable Testing delta --- bench/run-bench.sh | 49 +++++++ bench_adt/run-bench.sh | 77 ++++++++++ bench_adt/simple_if.smt2 | 163 +++++++++++++++++++++ bench_adt/simple_if_min.smt2 | 163 +++++++++++++++++++++ bench_horn_adt/run-bench.sh | 49 +++++++ bench_sim/run-bench.sh | 49 +++++++ constructor_selector.smt2 | 11 ++ constructor_selector_helper_assertion.smt2 | 17 +++ constructor_selector_uf.smt2 | 14 ++ include/adt/CHCSolver.hpp | 17 ++- include/deep/HornNonlin.hpp | 29 +++- include/ufo/Expr.hpp | 102 +++++++++---- include/ufo/Smt/ZExprConverter.hpp | 112 ++++++++++---- 13 files changed, 793 insertions(+), 59 deletions(-) create mode 100755 bench/run-bench.sh create mode 100755 bench_adt/run-bench.sh create mode 100644 bench_adt/simple_if.smt2 create mode 100644 bench_adt/simple_if_min.smt2 create mode 100755 bench_horn_adt/run-bench.sh create mode 100755 bench_sim/run-bench.sh create mode 100644 constructor_selector.smt2 create mode 100644 constructor_selector_helper_assertion.smt2 create mode 100644 constructor_selector_uf.smt2 diff --git a/bench/run-bench.sh b/bench/run-bench.sh new file mode 100755 index 000000000..6c8e41157 --- /dev/null +++ b/bench/run-bench.sh @@ -0,0 +1,49 @@ +#!/bin/bash +echo "This is the script for running regression tests" +echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')" +echo " - host name $(hostname -f)" +echo " - script path: $(readlink -f $0)" + +adtchc=../adtchc +if [[ ! $# -eq 0 ]] ; then + #echo 'Setting path to' $1 + adtchc=$1 +fi + +# run the interpolating version of OpenSMT +adtchc=${adtchc}' -i' + +picky=./utils/picky.smt2 +lookahead=./utils/lookahead.smt2 + +tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S') +mkdir ${tmpfolder} + +export outmod=false +export errmod=false +export rtmod=false +export err=false + +for file in $(find . -name '*.smt2' |sort); do + name=$(basename $file) + dir=$(dirname $file) + + sh -c "ulimit -St 60; ${adtchc} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null + grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err + + if [ -s "$tmpfolder/$name.err" ]; then + echo "stderr not empty for benchmark $file"; + err=true; + fi + + +done +#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}" + +if [[ ${err} == true ]]; then + echo "There were anomalies: check logs in ${tmpfolder}" + exit 1 +else + rm -rf ${tmpfolder} +fi + diff --git a/bench_adt/run-bench.sh b/bench_adt/run-bench.sh new file mode 100755 index 000000000..a40b591df --- /dev/null +++ b/bench_adt/run-bench.sh @@ -0,0 +1,77 @@ +#!/bin/bash +echo "This is the script for running regression tests" +echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')" +echo " - host name $(hostname -f)" +echo " - script path: $(readlink -f $0)" + +opensmt=../opensmt +if [[ ! $# -eq 0 ]] ; then + #echo 'Setting path to' $1 + opensmt=$1 +fi + +# run the interpolating version of OpenSMT +opensmt=${opensmt}' -i' + +picky=./utils/picky.smt2 +lookahead=./utils/lookahead.smt2 + +tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S') +mkdir ${tmpfolder} + +export outmod=false +export errmod=false +export rtmod=false +export err=false + +for file in $(find . -name '*.smt2' |sort); do + name=$(basename $file) + dir=$(dirname $file) + + sh -c "ulimit -St 60; ${opensmt} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null + grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err + + if [ -s "$tmpfolder/$name.err" ]; then + echo "stderr not empty for benchmark $file"; + err=true; + fi + + sh -c "ulimit -St 60; ${opensmt} $picky $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null + grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err + + if [ -s "$tmpfolder/$name.err" ]; then + echo "stderr not empty for picky benchmark $file"; + err=true; + fi + + sh -c "ulimit -St 60; ${opensmt} $lookahead $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null + grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err + + if [ -s "$tmpfolder/$name.err" ]; then + echo "stderr not empty for lookahead benchmark $file"; + err=true; + fi + + #diff -q ${tmpfolder}/${name}.out ${dir}/${name}.expected.out + #if [ $? != 0 ]; then + # echo "stdout differs for benchmark $file"; + # outmod=true; + # diff ${tmpfolder}/${name}.out ${dir}/${name}.expected.out + #fi + #diff -q ${tmpfolder}/${name}.err ${dir}/${name}.expected.err + #if [ $? != 0 ]; then + # echo "stderr differs for benchmark $file"; + # errmod=true; + # diff ${tmpfolder}/${name}.err ${dir}/${name}.expected.err + #fi + +done +#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}" + +if [[ ${err} == true ]]; then + echo "There were anomalies: check logs in ${tmpfolder}" + exit 1 +else + rm -rf ${tmpfolder} +fi + diff --git a/bench_adt/simple_if.smt2 b/bench_adt/simple_if.smt2 new file mode 100644 index 000000000..4d304883e --- /dev/null +++ b/bench_adt/simple_if.smt2 @@ -0,0 +1,163 @@ +(set-logic HORN) + +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |interface_0_C_31_0| (Int |abi_type| |crypto_type| |state_type| ) Bool) +(declare-fun |nondet_interface_1_C_31_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool) +(declare-fun |summary_constructor_2_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (state_0 |state_type|) (this_0 Int) (tx_0 |tx_type|)) +(=> (= error_0 0) (nondet_interface_1_C_31_0 error_0 this_0 abi_0 crypto_0 state_0 state_0)))) + + +(declare-fun |summary_3_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |summary_4_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_1 Int)) +(=> (and (and (nondet_interface_1_C_31_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_4_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 a_2_0 state_2 a_2_1 z_5_1))) (nondet_interface_1_C_31_0 error_1 this_0 abi_0 crypto_0 state_0 state_2)))) + + +(declare-fun |block_5_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |block_6_simple_if_29_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) +(block_5_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) +(=> (and (and (block_5_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= a_2_1 a_2_0))) true)) true) (block_6_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(declare-fun |block_7_return_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |block_8_if_header_simple_if_28_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |block_9_if_true_simple_if_18_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |block_10_if_false_simple_if_27_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |block_11_simple_if_29_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) +(=> (and (and (block_6_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_1 0) (and (and (>= a_2_1 0) (<= a_2_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))) true) (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) +(=> (and (and (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_9_1 (< expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 5) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 a_2_1) true)))))) expr_9_1) (block_9_if_true_simple_if_18_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) +(=> (and (and (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_9_1 (< expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 5) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 a_2_1) true)))))) (not expr_9_1)) (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_9_if_true_simple_if_18_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_2 expr_16_0) (and (=> true true) (and (= expr_16_0 0) (and (= a_2_2 expr_14_1) (and (=> true (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 expr_13_1) (and (=> true (and (>= expr_10_0 0) (<= expr_10_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_10_0 a_2_1) (and (=> true (and (>= expr_13_1 0) (<= expr_13_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_1 (+ expr_11_0 expr_12_0)) (and (=> true true) (and (= expr_12_0 1) (and (=> true (and (>= expr_11_0 0) (<= expr_11_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_11_0 a_2_1) true))))))))))))))) true) (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2)))) + + +(declare-fun |block_12_return_ghost_simple_if_17_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_12_return_ghost_simple_if_17_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2) (and (= z_5_2 expr_16_0) (and (=> true true) (and (= expr_16_0 0) (and (= a_2_2 expr_14_1) (and (=> true (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 expr_13_1) (and (=> true (and (>= expr_10_0 0) (<= expr_10_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_10_0 a_2_1) (and (=> true (and (>= expr_13_1 0) (<= expr_13_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_1 (+ expr_11_0 expr_12_0)) (and (=> true true) (and (= expr_12_0 1) (and (=> true (and (>= expr_11_0 0) (<= expr_11_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_11_0 a_2_1) true))))))))))))))) true) (block_11_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2)))) + + +(declare-fun |block_13_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))) (and (not expr_22_1) (= error_1 1))) (block_13_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (block_13_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (summary_3_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_2 expr_25_0) (and (=> true true) (and (= expr_25_0 1) (and (= error_1 error_0) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))))))) true) (block_7_return_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2)))) + + +(declare-fun |block_14_return_ghost_simple_if_26_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_14_return_ghost_simple_if_26_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2) (and (= z_5_2 expr_25_0) (and (=> true true) (and (= expr_25_0 1) (and (= error_1 error_0) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))))))) true) (block_11_simple_if_29_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_11_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) true) true) (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) true) true) (summary_3_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(declare-fun |block_15_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(block_15_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_15_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (summary_3_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 a_2_1 state_3 a_2_2 z_5_1) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3745062286)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 223)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 57)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 29)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 142)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= a_2_1 a_2_0))) true))))))) true) (summary_4_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_3 a_2_2 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (interface_0_C_31_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (= error_0 0))) (interface_0_C_31_0 this_0 abi_0 crypto_0 state_1)))) + + +(declare-fun |contract_initializer_16_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(declare-fun |contract_initializer_entry_17_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_17_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(declare-fun |contract_initializer_after_init_18_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (contract_initializer_entry_17_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_18_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (contract_initializer_after_init_18_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_16_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(declare-fun |implicit_constructor_entry_19_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_16_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_16_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (summary_constructor_2_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_31_0 this_0 abi_0 crypto_0 state_1)))) + + +(declare-fun |error_target_3_0| () Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (interface_0_C_31_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (= error_0 1))) error_target_3_0))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> error_target_3_0 false))) +(check-sat) diff --git a/bench_adt/simple_if_min.smt2 b/bench_adt/simple_if_min.smt2 new file mode 100644 index 000000000..4d304883e --- /dev/null +++ b/bench_adt/simple_if_min.smt2 @@ -0,0 +1,163 @@ +(set-logic HORN) + +(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) +(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) +(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) +(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) +(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) +(declare-fun |interface_0_C_31_0| (Int |abi_type| |crypto_type| |state_type| ) Bool) +(declare-fun |nondet_interface_1_C_31_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool) +(declare-fun |summary_constructor_2_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (state_0 |state_type|) (this_0 Int) (tx_0 |tx_type|)) +(=> (= error_0 0) (nondet_interface_1_C_31_0 error_0 this_0 abi_0 crypto_0 state_0 state_0)))) + + +(declare-fun |summary_3_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |summary_4_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_1 Int)) +(=> (and (and (nondet_interface_1_C_31_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_4_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 a_2_0 state_2 a_2_1 z_5_1))) (nondet_interface_1_C_31_0 error_1 this_0 abi_0 crypto_0 state_0 state_2)))) + + +(declare-fun |block_5_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |block_6_simple_if_29_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) +(block_5_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) +(=> (and (and (block_5_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= a_2_1 a_2_0))) true)) true) (block_6_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(declare-fun |block_7_return_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |block_8_if_header_simple_if_28_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |block_9_if_true_simple_if_18_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |block_10_if_false_simple_if_27_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(declare-fun |block_11_simple_if_29_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) +(=> (and (and (block_6_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_1 0) (and (and (>= a_2_1 0) (<= a_2_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))) true) (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) +(=> (and (and (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_9_1 (< expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 5) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 a_2_1) true)))))) expr_9_1) (block_9_if_true_simple_if_18_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) +(=> (and (and (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_9_1 (< expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 5) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 a_2_1) true)))))) (not expr_9_1)) (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_9_if_true_simple_if_18_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_2 expr_16_0) (and (=> true true) (and (= expr_16_0 0) (and (= a_2_2 expr_14_1) (and (=> true (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 expr_13_1) (and (=> true (and (>= expr_10_0 0) (<= expr_10_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_10_0 a_2_1) (and (=> true (and (>= expr_13_1 0) (<= expr_13_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_1 (+ expr_11_0 expr_12_0)) (and (=> true true) (and (= expr_12_0 1) (and (=> true (and (>= expr_11_0 0) (<= expr_11_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_11_0 a_2_1) true))))))))))))))) true) (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2)))) + + +(declare-fun |block_12_return_ghost_simple_if_17_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_12_return_ghost_simple_if_17_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2) (and (= z_5_2 expr_16_0) (and (=> true true) (and (= expr_16_0 0) (and (= a_2_2 expr_14_1) (and (=> true (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 expr_13_1) (and (=> true (and (>= expr_10_0 0) (<= expr_10_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_10_0 a_2_1) (and (=> true (and (>= expr_13_1 0) (<= expr_13_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_1 (+ expr_11_0 expr_12_0)) (and (=> true true) (and (= expr_12_0 1) (and (=> true (and (>= expr_11_0 0) (<= expr_11_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_11_0 a_2_1) true))))))))))))))) true) (block_11_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2)))) + + +(declare-fun |block_13_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))) (and (not expr_22_1) (= error_1 1))) (block_13_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (block_13_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (summary_3_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_2 expr_25_0) (and (=> true true) (and (= expr_25_0 1) (and (= error_1 error_0) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))))))) true) (block_7_return_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2)))) + + +(declare-fun |block_14_return_ghost_simple_if_26_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_14_return_ghost_simple_if_26_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2) (and (= z_5_2 expr_25_0) (and (=> true true) (and (= expr_25_0 1) (and (= error_1 error_0) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))))))) true) (block_11_simple_if_29_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_11_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) true) true) (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) true) true) (summary_3_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) + + +(declare-fun |block_15_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(block_15_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (block_15_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (summary_3_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 a_2_1 state_3 a_2_2 z_5_1) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3745062286)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 223)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 57)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 29)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 142)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= a_2_1 a_2_0))) true))))))) true) (summary_4_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_3 a_2_2 z_5_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (interface_0_C_31_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (= error_0 0))) (interface_0_C_31_0 this_0 abi_0 crypto_0 state_1)))) + + +(declare-fun |contract_initializer_16_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(declare-fun |contract_initializer_entry_17_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_17_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(declare-fun |contract_initializer_after_init_18_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (contract_initializer_entry_17_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_18_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (contract_initializer_after_init_18_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_16_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(declare-fun |implicit_constructor_entry_19_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_16_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_16_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (summary_constructor_2_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_31_0 this_0 abi_0 crypto_0 state_1)))) + + +(declare-fun |error_target_3_0| () Bool) +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> (and (and (interface_0_C_31_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (= error_0 1))) error_target_3_0))) + + +(assert +(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) +(=> error_target_3_0 false))) +(check-sat) diff --git a/bench_horn_adt/run-bench.sh b/bench_horn_adt/run-bench.sh new file mode 100755 index 000000000..6c8e41157 --- /dev/null +++ b/bench_horn_adt/run-bench.sh @@ -0,0 +1,49 @@ +#!/bin/bash +echo "This is the script for running regression tests" +echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')" +echo " - host name $(hostname -f)" +echo " - script path: $(readlink -f $0)" + +adtchc=../adtchc +if [[ ! $# -eq 0 ]] ; then + #echo 'Setting path to' $1 + adtchc=$1 +fi + +# run the interpolating version of OpenSMT +adtchc=${adtchc}' -i' + +picky=./utils/picky.smt2 +lookahead=./utils/lookahead.smt2 + +tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S') +mkdir ${tmpfolder} + +export outmod=false +export errmod=false +export rtmod=false +export err=false + +for file in $(find . -name '*.smt2' |sort); do + name=$(basename $file) + dir=$(dirname $file) + + sh -c "ulimit -St 60; ${adtchc} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null + grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err + + if [ -s "$tmpfolder/$name.err" ]; then + echo "stderr not empty for benchmark $file"; + err=true; + fi + + +done +#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}" + +if [[ ${err} == true ]]; then + echo "There were anomalies: check logs in ${tmpfolder}" + exit 1 +else + rm -rf ${tmpfolder} +fi + diff --git a/bench_sim/run-bench.sh b/bench_sim/run-bench.sh new file mode 100755 index 000000000..6c8e41157 --- /dev/null +++ b/bench_sim/run-bench.sh @@ -0,0 +1,49 @@ +#!/bin/bash +echo "This is the script for running regression tests" +echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')" +echo " - host name $(hostname -f)" +echo " - script path: $(readlink -f $0)" + +adtchc=../adtchc +if [[ ! $# -eq 0 ]] ; then + #echo 'Setting path to' $1 + adtchc=$1 +fi + +# run the interpolating version of OpenSMT +adtchc=${adtchc}' -i' + +picky=./utils/picky.smt2 +lookahead=./utils/lookahead.smt2 + +tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S') +mkdir ${tmpfolder} + +export outmod=false +export errmod=false +export rtmod=false +export err=false + +for file in $(find . -name '*.smt2' |sort); do + name=$(basename $file) + dir=$(dirname $file) + + sh -c "ulimit -St 60; ${adtchc} $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null + grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err + + if [ -s "$tmpfolder/$name.err" ]; then + echo "stderr not empty for benchmark $file"; + err=true; + fi + + +done +#echo "Stdout differs: ${outmod}, stderr differs: ${errmod}" + +if [[ ${err} == true ]]; then + echo "There were anomalies: check logs in ${tmpfolder}" + exit 1 +else + rm -rf ${tmpfolder} +fi + diff --git a/constructor_selector.smt2 b/constructor_selector.smt2 new file mode 100644 index 000000000..a88460da6 --- /dev/null +++ b/constructor_selector.smt2 @@ -0,0 +1,11 @@ +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) + +(declare-fun bytes_tuple_1 () |bytes_tuple|) + +(declare-fun arr () (Array Int Int)) + +(assert (= bytes_tuple_1 (|bytes_tuple| arr 1))) +(assert (not (= 1 (|bytes_tuple_accessor_length| bytes_tuple_1)))) + +(check-sat) +; should be unsat diff --git a/constructor_selector_helper_assertion.smt2 b/constructor_selector_helper_assertion.smt2 new file mode 100644 index 000000000..784e2f19f --- /dev/null +++ b/constructor_selector_helper_assertion.smt2 @@ -0,0 +1,17 @@ +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) + +(declare-fun uf ((|bytes_tuple|)) Int) +(declare-fun ufa ((|bytes_tuple|)) (Array Int Int)) + +(declare-fun bytes_tuple_1 () |bytes_tuple|) + +(declare-fun arr () (Array Int Int)) + +(assert (= bytes_tuple_1 (|bytes_tuple| arr 1))) +(assert (= 1 (uf bytes_tuple_1))) +(assert (= arr (ufa bytes_tuple_1))) + +(assert (not (= 1 (uf bytes_tuple_1)))) + +(check-sat) +; now, unsat diff --git a/constructor_selector_uf.smt2 b/constructor_selector_uf.smt2 new file mode 100644 index 000000000..a18e899c0 --- /dev/null +++ b/constructor_selector_uf.smt2 @@ -0,0 +1,14 @@ +(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) + +(declare-fun uf ((|bytes_tuple|)) Int) + +(declare-fun bytes_tuple_1 () |bytes_tuple|) + +(declare-fun arr () (Array Int Int)) + +(assert (= bytes_tuple_1 (|bytes_tuple| arr 1))) +(assert (not (= 1 (uf bytes_tuple_1)))) + +(check-sat) +(get-model) +; too much of an approximation, thus sat diff --git a/include/adt/CHCSolver.hpp b/include/adt/CHCSolver.hpp index fec9a2a92..07801a192 100644 --- a/include/adt/CHCSolver.hpp +++ b/include/adt/CHCSolver.hpp @@ -356,6 +356,7 @@ namespace ufo if (std::find(ordered_decls.begin(), ordered_decls.end(), decl) != ordered_decls.end()) return true; cur_decls.insert(decl); +// outs() << decl << "\n ************************ \n"; for (auto & chc : chcs) { if (chc.dstRelation == decl && !chc.isFact) { for (int i = 0; i < chc.srcRelations.size(); i++) { @@ -455,7 +456,14 @@ namespace ufo } // Get the possible version of return variables Expr cur = ordered_decls[idx]; + outs() << "Decls:"; + for (auto decl: ordered_decls){ + outs() << decl << "\n ************************ \n"; + } for (auto & chc : chcs) { + outs() << "Comparison: \n" << chc.dstRelation << "\n" << cur << "\n ************************ \n"; + + if (chc.dstRelation == cur) { size_t vars_size = chc.dstRelation->arity(); std::vector idxs; @@ -465,10 +473,10 @@ namespace ufo // add functions for filter variables here if (ignoreBaseVar) excludeBaseVar(cur, idxs); if (givePriority) givePriorityNonAdt(cur, idxs); - // outs() << *chc.dstRelation->left() << " " << idxs.size() << "\n"; + outs () << *chc.dstRelation->left() << " " << idxs.size() << "\n"; for (int i = idxs.size() - 1; i >= 0; --i) { buf[chc.dstRelation->left()] = idxs[i]; - // outs() << *chc.dstRelation->left() << " " << idxs[i] << "\n"; + outs () << *chc.dstRelation->left() << " " << idxs[i] << "\n"; if (findInterpretations(idx + 1, buf)) return true; } @@ -481,7 +489,7 @@ namespace ufo bool solve() { // Order current uninterpreted predicate symbols for (auto & decl: decls) { - // outs() << *decl << "\n"; + outs() << *decl << "\n"; ExprSet cur_decls; if (!orderDecls(decl, cur_decls)) return false; @@ -583,6 +591,9 @@ namespace ufo ExprVector constructors; ExprSet& decls = ruleManager.decls; + for(auto decl: decls){ + outs () << decl << "\n"; + } for (auto & a : z3.getAdtConstructors()) { constructors.push_back(regularizeQF(a)); diff --git a/include/deep/HornNonlin.hpp b/include/deep/HornNonlin.hpp index ca929a4eb..f8e76830d 100755 --- a/include/deep/HornNonlin.hpp +++ b/include/deep/HornNonlin.hpp @@ -102,12 +102,23 @@ namespace ufo return false; } + bool isAapp (Expr e) + { + if (isOpX(e)) + if (e->arity() > 0) + if (isOpX(e->arg(0))) + if (e->arg(0)->arity() >= 2) + return true; + return false; + } + void splitBody (Expr body, vector& srcVars, ExprVector &srcRelations, ExprSet& lin) { getConj (body, lin); for (auto c = lin.begin(); c != lin.end(); ) { Expr cnj = *c; + outs() << "Cnj: " << cnj << "\n"; if (isOpX(cnj) && isOpX(cnj->left())) { Expr rel = cnj->arg(0); @@ -119,7 +130,19 @@ namespace ufo srcVars.push_back(tmp); c = lin.erase(c); } - else ++c; + else { + if (isOpX(cnj) && isOpX(cnj->left())) + { + Expr rel = cnj->arg(0); + addDecl(rel); + srcRelations.push_back(rel); + ExprVector tmp; + for (auto it = cnj->args_begin()+1, end = cnj->args_end(); it != end; ++it) + tmp.push_back(*it); + srcVars.push_back(tmp); + c = lin.erase(c); + } else ++c; } + } } @@ -228,6 +251,8 @@ namespace ufo Expr body = r->arg(0); Expr head = r->arg(1); + outs() << "Head: " << head << "\n"; + outs() << "Body: " << body << "\n"; vector origSrcSymbs; ExprSet lin; splitBody(body, origSrcSymbs, hr.srcRelations, lin); @@ -299,6 +324,8 @@ namespace ufo hr.assignVarsAndRewrite (origSrcSymbs, tmp, origDstSymbs, invVars[hr.dstRelation]); +// outs() << "Head: " << hr.head << "\n"; + outs() << "Body 1: " << hr.body << "\n"; if ((isOpX(hr.body) && !hr.isQuery) || (hr.srcRelations.size() == 0 && hr.isQuery)) { diff --git a/include/ufo/Expr.hpp b/include/ufo/Expr.hpp index 5cc4c686b..e752886d2 100644 --- a/include/ufo/Expr.hpp +++ b/include/ufo/Expr.hpp @@ -2177,6 +2177,7 @@ namespace expr } }; struct FAPP_PS; + struct AAPP_PS; } NOP_BASE(BindOp) @@ -2185,6 +2186,10 @@ namespace expr NOP(FDECL,"fdecl",PREFIX,BindOp) /** Function application */ NOP(FAPP,"fapp",bind::FAPP_PS,BindOp) + /** Accessor declaration */ + NOP(ADECL,"adecl",PREFIX,BindOp) + /** Accessor application */ + NOP(AAPP,"aapp",bind::AAPP_PS,BindOp) namespace bind { @@ -2237,6 +2242,7 @@ namespace expr } inline bool isFdecl (Expr fdecl) { return isOpX (fdecl); } + inline bool isAdecl (Expr fdecl) { return isOpX (fdecl); } inline Expr fname (Expr fdecl) { return fdecl->first (); } inline Expr fapp (Expr fdecl) { return mk (fdecl); } @@ -2244,10 +2250,19 @@ namespace expr template Expr fapp (Expr fdecl, const Range &args) { - ExprVector _args; - _args.push_back (fdecl); - _args.insert (_args.end (), boost::begin (args), boost::end (args)); - return mknary (_args); + ExprVector _args; + _args.push_back (fdecl); + _args.insert (_args.end (), boost::begin (args), boost::end (args)); + return mknary (_args); + } + + template + Expr aapp (Expr adecl, const Range &args) + { + ExprVector _args; + _args.push_back (adecl); + _args.insert (_args.end (), boost::begin (args), boost::end (args)); + return mknary (_args); } inline Expr fapp (Expr fdecl, Expr a0, Expr a1 = Expr(), @@ -2268,6 +2283,8 @@ namespace expr inline bool isFapp (Expr fapp) { return isOpX (fapp); } + + inline bool isAapp (Expr fapp) { return isOpX (fapp); } inline Expr rangeTy (Expr fdecl) { return fdecl->last (); } @@ -2285,9 +2302,13 @@ namespace expr template bool isFdecl (Expr v) { - return isOpX (v) && isOpX (rangeTy (v)); + return isOpX (v) && isOpX (rangeTy (v)); } - + + template bool isAdecl (Expr v) + { + return isOpX (v) && isOpX (rangeTy (v)); + } /** constant is an applied nullary function */ template bool isConst (Expr v) @@ -2320,6 +2341,12 @@ namespace expr return rangeTy (v->left ()); } + if (isOpX (v)) + { + assert (isOpX (v->left ())); + return rangeTy (v->left ()); + } + if (isOpX(v)) return typeOf(v->last()); if (isOp(v) || isOp (v)) return mk (v->efac ()); if (isOpX (v)) return mk (v->efac ()); @@ -2360,29 +2387,54 @@ namespace expr struct FAPP_PS { - static inline void print (std::ostream &OS, - int depth, - int brkt, - const std::string &name, - const std::vector &args) - { - if (args.size () > 1) OS << "("; + static inline void print (std::ostream &OS, + int depth, + int brkt, + const std::string &name, + const std::vector &args) + { + if (args.size () > 1) OS << "("; - // -- strip fdecl if there is one - ENode *fname = args [0]; - if (isOpX (fname)) fname = fname->arg (0); - fname->Print (OS, depth+2, false); + // -- strip fdecl if there is one + ENode *fname = args [0]; + if (isOpX (fname)) fname = fname->arg (0); + fname->Print (OS, depth+2, false); - for (unsigned i = 1; i < args.size (); ++i) - { - OS << " "; - args [i]->Print (OS, depth+2, false); - } - - if (args.size () > 1) OS << ")"; - } + for (unsigned i = 1; i < args.size (); ++i) + { + OS << " "; + args [i]->Print (OS, depth+2, false); + } + + if (args.size () > 1) OS << ")"; + } }; + + struct AAPP_PS { + static inline void print (std::ostream &OS, + int depth, + int brkt, + const std::string &name, + const std::vector &args) + { + if (args.size () > 1) OS << "("; + + // -- strip fdecl if there is one + ENode *fname = args [0]; + if (isOpX (fname)) fname = fname->arg (0); + fname->Print (OS, depth+2, false); + + for (unsigned i = 1; i < args.size (); ++i) + { + OS << " "; + args [i]->Print (OS, depth+2, false); + } + + if (args.size () > 1) OS << ")"; + } + + }; /// Creates a new fdecl with the same signature as the given /// fdecl and a new name diff --git a/include/ufo/Smt/ZExprConverter.hpp b/include/ufo/Smt/ZExprConverter.hpp index 2f24d0b76..ab0f85c0f 100644 --- a/include/ufo/Smt/ZExprConverter.hpp +++ b/include/ufo/Smt/ZExprConverter.hpp @@ -488,6 +488,7 @@ namespace ufo else if (isOp (e)) { Z3_func_decl fdecl = reinterpret_cast (args[0]); + printf("Func decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); res = Z3_mk_map (ctx, fdecl, e->arity ()-1, &args[1]); } } @@ -578,6 +579,7 @@ namespace ufo for (int i = 0; i < Z3_get_datatype_sort_num_constructors(ctx, sort); i++) { Z3_func_decl decl = Z3_get_datatype_sort_constructor(ctx, sort, i); + printf("Datatype decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, decl))); Z3_ast zdecl = Z3_func_decl_to_ast(ctx, decl); adts.push_back(unmarshal(z3::ast(ctx, zdecl), efac, cache, seen, adts_seen, adts)); } @@ -602,44 +604,46 @@ namespace ufo return bind::bvar (idx, sort); } - else if (kind == Z3_FUNC_DECL_AST) + else if (kind == Z3_FUNC_DECL_AST) { - { - typename C::const_iterator it = cache.find (z); - if (it != cache.end ()) return it->second; - } - Z3_func_decl fdecl = Z3_to_func_decl (ctx, z); + { + typename C::const_iterator it = cache.find (z); + if (it != cache.end ()) return it->second; + } + Z3_func_decl fdecl = Z3_to_func_decl (ctx, z); - Z3_symbol symname = Z3_get_decl_name (ctx, fdecl); - - Expr name; - switch (Z3_get_symbol_kind (ctx, symname)) - { +// printf("Func decl ast: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); + + Z3_symbol symname = Z3_get_decl_name (ctx, fdecl); + + Expr name; + std::string st = Z3_get_symbol_string(ctx, symname) ; + switch (Z3_get_symbol_kind (ctx, symname)) { case Z3_STRING_SYMBOL: name = mkTerm (Z3_get_symbol_string (ctx, symname), efac); break; case Z3_INT_SYMBOL: name = mkTerm (Z3_get_symbol_int (ctx, symname), efac); break; - } - assert (name); - - ExprVector type; - for (unsigned p = 0; p < Z3_get_domain_size (ctx, fdecl); ++p) - { - Z3_sort sort = Z3_get_domain (ctx, fdecl, p); - type.push_back - (unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, sort)), - efac, cache, seen, adts_seen, adts)); - } + } + assert (name); - type.push_back - (unmarshal (z3::ast (ctx, - Z3_sort_to_ast (ctx, - Z3_get_range (ctx, fdecl))), - efac, cache, seen, adts_seen, adts)); + ExprVector type; + for (unsigned p = 0; p < Z3_get_domain_size (ctx, fdecl); ++p) + { + Z3_sort sort = Z3_get_domain (ctx, fdecl, p); + type.push_back + (unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, sort)), + efac, cache, seen, adts_seen, adts)); + } - return bind::fdecl (name, type); + type.push_back + (unmarshal (z3::ast (ctx, + Z3_sort_to_ast (ctx, + Z3_get_range (ctx, fdecl))), + efac, cache, seen, adts_seen, adts)); +// printf("Func dec: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); + return bind::fdecl (name, type); } else if (kind == Z3_QUANTIFIER_AST) { @@ -652,6 +656,8 @@ namespace ufo Z3_get_quantifier_bound_name (ctx, z, i), 0, nullptr, Z3_get_quantifier_bound_sort (ctx, z, i)); + + printf("Quantifier decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, decl))); z3::ast zdecl (ctx, Z3_func_decl_to_ast (ctx, decl)); args.push_back (unmarshal (zdecl, efac, cache, seen, adts_seen, adts)); assert (args.back ().get ()); @@ -752,15 +758,51 @@ namespace ufo (z3::ast(ctx, Z3_get_app_arg(ctx, app, i)), efac, cache, seen, adts_seen, adts)); /** newly introduced Z3 symbol */ - if (dkind == Z3_OP_UNINTERPRETED || dkind == Z3_OP_DT_CONSTRUCTOR) + // TODO: Bind the accessor variable + if (dkind == Z3_OP_UNINTERPRETED || dkind == Z3_OP_DT_CONSTRUCTOR ) { + if(dkind == Z3_OP_DT_ACCESSOR){ + printf("Accessor decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); + } else { + printf("Func app: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); + } Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), efac, cache, seen, adts_seen, adts), args); // -- XXX maybe use seen instead. not sure what is best. cache.insert (typename C::value_type (z, res)); return res; } - + if (dkind == Z3_OP_DT_ACCESSOR) { + Expr res = bind::aapp (unmarshal (z3::func_decl (ctx, fdecl), + efac, cache, seen, adts_seen, adts), args); + // -- XXX maybe use seen instead. not sure what is best. + cache.insert (typename C::value_type (z, res)); + return res; + } +// auto accessor = Z3_to_app(ctx, z); +// auto parameter = Z3_get_app_arg(ctx, accessor, 0); +// auto fdecl1 = Z3_get_app_decl (ctx, accessor); +// auto dkind1 = Z3_get_decl_kind (ctx, fdecl); +// while(Z3_is_app(ctx, parameter)){ +// accessor = Z3_to_app(ctx, parameter); +// parameter = Z3_get_app_arg(ctx, accessor, 0); +// fdecl1 = Z3_get_app_decl (ctx, accessor); +// dkind1 = Z3_get_decl_kind (ctx, fdecl); +// } +// Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), +// efac, cache, seen, adts_seen, adts), args); +// for (size_t i = 0; i < (size_t)Z3_get_app_num_args (ctx, app); i++) +// args.push_back (unmarshal +// (z3::ast(ctx, Z3_get_app_arg(ctx, app, i)), efac, cache, seen, adts_seen, adts)); +// +// unsigned idx = Z3_get_index_value(ctx, parameter); +// assert(idx != 0 && Z3_get_app_num_args(ctx, accessor) == 1); +// z3::ast zsort(ctx, Z3_sort_to_ast(ctx, Z3_get_sort(ctx, z))); +// Expr sort = unmarshal(zsort, efac, cache, seen, adts_seen, adts); +//// Expr res = bind::fapp ( unmarshal (z3::func_decl (ctx, fdecl), +//// efac, cache, seen, adts_seen, adts), bind::bvar(idx, sort)); +// return bind::bvar(idx, sort); +// } switch (dkind) { case Z3_OP_ITE: @@ -913,6 +955,16 @@ namespace ufo case Z3_OP_BASHR: e = mknary (args.begin (), args.end ()); break; +// case Z3_OP_DT_ACCESSOR: +// assert (args.size () == 1); +// Z3_sort sort = Z3_get_sort (ctx, z); +// Expr domain = unmarshal +// (z3::ast (ctx, Z3_sort_to_ast (ctx, +// Z3_get_array_sort_domain (ctx, sort))), +// efac, cache, seen, adts_seen, adts); +// +// e = op::Accessor::instantiate (domain, args[0]); +// break; default: return U::unmarshal (z, efac, cache, seen); } From 4d63c897c2bada4156ef3ba5fc763edf1538d184 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Mon, 10 Jul 2023 17:16:21 +0200 Subject: [PATCH 02/12] Conjuncts: additional conjuncts from adt constructors Conjuncts: removed not needed class of accessors Conjuncts: removed not needed class of accessors Conjuncts: removed not needed class of accessors Conjuncts: removed not needed class of accessors Conjuncts: debugging Conjuncts: debugging --- include/adt/CHCSolver.hpp | 4 +- include/deep/HornNonlin.hpp | 47 ++--- include/ufo/Expr.hpp | 52 ----- include/ufo/Smt/Z3n.hpp | 7 +- include/ufo/Smt/ZExprConverter.hpp | 296 ++++++++++++++++++++--------- 5 files changed, 229 insertions(+), 177 deletions(-) diff --git a/include/adt/CHCSolver.hpp b/include/adt/CHCSolver.hpp index 07801a192..73b3c8dba 100644 --- a/include/adt/CHCSolver.hpp +++ b/include/adt/CHCSolver.hpp @@ -458,10 +458,10 @@ namespace ufo Expr cur = ordered_decls[idx]; outs() << "Decls:"; for (auto decl: ordered_decls){ - outs() << decl << "\n ************************ \n"; +// outs() << decl << "\n ************************ \n"; } for (auto & chc : chcs) { - outs() << "Comparison: \n" << chc.dstRelation << "\n" << cur << "\n ************************ \n"; +// outs() << "Comparison: \n" << chc.dstRelation << "\n" << cur << "\n ************************ \n"; if (chc.dstRelation == cur) { diff --git a/include/deep/HornNonlin.hpp b/include/deep/HornNonlin.hpp index f8e76830d..8250bdab7 100755 --- a/include/deep/HornNonlin.hpp +++ b/include/deep/HornNonlin.hpp @@ -3,6 +3,10 @@ #include "ae/AeValSolver.hpp" + +// TODO: Dirty hack + + using namespace std; using namespace boost; @@ -102,25 +106,24 @@ namespace ufo return false; } - bool isAapp (Expr e) - { - if (isOpX(e)) - if (e->arity() > 0) - if (isOpX(e->arg(0))) - if (e->arg(0)->arity() >= 2) - return true; - return false; - } - void splitBody (Expr body, vector& srcVars, ExprVector &srcRelations, ExprSet& lin) { getConj (body, lin); for (auto c = lin.begin(); c != lin.end(); ) { Expr cnj = *c; - outs() << "Cnj: " << cnj << "\n"; - if (isOpX(cnj) && isOpX(cnj->left())) +// outs() << "Cnj: " << cnj << "\n"; + if (isOpX(cnj)) { + assert(isOpX(cnj->left())); + outs() << "Cnj func: " << cnj << "\n"; + std::string name; + std::stringstream str; + str << cnj; +// if(str.str() == "expr_9_1"){ +// c = lin.erase(c); +// continue; +// } Expr rel = cnj->arg(0); addDecl(rel); srcRelations.push_back(rel); @@ -130,19 +133,7 @@ namespace ufo srcVars.push_back(tmp); c = lin.erase(c); } - else { - if (isOpX(cnj) && isOpX(cnj->left())) - { - Expr rel = cnj->arg(0); - addDecl(rel); - srcRelations.push_back(rel); - ExprVector tmp; - for (auto it = cnj->args_begin()+1, end = cnj->args_end(); it != end; ++it) - tmp.push_back(*it); - srcVars.push_back(tmp); - c = lin.erase(c); - } else ++c; } - + else ++c; } } @@ -290,8 +281,10 @@ namespace ufo ExprVector origDstSymbs; if (!hr.isQuery) { - for (auto it = head->args_begin()+1, end = head->args_end(); it != end; ++it) + for (auto it = head->args_begin()+1, end = head->args_end(); it != end; ++it){ +// outs() << *it << "\n"; origDstSymbs.push_back(*it); + } } allOrigSymbs.insert(allOrigSymbs.end(), origDstSymbs.begin(), origDstSymbs.end()); //simplBoolReplCnj(allOrigSymbs, lin); // perhaps, not a very important optimization now; consider removing @@ -341,6 +334,8 @@ namespace ufo if (isOpX(cnj)) { Expr l = bind::fname(cnj->left()); Expr r = bind::fname(cnj->right()); +// outs() << "Left: " << l << "\n"; +// outs() << "Right: " << r << "\n"; if (std::find(constructors.begin(), constructors.end(), l) != constructors.end()) { for (int i = 0; i < cnj->left()->arity(); ++i) { Expr var = cnj->left()->arg(i); diff --git a/include/ufo/Expr.hpp b/include/ufo/Expr.hpp index e752886d2..3783487fe 100644 --- a/include/ufo/Expr.hpp +++ b/include/ufo/Expr.hpp @@ -2177,7 +2177,6 @@ namespace expr } }; struct FAPP_PS; - struct AAPP_PS; } NOP_BASE(BindOp) @@ -2186,10 +2185,6 @@ namespace expr NOP(FDECL,"fdecl",PREFIX,BindOp) /** Function application */ NOP(FAPP,"fapp",bind::FAPP_PS,BindOp) - /** Accessor declaration */ - NOP(ADECL,"adecl",PREFIX,BindOp) - /** Accessor application */ - NOP(AAPP,"aapp",bind::AAPP_PS,BindOp) namespace bind { @@ -2242,7 +2237,6 @@ namespace expr } inline bool isFdecl (Expr fdecl) { return isOpX (fdecl); } - inline bool isAdecl (Expr fdecl) { return isOpX (fdecl); } inline Expr fname (Expr fdecl) { return fdecl->first (); } inline Expr fapp (Expr fdecl) { return mk (fdecl); } @@ -2256,14 +2250,6 @@ namespace expr return mknary (_args); } - template - Expr aapp (Expr adecl, const Range &args) - { - ExprVector _args; - _args.push_back (adecl); - _args.insert (_args.end (), boost::begin (args), boost::end (args)); - return mknary (_args); - } inline Expr fapp (Expr fdecl, Expr a0, Expr a1 = Expr(), Expr a2 = Expr()) @@ -2283,8 +2269,6 @@ namespace expr inline bool isFapp (Expr fapp) { return isOpX (fapp); } - - inline bool isAapp (Expr fapp) { return isOpX (fapp); } inline Expr rangeTy (Expr fdecl) { return fdecl->last (); } @@ -2305,11 +2289,6 @@ namespace expr return isOpX (v) && isOpX (rangeTy (v)); } - template bool isAdecl (Expr v) - { - return isOpX (v) && isOpX (rangeTy (v)); - } - /** constant is an applied nullary function */ template bool isConst (Expr v) { @@ -2341,12 +2320,6 @@ namespace expr return rangeTy (v->left ()); } - if (isOpX (v)) - { - assert (isOpX (v->left ())); - return rangeTy (v->left ()); - } - if (isOpX(v)) return typeOf(v->last()); if (isOp(v) || isOp (v)) return mk (v->efac ()); if (isOpX (v)) return mk (v->efac ()); @@ -2410,31 +2383,6 @@ namespace expr } }; - - struct AAPP_PS { - static inline void print (std::ostream &OS, - int depth, - int brkt, - const std::string &name, - const std::vector &args) - { - if (args.size () > 1) OS << "("; - - // -- strip fdecl if there is one - ENode *fname = args [0]; - if (isOpX (fname)) fname = fname->arg (0); - fname->Print (OS, depth+2, false); - - for (unsigned i = 1; i < args.size (); ++i) - { - OS << " "; - args [i]->Print (OS, depth+2, false); - } - - if (args.size () > 1) OS << ")"; - } - - }; /// Creates a new fdecl with the same signature as the given /// fdecl and a new name diff --git a/include/ufo/Smt/Z3n.hpp b/include/ufo/Smt/Z3n.hpp index c43980419..e42eb29c8 100644 --- a/include/ufo/Smt/Z3n.hpp +++ b/include/ufo/Smt/Z3n.hpp @@ -189,12 +189,15 @@ namespace ufo Expr z3_from_smtlib_file (Z &z3, const char *fname) { z3::context &ctx = z3.get_ctx (); - - Z3_ast_vector b = Z3_parse_smtlib2_file (ctx, fname, 0, NULL, NULL, 0, NULL, NULL); + Z3_symbol* names; + Z3_ast_vector b = Z3_parse_smtlib2_file (ctx, fname, 0, names, NULL, 0, NULL, NULL); Z3_ast* args = new Z3_ast[Z3_ast_vector_size(ctx, b)]; + printf("Args size: %d \n", Z3_ast_vector_size(ctx, b)); for (unsigned i = 0; i < Z3_ast_vector_size(ctx, b); ++i) { args[i] = Z3_ast_vector_get(ctx, b, i); + Z3_string st = Z3_ast_to_string(ctx, args[i]); + printf("Ast: %d \n", st); } z3::ast ast (ctx, Z3_mk_and(ctx, Z3_ast_vector_size(ctx, b), args)); diff --git a/include/ufo/Smt/ZExprConverter.hpp b/include/ufo/Smt/ZExprConverter.hpp index ab0f85c0f..5b070671f 100644 --- a/include/ufo/Smt/ZExprConverter.hpp +++ b/include/ufo/Smt/ZExprConverter.hpp @@ -207,9 +207,9 @@ namespace ufo { z3::func_decl zfdecl (ctx, - reinterpret_cast - (static_cast - (marshal (bind::fname (e), ctx, cache, seen)))); + reinterpret_cast + (static_cast + (marshal (bind::fname (e), ctx, cache, seen)))); // -- marshall all arguments except for the first one @@ -507,6 +507,8 @@ namespace ufo } }; + static Expr left; + template struct BasicExprUnmarshal { @@ -548,29 +550,43 @@ namespace ufo Expr domain, range; switch (Z3_get_sort_kind (ctx, sort)) - { - case Z3_BOOL_SORT: - return sort::boolTy (efac); - case Z3_INT_SORT: - return sort::intTy (efac); - case Z3_REAL_SORT: - return sort::realTy (efac); - case Z3_BV_SORT: - return bv::bvsort (Z3_get_bv_sort_size (ctx, sort), efac); - case Z3_ARRAY_SORT: - domain = - unmarshal (z3::ast (ctx, - Z3_sort_to_ast - (ctx, Z3_get_array_sort_domain (ctx, sort))), - efac, cache, seen, adts_seen, adts); - range = - unmarshal (z3::ast (ctx, - Z3_sort_to_ast - (ctx, Z3_get_array_sort_range (ctx, sort))), - efac, cache, seen, adts_seen, adts); - return sort::arrayTy (domain, range); + { + case Z3_BOOL_SORT: + return sort::boolTy (efac); + case Z3_INT_SORT: + return sort::intTy (efac); + case Z3_REAL_SORT: + return sort::realTy (efac); + case Z3_BV_SORT: + return bv::bvsort (Z3_get_bv_sort_size (ctx, sort), efac); + case Z3_ARRAY_SORT: + domain = + unmarshal (z3::ast (ctx, + Z3_sort_to_ast + (ctx, Z3_get_array_sort_domain (ctx, sort))), + efac, cache, seen, adts_seen, adts); + range = + unmarshal (z3::ast (ctx, + Z3_sort_to_ast + (ctx, Z3_get_array_sort_range (ctx, sort))), + efac, cache, seen, adts_seen, adts); + return sort::arrayTy (domain, range); case Z3_DATATYPE_SORT: { +// std::cout << "datatype " << Z3_get_symbol_string(ctx, Z3_get_sort_name(ctx, sort)) << "\n"; + unsigned num = Z3_get_datatype_sort_num_constructors(ctx, sort); + while (num > 0) { + num--; + auto c = Z3_get_datatype_sort_constructor(ctx, sort, num); + unsigned num_accessors = Z3_get_domain_size(ctx, c); + + std::cout << "constructor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,c)) << " " << "\n"; + while(num_accessors > 0){ + num_accessors--; + auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors); + std::cout << "accessor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,as)) << "\n"; + } + } std::string name = Z3_get_symbol_string(ctx, Z3_get_sort_name(ctx, sort)); Expr adt_name = mkTerm (name, efac); if (find(adts_seen.begin(), adts_seen.end(), name) == adts_seen.end()) @@ -579,14 +595,50 @@ namespace ufo for (int i = 0; i < Z3_get_datatype_sort_num_constructors(ctx, sort); i++) { Z3_func_decl decl = Z3_get_datatype_sort_constructor(ctx, sort, i); - printf("Datatype decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, decl))); +// printf("Datatype decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, decl))); Z3_ast zdecl = Z3_func_decl_to_ast(ctx, decl); adts.push_back(unmarshal(z3::ast(ctx, zdecl), efac, cache, seen, adts_seen, adts)); + unsigned num_accessors = Z3_get_domain_size(ctx, decl); + +// std::cout << "constructor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,c)) << " " << "\n"; + while(num_accessors > 0){ + num_accessors--; + auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors); + auto symname = Z3_get_decl_name(ctx,as); + Expr name; + std::string st = Z3_get_symbol_string(ctx, symname) ; + switch (Z3_get_symbol_kind (ctx, symname)) { + case Z3_STRING_SYMBOL: + name = mkTerm (Z3_get_symbol_string (ctx, symname), efac); + break; + case Z3_INT_SYMBOL: + name = mkTerm (Z3_get_symbol_int (ctx, symname), efac); + break; + } + assert (name); + + ExprVector type; + for (unsigned p = 0; p < Z3_get_domain_size (ctx, as); ++p) + { + Z3_sort sort = Z3_get_domain (ctx, as, p); + type.push_back + (unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, sort)), + efac, cache, seen, adts_seen, adts)); + } + + type.push_back + (unmarshal (z3::ast (ctx, + Z3_sort_to_ast (ctx, + Z3_get_range (ctx, as))), + efac, cache, seen, adts_seen, adts)); +// printf("Func dec: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); + return bind::fdecl (name, type); + } } } return sort::adTy (adt_name); } - default: + default: std::string name = Z3_get_symbol_string(ctx, Z3_get_sort_name(ctx, sort)); Expr adt_name = mkTerm (name, efac); if (find(adts_seen.begin(), adts_seen.end(), name) == adts_seen.end()) @@ -594,8 +646,8 @@ namespace ufo adts_seen.push_back(name); } return sort::adTy (adt_name); - } - } + } +} else if (kind == Z3_VAR_AST) { unsigned idx = Z3_get_index_value (ctx, z); @@ -753,29 +805,83 @@ namespace ufo Expr e; ExprVector args; - for (size_t i = 0; i < (size_t)Z3_get_app_num_args (ctx, app); i++) - args.push_back (unmarshal - (z3::ast(ctx, Z3_get_app_arg(ctx, app, i)), efac, cache, seen, adts_seen, adts)); + for (size_t i = 0; i < (size_t)Z3_get_app_num_args (ctx, app); i++){ + if(dkind == Z3_OP_EQ && i == 1 && Z3_get_decl_kind (ctx, Z3_get_app_decl (ctx, Z3_to_app(ctx, z3::ast(ctx, Z3_get_app_arg(ctx, app, i))))) == Z3_OP_DT_CONSTRUCTOR){ + left = args[0]; + printf("We are in the state of eq with constructor\n"); + } + args.push_back (unmarshal + (z3::ast(ctx, Z3_get_app_arg(ctx, app, i)), efac, cache, seen, adts_seen, adts)); + } - /** newly introduced Z3 symbol */ - // TODO: Bind the accessor variable - if (dkind == Z3_OP_UNINTERPRETED || dkind == Z3_OP_DT_CONSTRUCTOR ) + + /** newly introduced Z3 symbol */ + // TODO: Bind the accessor variable + if (dkind == Z3_OP_DT_CONSTRUCTOR ) { - if(dkind == Z3_OP_DT_ACCESSOR){ - printf("Accessor decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); - } else { - printf("Func app: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); - } - Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), - efac, cache, seen, adts_seen, adts), args); - // -- XXX maybe use seen instead. not sure what is best. - cache.insert (typename C::value_type (z, res)); - return res; + + ExprVector subexpr; + if (left != NULL) { + Z3_sort sort = Z3_get_sort (ctx, z); + unsigned num = Z3_get_datatype_sort_num_constructors(ctx, sort); + while (num > 0) { + num--; + auto c = Z3_get_datatype_sort_constructor(ctx, sort, num); + unsigned num_accessors = Z3_get_domain_size(ctx, c); + if(c != fdecl){ + continue; + } + + outs() << "Datatype constructor constructor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,c)) << " " << "\n"; + while(num_accessors > 0){ + num_accessors--; + auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors); + ExprVector eq; + outs() << "Datatype constructor accessor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,as)) << "\n"; + outs() << "Accessor parameter: " << left << "\n"; + // TODO: represent it as a fapp, not fdecl; + // TODO: left part should be ast? Or smth else? NEED TO CHECK IF LEFT IS ASSIGNED!!! + // Put function call: accessor(data) into equality + eq.push_back (bind::fapp (unmarshal (z3::func_decl (ctx, as), + efac, cache, seen, adts_seen, adts), { left })); + // Put value from the constructor into equality + eq.push_back (args[num_accessors]); + // TODO: Get the second part of the equality higher up, so we can set some funcs + // accessor(data) = value + subexpr.push_back(mknary (eq.begin(), eq.end())); + } + } + } + + Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), + efac, cache, seen, adts_seen, adts), args); + subexpr.push_back(res); + Expr final = mknary (subexpr.begin(), subexpr.end()); + outs()<<"Resulting expression: " << final << "\n"; + for(auto expr: subexpr){ + outs()<<"Subexpression: " << expr << "\n"; + } + printf("Datatype constructor decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); + cache.insert (typename C::value_type (z, res)); + left = NULL; + return final; } + + if (dkind == Z3_OP_UNINTERPRETED) { + printf("Func app: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); + Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), + efac, cache, seen, adts_seen, adts), args); + // -- XXX maybe use seen instead. not sure what is best. + cache.insert (typename C::value_type (z, res)); + return res; + } + if (dkind == Z3_OP_DT_ACCESSOR) { - Expr res = bind::aapp (unmarshal (z3::func_decl (ctx, fdecl), + Z3_sort srt = Z3_get_sort(ctx, z); + Z3_func_decl acc = Z3_get_datatype_sort_constructor_accessor(ctx, srt,1,1); + Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), efac, cache, seen, adts_seen, adts), args); - // -- XXX maybe use seen instead. not sure what is best. +// -- XXX maybe use seen instead. not sure what is best. cache.insert (typename C::value_type (z, res)); return res; } @@ -803,59 +909,59 @@ namespace ufo //// efac, cache, seen, adts_seen, adts), bind::bvar(idx, sort)); // return bind::bvar(idx, sort); // } - switch (dkind) + switch (dkind) { - case Z3_OP_ITE: - e = mknary (args.begin (), args.end ()); - break; - case Z3_OP_AND: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_OR: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_XOR: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_IFF: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_IMPLIES: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_EQ: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_LT: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_GT: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_LE: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_GE: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_ADD: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_SUB: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_MUL: - e = mknary (args.begin(), args.end()); - break; - case Z3_OP_DIV: - e = mknary
(args.begin(), args.end()); - break; + case Z3_OP_ITE: + e = mknary (args.begin (), args.end ()); + break; + case Z3_OP_AND: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_OR: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_XOR: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_IFF: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_IMPLIES: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_EQ: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_LT: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_GT: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_LE: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_GE: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_ADD: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_SUB: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_MUL: + e = mknary (args.begin(), args.end()); + break; + case Z3_OP_DIV: + e = mknary
(args.begin(), args.end()); + break; case Z3_OP_IDIV: e = mknary (args.begin (), args.end ()); break; - case Z3_OP_MOD: - e = mknary (args.begin (), args.end ()); - break; + case Z3_OP_MOD: + e = mknary (args.begin (), args.end ()); + break; case Z3_OP_REM: e = mknary (args.begin (), args.end ()); break; From 8f18c7ac0d84db6f45a4ad6f833edd10e6fb89ab Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Thu, 13 Jul 2023 10:52:43 +0200 Subject: [PATCH 03/12] Conjuncts: hotfix(conjunctions should be level higher) Conjuncts: TODO Constructor additions: found a place to edit matching between accessors and vars Constructor additions: hacky tamp solution --- bench_adt/heap_insert_eq.smt2 | 43 ++++++++++ bench_adt/list_constructor_check.smt2 | 0 include/adt/CHCSolver.hpp | 13 ++- include/ufo/Expr.hpp | 72 +++++++++------- include/ufo/Smt/ZExprConverter.hpp | 119 ++++++++++++++------------ 5 files changed, 159 insertions(+), 88 deletions(-) create mode 100644 bench_adt/heap_insert_eq.smt2 create mode 100644 bench_adt/list_constructor_check.smt2 diff --git a/bench_adt/heap_insert_eq.smt2 b/bench_adt/heap_insert_eq.smt2 new file mode 100644 index 000000000..aca7e872f --- /dev/null +++ b/bench_adt/heap_insert_eq.smt2 @@ -0,0 +1,43 @@ +(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) + +(declare-datatypes () ((Heap (hleaf) (heap (rk Int) (value Int) (hleft Heap) (hright Heap))))) +(declare-fun rightHeight (Heap) Int) +(assert (= (rightHeight hleaf) 0)) +(assert (forall ((k Int) (v Int) (l Heap) (r Heap)) (= (rightHeight (heap k v l r)) (+ 1 (rightHeight r))))) + +(declare-fun rank (Heap) Int) +(assert (= (rank hleaf) 0)) +(assert (forall ((k Int) (v Int) (l Heap) (r Heap)) (= (rank (heap k v l r)) k))) + +(declare-fun hasLeftistProperty (Heap) Bool) +(assert (hasLeftistProperty hleaf)) +(assert (forall ((k Int) (v Int) (l Heap) (r Heap)) + (= (hasLeftistProperty (heap k v l r)) + (and (hasLeftistProperty l) (hasLeftistProperty r) + (<= (rightHeight r) (rightHeight l)) + (= k (+ 1 (rightHeight r))))))) + +(declare-fun hsize (Heap) Int) +(assert (= (hsize hleaf) 0)) +(assert (forall ((k Int) (v Int) (l Heap) (r Heap)) (= (hsize (heap k v l r)) (+ 1 (+ (hsize l) (hsize r)))))) + +(declare-fun mergea (Int Heap Heap) Heap) +(assert (forall ((v Int) (l Heap) (r Heap)) + (= (mergea v l r) (ite (<= (rank r) (rank l)) (heap (+ 1 (rank r)) v l r) (heap (+ 1 (rank l)) v r l))))) + +(declare-fun merge (Heap Heap) Heap) +(assert (forall ((h Heap)) (= (merge h hleaf) h))) +(assert (forall ((h Heap)) (= (merge hleaf h) h))) +(assert (forall ((k1 Int) (v1 Int) (l1 Heap) (r1 Heap) (k2 Int) (v2 Int) (l2 Heap) (r2 Heap)) + (= (merge (heap k1 v1 l1 r1) (heap k2 v2 l2 r2)) + (ite (< v2 v1) (mergea v1 l1 (merge r1 (heap k2 v2 l2 r2))) + (mergea v2 l2 (merge (heap k1 v1 l1 r1) r2)))))) + +(declare-fun hinsert (Heap Int) Heap) +(assert (forall ((h Heap) (n Int)) (= (hinsert h n) (merge (heap 1 n hleaf hleaf) h)))) + +; extra lemmas +(assert (forall ((x Heap)) (>= (hsize x) 0))) + +(assert (not (forall ((x Heap) (n Int)) (=> (hasLeftistProperty x) (hasLeftistProperty (hinsert x n)))))) +(check-sat) diff --git a/bench_adt/list_constructor_check.smt2 b/bench_adt/list_constructor_check.smt2 new file mode 100644 index 000000000..e69de29bb diff --git a/include/adt/CHCSolver.hpp b/include/adt/CHCSolver.hpp index 73b3c8dba..e226169f2 100644 --- a/include/adt/CHCSolver.hpp +++ b/include/adt/CHCSolver.hpp @@ -92,12 +92,15 @@ namespace ufo } } } + // TODO: HERE I CAN CHECK IF ACCESSOR, AND THEN DO THE REVERSE MATCHING, SO HEAD(SMTH) -> X, NOT X -> HEAD(SMTH) if ((elem->left()->arity() == 1) && !(isConstructor(bind::fname(elem->left())))) { - matching[elem->left()] = elem->right(); + matching[elem->right()] = elem->left(); +// matching[elem->left()] = elem->right(); return true; } else if ((elem->right()->arity() == 1) && !(isConstructor(bind::fname(elem->right())))) { - matching[elem->right()] = elem->left(); + matching[elem->left()] = elem->right(); +// matching[elem->right()] = elem->left(); return true; } return false; @@ -154,10 +157,14 @@ namespace ufo } replaceDeclsInLeftPart(chc, cnj); cnj.push_back(chc.body); +// outs() << "CHC: " << chc. << "\n"; + outs() << "CHC: " << chc.body << "\n"; Expr asmpt = mk(conjoin(cnj, efac), destination); + outs() << "Asmpt: " << asmpt << "\n"; while (!isOpX(asmpt) && findMatchingFromRule(chc, matching, asmpt)) { asmpt = replaceAll(asmpt, matching); asmpt = simplifyBool(asmpt); +// outs() << "Asmpt: " << asmpt << "\n"; matching.clear(); } asmpt = simplifyArithm(asmpt); @@ -195,6 +202,7 @@ namespace ufo // we should check that this variable is inductive in inductive rule for (auto & ind_chc : chcs) { + outs() << "Check chc: " << ind_chc.body << "\n"; if (ind_chc.dstRelation == decl && !ind_chc.isFact) { for (int k = 0; k < ind_chc.srcRelations.size(); ++k) { if (ind_chc.srcRelations[k] == decl) { @@ -214,6 +222,7 @@ namespace ufo if ((ind_body_elem->left() == ind_chc.dstVars[i] && ind_body_elem->right()->arity() == indConstructorArity) || (ind_body_elem->right() == ind_chc.dstVars[i] && ind_body_elem->left()->arity() == indConstructorArity)) { shouldBeChecked = true; + break; } } } diff --git a/include/ufo/Expr.hpp b/include/ufo/Expr.hpp index 3783487fe..2e569860d 100644 --- a/include/ufo/Expr.hpp +++ b/include/ufo/Expr.hpp @@ -1148,9 +1148,8 @@ namespace expr { if (expr->use_count () > 1) { - DagVisitCache::const_iterator cit - = cache.find (&*expr); - if (cit != cache.end ()) return cit->second; + DagVisitCache::const_iterator cit = cache.find (&*expr); + if (cit != cache.end ()) return cit->second; } @@ -1163,39 +1162,41 @@ namespace expr res = va.getExpr (); else { - res = va.isChangeDoKidsRewrite () ? va.getExpr () : expr; - if (res->arity () > 0) - { - bool changed = false; - std::vector kids; - - for (ENode::args_iterator b = res->args_begin (), - e = res->args_end (); - b != e; ++b) - { - Expr k = visit (v, *b, cache); - kids.push_back (k); - changed = (changed || k.get () != *b); - } - - if (changed) - { - if (!res->isMutable ()) - res = res->getFactory ().mkNary (res->op (), - kids.begin (), - kids.end ()); - else - res->renew_args (kids.begin (), kids.end ()); - } - } + res = va.isChangeDoKidsRewrite () ? va.getExpr () : expr; +// std::cout << "Res: " << res << "\n"; + if (res->arity () > 0) + { + bool changed = false; + std::vector kids; + + for (ENode::args_iterator b = res->args_begin (), e = res->args_end (); b != e; ++b) + { +// std::cout << "B: " << *b << "\n"; + Expr k = visit (v, *b, cache); + kids.push_back (k); +// std::cout << "k: " << k << "\n"; + changed = (changed || k.get () != *b); + } + + if (changed) + { + if (!res->isMutable ()) + res = res->getFactory ().mkNary (res->op (), + kids.begin (), + kids.end ()); + else + res->renew_args (kids.begin (), kids.end ()); + std::cout << "New res: " << res << "\n"; + } + } - res = va.rewrite (res); + res = va.rewrite (res); } if (expr->use_count () > 1) { - expr->Ref (); - cache[&*expr] = res; + expr->Ref (); + cache[&*expr] = res; } return res; @@ -3050,7 +3051,16 @@ namespace expr } if (m.empty()) return exp; RAVALLM rav(&m); + int s = exp->arity(); + std::cout << "Exp: " << exp << "\n"; Expr tmp = dagVisit (rav, exp); + // TODO :: really dirty, redo + // TODO: Problem is in the recursive overwrite of the constructor + int s1 = tmp->arity(); + std::cout << "Tmp: " << tmp << "\n"; + if(s == s1){ + std::cout << "Arity hasn't changed\n"; + } if (tmp == exp || !rec) return tmp; else return replaceAll(tmp, m, rec, iter+1); } diff --git a/include/ufo/Smt/ZExprConverter.hpp b/include/ufo/Smt/ZExprConverter.hpp index 5b070671f..b8b931fad 100644 --- a/include/ufo/Smt/ZExprConverter.hpp +++ b/include/ufo/Smt/ZExprConverter.hpp @@ -508,8 +508,10 @@ namespace ufo }; static Expr left; + ExprVector subexpr; - template + + template struct BasicExprUnmarshal { template @@ -598,42 +600,42 @@ namespace ufo // printf("Datatype decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, decl))); Z3_ast zdecl = Z3_func_decl_to_ast(ctx, decl); adts.push_back(unmarshal(z3::ast(ctx, zdecl), efac, cache, seen, adts_seen, adts)); - unsigned num_accessors = Z3_get_domain_size(ctx, decl); - -// std::cout << "constructor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,c)) << " " << "\n"; - while(num_accessors > 0){ - num_accessors--; - auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors); - auto symname = Z3_get_decl_name(ctx,as); - Expr name; - std::string st = Z3_get_symbol_string(ctx, symname) ; - switch (Z3_get_symbol_kind (ctx, symname)) { - case Z3_STRING_SYMBOL: - name = mkTerm (Z3_get_symbol_string (ctx, symname), efac); - break; - case Z3_INT_SYMBOL: - name = mkTerm (Z3_get_symbol_int (ctx, symname), efac); - break; - } - assert (name); - - ExprVector type; - for (unsigned p = 0; p < Z3_get_domain_size (ctx, as); ++p) - { - Z3_sort sort = Z3_get_domain (ctx, as, p); - type.push_back - (unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, sort)), - efac, cache, seen, adts_seen, adts)); - } - - type.push_back - (unmarshal (z3::ast (ctx, - Z3_sort_to_ast (ctx, - Z3_get_range (ctx, as))), - efac, cache, seen, adts_seen, adts)); -// printf("Func dec: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); - return bind::fdecl (name, type); - } +// unsigned num_accessors = Z3_get_domain_size(ctx, decl); +// +//// std::cout << "constructor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,c)) << " " << "\n"; +// while(num_accessors > 0){ +// num_accessors--; +// auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors); +// auto symname = Z3_get_decl_name(ctx,as); +// Expr name; +// std::string st = Z3_get_symbol_string(ctx, symname) ; +// switch (Z3_get_symbol_kind (ctx, symname)) { +// case Z3_STRING_SYMBOL: +// name = mkTerm (Z3_get_symbol_string (ctx, symname), efac); +// break; +// case Z3_INT_SYMBOL: +// name = mkTerm (Z3_get_symbol_int (ctx, symname), efac); +// break; +// } +// assert (name); +// +// ExprVector type; +// for (unsigned p = 0; p < Z3_get_domain_size (ctx, as); ++p) +// { +// Z3_sort sort = Z3_get_domain (ctx, as, p); +// type.push_back +// (unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, sort)), +// efac, cache, seen, adts_seen, adts)); +// } +// +// type.push_back +// (unmarshal (z3::ast (ctx, +// Z3_sort_to_ast (ctx, +// Z3_get_range (ctx, as))), +// efac, cache, seen, adts_seen, adts)); +//// printf("Func dec: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); +// return bind::fdecl (name, type); +// } } } return sort::adTy (adt_name); @@ -806,6 +808,7 @@ namespace ufo Expr e; ExprVector args; for (size_t i = 0; i < (size_t)Z3_get_app_num_args (ctx, app); i++){ + // TODO: Disequality, constructor inside constructor(maybe), IF then else if(dkind == Z3_OP_EQ && i == 1 && Z3_get_decl_kind (ctx, Z3_get_app_decl (ctx, Z3_to_app(ctx, z3::ast(ctx, Z3_get_app_arg(ctx, app, i))))) == Z3_OP_DT_CONSTRUCTOR){ left = args[0]; printf("We are in the state of eq with constructor\n"); @@ -819,8 +822,6 @@ namespace ufo // TODO: Bind the accessor variable if (dkind == Z3_OP_DT_CONSTRUCTOR ) { - - ExprVector subexpr; if (left != NULL) { Z3_sort sort = Z3_get_sort (ctx, z); unsigned num = Z3_get_datatype_sort_num_constructors(ctx, sort); @@ -839,32 +840,29 @@ namespace ufo ExprVector eq; outs() << "Datatype constructor accessor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,as)) << "\n"; outs() << "Accessor parameter: " << left << "\n"; - // TODO: represent it as a fapp, not fdecl; - // TODO: left part should be ast? Or smth else? NEED TO CHECK IF LEFT IS ASSIGNED!!! - // Put function call: accessor(data) into equality - eq.push_back (bind::fapp (unmarshal (z3::func_decl (ctx, as), - efac, cache, seen, adts_seen, adts), { left })); - // Put value from the constructor into equality + // Put value from the constructor into equality + eq.push_back (bind::fapp (unmarshal (z3::func_decl (ctx, as), + efac, cache, seen, adts_seen, adts), { left })); eq.push_back (args[num_accessors]); - // TODO: Get the second part of the equality higher up, so we can set some funcs // accessor(data) = value subexpr.push_back(mknary (eq.begin(), eq.end())); - } + } } } Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), efac, cache, seen, adts_seen, adts), args); - subexpr.push_back(res); - Expr final = mknary (subexpr.begin(), subexpr.end()); - outs()<<"Resulting expression: " << final << "\n"; - for(auto expr: subexpr){ - outs()<<"Subexpression: " << expr << "\n"; - } - printf("Datatype constructor decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); +// subexpr.push_back(res); +// Expr final; +// if(subexpr.size() > 0) final = mknary (subexpr.begin(), subexpr.end()); +// outs()<<"Resulting expression: " << final << "\n"; +// for(auto expr: subexpr){ +// outs()<<"Subexpression: " << expr << "\n"; +// } + outs() << "Datatype constructor decl: " << res << "\n"; cache.insert (typename C::value_type (z, res)); left = NULL; - return final; + return res; } if (dkind == Z3_OP_UNINTERPRETED) { @@ -931,6 +929,17 @@ namespace ufo break; case Z3_OP_EQ: e = mknary (args.begin(), args.end()); + if(subexpr.size() > 0){ + subexpr.push_back(e); + +// std::reverse(subexpr.begin(), subexpr.end()); + e = mknary(subexpr.begin(), subexpr.end()); + for(int i = subexpr.size(); i>0 ; i--){ + outs()<<"Subexpression: " << subexpr[i - 1] << "\n"; + } + subexpr.clear(); + outs()<<"Resulting expression: " << e << "\n"; + } break; case Z3_OP_LT: e = mknary (args.begin(), args.end()); From e17c8bde2ae70756896ab76fc9337e9ef7bbf7df Mon Sep 17 00:00:00 2001 From: Konstantin Date: Mon, 14 Aug 2023 17:40:27 +0300 Subject: [PATCH 04/12] Accessors: propper accessor processing is added Accessors: removed comments in CHCSolver Accessors: removed comments in CHCSolver Accessors: removed comments and prints in CHCSolver Accessors: quick replacement fix(it is possible that constructor is done with function call inside, so arity is not necessary 1) --- constructor_selector.smt2 | 11 -- constructor_selector_helper_assertion.smt2 | 17 --- constructor_selector_uf.smt2 | 14 -- include/adt/CHCSolver.hpp | 52 ++++---- include/deep/HornNonlin.hpp | 23 +--- include/ufo/Expr.hpp | 13 -- include/ufo/Smt/Z3n.hpp | 11 +- include/ufo/Smt/ZExprConverter.hpp | 148 +++++---------------- 8 files changed, 64 insertions(+), 225 deletions(-) delete mode 100644 constructor_selector.smt2 delete mode 100644 constructor_selector_helper_assertion.smt2 delete mode 100644 constructor_selector_uf.smt2 diff --git a/constructor_selector.smt2 b/constructor_selector.smt2 deleted file mode 100644 index a88460da6..000000000 --- a/constructor_selector.smt2 +++ /dev/null @@ -1,11 +0,0 @@ -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) - -(declare-fun bytes_tuple_1 () |bytes_tuple|) - -(declare-fun arr () (Array Int Int)) - -(assert (= bytes_tuple_1 (|bytes_tuple| arr 1))) -(assert (not (= 1 (|bytes_tuple_accessor_length| bytes_tuple_1)))) - -(check-sat) -; should be unsat diff --git a/constructor_selector_helper_assertion.smt2 b/constructor_selector_helper_assertion.smt2 deleted file mode 100644 index 784e2f19f..000000000 --- a/constructor_selector_helper_assertion.smt2 +++ /dev/null @@ -1,17 +0,0 @@ -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) - -(declare-fun uf ((|bytes_tuple|)) Int) -(declare-fun ufa ((|bytes_tuple|)) (Array Int Int)) - -(declare-fun bytes_tuple_1 () |bytes_tuple|) - -(declare-fun arr () (Array Int Int)) - -(assert (= bytes_tuple_1 (|bytes_tuple| arr 1))) -(assert (= 1 (uf bytes_tuple_1))) -(assert (= arr (ufa bytes_tuple_1))) - -(assert (not (= 1 (uf bytes_tuple_1)))) - -(check-sat) -; now, unsat diff --git a/constructor_selector_uf.smt2 b/constructor_selector_uf.smt2 deleted file mode 100644 index a18e899c0..000000000 --- a/constructor_selector_uf.smt2 +++ /dev/null @@ -1,14 +0,0 @@ -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) - -(declare-fun uf ((|bytes_tuple|)) Int) - -(declare-fun bytes_tuple_1 () |bytes_tuple|) - -(declare-fun arr () (Array Int Int)) - -(assert (= bytes_tuple_1 (|bytes_tuple| arr 1))) -(assert (not (= 1 (uf bytes_tuple_1)))) - -(check-sat) -(get-model) -; too much of an approximation, thus sat diff --git a/include/adt/CHCSolver.hpp b/include/adt/CHCSolver.hpp index e226169f2..d86fdf398 100644 --- a/include/adt/CHCSolver.hpp +++ b/include/adt/CHCSolver.hpp @@ -18,6 +18,7 @@ namespace ufo // Keep the current return values std::map values_inds; ExprVector &constructors; + ExprVector &accessors; ExprVector &assumptions; ExprSet &decls; @@ -35,8 +36,8 @@ namespace ufo map interpretations; public: - CHCSolver(ExprVector& _constructors, ExprSet& _adts, ExprFactory &_efac, ExprSet &_decls, ExprVector &_assms, vector &_chcs, bool _nonadtPriority = false, bool _ignoreBase = false) : - constructors(_constructors), adts(_adts), efac(_efac), decls(_decls), assumptions(_assms), chcs(_chcs), givePriority(_nonadtPriority), ignoreBaseVar(_ignoreBase) {} + CHCSolver(ExprVector& _constructors, ExprVector& _accessors, ExprSet& _adts, ExprFactory &_efac, ExprSet &_decls, ExprVector &_assms, vector &_chcs, bool _nonadtPriority = false, bool _ignoreBase = false) : + constructors(_constructors), accessors(_accessors), adts(_adts), efac(_efac), decls(_decls), assumptions(_assms), chcs(_chcs), givePriority(_nonadtPriority), ignoreBaseVar(_ignoreBase) {} Expr createNewApp(HornRuleExt chc, int i, int ind) { ExprVector types; @@ -92,15 +93,23 @@ namespace ufo } } } + // TODO: HERE I NEED TO CHECK IF WHAT I HAVE ON THE RIGHT IS AN ACCESSOR + if ((elem->right()->arity() == 2) && isAccessor(bind::fname(elem->right()))) { + matching[elem->right()] = elem->left(); + return true; + } + + else if ((elem->left()->arity() == 2) && isAccessor(bind::fname(elem->left()))) { + matching[elem->left()] = elem->right(); + return true; + } // TODO: HERE I CAN CHECK IF ACCESSOR, AND THEN DO THE REVERSE MATCHING, SO HEAD(SMTH) -> X, NOT X -> HEAD(SMTH) if ((elem->left()->arity() == 1) && !(isConstructor(bind::fname(elem->left())))) { - matching[elem->right()] = elem->left(); -// matching[elem->left()] = elem->right(); + matching[elem->left()] = elem->right(); return true; } else if ((elem->right()->arity() == 1) && !(isConstructor(bind::fname(elem->right())))) { - matching[elem->left()] = elem->right(); -// matching[elem->right()] = elem->left(); + matching[elem->right()] = elem->left(); return true; } return false; @@ -130,6 +139,11 @@ namespace ufo return std::find(constructors.begin(), constructors.end(), elem) != constructors.end(); } + + bool isAccessor(Expr elem) { + return std::find(accessors.begin(), accessors.end(), fname(elem)) != accessors.end(); + } + Expr createDestination(HornRuleExt chc) { int ind = values_inds[chc.dstRelation->left()]; ExprVector types; @@ -157,14 +171,10 @@ namespace ufo } replaceDeclsInLeftPart(chc, cnj); cnj.push_back(chc.body); -// outs() << "CHC: " << chc. << "\n"; - outs() << "CHC: " << chc.body << "\n"; Expr asmpt = mk(conjoin(cnj, efac), destination); - outs() << "Asmpt: " << asmpt << "\n"; while (!isOpX(asmpt) && findMatchingFromRule(chc, matching, asmpt)) { asmpt = replaceAll(asmpt, matching); asmpt = simplifyBool(asmpt); -// outs() << "Asmpt: " << asmpt << "\n"; matching.clear(); } asmpt = simplifyArithm(asmpt); @@ -202,7 +212,6 @@ namespace ufo // we should check that this variable is inductive in inductive rule for (auto & ind_chc : chcs) { - outs() << "Check chc: " << ind_chc.body << "\n"; if (ind_chc.dstRelation == decl && !ind_chc.isFact) { for (int k = 0; k < ind_chc.srcRelations.size(); ++k) { if (ind_chc.srcRelations[k] == decl) { @@ -222,7 +231,6 @@ namespace ufo if ((ind_body_elem->left() == ind_chc.dstVars[i] && ind_body_elem->right()->arity() == indConstructorArity) || (ind_body_elem->right() == ind_chc.dstVars[i] && ind_body_elem->left()->arity() == indConstructorArity)) { shouldBeChecked = true; - break; } } } @@ -365,7 +373,6 @@ namespace ufo if (std::find(ordered_decls.begin(), ordered_decls.end(), decl) != ordered_decls.end()) return true; cur_decls.insert(decl); -// outs() << decl << "\n ************************ \n"; for (auto & chc : chcs) { if (chc.dstRelation == decl && !chc.isFact) { for (int i = 0; i < chc.srcRelations.size(); i++) { @@ -465,12 +472,7 @@ namespace ufo } // Get the possible version of return variables Expr cur = ordered_decls[idx]; - outs() << "Decls:"; - for (auto decl: ordered_decls){ -// outs() << decl << "\n ************************ \n"; - } for (auto & chc : chcs) { -// outs() << "Comparison: \n" << chc.dstRelation << "\n" << cur << "\n ************************ \n"; if (chc.dstRelation == cur) { @@ -482,10 +484,8 @@ namespace ufo // add functions for filter variables here if (ignoreBaseVar) excludeBaseVar(cur, idxs); if (givePriority) givePriorityNonAdt(cur, idxs); - outs () << *chc.dstRelation->left() << " " << idxs.size() << "\n"; for (int i = idxs.size() - 1; i >= 0; --i) { buf[chc.dstRelation->left()] = idxs[i]; - outs () << *chc.dstRelation->left() << " " << idxs[i] << "\n"; if (findInterpretations(idx + 1, buf)) return true; } @@ -498,7 +498,6 @@ namespace ufo bool solve() { // Order current uninterpreted predicate symbols for (auto & decl: decls) { - outs() << *decl << "\n"; ExprSet cur_decls; if (!orderDecls(decl, cur_decls)) return false; @@ -598,18 +597,21 @@ namespace ufo // ruleManager.print(); ExprVector constructors; + ExprVector accessors; ExprSet& decls = ruleManager.decls; - for(auto decl: decls){ - outs () << decl << "\n"; - } for (auto & a : z3.getAdtConstructors()) { constructors.push_back(regularizeQF(a)); adts.insert(a->last()); } - CHCSolver sol (constructors, adts, efac, decls, ruleManager.extras, ruleManager.chcs, + for (auto & a : z3.getAdtAccessors()) { + accessors.push_back(regularizeQF(a)); + adts.insert(a->last()); + } + + CHCSolver sol (constructors, accessors, adts, efac, decls, ruleManager.extras, ruleManager.chcs, givePriorityNonAdt, ignoreBaseVar); bool res = containsOp(conjoin(decls, efac)) ? sol.solveArr() : sol.solve(); outs () << (res ? "sat\n" : "unknown\n"); diff --git a/include/deep/HornNonlin.hpp b/include/deep/HornNonlin.hpp index 8250bdab7..1d507e9b8 100755 --- a/include/deep/HornNonlin.hpp +++ b/include/deep/HornNonlin.hpp @@ -3,10 +3,6 @@ #include "ae/AeValSolver.hpp" - -// TODO: Dirty hack - - using namespace std; using namespace boost; @@ -112,18 +108,9 @@ namespace ufo for (auto c = lin.begin(); c != lin.end(); ) { Expr cnj = *c; -// outs() << "Cnj: " << cnj << "\n"; if (isOpX(cnj)) { assert(isOpX(cnj->left())); - outs() << "Cnj func: " << cnj << "\n"; - std::string name; - std::stringstream str; - str << cnj; -// if(str.str() == "expr_9_1"){ -// c = lin.erase(c); -// continue; -// } Expr rel = cnj->arg(0); addDecl(rel); srcRelations.push_back(rel); @@ -242,8 +229,6 @@ namespace ufo Expr body = r->arg(0); Expr head = r->arg(1); - outs() << "Head: " << head << "\n"; - outs() << "Body: " << body << "\n"; vector origSrcSymbs; ExprSet lin; splitBody(body, origSrcSymbs, hr.srcRelations, lin); @@ -281,10 +266,8 @@ namespace ufo ExprVector origDstSymbs; if (!hr.isQuery) { - for (auto it = head->args_begin()+1, end = head->args_end(); it != end; ++it){ -// outs() << *it << "\n"; + for (auto it = head->args_begin()+1, end = head->args_end(); it != end; ++it) origDstSymbs.push_back(*it); - } } allOrigSymbs.insert(allOrigSymbs.end(), origDstSymbs.begin(), origDstSymbs.end()); //simplBoolReplCnj(allOrigSymbs, lin); // perhaps, not a very important optimization now; consider removing @@ -317,8 +300,6 @@ namespace ufo hr.assignVarsAndRewrite (origSrcSymbs, tmp, origDstSymbs, invVars[hr.dstRelation]); -// outs() << "Head: " << hr.head << "\n"; - outs() << "Body 1: " << hr.body << "\n"; if ((isOpX(hr.body) && !hr.isQuery) || (hr.srcRelations.size() == 0 && hr.isQuery)) { @@ -334,8 +315,6 @@ namespace ufo if (isOpX(cnj)) { Expr l = bind::fname(cnj->left()); Expr r = bind::fname(cnj->right()); -// outs() << "Left: " << l << "\n"; -// outs() << "Right: " << r << "\n"; if (std::find(constructors.begin(), constructors.end(), l) != constructors.end()) { for (int i = 0; i < cnj->left()->arity(); ++i) { Expr var = cnj->left()->arg(i); diff --git a/include/ufo/Expr.hpp b/include/ufo/Expr.hpp index 2e569860d..b67130833 100644 --- a/include/ufo/Expr.hpp +++ b/include/ufo/Expr.hpp @@ -1163,7 +1163,6 @@ namespace expr else { res = va.isChangeDoKidsRewrite () ? va.getExpr () : expr; -// std::cout << "Res: " << res << "\n"; if (res->arity () > 0) { bool changed = false; @@ -1171,10 +1170,8 @@ namespace expr for (ENode::args_iterator b = res->args_begin (), e = res->args_end (); b != e; ++b) { -// std::cout << "B: " << *b << "\n"; Expr k = visit (v, *b, cache); kids.push_back (k); -// std::cout << "k: " << k << "\n"; changed = (changed || k.get () != *b); } @@ -1186,7 +1183,6 @@ namespace expr kids.end ()); else res->renew_args (kids.begin (), kids.end ()); - std::cout << "New res: " << res << "\n"; } } @@ -3051,16 +3047,7 @@ namespace expr } if (m.empty()) return exp; RAVALLM rav(&m); - int s = exp->arity(); - std::cout << "Exp: " << exp << "\n"; Expr tmp = dagVisit (rav, exp); - // TODO :: really dirty, redo - // TODO: Problem is in the recursive overwrite of the constructor - int s1 = tmp->arity(); - std::cout << "Tmp: " << tmp << "\n"; - if(s == s1){ - std::cout << "Arity hasn't changed\n"; - } if (tmp == exp || !rec) return tmp; else return replaceAll(tmp, m, rec, iter+1); } diff --git a/include/ufo/Smt/Z3n.hpp b/include/ufo/Smt/Z3n.hpp index e42eb29c8..55c8ff4fa 100644 --- a/include/ufo/Smt/Z3n.hpp +++ b/include/ufo/Smt/Z3n.hpp @@ -1,3 +1,4 @@ + /** SeaHorn Verification Framework Copyright (c) 2015 Carnegie Mellon University. @@ -189,15 +190,11 @@ namespace ufo Expr z3_from_smtlib_file (Z &z3, const char *fname) { z3::context &ctx = z3.get_ctx (); - Z3_symbol* names; - Z3_ast_vector b = Z3_parse_smtlib2_file (ctx, fname, 0, names, NULL, 0, NULL, NULL); + Z3_ast_vector b = Z3_parse_smtlib2_file (ctx, fname, 0, NULL, NULL, 0, NULL, NULL); Z3_ast* args = new Z3_ast[Z3_ast_vector_size(ctx, b)]; - printf("Args size: %d \n", Z3_ast_vector_size(ctx, b)); for (unsigned i = 0; i < Z3_ast_vector_size(ctx, b); ++i) { args[i] = Z3_ast_vector_get(ctx, b, i); - Z3_string st = Z3_ast_to_string(ctx, args[i]); - printf("Ast: %d \n", st); } z3::ast ast (ctx, Z3_mk_and(ctx, Z3_ast_vector_size(ctx, b), args)); @@ -289,6 +286,7 @@ namespace ufo protected: z3::context &get_ctx () { return ctx; } std::vector adts; + std::vector accessors; z3::ast toAst (Expr e) { @@ -301,7 +299,7 @@ namespace ufo ast_expr_map seen; std::vector adts_seen; - return U::unmarshal (a, get_efac (), cache.right, seen, adts_seen, adts); + return U::unmarshal (a, get_efac (), cache.right, seen, adts_seen, adts, accessors); } ExprFactory &get_efac () { return efac; } @@ -352,6 +350,7 @@ namespace ufo } ExprVector& getAdtConstructors(){ return adts; } + ExprVector& getAdtAccessors(){ return accessors; } template std::string toSmtLibDecls (const Range &rng) diff --git a/include/ufo/Smt/ZExprConverter.hpp b/include/ufo/Smt/ZExprConverter.hpp index b8b931fad..035bd87ef 100644 --- a/include/ufo/Smt/ZExprConverter.hpp +++ b/include/ufo/Smt/ZExprConverter.hpp @@ -517,7 +517,7 @@ namespace ufo template static Expr unmarshal (const z3::ast &z, ExprFactory &efac, C &cache, ast_expr_map &seen, - std::vector &adts_seen, std::vector &adts) + std::vector &adts_seen, std::vector &adts, std::vector &accessors) { z3::context &ctx = z.ctx (); @@ -566,16 +566,15 @@ namespace ufo unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, Z3_get_array_sort_domain (ctx, sort))), - efac, cache, seen, adts_seen, adts); + efac, cache, seen, adts_seen, adts, accessors); range = unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, Z3_get_array_sort_range (ctx, sort))), - efac, cache, seen, adts_seen, adts); + efac, cache, seen, adts_seen, adts, accessors); return sort::arrayTy (domain, range); case Z3_DATATYPE_SORT: { -// std::cout << "datatype " << Z3_get_symbol_string(ctx, Z3_get_sort_name(ctx, sort)) << "\n"; unsigned num = Z3_get_datatype_sort_num_constructors(ctx, sort); while (num > 0) { num--; @@ -597,45 +596,8 @@ namespace ufo for (int i = 0; i < Z3_get_datatype_sort_num_constructors(ctx, sort); i++) { Z3_func_decl decl = Z3_get_datatype_sort_constructor(ctx, sort, i); -// printf("Datatype decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, decl))); Z3_ast zdecl = Z3_func_decl_to_ast(ctx, decl); - adts.push_back(unmarshal(z3::ast(ctx, zdecl), efac, cache, seen, adts_seen, adts)); -// unsigned num_accessors = Z3_get_domain_size(ctx, decl); -// -//// std::cout << "constructor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,c)) << " " << "\n"; -// while(num_accessors > 0){ -// num_accessors--; -// auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors); -// auto symname = Z3_get_decl_name(ctx,as); -// Expr name; -// std::string st = Z3_get_symbol_string(ctx, symname) ; -// switch (Z3_get_symbol_kind (ctx, symname)) { -// case Z3_STRING_SYMBOL: -// name = mkTerm (Z3_get_symbol_string (ctx, symname), efac); -// break; -// case Z3_INT_SYMBOL: -// name = mkTerm (Z3_get_symbol_int (ctx, symname), efac); -// break; -// } -// assert (name); -// -// ExprVector type; -// for (unsigned p = 0; p < Z3_get_domain_size (ctx, as); ++p) -// { -// Z3_sort sort = Z3_get_domain (ctx, as, p); -// type.push_back -// (unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, sort)), -// efac, cache, seen, adts_seen, adts)); -// } -// -// type.push_back -// (unmarshal (z3::ast (ctx, -// Z3_sort_to_ast (ctx, -// Z3_get_range (ctx, as))), -// efac, cache, seen, adts_seen, adts)); -//// printf("Func dec: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); -// return bind::fdecl (name, type); -// } + adts.push_back(unmarshal(z3::ast(ctx, zdecl), efac, cache, seen, adts_seen, adts, accessors)); } } return sort::adTy (adt_name); @@ -654,7 +616,7 @@ namespace ufo { unsigned idx = Z3_get_index_value (ctx, z); z3::ast zsort (ctx, Z3_sort_to_ast (ctx, Z3_get_sort (ctx, z))); - Expr sort = unmarshal (zsort, efac, cache, seen, adts_seen, adts); + Expr sort = unmarshal (zsort, efac, cache, seen, adts_seen, adts, accessors); return bind::bvar (idx, sort); } @@ -688,15 +650,14 @@ namespace ufo Z3_sort sort = Z3_get_domain (ctx, fdecl, p); type.push_back (unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, sort)), - efac, cache, seen, adts_seen, adts)); + efac, cache, seen, adts_seen, adts, accessors)); } type.push_back (unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, Z3_get_range (ctx, fdecl))), - efac, cache, seen, adts_seen, adts)); -// printf("Func dec: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); + efac, cache, seen, adts_seen, adts, accessors)); return bind::fdecl (name, type); } else if (kind == Z3_QUANTIFIER_AST) @@ -711,13 +672,12 @@ namespace ufo 0, nullptr, Z3_get_quantifier_bound_sort (ctx, z, i)); - printf("Quantifier decl: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, decl))); z3::ast zdecl (ctx, Z3_func_decl_to_ast (ctx, decl)); - args.push_back (unmarshal (zdecl, efac, cache, seen, adts_seen, adts)); + args.push_back (unmarshal (zdecl, efac, cache, seen, adts_seen, adts, accessors)); assert (args.back ().get ()); } args.push_back (unmarshal (z3::ast (ctx, Z3_get_quantifier_body (ctx, z)), - efac, cache, seen, adts_seen, adts)); + efac, cache, seen, adts_seen, adts, accessors)); return Z3_is_quantifier_forall (ctx, z) ? mknary (args) : mknary (args); } @@ -736,36 +696,36 @@ namespace ufo assert (Z3_get_app_num_args (ctx, app) == 1); return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts)); + efac, cache, seen, adts_seen, adts, accessors)); } if (dkind == Z3_OP_UMINUS) return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts)); + efac, cache, seen, adts_seen, adts, accessors)); // XXX ignore to_real and to_int operators if (dkind == Z3_OP_TO_REAL || dkind == Z3_OP_TO_INT) return unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts); + efac, cache, seen, adts_seen, adts, accessors); if (dkind == Z3_OP_BNOT) return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts)); + efac, cache, seen, adts_seen, adts, accessors)); if (dkind == Z3_OP_BNEG) return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts)); + efac, cache, seen, adts_seen, adts, accessors)); if (dkind == Z3_OP_BREDAND) return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts)); + efac, cache, seen, adts_seen, adts, accessors)); if (dkind == Z3_OP_BREDOR) return mk (unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts)); + efac, cache, seen, adts_seen, adts, accessors)); if (dkind == Z3_OP_SIGN_EXT || dkind == Z3_OP_ZERO_EXT) { Expr sort = bv::bvsort (Z3_get_bv_sort_size (ctx, Z3_get_sort (ctx, z)), efac); Expr arg = unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts); + efac, cache, seen, adts_seen, adts, accessors); switch (dkind) { case Z3_OP_SIGN_EXT: @@ -779,7 +739,7 @@ namespace ufo if (dkind == Z3_OP_EXTRACT) { Expr arg = unmarshal (z3::ast (ctx, Z3_get_app_arg (ctx, app, 0)), - efac, cache, seen, adts_seen, adts); + efac, cache, seen, adts_seen, adts, accessors); Z3_func_decl d = Z3_get_app_decl (ctx, app); unsigned high = Z3_get_decl_int_parameter (ctx, d, 0); @@ -793,7 +753,7 @@ namespace ufo z3::ast zdecl (ctx, Z3_func_decl_to_ast (ctx, Z3_get_as_array_func_decl (ctx, z))); - return mk (unmarshal (zdecl, efac, cache, seen, adts_seen, adts)); + return mk (unmarshal (zdecl, efac, cache, seen, adts_seen, adts, accessors)); } { typename C::const_iterator it = cache.find (z); @@ -811,10 +771,9 @@ namespace ufo // TODO: Disequality, constructor inside constructor(maybe), IF then else if(dkind == Z3_OP_EQ && i == 1 && Z3_get_decl_kind (ctx, Z3_get_app_decl (ctx, Z3_to_app(ctx, z3::ast(ctx, Z3_get_app_arg(ctx, app, i))))) == Z3_OP_DT_CONSTRUCTOR){ left = args[0]; - printf("We are in the state of eq with constructor\n"); } args.push_back (unmarshal - (z3::ast(ctx, Z3_get_app_arg(ctx, app, i)), efac, cache, seen, adts_seen, adts)); + (z3::ast(ctx, Z3_get_app_arg(ctx, app, i)), efac, cache, seen, adts_seen, adts, accessors)); } @@ -833,17 +792,17 @@ namespace ufo continue; } - outs() << "Datatype constructor constructor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,c)) << " " << "\n"; while(num_accessors > 0){ num_accessors--; auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors); ExprVector eq; - outs() << "Datatype constructor accessor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,as)) << "\n"; - outs() << "Accessor parameter: " << left << "\n"; - // Put value from the constructor into equality - eq.push_back (bind::fapp (unmarshal (z3::func_decl (ctx, as), - efac, cache, seen, adts_seen, adts), { left })); + // Put value from the constructor into equality + eq.push_back (bind::fapp (unmarshal (z3::func_decl (ctx, as), + efac, cache, seen, adts_seen, adts, accessors), { left })); eq.push_back (args[num_accessors]); + + accessors.push_back(bind::fname((unmarshal (z3::func_decl (ctx, as), + efac, cache, seen, adts_seen, adts, accessors)))); // accessor(data) = value subexpr.push_back(mknary (eq.begin(), eq.end())); } @@ -851,14 +810,7 @@ namespace ufo } Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), - efac, cache, seen, adts_seen, adts), args); -// subexpr.push_back(res); -// Expr final; -// if(subexpr.size() > 0) final = mknary (subexpr.begin(), subexpr.end()); -// outs()<<"Resulting expression: " << final << "\n"; -// for(auto expr: subexpr){ -// outs()<<"Subexpression: " << expr << "\n"; -// } + efac, cache, seen, adts_seen, adts, accessors), args); outs() << "Datatype constructor decl: " << res << "\n"; cache.insert (typename C::value_type (z, res)); left = NULL; @@ -868,7 +820,7 @@ namespace ufo if (dkind == Z3_OP_UNINTERPRETED) { printf("Func app: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), - efac, cache, seen, adts_seen, adts), args); + efac, cache, seen, adts_seen, adts, accessors), args); // -- XXX maybe use seen instead. not sure what is best. cache.insert (typename C::value_type (z, res)); return res; @@ -878,35 +830,12 @@ namespace ufo Z3_sort srt = Z3_get_sort(ctx, z); Z3_func_decl acc = Z3_get_datatype_sort_constructor_accessor(ctx, srt,1,1); Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), - efac, cache, seen, adts_seen, adts), args); + efac, cache, seen, adts_seen, adts, accessors), args); + accessors.push_back(bind::fname(res)); // -- XXX maybe use seen instead. not sure what is best. cache.insert (typename C::value_type (z, res)); return res; } -// auto accessor = Z3_to_app(ctx, z); -// auto parameter = Z3_get_app_arg(ctx, accessor, 0); -// auto fdecl1 = Z3_get_app_decl (ctx, accessor); -// auto dkind1 = Z3_get_decl_kind (ctx, fdecl); -// while(Z3_is_app(ctx, parameter)){ -// accessor = Z3_to_app(ctx, parameter); -// parameter = Z3_get_app_arg(ctx, accessor, 0); -// fdecl1 = Z3_get_app_decl (ctx, accessor); -// dkind1 = Z3_get_decl_kind (ctx, fdecl); -// } -// Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), -// efac, cache, seen, adts_seen, adts), args); -// for (size_t i = 0; i < (size_t)Z3_get_app_num_args (ctx, app); i++) -// args.push_back (unmarshal -// (z3::ast(ctx, Z3_get_app_arg(ctx, app, i)), efac, cache, seen, adts_seen, adts)); -// -// unsigned idx = Z3_get_index_value(ctx, parameter); -// assert(idx != 0 && Z3_get_app_num_args(ctx, accessor) == 1); -// z3::ast zsort(ctx, Z3_sort_to_ast(ctx, Z3_get_sort(ctx, z))); -// Expr sort = unmarshal(zsort, efac, cache, seen, adts_seen, adts); -//// Expr res = bind::fapp ( unmarshal (z3::func_decl (ctx, fdecl), -//// efac, cache, seen, adts_seen, adts), bind::bvar(idx, sort)); -// return bind::bvar(idx, sort); -// } switch (dkind) { case Z3_OP_ITE: @@ -932,13 +861,8 @@ namespace ufo if(subexpr.size() > 0){ subexpr.push_back(e); -// std::reverse(subexpr.begin(), subexpr.end()); e = mknary(subexpr.begin(), subexpr.end()); - for(int i = subexpr.size(); i>0 ; i--){ - outs()<<"Subexpression: " << subexpr[i - 1] << "\n"; - } subexpr.clear(); - outs()<<"Resulting expression: " << e << "\n"; } break; case Z3_OP_LT: @@ -984,7 +908,7 @@ namespace ufo Expr domain = unmarshal (z3::ast (ctx, Z3_sort_to_ast (ctx, Z3_get_array_sort_domain (ctx, sort))), - efac, cache, seen, adts_seen, adts); + efac, cache, seen, adts_seen, adts, accessors); e = op::array::constArray (domain, args[0]); } @@ -1070,16 +994,6 @@ namespace ufo case Z3_OP_BASHR: e = mknary (args.begin (), args.end ()); break; -// case Z3_OP_DT_ACCESSOR: -// assert (args.size () == 1); -// Z3_sort sort = Z3_get_sort (ctx, z); -// Expr domain = unmarshal -// (z3::ast (ctx, Z3_sort_to_ast (ctx, -// Z3_get_array_sort_domain (ctx, sort))), -// efac, cache, seen, adts_seen, adts); -// -// e = op::Accessor::instantiate (domain, args[0]); -// break; default: return U::unmarshal (z, efac, cache, seen); } From 8c4e59cbd209fe480968e7a1411b863fa923a02b Mon Sep 17 00:00:00 2001 From: Konstantin Date: Wed, 16 Aug 2023 12:03:35 +0300 Subject: [PATCH 05/12] Accessors: quick PR fixes --- bench_adt/list_constructor_check.smt2 | 0 include/adt/CHCSolver.hpp | 2 -- include/ufo/Smt/Z3n.hpp | 1 - 3 files changed, 3 deletions(-) delete mode 100644 bench_adt/list_constructor_check.smt2 diff --git a/bench_adt/list_constructor_check.smt2 b/bench_adt/list_constructor_check.smt2 deleted file mode 100644 index e69de29bb..000000000 diff --git a/include/adt/CHCSolver.hpp b/include/adt/CHCSolver.hpp index d86fdf398..649cb65d7 100644 --- a/include/adt/CHCSolver.hpp +++ b/include/adt/CHCSolver.hpp @@ -473,8 +473,6 @@ namespace ufo // Get the possible version of return variables Expr cur = ordered_decls[idx]; for (auto & chc : chcs) { - - if (chc.dstRelation == cur) { size_t vars_size = chc.dstRelation->arity(); std::vector idxs; diff --git a/include/ufo/Smt/Z3n.hpp b/include/ufo/Smt/Z3n.hpp index 55c8ff4fa..6fe0f3d0a 100644 --- a/include/ufo/Smt/Z3n.hpp +++ b/include/ufo/Smt/Z3n.hpp @@ -1,4 +1,3 @@ - /** SeaHorn Verification Framework Copyright (c) 2015 Carnegie Mellon University. From 6c4a750aa9d95e05821ebe99e76ff5ae09dad4f0 Mon Sep 17 00:00:00 2001 From: Konstantin Date: Wed, 16 Aug 2023 12:06:56 +0300 Subject: [PATCH 06/12] Accessors: quick PR fixes --- include/ufo/Smt/ZExprConverter.hpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/include/ufo/Smt/ZExprConverter.hpp b/include/ufo/Smt/ZExprConverter.hpp index 035bd87ef..8bd24b8dc 100644 --- a/include/ufo/Smt/ZExprConverter.hpp +++ b/include/ufo/Smt/ZExprConverter.hpp @@ -581,11 +581,9 @@ namespace ufo auto c = Z3_get_datatype_sort_constructor(ctx, sort, num); unsigned num_accessors = Z3_get_domain_size(ctx, c); - std::cout << "constructor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,c)) << " " << "\n"; while(num_accessors > 0){ num_accessors--; auto as = Z3_get_datatype_sort_constructor_accessor(ctx, sort, num, num_accessors); - std::cout << "accessor: " << Z3_get_symbol_string(ctx, Z3_get_decl_name(ctx,as)) << "\n"; } } std::string name = Z3_get_symbol_string(ctx, Z3_get_sort_name(ctx, sort)); @@ -811,14 +809,12 @@ namespace ufo Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), efac, cache, seen, adts_seen, adts, accessors), args); - outs() << "Datatype constructor decl: " << res << "\n"; cache.insert (typename C::value_type (z, res)); left = NULL; return res; } if (dkind == Z3_OP_UNINTERPRETED) { - printf("Func app: %s \n", Z3_get_symbol_string(ctx, Z3_get_decl_name (ctx, fdecl))); Expr res = bind::fapp (unmarshal (z3::func_decl (ctx, fdecl), efac, cache, seen, adts_seen, adts, accessors), args); // -- XXX maybe use seen instead. not sure what is best. From 225a2bec36c55d9a21fb2ce0fba3f22518bdaf2e Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Thu, 31 Aug 2023 17:50:47 +0200 Subject: [PATCH 07/12] Adt-CHC: tests removal(tgnonlin) --- bench_adt/simple_if.smt2 | 163 ----------------------------------- bench_adt/simple_if_min.smt2 | 163 ----------------------------------- 2 files changed, 326 deletions(-) delete mode 100644 bench_adt/simple_if.smt2 delete mode 100644 bench_adt/simple_if_min.smt2 diff --git a/bench_adt/simple_if.smt2 b/bench_adt/simple_if.smt2 deleted file mode 100644 index 4d304883e..000000000 --- a/bench_adt/simple_if.smt2 +++ /dev/null @@ -1,163 +0,0 @@ -(set-logic HORN) - -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-fun |interface_0_C_31_0| (Int |abi_type| |crypto_type| |state_type| ) Bool) -(declare-fun |nondet_interface_1_C_31_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool) -(declare-fun |summary_constructor_2_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (state_0 |state_type|) (this_0 Int) (tx_0 |tx_type|)) -(=> (= error_0 0) (nondet_interface_1_C_31_0 error_0 this_0 abi_0 crypto_0 state_0 state_0)))) - - -(declare-fun |summary_3_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |summary_4_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_1 Int)) -(=> (and (and (nondet_interface_1_C_31_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_4_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 a_2_0 state_2 a_2_1 z_5_1))) (nondet_interface_1_C_31_0 error_1 this_0 abi_0 crypto_0 state_0 state_2)))) - - -(declare-fun |block_5_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |block_6_simple_if_29_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) -(block_5_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) -(=> (and (and (block_5_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= a_2_1 a_2_0))) true)) true) (block_6_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(declare-fun |block_7_return_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |block_8_if_header_simple_if_28_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |block_9_if_true_simple_if_18_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |block_10_if_false_simple_if_27_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |block_11_simple_if_29_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) -(=> (and (and (block_6_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_1 0) (and (and (>= a_2_1 0) (<= a_2_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))) true) (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) -(=> (and (and (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_9_1 (< expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 5) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 a_2_1) true)))))) expr_9_1) (block_9_if_true_simple_if_18_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) -(=> (and (and (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_9_1 (< expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 5) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 a_2_1) true)))))) (not expr_9_1)) (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_9_if_true_simple_if_18_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_2 expr_16_0) (and (=> true true) (and (= expr_16_0 0) (and (= a_2_2 expr_14_1) (and (=> true (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 expr_13_1) (and (=> true (and (>= expr_10_0 0) (<= expr_10_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_10_0 a_2_1) (and (=> true (and (>= expr_13_1 0) (<= expr_13_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_1 (+ expr_11_0 expr_12_0)) (and (=> true true) (and (= expr_12_0 1) (and (=> true (and (>= expr_11_0 0) (<= expr_11_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_11_0 a_2_1) true))))))))))))))) true) (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2)))) - - -(declare-fun |block_12_return_ghost_simple_if_17_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_12_return_ghost_simple_if_17_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2) (and (= z_5_2 expr_16_0) (and (=> true true) (and (= expr_16_0 0) (and (= a_2_2 expr_14_1) (and (=> true (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 expr_13_1) (and (=> true (and (>= expr_10_0 0) (<= expr_10_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_10_0 a_2_1) (and (=> true (and (>= expr_13_1 0) (<= expr_13_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_1 (+ expr_11_0 expr_12_0)) (and (=> true true) (and (= expr_12_0 1) (and (=> true (and (>= expr_11_0 0) (<= expr_11_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_11_0 a_2_1) true))))))))))))))) true) (block_11_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2)))) - - -(declare-fun |block_13_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))) (and (not expr_22_1) (= error_1 1))) (block_13_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (block_13_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (summary_3_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_2 expr_25_0) (and (=> true true) (and (= expr_25_0 1) (and (= error_1 error_0) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))))))) true) (block_7_return_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2)))) - - -(declare-fun |block_14_return_ghost_simple_if_26_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_14_return_ghost_simple_if_26_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2) (and (= z_5_2 expr_25_0) (and (=> true true) (and (= expr_25_0 1) (and (= error_1 error_0) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))))))) true) (block_11_simple_if_29_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_11_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) true) true) (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) true) true) (summary_3_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(declare-fun |block_15_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(block_15_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_15_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (summary_3_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 a_2_1 state_3 a_2_2 z_5_1) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3745062286)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 223)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 57)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 29)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 142)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= a_2_1 a_2_0))) true))))))) true) (summary_4_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_3 a_2_2 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (interface_0_C_31_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (= error_0 0))) (interface_0_C_31_0 this_0 abi_0 crypto_0 state_1)))) - - -(declare-fun |contract_initializer_16_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(declare-fun |contract_initializer_entry_17_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_17_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |contract_initializer_after_init_18_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (contract_initializer_entry_17_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_18_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (contract_initializer_after_init_18_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_16_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |implicit_constructor_entry_19_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_16_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_16_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (summary_constructor_2_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_31_0 this_0 abi_0 crypto_0 state_1)))) - - -(declare-fun |error_target_3_0| () Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (interface_0_C_31_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (= error_0 1))) error_target_3_0))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> error_target_3_0 false))) -(check-sat) diff --git a/bench_adt/simple_if_min.smt2 b/bench_adt/simple_if_min.smt2 deleted file mode 100644 index 4d304883e..000000000 --- a/bench_adt/simple_if_min.smt2 +++ /dev/null @@ -1,163 +0,0 @@ -(set-logic HORN) - -(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int)))))) -(declare-datatypes ((|bytes_tuple| 0)) (((|bytes_tuple| (|bytes_tuple_accessor_array| (Array Int Int)) (|bytes_tuple_accessor_length| Int))))) -(declare-datatypes ((|tx_type| 0)) (((|tx_type| (|block.basefee| Int) (|block.chainid| Int) (|block.coinbase| Int) (|block.difficulty| Int) (|block.gaslimit| Int) (|block.number| Int) (|block.timestamp| Int) (|blockhash| (Array Int Int)) (|msg.data| |bytes_tuple|) (|msg.sender| Int) (|msg.sig| Int) (|msg.value| Int) (|tx.gasprice| Int) (|tx.origin| Int))))) -(declare-datatypes ((|ecrecover_input_type| 0)) (((|ecrecover_input_type| (|hash| Int) (|v| Int) (|r| Int) (|s| Int))))) -(declare-datatypes ((|crypto_type| 0)) (((|crypto_type| (|ecrecover| (Array |ecrecover_input_type| Int)) (|keccak256| (Array |bytes_tuple| Int)) (|ripemd160| (Array |bytes_tuple| Int)) (|sha256| (Array |bytes_tuple| Int)))))) -(declare-datatypes ((|abi_type| 0)) (((|abi_type|)))) -(declare-fun |interface_0_C_31_0| (Int |abi_type| |crypto_type| |state_type| ) Bool) -(declare-fun |nondet_interface_1_C_31_0| (Int Int |abi_type| |crypto_type| |state_type| |state_type| ) Bool) -(declare-fun |summary_constructor_2_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (state_0 |state_type|) (this_0 Int) (tx_0 |tx_type|)) -(=> (= error_0 0) (nondet_interface_1_C_31_0 error_0 this_0 abi_0 crypto_0 state_0 state_0)))) - - -(declare-fun |summary_3_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |summary_4_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_1 Int)) -(=> (and (and (nondet_interface_1_C_31_0 error_0 this_0 abi_0 crypto_0 state_0 state_1) true) (and (= error_0 0) (summary_4_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 a_2_0 state_2 a_2_1 z_5_1))) (nondet_interface_1_C_31_0 error_1 this_0 abi_0 crypto_0 state_0 state_2)))) - - -(declare-fun |block_5_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |block_6_simple_if_29_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) -(block_5_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) -(=> (and (and (block_5_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= a_2_1 a_2_0))) true)) true) (block_6_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(declare-fun |block_7_return_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |block_8_if_header_simple_if_28_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |block_9_if_true_simple_if_18_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |block_10_if_false_simple_if_27_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(declare-fun |block_11_simple_if_29_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) -(=> (and (and (block_6_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_1 0) (and (and (>= a_2_1 0) (<= a_2_1 115792089237316195423570985008687907853269984665640564039457584007913129639935)) true))) true) (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) -(=> (and (and (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_9_1 (< expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 5) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 a_2_1) true)))))) expr_9_1) (block_9_if_true_simple_if_18_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int)) -(=> (and (and (block_8_if_header_simple_if_28_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_9_1 (< expr_7_0 expr_8_0)) (and (=> true true) (and (= expr_8_0 5) (and (=> true (and (>= expr_7_0 0) (<= expr_7_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_7_0 a_2_1) true)))))) (not expr_9_1)) (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_9_if_true_simple_if_18_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_2 expr_16_0) (and (=> true true) (and (= expr_16_0 0) (and (= a_2_2 expr_14_1) (and (=> true (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 expr_13_1) (and (=> true (and (>= expr_10_0 0) (<= expr_10_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_10_0 a_2_1) (and (=> true (and (>= expr_13_1 0) (<= expr_13_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_1 (+ expr_11_0 expr_12_0)) (and (=> true true) (and (= expr_12_0 1) (and (=> true (and (>= expr_11_0 0) (<= expr_11_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_11_0 a_2_1) true))))))))))))))) true) (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2)))) - - -(declare-fun |block_12_return_ghost_simple_if_17_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_12_return_ghost_simple_if_17_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2) (and (= z_5_2 expr_16_0) (and (=> true true) (and (= expr_16_0 0) (and (= a_2_2 expr_14_1) (and (=> true (and (>= expr_14_1 0) (<= expr_14_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_14_1 expr_13_1) (and (=> true (and (>= expr_10_0 0) (<= expr_10_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_10_0 a_2_1) (and (=> true (and (>= expr_13_1 0) (<= expr_13_1 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_13_1 (+ expr_11_0 expr_12_0)) (and (=> true true) (and (= expr_12_0 1) (and (=> true (and (>= expr_11_0 0) (<= expr_11_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_11_0 a_2_1) true))))))))))))))) true) (block_11_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_2 z_5_2)))) - - -(declare-fun |block_13_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))) (and (not expr_22_1) (= error_1 1))) (block_13_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (block_13_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (summary_3_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_10_if_false_simple_if_27_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (= z_5_2 expr_25_0) (and (=> true true) (and (= expr_25_0 1) (and (= error_1 error_0) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))))))) true) (block_7_return_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2)))) - - -(declare-fun |block_14_return_ghost_simple_if_26_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_14_return_ghost_simple_if_26_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2) (and (= z_5_2 expr_25_0) (and (=> true true) (and (= expr_25_0 1) (and (= error_1 error_0) (and (= expr_22_1 (>= expr_20_0 expr_21_0)) (and (=> true true) (and (= expr_21_0 5) (and (=> true (and (>= expr_20_0 0) (<= expr_20_0 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (= expr_20_0 a_2_1) true)))))))))) true) (block_11_simple_if_29_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_2)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_11_simple_if_29_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) true) true) (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_7_return_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) true) true) (summary_3_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1)))) - - -(declare-fun |block_15_function_simple_if__30_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| Int |state_type| Int Int ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(block_15_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (block_15_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (and (summary_3_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_2 a_2_1 state_3 a_2_2 z_5_1) (and (= state_2 (|state_type| (store (|balances| state_1) this_0 (+ (select (|balances| state_1) this_0) funds_2_0)))) (and (and (>= (+ (select (|balances| state_1) this_0) funds_2_0) 0) (<= (+ (select (|balances| state_1) this_0) funds_2_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= funds_2_0 (|msg.value| tx_0)) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (and (and (and (and (and (= (|msg.value| tx_0) 0) (= (|msg.sig| tx_0) 3745062286)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 0) 223)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 1) 57)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 2) 29)) (= (select (|bytes_tuple_accessor_array| (|msg.data| tx_0)) 3) 142)) (>= (|bytes_tuple_accessor_length| (|msg.data| tx_0)) 4))) (and (and (and (and (= state_1 state_0) (= error_0 0)) true) (and true (= a_2_1 a_2_0))) true))))))) true) (summary_4_function_simple_if__30_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_3 a_2_2 z_5_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (interface_0_C_31_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (= error_0 0))) (interface_0_C_31_0 this_0 abi_0 crypto_0 state_1)))) - - -(declare-fun |contract_initializer_16_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(declare-fun |contract_initializer_entry_17_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (= state_1 state_0) (= error_0 0)) true) (contract_initializer_entry_17_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |contract_initializer_after_init_18_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (contract_initializer_entry_17_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_after_init_18_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (contract_initializer_after_init_18_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) true) (contract_initializer_16_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(declare-fun |implicit_constructor_entry_19_C_31_0| (Int Int |abi_type| |crypto_type| |tx_type| |state_type| |state_type| ) Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (and (and (= state_1 state_0) (= error_0 0)) true) true) (>= (select (|balances| state_1) this_0) (|msg.value| tx_0))) (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (contract_initializer_16_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true)) (> error_1 0)) (summary_constructor_2_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (implicit_constructor_entry_19_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) (and (= error_1 0) (and (contract_initializer_16_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_1 state_2) true))) true) (summary_constructor_2_C_31_0 error_1 this_0 abi_0 crypto_0 tx_0 state_0 state_2)))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (summary_constructor_2_C_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 state_1) true) (and (and (and (and (and (and (and (and (and (and (and (and (and (>= (|block.basefee| tx_0) 0) (<= (|block.basefee| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935)) (and (>= (|block.chainid| tx_0) 0) (<= (|block.chainid| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.coinbase| tx_0) 0) (<= (|block.coinbase| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|block.difficulty| tx_0) 0) (<= (|block.difficulty| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.gaslimit| tx_0) 0) (<= (|block.gaslimit| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.number| tx_0) 0) (<= (|block.number| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|block.timestamp| tx_0) 0) (<= (|block.timestamp| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|msg.sender| tx_0) 0) (<= (|msg.sender| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|msg.value| tx_0) 0) (<= (|msg.value| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (and (>= (|tx.origin| tx_0) 0) (<= (|tx.origin| tx_0) 1461501637330902918203684832716283019655932542975))) (and (>= (|tx.gasprice| tx_0) 0) (<= (|tx.gasprice| tx_0) 115792089237316195423570985008687907853269984665640564039457584007913129639935))) (= (|msg.value| tx_0) 0)) (= error_0 0))) (interface_0_C_31_0 this_0 abi_0 crypto_0 state_1)))) - - -(declare-fun |error_target_3_0| () Bool) -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> (and (and (interface_0_C_31_0 this_0 abi_0 crypto_0 state_0) true) (and (summary_4_function_simple_if__30_31_0 error_0 this_0 abi_0 crypto_0 tx_0 state_0 a_2_0 state_1 a_2_1 z_5_1) (= error_0 1))) error_target_3_0))) - - -(assert -(forall ( (a_2_0 Int) (a_2_1 Int) (a_2_2 Int) (abi_0 |abi_type|) (crypto_0 |crypto_type|) (error_0 Int) (error_1 Int) (expr_10_0 Int) (expr_11_0 Int) (expr_12_0 Int) (expr_13_1 Int) (expr_14_1 Int) (expr_16_0 Int) (expr_20_0 Int) (expr_21_0 Int) (expr_22_1 Bool) (expr_25_0 Int) (expr_7_0 Int) (expr_8_0 Int) (expr_9_1 Bool) (funds_2_0 Int) (state_0 |state_type|) (state_1 |state_type|) (state_2 |state_type|) (state_3 |state_type|) (this_0 Int) (tx_0 |tx_type|) (z_5_0 Int) (z_5_1 Int) (z_5_2 Int)) -(=> error_target_3_0 false))) -(check-sat) From a0741f606a8679dc923faefe51e5c8cb370d8457 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Thu, 31 Aug 2023 17:51:29 +0200 Subject: [PATCH 08/12] Adt-CHC: tests removal(tgnonlin) --- bench_adt/heap_insert.smt2 | 43 -------------------------------------- 1 file changed, 43 deletions(-) delete mode 100644 bench_adt/heap_insert.smt2 diff --git a/bench_adt/heap_insert.smt2 b/bench_adt/heap_insert.smt2 deleted file mode 100644 index aca7e872f..000000000 --- a/bench_adt/heap_insert.smt2 +++ /dev/null @@ -1,43 +0,0 @@ -(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) - -(declare-datatypes () ((Heap (hleaf) (heap (rk Int) (value Int) (hleft Heap) (hright Heap))))) -(declare-fun rightHeight (Heap) Int) -(assert (= (rightHeight hleaf) 0)) -(assert (forall ((k Int) (v Int) (l Heap) (r Heap)) (= (rightHeight (heap k v l r)) (+ 1 (rightHeight r))))) - -(declare-fun rank (Heap) Int) -(assert (= (rank hleaf) 0)) -(assert (forall ((k Int) (v Int) (l Heap) (r Heap)) (= (rank (heap k v l r)) k))) - -(declare-fun hasLeftistProperty (Heap) Bool) -(assert (hasLeftistProperty hleaf)) -(assert (forall ((k Int) (v Int) (l Heap) (r Heap)) - (= (hasLeftistProperty (heap k v l r)) - (and (hasLeftistProperty l) (hasLeftistProperty r) - (<= (rightHeight r) (rightHeight l)) - (= k (+ 1 (rightHeight r))))))) - -(declare-fun hsize (Heap) Int) -(assert (= (hsize hleaf) 0)) -(assert (forall ((k Int) (v Int) (l Heap) (r Heap)) (= (hsize (heap k v l r)) (+ 1 (+ (hsize l) (hsize r)))))) - -(declare-fun mergea (Int Heap Heap) Heap) -(assert (forall ((v Int) (l Heap) (r Heap)) - (= (mergea v l r) (ite (<= (rank r) (rank l)) (heap (+ 1 (rank r)) v l r) (heap (+ 1 (rank l)) v r l))))) - -(declare-fun merge (Heap Heap) Heap) -(assert (forall ((h Heap)) (= (merge h hleaf) h))) -(assert (forall ((h Heap)) (= (merge hleaf h) h))) -(assert (forall ((k1 Int) (v1 Int) (l1 Heap) (r1 Heap) (k2 Int) (v2 Int) (l2 Heap) (r2 Heap)) - (= (merge (heap k1 v1 l1 r1) (heap k2 v2 l2 r2)) - (ite (< v2 v1) (mergea v1 l1 (merge r1 (heap k2 v2 l2 r2))) - (mergea v2 l2 (merge (heap k1 v1 l1 r1) r2)))))) - -(declare-fun hinsert (Heap Int) Heap) -(assert (forall ((h Heap) (n Int)) (= (hinsert h n) (merge (heap 1 n hleaf hleaf) h)))) - -; extra lemmas -(assert (forall ((x Heap)) (>= (hsize x) 0))) - -(assert (not (forall ((x Heap) (n Int)) (=> (hasLeftistProperty x) (hasLeftistProperty (hinsert x n)))))) -(check-sat) From 32b25b88c65b31bffb605dbd8fc0d37be6a7f060 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Thu, 31 Aug 2023 18:08:43 +0200 Subject: [PATCH 09/12] ADT-CHC: check of the accessors renaming --- bench_horn_adt/ADTIND/list_len_acc.smt2 | 0 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 bench_horn_adt/ADTIND/list_len_acc.smt2 diff --git a/bench_horn_adt/ADTIND/list_len_acc.smt2 b/bench_horn_adt/ADTIND/list_len_acc.smt2 new file mode 100644 index 000000000..e69de29bb From 23dec749125adb5794cac7a4f54759ca95caa5ba Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Thu, 31 Aug 2023 18:09:13 +0200 Subject: [PATCH 10/12] ADT-CHC: check of the accessors renaming --- bench_horn_adt/ADTIND/list_len_acc.smt2 | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/bench_horn_adt/ADTIND/list_len_acc.smt2 b/bench_horn_adt/ADTIND/list_len_acc.smt2 index e69de29bb..c725a6a1e 100644 --- a/bench_horn_adt/ADTIND/list_len_acc.smt2 +++ b/bench_horn_adt/ADTIND/list_len_acc.smt2 @@ -0,0 +1,10 @@ +(set-logic HORN) +(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) +(declare-fun length (Lst Int) Bool) +(declare-fun ff () Bool) +(assert (length nil 0)) + +(assert (forall ((x Int) (xs Lst) (ys Lst) (l Int)) + (=> (and (= xs (cons x ys)) (length ys l) (not (length (tail xs) l))) ff))) +(assert (not ff)) +(check-sat) \ No newline at end of file From c3ca4cc71690d240702e7d9043f19cc3c8821fe7 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Thu, 31 Aug 2023 18:18:56 +0200 Subject: [PATCH 11/12] ADT-CHC: check of the accessors renaming --- bench_horn_adt/ADTIND/list_value_check_acc.smt2 | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 bench_horn_adt/ADTIND/list_value_check_acc.smt2 diff --git a/bench_horn_adt/ADTIND/list_value_check_acc.smt2 b/bench_horn_adt/ADTIND/list_value_check_acc.smt2 new file mode 100644 index 000000000..1fcf3a901 --- /dev/null +++ b/bench_horn_adt/ADTIND/list_value_check_acc.smt2 @@ -0,0 +1,11 @@ +;There is some weird error rn +(set-logic HORN) +(declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) +(declare-fun length (Lst Int) Bool) +(declare-fun ff () Bool) +(assert (length nil 0)) + +(assert (forall ((x1 Int) (x2 Int) (xs Lst) (ys Lst) (zs Lst) (l Int)) + (=> (and (= xs (cons x1 ys)) (= ys (cons x2 zs)) (= (head (tail xs)) x2)) ff))) +(assert (not ff)) +(check-sat) \ No newline at end of file From 0fe90dfb67a4e03183826fc9cfe89d8806bfb215 Mon Sep 17 00:00:00 2001 From: BritikovKI Date: Wed, 6 Sep 2023 16:33:57 +0200 Subject: [PATCH 12/12] ADT-CHC: check of the accessors renaming --- bench_horn_adt/ADTIND/list_value_check_acc.smt2 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/bench_horn_adt/ADTIND/list_value_check_acc.smt2 b/bench_horn_adt/ADTIND/list_value_check_acc.smt2 index 1fcf3a901..0cd73991e 100644 --- a/bench_horn_adt/ADTIND/list_value_check_acc.smt2 +++ b/bench_horn_adt/ADTIND/list_value_check_acc.smt2 @@ -3,9 +3,9 @@ (declare-datatypes () ((Lst (cons (head Int) (tail Lst)) (nil)))) (declare-fun length (Lst Int) Bool) (declare-fun ff () Bool) -(assert (length nil 0)) +;(assert (length nil 0)) (assert (forall ((x1 Int) (x2 Int) (xs Lst) (ys Lst) (zs Lst) (l Int)) - (=> (and (= xs (cons x1 ys)) (= ys (cons x2 zs)) (= (head (tail xs)) x2)) ff))) + (=> (and (= xs (cons x1 ys)) (= ys (cons x2 zs)) (not (= (head (tail xs)) x2))) ff))) (assert (not ff)) (check-sat) \ No newline at end of file