tst: add some regression tests; remove dead file

tests/logitest.sexp

@@ -1,22 +0,0 @@
-
-(prover
-  (name sidekick-dev)
-  (cmd "${cur_dir}/../sidekick --no-check --time $timeout $file")
-  (unsat "Unsat")
-  (sat "Sat")
-  (unknown "Timeout|Unknown")
-  (version "git:."))
-
-(dir
-  (path $cur_dir)
-  (pattern ".*.(smt2|cnf)")
-  (expect (try (run smtlib-read-status) (run z3))))
-
-(task
-  (name sidekick-local-test)
-  (action
-    (run_provers
-      (provers sidekick-dev)
-      (timeout 10)
-      (dirs))))
-

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

tests/unsat/t_cstor1.smt2.tmp

@@ -0,0 +1,23 @@
+
+; test for constructors
+; :status unsat
+
+(declare-sort nat 0)
+(declare-cstor zero () nat)
+(declare-cstor succ (nat) nat)
+
+(declare-fun n0 () nat)
+(declare-fun n1 () nat)
+(declare-fun n2 () nat)
+
+(assert (= n0 (succ (succ (succ (succ zero))))))
+(assert (= n1 (succ (succ n2))))
+(assert (not (= n1 (succ (succ (succ (succ zero)))))))
+
+; (check-sat) ; sat
+
+(assert (= n2 (succ (succ zero))))
+
+(check-sat) ; unsat
+
+(exit)

tests/unsat/typed_v3l30091.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 ((_ is null) x4) (not ((_ is zero) zero))) (not (= x3 x1))))
+(check-sat)
+(exit)
+
+

tests/unsat/v3l60049.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 (not ((_ is leaf) x7)) ((_ is zero) x3)) (not ((_ is cons) x6))) (not ((_ is succ) zero))) (not (= x6 x5))) (not ((_ is cons) x5))))
+(check-sat)
+(exit)
+
+

tests/unsat/v3l90003.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 (= x4 null) (not (= x5 (children x7)))) (not ((_ is leaf) (car null)))) (not ((_ is node) x8))) (= (data (leaf zero)) x3)) (not (= x9 x7))) (not (= (pred x2) (data x9)))) ((_ is null) (cdr x6))) (= (car null) (leaf (succ x1)))))
+(check-sat)
+(exit)
+
+