Age | Commit message (Expand) | Author |
2013-08-13 | Minor fixes for --fmf-fmc for quantifiers containing datatypes | Andrew Reynolds |
2013-08-13 | initial modifications for per-ic cbqi | Andrew Reynolds |
2013-07-29 | Fix numerous compiler warnings on various platforms | Morgan Deters |
2013-07-22 | Allow BV and DT in either order in the logic string | Morgan Deters |
2013-07-22 | Add option --cbqi-recurse. | Andrew Reynolds |
2013-07-22 | Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastru... | Andrew Reynolds |
2013-07-19 | possible fix for bug 521 | Dejan Jovanovic |
2013-07-19 | Minor fix for --no-condense-function-values | Morgan Deters |
2013-07-18 | Fix quantifier instantiation bug in cbqi, add default priorities in rewrite e... | Andrew Reynolds |
2013-07-17 | Fix bug 516; include some bug testcases. | Morgan Deters |
2013-07-16 | fixed seg fault when bv equality is turned off | Liana Hadarean |
2013-07-16 | fixed bug520 | Liana Hadarean |
2013-07-16 | "Tabular"-style function definitions in models with --no-condense-function-va... | Morgan Deters |
2013-07-16 | Minor bugfixes to model-building | Morgan Deters |
2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | 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-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-27 | Better check-models output for some kinds of problems; add anassertion that t... | Morgan Deters |
2013-06-27 | Small fix for IS_INTEGER. | Morgan Deters |
2013-06-26 | Add support for interval models in bounded integers MBQI (in progress). | Andrew Reynolds |
2013-06-25 | Refactoring of model engine to separate individual implementations of model b... | Andrew Reynolds |
2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al... | Morgan Deters |
2013-06-24 | Add options for symmetry breaking in uf+ss totality axiom approach, option fo... | Andrew Reynolds |
2013-06-19 | Workaround for suspected clang 3.0 codegen bug on Mac | Morgan Deters |
2013-06-17 | Make --var-elim-quant true by default. Add rewrite engine to quantifiers mod... | Andrew Reynolds |
2013-06-07 | Fix for bug 517. | 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 quant... | Andrew Reynolds |
2013-06-04 | Add --no-condense-function-values option for explicit function models (useful... | Morgan Deters |
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 |
2013-05-29 | Merge branch '1.2.x' | Morgan Deters |
2013-05-28 | Standardize SMT-LIBv2 set of logics to use LogicInfo. | Morgan Deters |
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 |
2013-05-22 | Significant work on bounded integer quantification to handle non-trivial boun... | Andrew Reynolds |
2013-05-22 | Add regressions for finite model finding | Andrew Reynolds |
2013-05-21 | Merge branch '1.2.x' | Morgan Deters |
2013-05-21 | Fix bug 512: an assertion failure only appearing with clang on Mac OS, due to... | Morgan Deters |
2013-05-21 | Merge branch '1.2.x' | Morgan Deters |
2013-05-21 | Fix incremental bug in symmetry breaker. | Morgan Deters |
2013-05-20 | Better error on invalid logic strings. | Morgan Deters |
2013-05-20 | configure fix for building with glpk on redhat, perhaps others | Morgan Deters |
2013-05-20 | disable Logic-checking with finite model finding for now, since FMF uses Rati... | Morgan Deters |