| 2016-06-03 |
ajreynol | Remove NodeListMap from strings, fixes memory leaks...
|
commit | commitdiff | tree |
| 2016-06-03 |
ajreynol | Simple memory fixes, minor cleanup in quantifiers.
|
commit | commitdiff | tree |
| 2016-06-03 |
ajreynol | Reduce number of passes in quantifiers rewriter.
|
commit | commitdiff | tree |
| 2016-06-01 |
ajreynol | Fix to ignore a case of triggers with no free variables.
|
commit | commitdiff | tree |
| 2016-06-01 |
ajreynol | Initial infrastructure for bounded set quantification...
|
commit | commitdiff | tree |
| 2016-05-26 |
ajreynol | Use term indexing in TheoryUF::computeCareGraph. Do...
|
commit | commitdiff | tree |
| 2016-05-24 |
ajreynol | Improvements to symmetry breaking in sygus search....
|
commit | commitdiff | tree |
| 2016-05-23 |
ajreynol | Fix related to parametric sorts whose interpretation...
|
commit | commitdiff | tree |
| 2016-05-21 |
ajreynol | Minor fix for strings.
|
commit | commitdiff | tree |
| 2016-05-20 |
ajreynol | Minor fix to strings, cleanup in datatypes.
|
commit | commitdiff | tree |
| 2016-05-20 |
ajreynol | Improvements to theory combination + strings: do not...
|
commit | commitdiff | tree |
| 2016-05-18 |
ajreynol | Refactor modes for sygus+single invocation. Add option...
|
commit | commitdiff | tree |
| 2016-05-17 |
ajreynol | Minor fix cbqi for constant monomials.
|
commit | commitdiff | tree |
| 2016-05-16 |
ajreynol | Enable --sygus-direct-eval by default, limit to terms...
|
commit | commitdiff | tree |
| 2016-05-15 |
ajreynol | Work on --sygus-direct-eval. Minor optimizations, updates...
|
commit | commitdiff | tree |
| 2016-05-12 |
ajreynol | Add casc scripts. Improvements to qcf related to nested...
|
commit | commitdiff | tree |
| 2016-05-10 |
ajreynol | Fix for --inst-max-level
|
commit | commitdiff | tree |
| 2016-05-10 |
ajreynol | Add smt comp 2016 scripts. Fix for --relevant-triggers...
|
commit | commitdiff | tree |
| 2016-05-06 |
ajreynol | Minor clean up, fixes related to sygus.
|
commit | commitdiff | tree |
| 2016-05-05 |
ajreynol | Compute term indices lazily in TermDb. Optimization...
|
commit | commitdiff | tree |
| 2016-05-02 |
ajreynol | Clean up issues related to compiled scc in LFSC. Refactor...
|
commit | commitdiff | tree |
| 2016-04-28 |
ajreynol | More work on inst propagate. Optimization for qcf...
|
commit | commitdiff | tree |
| 2016-04-14 |
ajreynol | Add option --snorm-infer-eq to infer equalities based...
|
commit | commitdiff | tree |
| 2016-04-14 |
ajreynol | Add missing function for regexp to expr manager.
|
commit | commitdiff | tree |
| 2016-04-13 |
ajreynol | Update native language support for strings.
|
commit | commitdiff | tree |
| 2016-04-13 |
ajreynol | Minor improvements for alpha equivalence and partial...
|
commit | commitdiff | tree |
| 2016-04-13 |
ajreynol | Handle parametric datatypes with --quant-ind. Minor...
|
commit | commitdiff | tree |
| 2016-04-12 |
ajreynol | Bug fixes related to parametric datatypes + theory...
|
commit | commitdiff | tree |
| 2016-04-12 |
ajreynol | Optimizations for QCF to check relevant domain of variable...
|
commit | commitdiff | tree |
| 2016-04-11 |
ajreynol | Minor fixes for inst match generators. Updates to qip.
|
commit | commitdiff | tree |
| 2016-04-10 |
ajreynol | More work on instantiation propagation. Enable external...
|
commit | commitdiff | tree |
| 2016-04-09 |
ajreynol | Minor refactoring of entailment tests and quantifiers...
|
commit | commitdiff | tree |
| 2016-04-07 |
ajreynol | Refactor trigger selection, revisions to --relational...
|
commit | commitdiff | tree |
| 2016-04-04 |
ajreynol | New options for trigger selection, add option --strict...
|
commit | commitdiff | tree |
| 2016-04-01 |
ajreynol | Improvements to equality inference module: add missing...
|
commit | commitdiff | tree |
| 2016-03-31 |
ajreynol | Improvements to trigger selection, min triggers by...
|
commit | commitdiff | tree |
| 2016-03-30 |
ajreynol | Updates to E-matching to avoid entailed instantiations...
|
commit | commitdiff | tree |
| 2016-03-28 |
ajreynol | Minor cleanup from last commit (quant util, equality...
|
commit | commitdiff | tree |
| 2016-03-28 |
ajreynol | Implement equality inference module for arithmetic...
|
commit | commitdiff | tree |
| 2016-03-22 |
ajreynol | Bug fix for define functions + incremental. Minor work...
|
commit | commitdiff | tree |
| 2016-03-18 |
ajreynol | Limit duplicate propagating instances to avoid exponential...
|
commit | commitdiff | tree |
| 2016-03-16 |
ajreynol | Change internal representative selection for finite...
|
commit | commitdiff | tree |
| 2016-03-12 |
ajreynol | Add options related to interleaving quantifiers and...
|
commit | commitdiff | tree |
| 2016-03-10 |
ajreynol | Faster conditional rewriting for and/or beneath quantifiers...
|
commit | commitdiff | tree |
| 2016-03-08 |
ajreynol | Extend synthesis solver to handle single invocation...
|
commit | commitdiff | tree |
| 2016-03-07 |
ajreynol | Minor change to F-Length inference in strings. No internal...
|
commit | commitdiff | tree |
| 2016-03-03 |
ajreynol | Add missing code to track dependencies recursively...
|
commit | commitdiff | tree |
| 2016-03-02 |
ajreynol | Work towards complete instantiation for datatypes.
|
commit | commitdiff | tree |
| 2016-03-01 |
ajreynol | Shorter explanations for strings based on tracking...
|
commit | commitdiff | tree |
| 2016-02-29 |
ajreynol | Minor options to datatypes.
|
commit | commitdiff | tree |
| 2016-02-26 |
ajreynol | Refactoring of inferences in strings. Add several options.
|
commit | commitdiff | tree |
| 2016-02-25 |
ajreynol | Minor improvement to partial qe. Add options for representat...
|
commit | commitdiff | tree |
| 2016-02-24 |
ajreynol | Add entailment checks between length terms to reduce...
|
commit | commitdiff | tree |
| 2016-02-23 |
ajreynol | Fix term database for non-equal, congruent terms in...
|
commit | commitdiff | tree |
| 2016-02-19 |
ajreynol | Fixes and improvements for datatypes properties and...
|
commit | commitdiff | tree |
| 2016-02-19 |
ajreynol | Implement dynamic splitting for quantified formulas...
|
commit | commitdiff | tree |
| 2016-02-18 |
ajreynol | Correct subtyping for arrays, disable subtyping for...
|
commit | commitdiff | tree |
| 2016-02-17 |
ajreynol | Refactor quantifiers attributes. Make quantifier elimination...
|
commit | commitdiff | tree |
| 2016-02-16 |
ajreynol | Public interface for quantifier elimination. Minor...
|
commit | commitdiff | tree |
| 2016-02-16 |
ajreynol | More simplification to internal implementation of tuples...
|
commit | commitdiff | tree |
| 2016-02-15 |
ajreynol | Minor change to last commit
|
commit | commitdiff | tree |
| 2016-02-15 |
ajreynol | Eliminate most of the internal representation infrastructure...
|
commit | commitdiff | tree |
| 2016-02-11 |
ajreynol | More aggressive conditional rewriting for quantified...
|
commit | commitdiff | tree |
| 2016-02-10 |
ajreynol | Fix model postprocessor for tuples, add regression.
|
commit | commitdiff | tree |
| 2016-02-09 |
ajreynol | Fix regression, minor change to output.
|
commit | commitdiff | tree |
| 2016-02-09 |
ajreynol | Eager introduction of eqc, lemma cache for ground fmf...
|
commit | commitdiff | tree |
| 2016-02-08 |
ajreynol | Updates related to finite model finding and (co)datatypes...
|
commit | commitdiff | tree |
| 2016-02-05 |
ajreynol | Add two optimizations for datatypes, currently disabled...
|
commit | commitdiff | tree |
| 2016-02-01 |
ajreynol | Simplify fmc model construction, add regression. Improve...
|
commit | commitdiff | tree |
| 2016-01-20 |
ajreynol | Fix bug in fmc mbqi where modelscomputed for mbqi could...
|
commit | commitdiff | tree |
| 2016-01-18 |
ajreynol | Bug fix rewriter for fun defs.
|
commit | commitdiff | tree |
| 2016-01-15 |
ajreynol | Type enumerators take optional argument indicating...
|
commit | commitdiff | tree |
| 2016-01-14 |
ajreynol | Ensure model construction for parametric sorts involving...
|
commit | commitdiff | tree |
| 2016-01-13 |
ajreynol | Lemma cache datatypes. Do not send true lemma in quantifiers...
|
commit | commitdiff | tree |
| 2015-12-22 |
ajreynol | Bug fix uf-ss-totality.
|
commit | commitdiff | tree |
| 2015-12-22 |
ajreynol | Always split on constructor types for datatypes involving...
|
commit | commitdiff | tree |
| 2015-12-22 |
ajreynol | Bug fix for cbqi, do not use model values for terms...
|
commit | commitdiff | tree |
| 2015-12-17 |
ajreynol | Minor
|
commit | commitdiff | tree |
| 2015-12-16 |
ajreynol | Work on purification for quantifiers, minor updates.
|
commit | commitdiff | tree |
| 2015-12-15 |
ajreynol | Add option uf-ss-fair-monotone. Minor cleanup and improvemen...
|
commit | commitdiff | tree |
| 2015-12-10 |
ajreynol | Add option fmf-empty-sorts.
|
commit | commitdiff | tree |
| 2015-12-02 |
ajreynol | Minor fixes for cegqi-si-partial.
|
commit | commitdiff | tree |
| 2015-12-01 |
ajreynol | More work on --cegqi-si-partial, incomplete.
|
commit | commitdiff | tree |
| 2015-11-28 |
ajreynol | Initial work on --cegqi-si-partial, refactoring.
|
commit | commitdiff | tree |
| 2015-11-26 |
ajreynol | Update to new implementation of single invocation partition...
|
commit | commitdiff | tree |
| 2015-11-26 |
ajreynol | Front-end support for get-value of sort cardinality...
|
commit | commitdiff | tree |
| 2015-11-25 |
ajreynol | Infrastructure for partially single invocation properties...
|
commit | commitdiff | tree |
| 2015-11-18 |
ajreynol | Option for midpoints in cbqi.
|
commit | commitdiff | tree |
| 2015-11-17 |
ajreynol | Improve relevant domain computation for arithmetic...
|
commit | commitdiff | tree |
| 2015-11-12 |
ajreynol | Minor fixes and improvements to purify quant, relational...
|
commit | commitdiff | tree |
| 2015-11-11 |
ajreynol | Minor fixes to cbqi, purify-quant. Better error checking...
|
commit | commitdiff | tree |
| 2015-11-10 |
ajreynol | Fix infinite loop in datatype enumerator. Minor fixes...
|
commit | commitdiff | tree |
| 2015-11-04 |
ajreynol | Better combination of UF with cbqi, refactor quantifiers...
|
commit | commitdiff | tree |
| 2015-10-31 |
ajreynol | Improvements to handling of mixed Int/Real quantifiers.
|
commit | commitdiff | tree |
| 2015-10-26 |
ajreynol | Promote InstStrategyCbqi to quantifier module. Cleanup...
|
commit | commitdiff | tree |
| 2015-10-26 |
ajreynol | Extend counterexample-guided instantiation to extended...
|
commit | commitdiff | tree |
| 2015-10-24 |
ajreynol | Fixes related to string contains.
|
commit | commitdiff | tree |
| 2015-10-22 |
ajreynol | Enable counterexample-guided quantifier instantiation...
|
commit | commitdiff | tree |
| 2015-10-21 |
ajreynol | Minor refactoring in strings related to length.
|
commit | commitdiff | tree |
| 2015-10-20 |
ajreynol | Refactor strings, remove old cycle checks in normalize...
|
commit | commitdiff | tree |
| next |
projects / cvc5.git / search