summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/full_model_check.cpp
AgeCommit message (Expand)Author
2014-05-12Minor updates/fix to --cbqi-recurseAndrew Reynolds
2014-05-11More preparation for CASC proofs. Minor fix for sort inference (rewrite new ...Andrew Reynolds
2014-04-28Merge remote-tracking branch 'upstream/master' into setsKshitij Bansal
2014-04-17simplify mkSkolem naming system: don't use $$Kshitij Bansal
2014-04-14Fix bug in mbqi=fmc handling theory symbols. Fix mbqi=fmc models (Bug 557). ...Andrew Reynolds
2014-03-11Initial refactor of rewrite rules, make theory_rewriterules empty theory. Pu...Andrew Reynolds
2014-01-27More optimization of QCF and instantiation caching. Fix CDInstMatchTrie.Andrew Reynolds
2014-01-03Removing and consolidating options for uf-ss and quantifiers. Bug fix for in...Andrew Reynolds
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-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-08-13Minor cleanup.Morgan Deters
2013-08-13Minor fixes for --fmf-fmc for quantifiers containing datatypesAndrew Reynolds
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-07-02Minor fixes for bounded integers, rewrite engine.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-05Fix bug in --fmf-fmc for producing models of functions not appearing in quant...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