simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

test: add some regression tests

Browse source
This commit is contained in:
Simon Cruanes 2020-02-21 16:46:57 -06:00
parent da3cb275be
commit 0b283a384d
3 changed files with 93 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

31
tests/sat/typed_v2l20091.cvc.smt2 Normal file
View file

@ -0,0 +1,31 @@
(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 () list)
(declare-fun x4 () list)
(declare-fun x5 () tree)
(declare-fun x6 () tree)
(assert (and (= (ite ((_ is cons) x4) (cdr x4) null) null) (not (= (cons (leaf (ite ((_ is leaf) (leaf x2)) (data (leaf x2)) zero)) (cons x6 (ite ((_ is node) (leaf zero)) (children (leaf zero)) null))) null))))
(check-sat)
(exit)

34
tests/sat/typed_v3l60005.cvc.smt2 Normal file
View file

@ -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 (and (and (and (not (= (leaf x3) (leaf (succ x1)))) (= x3 (ite ((_ is leaf) x8) (data x8) zero))) (not ((_ is cons) null))) (= x8 x9)) (= (node x5) (ite ((_ is cons) x6) (car x6) (leaf zero)))) (not (= x4 (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) x9) (children x9) null)) (cdr (ite ((_ is node) x9) (children x9) null)) null)) (cdr (ite ((_ is cons) (ite ((_ is node) x9) (children x9) null)) (cdr (ite ((_ is node) x9) (children x9) null)) null)) null)) (cdr (ite ((_ is cons) (ite ((_ is cons) (ite ((_ is node) x9) (children x9) null)) (cdr (ite ((_ is node) x9) (children x9) null)) null)) (cdr (ite ((_ is cons) (ite ((_ is node) x9) (children x9) null)) (cdr (ite ((_ is node) x9) (children x9) null)) null)) null)) null)))))
(check-sat)
(exit)

28
tests/unsat/typed_v1l90014.cvc.smt2 Normal file
View file

File diff suppressed because one or more lines are too long