| 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 |
| 2010-04-01 |
Morgan Deters | * Minor code formatting stuff in src/expr/type.{h,cpp... |
commit | commitdiff | tree |
| 2010-04-01 |
Morgan Deters | minor forgotten things in last commit |
commit | commitdiff | tree |
| 2010-04-01 |
Morgan Deters | PARSER STUFF: |
commit | commitdiff | tree |
| 2010-04-01 |
Christopher... | Adding check for --disable-shared on --enable-coverage |
commit | commitdiff | tree |
| 2010-03-31 |
Christopher... | Fix bug in SMT-LIB with let/flet bindings |
commit | commitdiff | tree |
| 2010-03-31 |
Christopher... | Finishing parser cleanup. Code is now review-ready. |
commit | commitdiff | tree |
| 2010-03-31 |
Christopher... | More parser cleanup. Should fix problems with last... |
commit | commitdiff | tree |
| 2010-03-31 |
Christopher... | Code cleanup in parser |
commit | commitdiff | tree |
| 2010-03-31 |
Christopher... | Adding 'generated/' to .gitignore |
commit | commitdiff | tree |
| 2010-03-30 |
Christopher... | Removing unnecessary .gitignores |
commit | commitdiff | tree |
| 2010-03-30 |
Christopher... | Merging from branches/antlr3 (r246:354) |
commit | commitdiff | tree |
| 2010-03-30 |
Morgan Deters | again, re-enabling integer/rational tests (though they... |
commit | commitdiff | tree |
| 2010-03-30 |
Morgan Deters | I think this finishes off the CDMap<>/Attribute leaks |
commit | commitdiff | tree |
| 2010-03-30 |
Morgan Deters | fixing mistaken commit to unit test Makefile.am which... |
commit | commitdiff | tree |
| 2010-03-30 |
Morgan Deters | Highlights of this commit are: |
commit | commitdiff | tree |
| 2010-03-28 |
Tim King | Improved the documentation and testing for Rational. |
commit | commitdiff | tree |
| 2010-03-28 |
Christopher... | Rm'ing test file (sorry for spam) |
commit | commitdiff | tree |
| 2010-03-28 |
Christopher... | Adding test file |
commit | commitdiff | tree |
| 2010-03-26 |
Tim King | Added GMP backed Rational and Integer classes, and... |
commit | commitdiff | tree |
| 2010-03-25 |
Christopher... | Merging let/flet rules in SMT parser |
commit | commitdiff | tree |
| 2010-03-25 |
Christopher... | Adding comments to NodeManager |
commit | commitdiff | tree |
| 2010-03-25 |
Morgan Deters | new domain-specific language for kinds files: permits... |
commit | commitdiff | tree |
| 2010-03-23 |
Clark Barrett | Documented that ContextObj::destroy() only restores... |
commit | commitdiff | tree |
| 2010-03-23 |
Tim King | Fixed some memory cleanup and destruction issues with... |
commit | commitdiff | tree |
| 2010-03-16 |
Morgan Deters | * test/unit/Makefile.am, test/unit/expr/attribute_white.h, |
commit | commitdiff | tree |
| 2010-03-15 |
Morgan Deters | This checkin resolves bug #57. |
commit | commitdiff | tree |
| 2010-03-14 |
Morgan Deters | * test/unit/context/context_black.h: added a test for... |
commit | commitdiff | tree |
| 2010-03-13 |
Clark Barrett | Fix for bug 45 |
commit | commitdiff | tree |
| 2010-03-12 |
Morgan Deters | * src/context/cdmap.h: rename orderedIterator to iterat... |
commit | commitdiff | tree |
| 2010-03-12 |
Dejan Jovanović | Fixing unnecessary construction of NOT nodes when... |
commit | commitdiff | tree |
| 2010-03-12 |
Morgan Deters | * Added shutdown() functions to SmtEngine, TheoryEngine... |
commit | commitdiff | tree |
| 2010-03-11 |
Morgan Deters | naive rewriting to fix minisat invariant; rewrite ... |
commit | commitdiff | tree |
| 2010-03-11 |
Dejan Jovanović | Changing const TNode& to TNode in the CNF conversion... |
commit | commitdiff | tree |
| 2010-03-11 |
Tim King | Added some hand generated UF tests. Unfortunartely... |
commit | commitdiff | tree |
| 2010-03-11 |
Dejan Jovanović | Boolean variables were marked as theory literals by... |
commit | commitdiff | tree |
| 2010-03-11 |
Dejan Jovanović | Fix for the main bug that was bugging me -- Bug 49... |
commit | commitdiff | tree |
| 2010-03-10 |
Morgan Deters | fix production-build unit testing errors (they assumed... |
commit | commitdiff | tree |
| 2010-03-10 |
Christopher... | Lexical scoping for let-bound variables (Bug #53) |
commit | commitdiff | tree |
| 2010-03-10 |
Christopher... | Adding preliminary let/flet support to SMT parser ... |
commit | commitdiff | tree |
| 2010-03-09 |
Christopher... | Adding support for "distinct" builtin in SMT parser |
commit | commitdiff | tree |
| 2010-03-09 |
Christopher... | Adding support for sort U in QF_UF. |
commit | commitdiff | tree |
| 2010-03-09 |
Dejan Jovanović | Adding the smallest of test cases from the smtlib. |
commit | commitdiff | tree |
| 2010-03-09 |
Dejan Jovanović | removing makefile.in |
commit | commitdiff | tree |
| 2010-03-09 |
Tim King | Fixed non-debug build problems |
commit | commitdiff | tree |
| 2010-03-09 |
Dejan Jovanović | one more simple test for uf |
commit | commitdiff | tree |
| 2010-03-09 |
Dejan Jovanović | (no commit message) |
commit | commitdiff | tree |
| 2010-03-08 |
Morgan Deters | This fixes regressions at levels >= 1 which were failing |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog