projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: be47019) | patch
sets: "insert" operator
authorKshitij Bansal <kshitij@cs.nyu.edu>
Sun, 29 Jun 2014 22:44:40 +0000 (18:44 -0400)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Sun, 29 Jun 2014 22:49:07 +0000 (18:49 -0400)
commitf4d031742d969c689d38c0756a5026a434ef89b3
tree54c1ef98847dbc809c0bc3cb59f20b882c42e075tree
parentbe4701964ca423017d15e50697461a93587466dbcommit | diff
sets: "insert" operator

new™! support for (insert (X (Set X)) (Set X) :right-associative)
from the finte sets theory prosoal.

e.g., (insert 1 2 3 4 (singleton 5))
src/parser/smt2/smt2.cpp diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
src/theory/sets/kinds diff | blob | history
src/theory/sets/theory_sets_rewriter.cpp diff | blob | history
src/theory/sets/theory_sets_type_rules.h diff | blob | history
test/regress/regress0/sets/Makefile.am diff | blob | history
test/regress/regress0/sets/insert.smt2 [new file with mode: 0644] blob