Age | Commit message (Collapse) | Author |
|
Conflicts:
src/smt/smt_engine.cpp
|
|
|
|
|
|
(Cherry-picked from commit c71ec27 in master.)
|
|
|
|
|
|
|
|
|
|
datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts
|
|
|
|
|
|
|
|
|
|
|
|
decision/ code refactoring
|
|
|
|
other minor: cleanup some remaning fragments of GiveUpException(),
hopefully all is gone now.
|
|
|
|
|
|
|
|
* update some copyrights for 2013
* cleaned up some comments/ifdefs, indentation
* some spelling corrections
* add some missing makefiles
|
|
|
|
|
|
|
|
|
|
Signed-off-by: Kshitij Bansal <kshitij@cs.nyu.edu>
|
|
|
|
|
|
|
|
|
|
|
|
(cherry picked from commit c33a1abc78bcd51f3f95562b117498caf252cafc)
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
|
|
|
|
|
|
|
|
|
Conflicts:
src/theory/quantifiers/theory_quantifiers.cpp
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
decision/ : save d_prvsIndex in JH
|
|
|