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