Age | Commit message (Expand) | Author |
2013-03-19 | Adding evaluation of constant terms to the equality engine. Evaluation on a p... | Dejan Jovanović |
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-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-04 | Model no longer adds subterms of quantifiers to equality engine, this fixed b... | Andrew Reynolds |
2012-12-01 | remove instantiator framework | Morgan Deters |
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-16 | fixing and refactoring the equality iterator | Dejan Jovanović |
2012-11-15 | More fixes to model generation, with previously failing testcases | Clark Barrett |
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-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-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 |
2012-10-10 | cleanup up some static data members in the quantifiers code | Andrew Reynolds |
2012-10-09 | More fixes to model code | Clark Barrett |
2012-10-09 | fix for bug 415 | Dejan Jovanović |
2012-10-09 | fix beta reduction in both preRewrite() *and* postRewrite(), related to bug 4... | Morgan Deters |
2012-10-09 | adding mergePredicates method to the equality engine to be able to | Dejan Jovanović |
2012-10-08 | * Models' SubstitutionMaps are now attached to the user context | Morgan Deters |
2012-10-06 | * Clean up some options documentation | Morgan Deters |
2012-10-03 | New model code, mostly workin | Clark Barrett |
2012-10-01 | initial draft of skolemization during pre-processing, made simple cliques the... | Andrew Reynolds |
2012-09-26 | updates to model generation : do not modify equality engine during getValue, ... | Andrew Reynolds |
2012-09-26 | Fix type checking for define-funs (resolves bug 398). | Morgan Deters |
2012-09-22 | Separate public-facing and internal-facing interfaces to Statistics. | Morgan Deters |
2012-09-22 | another fix for the equality class iterator | Dejan Jovanović |
2012-09-19 | General subscriber infrastructure for NodeManager, as discussed in the | Morgan Deters |
2012-09-19 | fix for bug 370. | Dejan Jovanović |
2012-09-19 | Changing the equality engines's euivalence class iterator. Andy please check ... | Dejan Jovanović |
2012-09-17 | minor fix for models, added simple cliques option for uf strong solver | Andrew Reynolds |
2012-09-13 | ensure that get-value and get-model are consistent, rewrite function value bo... | Andrew Reynolds |
2012-09-12 | Adding model assertions after SAT responses. | Morgan Deters |
2012-08-31 | merge from fmf-devel branch. more updates to models: now with collectModelIn... | Andrew Reynolds |
2012-08-29 | * Numerous documentation fixes (fix doxygen warnings, add missing documentati... | Morgan Deters |
2012-08-24 | * disallow internal uses of mkVar() (you have to mkSkolem()) | Morgan Deters |
2012-08-16 | Replace propagateAsDecision() with Theory::getNextDecisionRequest(): | Morgan Deters |
2012-08-14 | Switched a number of EqClassIterator operations to const as well as the inter... | Tim King |
2012-08-03 | fix uses of getMetaKind() from outside the expr package. (they now use isCon... | Morgan Deters |
2012-07-31 | Moving some instantiation-related stuff from src/theory to src/theory/quantif... | Morgan Deters |
2012-07-31 | Options merge. This commit: | Morgan Deters |