Age | Commit message (Collapse) | Author |
|
|
|
|
|
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
|
|
|
|
|
|
|
|
when merging to master
|
|
|
|
|
|
|
|
|
|
|
|
* 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.
(cherry picked from *part* of commit e54c0f73712b25f1d6d49a3817c923eea077da81)
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
|
|
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')
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|