Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-02-16 | refactoring justification_heuristic code | Kshitij Bansal | |
2013-02-16 | rm decision jh GiveUp related code | Kshitij Bansal | |
2013-02-15 | Merge branch '1.0.x' | Kshitij Bansal | |
2013-02-15 | prvs commit: lower warning to notice | Kshitij Bansal | |
Signed-off-by: Kshitij Bansal <kshitij@cs.nyu.edu> | |||
2013-02-15 | Merge branch '1.0.x' | Kshitij Bansal | |
2013-02-15 | make incremental+portfolio experimental | Kshitij Bansal | |
2013-02-15 | Merge pull request #5 from kbansal/1.0.x | Kshitij Bansal | |
make incremental+portfolio experimental | |||
2013-02-15 | make incremental+portfolio experimental | Kshitij Bansal | |
2013-02-15 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-15 | Fix builds/ links to survive configuring twice with different prefixes | Morgan Deters | |
2013-02-15 | Fix ECHO command in CVC language parser to not output quotation marks | Morgan Deters | |
2013-02-15 | Merge branch '1.0.x' | Tim King | |
2013-02-15 | repairs a bug in rewriterule engine: constructor cannot be used as a pattern | Tianyi Liang | |
(cherry picked from commit c33a1abc78bcd51f3f95562b117498caf252cafc) Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2013-02-14 | Merge pull request #4 from tiliang/master | Dejan Jovanović | |
a bugfix in rewriting rules | |||
2013-02-14 | Removing BVDebug and replacing with Debug. | Tim King | |
2013-02-13 | repairs a bug in rewriterule engine: constructor cannot be used as a pattern | Tianyi Liang | |
2013-02-12 | Fix a preprocessing performance issue. | Morgan Deters | |
2013-02-08 | Fix user-values in SMT-LIB v1.2 | Morgan Deters | |
2013-02-07 | Merge branch '1.0.x' | Morgan Deters | |
Conflicts: src/theory/quantifiers/theory_quantifiers.cpp | |||
2013-02-07 | Only put quantifier assertions in model equality engine if fullModel==true | Morgan Deters | |
2013-02-07 | Significant work on bug #491 (not yet closed). | Morgan Deters | |
2013-02-07 | More complete fix for bug 484 (includes fixes for records and tuples). | Morgan Deters | |
2013-02-07 | Fix error in tuple type-checking. | Morgan Deters | |
2013-02-07 | Make --default-dag-thresh apply to stringstreams | Morgan Deters | |
2013-02-07 | Do not install the "private-library" header | Morgan Deters | |
2013-02-06 | make datatypes enumerator behavior clearer (no exceptions in normal operation) | Morgan Deters | |
2013-02-06 | make datatypes enumerator behavior clearer (no exceptions in normal operation) | Morgan Deters | |
2013-02-05 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-05 | Fix a compiler warning in NodeBuilder | Morgan Deters | |
2013-02-05 | Merge remote-tracking branch 'origin/1.0.x' | Kshitij Bansal | |
2013-02-05 | Merge pull request #3 from kbansal/1.0.x | Kshitij Bansal | |
decision/ : save d_prvsIndex in JH | |||
2013-02-05 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-05 | remove now-unnecessary wrappers from Type interface | Morgan Deters | |
2013-02-05 | Fix to miplib trick to make it less "cautious" and apply in more cases | Morgan Deters | |
2013-02-05 | decision/ : save d_prvsIndex in JH | Kshitij Bansal | |
2013-02-05 | dos2unix conversion for a number of files; this avoids spurious conflicts ↵ | Morgan Deters | |
when merging to master | |||
2013-02-05 | More improvements for E-matching | Andrew Reynolds | |
2013-02-04 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-04 | Fix NodeBuilder bug which could attempt to allocate beyond hard limit | Morgan Deters | |
2013-02-04 | driver::totalTime statistic is now reported correctly on crashes, too | Morgan Deters | |
2013-02-04 | fixed files with DOS newlines; fixed contrib/ scripts to use git | Morgan Deters | |
2013-02-04 | Some fixes for the miplib preprocessing pass. | Morgan Deters | |
* 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 | |||
2013-02-04 | Printing commands as they're executed now requires verbosity 3+ | Morgan Deters | |
2013-02-04 | Merge branch '1.0.x' | Morgan Deters | |
2013-02-04 | Model no longer adds subterms of quantifiers to equality engine, this fixed ↵ | Morgan Deters | |
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> | |||
2013-02-04 | Model no longer adds subterms of quantifiers to equality engine, this fixed ↵ | Andrew Reynolds | |
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. | |||
2013-02-03 | Some cleanup of miplib regressions and options | Morgan Deters | |
2013-02-03 | Merge from mdeters/miplib branch (commit ↵ | Morgan Deters | |
'ce7c485182902ae43871057185095f71f74a8a58') | |||
2013-02-03 | new option for doing top-level miplib substitutions (or not) | Morgan Deters | |
2013-02-03 | extended miplib trick to 6 vars, should work on pp miplib examples now | Morgan Deters | |