summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2013-07-02Make uf strong solver user-context dependent, fixes bug 522.Andrew Reynolds
2013-07-02Minor fixes for bounded integers, rewrite engine.Andrew Reynolds
2013-06-28More bug fixes for interval models.Andrew Reynolds
2013-06-27Better check-models output for some kinds of problems; add anassertion that t...Morgan Deters
2013-06-27Small fix for IS_INTEGER.Morgan Deters
2013-06-26Add support for interval models in bounded integers MBQI (in progress).Andrew Reynolds
2013-06-25Refactoring of model engine to separate individual implementations of model b...Andrew Reynolds
2013-06-24Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk al...Morgan Deters
2013-06-24Add options for symmetry breaking in uf+ss totality axiom approach, option fo...Andrew Reynolds
2013-06-19Workaround for suspected clang 3.0 codegen bug on MacMorgan Deters
2013-06-17Make --var-elim-quant true by default. Add rewrite engine to quantifiers mod...Andrew Reynolds
2013-06-07Fix for bug 517.Morgan Deters
2013-06-06small parese issue in IDLDejan Jovanović
2013-06-06typoDejan Jovanović
2013-06-06IDL example theory (to be used with --use-theory=idl).Dejan Jovanović
2013-06-05Fix bug in --fmf-fmc for producing models of functions not appearing in quant...Andrew Reynolds
2013-06-04Add --no-condense-function-values option for explicit function models (useful...Morgan Deters
2013-06-04Merge branch '1.2.x'Morgan Deters
2013-06-04Fix clang static initialization order issue; fixes bug 512.Morgan Deters
2013-06-04Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant ...Andrew Reynolds
2013-05-29Merge branch '1.2.x'Morgan Deters
2013-05-28Standardize SMT-LIBv2 set of logics to use LogicInfo.Morgan Deters
2013-05-23Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.Andrew Reynolds
2013-05-22Merge branch 'master' of https://github.com/CVC4/CVC4Andrew Reynolds
2013-05-22Significant work on bounded integer quantification to handle non-trivial boun...Andrew Reynolds
2013-05-22Add regressions for finite model findingAndrew Reynolds
2013-05-21Merge branch '1.2.x'Morgan Deters
2013-05-21Fix bug 512: an assertion failure only appearing with clang on Mac OS, due to...Morgan Deters
2013-05-21Merge branch '1.2.x'Morgan Deters
2013-05-21Fix incremental bug in symmetry breaker.Morgan Deters
2013-05-20Better error on invalid logic strings.Morgan Deters
2013-05-20configure fix for building with glpk on redhat, perhaps othersMorgan Deters
2013-05-20disable Logic-checking with finite model finding for now, since FMF uses Rati...Morgan Deters
2013-05-20Fix erroneous results when the logic was incorrectly specified (by throwing L...Morgan Deters
2013-05-17Better error on invalid logic strings.Morgan Deters
2013-05-16configure fix for building with glpk on redhat, perhaps othersMorgan Deters
2013-05-16Fix minor bug in full_model_check.cppAndrew Reynolds
2013-05-14added some extra options to the bit-vector theorylianah
2013-05-14Refactoring to separate old and new model building/checking code.Andrew Reynolds
2013-05-11Preliminary version of finite model finding over bounded integer quantificati...Andrew Reynolds
2013-05-10disable Logic-checking with finite model finding for now, since FMF uses Rati...Morgan Deters
2013-05-10Fix erroneous results when the logic was incorrectly specified (by throwing L...Morgan Deters
2013-05-10Add documentation for --disable-fmf-inst-gen, which removes a warningMorgan Deters
2013-05-09Add simplification option --fo-prop-quant. Add model support for new model-c...Andrew Reynolds
2013-05-09Changing the integer normal form to increase matching.Tim King
2013-05-08Add new method for checking candidate models, --fmf-fmc. Add infrastructure ...Andrew Reynolds
2013-05-08Removing arithmetic compile warning for releaseMorgan Deters
2013-05-08Fixed assertion bugClark Barrett
2013-05-07fix for nonterminating model-based array loopMorgan Deters
2013-05-07added type checking rule to check for bit-vector constants of size 0lianah
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback