| 2013-09-05 |
Morgan Deters | Fix bugs/issues with missed-t-prop dump output |
commit | commitdiff | tree |
| 2013-09-05 |
Morgan Deters | Fix declare-fun/define-fun in dumps; resolves bugs... |
commit | commitdiff | tree |
| 2013-08-31 |
Morgan Deters | Add ability to mkConst(TupleSelect) and friends in... |
commit | commitdiff | tree |
| 2013-08-26 |
Kshitij Bansal | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-08-26 |
Kshitij Bansal | bug 374 fix: assert litVal=desiredVal only for leaf... |
commit | commitdiff | tree |
| 2013-08-26 |
Kshitij Bansal | Bug 374 benchmarks |
commit | commitdiff | tree |
| 2013-08-20 |
Morgan Deters | Change recursive expandDefinitions() to an interative... |
commit | commitdiff | tree |
| 2013-08-13 |
Morgan Deters | --segv-nospin is now default. |
commit | commitdiff | tree |
| 2013-08-13 |
Morgan Deters | Minor cleanup. |
commit | commitdiff | tree |
| 2013-08-13 |
Andrew Reynolds | Minor fixes for --fmf-fmc for quantifiers containing... |
commit | commitdiff | tree |
| 2013-08-13 |
Andrew Reynolds | initial modifications for per-ic cbqi |
commit | commitdiff | tree |
| 2013-08-09 |
Morgan Deters | Clean up "make install"-produced intermediate files... |
commit | commitdiff | tree |
| 2013-08-08 |
Morgan Deters | Fix a serious bug in the preprocessor; problem inputs... |
commit | commitdiff | tree |
| 2013-08-08 |
Morgan Deters | Parameterized, uninterpreted sorts need no Boolean... |
commit | commitdiff | tree |
| 2013-07-30 |
Morgan Deters | Minor fixes to build system. |
commit | commitdiff | tree |
| 2013-07-29 |
Morgan Deters | Fix numerous compiler warnings on various platforms |
commit | commitdiff | tree |
| 2013-07-24 |
Morgan Deters | Regressions now checking models on unknown too. But... |
commit | commitdiff | tree |
| 2013-07-24 |
Morgan Deters | Fixes for building with mingw win64. |
commit | commitdiff | tree |
| 2013-07-24 |
Morgan Deters | Don't allow --stats if not a statistics-enabled build |
commit | commitdiff | tree |
| 2013-07-24 |
Morgan Deters | some portfolio driver cleanup |
commit | commitdiff | tree |
| 2013-07-24 |
Morgan Deters | Some fixes for (get-info :all-options) |
commit | commitdiff | tree |
| 2013-07-23 |
Morgan Deters | fix for win32 option parsing via mingw32 |
commit | commitdiff | tree |
| 2013-07-23 |
Morgan Deters | (get-info :all-options) to get option values; also... |
commit | commitdiff | tree |
| 2013-07-22 |
Morgan Deters | Allow BV and DT in either order in the logic string |
commit | commitdiff | tree |
| 2013-07-22 |
Andrew Reynolds | Add option --cbqi-recurse. |
commit | commitdiff | tree |
| 2013-07-22 |
Andrew Reynolds | Bug fix for --fmf-fmc for non-uninterpreted sort quanti... |
commit | commitdiff | tree |
| 2013-07-20 |
Morgan Deters | enable bug521 regression tests |
commit | commitdiff | tree |
| 2013-07-19 |
Dejan Jovanovic | possible fix for bug 521 |
commit | commitdiff | tree |
| 2013-07-19 |
Morgan Deters | Minor fix for --no-condense-function-values |
commit | commitdiff | tree |
| 2013-07-18 |
Andrew Reynolds | Fix quantifier instantiation bug in cbqi, add default... |
commit | commitdiff | tree |
| 2013-07-17 |
Morgan Deters | Fix bug 516; include some bug testcases. |
commit | commitdiff | tree |
| 2013-07-16 |
Liana Hadarean | fixed seg fault when bv equality is turned off |
commit | commitdiff | tree |
| 2013-07-16 |
Liana Hadarean | fixed bug520 |
commit | commitdiff | tree |
| 2013-07-16 |
Morgan Deters | Fix for get-antlr script and PIC/non-PIC objects, on... |
commit | commitdiff | tree |
| 2013-07-16 |
Morgan Deters | "Tabular"-style function definitions in models with... |
commit | commitdiff | tree |
| 2013-07-16 |
Morgan Deters | Minor bugfixes to model-building |
commit | commitdiff | tree |
| 2013-07-13 |
Morgan Deters | Remove now-unused language bindings interface file. |
commit | commitdiff | tree |
| 2013-07-13 |
Morgan Deters | Fix language bindings and portfolio builds. |
commit | commitdiff | tree |
| 2013-07-12 |
Morgan Deters | Fix for curious GCC 4.8 translation with -O. |
commit | commitdiff | tree |
| 2013-07-11 |
Morgan Deters | Remove auto-aritization from TPTP parser |
commit | commitdiff | tree |
| 2013-07-11 |
Morgan Deters | Support for TPTP's TFF0 (with arithmetic) |
commit | commitdiff | tree |
| 2013-07-11 |
Morgan Deters | Fix for Boolean-term rewriting and LAMBDAs |
commit | commitdiff | tree |
| 2013-07-10 |
Morgan Deters | Fix for bug 519; don't involve ITESimplifier in model... |
commit | commitdiff | tree |
| 2013-07-09 |
Andrew Reynolds | add relevant domain computation |
commit | commitdiff | tree |
| 2013-07-07 |
Morgan Deters | Model output is now const; this related to bug 519 |
commit | commitdiff | tree |
| 2013-07-05 |
Morgan Deters | Fix for a datatype parsing bug that Tim found. |
commit | commitdiff | tree |
| 2013-07-02 |
Andrew Reynolds | Make uf strong solver user-context dependent, fixes... |
commit | commitdiff | tree |
| 2013-07-02 |
Andrew Reynolds | Minor fixes for bounded integers, rewrite engine. |
commit | commitdiff | tree |
| 2013-06-28 |
Andrew Reynolds | More bug fixes for interval models. |
commit | commitdiff | tree |
| 2013-06-28 |
Morgan Deters | Fix portfolio builds after yesterday's commits. |
commit | commitdiff | tree |
| 2013-06-27 |
Morgan Deters | Better check-models output for some kinds of problems... |
commit | commitdiff | tree |
| 2013-06-27 |
Morgan Deters | Fix minor warnings found by recent clang/gcc. |
commit | commitdiff | tree |
| 2013-06-27 |
Morgan Deters | Remove output.h from public space, to avoid clashes... |
commit | commitdiff | tree |
| 2013-06-27 |
Morgan Deters | Small fix for IS_INTEGER. |
commit | commitdiff | tree |
| 2013-06-27 |
Morgan Deters | Remove macros EXPECT_TRUE / EXPECT_FALSE from cvc4_publ... |
commit | commitdiff | tree |
| 2013-06-27 |
Morgan Deters | Better user documentation for mkVar() and mkBoundVar(). |
commit | commitdiff | tree |
| 2013-06-27 |
Morgan Deters | Minor printer cleanup for SMT-LIBv2 symbols "div" and... |
commit | commitdiff | tree |
| 2013-06-26 |
Andrew Reynolds | Add support for interval models in bounded integers... |
commit | commitdiff | tree |
| 2013-06-25 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-06-25 |
Morgan Deters | Proposed fix for bug #513 |
commit | commitdiff | tree |
| 2013-06-25 |
Andrew Reynolds | Refactoring of model engine to separate individual... |
commit | commitdiff | tree |
| 2013-06-25 |
Morgan Deters | Add files missing from last commit |
commit | commitdiff | tree |
| 2013-06-25 |
Morgan Deters | Support for abs, to_int, is_int, divisible in SMT-LIB... |
commit | commitdiff | tree |
| 2013-06-24 |
Andrew Reynolds | Add options for symmetry breaking in uf+ss totality... |
commit | commitdiff | tree |
| 2013-06-21 |
Morgan Deters | Fix failure in non-assertion builds on incorrect SmtEng... |
commit | commitdiff | tree |
| 2013-06-19 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-06-19 |
Morgan Deters | Workaround for suspected clang 3.0 codegen bug on Mac |
commit | commitdiff | tree |
| 2013-06-19 |
Morgan Deters | Fix to the "include" extended feature of the SMT-LIB... |
commit | commitdiff | tree |
| 2013-06-19 |
Morgan Deters | Give a more useful parse error message for "undeclared... |
commit | commitdiff | tree |
| 2013-06-17 |
Morgan Deters | Java streams example I forgot to add a long time ago |
commit | commitdiff | tree |
| 2013-06-17 |
Andrew Reynolds | Make --var-elim-quant true by default. Add rewrite... |
commit | commitdiff | tree |
| 2013-06-16 |
Andrew Reynolds | Fix in SMT2 parser for parametric datatypes |
commit | commitdiff | tree |
| 2013-06-10 |
Morgan Deters | another fix for array-store-all printing |
commit | commitdiff | tree |
| 2013-06-10 |
Morgan Deters | Better array-store-all output for SMT-LIB. |
commit | commitdiff | tree |
| 2013-06-08 |
Morgan Deters | Fix typos in alttheoryskel |
commit | commitdiff | tree |
| 2013-06-08 |
Morgan Deters | Fixes for Boolean terms in arrays (including fix for... |
commit | commitdiff | tree |
| 2013-06-07 |
Morgan Deters | One more case for arrays of Boolean. |
commit | commitdiff | tree |
| 2013-06-07 |
Morgan Deters | Fix for bug 517. |
commit | commitdiff | tree |
| 2013-06-07 |
Morgan Deters | Allow disabling include-file feature |
commit | commitdiff | tree |
| 2013-06-07 |
Dejan Jovanović | small parese issue in IDL |
commit | commitdiff | tree |
| 2013-06-06 |
Dejan Jovanović | typo |
commit | commitdiff | tree |
| 2013-06-06 |
Dejan Jovanović | IDL example theory (to be used with --use-theory=idl). |
commit | commitdiff | tree |
| 2013-06-05 |
Andrew Reynolds | Fix bug in --fmf-fmc for producing models of functions... |
commit | commitdiff | tree |
| 2013-06-04 |
Morgan Deters | File inclusion in Smt2 parser. |
commit | commitdiff | tree |
| 2013-06-04 |
Morgan Deters | Add --no-condense-function-values option for explicit... |
commit | commitdiff | tree |
| 2013-06-04 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-06-04 |
Morgan Deters | Fix clang static initialization order issue; fixes... |
commit | commitdiff | tree |
| 2013-06-04 |
Andrew Reynolds | Add partial support for MBQI with arrays when using... |
commit | commitdiff | tree |
| 2013-06-03 |
Morgan Deters | Merge tag 'casc24' |
commit | commitdiff | tree |
| 2013-06-03 |
Morgan Deters | Updated CASC scripts, as provided to Geoff Sutcliffe |
commit | commitdiff | tree |
| 2013-05-29 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| 2013-05-29 |
Morgan Deters | Per SMT-LIB spec, allow (set-info..) command to succeed... |
commit | commitdiff | tree |
| 2013-05-29 |
Morgan Deters | SMT-LIB printer updates (some missing cases). |
commit | commitdiff | tree |
| 2013-05-29 |
Morgan Deters | Fix bug where strict mode didn't allow DIV or MOD,... |
commit | commitdiff | tree |
| 2013-05-28 |
Morgan Deters | Standardize SMT-LIBv2 set of logics to use LogicInfo. |
commit | commitdiff | tree |
| 2013-05-23 |
Andrew Reynolds | Refactoring to prepare for MBQI with integer quantifica... |
commit | commitdiff | tree |
| 2013-05-22 |
Andrew Reynolds | Merge branch 'master' of https://github.com/CVC4/CVC4 |
commit | commitdiff | tree |
| 2013-05-22 |
Andrew Reynolds | Significant work on bounded integer quantification... |
commit | commitdiff | tree |
| 2013-05-22 |
Andrew Reynolds | Add regressions for finite model finding |
commit | commitdiff | tree |
| 2013-05-21 |
Morgan Deters | Merge branch '1.2.x' |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog