projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 13dee9f) | patch
Fix for when variables are (partially) bound in multiple ways, add regression. Improv...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 11 Jan 2017 20:34:18 +0000 (14:34 -0600)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 11 Jan 2017 20:34:18 +0000 (14:34 -0600)
commit97aaf2ffbb542b5c097b49071fd24ae40898eeb0
treec21c86dc32876bc3da0777fe274dd362ebb17039tree
parent13dee9ff9189134158ff21524e7ecc73dcdce971commit | diff
Fix for when variables are (partially) bound in multiple ways, add regression. Improve printing for bound int module. Track when relations are enabled in sets, set incomplete if card+rels are both enabled since model construction is not guaranteed to succeed.
src/theory/quantifiers/bounded_integers.cpp diff | blob | history
src/theory/sets/theory_sets_private.cpp diff | blob | history
src/theory/sets/theory_sets_private.h diff | blob | history
src/theory/sets/theory_sets_rels.cpp diff | blob | history
src/theory/sets/theory_sets_rels.h diff | blob | history
test/regress/regress0/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/ko-bound-set.cvc [new file with mode: 0644] blob