projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 698f5a0) | patch
Optimizations for datatypes: check for clashes modulo equality. Avoid building model...
authorajreynol <reynolds@larapc05.epfl.ch>
Mon, 28 Apr 2014 15:34:00 +0000 (17:34 +0200)
committerajreynol <reynolds@larapc05.epfl.ch>
Mon, 28 Apr 2014 15:34:00 +0000 (17:34 +0200)
commit9b97c9144875e072da4098f102f8989be26e5cdf
tree2f95fbd431085345784a7b4e0c7c569d3a428db3tree
parent698f5a09b1c0177abfd2eaa2b110de100fd108efcommit | diff
Optimizations for datatypes: check for clashes modulo equality.  Avoid building model at fullModel=false when possible.  Minor cleanup.
src/theory/datatypes/theory_datatypes.cpp diff | blob | history
src/theory/datatypes/theory_datatypes.h diff | blob | history
src/theory/quantifiers/bounded_integers.h diff | blob | history
src/theory/quantifiers/instantiation_engine.h diff | blob | history
src/theory/quantifiers/model_engine.cpp diff | blob | history
src/theory/quantifiers/model_engine.h diff | blob | history
src/theory/quantifiers/quant_conflict_find.h diff | blob | history
src/theory/quantifiers/rewrite_engine.h diff | blob | history
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/quantifiers_engine.h diff | blob | history