summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/relevant_domain.cpp
AgeCommit message (Expand)Author
2016-05-02Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ...ajreynol
2016-04-12Optimizations for QCF to check relevant domain of variable argument positions...ajreynol
2016-04-09Minor refactoring of entailment tests and quantifiers util. Initial draft of ...ajreynol
2016-04-03Updating the copyright headers and scripts.Tim King
2016-03-10Faster conditional rewriting for and/or beneath quantifiers. Improvements to ...ajreynol
2015-11-17Improve relevant domain computation for arithmetic, full saturation strategy....ajreynol
2015-11-12Minor fixes and improvements to purify quant, relational triggers.ajreynol
2014-07-01Update copyrights.Morgan Deters
2014-03-12Work on array pf signature, add working example. Add quantifiers proof signa...Andrew Reynolds
2014-03-11Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu...Andrew Reynolds
2014-02-27Bug fix for QCF algorithm, was missing instantiations. Make prop-eq the defa...Andrew Reynolds
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