summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2012-01-25Adding regress1 test ooo.rf6.smt2.Tim King
2012-01-23Partial fix to TheoryEngine::getExplanation so that SharedAssertions request ...Tim King
2012-01-23fix for bug295Dejan Jovanović
2012-01-17updates to smt2 parser to support datatypes, minor updates to datatypes theor...Andrew Reynolds
2011-12-15Partial fix to bug 295.Tim King
2011-12-15Fix to the previous commit.Tim King
2011-12-15Partial fix in arithmetic for propagating shared terms. This partially resolv...Tim King
2011-12-14added minor documentation for parametric datatypes, for bug 283Andrew Reynolds
2011-12-14minor fixes to printing and parsing of CVC-language defined functions and lam...Morgan Deters
2011-12-14some more bug fixes (TNode -> Node, normalize literals in explanations)Dejan Jovanović
2011-12-12* merging some uf stuff from incremental_work branch that somehow nobody merg...Dejan Jovanović
2011-12-10adding additional checks for theories propagating literals that already have ...Dejan Jovanović
2011-12-10a bit more changes, when propagting equalities/dis-equalities don't assert th...Dejan Jovanović
2011-12-10attempt to fix bug 293: if a split on a trivial shared pair is requested from...Dejan Jovanović
2011-12-08Disable a BV rewriter statistic (after checking with Liana) that was static,Morgan Deters
2011-12-06LemmaStatus changes, as agreed to during 12/2 meeting.Morgan Deters
2011-12-06oops, removing some integer operations that leaked in (they aren't part of tr...Morgan Deters
2011-12-06fix errors in smt-lib2 output; needed for debuggingMorgan Deters
2011-12-05change short-circuiting behavior of Command execution in the main driver; all...Morgan Deters
2011-12-02Error detection is different now---with new Command infrastructure, exception...Morgan Deters
2011-11-30disable bug288.smt so that "make check" goes through---pending integers merge...Morgan Deters
2011-11-30fix linking errors on oneiricMorgan Deters
2011-11-30Simplified bug288.smt to reflect the problem in integers better.Tim King
2011-11-30Added a failing regression test corresponding to bug 289.Tim King
2011-11-30Adding a failing UFLIA benchmark corresponding to bug #288.Tim King
2011-11-29Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic no...Tim King
2011-11-26Fix Java JNI installation pathMorgan Deters
2011-11-22fix module name for CVC4 jar file; part of the fix for the Debian package bui...Morgan Deters
2011-11-22More language bindings work:Morgan Deters
2011-11-16Fix "make dist". Fixes to python and ruby bindings; ruby example written. T...Morgan Deters
2011-11-16Addressed many of the concerns raised in the public interface review of CVC4 ...Morgan Deters
2011-11-16fix to build system for java bindingsMorgan Deters
2011-11-16* Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy!Morgan Deters
2011-11-15Bindings work (ocaml bindings are now sort of working); also minor cleanupMorgan Deters
2011-11-15additional minor changes to get python binding on better footingMorgan Deters
2011-11-15fixes for python language binding, added python exampleMorgan Deters
2011-11-14public tests need to be linked against gmp/cln explicitly---looks like a subt...Morgan Deters
2011-11-06datatype stuff in compatibility interface implementedMorgan Deters
2011-11-05Context::ScopedPush implemented (in support of theory speculation, like upcom...Morgan Deters
2011-11-04STRING_TYPE and CONST_STRING and associate type infrastructure implemented.Morgan Deters
2011-11-02Only print a shortlist of most-commonly-used options on option processing err...Morgan Deters
2011-11-02give an option error if the user specifies --proof in a non-proof-enabled buildMorgan Deters
2011-11-02fully implement the always-check-again-after-the-output-channel-is-used fix f...Morgan Deters
2011-11-02Sometimes antlr decides to generate lexers and parsers in a different directo...Morgan Deters
2011-11-02better Integer asserts when there's overflow on conversion to unsigned long /...Morgan Deters
2011-11-01Improvements to header installation on user machines. Internally, we canMorgan Deters
2011-10-31fixes to assertions in GMP to match CLN behaviorMorgan Deters
2011-10-31Added assertions to the CLN implementation of Integer for getLong() and getUn...Tim King
2011-10-31another make distclean fixMorgan Deters
2011-10-31fixes to "make distclean" and "make maintainerclean"Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback