| 2014-05-08 |
Andrew Reynolds | Fixes to quantifiers rewriter to prevent miniscoping...
|
commit | commitdiff | tree |
| 2014-05-08 |
Andrew Reynolds | Basic optimizations for ambqi : only normalize UF applied...
|
commit | commitdiff | tree |
| 2014-05-07 |
Andrew Reynolds | Fixes to ambqi, now solution-sound.
|
commit | commitdiff | tree |
| 2014-05-06 |
Andrew Reynolds | First draft of ambqi_builder (new implementation of...
|
commit | commitdiff | tree |
| 2014-05-02 |
Andrew Reynolds | Simplification of EqualityEngine::areDisequal. Comparison...
|
commit | commitdiff | tree |
| 2014-05-02 |
Andrew Reynolds | Add option --dt-stc-ind for strengthening skolemization...
|
commit | commitdiff | tree |
| 2014-04-28 |
Andrew Reynolds | Preparation for models for co-inductive datatypes....
|
commit | commitdiff | tree |
| 2014-04-24 |
Andrew Reynolds | Add --inst-max-level=N option for Kshitij. Support...
|
commit | commitdiff | tree |
| 2014-04-22 |
Andrew Reynolds | Minor fix to avoid rewriting datatype equalities into...
|
commit | commitdiff | tree |
| 2014-04-17 |
Andrew Reynolds | Minor refactoring and optimizing.
|
commit | commitdiff | tree |
| 2014-04-14 |
Andrew Reynolds | Fix bug in mbqi=fmc handling theory symbols. Fix mbqi...
|
commit | commitdiff | tree |
| 2014-04-14 |
Andrew Reynolds | Add initial support for co-datatypes.
|
commit | commitdiff | tree |
| 2014-04-10 |
Andrew Reynolds | Expand definitions in theory datatypes, now has the...
|
commit | commitdiff | tree |
| 2014-04-10 |
Andrew Reynolds | Add support for cardinality constraints logic UFC....
|
commit | commitdiff | tree |
| 2014-04-09 |
Andrew Reynolds | Revert E-matching datatypes fix.
|
commit | commitdiff | tree |
| 2014-04-09 |
Andrew Reynolds | Handle fmf.card as input from user, add support in...
|
commit | commitdiff | tree |
| 2014-03-20 |
Andrew Reynolds | Minor fix for CBQI, ignore inst constant nodes.
|
commit | commitdiff | tree |
| 2014-03-19 |
Andrew Reynolds | Fix a memory leak in LFSC proof checker. Largest QF_UF...
|
commit | commitdiff | tree |
| 2014-03-14 |
Andrew Reynolds | Add ability to provide theory-specific proof rules...
|
commit | commitdiff | tree |
| 2014-03-13 |
Andrew Reynolds | Add working example of LFSC proof with quantifiers...
|
commit | commitdiff | tree |
| 2014-03-12 |
Andrew Reynolds | Work on array pf signature, add working example. Add...
|
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / search