| 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 |
| 2011-04-02 |
Morgan Deters | with --with-google-perftools, don't just take it on... |
commit | commitdiff | tree |
| 2011-04-02 |
Morgan Deters | minor fixes |
commit | commitdiff | tree |
| 2011-04-01 |
Morgan Deters | minor bugfixes (fixes broken dynamic-library build... |
commit | commitdiff | tree |
| 2011-04-01 |
Morgan Deters | documentation fix |
commit | commitdiff | tree |
| 2011-04-01 |
Morgan Deters | This commit is a merge from the "betterstats" branch... |
commit | commitdiff | tree |
| 2011-03-31 |
Tim King | Fixes to Valuation. |
commit | commitdiff | tree |
| 2011-03-30 |
Morgan Deters | improve recent low-coverage complaints |
commit | commitdiff | tree |
| 2011-03-30 |
Dejan Jovanović | adding CVC4:: qualifier to the #define for debugging... |
commit | commitdiff | tree |
| 2011-03-30 |
Tim King | Moved the constructor for Options out of the header... |
commit | commitdiff | tree |
| 2011-03-30 |
Tim King | Added the command line flag --rewrite-arithmetic-equali... |
commit | commitdiff | tree |
| 2011-03-30 |
Morgan Deters | Add Valuation::getSatValue() so that theories can acces... |
commit | commitdiff | tree |
| 2011-03-30 |
Tim King | Merged the branch sparse-tableau into trunk. |
commit | commitdiff | tree |
| 2011-03-27 |
Morgan Deters | fixes to attribute-internals warnings on 64-bit; also... |
commit | commitdiff | tree |
| 2011-03-26 |
Dejan Jovanović | fix for bug 253, was propagating an asserted literal |
commit | commitdiff | tree |
| 2011-03-26 |
Morgan Deters | fix typo |
commit | commitdiff | tree |
| 2011-03-25 |
Morgan Deters | This is a merge from the "theoryfixes+cdattrhash" branc... |
commit | commitdiff | tree |
| 2011-03-25 |
Morgan Deters | Fix for a bug Andrew Reynolds found for iterators that... |
commit | commitdiff | tree |
| 2011-03-22 |
Tim King | Merges the small changes on the queue-period branch... |
commit | commitdiff | tree |
| 2011-03-22 |
Dejan Jovanović | updating debug output usage to eliviate impact of bug 252 |
commit | commitdiff | tree |
| 2011-03-21 |
Dejan Jovanović | more bugfixes, some basic propagation, and testcases... |
commit | commitdiff | tree |
| 2011-03-21 |
Dejan Jovanović | fixing a bug in the BV rewrite, off by one error when... |
commit | commitdiff | tree |
| 2011-03-20 |
Dejan Jovanović | again a typo |
commit | commitdiff | tree |
| 2011-03-20 |
Dejan Jovanović | more bugfixes for bitvectors |
commit | commitdiff | tree |
| 2011-03-20 |
Dejan Jovanović | fixing the failure from last nigth, due to using a... |
commit | commitdiff | tree |
| 2011-03-20 |
Dejan Jovanović | missed one case |
commit | commitdiff | tree |
| 2011-03-20 |
Dejan Jovanović | commit for the version of bitvectors that passes all... |
commit | commitdiff | tree |
| 2011-03-19 |
Tim King | Merges the pqueue-set branch into trunk. During VarOrd... |
commit | commitdiff | tree |
| 2011-03-18 |
Tim King | - The learned clauses from the miplib trick were being... |
commit | commitdiff | tree |
| 2011-03-17 |
Tim King | Switched SimplexDecisionProcedure::d_delayedLemmas... |
commit | commitdiff | tree |
| 2011-03-17 |
Tim King | SimplexDecisionProcedure no longer takes an OutputChann... |
commit | commitdiff | tree |
| 2011-03-17 |
Tim King | - Removes arith_constants.h |
commit | commitdiff | tree |
| 2011-03-17 |
Tim King | Adds debugging output to EngineOutputChannel::lemma. |
commit | commitdiff | tree |
| 2011-03-17 |
Tim King | Fix for the bug introduced in 1477. The stuff that... |
commit | commitdiff | tree |
| 2011-03-17 |
Dejan Jovanović | push and pop manipulators for output stream so that... |
commit | commitdiff | tree |
| 2011-03-16 |
Tim King | - Turns on the excluded middle assertions during the... |
commit | commitdiff | tree |
| 2011-03-16 |
Tim King | - Turns on the miplibTrick. This detects during the... |
commit | commitdiff | tree |
| 2011-03-15 |
Dejan Jovanović | real fix for bug 245, previous one was faulty |
commit | commitdiff | tree |
| 2011-03-15 |
Morgan Deters | small fixes for run_regression script to workaround... |
commit | commitdiff | tree |
| 2011-03-15 |
Dejan Jovanović | fix for bug 254, lemmas were propagating at lower level... |
commit | commitdiff | tree |
| 2011-03-15 |
Morgan Deters | Merge from cudd branch. This mostly just adds support... |
commit | commitdiff | tree |
| 2011-03-14 |
Dejan Jovanović | adding support for google performance tools to the... |
commit | commitdiff | tree |
| 2011-03-14 |
Morgan Deters | change to the run_regression script to better manage... |
commit | commitdiff | tree |
| 2011-03-14 |
Morgan Deters | Fix to bug 251 (non-spurious warnings in builds) by... |
commit | commitdiff | tree |
| 2011-03-10 |
Morgan Deters | Fix bug 246 (occasional buffer overflow related to... |
commit | commitdiff | tree |
| 2011-03-10 |
Morgan Deters | ITE removal in TheoryEngine was not properly handling... |
commit | commitdiff | tree |
| 2011-03-08 |
Morgan Deters | Clean up Theory base class as per code review bug ... |
commit | commitdiff | tree |
| 2011-03-08 |
Tim King | - Merges queue-interrogation branch into the trunk... |
commit | commitdiff | tree |
| 2011-03-07 |
Tim King | Merges branches/arithmetic/tableau-reset into the trunk... |
commit | commitdiff | tree |
| 2011-03-05 |
Tim King | - Adds PermissiveBackArithVarSet. This is very similar... |
commit | commitdiff | tree |
| 2011-03-05 |
Tim King | Enables the PreferenceFunction minBoundAndRowCount. |
commit | commitdiff | tree |
| 2011-03-05 |
Tim King | - Adds "PreferenceFunction" to SimplexDecisionProcedure... |
commit | commitdiff | tree |
| 2011-03-05 |
Tim King | - Made Rational::sgn() function const. |
commit | commitdiff | tree |
| 2011-03-05 |
Morgan Deters | adding three features to CVC parser that drastically... |
commit | commitdiff | tree |
| 2011-03-03 |
Morgan Deters | fix for bug #244, "Segfault if file cannot be found... |
commit | commitdiff | tree |
| 2011-03-03 |
Tim King | - Creates a queue for lemmas discovered during the... |
commit | commitdiff | tree |
| 2011-03-03 |
Morgan Deters | resurrecting triple.h from r1023 (after which it was... |
commit | commitdiff | tree |
| 2011-03-03 |
Tim King | Merged the tableau-copy branch into trunk. This adds... |
commit | commitdiff | tree |
| 2011-03-03 |
Dejan Jovanović | fixing a type that caused the segfaults in the regressions |
commit | commitdiff | tree |
| 2011-03-02 |
Dejan Jovanović | fixing the big with lemma reallocation in minisat garba... |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog