projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8bb55a2) | patch
Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cbqi for...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 15 Jun 2017 15:31:58 +0000 (10:31 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 15 Jun 2017 15:31:58 +0000 (10:31 -0500)
commit3344979103bcec622276fca7c2a21cc0945f6c56
tree8cdcd2cec0db34d70a2bbdb0443bbe3d250995cftree
parent8bb55a22b7c0f20305274f8609b9e8404e4bb41ccommit | diff
Ensure uninterpreted constants do not escape datatypes, fixes bug 823. Fix cbqi for datatypes with uninterpreted sort subfields. Simplify fmc model construction.
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/quantifiers/first_order_model.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h diff | blob | history