cvc5.git
2011-09-02 Dejan Jovanović* Changing pre-registration to be context dependent...
2011-08-30 Dejan JovanovićFixin the SAT solver for Andy. Even if a SAT lemma...
2011-08-27 Dejan JovanovićRemoving Theory::registerTerm() as discussed in the...
2011-08-25 Dejan JovanovićFixing the broken unit tests
2011-08-24 Dejan JovanovićSimplification of the preregister and register throught...
2011-08-23 Dejan Jovanovićsome uf cleanup
2011-08-17 Dejan Jovanovićnew implementation of lemmas on demand
2011-07-12 Morgan Detersforgot to reflect naming change in makefile. fixed
2011-07-12 Morgan Detersfix bug 272, array unsoundness, and some array cleanup
2011-07-11 Morgan Detersremove some array regressions from "make check" so...
2011-07-11 Morgan Detersstatus of examples
2011-07-11 Morgan Detersnew array bugs ?
2011-07-11 Morgan Detersfixing out of place typename (error on g++ 4.4.3-4ubuntu5)
2011-07-11 Morgan Deterssubmission script
2011-07-11 Clark BarrettAdding static_fact_manager
2011-07-11 Clark BarrettClark's work on array theory - can now solve all QF_AX...
2011-07-11 Morgan Detersfix some confusing debug output (bogus counter)
2011-07-11 Morgan Detersmark the new minimized benchmark as unsat
2011-07-11 Morgan Detersif running in QF_AX, equalities over terms of uninterpr...
2011-07-11 Morgan Detersminimized example
2011-07-11 Morgan Detersarray benchmarks
2011-07-11 Dejan Jovanovićadding disequality propagation
2011-07-11 Morgan Detersmerge from symmetry branch
2011-07-10 Clark BarrettReverting mistaken check-in
2011-07-10 Dejan Jovanovićchanging the sat solver remove clauses constants
2011-07-10 Clark BarrettFixed bug in default solve - wasn't returning when...
2011-07-10 Dejan Jovanovićanother typo
2011-07-10 Dejan Jovanovićyet another uf bug fix, hopefully the last
2011-07-10 Dejan Jovanovićanother bugfix for uf
2011-07-09 Dejan Jovanovićsome immediate bug fixes
2011-07-09 Morgan Detersfix submission makefile
2011-07-09 Morgan Detersminor fixups
2011-07-09 Dejan Jovanovićsurprize surprize
2011-07-07 Dejan Jovanovićremoving duplicate clauses in ite cnf conversion
2011-07-07 Morgan Deterscudd-building prefs with --with-cudd / --without-cudd
2011-07-06 Dejan JovanovićFixing two bugs:
2011-07-05 Dejan Jovanovićmissing test case
2011-07-05 Dejan Jovanovićupdated preprocessing and rewriting input equalities...
2011-06-30 Morgan DetersAllow (- x) for unary minus in SMT-LIBv1, in addition...
2011-06-30 Tim KingChanged the defaults for arithPivotThreshold and arithP...
2011-06-30 Tim KingMerging the playground branch upto r1957 into trunk.
2011-06-30 Morgan Detersonly use theory registration if (1) a theory requests...
2011-06-30 Morgan Deterssome things I had laying around in a directory but...
2011-06-29 Tim KingFixed spelling mistake and documentation for --enable...
2011-06-18 Morgan DetersSome fixes inspired by Fedora 15:
2011-06-06 Morgan Deterscompilation fix for x86 (from previous commit)
2011-06-06 Morgan DetersFix for Mac OS breakage (x86 didn't crash, but probably...
2011-06-03 Andrew Reynoldsfixed various bugs related to ambiguous parametric...
2011-06-03 Morgan Detersdatatypes work
2011-06-02 Morgan Detersminor fix to build system for system tests
2011-06-02 Andrew Reynoldsadded (temporary) support for ensuring that all ambiguo...
2011-06-01 Morgan Detersminor fix, and better output for type errors
2011-06-01 Morgan Deterstype ascriptions (casts) for parameterized datatypes...
2011-05-31 Tim KingThis commit contains the code for allowing arbitrary...
2011-05-28 Morgan Detersfix unit test linking issue
2011-05-28 Morgan Detersinclude subversion information used for each build...
2011-05-26 Morgan Detersapply arithmetic static learner's miplibtrick in a...
2011-05-23 Morgan Detersfixes for "make dist" and "make doc", minor cleanups
2011-05-23 Morgan DetersMerge from arrays2 branch.
2011-05-14 Morgan Detersfix production-build compiler warning
2011-05-14 Morgan Detersre-add a removed Datatype constructor that was causing...
2011-05-14 Morgan Detersreverting node manager change from 1881; also part...
2011-05-14 Morgan Detersadd AscriptionType stuff to support nullary parameteriz...
2011-05-13 Andrew Reynoldsadded support for parametric datatypes, updated cvc...
2011-05-13 Morgan Deters* fix for Mac OS (includes some ThreadLocal stuff copie...
2011-05-06 Tim KingDeleting dead code.
2011-05-06 Andrew Reynoldsadded 10 benchmarks to regress/regress0/datatypes from...
2011-05-06 Andrew Reynoldssignificant revisions/improvements to code for theory...
2011-05-05 Morgan DetersMerge from nonclausal-simplification-v2 branch:
2011-05-05 Morgan Detersluby sequence generator; can use to plot MiniSat's...
2011-05-04 Morgan DetersStronger support for zero-performance-penalty output...
2011-05-03 Morgan Detersoutput fixes for performance
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.
next