summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/model_builder.h
AgeCommit message (Expand)Author
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-02-06Resolving warnings from -Winconsistent-missing-override on clang. (#1563)Tim King
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
2017-11-01(Refactor) Split term util (#1303)Andrew Reynolds
2017-11-01(Move-only) Refactor and document theory model part 2 (#1305)Andrew Reynolds
2017-07-07Update copyright headers.Mathias Preiner
2017-04-24Fixes and simplifications for fmf mbqi.ajreynol
2017-03-24Refactor model building for quantifiers to be a single pass, simplification. ...ajreynol
2016-12-02Refactor preprocessing of models in fmf. Fix options --fmf-empty-sorts and --...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-05-02Clean up issues related to compiled scc in LFSC. Refactor --partial-trigger, ...ajreynol
2016-04-20update from the masterPaulMeng
2016-04-03Updating the copyright headers and scripts.Tim King
2015-10-26Promote InstStrategyCbqi to quantifier module. Cleanup unused code.ajreynol
2015-06-27Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by de...ajreynol
2015-04-28Fix smt2 printing of fun-def. Simplification of mbqi interface.ajreynol
2015-04-24Fix compiler errors due to unbalanced throw specifiers.Clark Barrett
2015-04-21Changes needed to compile at Google, plus some bug fixes from Google.Clark Barrett
2014-11-13Remove two obsolete versions of MBQI.ajreynol
2014-10-13Model building into quantifiers engine. Simplify axiom-inst mode.ajreynol
2014-07-01Update copyrights.Morgan Deters
2013-11-27General pre-release cleanup commitMorgan Deters
2013-06-28More bug fixes for interval models.Andrew Reynolds
2013-06-25Refactoring of model engine to separate individual implementations of model b...Andrew Reynolds
2013-06-17Make --var-elim-quant true by default. Add rewrite engine to quantifiers mod...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-04-02Regenerated copyrights: canonicalized names, no emailsMorgan Deters
2013-04-01update copyrightsMorgan Deters
2013-03-06fixed two bugs for the new E-matching implementation, added aggressive minisc...Andrew Reynolds
2012-11-02more minor updates to inst gen and representative selection, clean up of equa...Andrew Reynolds
2012-10-31cleaning up some of the equality query stuff, implemented a new representativ...Andrew Reynolds
2012-10-29more updates and minor bug fixes for fmf/inst-gen quantifier instantiationAndrew Reynolds
2012-10-23more major cleanup of quantifiers code, separating rewrite-rules-specific cod...Andrew Reynolds
2012-10-23more updates to inst gen: fixed partial instantiations, recognize duplicate d...Andrew Reynolds
2012-10-16first draft of new inst gen method (still with bugs), some cleanup of quantif...Andrew Reynolds
2012-10-11Standardizing copyright notice. Touches **ALL** sources, guys, sorry.. it'sMorgan Deters
2012-10-09fixed datatypes rewriter to detect clashes between non-datatype subfields. c...Andrew Reynolds
2012-08-31merge from fmf-devel branch. more updates to models: now with collectModelIn...Andrew Reynolds
2012-07-31Moving some instantiation-related stuff from src/theory to src/theory/quantif...Morgan Deters
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback