| 2014-09-03 |
ajreynol | Implement and enable --dt-var-exp-quant, cleanup trace...
|
commit | commitdiff | tree |
| 2014-09-03 |
ajreynol | Work on conjecture generator : do not generalize subterms...
|
commit | commitdiff | tree |
| 2014-08-29 |
ajreynol | Set instantiation level on skolemized bodies of quantifiers...
|
commit | commitdiff | tree |
| 2014-08-29 |
ajreynol | Do not use pure theory terms as single triggers. Minor...
|
commit | commitdiff | tree |
| 2014-08-27 |
ajreynol | Fix assertion in rep_set.cpp, avoid full check in datatypes...
|
commit | commitdiff | tree |
| 2014-08-26 |
ajreynol | Bug fixes for --purify-triggers, --dt-force-assignment.
|
commit | commitdiff | tree |
| 2014-08-25 |
ajreynol | New option --purify-triggers. Refactoring of InstMatchGener...
|
commit | commitdiff | tree |
| 2014-08-21 |
ajreynol | Avoid doing work in quantifiers engine when no quantifiers...
|
commit | commitdiff | tree |
| 2014-08-20 |
ajreynol | Fix --inst-max-level for strategies that use arbitrary...
|
commit | commitdiff | tree |
| 2014-08-20 |
ajreynol | Update bv proof signature and example, after discussions...
|
commit | commitdiff | tree |
| 2014-08-20 |
ajreynol | Add option for inductive strengthening based on well...
|
commit | commitdiff | tree |
| 2014-08-18 |
ajreynol | Add support for quantifier-specific instantiation levels...
|
commit | commitdiff | tree |
| 2014-08-08 |
ajreynol | Add draft of BV proof signature (incomplete) and example...
|
commit | commitdiff | tree |
| 2014-08-05 |
ajreynol | Minor fix : do not drop instantiation patterns when...
|
commit | commitdiff | tree |
| 2014-08-01 |
ajreynol | Minor cleanup from previous commit. Better organization...
|
commit | commitdiff | tree |
| 2014-07-31 |
ajreynol | New module for generating candidate equality conjectures...
|
commit | commitdiff | tree |
| 2014-07-25 |
ajreynol | Minor bug fix for exhaustive instantiation in model_engine.
|
commit | commitdiff | tree |
| 2014-07-19 |
ajreynol | Minor fix for explanations for co-datatypes. Bug fix...
|
commit | commitdiff | tree |
| 2014-06-25 |
Andrew Reynolds | Merge pull request #34 from mdeters/datatypes-kinds
|
commit | commitdiff | tree |
| 2014-06-25 |
Andrew Reynolds | Merge pull request #37 from mdeters/quants-kinds
|
commit | commitdiff | tree |
| 2014-06-25 |
Andrew Reynolds | Merge pull request #38 from mdeters/uf-kinds
|
commit | commitdiff | tree |
| 2014-06-23 |
ajreynol | Make language explicit in casc scripts
|
commit | commitdiff | tree |
| 2014-05-28 |
Andrew Reynolds | Add option to avoid dumping partial models/proofs.
|
commit | commitdiff | tree |
| 2014-05-25 |
Andrew Reynolds | Improve quantifier instantiation: always use original...
|
commit | commitdiff | tree |
| 2014-05-23 |
Andrew Reynolds | Fix bug in E-matching Real/Int terms.
|
commit | commitdiff | tree |
| 2014-05-15 |
Andrew Reynolds | Minor fixes. Add SMTCOMP 2014 script.
|
commit | commitdiff | tree |
| 2014-05-14 |
Andrew Reynolds | Finish --dump-instantiations option. Update scripts.
|
commit | commitdiff | tree |
| 2014-05-12 |
Andrew Reynolds | Minor updates/fix to --cbqi-recurse
|
commit | commitdiff | tree |
| 2014-05-11 |
Andrew Reynolds | More preparation for CASC proofs. Minor fix for sort...
|
commit | commitdiff | tree |
| 2014-05-10 |
Andrew Reynolds | Bug fixes to CBQI. Add first draft of CASC j7 TFF...
|
commit | commitdiff | tree |
| 2014-05-09 |
Andrew Reynolds | Initial draft of run scripts for CASC j7
|
commit | commitdiff | tree |
| 2014-05-09 |
Andrew Reynolds | Add variable ordering to ambqi. Bug fix to macros...
|
commit | commitdiff | tree |
| 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-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-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-03 |
Andrew Reynolds | Added support for converting unsorted problems to multi...
|
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 |
| next |
projects / cvc5.git / search