summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/full_model_check.h
AgeCommit message (Expand)Author
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
2017-07-07Update copyright headers.Mathias Preiner
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ...ajreynol
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
2016-10-11Merge branch 'origin' of https://github.com/CVC4/CVC4.gitPaul Meng
2016-09-15Refactor setIncomplete in quantifiers.ajreynol
2016-07-05Merge branch 'master' of https://github.com/CVC4/CVC4.gitPaulMeng
2016-04-20update from the masterPaulMeng
2016-04-03Updating the copyright headers and scripts.Tim King
2016-02-08Updates related to finite model finding and (co)datatypes. Bug fix enumerator...ajreynol
2015-04-28Fix smt2 printing of fun-def. Simplification of mbqi interface.ajreynol
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2014-04-29Mostly resolves bug #561 memory leaks, and more.Morgan Deters
2014-01-03Added support for proof production in Equality Engine. Cleaned up existing p...Andrew Reynolds
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-06Bug fixes for bounded integer quantification. Current best strategy is to tu...Andrew Reynolds
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-08-13Minor cleanup.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-22Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers, added infrastru...Andrew Reynolds
2013-06-28More bug fixes for interval models.Andrew Reynolds
2013-06-26Add support for interval models in bounded integers MBQI (in progress).Andrew Reynolds
2013-06-25Refactoring of model engine to separate individual implementations of model b...Andrew Reynolds
2013-06-24Add options for symmetry breaking in uf+ss totality axiom approach, option fo...Andrew Reynolds
2013-06-04Add partial support for MBQI with arrays when using --fmf-fmc. Fix constant ...Andrew 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-05-14Refactoring to separate old and new model building/checking code.Andrew Reynolds
2013-05-09Add simplification option --fo-prop-quant. Add model support for new model-c...Andrew Reynolds
2013-05-08Add new method for checking candidate models, --fmf-fmc. Add infrastructure ...Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback