From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 30 Jun 2014 17:28:09 +0000 (-0400)
Subject: Merge pull request #47 from kbansal/sets
X-Git-Tag: cvc5-1.0.0~6712
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b06d25a020240fa455798308418ad802f9f40ea3;p=cvc5.git

Merge pull request #47 from kbansal/sets

Sets theory operators in SMTLIB2 and kinds to use from API have changed. They now are:

SMTLIB: emptyset, singleton*, insert*, union, intersection, setminus, member*, subset*
API: EMPTYSET, SINGLETON*, INSERT*, UNION, INTERSECTION, SETMINUS, MEMBER, SUBSET

(those marked with [*] have changed or been added, others are as earlier)

In the set-logic string use FS to enable sets.

A not-so-well-tested perl command for translating old benchmarks:
  perl -pi -e 's/\(set-logic (.+)_SETS\)/\(set-logic \1FS\)/; s/\(in\b/\(member/g; s/\(setenum\b/\(singleton/g; s/\(subseteq\b/\(subset/g; '
---

b06d25a020240fa455798308418ad802f9f40ea3