| 2012-09-27 |
Morgan Deters | * Rename SMT parts (printer, parser) to SMT1 |
blob | commitdiff | raw |
| 2012-09-21 |
Morgan Deters | SMT-LIBv2 compliance updates: |
blob | commitdiff | raw | diff to current |
| 2012-09-15 |
Morgan Deters | minor interface improvements, compliance fixes |
blob | commitdiff | raw | diff to current |
| 2012-08-31 |
Andrew Reynolds | merge from fmf-devel branch. more updates to models... |
blob | commitdiff | raw | diff to current |
| 2012-08-24 |
Morgan Deters | * disallow internal uses of mkVar() (you have to mkSkol... |
blob | commitdiff | raw | diff to current |
| 2012-08-24 |
Morgan Deters | fix get-value output in a couple ways; this fixes bug... |
blob | commitdiff | raw | diff to current |
| 2012-07-31 |
Morgan Deters | Options merge. This commit: |
blob | commitdiff | raw | diff to current |
| 2012-07-27 |
Andrew Reynolds | merging fmf-devel branch, includes refactored datatype... |
blob | commitdiff | raw | diff to current |
| 2012-07-27 |
François Bobot | Merge quantifiers2-trunk: |
blob | commitdiff | raw | diff to current |
| 2012-07-18 |
Morgan Deters | more compliance fixes for SMT-LIBv2 |
blob | commitdiff | raw | diff to current |
| 2012-07-17 |
Morgan Deters | SMT-LIBv2 compliance updates: |
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-07-10 |
Dejan Jovanović | going back to 1. being a non decimal |
blob | commitdiff | raw | diff to current |
| 2012-07-10 |
Dejan Jovanović | small changes: |
blob | commitdiff | raw | diff to current |
| 2012-07-08 |
Morgan Deters | Bugs resolved by this commit: #314, #322, #359, #364... |
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-06-08 |
Morgan Deters | Fix SMT-LIBv2 ALL_SUPPORTED logic inference (by inferri... |
blob | commitdiff | raw | diff to current |
| 2012-06-07 |
Morgan Deters | LogicInfo locking implemented, and some initialization... |
blob | commitdiff | raw | diff to current |
| 2012-06-07 |
Morgan Deters | Adding EchoCommand and associated printer and parser... |
blob | commitdiff | raw | diff to current |
| 2012-05-15 |
Morgan Deters | removing all extended commands (as inspired by the... |
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-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minis... |
blob | commitdiff | raw | diff to current |
| 2012-01-17 |
Andrew Reynolds | updates to smt2 parser to support datatypes, minor... |
blob | commitdiff | raw | diff to current |
| 2011-11-16 |
Morgan Deters | Addressed many of the concerns raised in the public... |
blob | commitdiff | raw | diff to current |
| 2011-10-29 |
Morgan Deters | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF... |
blob | commitdiff | raw | diff to current |
| 2011-10-28 |
Morgan Deters | * ability to output NodeBuilders without first converti... |
blob | commitdiff | raw | diff to current |
| 2011-10-21 |
Morgan Deters | some printing and parser fixes for problems recently... |
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 |
Morgan Deters | Minor fixes to various parts of CVC4, including the... |
blob | commitdiff | raw | diff to current |
| 2011-05-01 |
Morgan Deters | minor fixes, plus experimental readline support in... |
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 | mostly CVC presentation language parsing and printing |
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-10 |
Morgan Deters | additional model gen and SMT-LIBv2 compliance work... |
blob | commitdiff | raw | diff to current |
| 2010-10-09 |
Morgan Deters | support for SMT-LIBv2 :named attributes, and attributes... |
blob | commitdiff | raw | diff to current |
| 2010-10-09 |
Morgan Deters | Model generation for arith, boolean, and uf theories via |
blob | commitdiff | raw | diff to current |
| 2010-10-08 |
Morgan Deters | * (define-fun...) now has proper type checking in non... |
blob | commitdiff | raw | diff to current |
| 2010-10-07 |
Morgan Deters | SMT-LIBv2 (define-fun...) command now functional; does... |
blob | commitdiff | raw | diff to current |
| 2010-10-06 |
Morgan Deters | declare-sort, define-sort working but not thoroughly... |
blob | commitdiff | raw | diff to current |
| 2010-10-05 |
Morgan Deters | parser and core support for SMT-LIBv2 commands get... |
blob | commitdiff | raw | diff to current |
| 2010-07-27 |
Christopher L. Conway | Moving EQ->IFF handling from TheoryEngine to parser... |
blob | commitdiff | raw | diff to current |
| 2010-07-08 |
Christopher L. Conway | Adding missing operators in SMT2 parser: UMINUS, DIVISI... |
blob | commitdiff | raw | diff to current |
| 2010-07-06 |
Christopher L. Conway | Adding Array types to SMT2 parser |
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 |
Christopher L. Conway | Parsing support for SMT divisions: LRA, QF_UFLIA, QF_UF... |
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-01 |
Christopher L. Conway | Adding SMT v2 parsing support for: QF_IDL, QF_NIA,... |
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-12 |
Christopher L. Conway | Adding ParserBuilder, reducing visibility of Parser... |
blob | commitdiff | raw | diff to current |
| 2010-05-12 |
Christopher L. Conway | true and false are only defined if the core theory... |
blob | commitdiff | raw | diff to current |
| 2010-05-12 |
Christopher L. Conway | Adding class Smt2 to handle declaration of logic and... |
blob | commitdiff | raw | diff to current |
| 2010-05-07 |
Christopher L. Conway | Tightening lexer rules for numerals in SMT v2 |
blob | commitdiff | raw | diff to current |
| 2010-05-06 |
Christopher L. Conway | Adding --strict-parsing option |
blob | commitdiff | raw | diff to current |
| 2010-05-06 |
Christopher L. Conway | Adding AntlrInput::tokenTextSubstr |
blob | commitdiff | raw | diff to current |
| 2010-05-06 |
Christopher L. Conway | Adding bit-vector constants in SMT2 |
blob | commitdiff | raw | diff to current |
| 2010-05-04 |
Christopher L. Conway | Minor change to SMT v2 grammar |
blob | commitdiff | raw | diff to current |
| 2010-05-04 |
Christopher L. Conway | Adding general support for SMT2 set-info command |
blob | commitdiff | raw | diff to current |
| 2010-05-04 |
Christopher L. Conway | Handling SMT 2.0 symbols and info flags |
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 |
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 |
|
projects / cvc5.git / history