summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers
AgeCommit message (Expand)Author
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Merging some cleanup work:Morgan Deters
2013-03-30do simple ite rewriting within quantifiersAndrew Reynolds
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-11ite removal option for quantifiers --ite-remove-quant, e-matching for boolean...Andrew Reynolds
2013-03-06fixed two bugs for the new E-matching implementation, added aggressive minisc...Andrew Reynolds
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-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-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-04Model no longer adds subterms of quantifiers to equality engine, this fixed b...Andrew Reynolds
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 errors and reduce warnings on clang (merge from mdeters/clang)Morgan Deters
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
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-05Improved garbage collection for TheoryArith. The merges all of the code over...Tim King
2012-12-01drastic simplification of quantifiers code regarding equality queries, instan...Andrew Reynolds
2012-11-30quantifiers now uses master equality engine, preparation work to cleanup codeAndrew Reynolds
2012-11-26Adding support for a master equality engine. Each theory gets the master equa...Dejan Jovanović
2012-11-18support for quantifiers macros, bug fix for bug 454 involving E-matching Arra...Andrew Reynolds
2012-11-14replaced all static member data from rewrite rule triggers, added infrastruct...Andrew Reynolds
2012-11-13refactoring of quantifiers rewriter based on code review from yesterday, refa...Andrew Reynolds
2012-11-12minor bug fixes for quantifiers, added sort inference module (not ready to be...Andrew Reynolds
2012-11-10Fix to quantifier rewritting not being idempotent. See bug 441.Tim King
2012-11-07* Type ascription bug fixed (resolves bug 432), but there are others I discov...Morgan Deters
2012-11-02more minor updates to inst gen and representative selection, clean up of equa...Andrew Reynolds
2012-10-31cleaning up some of the equality query stuff, implemented a new representativ...Andrew Reynolds
2012-10-29more updates and minor bug fixes for fmf/inst-gen quantifier instantiationAndrew Reynolds
2012-10-24efficient e-matching now specific to rewrite rulesAndrew Reynolds
2012-10-23more major cleanup of quantifiers code, separating rewrite-rules-specific cod...Andrew Reynolds
2012-10-23more updates to inst gen: fixed partial instantiations, recognize duplicate d...Andrew Reynolds
2012-10-19--fallback-sequential / --no-fallback-sequential optionKshitij Bansal
2012-10-17first working version of new inst-gen-style quantifier instantiation techniqu...Andrew Reynolds
2012-10-16more cleanup of quantifiers codeAndrew Reynolds
2012-10-16first draft of new inst gen method (still with bugs), some cleanup of quantif...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback