diff options
Diffstat (limited to 'test/regress/regress0/quantifiers')
11 files changed, 358 insertions, 8 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index df146752e..6b5e0d1ed 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -38,10 +38,9 @@ TESTS = \ gauss_init_0030.fof.smt2 \ qcft-javafe.filespace.TreeWalker.006.smt2 \ qcft-smtlib3dbc51.smt2 \ - symmetric_unsat_7.smt2 \ javafe.ast.StmtVec.009.smt2 \ ARI176e1.smt2 \ - bi-artm-s.smt2 \ + bi-artm-s.smt2 \ simp-typ-test.smt2 \ macros-int-real.smt2 \ stream-x2014-09-18-unsat.smt2 \ @@ -65,12 +64,22 @@ TESTS = \ ext-ex-deq-trigger.smt2 \ matching-lia-1arg.smt2 \ RND_4_16.smt2 \ - cdt-0208-to.smt2 \ - psyco-196.smt2 \ - agg-rew-test.smt2 \ - agg-rew-test-cf.smt2 \ - rew-to-0211-dd.smt2 \ - rew-to-scala.smt2 + cdt-0208-to.smt2 \ + psyco-196.smt2 \ + agg-rew-test.smt2 \ + agg-rew-test-cf.smt2 \ + rew-to-0211-dd.smt2 \ + rew-to-scala.smt2 \ + macro-subtype-param.smt2 \ + macros-real-arg.smt2 \ + subtype-param-unk.smt2 \ + subtype-param.smt2 \ + anti-sk-simp.smt2 \ + pure_dt_cbqi.smt2 \ + florian-case-ax.smt2 \ + double-pattern.smt2 \ + qcf-rel-dom-opt.smt2 \ + parametric-lists.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/anti-sk-simp.smt2 b/test/regress/regress0/quantifiers/anti-sk-simp.smt2 new file mode 100755 index 000000000..ba4f9cbb9 --- /dev/null +++ b/test/regress/regress0/quantifiers/anti-sk-simp.smt2 @@ -0,0 +1,10 @@ +; COMMAND-LINE: --quant-anti-skolem +; EXPECT: unsat +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-fun f (Int) Int) +(declare-fun a () Int) +(declare-fun b () Int) +(assert (forall ((X Int)) (< X (f X)))) +(assert (forall ((X Int)) (> (+ a b) (f X)))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/double-pattern.smt2 b/test/regress/regress0/quantifiers/double-pattern.smt2 new file mode 100644 index 000000000..4ce21d446 --- /dev/null +++ b/test/regress/regress0/quantifiers/double-pattern.smt2 @@ -0,0 +1,6 @@ +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) +(assert (forall ((x Int)) (! (! (P x) :pattern ((P x))) :pattern ((P x))))) +(assert (not (P 0))) +(check-sat) diff --git a/test/regress/regress0/quantifiers/florian-case-ax.smt2 b/test/regress/regress0/quantifiers/florian-case-ax.smt2 new file mode 100644 index 000000000..35ebb28e9 --- /dev/null +++ b/test/regress/regress0/quantifiers/florian-case-ax.smt2 @@ -0,0 +1,168 @@ +(set-logic AUFLIA) +(set-info :status unsat) +(declare-sort U 0) +(declare-fun A (U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U U U + U U + U) (Array Int U)) + +(assert + (forall ((v_184 U) (v_185 U) + (v_186 U) (v_187 U) + (v_188 U) (v_189 U) + (v_190 U) (v_191 U) + (v_192 U) (v_193 U) + (v_194 U) (v_195 U) + (v_196 U) (v_197 U) + (v_198 U) (v_199 U) + (v_200 U) (v_201 U) + (v_202 U) (v_203 U) + (v_204 U) (v_205 U) + (v_206 U) (v_207 U) + (v_208 U) (v_209 U) + (v_210 U) (v_211 U) + (v_212 U) (v_213 U) + (v_214 U) (v_215 U) + (v_216 U) (v_217 U) + (v_218 U) (v_219 U) + (v_220 U) (v_221 U) + (v_222 U) (v_223 U) + (v_224 U) (v_225 U) + (v_226 U) (v_227 U) + (v_228 U) (v_229 U) + (v_230 U) (v_231 U) + (v_232 U) (v_233 U) + (v_234 U) (v_235 U) + (v_236 U) (v_237 U) + (v_238 U) (v_239 U) + (v_240 U) (v_241 U) (v_242 Int)) + (let ((v_183 (A v_184 v_185 v_186 v_187 + v_188 v_189 v_190 v_191 v_192 + v_193 v_194 v_195 v_196 v_197 + v_198 v_199 v_200 v_201 v_202 + v_203 v_204 v_205 v_206 v_207 + v_208 v_209 v_210 v_211 v_212 + v_213 v_214 v_215 v_216 v_217 + v_218 v_219 v_220 v_221 v_222 + v_223 v_224 v_225 v_226 v_227 + v_228 v_229 v_230 v_231 v_232 + v_233 v_234 v_235 v_236 v_237 + v_238 v_239 v_240 v_241))) + (ite (= v_242 59) (= (select v_183 v_242) v_240) + (ite (= v_242 58) (= (select v_183 v_242) v_239) + (ite (= v_242 57) (= (select v_183 v_242) v_238) + (ite (= v_242 56) (= (select v_183 v_242) v_237) + (ite (= v_242 55) (= (select v_183 v_242) v_236) + (ite (= v_242 54) (= (select v_183 v_242) v_235) + (ite (= v_242 53) (= (select v_183 v_242) v_234) + (ite (= v_242 52) (= (select v_183 v_242) v_233) + (ite (= v_242 51) (= (select v_183 v_242) v_232) + (ite (= v_242 50) (= (select v_183 v_242) v_231) + (ite (= v_242 49) (= (select v_183 v_242) v_230) + (ite (= v_242 48) (= (select v_183 v_242) v_229) + (ite (= v_242 47) (= (select v_183 v_242) v_228) + (ite (= v_242 46) (= (select v_183 v_242) v_227) + (ite (= v_242 45) (= (select v_183 v_242) v_226) + (ite (= v_242 44) (= (select v_183 v_242) v_225) + (ite (= v_242 43) (= (select v_183 v_242) v_224) + (ite (= v_242 41) (= (select v_183 v_242) v_223) + (ite (= v_242 40) (= (select v_183 v_242) v_222) + (ite (= v_242 39) (= (select v_183 v_242) v_221) + (ite (= v_242 37) (= (select v_183 v_242) v_220) + (ite (= v_242 36) (= (select v_183 v_242) v_219) + (ite (= v_242 34) (= (select v_183 v_242) v_218) + (ite (= v_242 33) (= (select v_183 v_242) v_217) + (ite (= v_242 32) (= (select v_183 v_242) v_216) + (ite (= v_242 31) (= (select v_183 v_242) v_215) + (ite (= v_242 30) (= (select v_183 v_242) v_214) + (ite (= v_242 29) (= (select v_183 v_242) v_213) + (ite (= v_242 28) (= (select v_183 v_242) v_212) + (ite (= v_242 27) (= (select v_183 v_242) v_211) + (ite (= v_242 26) (= (select v_183 v_242) v_210) + (ite (= v_242 25) (= (select v_183 v_242) v_209) + (ite (= v_242 24) (= (select v_183 v_242) v_208) + (ite (= v_242 23) (= (select v_183 v_242) v_207) + (ite (= v_242 22) (= (select v_183 v_242) v_206) + (ite (= v_242 21) (= (select v_183 v_242) v_205) + (ite (= v_242 20) (= (select v_183 v_242) v_204) + (ite (= v_242 19) (= (select v_183 v_242) v_203) + (ite (= v_242 18) (= (select v_183 v_242) v_202) + (ite (= v_242 17) (= (select v_183 v_242) v_201) + (ite (= v_242 16) (= (select v_183 v_242) v_200) + (ite (= v_242 15) (= (select v_183 v_242) v_199) + (ite (= v_242 14) (= (select v_183 v_242) v_198) + (ite (= v_242 13) (= (select v_183 v_242) v_197) + (ite (= v_242 12) (= (select v_183 v_242) v_196) + (ite (= v_242 11) (= (select v_183 v_242) v_195) + (ite (= v_242 10) (= (select v_183 v_242) v_194) + (ite (= v_242 9) (= (select v_183 v_242) v_193) + (ite (= v_242 8) (= (select v_183 v_242) v_192) + (ite (= v_242 7) (= (select v_183 v_242) v_191) + (ite (= v_242 6) (= (select v_183 v_242) v_190) + (ite (= v_242 5) (= (select v_183 v_242) v_189) + (ite (= v_242 4) (= (select v_183 v_242) v_188) + (ite (= v_242 3) (= (select v_183 v_242) v_187) + (ite (= v_242 2) (= (select v_183 v_242) v_186) + (ite (= v_242 1) (= (select v_183 v_242) v_185) + (ite (= v_242 0) (= (select v_183 v_242) v_184) + (= (select v_183 v_242) v_241))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + +(declare-const c_184 U) (declare-const c_185 U) +(declare-const c_186 U) (declare-const c_187 U) +(declare-const c_188 U) (declare-const c_189 U) +(declare-const c_190 U) (declare-const c_191 U) +(declare-const c_192 U) (declare-const c_193 U) +(declare-const c_194 U) (declare-const c_195 U) +(declare-const c_196 U) (declare-const c_197 U) +(declare-const c_198 U) (declare-const c_199 U) +(declare-const c_200 U) (declare-const c_201 U) +(declare-const c_202 U) (declare-const c_203 U) +(declare-const c_204 U) (declare-const c_205 U) +(declare-const c_206 U) (declare-const c_207 U) +(declare-const c_208 U) (declare-const c_209 U) +(declare-const c_210 U) (declare-const c_211 U) +(declare-const c_212 U) (declare-const c_213 U) +(declare-const c_214 U) (declare-const c_215 U) +(declare-const c_216 U) (declare-const c_217 U) +(declare-const c_218 U) (declare-const c_219 U) +(declare-const c_220 U) (declare-const c_221 U) +(declare-const c_222 U) (declare-const c_223 U) +(declare-const c_224 U) (declare-const c_225 U) +(declare-const c_226 U) (declare-const c_227 U) +(declare-const c_228 U) (declare-const c_229 U) +(declare-const c_230 U) (declare-const c_231 U) +(declare-const c_232 U) (declare-const c_233 U) +(declare-const c_234 U) (declare-const c_235 U) +(declare-const c_236 U) (declare-const c_237 U) +(declare-const c_238 U) (declare-const c_239 U) +(declare-const c_240 U) (declare-const c_241 U) + +(declare-fun b () Int) +(declare-fun c () U) +(assert (not (= (select (A c_184 c_185 c_186 c_187 + c_188 c_189 c_190 c_191 c_192 + c_193 c_194 c_195 c_196 c_197 + c_198 c_199 c_200 c_201 c_202 + c_203 c_204 c_205 c_206 c_207 + c_208 c_209 c_210 c_211 c_212 + c_213 c_214 c_215 c_216 c_217 + c_218 c_219 c_220 c_221 c_222 + c_223 c_224 c_225 c_226 c_227 + c_228 c_229 c_230 c_231 c_232 + c_233 c_234 c_235 c_236 c_237 + c_238 c_239 c_240 c_241) b) c))) +(assert (and (= b 28) (= c c_212))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 new file mode 100644 index 000000000..20de79047 --- /dev/null +++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --macros-quant +; EXPECT: unknown +; this will fail if type rule for APPLY_UF requires to be subtypes +(set-logic ALL_SUPPORTED) + +(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) + +(declare-fun R ((List Int)) Bool) +(assert (forall ((x (List Int))) (R x))) +(declare-fun j1 () (List Real)) +(assert (not (R j1))) + +(declare-fun Q ((Array Real Int)) Bool) +(assert (forall ((x (Array Real Int))) (Q x))) +(declare-fun j2 () (Array Int Real)) +(assert (not (Q j2))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2 new file mode 100644 index 000000000..675c96d68 --- /dev/null +++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2 @@ -0,0 +1,11 @@ +; COMMAND-LINE: --macros-quant +; EXPECT: unsat +; this will fail if type rule for APPLY_UF is made strict +(set-logic UFLIRA) +(declare-fun P (Int) Bool) +(assert (forall ((x Int)) (P x))) +(declare-fun k () Real) +(declare-fun k2 () Int) +(assert (or (not (P k)) (not (P k2)))) +(assert (= k 0)) +(check-sat) diff --git a/test/regress/regress0/quantifiers/parametric-lists.smt2 b/test/regress/regress0/quantifiers/parametric-lists.smt2 new file mode 100644 index 000000000..c117934f8 --- /dev/null +++ b/test/regress/regress0/quantifiers/parametric-lists.smt2 @@ -0,0 +1,42 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes (T) ((List (cons (head T) (tail (List T))) (nil)))) +(declare-datatypes () ((KV (kv (key Int) (value Int)) (nilKV)))) ; key value pair +(declare-fun mapper ((List Int)) (List KV)) +(assert + (forall + ((input (List Int))) + (ite + (= input (as nil (List Int))) + (= (as nil (List KV)) (mapper input)) + (= (cons (kv 0 (head input)) (mapper (tail input))) (mapper input)) + ) + ) +) +(declare-fun reduce ((List KV)) Int) +(assert + (forall + ((inputk (List KV))) + (ite + (= inputk (as nil (List KV))) + (= 0 (reduce inputk)) + (= (+ (value (head inputk)) (reduce (tail inputk))) (reduce inputk)) + ) + ) +) +(declare-fun sum ((List Int)) Int) +(assert + (forall + ((input (List Int))) + (ite + (= input (as nil (List Int))) + (= 0 (sum input)) + (= (+ (head input) (sum (tail input))) (sum input)) + ) + ) +) +(assert + (not (= (sum (cons 0 (as nil (List Int)))) (reduce (mapper (cons 0 (as nil (List Int))))))) +) +(check-sat) + diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 new file mode 100644 index 000000000..a11d14e4a --- /dev/null +++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () ((nat (Suc (pred nat)) (zero))))
+(declare-fun y () nat)
+(assert (forall ((x nat)) (not (= y (Suc x)))))
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 new file mode 100644 index 000000000..539f181af --- /dev/null +++ b/test/regress/regress0/quantifiers/qcf-rel-dom-opt.smt2 @@ -0,0 +1,45 @@ +(set-logic UFLIA) +(set-info :status unsat) +(declare-fun P (Int) Bool) + +(assert (P 0)) +(assert (P 1)) +(assert (P 2)) +(assert (P 3)) +(assert (P 4)) +(assert (P 5)) +(assert (P 6)) +(assert (P 7)) +(assert (P 8)) +(assert (P 9)) + +(assert (P 10)) +(assert (P 11)) +(assert (P 12)) +(assert (P 13)) +(assert (P 14)) +(assert (P 15)) +(assert (P 16)) +(assert (P 17)) +(assert (P 18)) +(assert (P 19)) + +(assert (P 20)) +(assert (P 21)) +(assert (P 22)) +(assert (P 23)) +(assert (P 24)) +(assert (P 25)) +(assert (P 26)) +(assert (P 27)) +(assert (P 28)) +(assert (P 29)) + +(declare-fun Q (Int Int Int Int Int) Bool) +(assert (forall ((x Int) (y Int) (z Int) (w Int) (q Int)) (or (not (P x)) (not (P y)) (not (P z)) (not (P w)) (not (P q)) (Q x y z w q)))) + +(declare-fun R (Int) Bool) +(assert (R 0)) +(assert (forall ((x Int)) (not (R x)))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 new file mode 100644 index 000000000..836449cb9 --- /dev/null +++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 @@ -0,0 +1,19 @@ +; COMMAND-LINE: +; EXPECT: unknown +; this will fail if type rule for APPLY_UF requires arguments to be subtypes +(set-logic ALL_SUPPORTED) + +(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) + +(declare-fun R ((List Int)) Bool) + +(assert (forall ((x (List Int))) (R x))) +(declare-fun j1 () (List Real)) +(assert (not (R j1))) + +(declare-fun Q ((Array Int Real)) Bool) +(assert (forall ((x (Array Int Int))) (Q x))) +(declare-fun j2 () (Array Int Real)) +(assert (not (Q j2))) + +(check-sat) diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2 new file mode 100644 index 000000000..08615abf6 --- /dev/null +++ b/test/regress/regress0/quantifiers/subtype-param.smt2 @@ -0,0 +1,16 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) + +(declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) + +(declare-fun R ((List Int)) Bool) +(assert (forall ((x (List Real))) (R x))) + +(declare-fun Q ((Array Int Real)) Bool) +(assert (forall ((x (Array Int Int))) (Q x))) + +(declare-fun k1 () (List Int)) +(declare-fun k2 () (Array Real Int)) +(assert (or (not (R k1)) (not (Q k2)))) + +(check-sat) |