| 2011-07-09 |
Dejan Jovanović | surprize surprize |
commit | commitdiff | tree |
| 2011-07-07 |
Dejan Jovanović | removing duplicate clauses in ite cnf conversion |
commit | commitdiff | tree |
| 2011-07-07 |
Morgan Deters | cudd-building prefs with --with-cudd / --without-cudd |
commit | commitdiff | tree |
| 2011-07-06 |
Dejan Jovanović | Fixing two bugs: |
commit | commitdiff | tree |
| 2011-07-05 |
Dejan Jovanović | missing test case |
commit | commitdiff | tree |
| 2011-07-05 |
Dejan Jovanović | updated preprocessing and rewriting input equalities... |
commit | commitdiff | tree |
| 2011-06-30 |
Morgan Deters | Allow (- x) for unary minus in SMT-LIBv1, in addition... |
commit | commitdiff | tree |
| 2011-06-30 |
Tim King | Changed the defaults for arithPivotThreshold and arithP... |
commit | commitdiff | tree |
| 2011-06-30 |
Tim King | Merging the playground branch upto r1957 into trunk. |
commit | commitdiff | tree |
| 2011-06-30 |
Morgan Deters | only use theory registration if (1) a theory requests... |
commit | commitdiff | tree |
| 2011-06-30 |
Morgan Deters | some things I had laying around in a directory but... |
commit | commitdiff | tree |
| 2011-06-29 |
Tim King | Fixed spelling mistake and documentation for --enable... |
commit | commitdiff | tree |
| 2011-06-18 |
Morgan Deters | Some fixes inspired by Fedora 15: |
commit | commitdiff | tree |
| 2011-06-06 |
Morgan Deters | compilation fix for x86 (from previous commit) |
commit | commitdiff | tree |
| 2011-06-06 |
Morgan Deters | Fix for Mac OS breakage (x86 didn't crash, but probably... |
commit | commitdiff | tree |
| 2011-06-03 |
Andrew Reynolds | fixed various bugs related to ambiguous parametric... |
commit | commitdiff | tree |
| 2011-06-03 |
Morgan Deters | datatypes work |
commit | commitdiff | tree |
| 2011-06-02 |
Morgan Deters | minor fix to build system for system tests |
commit | commitdiff | tree |
| 2011-06-02 |
Andrew Reynolds | added (temporary) support for ensuring that all ambiguo... |
commit | commitdiff | tree |
| 2011-06-01 |
Morgan Deters | minor fix, and better output for type errors |
commit | commitdiff | tree |
| 2011-06-01 |
Morgan Deters | type ascriptions (casts) for parameterized datatypes... |
commit | commitdiff | tree |
| 2011-05-31 |
Tim King | This commit contains the code for allowing arbitrary... |
commit | commitdiff | tree |
| 2011-05-28 |
Morgan Deters | fix unit test linking issue |
commit | commitdiff | tree |
| 2011-05-28 |
Morgan Deters | include subversion information used for each build... |
commit | commitdiff | tree |
| 2011-05-26 |
Morgan Deters | apply arithmetic static learner's miplibtrick in a... |
commit | commitdiff | tree |
| 2011-05-23 |
Morgan Deters | fixes for "make dist" and "make doc", minor cleanups |
commit | commitdiff | tree |
| 2011-05-23 |
Morgan Deters | Merge from arrays2 branch. |
commit | commitdiff | tree |
| 2011-05-14 |
Morgan Deters | fix production-build compiler warning |
commit | commitdiff | tree |
| 2011-05-14 |
Morgan Deters | re-add a removed Datatype constructor that was causing... |
commit | commitdiff | tree |
| 2011-05-14 |
Morgan Deters | reverting node manager change from 1881; also part... |
commit | commitdiff | tree |
| 2011-05-14 |
Morgan Deters | add AscriptionType stuff to support nullary parameteriz... |
commit | commitdiff | tree |
| 2011-05-13 |
Andrew Reynolds | added support for parametric datatypes, updated cvc... |
commit | commitdiff | tree |
| 2011-05-13 |
Morgan Deters | * fix for Mac OS (includes some ThreadLocal stuff copie... |
commit | commitdiff | tree |
| 2011-05-06 |
Tim King | Deleting dead code. |
commit | commitdiff | tree |
| 2011-05-06 |
Andrew Reynolds | added 10 benchmarks to regress/regress0/datatypes from... |
commit | commitdiff | tree |
| 2011-05-06 |
Andrew Reynolds | significant revisions/improvements to code for theory... |
commit | commitdiff | tree |
| 2011-05-05 |
Morgan Deters | Merge from nonclausal-simplification-v2 branch: |
commit | commitdiff | tree |
| 2011-05-05 |
Morgan Deters | luby sequence generator; can use to plot MiniSat's... |
commit | commitdiff | tree |
| 2011-05-04 |
Morgan Deters | Stronger support for zero-performance-penalty output... |
commit | commitdiff | tree |
| 2011-05-03 |
Morgan Deters | output fixes for performance |
commit | commitdiff | tree |
| 2011-05-02 |
Andrew Reynolds | minor updates to exp manager, fixed 32bit vs 64bit... |
commit | commitdiff | tree |
| 2011-05-02 |
Morgan Deters | fix for configure |
commit | commitdiff | tree |
| 2011-05-02 |
Morgan Deters | adding some previously-failing "bug" test cases for... |
commit | commitdiff | tree |
| 2011-05-02 |
Dejan Jovanović | updating bv regressions |
commit | commitdiff | tree |
| 2011-05-02 |
Dejan Jovanović | parser fixes for bug 243 |
commit | commitdiff | tree |
| 2011-05-02 |
Dejan Jovanović | updates for bitvectors |
commit | commitdiff | tree |
| 2011-05-02 |
Morgan Deters | more minor fixes related to last few commits |
commit | commitdiff | tree |
| 2011-05-02 |
Morgan Deters | another small fix |
commit | commitdiff | tree |
| 2011-05-02 |
Morgan Deters | fix broken build; sorry, all! |
commit | commitdiff | tree |
| 2011-05-02 |
Morgan Deters | fix a performance issue from last commit |
commit | commitdiff | tree |
| 2011-05-02 |
Morgan Deters | Minor fixes to various parts of CVC4, including the... |
commit | commitdiff | tree |
| 2011-05-01 |
Morgan Deters | minor fixes, plus experimental readline support in... |
commit | commitdiff | tree |
| 2011-04-29 |
Andrew Reynolds | refactoring to datatypes theory, added working prototyp... |
commit | commitdiff | tree |
| 2011-04-28 |
Andrew Reynolds | more fixes/improvements to datatypes theory and transit... |
commit | commitdiff | tree |
| 2011-04-27 |
Andrew Reynolds | cleaned up some of the hacks in the datatypes theory... |
commit | commitdiff | tree |
| 2011-04-25 |
Morgan Deters | Monday tasks: |
commit | commitdiff | tree |
| 2011-04-25 |
Morgan Deters | small unit test fix; was broken only in non-assertion... |
commit | commitdiff | tree |
| 2011-04-25 |
Morgan Deters | Weekend work. The main points: |
commit | commitdiff | tree |
| 2011-04-23 |
Morgan Deters | fix for parser/tests for ANTLR 3.2 (it was working... |
commit | commitdiff | tree |
| 2011-04-23 |
Morgan Deters | * reviewed BooleanSimplification, added documentation... |
commit | commitdiff | tree |
| 2011-04-23 |
Morgan Deters | make run_regression script robust to DOS newlines :( |
commit | commitdiff | tree |
| 2011-04-22 |
Andrew Reynolds | added fixes for datatype theory solver to account for... |
commit | commitdiff | tree |
| 2011-04-22 |
Morgan Deters | fix to last commit |
commit | commitdiff | tree |
| 2011-04-22 |
Morgan Deters | Fixing SmtEngine::getValue() by adding a NodeManagerSco... |
commit | commitdiff | tree |
| 2011-04-20 |
Morgan Deters | numerous bugfixes |
commit | commitdiff | tree |
| 2011-04-20 |
Morgan Deters | incorrect usage of C++ std::string caused a test to... |
commit | commitdiff | tree |
| 2011-04-20 |
Morgan Deters | Minor mixed-bag commit. Expected performance impact... |
commit | commitdiff | tree |
| 2011-04-20 |
Morgan Deters | Tuesday end-of-day commit. |
commit | commitdiff | tree |
| 2011-04-18 |
Tim King | Removing dead code that came in on commit r1740. |
commit | commitdiff | tree |
| 2011-04-18 |
Morgan Deters | more work on CVC language |
commit | commitdiff | tree |
| 2011-04-18 |
Morgan Deters | mostly CVC presentation language parsing and printing |
commit | commitdiff | tree |
| 2011-04-18 |
Tim King | This commit merges the branch arithmetic/propagation... |
commit | commitdiff | tree |
| 2011-04-18 |
Morgan Deters | Partial merge from datatypes-merge branch: |
commit | commitdiff | tree |
| 2011-04-18 |
Christopher... | Fixing output for EOF token in parser errors |
commit | commitdiff | tree |
| 2011-04-16 |
Morgan Deters | also a fix for a system test related to ParserBuilder |
commit | commitdiff | tree |
| 2011-04-16 |
Morgan Deters | unit test fixes for new NodeManager constructor (relate... |
commit | commitdiff | tree |
| 2011-04-15 |
Morgan Deters | parser/driver fixes for last commit |
commit | commitdiff | tree |
| 2011-04-15 |
Morgan Deters | partial merge from portfolio branch, adding conversions... |
commit | commitdiff | tree |
| 2011-04-14 |
Dejan Jovanović | reverting back the minisat code and adding a simpler... |
commit | commitdiff | tree |
| 2011-04-14 |
Morgan Deters | Three things: |
commit | commitdiff | tree |
| 2011-04-14 |
Dejan Jovanović | fixing an uninitialized literal variable |
commit | commitdiff | tree |
| 2011-04-13 |
Dejan Jovanović | adding support for unit conflicts in minisat... |
commit | commitdiff | tree |
| 2011-04-13 |
Morgan Deters | fix compiler warning in non-replay builds |
commit | commitdiff | tree |
| 2011-04-13 |
Morgan Deters | cache the LET rewriting (and defined-function expansion... |
commit | commitdiff | tree |
| 2011-04-13 |
Morgan Deters | add disequality token ("/=") and rules to CVC parser |
commit | commitdiff | tree |
| 2011-04-12 |
Morgan Deters | another small fix to "make dist" that can lead to a... |
commit | commitdiff | tree |
| 2011-04-11 |
Clark Barrett | Transitive closure module is working |
commit | commitdiff | tree |
| 2011-04-11 |
Morgan Deters | fix "make dist" issues in makefiles |
commit | commitdiff | tree |
| 2011-04-10 |
Morgan Deters | merge from replay branch |
commit | commitdiff | tree |
| 2011-04-10 |
Morgan Deters | Add -lprofiler when --with-google-perftools is offered... |
commit | commitdiff | tree |
| 2011-04-09 |
Dejan Jovanović | changing the sat solver to assert propagated literals... |
commit | commitdiff | tree |
| 2011-04-08 |
Clark Barrett | Added util class |
commit | commitdiff | tree |
| 2011-04-07 |
Tim King | Made Valuation::getValue() and Valuation::getSatValue... |
commit | commitdiff | tree |
| 2011-04-05 |
Morgan Deters | Memory fix for congruence closure; affects many UF... |
commit | commitdiff | tree |
| 2011-04-05 |
Tim King | Added options for setting the random decision frequency... |
commit | commitdiff | tree |
| 2011-04-05 |
Morgan Deters | Minor adjustments to the Registrar commit in 1644,... |
commit | commitdiff | tree |
| 2011-04-04 |
Tim King | Merging the satliteral-before-prereg branch into trunk... |
commit | commitdiff | tree |
| 2011-04-04 |
Tim King | Reverts previous commit r1636. |
commit | commitdiff | tree |
| 2011-04-04 |
Morgan Deters | Add documentation to Node and TNode (closes bug #201). |
commit | commitdiff | tree |
| 2011-04-02 |
Tim King | Delayed the addition of unate propagation lemmas until... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog