Age | Commit message (Expand) | Author |
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 |
2013-05-20 | Fix erroneous results when the logic was incorrectly specified (by throwing L... | Morgan Deters |
2013-05-17 | Better error on invalid logic strings. | Morgan Deters |
2013-05-16 | configure fix for building with glpk on redhat, perhaps others | Morgan Deters |
2013-05-16 | Fix minor bug in full_model_check.cpp | Andrew Reynolds |
2013-05-14 | added some extra options to the bit-vector theory | lianah |
2013-05-14 | Refactoring to separate old and new model building/checking code. | Andrew Reynolds |
2013-05-11 | Preliminary version of finite model finding over bounded integer quantificati... | Andrew Reynolds |
2013-05-10 | disable Logic-checking with finite model finding for now, since FMF uses Rati... | Morgan Deters |
2013-05-10 | Fix erroneous results when the logic was incorrectly specified (by throwing L... | Morgan Deters |
2013-05-10 | Add documentation for --disable-fmf-inst-gen, which removes a warning | Morgan Deters |
2013-05-09 | Add simplification option --fo-prop-quant. Add model support for new model-c... | Andrew Reynolds |
2013-05-09 | Changing the integer normal form to increase matching. | Tim King |
2013-05-08 | Add new method for checking candidate models, --fmf-fmc. Add infrastructure ... | Andrew Reynolds |
2013-05-08 | Removing arithmetic compile warning for release | Morgan Deters |
2013-05-08 | Fixed assertion bug | Clark Barrett |
2013-05-07 | fix for nonterminating model-based array loop | Morgan Deters |
2013-05-07 | added type checking rule to check for bit-vector constants of size 0 | lianah |
2013-05-07 | one more fix for rewrites | lianah |
2013-05-07 | fixed bv rewrite blow-up | lianah |
2013-05-07 | fix for bug500 | Dejan Jovanović |