summaryrefslogtreecommitdiff
path: root/src/parser/smt2
AgeCommit message (Expand)Author
2013-12-02Minor cleanup.Morgan Deters
2013-11-11Expanded usefulness of (set-info :cvc4-logic ...)Morgan Deters
2013-10-20adds regular expression rangeTianyi Liang
2013-10-01adds partial function substr. the use of this function should be guarded, esp...Tianyi Liang
2013-10-01Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535Andrew Reynolds
2013-09-27removes unsound cases, adds unrollingTianyi Liang
2013-09-27for morgan to see the regression problemsTianyi Liang
2013-09-18Support for bv2nat/int2bv in parser and BV rewriter.Morgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-09-11Theory of strings.Tianyi Liang
2013-09-09Add support for check-sat with argument.Morgan Deters
2013-09-09Support per-command verbosity settings.Morgan Deters
2013-09-05Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a se...Morgan Deters
2013-07-11Support for TPTP's TFF0 (with arithmetic)Morgan Deters
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback