| 2012-11-13 |
Clark Barrett | Fixed bug in array constant normalization found by... |
tree | commitdiff |
| 2012-11-10 |
Clark Barrett | Fixed missing \ in uflra/Makefile.ma |
tree | commitdiff |
| 2012-11-09 |
Clark Barrett | Fix for another model assertion failure |
tree | commitdiff |
| 2012-11-08 |
Clark Barrett | Fixed two small bugs in model generation |
tree | commitdiff |
| 2012-10-29 |
Clark Barrett | Disable some array optimizations when models are on |
tree | commitdiff |
| 2012-10-23 |
Clark Barrett | Added reads that were missing in collectModelInfo |
tree | commitdiff |
| 2012-10-16 |
Andrew Reynolds | more cleanup of quantifiers code |
tree | commitdiff |
| 2012-10-11 |
Morgan Deters | Standardizing copyright notice. Touches **ALL** source... |
tree | commitdiff |
| 2012-10-05 |
Morgan Deters | Bug-related: |
tree | commitdiff |
| 2012-10-04 |
Clark Barrett | Implemented array type enumerator, more fixes for models |
tree | commitdiff |
| 2012-10-03 |
Clark Barrett | New model code, mostly workin |
tree | commitdiff |
| 2012-09-28 |
Morgan Deters | rename Assert.h/Assert.cpp to cvc4_assert.h/cvc4_assert... |
tree | commitdiff |
| 2012-09-22 |
Morgan Deters | Separate public-facing and internal-facing interfaces... |
tree | commitdiff |
| 2012-09-19 |
Morgan Deters | General subscriber infrastructure for NodeManager,... |
tree | commitdiff |
| 2012-08-31 |
Andrew Reynolds | merge from fmf-devel branch. more updates to models... |
tree | commitdiff |
| 2012-08-28 |
Morgan Deters | Improved compatibility layer, now supports quantifiers... |
tree | commitdiff |
| 2012-08-26 |
Clark Barrett | Array constants finished and working. Unit tests for... |
tree | commitdiff |
| 2012-08-24 |
Morgan Deters | * disallow internal uses of mkVar() (you have to mkSkol... |
tree | commitdiff |
| 2012-08-24 |
Morgan Deters | fix warning in arrays rewriter |
tree | commitdiff |
| 2012-08-23 |
Morgan Deters | attribute stuff for Clark's array constants |
tree | commitdiff |
| 2012-08-23 |
Clark Barrett | Array constant coding done except for the attributes... |
tree | commitdiff |
| 2012-08-22 |
Clark Barrett | More progress on array constants. |
tree | commitdiff |
| 2012-08-19 |
Clark Barrett | 1. Fix for inst_match.cpp to allow compilation on fedora |
tree | commitdiff |
| 2012-08-16 |
Morgan Deters | Replace propagateAsDecision() with Theory::getNextDecis... |
tree | commitdiff |
| 2012-08-07 |
Morgan Deters | Some items from the CVC4 public interface review: |
tree | commitdiff |
| 2012-08-03 |
Morgan Deters | the array-store "construle" for isConst |
tree | commitdiff |
| 2012-08-03 |
Morgan Deters | ArrayStoreAll infrastructure |
tree | commitdiff |
| 2012-08-03 |
Morgan Deters | fix uses of getMetaKind() from outside the expr package... |
tree | commitdiff |
| 2012-08-01 |
Morgan Deters | add isFinished() to type enumerators (so we don't rely... |
tree | commitdiff |
| 2012-08-01 |
Morgan Deters | some fixes for Mac OS |
tree | commitdiff |
| 2012-07-31 |
Morgan Deters | Moving some instantiation-related stuff from src/theory... |
tree | commitdiff |
| 2012-07-31 |
Morgan Deters | Options merge. This commit: |
tree | commitdiff |
| 2012-07-27 |
Morgan Deters | Minor cleanup after today's commits: |
tree | commitdiff |
| 2012-07-27 |
Andrew Reynolds | merging fmf-devel branch, includes refactored datatype... |
tree | commitdiff |
| 2012-07-27 |
François Bobot | Merge quantifiers2-trunk: |
tree | commitdiff |
| 2012-07-14 |
Morgan Deters | Type enumerator infrastructure and uninterpreted consta... |
tree | commitdiff |
| 2012-07-12 |
Andrew Reynolds | merged fmf-devel branch, includes support for SMT2... |
tree | commitdiff |
| 2012-06-18 |
Clark Barrett | Reverting buggy rewriter code |
tree | commitdiff |
| 2012-06-18 |
Clark Barrett | Fixed bug in rewriter |
tree | commitdiff |
| 2012-06-18 |
Clark Barrett | Fix for slow array rewrite and minor bug fix in arrays... |
tree | commitdiff |
| 2012-06-17 |
Clark Barrett | Fix array bug causing incorrect answers |
tree | commitdiff |
| 2012-06-16 |
Dejan Jovanović | changing theoryOf in shared mode with arrays to move... |
tree | commitdiff |
| 2012-06-14 |
Dejan Jovanović | * removing rewriteEquality from the rewriter |
tree | commitdiff |
| 2012-06-13 |
Clark Barrett | Fixed failing assertion when EqualityEngine is in conflict |
tree | commitdiff |
| 2012-06-12 |
Dejan Jovanović | bufixes and the bugs |
tree | commitdiff |
| 2012-06-12 |
Clark Barrett | Fixed failing assertion in arrays for bug 347 |
tree | commitdiff |
| 2012-06-11 |
Morgan Deters | Merge from quantifiers2-trunkmerge branch. |
tree | commitdiff |
| 2012-06-11 |
Clark Barrett | Fix for array bug with decision heuristic |
tree | commitdiff |
| 2012-06-10 |
Dejan Jovanović | fixes for bug347 |
tree | commitdiff |
| 2012-06-07 |
Dejan Jovanović | fixing the wrong results. arrays equality adaptor had... |
tree | commitdiff |
| 2012-06-07 |
Dejan Jovanović | fixing some bugs in propagation of disequalities |
tree | commitdiff |
| 2012-06-06 |
Dejan Jovanović | Changes to the combination mechanism, lots of details... |
tree | commitdiff |
| 2012-05-30 |
Clark Barrett | Fixed problem with array queue growing too large |
tree | commitdiff |
| 2012-05-28 |
Clark Barrett | Added some BV rewrites, fixed bugs in array theory... |
tree | commitdiff |
| 2012-05-27 |
Dejan Jovanović | Committing the work on equality engine, I need to see... |
tree | commitdiff |
| 2012-05-25 |
Clark Barrett | Checking in fix for bug 340 - somehow didn't get checke... |
tree | commitdiff |
| 2012-05-21 |
Dejan Jovanović | Updating equality manager to handle tagged trigger... |
tree | commitdiff |
| 2012-05-19 |
Tim King | - The array type rules were fixed to use isSubtypeOf. |
tree | commitdiff |
| 2012-05-14 |
Clark Barrett | Fixed assertion failures in array theory |
tree | commitdiff |
| 2012-05-14 |
Dejan Jovanović | fixing up preregistration again |
tree | commitdiff |
| 2012-05-11 |
Clark Barrett | Added some ITE rewrites, |
tree | commitdiff |
| 2012-05-09 |
Dejan Jovanović | * simplifying equality engine interface |
tree | commitdiff |
| 2012-05-03 |
Dejan Jovanović | Some cleanup starting off from trying to understand... |
tree | commitdiff |
| 2012-04-27 |
Clark Barrett | Fixed warning in decision_engine.h, minor tweak to... |
tree | commitdiff |
| 2012-04-20 |
Clark Barrett | Updates to array theory - much more lazy about introduc... |
tree | commitdiff |
| 2012-04-14 |
Clark Barrett | Fixed bug in sharing with arrays of different types |
tree | commitdiff |
| 2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
tree | commitdiff |
| 2012-04-02 |
Tim King | - Merged in the branch cdlist-cleanup. |
tree | commitdiff |
| 2012-03-09 |
Morgan Deters | Some work on the dump infrastructure to support portfol... |
tree | commitdiff |
| 2012-03-02 |
Dejan Jovanović | CDMap -> CDHashMap |
tree | commitdiff |
| 2012-02-25 |
Dejan Jovanović | ppAsert -> ppAssert |
tree | commitdiff |
| 2012-02-24 |
Dejan Jovanović | Theory interface changes: |
tree | commitdiff |
| 2012-02-20 |
Morgan Deters | portfolio merge |
tree | commitdiff |
| 2011-11-01 |
Morgan Deters | Improvements to header installation on user machines... |
tree | commitdiff |
| 2011-10-17 |
Dejan Jovanović | Sharing work |
tree | commitdiff |
| 2011-10-05 |
Morgan Deters | remove some debugging code that slowed down last night... |
tree | commitdiff |
| 2011-09-29 |
Morgan Deters | Some base infrastructure for user push/pop; a few bugfi... |
tree | commitdiff |
| 2011-09-15 |
Dejan Jovanović | additional stuff for sharing, |
tree | commitdiff |
| 2011-09-02 |
Morgan Deters | Merge from my post-smtcomp branch. Includes: |
tree | commitdiff |
| 2011-07-12 |
Morgan Deters | fix bug 272, array unsoundness, and some array cleanup |
tree | commitdiff |
| 2011-07-11 |
Morgan Deters | fixing out of place typename (error on g++ 4.4.3-4ubuntu5) |
tree | commitdiff |
| 2011-07-11 |
Clark Barrett | Adding static_fact_manager |
tree | commitdiff |
| 2011-07-11 |
Clark Barrett | Clark's work on array theory - can now solve all QF_AX... |
tree | commitdiff |
| 2011-05-23 |
Morgan Deters | Merge from arrays2 branch. |
tree | commitdiff |
| 2011-04-25 |
Morgan Deters | Monday tasks: |
tree | commitdiff |
| 2011-04-25 |
Morgan Deters | Weekend work. The main points: |
tree | commitdiff |
| 2011-04-20 |
Morgan Deters | Minor mixed-bag commit. Expected performance impact... |
tree | commitdiff |
| 2011-03-25 |
Morgan Deters | This is a merge from the "theoryfixes+cdattrhash" branc... |
tree | commitdiff |
| 2011-02-26 |
Morgan Deters | Commit to fix bug 241 (improper "using namespace std... |
tree | commitdiff |
| 2011-02-26 |
Morgan Deters | Merge from theory-break-dependences branch to break... |
tree | commitdiff |
| 2011-01-05 |
Dejan Jovanović | Commit for the theory engine and rewriter changes.... |
tree | commitdiff |
| 2010-11-16 |
Tim King | Added Theory::presolve(). |
tree | commitdiff |
| 2010-10-09 |
Morgan Deters | Model generation for arith, boolean, and uf theories via |
tree | commitdiff |
| 2010-10-05 |
Morgan Deters | parser and core support for SMT-LIBv2 commands get... |
tree | commitdiff |
| 2010-10-04 |
Morgan Deters | remove/shuffle some #include dependencies; fix some... |
tree | commitdiff |
| 2010-10-03 |
Morgan Deters | file header documentation regenerated with contributors... |
tree | commitdiff |
| 2010-07-27 |
Christopher L. Conway | Adding optional 'check' parameter to getType() methods |
tree | commitdiff |
| 2010-07-07 |
Clark Barrett | Shared term manager tested and working |
tree | commitdiff |
| 2010-07-07 |
Clark Barrett | Added shared term manager. Basic mechanism for identif... |
tree | commitdiff |
| 2010-07-04 |
Morgan Deters | With "-d extra-checking", rewrites are now checked... |
tree | commitdiff |
| next |
projects / cvc5.git / history