diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-09-22 13:38:46 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-22 20:38:46 +0000 |
commit | e116c00719a7574064c09da4abb10b3297415c90 (patch) | |
tree | e71e489d7c591067eeab793a80d139e47718befe /test/regress/regress1/trim.cvc.smt2 | |
parent | ba259d66be877de3cc77e4f62083905ace942c82 (diff) |
Remove CVC language support (#7219)
This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.
Diffstat (limited to 'test/regress/regress1/trim.cvc.smt2')
-rw-r--r-- | test/regress/regress1/trim.cvc.smt2 | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/regress1/trim.cvc.smt2 b/test/regress/regress1/trim.cvc.smt2 new file mode 100644 index 000000000..31dc96ca3 --- /dev/null +++ b/test/regress/regress1/trim.cvc.smt2 @@ -0,0 +1,26 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-datatypes ((myType 0)) (((A) (B)))) + +(declare-datatypes ((|__cvc5_record_pos_(Set myType)_neg_(Set myType)| 0)) (((|__cvc5_record_pos_(Set myType)_neg_(Set myType)_ctor| (pos (Set myType)) (neg (Set myType)))))) + + + +(declare-fun emptymyTypeSet () (Set myType)) +(assert (= emptymyTypeSet (as emptyset (Set myType)))) +(declare-fun d () (Array myType |__cvc5_record_pos_(Set myType)_neg_(Set myType)|)) +(declare-fun l () (Array myType (Set String))) +(assert (= (select l A) (union (singleton "L") (singleton "H")))) +(assert (= (select l B) (singleton "L"))) +(declare-fun ic0_i () (Set myType)) +(declare-fun ic0_c () (Set myType)) +(assert (forall ((r myType)) (=> (member r ic0_i) (forall ((r2 myType)) (=> (member r2 (neg (select d r))) (member r2 ic0_c)))))) +(assert (subset (singleton A) ic0_i)) +(assert (or (exists ((e0 myType)) (=> (member e0 ic0_i) (subset (select l A) (select l e0)))) (subset (intersection ic0_i ic0_c) emptymyTypeSet))) +(declare-fun ic1_i () (Set myType)) +(declare-fun ic1_c () (Set myType)) +(assert (forall ((r myType)) (=> (member r (pos (select d B))) (member r ic1_i)))) +(assert (or (exists ((e1 myType)) (=> (member e1 ic1_i) (subset (select l B) (select l e1)))) (subset (intersection ic1_i ic1_c) emptymyTypeSet))) +(check-sat) |