projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f5be8f1) | patch
Fixes for handling set universe: restrict upwards rule for universe to memberships...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 19 Apr 2017 21:16:35 +0000 (16:16 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 19 Apr 2017 21:16:53 +0000 (16:16 -0500)
commitebc103db4ac5210585525f1e9abb06b1da3c5cbf
tree5af553e9862993bb96e3e3dc57a6dafcbafe6f27tree
parentf5be8f194bb40327f05ed87272e95722562b2483commit | diff
Fixes for handling set universe: restrict upwards rule for universe to memberships into variable sets, do not variable eliminate sets during ppAssert.
src/theory/sets/theory_sets.cpp diff | blob | history
src/theory/sets/theory_sets.h diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/sets/theory_sets_private.h diff | blob | history
test/regress/regress0/sets/Makefile.am diff | blob | history
test/regress/regress0/sets/nonvar-univ.smt2 [new file with mode: 0644] blob
test/regress/regress0/sets/pre-proc-univ.smt2 [new file with mode: 0644] blob