From b8ddf766460bfcf475e08ff52c889246e78f76cc Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Sun, 22 Jun 2014 01:17:27 -0400 Subject: Renaming of SMT2 operator names, kinds for set theory * SET_SINGLETON kind renamed to just SINGLETON * "setenum" smt2 opertor renamed to "singleton"[1] * "in" smt2 operator renamed to "member"[2] [1] It was anyhow accepting exactly one argument, so was bit misleading to call set enumerator. [2] The corresponding kind was called MEMBER, so this will also make them consistent. Only inconsistency now is for subset: kind is called SUBSET but operator is called "subseteq". --- test/regress/regress0/sets/sets-new.smt2 | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'test/regress/regress0/sets/sets-new.smt2') diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index accb09799..0f43ee10d 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -6,11 +6,11 @@ (declare-fun A () SetInt) (declare-fun B () SetInt) (declare-fun x () Int) -(assert (in x (union A B))) +(assert (member x (union A B))) -(assert (not (in x (intersection A B)))) -(assert (not (in x (setminus A B)))) -;(assert (not (in x (setminus B A)))) -;(assert (in x B)) +(assert (not (member x (intersection A B)))) +(assert (not (member x (setminus A B)))) +;(assert (not (member x (setminus B A)))) +;(assert (member x B)) (check-sat) -- cgit v1.2.3