Age | Commit message (Expand) | Author |
2013-04-01 | update copyrights | Morgan Deters |
2013-04-01 | Merging some cleanup work: | Morgan Deters |
2013-03-30 | do simple ite rewriting within quantifiers | Andrew Reynolds |
2013-03-15 | changed default option for quantifier instantiation | Andrew Reynolds |
2013-03-14 | Merge branch '1.0.x' | Morgan Deters |
2013-03-14 | fix to build system: #include the proper file when they are in both builds an... | Morgan Deters |
2013-03-11 | ite removal option for quantifiers --ite-remove-quant, e-matching for boolean... | Andrew Reynolds |
2013-03-06 | fixed two bugs for the new E-matching implementation, added aggressive minisc... | Andrew Reynolds |
2013-02-24 | added option --model-u-dt-enum for outputting uninterpreted sorts as datatype... | Andrew Reynolds |
2013-02-16 | Some cleanup and copyright updating | Morgan Deters |
2013-02-07 | Merge branch '1.0.x' | Morgan Deters |
2013-02-07 | Only put quantifier assertions in model equality engine if fullModel==true | Morgan Deters |
2013-02-07 | Significant work on bug #491 (not yet closed). | Morgan Deters |
2013-02-05 | dos2unix conversion for a number of files; this avoids spurious conflicts whe... | Morgan Deters |
2013-02-05 | More improvements for E-matching | Andrew Reynolds |
2013-02-04 | fixed files with DOS newlines; fixed contrib/ scripts to use git | Morgan Deters |
2013-02-04 | Model no longer adds subterms of quantifiers to equality engine, this fixed b... | Andrew Reynolds |
2013-01-28 | fix for finite model finding caused by new collectModelInfo code | Andrew Reynolds |
2013-01-28 | made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_pro... | Andrew Reynolds |
2013-01-28 | made QuantifiersEngine::d_inst_match_trie and QuantifiersEngine::d_lemmas_pro... | Andrew Reynolds |
2013-01-27 | some fixes for Intel benchmarks regarding quantifiers and datatypes, datatype... | Andrew Reynolds |
2013-01-27 | some fixes for Intel benchmarks regarding quantifiers and datatypes, datatype... | Andrew Reynolds |
2013-01-26 | Merge branch '1.0.x' | Morgan Deters |
2013-01-26 | another fix for quantifier models (related to bug 486) | Morgan Deters |
2013-01-25 | Fix errors and reduce warnings on clang (merge from mdeters/clang) | Morgan Deters |
2013-01-23 | partially address bug 486: allow some model inspection of quantifiers | Morgan Deters |
2013-01-23 | partially address bug 486: allow some model inspection of quantifiers | Morgan Deters |
2012-12-11 | adding cache for preprocessing datatypes terms to fix bug 475, fix for handli... | Andrew Reynolds |
2012-12-11 | adding cache for preprocessing datatypes terms to fix bug 475, fix for handli... | Andrew Reynolds |
2012-12-05 | Improved garbage collection for TheoryArith. The merges all of the code over... | Tim King |
2012-12-01 | drastic simplification of quantifiers code regarding equality queries, instan... | Andrew Reynolds |
2012-11-30 | quantifiers now uses master equality engine, preparation work to cleanup code | Andrew Reynolds |
2012-11-26 | Adding support for a master equality engine. Each theory gets the master equa... | Dejan Jovanović |
2012-11-18 | support for quantifiers macros, bug fix for bug 454 involving E-matching Arra... | Andrew Reynolds |
2012-11-14 | replaced all static member data from rewrite rule triggers, added infrastruct... | Andrew Reynolds |
2012-11-13 | refactoring of quantifiers rewriter based on code review from yesterday, refa... | Andrew Reynolds |
2012-11-12 | minor bug fixes for quantifiers, added sort inference module (not ready to be... | Andrew Reynolds |
2012-11-10 | Fix 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-02 | more minor updates to inst gen and representative selection, clean up of equa... | Andrew Reynolds |
2012-10-31 | cleaning up some of the equality query stuff, implemented a new representativ... | Andrew Reynolds |
2012-10-29 | more updates and minor bug fixes for fmf/inst-gen quantifier instantiation | Andrew Reynolds |
2012-10-24 | efficient e-matching now specific to rewrite rules | Andrew Reynolds |
2012-10-23 | more major cleanup of quantifiers code, separating rewrite-rules-specific cod... | Andrew Reynolds |
2012-10-23 | more updates to inst gen: fixed partial instantiations, recognize duplicate d... | Andrew Reynolds |
2012-10-19 | --fallback-sequential / --no-fallback-sequential option | Kshitij Bansal |
2012-10-17 | first working version of new inst-gen-style quantifier instantiation techniqu... | Andrew Reynolds |
2012-10-16 | more cleanup of quantifiers code | Andrew Reynolds |
2012-10-16 | first draft of new inst gen method (still with bugs), some cleanup of quantif... | Andrew Reynolds |
2012-10-11 | Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it's | Morgan Deters |