summaryrefslogtreecommitdiff
path: root/src/theory/uf
AgeCommit message (Expand)Author
2014-06-20UF kinds documentationMorgan Deters
2014-05-02Simplification of EqualityEngine::areDisequal. Comparison for production : h...Andrew Reynolds
2014-04-29Fix compiler warning re: TheoryUF destructor.Morgan Deters
2014-04-29Mostly resolves bug #561 memory leaks, and more.Morgan Deters
2014-04-10Add support for cardinality constraints logic UFC. Add regressions in fmf/. ...Andrew Reynolds
2014-04-09Handle fmf.card as input from user, add support in SMT2 parser, as requested ...Andrew Reynolds
2014-03-14Add ability to provide theory-specific proof rules to EqualityEngine, extends...Andrew Reynolds
2014-02-21Merge branch '1.3.x'Morgan Deters
2014-02-21No diamond-breaking under quantifiers (resolves bug #550).Morgan Deters
2014-02-21add new theory (sets)Kshitij Bansal
2014-01-22Delay QuantifiersEngine and UF strong solver initialization until after final...Morgan Deters
2014-01-10Add new method --quant-cf for finding conflicts eagerly for quantified formul...Andrew Reynolds
2014-01-07minor fix, bring back the assertion.Tianyi Liang
2014-01-07string contain changesTianyi Liang
2014-01-03Removing and consolidating options for uf-ss and quantifiers. Bug fix for in...Andrew Reynolds
2014-01-03Added support for proof production in Equality Engine. Cleaned up existing p...Andrew Reynolds
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-11-19Bug fix for previous commitAndrew Reynolds
2013-11-19Add fair strategy for finite model finding multiple sorts --uf-ss-fair.Andrew Reynolds
2013-11-10Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-11-06Bug fixes for bounded integer quantification. Current best strategy is to tu...Andrew Reynolds
2013-10-24Fix for bug515Clark Barrett
2013-10-03Added support for converting unsorted problems to multi-sorted problems via s...Andrew Reynolds
2013-09-30Bug fixes and improvements for symmetry breaking, it now supports multiple so...Andrew Reynolds
2013-09-27Add new symmetry breaking technique for finite model finding. Improvements t...Andrew Reynolds
2013-09-24Reduce compiler dependencies on substitutions.h,Clark Barrett
2013-09-23Revert Clark's last commit, at his request; there are some bugs.Morgan Deters
2013-09-23Cleaner version of bug-fix for 528, also moved substitutions.h out of theory.hClark Barrett
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback