summaryrefslogtreecommitdiff
path: root/src/parser
AgeCommit message (Collapse)Author
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-02Minor cleanup.Morgan Deters
2013-11-14Allow empty record literals (fixing an oversight in previous work on empty ↵Morgan Deters
tuples/records)
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, ↵Tianyi Liang
especially for disequalities
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
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
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 ↵Morgan Deters
segfault in smt2 printer
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
This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases.
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 ↵Morgan Deters
users' space. Specifically, output.h was moved to CVC4's "private-library" rules, which means that it's not installed on users' machines, and public headers should not include it. Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
2013-06-27Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_public.h so that they ↵Morgan Deters
don't escape to user space Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list.
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk ↵Morgan Deters
allows linearization of div,mod,/ by a constant.
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
Indeed, "-1" is a valid user symbol in SMT-LIB; this commit makes a small change to the parser to detect when something like "-1" is used but undeclared, and adds a note to the error message giving the syntax for unary minus.
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
The extended command (include-file "filename") now includes file content.
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 ↵Morgan Deters
division
2013-05-28Standardize SMT-LIBv2 set of logics to use LogicInfo.Morgan Deters
Previously, SMT-LIB logics were treated specially, as in SMT-LIB v1.2. This led to inconsistencies---such as nonstandard logics like "QF_LIRA" being accepted in set-logic but not providing the "Real" sort. Now, the LogicInfo is used and queried, so nonstandard logics should work fine and declare the correct symbols. SMT-LIB v1.2, unfortunately, can't take advantage of this fully since symbols like "Array" have substantially different meanings in different logics.
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
Conflicts: library_versions src/parser/parser.h
2013-05-20Detect multiply-defined :named annotations and issue an error.Morgan Deters
Thanks to David Cok for pointing out this issue. Conflicts: library_versions
2013-05-20Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive ↵Morgan Deters
mode. Thanks to David Cok for raising this issue.
2013-05-20Compliance fixes for :named annotations: they must name closed subterms, the ↵Morgan Deters
names must be user-permitted names, etc. Thanks to David Cok for raising this issue.
2013-05-20As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => ↵Morgan Deters
takes n>2 args and is right-assoc. Thanks to David Cok for pointing out this issue.
2013-05-20Better error on illegal (pop N); also more compliant SMT-LIB error messages ↵Morgan Deters
in some places Thanks to David Cok for reporting these issues.
2013-05-20Disallow construction of (_ BitVec 0).Morgan Deters
Thanks to David Cok for reporting this issue.
2013-05-20Fixed "success" response to (push N) / (pop N) with N > 1.Morgan Deters
Thanks to David Cok for reporting this issue.
2013-05-17As per SMT-LIB standard: make - and xor take n>2 args and be left-assoc; => ↵Morgan Deters
takes n>2 args and is right-assoc. Thanks to David Cok for pointing out this issue.
2013-05-17Better error on illegal (pop N); also more compliant SMT-LIB error messages ↵Morgan Deters
in some places Thanks to David Cok for reporting these issues.
2013-05-17Disallow construction of (_ BitVec 0).Morgan Deters
Thanks to David Cok for reporting this issue.
2013-05-17Fixed "success" response to (push N) / (pop N) with N > 1.Morgan Deters
Thanks to David Cok for reporting this issue.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback