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 |
2010-05-01 |
Dejan Jovanović | Fix for the last night's build errors (type that broke... |
commit | commitdiff | tree |
2010-05-01 |
Christopher... | Adding missed antlr_input files |
commit | commitdiff | tree |
2010-05-01 |
Christopher... | Fixing private/public header warnings in parser library |
commit | commitdiff | tree |
2010-05-01 |
Christopher... | Adding comments to bounded token files |
commit | commitdiff | tree |
2010-04-30 |
Dejan Jovanović | Fix for bug 115, mapping was going in the wrong direction. |
commit | commitdiff | tree |
2010-04-29 |
Dejan Jovanović | Added the capability to construct expressions by passin... |
commit | commitdiff | tree |
2010-04-29 |
Christopher... | (Not) Handling parameterized sorts in SMT v2 |
commit | commitdiff | tree |
2010-04-29 |
Christopher... | Minor fix to SMT v2 parser tests |
commit | commitdiff | tree |
2010-04-29 |
Christopher... | First draft implementation of SMT v2 parser |
commit | commitdiff | tree |
2010-04-28 |
Christopher... | SMT parser has to map 'Real' to RealType |
commit | commitdiff | tree |
2010-04-28 |
Tim King | Merging the arithmetic theory draft (lra-init) back... |
commit | commitdiff | tree |
2010-04-28 |
Dejan Jovanović | adding integer and real types to the public interface |
commit | commitdiff | tree |
2010-04-28 |
Dejan Jovanović | Build fix for parser |
commit | commitdiff | tree |
2010-04-28 |
Christopher... | Refactoring Input/Parser code to support external manip... |
commit | commitdiff | tree |
2010-04-28 |
Tim King | Added theory/arith/kind and enabled the smt parser... |
commit | commitdiff | tree |
2010-04-27 |
Christopher... | Adding Integer and Rational constants to SMT |
commit | commitdiff | tree |
2010-04-27 |
Christopher... | Adding a bit of documentation to the SMT parser |
commit | commitdiff | tree |
2010-04-26 |
Dejan Jovanović | Some cleanup. Also added the integer and real types. |
commit | commitdiff | tree |
next |