| 2012-08-24 |
Morgan Deters | * disallow internal uses of mkVar() (you have to mkSkol... |
blob | commitdiff | raw |
| 2012-07-31 |
Morgan Deters | Options merge. This commit: |
blob | commitdiff | raw | diff to current |
| 2012-07-12 |
Andrew Reynolds | merged fmf-devel branch, includes support for SMT2... |
blob | commitdiff | raw | diff to current |
| 2012-06-18 |
Andrew Reynolds | fixed smt version 1 parser for quantifiers |
blob | commitdiff | raw | diff to current |
| 2012-06-13 |
Morgan Deters | Don't use the "inlined" feature of ANTLR 3.2, which... |
blob | commitdiff | raw | diff to current |
| 2012-06-11 |
Morgan Deters | Merge from quantifiers2-trunkmerge branch. |
blob | commitdiff | raw | diff to current |
| 2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
blob | commitdiff | raw | diff to current |
| 2012-04-06 |
Morgan Deters | * Fix ITEs and functions in CVC language printer. |
blob | commitdiff | raw | diff to current |
| 2012-03-21 |
Morgan Deters | Disable nonclausal simplification for QF_SAT benchmarks... |
blob | commitdiff | raw | diff to current |
| 2012-03-09 |
Morgan Deters | fix a "lost command" bug and associated memory leak... |
blob | commitdiff | raw | diff to current |
| 2011-10-04 |
Morgan Deters | Oh, here's another cute compatibility fix for libantlr3... |
blob | commitdiff | raw | diff to current |
| 2011-09-02 |
Morgan Deters | Merge from my post-smtcomp branch. Includes: |
blob | commitdiff | raw | diff to current |
| 2011-06-30 |
Morgan Deters | Allow (- x) for unary minus in SMT-LIBv1, in addition... |
blob | commitdiff | raw | diff to current |
| 2011-05-02 |
Dejan Jovanović | parser fixes for bug 243 |
blob | commitdiff | raw | diff to current |
| 2011-05-02 |
Morgan Deters | Minor fixes to various parts of CVC4, including the... |
blob | commitdiff | raw | diff to current |
| 2011-04-23 |
Morgan Deters | * reviewed BooleanSimplification, added documentation... |
blob | commitdiff | raw | diff to current |
| 2011-04-20 |
Morgan Deters | Tuesday end-of-day commit. |
blob | commitdiff | raw | diff to current |
| 2011-04-18 |
Morgan Deters | Partial merge from datatypes-merge branch: |
blob | commitdiff | raw | diff to current |
| 2011-03-25 |
Morgan Deters | This is a merge from the "theoryfixes+cdattrhash" branc... |
blob | commitdiff | raw | diff to current |
| 2010-10-20 |
Christopher L. Conway | Fixing minor whitespace bug in the parser |
blob | commitdiff | raw | diff to current |
| 2010-10-12 |
Morgan Deters | Merge from cc-memout branch. Here are the main points |
blob | commitdiff | raw | diff to current |
| 2010-09-20 |
Dejan Jovanović | bitvector rewriting for the core theory and testcases |
blob | commitdiff | raw | diff to current |
| 2010-07-06 |
Morgan Deters | Fixes for doubled-statistics (bug 171), a fix to muzzle... |
blob | commitdiff | raw | diff to current |
| 2010-06-30 |
Morgan Deters | * theory "tree" rewriting implemented and works |
blob | commitdiff | raw | diff to current |
| 2010-06-14 |
Christopher L. Conway | Adding array select/store to SMT v1 and v2 parsers |
blob | commitdiff | raw | diff to current |
| 2010-06-04 |
Morgan Deters | ** Don't fear the files-changed list, almost all change... |
blob | commitdiff | raw | diff to current |
| 2010-06-04 |
Christopher L. Conway | Enabling RDL/IDL in SMT v1 and adding some simple tests |
blob | commitdiff | raw | diff to current |
| 2010-06-01 |
Christopher L. Conway | Fixing failing test in r521 |
blob | commitdiff | raw | diff to current |
| 2010-05-31 |
Christopher L. Conway | First draft implementation of mkAssociative |
blob | commitdiff | raw | diff to current |
| 2010-05-20 |
Tim King | Added the division symbol to the parser, and minimal... |
blob | commitdiff | raw | diff to current |
| 2010-05-02 |
Dejan Jovanović | smt parser for bit-vectors |
blob | commitdiff | raw | diff to current |
| 2010-05-01 |
Christopher L. Conway | Fixing private/public header warnings in parser library |
blob | commitdiff | raw | diff to current |
| 2010-04-29 |
Dejan Jovanović | Added the capability to construct expressions by passin... |
blob | commitdiff | raw | diff to current |
| 2010-04-29 |
Christopher L. Conway | (Not) Handling parameterized sorts in SMT v2 |
blob | commitdiff | raw | diff to current |
| 2010-04-29 |
Christopher L. Conway | First draft implementation of SMT v2 parser |
blob | commitdiff | raw | diff to current |
| 2010-04-28 |
Christopher L. Conway | SMT parser has to map 'Real' to RealType |
blob | commitdiff | raw | diff to current |
| 2010-04-28 |
Dejan Jovanović | Build fix for parser |
blob | commitdiff | raw | diff to current |
| 2010-04-28 |
Christopher L. Conway | Refactoring Input/Parser code to support external manip... |
blob | commitdiff | raw | diff to current |
| 2010-04-28 |
Tim King | Added theory/arith/kind and enabled the smt parser... |
blob | commitdiff | raw | diff to current |
| 2010-04-27 |
Christopher L. Conway | Adding Integer and Rational constants to SMT |
blob | commitdiff | raw | diff to current |
| 2010-04-27 |
Christopher L. Conway | Adding a bit of documentation to the SMT parser |
blob | commitdiff | raw | diff to current |
| 2010-04-14 |
Dejan Jovanović | Marging from types 404:415, changes: Massive |
blob | commitdiff | raw | diff to current |
| 2010-04-13 |
Christopher L. Conway | Merging from branches/decl-scopes (r401:411) |
blob | commitdiff | raw | diff to current |
| 2010-04-05 |
Christopher L. Conway | Minor refactorings, in response to code review (Bug... |
blob | commitdiff | raw | diff to current |
| 2010-04-02 |
Christopher L. Conway | Overriding ANTLR3 error recovery routine |
blob | commitdiff | raw | diff to current |
| 2010-04-01 |
Christopher L. Conway | Changing min/maxArity to use metakind info. |
blob | commitdiff | raw | diff to current |
| 2010-04-01 |
Christopher L. Conway | Parser tweaks to address review |
blob | commitdiff | raw | diff to current |
| 2010-04-01 |
Morgan Deters | reran update-copyright.pl to get new contributors and... |
blob | commitdiff | raw | diff to current |
| 2010-04-01 |
Morgan Deters | PARSER STUFF: |
blob | commitdiff | raw | diff to current |
| 2010-03-31 |
Christopher L. Conway | Fix bug in SMT-LIB with let/flet bindings |
blob | commitdiff | raw | diff to current |
| 2010-03-31 |
Christopher L. Conway | Finishing parser cleanup. Code is now review-ready. |
blob | commitdiff | raw | diff to current |
| 2010-03-31 |
Christopher L. Conway | More parser cleanup. Should fix problems with last... |
blob | commitdiff | raw | diff to current |
| 2010-03-31 |
Christopher L. Conway | Code cleanup in parser |
blob | commitdiff | raw | diff to current |
| 2010-03-30 |
Christopher L. Conway | Merging from branches/antlr3 (r246:354) |
blob | commitdiff | raw | diff to current |
|
projects / cvc5.git / history