summaryrefslogtreecommitdiff
path: root/src/util
AgeCommit message (Expand)Author
2010-05-25Added Rational constructors that only take a numerator. The const char* Ratio...Tim King
2010-05-12Adding class Smt2 to handle declaration of logic and theory symbolsChristopher L. Conway
2010-05-07make CVC4::Rational public (fixes broken build)Morgan Deters
2010-05-06Adding --strict-parsing optionChristopher L. Conway
2010-05-06Adding tests for Rational::fromDecimalChristopher L. Conway
2010-05-06Adding bit-vector constants in SMT2Christopher L. Conway
2010-05-06Implementing Rational::fromDecimal and adding support for real constants in S...Christopher L. Conway
2010-05-05changing the interface to bit-vector constant constructorDejan Jovanović
2010-05-05bit-vector constant constructor from stringDejan Jovanović
2010-05-04Disabling semantic checks in competition mode.Christopher L. Conway
2010-05-04Adding general support for SMT2 set-info commandChristopher L. Conway
2010-05-04Type-checking classes and hooks (not tested yet).Dejan Jovanović
2010-05-02smt parser for bit-vectorsDejan Jovanović
2010-04-29Added the capability to construct expressions by passing the operator instead...Dejan Jovanović
2010-04-28Merging the arithmetic theory draft (lra-init) back into the main trunk. Thi...Tim King
2010-04-14Marging from types 404:415, changes: MassiveDejan Jovanović
2010-04-09added experimental "make lcov" target (it runs only unit tests); better cover...Morgan Deters
2010-04-04* Node::isAtomic() now looks at an "atomic" attribute of argumentsMorgan Deters
2010-04-01reran update-copyright.pl to get new contributors and add new header comments...Morgan Deters
2010-04-01PARSER STUFF:Morgan Deters
2010-03-30Removing unnecessary .gitignoresChristopher L. Conway
2010-03-30Merging from branches/antlr3 (r246:354)Christopher L. Conway
2010-03-30Highlights of this commit are:Morgan Deters
2010-03-28Improved the documentation and testing for Rational.Tim King
2010-03-26Added GMP backed Rational and Integer classes, and white box tests for them. ...Tim King
2010-03-16* test/unit/Makefile.am, test/unit/expr/attribute_white.h,Morgan Deters
2010-03-15This checkin resolves bug #57.Morgan Deters
2010-03-12* Added shutdown() functions to SmtEngine, TheoryEngine, PropEngine,Morgan Deters
2010-03-08This fixes regressions at levels >= 1 which were failingMorgan Deters
2010-03-05* public/private code untangled (smt/smt_engine.h no longer #includesMorgan Deters
2010-03-02* NodeBuilder work: specifically, convenience builders. "a && b && c || d && e"Morgan Deters
2010-02-27Adding --mmap option to use memory-mapped file input, which provides a margin...Christopher L. Conway
2010-02-26* test/unit/context/context_black.h: Test CDList<>. In particular,Morgan Deters
2010-02-22* configure.ac: Remove doc/ from search path for Makefile.amsMorgan Deters
2010-02-22fix bug 22 (remove tracing from non-trace builds; remove all outputMorgan Deters
2010-02-19specialized implementation for boolean node attributes ("flags"): they now sh...Morgan Deters
2010-02-18Adding --no-checking option to disable semantic checks in parserChristopher L. Conway
2010-02-16Adding --parse-only optionChristopher L. Conway
2010-02-12build fixDejan Jovanović
2010-02-12Fix to compile out Debug(...) << ... statements in optimized mode. Someone pl...Dejan Jovanović
2010-02-04minor interface changes to TheoryEngine/Theory after meeting and conversation...Morgan Deters
2010-02-04remove -*- c++ -*- emacs tag from source files (it overrides cvc4-c++-editing...Morgan Deters
2010-02-04minor cleanup; give the main driver a different exit code for SAT-INVALID/UNS...Morgan Deters
2010-02-04src/expr/kind.h is now automatically generated.Morgan Deters
2010-02-04minor fix for update-copyright.pl; ran update-copyright.pl on all sources; re...Morgan Deters
2010-02-03Addressed many of the concerns of bug 10 (build system code review).Morgan Deters
2010-02-03ELSEIF support and parser debugging with '-d parser'Dejan Jovanović
2010-02-03simple ITE parsingDejan Jovanović
2010-02-02Switched cnf conversion to go through CnfStream.Tim King
2010-01-30cnf conversion (variable-introducing), cleanups, fixes to minisat calling for...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback