summaryrefslogtreecommitdiff
path: root/src/parser/smt/Smt.g
AgeCommit message (Expand)Author
2012-09-27* Rename SMT parts (printer, parser) to SMT1Morgan Deters
2012-08-24* disallow internal uses of mkVar() (you have to mkSkolem())Morgan Deters
2012-07-31Options merge. This commit:Morgan Deters
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
2012-06-18fixed smt version 1 parser for quantifiersAndrew Reynolds
2012-06-13Don't use the "inlined" feature of ANTLR 3.2, which causes a buffer overflow ...Morgan Deters
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
2012-04-11merge from arrays-clark branchMorgan Deters
2012-04-06* Fix ITEs and functions in CVC language printer.Morgan Deters
2012-03-21Disable nonclausal simplification for QF_SAT benchmarks by default.Morgan Deters
2012-03-09fix a "lost command" bug and associated memory leak in SMT-LIBv1 parser due t...Morgan Deters
2011-10-04Oh, here's another cute compatibility fix for libantlr3c 3.4-beta4. They #de...Morgan Deters
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
2011-06-30Allow (- x) for unary minus in SMT-LIBv1, in addition to the standard (~ x),Morgan Deters
2011-05-02parser fixes for bug 243Dejan Jovanović
2011-05-02Minor fixes to various parts of CVC4, including the removal of the uintptr_t ...Morgan Deters
2011-04-23* reviewed BooleanSimplification, added documentation & unit testMorgan Deters
2011-04-20Tuesday end-of-day commit.Morgan Deters
2011-04-18Partial merge from datatypes-merge branch:Morgan Deters
2011-03-25This is a merge from the "theoryfixes+cdattrhash" branch. The changesMorgan Deters
2010-10-20Fixing minor whitespace bug in the parserChristopher L. Conway
2010-10-12Merge from cc-memout branch. Here are the main pointsMorgan Deters
2010-09-20bitvector rewriting for the core theory and testcasesDejan Jovanović
2010-07-06Fixes for doubled-statistics (bug 171), a fix to muzzled builds and some mino...Morgan Deters
2010-06-30* theory "tree" rewriting implemented and worksMorgan Deters
2010-06-14Adding array select/store to SMT v1 and v2 parsersChristopher L. Conway
2010-06-04** Don't fear the files-changed list, almost all changes are in the **Morgan Deters
2010-06-04Enabling RDL/IDL in SMT v1 and adding some simple testsChristopher L. Conway
2010-06-01Fixing failing test in r521Christopher L. Conway
2010-05-31First draft implementation of mkAssociativeChristopher L. Conway
2010-05-20Added the division symbol to the parser, and minimal support for it in Theory...Tim King
2010-05-02smt parser for bit-vectorsDejan Jovanović
2010-05-01Fixing private/public header warnings in parser libraryChristopher L. Conway
2010-04-29Added the capability to construct expressions by passing the operator instead...Dejan Jovanović
2010-04-29(Not) Handling parameterized sorts in SMT v2Christopher L. Conway
2010-04-29First draft implementation of SMT v2 parserChristopher L. Conway
2010-04-28SMT parser has to map 'Real' to RealTypeChristopher L. Conway
2010-04-28Build fix for parserDejan Jovanović
2010-04-28Refactoring Input/Parser code to support external manipulation of the parser ...Christopher L. Conway
2010-04-28Added theory/arith/kind and enabled the smt parser to read in these symbols. ...Tim King
2010-04-27Adding Integer and Rational constants to SMTChristopher L. Conway
2010-04-27Adding a bit of documentation to the SMT parserChristopher L. Conway
2010-04-14Marging from types 404:415, changes: MassiveDejan Jovanović
2010-04-13Merging from branches/decl-scopes (r401:411)Christopher L. Conway
2010-04-05Minor refactorings, in response to code review (Bug #73)Christopher L. Conway
2010-04-02Overriding ANTLR3 error recovery routineChristopher L. Conway
2010-04-01Changing min/maxArity to use metakind info.Christopher L. Conway
2010-04-01Parser tweaks to address reviewChristopher L. Conway
2010-04-01reran update-copyright.pl to get new contributors and add new header comments...Morgan Deters
2010-04-01PARSER STUFF:Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback