summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Expand)Author
2013-03-15changed default option for quantifier instantiationAndrew Reynolds
2013-03-14Merge branch '1.0.x'Morgan Deters
2013-03-14fix to build system: #include the proper file when they are in both builds an...Morgan Deters
2013-03-13Added a rewrite for iff:Clark Barrett
2013-03-11ite removal option for quantifiers --ite-remove-quant, e-matching for boolean...Andrew Reynolds
2013-03-06Best heuristics for handling decision requests from arraysClark Barrett
2013-03-06fixed two bugs for the new E-matching implementation, added aggressive minisc...Andrew Reynolds
2013-02-26Bug fix for rep-set.Morgan Deters
2013-02-26Merge branch '1.0.x'lianah
2013-02-26Merge branch '1.0.x' of https://github.com/CVC4/CVC4 into 1.0.xlianah
2013-02-26fix for bv crash in incremental mode; this is a temporary fix for bug 493lianah
2013-02-24added option --model-u-dt-enum for outputting uninterpreted sorts as datatype...Andrew Reynolds
2013-02-16Some cleanup and copyright updatingMorgan Deters
2013-02-15Merge branch '1.0.x'Tim King
2013-02-15repairs a bug in rewriterule engine: constructor cannot be used as a patternTianyi Liang
2013-02-14Removing BVDebug and replacing with Debug.Tim King
2013-02-13repairs a bug in rewriterule engine: constructor cannot be used as a patternTianyi Liang
2013-02-12Fix a preprocessing performance issue.Morgan Deters
2013-02-07Merge branch '1.0.x'Morgan Deters
2013-02-07Only put quantifier assertions in model equality engine if fullModel==trueMorgan Deters
2013-02-07Significant work on bug #491 (not yet closed).Morgan Deters
2013-02-07More complete fix for bug 484 (includes fixes for records and tuples).Morgan Deters
2013-02-07Fix error in tuple type-checking.Morgan Deters
2013-02-06make datatypes enumerator behavior clearer (no exceptions in normal operation)Morgan Deters
2013-02-06make datatypes enumerator behavior clearer (no exceptions in normal operation)Morgan Deters
2013-02-05dos2unix conversion for a number of files; this avoids spurious conflicts whe...Morgan Deters
2013-02-05More improvements for E-matchingAndrew Reynolds
2013-02-04fixed files with DOS newlines; fixed contrib/ scripts to use gitMorgan Deters
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...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-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-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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback