2010-06-14 |
Tim King | Fix to arith to make sure it only attempts to report... |
commit | commitdiff | tree |
2010-06-14 |
Clark Barrett | Started work on array theory |
commit | commitdiff | tree |
2010-06-06 |
Tim King | Some assorted fixes and local optimizations for theory... |
commit | commitdiff | tree |
2010-06-06 |
Tim King | Adding += and *= to Rational. |
commit | commitdiff | tree |
2010-06-04 |
Tim King | Changed how assignments are saved during check. These... |
commit | commitdiff | tree |
2010-06-04 |
Tim King | Changed several arguments to const references. |
commit | commitdiff | tree |
2010-06-04 |
Christopher... | Adding QF_SAT to SMT parsers |
commit | commitdiff | tree |
2010-06-04 |
Christopher... | Reimplementing AntlrInputStream::newStreamInputStream |
commit | commitdiff | tree |
2010-06-04 |
Morgan Deters | ** Don't fear the files-changed list, almost all change... |
commit | commitdiff | tree |
2010-06-04 |
Christopher... | Missing files in last commit |
commit | commitdiff | tree |
2010-06-04 |
Christopher... | Enabling RDL/IDL in SMT v1 and adding some simple tests |
commit | commitdiff | tree |
2010-06-03 |
Christopher... | Implementing input from stdin (Fixes: #144) |
commit | commitdiff | tree |
2010-06-03 |
Tim King | Fixes 2 issues with assignments. The first is construct... |
commit | commitdiff | tree |
2010-06-03 |
Tim King | Adds toString to DeltaRational |
commit | commitdiff | tree |
2010-06-03 |
Tim King | Fixes a bug where registration occurs before preregistr... |
commit | commitdiff | tree |
2010-06-03 |
Christopher... | Changing ANTLR3 detection in configure (Fixes #147) |
commit | commitdiff | tree |
2010-06-03 |
Morgan Deters | * Added NodeBuilder<>::getChild() to make interface... |
commit | commitdiff | tree |
2010-06-03 |
Morgan Deters | resolving bug 139: metaKindOf() warnings still exist... |
commit | commitdiff | tree |
2010-06-02 |
Morgan Deters | added a handful of debugTagIsOn("context") checks to... |
commit | commitdiff | tree |
2010-06-02 |
Morgan Deters | more VERBOSE test failures |
commit | commitdiff | tree |
2010-06-01 |
Christopher... | Fixing test failures in production build |
commit | commitdiff | tree |
2010-06-01 |
Tim King | This commit adds a debugTagIsOn() guard around some... |
commit | commitdiff | tree |
2010-06-01 |
Tim King | This commit is a fix for a bug in removeITEs(). The... |
commit | commitdiff | tree |
2010-06-01 |
Christopher... | Adding SMT v2 parsing support for: QF_IDL, QF_NIA,... |
commit | commitdiff | tree |
2010-06-01 |
Christopher... | Checking for executable permission on antlr3 script |
commit | commitdiff | tree |
2010-06-01 |
Tim King | Fixed a bug in partial_model.cpp where the data was... |
commit | commitdiff | tree |
2010-06-01 |
Christopher... | Fixing failing test in r521 |
commit | commitdiff | tree |
2010-06-01 |
Dejan Jovanović | In order for splitting on demand to be able to retract... |
commit | commitdiff | tree |
2010-05-31 |
Christopher... | First draft implementation of mkAssociative |
commit | commitdiff | tree |
2010-05-29 |
Tim King | Adding a couple of example from fuzzsmt to regress1. |
commit | commitdiff | tree |
2010-05-29 |
Tim King | Couple of fixes to theory arith. pivotAndUpdate now... |
commit | commitdiff | tree |
2010-05-29 |
Tim King | After blasting the disjuncts, TheoryEngine rewrite... |
commit | commitdiff | tree |
2010-05-28 |
Tim King | This update enables TheoryArith to accept assertions... |
commit | commitdiff | tree |
2010-05-28 |
Tim King | Bug fixes for combining coefficients of rewritten nodes. |
commit | commitdiff | tree |
2010-05-28 |
Tim King | Added printModel() to src/theory/arith/partial_model... |
commit | commitdiff | tree |
2010-05-28 |
Tim King | A few changes to the organization of TheoryEngine rewri... |
commit | commitdiff | tree |
2010-05-28 |
Tim King | Moving the ITE removal from CnfStream to TheoryEngine... |
commit | commitdiff | tree |
2010-05-27 |
Morgan Deters | fix bug #134: infinite deallocation loop |
commit | commitdiff | tree |
2010-05-27 |
Morgan Deters | small cosmetic change to tests summary output |
commit | commitdiff | tree |
2010-05-27 |
Morgan Deters | Remove isAtomic() as per 4/27/2010 meeting. Add commen... |
commit | commitdiff | tree |
2010-05-27 |
Morgan Deters | fix compiler comparison-signedness warnings |
commit | commitdiff | tree |
2010-05-27 |
Tim King | Reverting this file to not include any comments. (Morga... |
commit | commitdiff | tree |
2010-05-27 |
Morgan Deters | added the ability to add custom expected stdout, stderr... |
commit | commitdiff | tree |
2010-05-27 |
Tim King | Preregistration has been turned on. Highly experimental... |
commit | commitdiff | tree |
2010-05-27 |
Morgan Deters | Use the newer automake test driver "parallel-tests... |
commit | commitdiff | tree |
2010-05-27 |
Christopher... | Adding debug assertions on most TNode operations |
commit | commitdiff | tree |
2010-05-27 |
Christopher... | Adding NodeManager::prepareToBeDestroyed() (Fixes:... |
commit | commitdiff | tree |
2010-05-27 |
Christopher... | Adding .cvc4_config to .gitignore |
commit | commitdiff | tree |
2010-05-27 |
Morgan Deters | fix bug #111: errors in building lcov-all |
commit | commitdiff | tree |
2010-05-27 |
Morgan Deters | fix bug 120; competition mode regression failures for... |
commit | commitdiff | tree |
2010-05-26 |
Tim King | . '+Outstanding case split in theory arith' |
commit | commitdiff | tree |
2010-05-26 |
Christopher... | Adding CnfStreamBlack tests for all Boolean connectives |
commit | commitdiff | tree |
2010-05-26 |
Christopher... | Fixing test failures in CnfStreamBlack (it was the... |
commit | commitdiff | tree |
2010-05-26 |
Christopher... | Adding documentation to my-configure |
commit | commitdiff | tree |
2010-05-26 |
Christopher... | Fixing my-configure |
commit | commitdiff | tree |
2010-05-26 |
Christopher... | Adding contrib/my-configure |
commit | commitdiff | tree |
2010-05-26 |
Christopher... | Adding CnfStream unit tests |
commit | commitdiff | tree |
2010-05-26 |
Morgan Deters | CDMap<> and CDOmap<> fixes to resolve bug 123 |
commit | commitdiff | tree |
2010-05-26 |
Tim King | Fix for bug 131. Added some additional debugging assert... |
commit | commitdiff | tree |
2010-05-26 |
Morgan Deters | CDMap: fix bug 130 |
commit | commitdiff | tree |
2010-05-26 |
Christopher... | Prevent lexer errors being raised if a parser error... |
commit | commitdiff | tree |
2010-05-25 |
Tim King | Added Rational constructors that only take a numerator... |
commit | commitdiff | tree |
2010-05-25 |
Dejan Jovanović | Some initial changes to allow for lemmas on demand. |
commit | commitdiff | tree |
2010-05-21 |
Tim King | Small fixes to TheoryArith. Added a hack to make Integ... |
commit | commitdiff | tree |
2010-05-20 |
Tim King | Added the division symbol to the parser, and minimal... |
commit | commitdiff | tree |
2010-05-19 |
Tim King | Significant revision to theory/arith. The new draft... |
commit | commitdiff | tree |
2010-05-14 |
Christopher... | Adding debugging code in PropEngine/CnfStream |
commit | commitdiff | tree |
2010-05-14 |
Christopher... | Adding ITE tests |
commit | commitdiff | tree |
2010-05-14 |
Christopher... | Adding rudimentary ITE handling in CnfStream |
commit | commitdiff | tree |
2010-05-14 |
Christopher... | Virtualizing interface between CnfStream and SatSolver |
commit | commitdiff | tree |
2010-05-13 |
Christopher... | Minor refactorings to PropEngine, SatSolver |
commit | commitdiff | tree |
2010-05-13 |
Christopher... | Minor refactorings and corrections to comments |
commit | commitdiff | tree |
2010-05-12 |
Christopher... | Adding ParserBuilder, reducing visibility of Parser... |
commit | commitdiff | tree |
2010-05-12 |
Christopher... | true and false are only defined if the core theory... |
commit | commitdiff | tree |
2010-05-12 |
Christopher... | Refactoring parser tests |
commit | commitdiff | tree |
2010-05-12 |
Christopher... | Adding class Smt2 to handle declaration of logic and... |
commit | commitdiff | tree |
2010-05-07 |
Christopher... | Tightening lexer rules for numerals in SMT v2 |
commit | commitdiff | tree |
2010-05-07 |
Morgan Deters | make CVC4::Rational public (fixes broken build) |
commit | commitdiff | tree |
2010-05-06 |
Christopher... | Adding --strict-parsing option |
commit | commitdiff | tree |
2010-05-06 |
Christopher... | Adding AntlrInput::tokenTextSubstr |
commit | commitdiff | tree |
2010-05-06 |
Christopher... | Adding tests for Rational::fromDecimal |
commit | commitdiff | tree |
2010-05-06 |
Christopher... | Adding tests for Integer::pow |
commit | commitdiff | tree |
2010-05-06 |
Christopher... | Adding bit-vector constants in SMT2 |
commit | commitdiff | tree |
2010-05-06 |
Christopher... | Implementing Rational::fromDecimal and adding support... |
commit | commitdiff | tree |
2010-05-06 |
Dejan Jovanović | fixing the nightly failure. TypeCheckingException is... |
commit | commitdiff | tree |
2010-05-05 |
Dejan Jovanović | changing the interface to bit-vector constant constructor |
commit | commitdiff | tree |
2010-05-05 |
Dejan Jovanović | bit-vector constant constructor from string |
commit | commitdiff | tree |
2010-05-05 |
Dejan Jovanović | bug fixes for types, old unit tests for types work now |
commit | commitdiff | tree |
2010-05-04 |
Christopher... | Adding simple SMT2 parser tests |
commit | commitdiff | tree |
2010-05-04 |
Christopher... | Disabling semantic checks in competition mode. |
commit | commitdiff | tree |
2010-05-04 |
Christopher... | Minor change to SMT v2 grammar |
commit | commitdiff | tree |
2010-05-04 |
Christopher... | Adding general support for SMT2 set-info command |
commit | commitdiff | tree |
2010-05-04 |
Christopher... | Handling SMT 2.0 symbols and info flags |
commit | commitdiff | tree |
2010-05-04 |
Dejan Jovanović | Type-checking classes and hooks (not tested yet). |
commit | commitdiff | tree |
2010-05-03 |
Morgan Deters | more reasonable smt 2.0 benchmark test |
commit | commitdiff | tree |
2010-05-03 |
Morgan Deters | main driver supports .smt2 input, added an smt2 regress... |
commit | commitdiff | tree |
2010-05-03 |
Morgan Deters | theory detection fixes; fixes build breakage when you... |
commit | commitdiff | tree |
2010-05-03 |
Christopher... | Small mistake in previous commit |
commit | commitdiff | tree |
2010-05-03 |
Christopher... | Importing ANTLR3 lexer nextToken function to avoid... |
commit | commitdiff | tree |
2010-05-02 |
Dejan Jovanović | smt parser for bit-vectors |
commit | commitdiff | tree |
next |