cvc5.git
2011-05-02 Andrew Reynoldsminor updates to exp manager, fixed 32bit vs 64bit...
2011-05-02 Morgan Detersfix for configure
2011-05-02 Morgan Detersadding some previously-failing "bug" test cases for...
2011-05-02 Dejan Jovanovićupdating bv regressions
2011-05-02 Dejan Jovanovićparser fixes for bug 243
2011-05-02 Dejan Jovanovićupdates for bitvectors
2011-05-02 Morgan Detersmore minor fixes related to last few commits
2011-05-02 Morgan Detersanother small fix
2011-05-02 Morgan Detersfix broken build; sorry, all!
2011-05-02 Morgan Detersfix a performance issue from last commit
2011-05-02 Morgan DetersMinor fixes to various parts of CVC4, including the...
2011-05-01 Morgan Detersminor fixes, plus experimental readline support in...
2011-04-29 Andrew Reynoldsrefactoring to datatypes theory, added working prototyp...
2011-04-28 Andrew Reynoldsmore fixes/improvements to datatypes theory and transit...
2011-04-27 Andrew Reynoldscleaned up some of the hacks in the datatypes theory...
2011-04-25 Morgan DetersMonday tasks:
2011-04-25 Morgan Deterssmall unit test fix; was broken only in non-assertion...
2011-04-25 Morgan DetersWeekend work. The main points:
2011-04-23 Morgan Detersfix for parser/tests for ANTLR 3.2 (it was working...
2011-04-23 Morgan Deters* reviewed BooleanSimplification, added documentation...
2011-04-23 Morgan Detersmake run_regression script robust to DOS newlines :(
2011-04-22 Andrew Reynoldsadded fixes for datatype theory solver to account for...
2011-04-22 Morgan Detersfix to last commit
2011-04-22 Morgan DetersFixing SmtEngine::getValue() by adding a NodeManagerSco...
2011-04-20 Morgan Detersnumerous bugfixes
2011-04-20 Morgan Detersincorrect usage of C++ std::string caused a test to...
2011-04-20 Morgan DetersMinor mixed-bag commit. Expected performance impact...
2011-04-20 Morgan DetersTuesday end-of-day commit.
2011-04-18 Tim KingRemoving dead code that came in on commit r1740.
2011-04-18 Morgan Detersmore work on CVC language
2011-04-18 Morgan Detersmostly CVC presentation language parsing and printing
2011-04-18 Tim KingThis commit merges the branch arithmetic/propagation...
2011-04-18 Morgan DetersPartial merge from datatypes-merge branch:
2011-04-18 Christopher... Fixing output for EOF token in parser errors
2011-04-16 Morgan Detersalso a fix for a system test related to ParserBuilder
2011-04-16 Morgan Detersunit test fixes for new NodeManager constructor (relate...
2011-04-15 Morgan Detersparser/driver fixes for last commit
2011-04-15 Morgan Deterspartial merge from portfolio branch, adding conversions...
2011-04-14 Dejan Jovanovićreverting back the minisat code and adding a simpler...
2011-04-14 Morgan DetersThree things:
2011-04-14 Dejan Jovanovićfixing an uninitialized literal variable
2011-04-13 Dejan Jovanovićadding support for unit conflicts in minisat...
2011-04-13 Morgan Detersfix compiler warning in non-replay builds
2011-04-13 Morgan Deterscache the LET rewriting (and defined-function expansion...
2011-04-13 Morgan Detersadd disequality token ("/=") and rules to CVC parser
2011-04-12 Morgan Detersanother small fix to "make dist" that can lead to a...
2011-04-11 Clark BarrettTransitive closure module is working
2011-04-11 Morgan Detersfix "make dist" issues in makefiles
2011-04-10 Morgan Detersmerge from replay branch
2011-04-10 Morgan DetersAdd -lprofiler when --with-google-perftools is offered...
2011-04-09 Dejan Jovanovićchanging the sat solver to assert propagated literals...
2011-04-08 Clark BarrettAdded util class
2011-04-07 Tim KingMade Valuation::getValue() and Valuation::getSatValue...
2011-04-05 Morgan DetersMemory fix for congruence closure; affects many UF...
2011-04-05 Tim KingAdded options for setting the random decision frequency...
2011-04-05 Morgan DetersMinor adjustments to the Registrar commit in 1644,...
2011-04-04 Tim KingMerging the satliteral-before-prereg branch into trunk...
2011-04-04 Tim KingReverts previous commit r1636.
2011-04-04 Morgan DetersAdd documentation to Node and TNode (closes bug #201).
2011-04-02 Tim KingDelayed the addition of unate propagation lemmas until...
2011-04-02 Morgan Deterswith --with-google-perftools, don't just take it on...
2011-04-02 Morgan Detersminor fixes
2011-04-01 Morgan Detersminor bugfixes (fixes broken dynamic-library build...
2011-04-01 Morgan Detersdocumentation fix
2011-04-01 Morgan DetersThis commit is a merge from the "betterstats" branch...
2011-03-31 Tim KingFixes to Valuation.
2011-03-30 Morgan Detersimprove recent low-coverage complaints
2011-03-30 Dejan Jovanovićadding CVC4:: qualifier to the #define for debugging...
2011-03-30 Tim KingMoved the constructor for Options out of the header...
2011-03-30 Tim KingAdded the command line flag --rewrite-arithmetic-equali...
2011-03-30 Morgan DetersAdd Valuation::getSatValue() so that theories can acces...
2011-03-30 Tim KingMerged the branch sparse-tableau into trunk.
2011-03-27 Morgan Detersfixes to attribute-internals warnings on 64-bit; also...
2011-03-26 Dejan Jovanovićfix for bug 253, was propagating an asserted literal
2011-03-26 Morgan Detersfix typo
2011-03-25 Morgan DetersThis is a merge from the "theoryfixes+cdattrhash" branc...
2011-03-25 Morgan DetersFix for a bug Andrew Reynolds found for iterators that...
2011-03-22 Tim KingMerges the small changes on the queue-period branch...
2011-03-22 Dejan Jovanovićupdating debug output usage to eliviate impact of bug 252
2011-03-21 Dejan Jovanovićmore bugfixes, some basic propagation, and testcases...
2011-03-21 Dejan Jovanovićfixing a bug in the BV rewrite, off by one error when...
2011-03-20 Dejan Jovanovićagain a typo
2011-03-20 Dejan Jovanovićmore bugfixes for bitvectors
2011-03-20 Dejan Jovanovićfixing the failure from last nigth, due to using a...
2011-03-20 Dejan Jovanovićmissed one case
2011-03-20 Dejan Jovanovićcommit for the version of bitvectors that passes all...
2011-03-19 Tim KingMerges the pqueue-set branch into trunk. During VarOrd...
2011-03-18 Tim King- The learned clauses from the miplib trick were being...
2011-03-17 Tim KingSwitched SimplexDecisionProcedure::d_delayedLemmas...
2011-03-17 Tim KingSimplexDecisionProcedure no longer takes an OutputChann...
2011-03-17 Tim King- Removes arith_constants.h
2011-03-17 Tim KingAdds debugging output to EngineOutputChannel::lemma.
2011-03-17 Tim KingFix for the bug introduced in 1477. The stuff that...
2011-03-17 Dejan Jovanovićpush and pop manipulators for output stream so that...
2011-03-16 Tim King- Turns on the excluded middle assertions during the...
2011-03-16 Tim King- Turns on the miplibTrick. This detects during the...
2011-03-15 Dejan Jovanovićreal fix for bug 245, previous one was faulty
2011-03-15 Morgan Deterssmall fixes for run_regression script to workaround...
2011-03-15 Dejan Jovanovićfix for bug 254, lemmas were propagating at lower level...
2011-03-15 Morgan DetersMerge from cudd branch. This mostly just adds support...
next