summaryrefslogtreecommitdiff
path: root/src/parser/smt2
AgeCommit message (Expand)Author
2013-07-05Fix for a datatype parsing bug that Tim found.Morgan Deters
2013-06-27Fix minor warnings found by recent clang/gcc.Morgan Deters
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
2013-06-19Fix to the "include" extended feature of the SMT-LIB parserMorgan Deters
2013-06-19Give a more useful parse error message for "undeclared variable -1".Morgan Deters
2013-06-15Fix in SMT2 parser for parametric datatypesAndrew Reynolds
2013-06-07Allow disabling include-file featureMorgan Deters
2013-06-04File inclusion in Smt2 parser.Morgan Deters
2013-05-29Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real di...Morgan Deters
2013-05-28Standardize SMT-LIBv2 set of logics to use LogicInfo.Morgan Deters
2013-05-20Detect multiply-defined :named annotations and issue an error.Morgan Deters
2013-05-20Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive m...Morgan Deters
2013-05-20Compliance fixes for :named annotations: they must name closed subterms, the ...Morgan Deters
2013-05-20As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => t...Morgan Deters
2013-05-20Better error on illegal (pop N); also more compliant SMT-LIB error messages i...Morgan Deters
2013-05-20Disallow construction of (_ BitVec 0).Morgan Deters
2013-05-20Fixed "success" response to (push N) / (pop N) with N > 1.Morgan Deters
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-26Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javacMorgan Deters
2013-03-21Add the ability to "mute" commands, needed for SMT-LIB compliance.Morgan Deters
2013-03-21Some model and printing fixes for defined functions in input.Morgan Deters
2013-03-19Minor fixes to build systemMorgan Deters
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds an...Morgan Deters
2013-03-08Disallow overflow in bitvector literals (parser only)Morgan Deters
2013-02-16Some cleanup and copyright updatingMorgan Deters
2012-12-11Ignore unknown term annotations (giving a warning). Resolves bug 479.Morgan Deters
2012-11-30fix the syntax of assert-rewrite/-propagation/-reduction by putting the patte...François Bobot
2012-11-08added support for parametric datatypes in smt2 parser, includes support for '...Andrew Reynolds
2012-10-22fix parser generation in distributed tarballs (should fix bug #427)Morgan Deters
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-10Abstract values for SMT-LIB.Morgan Deters
2012-10-09* make Model class private (as discussed at meeting today)Morgan Deters
2012-10-08fix SMT-LIBv2 compliance mode for bitvectors (was completely broken; didn't a...Morgan Deters
2012-10-06* Fix some regressions' expected outputs.Morgan Deters
2012-10-05Bug-related:Morgan Deters
2012-10-02* re-enable some Z3 extended commands:Morgan Deters
2012-09-28Public interface review items:Morgan Deters
2012-09-27* Rename SMT parts (printer, parser) to SMT1Morgan Deters
2012-09-21SMT-LIBv2 compliance updates:Morgan Deters
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-09-15minor interface improvements, compliance fixesMorgan Deters
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-08-24* disallow internal uses of mkVar() (you have to mkSkolem())Morgan Deters
2012-08-24fix get-value output in a couple ways; this fixes bug #378Morgan Deters
2012-08-16The SmtEngine now ensures that setLogicInternal() is called even if there is ...Morgan Deters
2012-08-03better parser makefile fixMorgan Deters
2012-08-02fixes to paths in parser makefiles; if you've noticed strange SMT2 parser beh...Morgan Deters
2012-08-01fixes to some *clean targetsMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback