Age | Commit message (Collapse) | Author |
|
* TNode violation bug fix (thanks to Tim King for discovery & fix)
* change Boolean miplib-trick substitution option into a threshold
* ppAssert() the generated miplib constraints to arithmetic
|
|
|
|
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')
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
* timer statistics now supported (closes bug 488)
* use of --mmap doesn't crash anymore (closes bug 489)
|
|
QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486
(cherry-picked from master c5d1a5d8f898bf22c6bbc98f1d484b07706c035b)
|
|
|
|
QuantifiersEngine::d_lemmas_produced user-level context dependent. this fixes bug 486
|
|
datatypes theory still crashes for datatypes with boolean subfields
(cherry picked from master bcbf52ffbe0416ecf70bdb644017c338c0540793)
|
|
datatypes theory still crashes for datatypes with boolean subfields
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
bracketing
|
|
|
|
fixes bug 484
|
|
|
|
|
|
|
|
|
|
|