summaryrefslogtreecommitdiff
path: root/src/theory/uf
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-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
2012-10-01initial draft of skolemization during pre-processing, made simple cliques the...Andrew Reynolds
2012-09-26updates to model generation : do not modify equality engine during getValue, ...Andrew Reynolds
2012-09-26Fix type checking for define-funs (resolves bug 398).Morgan Deters
2012-09-22Separate public-facing and internal-facing interfaces to Statistics.Morgan Deters
2012-09-22another fix for the equality class iterator Dejan Jovanović
2012-09-19General subscriber infrastructure for NodeManager, as discussed in theMorgan Deters
2012-09-19fix for bug 370.Dejan Jovanović
2012-09-19Changing the equality engines's euivalence class iterator. Andy please check ...Dejan Jovanović
2012-09-17minor fix for models, added simple cliques option for uf strong solverAndrew Reynolds
2012-09-13ensure that get-value and get-model are consistent, rewrite function value bo...Andrew Reynolds
2012-09-12Adding model assertions after SAT responses.Morgan Deters
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback