Age | Commit message (Collapse) | Author | |
---|---|---|---|
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-11 | Fix for Boolean-term rewriting and LAMBDAs | Morgan Deters | |
2013-07-09 | Fix for bug 519; don't involve ITESimplifier in model generation. | Morgan Deters | |
2013-07-09 | add relevant domain computation | Andrew Reynolds | |
2013-07-06 | Model output is now const; this related to bug 519 | Morgan Deters | |
2013-07-05 | Fix for a datatype parsing bug that Tim found. | Morgan Deters | |
2013-07-02 | Make uf strong solver user-context dependent, fixes bug 522. | Andrew Reynolds | |
2013-07-02 | Minor fixes for bounded integers, rewrite engine. | Andrew Reynolds | |
2013-06-28 | More bug fixes for interval models. | Andrew Reynolds | |
2013-06-28 | Fix portfolio builds after yesterday's commits. | Morgan Deters | |
2013-06-27 | Better check-models output for some kinds of problems; add anassertion that ↵ | Morgan Deters | |
the master equality engine is consistent when it needs to be. This is intended to help root out some recent model-generation bugs. | |||
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 | Small fix for IS_INTEGER. | Morgan Deters | |
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-27 | Better user documentation for mkVar() and mkBoundVar(). | Morgan Deters | |
Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list. | |||
2013-06-27 | Minor printer cleanup for SMT-LIBv2 symbols "div" and "mod". | Morgan Deters | |
Thanks to Alex Horn for raising the issue on the CVC-BUGS mailing list. | |||
2013-06-26 | Add support for interval models in bounded integers MBQI (in progress). | Andrew Reynolds | |
2013-06-25 | Merge branch '1.2.x' | Morgan Deters | |
2013-06-25 | Proposed fix for bug #513 | Morgan Deters | |
2013-06-25 | Refactoring of model engine to separate individual implementations of model ↵ | Andrew Reynolds | |
builder. Begin work on interval models for integers. Other minor cleanup. | |||
2013-06-24 | Add files missing from last commit | Morgan Deters | |
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-24 | Add options for symmetry breaking in uf+ss totality axiom approach, option ↵ | Andrew Reynolds | |
for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine | |||
2013-06-21 | Fix failure in non-assertion builds on incorrect SmtEngine use. | Morgan Deters | |
2013-06-19 | Merge branch '1.2.x' | Morgan Deters | |
2013-06-19 | Workaround for suspected clang 3.0 codegen bug on Mac | Morgan Deters | |
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-17 | Java streams example I forgot to add a long time ago | Morgan Deters | |
2013-06-17 | Make --var-elim-quant true by default. Add rewrite engine to quantifiers ↵ | Andrew Reynolds | |
module. | |||
2013-06-15 | Fix in SMT2 parser for parametric datatypes | Andrew Reynolds | |
2013-06-09 | another fix for array-store-all printing | Morgan Deters | |
2013-06-09 | Better array-store-all output for SMT-LIB. | Morgan Deters | |
2013-06-08 | Fix typos in alttheoryskel | Morgan Deters | |
2013-06-08 | Fixes for Boolean terms in arrays (including fix for bug 517). | Morgan Deters | |
2013-06-07 | One more case for arrays of Boolean. | Morgan Deters | |
2013-06-07 | Fix for bug 517. | Morgan Deters | |
2013-06-07 | Allow disabling include-file feature | Morgan Deters | |
2013-06-06 | small parese issue in IDL | Dejan Jovanović | |
2013-06-06 | typo | Dejan Jovanović | |
2013-06-06 | IDL example theory (to be used with --use-theory=idl). | Dejan Jovanović | |
2013-06-05 | Fix bug in --fmf-fmc for producing models of functions not appearing in ↵ | Andrew Reynolds | |
quantified formulas. | |||
2013-06-04 | File inclusion in Smt2 parser. | Morgan Deters | |
The extended command (include-file "filename") now includes file content. | |||
2013-06-04 | Add --no-condense-function-values option for explicit function models ↵ | Morgan Deters | |
(useful in some applications) | |||
2013-06-04 | Merge branch '1.2.x' | Morgan Deters | |
2013-06-04 | Fix clang static initialization order issue; fixes bug 512. | Morgan Deters | |
2013-06-04 | Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant ↵ | Andrew Reynolds | |
bounds for bounded integers. | |||
2013-06-03 | Merge tag 'casc24' | Morgan Deters | |
2013-06-03 | Updated CASC scripts, as provided to Geoff Sutcliffecasc24 | Morgan Deters | |