| 2014-03-12 |
Andrew Reynolds | Minor fixes post-merge of RR.
|
commit | commitdiff | tree |
| 2014-03-11 |
Andrew Reynolds | Initial refactor of rewrite rules, make theory_rewriterules...
|
commit | commitdiff | tree |
| 2014-02-27 |
Andrew Reynolds | Bug fix for QCF algorithm, was missing instantiations...
|
commit | commitdiff | tree |
| 2014-02-25 |
Andrew Reynolds | Add options --full-saturate-quant and --mbqi=trust...
|
commit | commitdiff | tree |
| 2014-02-20 |
Andrew Reynolds | Fix ite and iff handling in QCF. Add option for heuristic...
|
commit | commitdiff | tree |
| 2014-02-14 |
Andrew Reynolds | Make QCF more incremental. Fix bug in QCF handling...
|
commit | commitdiff | tree |
| 2014-02-09 |
Andrew Reynolds | More complete guess instantiation strategy, cvc4 now...
|
commit | commitdiff | tree |
| 2014-02-05 |
Andrew Reynolds | Bug fix for theory strings related to old cycle detection...
|
commit | commitdiff | tree |
| 2014-02-04 |
Andrew Reynolds | Do not use transitive closure module for cycle detection...
|
commit | commitdiff | tree |
| 2014-02-04 |
Andrew Reynolds | Add variable ordering for QCF to accelerate matching...
|
commit | commitdiff | tree |
| 2014-02-03 |
Andrew Reynolds | Handle nested (universal) quantifiers in QCF algorithm...
|
commit | commitdiff | tree |
| 2014-01-30 |
Andrew Reynolds | Refactor QCF slightly. Bug fix for relevant domain...
|
commit | commitdiff | tree |
| 2014-01-28 |
Andrew Reynolds | More optimizations of quantifier instantiation data...
|
commit | commitdiff | tree |
| 2014-01-27 |
Andrew Reynolds | More optimization of QCF and instantiation caching...
|
commit | commitdiff | tree |
| 2014-01-26 |
Andrew Reynolds | More optimization of QCF. Fixed InstMatchTrie for...
|
commit | commitdiff | tree |
| 2014-01-24 |
Andrew Reynolds | Simplify the QCF algorithm by more aggressive flattening...
|
commit | commitdiff | tree |
| 2014-01-18 |
Andrew Reynolds | Fixed non-termination issue in bounded integers.
|
commit | commitdiff | tree |
| 2014-01-18 |
Andrew Reynolds | Performance optimization for E-matching, working on...
|
commit | commitdiff | tree |
| 2014-01-17 |
Andrew Reynolds | More optimizations for quantifiers conflict find. ...
|
commit | commitdiff | tree |
| 2014-01-15 |
Andrew Reynolds | Optimizations for quantifiers conflict find: better...
|
commit | commitdiff | tree |
| 2014-01-10 |
Andrew Reynolds | Add stats to quantifiers conflict find. Added option...
|
commit | commitdiff | tree |
| 2014-01-10 |
Andrew Reynolds | Add new method --quant-cf for finding conflicts eagerly...
|
commit | commitdiff | tree |
| 2014-01-04 |
Andrew Reynolds | Removing and consolidating options for uf-ss and quantifiers...
|
commit | commitdiff | tree |
| 2014-01-03 |
Andrew Reynolds | Added support for proof production in Equality Engine...
|
commit | commitdiff | tree |
| 2013-11-27 |
Andrew Reynolds | Bug fix for E-matching select terms, minor fix for...
|
commit | commitdiff | tree |
| 2013-11-19 |
Andrew Reynolds | Bug fix for previous commit
|
commit | commitdiff | tree |
| 2013-11-19 |
Andrew Reynolds | Add fair strategy for finite model finding multiple...
|
commit | commitdiff | tree |
| 2013-11-06 |
Andrew Reynolds | Bug fixes for bounded integer quantification. Current...
|
commit | commitdiff | tree |
| 2013-10-15 |
Andrew Reynolds | performance optimizations for quantifier instantiation
|
commit | commitdiff | tree |
| 2013-10-10 |
Andrew Reynolds | Minor bug fix to datatypes.
|
commit | commitdiff | tree |
| 2013-10-09 |
Andrew Reynolds | More improvements to datatypes, eager selector collapsing...
|
commit | commitdiff | tree |
| 2013-10-08 |
Andrew Reynolds | Optimizations for datatypes theory. There seems to...
|
commit | commitdiff | tree |
| 2013-10-07 |
Andrew Reynolds | Multiple fixes for datatypes theory solver: add support...
|
commit | commitdiff | tree |
| 2013-10-03 |
Andrew Reynolds | Adding example proof signatures for LFSC.
|
commit | commitdiff | tree |
| 2013-10-02 |
Andrew Reynolds | Added support for converting unsorted problems to multi...
|
commit | commitdiff | tree |
| 2013-10-01 |
Andrew Reynolds | Fix a bug in smt2 parser for quantified formulas with...
|
commit | commitdiff | tree |
| 2013-09-30 |
Andrew Reynolds | Bug fixes and improvements for symmetry breaking, it...
|
commit | commitdiff | tree |
| 2013-09-27 |
Andrew Reynolds | Add new symmetry breaking technique for finite model...
|
commit | commitdiff | tree |
| 2013-09-15 |
Andrew Reynolds | Change default option of simple ite lifting within...
|
commit | commitdiff | tree |
| 2013-09-09 |
Andrew Reynolds | Another minor fix for datatypes to repair my previous...
|
commit | commitdiff | tree |
| 2013-09-07 |
Andrew Reynolds | Fix datatypes for bug 503
|
commit | commitdiff | tree |
| 2013-08-13 |
Andrew Reynolds | Minor fixes for --fmf-fmc for quantifiers containing...
|
commit | commitdiff | tree |
| 2013-08-13 |
Andrew Reynolds | initial modifications for per-ic cbqi
|
commit | commitdiff | tree |
| 2013-07-22 |
Andrew Reynolds | Add option --cbqi-recurse.
|
commit | commitdiff | tree |
| 2013-07-22 |
Andrew Reynolds | Bug fix for --fmf-fmc for non-uninterpreted sort quantifiers...
|
commit | commitdiff | tree |
| 2013-07-18 |
Andrew Reynolds | Fix quantifier instantiation bug in cbqi, add default...
|
commit | commitdiff | tree |
| 2013-07-09 |
Andrew Reynolds | add relevant domain computation
|
commit | commitdiff | tree |
| 2013-07-02 |
Andrew Reynolds | Make uf strong solver user-context dependent, fixes...
|
commit | commitdiff | tree |
| 2013-07-02 |
Andrew Reynolds | Minor fixes for bounded integers, rewrite engine.
|
commit | commitdiff | tree |
| 2013-06-28 |
Andrew Reynolds | More bug fixes for interval models.
|
commit | commitdiff | tree |
| 2013-06-26 |
Andrew Reynolds | Add support for interval models in bounded integers...
|
commit | commitdiff | tree |
| 2013-06-25 |
Andrew Reynolds | Refactoring of model engine to separate individual...
|
commit | commitdiff | tree |
| 2013-06-24 |
Andrew Reynolds | Add options for symmetry breaking in uf+ss totality...
|
commit | commitdiff | tree |
| 2013-06-17 |
Andrew Reynolds | Make --var-elim-quant true by default. Add rewrite...
|
commit | commitdiff | tree |
| 2013-06-16 |
Andrew Reynolds | Fix in SMT2 parser for parametric datatypes
|
commit | commitdiff | tree |
| 2013-06-05 |
Andrew Reynolds | Fix bug in --fmf-fmc for producing models of functions...
|
commit | commitdiff | tree |
| 2013-06-04 |
Andrew Reynolds | Add partial support for MBQI with arrays when using...
|
commit | commitdiff | tree |
| 2013-05-23 |
Andrew Reynolds | Refactoring to prepare for MBQI with integer quantification...
|
commit | commitdiff | tree |
| 2013-05-22 |
Andrew Reynolds | Merge branch 'master' of https://github.com/CVC4/CVC4
|
commit | commitdiff | tree |
| 2013-05-22 |
Andrew Reynolds | Significant work on bounded integer quantification...
|
commit | commitdiff | tree |
| 2013-05-22 |
Andrew Reynolds | Add regressions for finite model finding
|
commit | commitdiff | tree |
| 2013-05-20 |
Andrew Reynolds | Possible final version of run scripts for casc.
|
commit | commitdiff | tree |
| 2013-05-17 |
Andrew Reynolds | Add model-producing run script for casc.
|
commit | commitdiff | tree |
| 2013-05-17 |
Andrew Reynolds | Add support for --dump-models option, in preparation...
|
commit | commitdiff | tree |
| 2013-05-16 |
Andrew Reynolds | Fix minor bug in full_model_check.cpp
|
commit | commitdiff | tree |
| 2013-05-14 |
Andrew Reynolds | Update casc24-fnt run script. Add casc24-fof run script.
|
commit | commitdiff | tree |
| 2013-05-14 |
Andrew Reynolds | Add support for quantifier patterns in smt2 printer.
|
commit | commitdiff | tree |
| 2013-05-14 |
Andrew Reynolds | Refactoring to separate old and new model building...
|
commit | commitdiff | tree |
| 2013-05-11 |
Andrew Reynolds | Preliminary version of finite model finding over bounded...
|
commit | commitdiff | tree |
| 2013-05-10 |
Andrew Reynolds | Update casc run script. Work on compliance for SZS...
|
commit | commitdiff | tree |
| 2013-05-10 |
Andrew Reynolds | Add simplification option --fo-prop-quant. Add model...
|
commit | commitdiff | tree |
| 2013-05-09 |
Andrew Reynolds | Add new method for checking candidate models, --fmf...
|
commit | commitdiff | tree |
| 2013-04-30 |
Andrew Reynolds | Add option in quantifiers for clause splitting
|
commit | commitdiff | tree |
| 2013-04-03 |
Andrew Reynolds | abort quantifiers check if master equality engine is...
|
commit | commitdiff | tree |
| 2013-03-30 |
Andrew Reynolds | do simple ite rewriting within quantifiers
|
commit | commitdiff | tree |
| 2013-03-15 |
Andrew Reynolds | changed default option for quantifier instantiation
|
commit | commitdiff | tree |
| 2013-03-11 |
Andrew Reynolds | ite removal option for quantifiers --ite-remove-quant...
|
commit | commitdiff | tree |
| 2013-03-06 |
Andrew Reynolds | fixed two bugs for the new E-matching implementation...
|
commit | commitdiff | tree |
| 2013-02-24 |
Andrew Reynolds | added option --model-u-dt-enum for outputting uninterpreted...
|
commit | commitdiff | tree |
| 2013-02-05 |
Andrew Reynolds | More improvements for E-matching
|
commit | commitdiff | tree |
| 2013-02-04 |
Andrew Reynolds | Model no longer adds subterms of quantifiers to equality...
|
commit | commitdiff | tree |
| 2013-01-29 |
Andrew Reynolds | currently disabling bug486 regression. we need to...
|
commit | commitdiff | tree |
| 2013-01-29 |
Andrew Reynolds | fix for finite model finding caused by new collectModelInfo...
|
commit | commitdiff | tree |
| 2013-01-28 |
Andrew Reynolds | made QuantifiersEngine::d_inst_match_trie and QuantifiersEng...
|
commit | commitdiff | tree |
| 2013-01-27 |
Andrew Reynolds | some fixes for Intel benchmarks regarding quantifiers...
|
commit | commitdiff | tree |
| 2012-12-11 |
Andrew Reynolds | adding cache for preprocessing datatypes terms to fix...
|
commit | commitdiff | tree |
| 2012-12-01 |
Andrew Reynolds | drastic simplification of quantifiers code regarding...
|
commit | commitdiff | tree |
| 2012-11-30 |
Andrew Reynolds | quantifiers now uses master equality engine, preparation...
|
commit | commitdiff | tree |
| 2012-11-30 |
Andrew Reynolds | parametric datatypes fix related to non-ascribed type...
|
commit | commitdiff | tree |
| 2012-11-29 |
Andrew Reynolds | require type ascriptions for parametric datatype constructor...
|
commit | commitdiff | tree |
| 2012-11-29 |
Andrew Reynolds | fixes bug 438, incorporate subtypes into type unification...
|
commit | commitdiff | tree |
| 2012-11-18 |
Andrew Reynolds | support for quantifiers macros, bug fix for bug 454...
|
commit | commitdiff | tree |
| 2012-11-14 |
Andrew Reynolds | replaced all static member data from rewrite rule triggers...
|
commit | commitdiff | tree |
| 2012-11-13 |
Andrew Reynolds | refactoring of quantifiers rewriter based on code review...
|
commit | commitdiff | tree |
| 2012-11-12 |
Andrew Reynolds | minor bug fixes for quantifiers, added sort inference...
|
commit | commitdiff | tree |
| 2012-11-08 |
Andrew Reynolds | added support for parametric datatypes in smt2 parser...
|
commit | commitdiff | tree |
| 2012-11-02 |
Andrew Reynolds | more minor updates to inst gen and representative selection...
|
commit | commitdiff | tree |
| 2012-10-31 |
Andrew Reynolds | cleaning up some of the equality query stuff, implemented...
|
commit | commitdiff | tree |
| 2012-10-29 |
Andrew Reynolds | more updates and minor bug fixes for fmf/inst-gen quantifier...
|
commit | commitdiff | tree |
| 2012-10-26 |
Andrew Reynolds | bug fix for parametric datatypes, previously datatypes...
|
commit | commitdiff | tree |
| next |
projects / cvc5.git / search