summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/relevant_domain.cpp
AgeCommit message (Expand)Author
2014-02-09More complete guess instantiation strategy, cvc4 now typically times out inst...Andrew Reynolds
2014-01-30Refactor QCF slightly. Bug fix for relevant domain (non-ground terms were ad...Andrew Reynolds
2014-01-28More optimizations of quantifier instantiation data structures.Andrew Reynolds
2014-01-26More optimization of QCF. Fixed InstMatchTrie for caching instantiations. U...Andrew Reynolds
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-09add relevant domain computationAndrew Reynolds
2013-05-23Refactoring to prepare for MBQI with integer quantification. Minor bug fixes.Andrew Reynolds
2013-05-22Significant work on bounded integer quantification to handle non-trivial boun...Andrew Reynolds
2013-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2012-10-29more updates and minor bug fixes for fmf/inst-gen quantifier instantiationAndrew Reynolds
2012-10-16more cleanup of quantifiers codeAndrew Reynolds
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-07-27Minor cleanup after today's commits:Morgan Deters
2012-07-27merging fmf-devel branch, includes refactored datatype theory, updates to mod...Andrew Reynolds
2012-07-12merged fmf-devel branch, includes support for SMT2 command get-value and (ext...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback