diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2019-03-15 18:35:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-15 18:35:43 -0500 |
| commit | 2989780f0242d14712927bd4c01c4a521a8fe399 (patch) | |
| tree | 3de200dd87eedd3705ef7509db955a8ca17b3725 /test | |
| parent | e8f23236b7f797fd3cd8900df0422d44f1a6a7e0 (diff) | |
New beta-reduction for HOL solving (#2869)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/ho/shadowing-defs.smt2 | 41 |
2 files changed, 42 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 9b1ce17e4..fb0e358e2 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -476,6 +476,7 @@ set(regress_0_tests regress0/ho/ite-apply-eq.smt2 regress0/ho/lambda-equality-non-canon.smt2 regress0/ho/modulo-func-equality.smt2 + regress0/ho/shadowing-defs.smt2 regress0/ho/simple-matching-partial.smt2 regress0/ho/simple-matching.smt2 regress0/ho/trans.smt2 diff --git a/test/regress/regress0/ho/shadowing-defs.smt2 b/test/regress/regress0/ho/shadowing-defs.smt2 new file mode 100644 index 000000000..722e970b6 --- /dev/null +++ b/test/regress/regress0/ho/shadowing-defs.smt2 @@ -0,0 +1,41 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unknown +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-sort mu 0) + +(declare-fun mnot ((-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mnot (lambda ((Phi (-> $$unsorted Bool)) (W $$unsorted)) (not (Phi W))))) + +(declare-fun mor ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mor (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (W $$unsorted)) (or (Phi W) (Psi W))))) + +(declare-fun mand ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mand (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mor (mnot Phi) (mnot Psi)) __flatten_var_0)))) + +(declare-fun mimplies ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mimplies (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mor (mnot Phi) Psi __flatten_var_0)))) + +(declare-fun mforall_ind ((-> mu $$unsorted Bool) $$unsorted) Bool) +(assert (= mforall_ind (lambda ((Phi (-> mu $$unsorted Bool)) (W $$unsorted)) (forall ((X mu)) (Phi X W) )))) + +(declare-fun mbox ((-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mbox (lambda ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (W $$unsorted)) (forall ((V $$unsorted)) (or (not (R W V)) (Phi V)) )))) + +(declare-fun mvalid ((-> $$unsorted Bool)) Bool) +(assert (= mvalid (lambda ((Phi (-> $$unsorted Bool))) (forall ((W $$unsorted)) (Phi W) )))) + +(declare-fun a1 ($$unsorted $$unsorted) Bool) +(declare-fun a2 ($$unsorted $$unsorted) Bool) +(declare-fun a3 ($$unsorted $$unsorted) Bool) + +(declare-fun jan () mu) +(declare-fun cola () mu) + +(declare-fun likes (mu mu $$unsorted) Bool) + +(declare-fun very_much_likes (mu mu $$unsorted) Bool) + +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mbox a3 (mimplies (mand (likes X Y) (mand (mbox a1 (likes X Y)) (mbox a2 (likes X Y)))) (very_much_likes X Y)) __flatten_var_0)) __flatten_var_0))))) + +(check-sat)
\ No newline at end of file |