summaryrefslogtreecommitdiff
path: root/src/theory/uf
AgeCommit message (Expand)Author
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-19possible fix for bug 521Dejan Jovanovic
2013-07-16"Tabular"-style function definitions in models with --no-condense-function-va...Morgan Deters
2013-07-02Make uf strong solver user-context dependent, fixes bug 522.Andrew Reynolds
2013-06-25Refactoring of model engine to separate individual implementations of model b...Andrew Reynolds
2013-06-24Add options for symmetry breaking in uf+ss totality axiom approach, option fo...Andrew Reynolds
2013-06-04Add --no-condense-function-values option for explicit function models (useful...Morgan Deters
2013-05-21Merge branch '1.2.x'Morgan Deters
2013-05-21Fix incremental bug in symmetry breaker.Morgan Deters
2013-05-09Add simplification option --fo-prop-quant. Add model support for new model-c...Andrew Reynolds
2013-05-08Add new method for checking candidate models, --fmf-fmc. Add infrastructure ...Andrew Reynolds
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-04-01Merging some cleanup work:Morgan Deters
2013-03-21another typo/bugfix for equality constant evaluationDejan Jovanović
2013-03-21fixing markings of internal nodes in equality engineDejan Jovanović
2013-03-21more equality constant evaluationDejan Jovanović
2013-03-21fixing constant evaluation bugsDejan Jovanović
2013-03-19Adding evaluation of constant terms to the equality engine. Evaluation on a p...Dejan Jovanović
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-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-04Model no longer adds subterms of quantifiers to equality engine, this fixed b...Andrew Reynolds
2012-12-01remove instantiator frameworkMorgan Deters
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-16fixing and refactoring the equality iteratorDejan Jovanović
2012-11-15More fixes to model generation, with previously failing testcasesClark Barrett
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-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-16more cleanup of quantifiers codeAndrew Reynolds
2012-10-16first draft of new inst gen method (still with bugs), some cleanup of quantif...Andrew Reynolds
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-10cleanup up some static data members in the quantifiers codeAndrew Reynolds
2012-10-09More fixes to model codeClark Barrett
2012-10-09fix for bug 415Dejan Jovanović
2012-10-09fix beta reduction in both preRewrite() *and* postRewrite(), related to bug 4...Morgan Deters
2012-10-09adding mergePredicates method to the equality engine to be able toDejan Jovanović
2012-10-08* Models' SubstitutionMaps are now attached to the user contextMorgan Deters
2012-10-06* Clean up some options documentationMorgan Deters
2012-10-03New model code, mostly workinClark Barrett
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback