summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/bounded_integers.cpp
AgeCommit message (Expand)Author
2015-06-09Bug fix instantiations for fmf-bound-int. Disable nested pre-skolemization f...ajreynol
2015-03-04More work on arithmetic single invocation synthesis conjectures.ajreynol
2015-02-02Single invocation module for counterexample guided quantifier instantiation -...ajreynol
2014-10-18Fix for bounded integers when incremental, fixes bug 588. Add option --dt-bi...ajreynol
2014-08-01Minor cleanup from previous commit. Better organization for how quantifiers ...ajreynol
2014-07-01Update copyrights.Morgan Deters
2014-05-13Add lazy strategy for bounded integers to avoid non-terminating unsat cases. ...ajreynol
2014-04-17simplify mkSkolem naming system: don't use $$Kshitij Bansal
2014-03-11Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu...Andrew Reynolds
2014-03-07Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodi...Morgan Deters
2014-03-04Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (r...Morgan Deters
2014-01-18Fixed non-termination issue in bounded integers.Andrew Reynolds
2014-01-10Add new method --quant-cf for finding conflicts eagerly for quantified formul...Andrew Reynolds
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-11-26Bug fix for E-matching select terms, minor fix for bounded integers, bug fix ...Andrew Reynolds
2013-11-06Bug fixes for bounded integer quantification. Current best strategy is to tu...Andrew Reynolds
2013-09-27Add new symmetry breaking technique for finite model finding. Improvements t...Andrew Reynolds
2013-09-15Change default option of simple ite lifting within quantifier bodies. add so...Andrew Reynolds
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
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-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-11Preliminary version of finite model finding over bounded integer quantificati...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