summaryrefslogtreecommitdiff
path: root/src/parser
AgeCommit message (Expand)Author
2013-11-14Allow empty record literals (fixing an oversight in previous work on empty tu...Morgan Deters
2013-11-11Expanded usefulness of (set-info :cvc4-logic ...)Morgan Deters
2013-11-07Flatten libcvc4 build structure; remove some #include interdependencesMorgan 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-09Fix declare-datatypes dumping bug (bug 385).Morgan Deters
2013-09-09Support per-command verbosity settings.Morgan Deters
2013-09-09Support empty (and 1-ary) tuples and records.Morgan Deters
2013-09-05Fix FLOOR and DISTINCT in CVC language parser.Morgan Deters
2013-09-05Fix lambda handling in CVC parserMorgan Deters
2013-09-05Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a se...Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-11Remove auto-aritization from TPTP parserMorgan 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-27Remove output.h from public space, to avoid clashes with symbols defined in u...Morgan Deters
2013-06-27Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they don'...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-29Merge branch '1.2.x'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-21Merge branch '1.2.x'Morgan Deters
2013-05-21Fix an error that valgrind found.Morgan Deters
2013-05-20Merge branch '1.2.x'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-05-17As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => t...Morgan Deters
2013-05-17Better error on illegal (pop N); also more compliant SMT-LIB error messages i...Morgan Deters
2013-05-17Disallow construction of (_ BitVec 0).Morgan Deters
2013-05-17Fixed "success" response to (push N) / (pop N) with N > 1.Morgan Deters
2013-05-10Update casc run script. Work on compliance for SZS output.Andrew Reynolds
2013-04-22add bit0 and bit1 constants to smt-lib v1 parserMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback