Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-12-02 | Minor cleanup. | Morgan Deters | |
2013-11-14 | Allow empty record literals (fixing an oversight in previous work on empty ↵ | Morgan Deters | |
tuples/records) | |||
2013-11-11 | Expanded usefulness of (set-info :cvc4-logic ...) | Morgan Deters | |
2013-11-07 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters | |
2013-10-20 | adds regular expression range | Tianyi Liang | |
2013-10-01 | adds partial function substr. the use of this function should be guarded, ↵ | Tianyi Liang | |
especially for disequalities | |||
2013-10-01 | Fix a bug in smt2 parser for quantified formulas with attributes, fixes bug 535 | Andrew Reynolds | |
2013-09-27 | removes unsound cases, adds unrolling | Tianyi Liang | |
2013-09-27 | for morgan to see the regression problems | Tianyi Liang | |
2013-09-18 | Support for bv2nat/int2bv in parser and BV rewriter. | Morgan Deters | |
2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters | |
2013-09-11 | Theory of strings. | Tianyi Liang | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2013-09-09 | Add support for check-sat with argument. | Morgan Deters | |
2013-09-09 | Fix declare-datatypes dumping bug (bug 385). | Morgan Deters | |
2013-09-09 | Support per-command verbosity settings. | Morgan Deters | |
2013-09-09 | Support empty (and 1-ary) tuples and records. | Morgan Deters | |
2013-09-05 | Fix FLOOR and DISTINCT in CVC language parser. | Morgan Deters | |
2013-09-05 | Fix lambda handling in CVC parser | Morgan Deters | |
2013-09-05 | Fix declare-fun/define-fun in dumps; resolves bugs 408 and 385; also fix a ↵ | Morgan Deters | |
segfault in smt2 printer | |||
2013-07-29 | Fix numerous compiler warnings on various platforms | Morgan Deters | |
2013-07-11 | Remove auto-aritization from TPTP parser | Morgan Deters | |
2013-07-11 | Support 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-05 | Fix for a datatype parsing bug that Tim found. | Morgan Deters | |
2013-06-27 | Fix minor warnings found by recent clang/gcc. | Morgan Deters | |
2013-06-27 | Remove 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-27 | Remove 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-24 | Support 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-19 | Fix to the "include" extended feature of the SMT-LIB parser | Morgan Deters | |
2013-06-19 | Give 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-15 | Fix in SMT2 parser for parametric datatypes | Andrew Reynolds | |
2013-06-07 | Allow disabling include-file feature | Morgan Deters | |
2013-06-04 | File inclusion in Smt2 parser. | Morgan Deters | |
The extended command (include-file "filename") now includes file content. | |||
2013-05-29 | Merge branch '1.2.x' | Morgan Deters | |
2013-05-29 | Fix bug where strict mode didn't allow DIV or MOD, and Ints permitted real ↵ | Morgan Deters | |
division | |||
2013-05-28 | Standardize 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-21 | Merge branch '1.2.x' | Morgan Deters | |
2013-05-21 | Fix an error that valgrind found. | Morgan Deters | |
2013-05-20 | Merge branch '1.2.x' | Morgan Deters | |
Conflicts: library_versions src/parser/parser.h | |||
2013-05-20 | Detect multiply-defined :named annotations and issue an error. | Morgan Deters | |
Thanks to David Cok for pointing out this issue. Conflicts: library_versions | |||
2013-05-20 | Fix parsing of SMT-LIBv2 |quoted| symbols that span newlines in interactive ↵ | Morgan Deters | |
mode. Thanks to David Cok for raising this issue. | |||
2013-05-20 | Compliance 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-20 | As 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-20 | Better 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-20 | Disallow construction of (_ BitVec 0). | Morgan Deters | |
Thanks to David Cok for reporting this issue. | |||
2013-05-20 | Fixed "success" response to (push N) / (pop N) with N > 1. | Morgan Deters | |
Thanks to David Cok for reporting this issue. | |||
2013-05-17 | As 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-17 | Better 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-17 | Disallow construction of (_ BitVec 0). | Morgan Deters | |
Thanks to David Cok for reporting this issue. | |||
2013-05-17 | Fixed "success" response to (push N) / (pop N) with N > 1. | Morgan Deters | |
Thanks to David Cok for reporting this issue. | |||
2013-05-10 | Update casc run script. Work on compliance for SZS output. | Andrew Reynolds | |