test: add some basic datatype tests

tests/sat/v1l20001.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 (not ((_ is leaf) (node (cdr (cons (leaf (data (leaf zero))) x2))))) ((_ is cons) (cons x3 (cdr (cons (node x2) (cons x3 (cdr (cdr (cdr (children (car (cons (car null) null)))))))))))))
+(check-sat)
+(exit)
+
+

tests/sat/v1l20060.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 (not ((_ is cons) x2)) (not (= (leaf (data (leaf x1))) x3))))
+(check-sat)
+(exit)
+
+

tests/sat/v3l30062.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 (= x5 null)) ((_ is leaf) x8)) (not (= x2 (pred x1)))))
+(check-sat)
+(exit)
+
+

tests/sat/v5l90073.cvc.smt2

@@ -0,0 +1,40 @@
+(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 () nat)
+(declare-fun x5 () nat)
+(declare-fun x6 () list)
+(declare-fun x7 () list)
+(declare-fun x8 () list)
+(declare-fun x9 () list)
+(declare-fun x10 () list)
+(declare-fun x11 () tree)
+(declare-fun x12 () tree)
+(declare-fun x13 () tree)
+(declare-fun x14 () tree)
+(declare-fun x15 () tree)
+
+(assert (and (and (and (and (and (and (and (and (not ((_ is cons) x10)) ((_ is cons) x8)) (not (= (leaf x4) x12))) (not (= (pred x1) (pred (pred (data (node (cdr null)))))))) (not (= x4 x2))) (not ((_ is node) x12))) (not (= x3 (succ zero)))) (= x6 x10)) (not (= (cons (node x10) x10) (cdr null)))))
+(check-sat)
+(exit)
+
+

tests/unsat/v1l50092.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 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 () list)
+(declare-fun x3 () tree)
+
+(assert (and (and (and (and (= (node (cons x3 (cdr null))) x3) (= (cdr (cdr (cons (car x2) (cdr null)))) (children (leaf (pred (succ zero)))))) (not (= x2 (cons (leaf x1) x2)))) (= (car x2) x3)) (not ((_ is succ) zero))))
+(check-sat)
+(exit)
+
+

tests/unsat/v1l90033.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 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 () list)
+(declare-fun x3 () tree)
+
+(assert (and (and (and (and (and (and (and (and (not ((_ is cons) x2)) (not ((_ is node) (car (cdr (cdr (cdr null))))))) (= null (cons (car x2) null))) (not ((_ is cons) null))) (= (node null) (leaf zero))) (not ((_ is zero) (data x3)))) ((_ is cons) null)) ((_ is zero) x1)) (not (= (pred zero) (data (leaf x1))))))
+(check-sat)
+(exit)
+
+