diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-09-09 14:47:53 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-02-21 07:25:13 -0500 |
commit | 50c26544c83a71e87efa487e4af063b1b5647c0f (patch) | |
tree | 82d4f3b2632a2cf06aff70550f37f80dc80d9543 /src/printer | |
parent | 53b8499f48a00dc876d56c76fbc79aafe5803529 (diff) |
add new theory (sets)
Specification (smt2) -- as per this commit, subject to change
- Parameterized sort Set, e.g. (Set Int)
- Empty set constant (typed), use with "as" to specify the type, e.g.
(as emptyset (Set Int))
- Create a singleton set
(setenum X (Set X)) : creates singleton set
- Functions/operators
(union (Set X) (Set X) (Set X))
(intersection (Set X) (Set X) (Set X))
(setminus (Set X) (Set X) (Set X))
- Predicates
(in X (Set X) Bool) : membership
(subseteq (Set X) (Set X) Bool) : set containment
Diffstat (limited to 'src/printer')
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5dc3043af..fcb352ea7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -203,6 +203,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; } + case kind::EMPTYSET: + out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")"; + break; + default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant @@ -343,7 +347,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, stillNeedToPrintParams = false; break; - // datatypes + // sets + case kind::UNION: + case kind::INTERSECTION: + case kind::SETMINUS: + case kind::SUBSET: + case kind::IN: + case kind::SET_TYPE: + case kind::SET_SINGLETON: out << smtKindString(k) << " "; break; + + // datatypes case kind::APPLY_TYPE_ASCRIPTION: { out << "as "; toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types); @@ -528,6 +541,14 @@ static string smtKindString(Kind k) throw() { case kind::BITVECTOR_SIGN_EXTEND: return "sign_extend"; case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left"; case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right"; + + case kind::UNION: return "union"; + case kind::INTERSECTION: return "intersection"; + case kind::SETMINUS: return "setminus"; + case kind::SUBSET: return "subseteq"; + case kind::IN: return "in"; + case kind::SET_TYPE: return "Set"; + case kind::SET_SINGLETON: return "setenum"; default: ; /* fall through */ } |