From 6aae70f15a31ab4fa03c240494d71bcbe6f6b6d9 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 17 Jan 2020 19:12:50 -0600 Subject: [PATCH] test: add more regression tests for datatypes --- tests/sat/typed_v3l30001.cvc.smt2 | 34 +++++++++++++++++ tests/sat/v1l20035.cvc.smt2 | 28 ++++++++++++++ tests/sat/v3l20077.cvc.smt2 | 34 +++++++++++++++++ tests/unsat/typed_v10l40007.cvc.smt2 | 55 ++++++++++++++++++++++++++++ tests/unsat/typed_v3l20047.cvc.smt2 | 34 +++++++++++++++++ tests/unsat/typed_v3l90060.cvc.smt2 | 34 +++++++++++++++++ 6 files changed, 219 insertions(+) create mode 100644 tests/sat/typed_v3l30001.cvc.smt2 create mode 100644 tests/sat/v1l20035.cvc.smt2 create mode 100644 tests/sat/v3l20077.cvc.smt2 create mode 100644 tests/unsat/typed_v10l40007.cvc.smt2 create mode 100644 tests/unsat/typed_v3l20047.cvc.smt2 create mode 100644 tests/unsat/typed_v3l90060.cvc.smt2 diff --git a/tests/sat/typed_v3l30001.cvc.smt2 b/tests/sat/typed_v3l30001.cvc.smt2 new file mode 100644 index 00000000..6fc4c0ea --- /dev/null +++ b/tests/sat/typed_v3l30001.cvc.smt2 @@ -0,0 +1,34 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status sat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () list) +(declare-fun x5 () list) +(declare-fun x6 () list) +(declare-fun x7 () tree) +(declare-fun x8 () tree) +(declare-fun x9 () tree) + +(assert (and (and (not ((_ is node) (leaf zero))) ((_ is succ) x1)) (= (leaf x1) (ite ((_ is cons) x5) (car x5) (leaf zero))))) +(check-sat) +(exit) + + diff --git a/tests/sat/v1l20035.cvc.smt2 b/tests/sat/v1l20035.cvc.smt2 new file mode 100644 index 00000000..4f31091b --- /dev/null +++ b/tests/sat/v1l20035.cvc.smt2 @@ -0,0 +1,28 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status sat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () list) +(declare-fun x3 () tree) + +(assert (and (= (cons x3 (cdr x2)) (cons x3 (cdr (children (node (cdr x2)))))) (not (= (pred (pred (data (node (cdr (children (leaf (data (car (children (leaf zero))))))))))) (pred (pred x1)))))) +(check-sat) +(exit) + + diff --git a/tests/sat/v3l20077.cvc.smt2 b/tests/sat/v3l20077.cvc.smt2 new file mode 100644 index 00000000..1aabb13f --- /dev/null +++ b/tests/sat/v3l20077.cvc.smt2 @@ -0,0 +1,34 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status sat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () list) +(declare-fun x5 () list) +(declare-fun x6 () list) +(declare-fun x7 () tree) +(declare-fun x8 () tree) +(declare-fun x9 () tree) + +(assert (and (not ((_ is zero) x1)) (= (cdr x6) x6))) +(check-sat) +(exit) + + diff --git a/tests/unsat/typed_v10l40007.cvc.smt2 b/tests/unsat/typed_v10l40007.cvc.smt2 new file mode 100644 index 00000000..9a371f06 --- /dev/null +++ b/tests/unsat/typed_v10l40007.cvc.smt2 @@ -0,0 +1,55 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status unsat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () nat) +(declare-fun x5 () nat) +(declare-fun x6 () nat) +(declare-fun x7 () nat) +(declare-fun x8 () nat) +(declare-fun x9 () nat) +(declare-fun x10 () nat) +(declare-fun x11 () list) +(declare-fun x12 () list) +(declare-fun x13 () list) +(declare-fun x14 () list) +(declare-fun x15 () list) +(declare-fun x16 () list) +(declare-fun x17 () list) +(declare-fun x18 () list) +(declare-fun x19 () list) +(declare-fun x20 () list) +(declare-fun x21 () tree) +(declare-fun x22 () tree) +(declare-fun x23 () tree) +(declare-fun x24 () tree) +(declare-fun x25 () tree) +(declare-fun x26 () tree) +(declare-fun x27 () tree) +(declare-fun x28 () tree) +(declare-fun x29 () tree) +(declare-fun x30 () tree) + +(assert (and (and (and (not (= x29 x25)) (= (succ x8) (ite ((_ is succ) (ite ((_ is succ) x8) (pred x8) zero)) (pred (ite ((_ is succ) x8) (pred x8) zero)) zero))) (not (= x21 x27))) (not ((_ is cons) x14)))) +(check-sat) +(exit) + + diff --git a/tests/unsat/typed_v3l20047.cvc.smt2 b/tests/unsat/typed_v3l20047.cvc.smt2 new file mode 100644 index 00000000..03a74b85 --- /dev/null +++ b/tests/unsat/typed_v3l20047.cvc.smt2 @@ -0,0 +1,34 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status unsat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () list) +(declare-fun x5 () list) +(declare-fun x6 () list) +(declare-fun x7 () tree) +(declare-fun x8 () tree) +(declare-fun x9 () tree) + +(assert (and (not ((_ is zero) (ite ((_ is succ) (ite ((_ is leaf) x8) (data x8) zero)) (pred (ite ((_ is leaf) x8) (data x8) zero)) zero))) (= (ite ((_ is cons) x4) (car x4) (leaf zero)) (node x4)))) +(check-sat) +(exit) + + diff --git a/tests/unsat/typed_v3l90060.cvc.smt2 b/tests/unsat/typed_v3l90060.cvc.smt2 new file mode 100644 index 00000000..28c9334a --- /dev/null +++ b/tests/unsat/typed_v3l90060.cvc.smt2 @@ -0,0 +1,34 @@ +(set-info :smt-lib-version 2.6) +(set-logic QF_DT) +(set-info :source | +Generated by: Andrew Reynolds +Generated on: 2017-04-28 +Generator: Random, converted to v2.6 by CVC4 +Application: Regressions for datatypes decision procedure. +Target solver: CVC3 +Publications: "An Abstract Decision Procedure for Satisfiability in the Theory of Inductive Data Types" by Clark Barrett, Igor Shikanian, and Cesare Tinelli, Journal on Satisfiability, Boolean Modeling and Computation 2007. +|) +(set-info :license "https://creativecommons.org/licenses/by/4.0/") +(set-info :category "random") +(set-info :status unsat) + + +(declare-datatypes ((nat 0)(list 0)(tree 0)) (((succ (pred nat)) (zero)) +((cons (car tree) (cdr list)) (null)) +((node (children list)) (leaf (data nat))) +)) +(declare-fun x1 () nat) +(declare-fun x2 () nat) +(declare-fun x3 () nat) +(declare-fun x4 () list) +(declare-fun x5 () list) +(declare-fun x6 () list) +(declare-fun x7 () tree) +(declare-fun x8 () tree) +(declare-fun x9 () tree) + +(assert (and (and (and (and (and (and (and (and (= (node x4) x9) (= x7 x7)) ((_ is succ) (succ x2))) ((_ is succ) (succ (ite ((_ is succ) (ite ((_ is leaf) (leaf zero)) (data (leaf zero)) zero)) (pred (ite ((_ is leaf) (leaf zero)) (data (leaf zero)) zero)) zero)))) ((_ is zero) (ite ((_ is succ) zero) (pred zero) zero))) (= x5 null)) (not (= (ite ((_ is cons) (ite ((_ is node) x8) (children x8) null)) (car (ite ((_ is node) x8) (children x8) null)) (leaf zero)) x7))) (not (= zero x1))) (= (ite ((_ is cons) (cons (ite ((_ is cons) (ite ((_ is node) x9) (children x9) null)) (car (ite ((_ is node) x9) (children x9) null)) (leaf zero)) null)) (car (cons (ite ((_ is cons) (ite ((_ is node) x9) (children x9) null)) (car (ite ((_ is node) x9) (children x9) null)) (leaf zero)) null)) (leaf zero)) x9))) +(check-sat) +(exit) + +