Age | Commit message (Collapse) | Author | |
---|---|---|---|
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 | |
2013-05-29 | Merge branch '1.2.x' | Morgan Deters | |
2013-05-29 | Per SMT-LIB spec, allow (set-info..) command to succeed implicitly with ↵ | Morgan Deters | |
unknown key. | |||
2013-05-29 | SMT-LIB printer updates (some missing cases). | 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-23 | Refactoring to prepare for MBQI with integer quantification. Minor bug fixes. | Andrew Reynolds | |
2013-05-22 | Merge branch 'master' of https://github.com/CVC4/CVC4 | Andrew Reynolds | |
Conflicts: src/theory/arith/theory_arith_private.cpp src/theory/quantifiers_engine.cpp | |||
2013-05-22 | Significant work on bounded integer quantification to handle non-trivial ↵ | Andrew Reynolds | |
bounds. Refactoring of InstConstantAttribute to be internal to TermDb. | |||
2013-05-22 | Add regressions for finite model finding | Andrew Reynolds | |