Age | Commit message (Expand) | Author |
2013-07-19 | possible fix for bug 521 | Dejan Jovanovic |
2013-07-16 | "Tabular"-style function definitions in models with --no-condense-function-va... | Morgan Deters |
2013-07-02 | Make uf strong solver user-context dependent, fixes bug 522. | Andrew Reynolds |
2013-06-25 | Refactoring of model engine to separate individual implementations of model b... | Andrew Reynolds |
2013-06-24 | Add options for symmetry breaking in uf+ss totality axiom approach, option fo... | Andrew Reynolds |
2013-06-04 | Add --no-condense-function-values option for explicit function models (useful... | Morgan Deters |
2013-05-21 | Merge branch '1.2.x' | Morgan Deters |
2013-05-21 | Fix incremental bug in symmetry breaker. | Morgan Deters |
2013-05-09 | Add simplification option --fo-prop-quant. Add model support for new model-c... | Andrew Reynolds |
2013-05-08 | Add new method for checking candidate models, --fmf-fmc. Add infrastructure ... | Andrew Reynolds |
2013-04-02 | Regenerated copyrights: canonicalized names, no emails | Morgan Deters |
2013-04-01 | update copyrights | Morgan Deters |
2013-04-01 | Merging some cleanup work: | Morgan Deters |
2013-03-21 | another typo/bugfix for equality constant evaluation | Dejan Jovanović |
2013-03-21 | fixing markings of internal nodes in equality engine | Dejan Jovanović |
2013-03-21 | more equality constant evaluation | Dejan Jovanović |
2013-03-21 | fixing constant evaluation bugs | Dejan Jovanović |
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 |