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 |
2010-04-26 |
Dejan Jovanović | Adding the intermediary TypeNode to represent (and... |
commit | commitdiff | tree |
2010-04-17 |
Christopher... | Fixing compiler error for optimized builds |
commit | commitdiff | tree |
2010-04-15 |
Dejan Jovanović | Adding info in the minisat README |
commit | commitdiff | tree |
2010-04-15 |
Christopher... | Implementing missing NodeBuilder::constructNode |
commit | commitdiff | tree |
2010-04-15 |
Christopher... | Enhancements to NodeManager tests, taking advantage... |
commit | commitdiff | tree |
2010-04-15 |
Christopher... | Removing horrible, system-locking option from Eclipse... |
commit | commitdiff | tree |
2010-04-15 |
Christopher... | Moving debug output in ~ContextObj under a conditional... |
commit | commitdiff | tree |
2010-04-14 |
Dejan Jovanović | Marging from types 404:415, changes: Massive |
commit | commitdiff | tree |
2010-04-14 |
Morgan Deters | * Better dependency tracking for unit test building... |
commit | commitdiff | tree |
2010-04-13 |
Christopher... | Merging from branches/decl-scopes (r401:411) |
commit | commitdiff | tree |
2010-04-13 |
Christopher... | Doxygen fixes |
commit | commitdiff | tree |
2010-04-09 |
Morgan Deters | minor fixes to lcov build target, better contextobj... |
commit | commitdiff | tree |
2010-04-09 |
Morgan Deters | added experimental "make lcov" target (it runs only... |
commit | commitdiff | tree |
2010-04-08 |
Morgan Deters | A handful of build system fixes: |
commit | commitdiff | tree |
2010-04-07 |
Tim King | This update contains more black-box tests as part of... |
commit | commitdiff | tree |
2010-04-06 |
Morgan Deters | * Add some protected ContextObj accessors for ContextOb... |
commit | commitdiff | tree |
2010-04-05 |
Christopher... | Adding black-box tests for NodeManager (Closes bug... |
commit | commitdiff | tree |
2010-04-05 |
Christopher... | Removing unused functions that were causing compiler... |
commit | commitdiff | tree |
2010-04-05 |
Christopher... | Simplifying ANTLR3 overrides |
commit | commitdiff | tree |
2010-04-05 |
Morgan Deters | updating COPYING file to reflect that antlr_input_impor... |
commit | commitdiff | tree |
2010-04-05 |
Christopher... | Updating copyright exclusion |
commit | commitdiff | tree |
2010-04-05 |
Christopher... | Moving sources copied from libantlr3c to separate file |
commit | commitdiff | tree |
2010-04-05 |
Christopher... | Ignoring gcov files |
commit | commitdiff | tree |
2010-04-05 |
Christopher... | Moving code imported from libantlr3c to separate file... |
commit | commitdiff | tree |
2010-04-05 |
Morgan Deters | fix most of the warnings in the parser by (1) quieting... |
commit | commitdiff | tree |
2010-04-05 |
Christopher... | Adding match override to AntlrInput, in attempt to... |
commit | commitdiff | tree |
2010-04-05 |
Christopher... | Minor refactorings, in response to code review (Bug... |
commit | commitdiff | tree |
2010-04-05 |
Christopher... | Typos and renames for code review |
commit | commitdiff | tree |
2010-04-05 |
Morgan Deters | minor formatting and code guidelines, related to parser... |
commit | commitdiff | tree |
2010-04-04 |
Morgan Deters | * Addressed issues brought up in Chris's review of... |
commit | commitdiff | tree |
2010-04-04 |
Morgan Deters | * Node::isAtomic() now looks at an "atomic" attribute... |
commit | commitdiff | tree |
2010-04-04 |
Morgan Deters | Recommit revision 365 (undoing revision 375, which... |
commit | commitdiff | tree |
2010-04-03 |
Christopher... | Reverting r365 |
commit | commitdiff | tree |
2010-04-02 |
Christopher... | Overriding ANTLR3 error recovery routine |
commit | commitdiff | tree |
2010-04-02 |
Christopher... | Fixing double delete bug in main.cpp |
commit | commitdiff | tree |
2010-04-02 |
Tim King | Fixed the 32 bit vs. 64 bit problem in the rational... |
commit | commitdiff | tree |
2010-04-01 |
Christopher... | Changing min/maxArity to use metakind info. |
commit | commitdiff | tree |
2010-04-01 |
Christopher... | Parser tweaks to address review |
commit | commitdiff | tree |
2010-04-01 |
Christopher... | Adding newly generated files |
commit | commitdiff | tree |
2010-04-01 |
Christopher... | Removing Expr::operator=(uintptr_t n), as it's no longe... |
commit | commitdiff | tree |
2010-04-01 |
Morgan Deters | cvc4 --show-config now gives library version |
commit | commitdiff | tree |
2010-04-01 |
Morgan Deters | reran update-copyright.pl to get new contributors and... |
commit | commitdiff | tree |
next |