Age | Commit message (Expand) | Author |
2015-04-07 | Removing the reference to THEORY_BOOL from the equality engine. This theory | Dejan Jovanovic |
2015-03-25 | change const are triggers from false to true in equality engines | Kshitij Bansal |
2015-03-14 | Patches for 32-bit ARM | Tianyi Liang |
2015-01-16 | Minor: Ensure indexed terms are in EE. Add support for bv constants in sygus... | ajreynol |
2014-12-26 | Adding an option to the equality engine constructor to treat all constants as | Dejan Jovanovic |
2014-12-12 | Add cvc parsing support for cardinality constraints. Bug fix for enumerating... | ajreynol |
2014-12-03 | Revert "Disable constants sharing in eq engine, disable hack in theory engine." | Kshitij Bansal |
2014-11-20 | Disable constants sharing in eq engine, disable hack in theory engine. Chang... | ajreynol |
2014-11-19 | Making construction of trigger sets not use the global engine state. | Dejan Jovanović |
2014-11-17 | New, uniform checkTime statistic for all theories (as discussed in meeting). | Morgan Deters |
2014-11-14 | Be lazier to consider EQC in UF+cardinality solver. Minor cleanup. | ajreynol |
2014-11-05 | More work on datatypes theory combination: fix bug in care graph, do not assi... | ajreynol |
2014-09-24 | Refactor option for uf+cardinality constraints solver. | ajreynol |
2014-09-03 | check() optimization | Kshitij Bansal |
2014-08-04 | Some fixes to symmetry breaker (resolves bug 576). | Morgan Deters |
2014-07-01 | Update copyrights. | Morgan Deters |
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 |