summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_conflict_find.cpp
AgeCommit message (Expand)Author
2014-02-14Make QCF more incremental. Fix bug in QCF handling of ITE formulas, add supp...Andrew Reynolds
2014-02-09More complete guess instantiation strategy, cvc4 now typically times out inst...Andrew Reynolds
2014-02-05Bug fix for theory strings related to old cycle detection code (was leading t...Andrew Reynolds
2014-02-04Add variable ordering for QCF to accelerate matching procedure. Preparing fo...Andrew Reynolds
2014-02-03Handle nested (universal) quantifiers in QCF algorithm. Make relevant domain...Andrew Reynolds
2014-01-30Refactor QCF slightly. Bug fix for relevant domain (non-ground terms were ad...Andrew Reynolds
2014-01-27More optimization of QCF and instantiation caching. Fix CDInstMatchTrie.Andrew Reynolds
2014-01-26More optimization of QCF. Fixed InstMatchTrie for caching instantiations. U...Andrew Reynolds
2014-01-24Simplify the QCF algorithm by more aggressive flattening, removes EqRegistry ...Andrew Reynolds
2014-01-18Performance optimization for E-matching, working on using QCF module for prop...Andrew Reynolds
2014-01-17More optimizations for quantifiers conflict find. Add trust user patterns mode.Andrew Reynolds
2014-01-15Optimizations for quantifiers conflict find: better caching, process matching...Andrew Reynolds
2014-01-10Add stats to quantifiers conflict find. Added option for qcf. Working on ha...Andrew Reynolds
2014-01-10Add new method --quant-cf for finding conflicts eagerly for quantified formul...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback