diff options
Diffstat (limited to 'test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2')
| -rw-r--r-- | test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 | 101 |
1 files changed, 101 insertions, 0 deletions
diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 new file mode 100644 index 000000000..1670e0711 --- /dev/null +++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 @@ -0,0 +1,101 @@ +; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-check-proofs +; EXPECT: unsat + +(set-logic ALL) +(declare-sort $$unsorted 0) +(declare-sort mu 0) +(declare-fun meq_ind (mu mu $$unsorted) Bool) +(assert (= meq_ind (lambda ((X mu) (Y mu) (W $$unsorted)) (= X Y)))) +(declare-fun meq_prop ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= meq_prop (lambda ((X (-> $$unsorted Bool)) (Y (-> $$unsorted Bool)) (W $$unsorted)) (= (X W) (Y W))))) +(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 mimplied ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mimplied (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mor (mnot Psi) Phi __flatten_var_0)))) +(declare-fun mequiv ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mequiv (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mand (mimplies Phi Psi) (mimplies Psi Phi) __flatten_var_0)))) +(declare-fun mxor ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mxor (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mequiv 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 mforall_prop ((-> (-> $$unsorted Bool) $$unsorted Bool) $$unsorted) Bool) +(assert (= mforall_prop (lambda ((Phi (-> (-> $$unsorted Bool) $$unsorted Bool)) (W $$unsorted)) (forall ((P (-> $$unsorted Bool))) (Phi P W) )))) +(declare-fun mexists_ind ((-> mu $$unsorted Bool) $$unsorted) Bool) +(assert (= mexists_ind (lambda ((Phi (-> mu $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mnot (Phi X) __flatten_var_0))) __flatten_var_0)))) +(declare-fun mexists_prop ((-> (-> $$unsorted Bool) $$unsorted Bool) $$unsorted) Bool) +(assert (= mexists_prop (lambda ((Phi (-> (-> $$unsorted Bool) $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mforall_prop (lambda ((P (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (Phi P) __flatten_var_0))) __flatten_var_0)))) +(declare-fun mtrue ($$unsorted) Bool) +(assert (= mtrue (lambda ((W $$unsorted)) true))) +(declare-fun mfalse ($$unsorted) Bool) +(assert (= mfalse (mnot mtrue))) +(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 mdia ((-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool) +(assert (= mdia (lambda ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted)) (mnot (mbox R (mnot Phi)) __flatten_var_0)))) +(declare-fun mreflexive ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mreflexive (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted)) (R S S) )))) +(declare-fun msymmetric ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= msymmetric (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted)) (=> (R S T) (R T S)) )))) +(declare-fun mserial ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mserial (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted)) (exists ((T $$unsorted)) (R S T) ) )))) +(declare-fun mtransitive ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mtransitive (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (and (R S T) (R T U)) (R S U)) )))) +(declare-fun meuclidean ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= meuclidean (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (and (R S T) (R S U)) (R T U)) )))) +(declare-fun mpartially_functional ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mpartially_functional (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (and (R S T) (R S U)) (= T U)) )))) +(declare-fun mfunctional ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mfunctional (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted)) (exists ((T $$unsorted)) (and (R S T) (forall ((U $$unsorted)) (=> (R S U) (= T U)) )) ) )))) +(declare-fun mweakly_dense ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mweakly_dense (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (R S T) (exists ((U $$unsorted)) (and (R S U) (R U T)) )) )))) +(declare-fun mweakly_connected ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mweakly_connected (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (and (R S T) (R S U)) (or (R T U) (= T U) (R U T))) )))) +(declare-fun mweakly_directed ((-> $$unsorted $$unsorted Bool)) Bool) +(assert (= mweakly_directed (lambda ((R (-> $$unsorted $$unsorted Bool))) (forall ((S $$unsorted) (T $$unsorted) (U $$unsorted)) (=> (and (R S T) (R S U)) (exists ((V $$unsorted)) (and (R T V) (R U V)) )) )))) +(declare-fun mvalid ((-> $$unsorted Bool)) Bool) +(assert (= mvalid (lambda ((Phi (-> $$unsorted Bool))) (forall ((W $$unsorted)) (Phi W) )))) +(declare-fun minvalid ((-> $$unsorted Bool)) Bool) +(assert (= minvalid (lambda ((Phi (-> $$unsorted Bool))) (forall ((W $$unsorted)) (not (Phi W)) )))) +(declare-fun msatisfiable ((-> $$unsorted Bool)) Bool) +(assert (= msatisfiable (lambda ((Phi (-> $$unsorted Bool))) (exists ((W $$unsorted)) (Phi W) )))) +(declare-fun mcountersatisfiable ((-> $$unsorted Bool)) Bool) +(assert (= mcountersatisfiable (lambda ((Phi (-> $$unsorted Bool))) (exists ((W $$unsorted)) (not (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 piotr () mu) +(declare-fun cola () mu) +(declare-fun pepsi () mu) +(declare-fun beer () mu) +(declare-fun likes (mu mu $$unsorted) Bool) +(declare-fun very_much_likes (mu mu $$unsorted) Bool) +(declare-fun possibly_likes (mu mu $$unsorted) Bool) +(assert (mvalid (mbox a1 (likes jan cola)))) +(assert (mvalid (mbox a1 (likes piotr pepsi)))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mbox a1 (mimplies (mdia a1 (likes X pepsi)) (likes X cola)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mbox a1 (mimplies (mdia a1 (likes X cola)) (likes X pepsi)) __flatten_var_0))))) +(assert (mvalid (mbox a2 (likes jan pepsi)))) +(assert (mvalid (mbox a1 (likes piotr cola)))) +(assert (mvalid (mbox a1 (likes piotr beer)))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mbox a2 (mimplies (likes X pepsi) (likes X cola)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mbox a2 (mimplies (likes X cola) (likes X pepsi)) __flatten_var_0))))) +(assert (mvalid (mbox a3 (likes jan cola)))) +(assert (mvalid (mdia a3 (likes piotr pepsi)))) +(assert (mvalid (mdia a1 (likes piotr beer)))) +(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))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mimplies (mbox a3 (very_much_likes X Y)) (very_much_likes X Y) __flatten_var_0)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mimplies (mdia a3 (very_much_likes X Y)) (likes X Y) __flatten_var_0)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mimplies (mdia a1 (likes X Y)) (possibly_likes X Y) __flatten_var_0)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mimplies (mdia a2 (likes X Y)) (possibly_likes X Y) __flatten_var_0)) __flatten_var_0))))) +(assert (mvalid (mforall_ind (lambda ((X mu) (__flatten_var_0 $$unsorted)) (mforall_ind (lambda ((Y mu) (__flatten_var_0 $$unsorted)) (mimplies (mdia a3 (likes X Y)) (possibly_likes X Y) __flatten_var_0)) __flatten_var_0))))) +(assert (not (mvalid (very_much_likes jan cola)))) +(meta-info :filename "AGT034^2") + +(check-sat)
\ No newline at end of file |