diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-12 16:29:20 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-12 16:29:20 -0500 |
| commit | dd01099518aab8d42d788dfadadbe11763ec9d18 (patch) | |
| tree | ab3accd00c5e4ee3f2035349b9387bf8b9d85e90 /test | |
| parent | 4ff2946e1338d3f500b7e6bababee50fadad68d6 (diff) | |
Bug fixes related to parametric datatypes + theory combination + quantifiers. Add regression.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/quantifiers/parametric-lists.smt2 | 42 |
2 files changed, 44 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index b51313deb..6b5e0d1ed 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -78,7 +78,8 @@ TESTS = \ pure_dt_cbqi.smt2 \ florian-case-ax.smt2 \ double-pattern.smt2 \ - qcf-rel-dom-opt.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/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) + |