summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2013-02-04Some fixes for the miplib preprocessing pass.Morgan Deters
2013-02-04Model no longer adds subterms of quantifiers to equality engine, this fixed b...Andrew Reynolds
2013-02-03Some cleanup of miplib regressions and optionsMorgan Deters
2013-02-03new option for doing top-level miplib substitutions (or not)Morgan Deters
2013-02-03new miplib pass, works for 1 or 2 varsMorgan Deters
2013-02-03Remove old miplibtrick from arith static learnerMorgan Deters
2013-01-31Adding a heuristic to more eagerly split bounded integer variables.Tim King
2013-01-28fix for finite model finding caused by new collectModelInfo codeAndrew Reynolds
2013-01-28made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_pro...Andrew Reynolds
2013-01-27some fixes for Intel benchmarks regarding quantifiers and datatypes, datatype...Andrew Reynolds
2013-01-26Merge branch '1.0.x'Morgan Deters
2013-01-26another fix for quantifier models (related to bug 486)Morgan Deters
2013-01-25fix --check-model --finite-model-find when used together (related to bug 486)Morgan Deters
2013-01-25Fix errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
2013-01-25fix --check-model --finite-model-find when used together (related to bug 486)Morgan Deters
2013-01-24Add win32 support (merge from mdeters/win32, with some cleanup).Morgan Deters
2013-01-23Adding miplibtrick option.Tim King
2013-01-23Adding substitution size cap.Tim King
2013-01-23partially address bug 486: allow some model inspection of quantifiersMorgan Deters
2013-01-23partially address bug 486: allow some model inspection of quantifiersMorgan Deters
2013-01-22Merge branch '1.0.x'Morgan Deters
2013-01-22fix for theory preprocessing cache on clang, perhaps others.Morgan Deters
2012-12-21Merge branch '1.0.x'Dejan Jovanović
2012-12-21adding copy constructor for the datatype enumeratorDejan Jovanović
2012-12-14Merging in patch from branch '1.0.x'.Tim King
2012-12-14Merge remote-tracking branch 'main-repo/1.0.x' into 1.0.xTim King
2012-12-14Changing the rewriter to use Boute's Euclidean definition of division.Tim King
2012-12-12Merge pull request #2 from CVC4/1.0.xDejan Jovanović
2012-12-12* fixed bug 481 by adding check for division by 0 in bit-vector division circuitlianah
2012-12-11adding cache for preprocessing datatypes terms to fix bug 475, fix for handli...Andrew Reynolds
2012-12-11adding cache for preprocessing datatypes terms to fix bug 475, fix for handli...Andrew Reynolds
2012-12-06* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issuesMorgan Deters
2012-12-06Fix for fuzzer-found model bugClark Barrett
2012-12-06* some build fixes; thanks; thanks to Kunal Ganeshpure for noting these issuesMorgan Deters
2012-12-05Improved garbage collection for TheoryArith. The merges all of the code over...Tim King
2012-12-05Cleanup of arithmetic, and some new utility functions for the coming fcsimple...Tim King
2012-12-05This commit merges in CDTrailHashMap and CDInsertHashMap. CDHashSet now uses ...Tim King
2012-12-03Fix for fuzzer-found model bugClark Barrett
2012-12-01Throw a logic exception if user makes an assertion using a STORE_ALLClark Barrett
2012-12-01remove instantiator frameworkMorgan Deters
2012-12-01Fix the way abstract values are typed; fixes some compliance issues.Morgan Deters
2012-12-01drastic simplification of quantifiers code regarding equality queries, instan...Andrew Reynolds
2012-11-30Changing the documentation of ARR_TABLE_FUN to say (internal symbol).Tim King
2012-11-30quantifiers now uses master equality engine, preparation work to cleanup codeAndrew Reynolds
2012-11-30parametric datatypes fix related to non-ascribed type constructors introduced...Andrew Reynolds
2012-11-30Partial fix for bug 435; still needs some effort.Morgan Deters
2012-11-29require type ascriptions for parametric datatype constructors (making them ca...Andrew Reynolds
2012-11-29Fixing function models with Boolean terms. Also, LAMBDA's should not be const.Clark Barrett
2012-11-28Fix for getValue. Now it can handle lambda applicationsClark Barrett
2012-11-27Functions and predicates over Boolean now work with --check-models and output...Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback