summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
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
2013-05-07one more fix for rewriteslianah
2013-05-07fixed bv rewrite blow-uplianah
2013-05-07fix for bug500Dejan Jovanović
2013-05-07Fixes a bug with arithmetic's new attempt solution infrastructure. This caus...Tim King
2013-05-07Improving arithmetic debugging output.Tim King
2013-05-07Disabling an incorrect prototyping line from the simplex merges. Fixes bug 510.Tim King
2013-05-06fixed bv rewrite rule bugLiana Hadarean
2013-05-06Removing excess verbosity from ApproxSimplex (after discussing with Tim)Morgan Deters
2013-05-06Adding a heuristic for guessing an optimization function when using glpk.Tim King
2013-05-06Some bug fixes for mb arraysClark Barrett
2013-05-05Adding cut offs for likely integer infeasible paths.Tim King
2013-05-03Adding a smarter technique for pivoting in solutions for glpk.Tim King
2013-05-03Fixing compilation of unit tests. These problems were due to splitLemma() bei...Tim King
2013-05-03More misc. arithmetic cleanup. Removing unused files and functions. Also remo...Tim King
2013-05-03Code cleanup. Reducing misc. warnings in arithmetic.Tim King
2013-05-03Removing arithmetic legacy code and unifying functions.Tim King
2013-05-03Fixing a debug typo.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback