Age | Commit message (Collapse) | Author |
|
|
|
* one that Tim found in model generation for records containing Booleans
* another that the fuzzer found in quantifiers + check-models
Test cases enabled/added for both.
|
|
|
|
* Comment cleanup
* Spelling fixes
* Fix warnings
* Documentation updates
* References in docs to cryptominisat removed
* Unneeded scope resolutions removed
* Old, unused regression removed
|
|
|
|
previously-failing testcase.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
inequalities
|
|
|
|
|
|
|
|
|
|
|
|
|
|
incremental); currently disabled though
|
|
|
|
|
|
|
|
and src
|
|
|
|
|
|
* update some copyrights for 2013
* cleaned up some comments/ifdefs, indentation
* some spelling corrections
* add some missing makefiles
|
|
Conflicts:
src/theory/quantifiers/theory_quantifiers.cpp
|
|
|
|
|
|
|
|
|
|
|
|
bug 492 and resolves previous issue for bug 486.\n Multiple improvements for E-matching: do not choose multi-triggers if single triggers exist, only create multi-triggers that contain all variables, consider multiple terms per equivalence class but only add one instantiation per round per (trigger,term) pair.\nImprovements for strong solver: make use of sort inference information when choosing splits, check for cliques eagerly when disequalities are asserted.
|
|
|
|
'ce7c485182902ae43871057185095f71f74a8a58')
|
|
|
|
|
|
|
|
getValue/collectModelInfo for quantifiers more.
|
|
(cherry-picked from master 23b4fd82d1ed326cd57e9bc57ef9fab98b0b1c87)
|
|
|
|
|
|
|
|
|
|
bracketing
|
|
|