2014-11-13 |
Clark Barrett | Minor changes to AUTHORS and COPYING
|
commit | commitdiff | tree |
2014-11-08 |
Clark Barrett | Fixed bug in model builder with subtypes
|
commit | commitdiff | tree |
2014-11-02 |
Clark Barrett | Added cache to getModelValue
|
commit | commitdiff | tree |
2014-10-30 |
Clark Barrett | Be more lazy about generating array lemmas
|
commit | commitdiff | tree |
2014-10-30 |
Clark Barrett | Added new, much faster, care graph computation for...
|
commit | commitdiff | tree |
2014-10-21 |
Clark Barrett | Fixed bug 590, added regression test
|
commit | commitdiff | tree |
2014-10-02 |
Clark Barrett | Added internal support for constant arrays.
|
commit | commitdiff | tree |
2014-10-02 |
Clark Barrett | Added option for developer use only
|
commit | commitdiff | tree |
2014-10-02 |
Clark Barrett | More model-based combination for arrays
|
commit | commitdiff | tree |
2014-10-02 |
Clark Barrett | Better getEqualityStatus for arrays, smarter combination...
|
commit | commitdiff | tree |
2014-06-27 |
Clark Barrett | Fix for bug543
|
commit | commitdiff | tree |
2014-06-27 |
Clark Barrett | Updated run script for QF_ABV
|
commit | commitdiff | tree |
2014-06-13 |
Clark Barrett | Update for QF_AUFLIA strategy
|
commit | commitdiff | tree |
2014-06-12 |
Clark Barrett | Modified run script for QF_AX
|
commit | commitdiff | tree |
2014-06-12 |
Clark Barrett | Modified run script for QF_LRA
|
commit | commitdiff | tree |
2014-05-26 |
Clark Barrett | Fixing Tim's subtype/solving bug for arrays
|
commit | commitdiff | tree |
2013-11-25 |
Clark Barrett | Array collectModelInfo fix for Andy
|
commit | commitdiff | tree |
2013-10-28 |
Clark Barrett | Turn off model-based arrays (causing crashes in portfolio)
|
commit | commitdiff | tree |
2013-10-24 |
Clark Barrett | Fix for bug515
|
commit | commitdiff | tree |
2013-09-24 |
Clark Barrett | Reduce compiler dependencies on substitutions.h,
|
commit | commitdiff | tree |
2013-09-24 |
Clark Barrett | Better fix for bug 528
|
commit | commitdiff | tree |
2013-09-23 |
Clark Barrett | Cleaner version of bug-fix for 528, also moved substitutions...
|
commit | commitdiff | tree |
2013-09-19 |
Clark Barrett | Fix for bug 528
|
commit | commitdiff | tree |
2013-05-08 |
Clark Barrett | Fixed assertion bug
|
commit | commitdiff | tree |
2013-05-06 |
Clark Barrett | Some bug fixes for mb arrays
|
commit | commitdiff | tree |
2013-04-11 |
Clark Barrett | Improved speed of no redundant lemma assertion by using...
|
commit | commitdiff | tree |
2013-04-11 |
Clark Barrett | Fixes for getModelVal in bv theory
|
commit | commitdiff | tree |
2013-04-11 |
Clark Barrett | Added check for infinite lemma loop
|
commit | commitdiff | tree |
2013-04-02 |
Clark Barrett | Fix regression error by turning off model-based solver...
|
commit | commitdiff | tree |
2013-04-02 |
Clark Barrett | Turning on model based array solver for QF_AX
|
commit | commitdiff | tree |
2013-04-02 |
Clark Barrett | Made eager lemmas an option, enabled for QF_AX
|
commit | commitdiff | tree |
2013-04-02 |
Clark Barrett | Disabling eager array index splitting for QF_AX
|
commit | commitdiff | tree |
2013-03-31 |
Clark Barrett | Disabling eager array index splitting for QF_AUFLIA
|
commit | commitdiff | tree |
2013-03-28 |
Clark Barrett | Fixed a warning, made eager-index default to true ...
|
commit | commitdiff | tree |
2013-03-28 |
Clark Barrett | Fixed bug in arrays
|
commit | commitdiff | tree |
2013-03-28 |
Clark Barrett | Added assertion
|
commit | commitdiff | tree |
2013-03-28 |
Clark Barrett | Updates to model-based array solver
|
commit | commitdiff | tree |
2013-03-28 |
Clark Barrett | New model-based array procedure
|
commit | commitdiff | tree |
2013-03-14 |
Clark Barrett | Added a rewrite for iff:
|
commit | commitdiff | tree |
2013-03-06 |
Clark Barrett | Best heuristics for handling decision requests from...
|
commit | commitdiff | tree |
2012-12-06 |
Clark Barrett | Fix for fuzzer-found model bug
|
commit | commitdiff | tree |
2012-12-03 |
Clark Barrett | Fix for fuzzer-found model bug
|
commit | commitdiff | tree |
2012-12-01 |
Clark Barrett | Throw a logic exception if user makes an assertion...
|
commit | commitdiff | tree |
2012-11-30 |
Clark Barrett | Fix assertion in smt_engine's getValue
|
commit | commitdiff | tree |
2012-11-29 |
Clark Barrett | Fix for nasty corner case found by fuzzer...
|
commit | commitdiff | tree |
2012-11-29 |
Clark Barrett | Fixing function models with Boolean terms. Also, LAMBDA...
|
commit | commitdiff | tree |
2012-11-28 |
Clark Barrett | Fix for getValue. Now it can handle lambda applications
|
commit | commitdiff | tree |
2012-11-17 |
Clark Barrett | Fixed last currently known bug in array models
|
commit | commitdiff | tree |
2012-11-16 |
Clark Barrett | Fix for bug451
|
commit | commitdiff | tree |
2012-11-15 |
Clark Barrett | More fixes to model generation, with previously failing...
|
commit | commitdiff | tree |
2012-11-15 |
Clark Barrett | fuzz15 should have been fuzz14
|
commit | commitdiff | tree |
2012-11-15 |
Clark Barrett | Fixed another AUFBV model bug. BV equality subtheory...
|
commit | commitdiff | tree |
2012-11-14 |
Clark Barrett | bug fixes to models, array rewriter with previously...
|
commit | commitdiff | tree |
2012-11-13 |
Clark Barrett | More bugfixes for models
|
commit | commitdiff | tree |
2012-11-13 |
Clark Barrett | Relaxing too-strict assertion
|
commit | commitdiff | tree |
2012-11-13 |
Clark Barrett | Fixed an array rewriting bug found by fuzzer
|
commit | commitdiff | tree |
2012-11-13 |
Clark Barrett | Testcases for fixed bugs
|
commit | commitdiff | tree |
2012-11-13 |
Clark Barrett | Fixed bug in array constant normalization found by...
|
commit | commitdiff | tree |
2012-11-10 |
Clark Barrett | Fixed missing \ in uflra/Makefile.ma
|
commit | commitdiff | tree |
2012-11-10 |
Clark Barrett | Finally tracked down problems in regressions and fuzz...
|
commit | commitdiff | tree |
2012-11-09 |
Clark Barrett | Fix for another model assertion failure
|
commit | commitdiff | tree |
2012-11-08 |
Clark Barrett | Fixed two small bugs in model generation
|
commit | commitdiff | tree |
2012-11-08 |
Clark Barrett | Added getBaseType - Morgan please check
|
commit | commitdiff | tree |
2012-10-29 |
Clark Barrett | Tweak to options configuration for turning off minisat...
|
commit | commitdiff | tree |
2012-10-29 |
Clark Barrett | Disable minisat elimination when models are on
|
commit | commitdiff | tree |
2012-10-29 |
Clark Barrett | Disable some array optimizations when models are on
|
commit | commitdiff | tree |
2012-10-29 |
Clark Barrett | auflia directory missing from regression summary -...
|
commit | commitdiff | tree |
2012-10-26 |
Clark Barrett | Fixed a failing datatype regression with check-models
|
commit | commitdiff | tree |
2012-10-26 |
Clark Barrett | More bug fixes and more checks for models
|
commit | commitdiff | tree |
2012-10-23 |
Clark Barrett | More debugging info, small changes to model builder
|
commit | commitdiff | tree |
2012-10-23 |
Clark Barrett | Added reads that were missing in collectModelInfo
|
commit | commitdiff | tree |
2012-10-12 |
Clark Barrett | Added assertions and tracing code for collectModelInfo...
|
commit | commitdiff | tree |
2012-10-12 |
Clark Barrett | Latest changes to model code
|
commit | commitdiff | tree |
2012-10-09 |
Clark Barrett | More fixes to model code
|
commit | commitdiff | tree |
2012-10-08 |
Clark Barrett | Fixed problem in assertEqualityEngine: predicates that...
|
commit | commitdiff | tree |
2012-10-04 |
Clark Barrett | Implemented array type enumerator, more fixes for models
|
commit | commitdiff | tree |
2012-10-03 |
Clark Barrett | New model code, mostly workin
|
commit | commitdiff | tree |
2012-08-26 |
Clark Barrett | Array constants finished and working. Unit tests for...
|
commit | commitdiff | tree |
2012-08-23 |
Clark Barrett | Array constant coding done except for the attributes...
|
commit | commitdiff | tree |
2012-08-22 |
Clark Barrett | More progress on array constants.
|
commit | commitdiff | tree |
2012-08-19 |
Clark Barrett | 1. Fix for inst_match.cpp to allow compilation on fedora
|
commit | commitdiff | tree |
2012-06-28 |
Clark Barrett | Fixed bug in bv rewriter that caused wrong answer in...
|
commit | commitdiff | tree |
2012-06-18 |
Clark Barrett | Reverting buggy rewriter code
|
commit | commitdiff | tree |
2012-06-18 |
Clark Barrett | Fixed bug in rewriter
|
commit | commitdiff | tree |
2012-06-18 |
Clark Barrett | Fix for slow array rewrite and minor bug fix in arrays...
|
commit | commitdiff | tree |
2012-06-18 |
Clark Barrett | small bug fix and performance fix in ite simplifier
|
commit | commitdiff | tree |
2012-06-17 |
Clark Barrett | Removed assertion that can fail
|
commit | commitdiff | tree |
2012-06-17 |
Clark Barrett | Fix array bug causing incorrect answers
|
commit | commitdiff | tree |
2012-06-15 |
Clark Barrett | Reverting rewrite rule to working version
|
commit | commitdiff | tree |
2012-06-15 |
Clark Barrett | Fixes some assertion failures
|
commit | commitdiff | tree |
2012-06-15 |
Clark Barrett | Fix for incompleteness bug with decision engine: repeated...
|
commit | commitdiff | tree |
2012-06-14 |
Clark Barrett | New substitutions implementation - fixes performance...
|
commit | commitdiff | tree |
2012-06-14 |
Clark Barrett | Removed an assertion, unneeded header file
|
commit | commitdiff | tree |
2012-06-13 |
Clark Barrett | Fixed failing assertion when EqualityEngine is in conflict
|
commit | commitdiff | tree |
2012-06-13 |
Clark Barrett | Fixed definition of bvsmod
|
commit | commitdiff | tree |
2012-06-13 |
Clark Barrett | Fixes more problems in bv rewrites
|
commit | commitdiff | tree |
2012-06-13 |
Clark Barrett | Fixes lots of problems in bv rewrite rules and adds...
|
commit | commitdiff | tree |
2012-06-12 |
Clark Barrett | Moved some things around in the preprocessor. Now...
|
commit | commitdiff | tree |
2012-06-12 |
Clark Barrett | Fixed fuzzing bug
|
commit | commitdiff | tree |
2012-06-12 |
Clark Barrett | Changed bitvector theory rewriter so that equalities...
|
commit | commitdiff | tree |
next |