| 2017-03-22 |
ajreynol | Fix more cases of rewritten explanations in strings...
|
commit | commitdiff | tree |
| 2017-03-22 |
ajreynol | Minor fix for bounded integers.
|
commit | commitdiff | tree |
| 2017-03-22 |
ajreynol | Work on new approach for sygus involving conditional...
|
commit | commitdiff | tree |
| 2017-03-21 |
ajreynol | Improve computeCareGraph functions to check shared...
|
commit | commitdiff | tree |
| 2017-03-16 |
ajreynol | More fixes, features to examples.
|
commit | commitdiff | tree |
| 2017-03-16 |
ajreynol | Minor fixes, always expand applications of lambdas...
|
commit | commitdiff | tree |
| 2017-03-16 |
ajreynol | Support for SMT LIB 2.6 syntax declare-datatype and...
|
commit | commitdiff | tree |
| 2017-03-16 |
ajreynol | Parsing support for SMT LIB 2.6. Minor fixes for printing...
|
commit | commitdiff | tree |
| 2017-03-15 |
ajreynol | Fix regress1 Makefile for rewriterules, fixes bug 783.
|
commit | commitdiff | tree |
| 2017-03-15 |
ajreynol | Allow 0 argument recursive functions. Fixes bug 782.
|
commit | commitdiff | tree |
| 2017-03-10 |
ajreynol | Minor fix for cbqi-all.
|
commit | commitdiff | tree |
| 2017-03-07 |
ajreynol | More fixes for printing/parsing sets, fix kind name.
|
commit | commitdiff | tree |
| 2017-03-07 |
ajreynol | Fix cvc parser for set compliment.
|
commit | commitdiff | tree |
| 2017-03-06 |
ajreynol | Do not eagerly construct explanations in relation solver.
|
commit | commitdiff | tree |
| 2017-03-06 |
ajreynol | Support for set compliment and universe set. Simplify...
|
commit | commitdiff | tree |
| 2017-03-03 |
ajreynol | Fix for collectModelInfo related to finite types +...
|
commit | commitdiff | tree |
| 2017-03-03 |
ajreynol | Another minor fix for sets related to sharing + finite...
|
commit | commitdiff | tree |
| 2017-03-02 |
ajreynol | Fixes related to sets.
|
commit | commitdiff | tree |
| 2017-03-02 |
ajreynol | Minor cleanup and reorganization related to last commit.
|
commit | commitdiff | tree |
| 2017-03-02 |
ajreynol | Eliminate Boolean term conversion. Generalizes removeITE...
|
commit | commitdiff | tree |
| 2017-02-16 |
ajreynol | Minor fixes for relations, quantifiers dsplit.
|
commit | commitdiff | tree |
| 2017-02-16 |
ajreynol | Fixes for sets+rels check. Minor.
|
commit | commitdiff | tree |
| 2017-02-15 |
ajreynol | Minimization modes for fmf bound.
|
commit | commitdiff | tree |
| 2017-02-07 |
ajreynol | Generalize finite bound inference to unifiable variables...
|
commit | commitdiff | tree |
| 2017-01-30 |
ajreynol | Fix regexp cache issue in strings, add regression.
|
commit | commitdiff | tree |
| 2017-01-18 |
ajreynol | Minor fix in relations.
|
commit | commitdiff | tree |
| 2017-01-13 |
ajreynol | Do not rewrite explanations in strings.
|
commit | commitdiff | tree |
| 2017-01-11 |
ajreynol | Fix for when variables are (partially) bound in multiple...
|
commit | commitdiff | tree |
| 2017-01-06 |
ajreynol | Minor fix for sets.
|
commit | commitdiff | tree |
| 2017-01-04 |
ajreynol | Fix for tff type declarations inTPTP parser, fixes...
|
commit | commitdiff | tree |
| 2016-12-08 |
ajreynol | Enable remaining cardinality benchmarks
|
commit | commitdiff | tree |
| 2016-12-08 |
ajreynol | Add missing regression
|
commit | commitdiff | tree |
| 2016-12-07 |
ajreynol | Add sets regression, fixes bug 754. Minor fix to regexp...
|
commit | commitdiff | tree |
| 2016-12-07 |
ajreynol | Added cardinality to cvc language, fixes bug 753. Throw...
|
commit | commitdiff | tree |
| 2016-12-07 |
ajreynol | Fix boolean term conversion for INST_ATTRIBUTE, fixes...
|
commit | commitdiff | tree |
| 2016-12-07 |
ajreynol | Refactoring, generalization of bounded inference module...
|
commit | commitdiff | tree |
| 2016-12-07 |
ajreynol | Fix nf exp tracking for non-linear string equalities...
|
commit | commitdiff | tree |
| 2016-12-06 |
ajreynol | Improve bounds for global heap in sep, refactor preprocessin...
|
commit | commitdiff | tree |
| 2016-12-03 |
ajreynol | Fix unit test for datatypes, add interface functions...
|
commit | commitdiff | tree |
| 2016-12-02 |
ajreynol | Bug fixes and refactoring of parametric datatypes,...
|
commit | commitdiff | tree |
| 2016-12-02 |
ajreynol | Refactor preprocessing of models in fmf. Fix options...
|
commit | commitdiff | tree |
| 2016-12-01 |
ajreynol | Fix quantifiers dynamic splitting module for incremental...
|
commit | commitdiff | tree |
| 2016-12-01 |
ajreynol | Improvement and bug fix for str.indexof reduction,...
|
commit | commitdiff | tree |
| 2016-11-22 |
ajreynol | Fix smt2 and cvc printers for testers when output and...
|
commit | commitdiff | tree |
| 2016-11-21 |
ajreynol | Refactoring related to track instantiation option.
|
commit | commitdiff | tree |
| 2016-11-14 |
ajreynol | Minor improvement to caching for extf bv inferences.
|
commit | commitdiff | tree |
| 2016-11-11 |
ajreynol | Add simple inferences for extended bitvector functions...
|
commit | commitdiff | tree |
| 2016-11-10 |
ajreynol | Add option for enabling/disabling lazy extended function...
|
commit | commitdiff | tree |
| 2016-11-09 |
ajreynol | Fix tptp parser memory leaks for include.
|
commit | commitdiff | tree |
| 2016-11-08 |
ajreynol | Minor fixes related to ExtTheory + incremental, fixes...
|
commit | commitdiff | tree |
| 2016-11-08 |
ajreynol | Add a few options to separation logic and sets. Minor...
|
commit | commitdiff | tree |
| 2016-11-04 |
ajreynol | Fix a few more minor memory leaks.
|
commit | commitdiff | tree |
| 2016-11-03 |
ajreynol | Make data points accurate in sep logic models.
|
commit | commitdiff | tree |
| 2016-11-03 |
ajreynol | Add priorities to getNextDecision. Properly handle...
|
commit | commitdiff | tree |
| 2016-11-02 |
ajreynol | Add missing regression.
|
commit | commitdiff | tree |
| 2016-11-02 |
ajreynol | Fix bug in separation logic for finite pto-data types...
|
commit | commitdiff | tree |
| 2016-11-02 |
ajreynol | Fix a few obvious memory leaks in sygus and quantifiers...
|
commit | commitdiff | tree |
| 2016-11-01 |
ajreynol | Minor fix to cvc3_compat.
|
commit | commitdiff | tree |
| 2016-11-01 |
ajreynol | Make tuple and record names unique. Do not print internal...
|
commit | commitdiff | tree |
| 2016-11-01 |
ajreynol | Fix memory leak in TheorySetsRels. Minor cleanup.
|
commit | commitdiff | tree |
| 2016-11-01 |
ajreynol | Revert change to Datatypes API to return vector of...
|
commit | commitdiff | tree |
| 2016-11-01 |
ajreynol | Revert change to datatypes API for passing pointers...
|
commit | commitdiff | tree |
| 2016-11-01 |
ajreynol | Working memory leak free version, changes interface...
|
commit | commitdiff | tree |
| 2016-10-31 |
ajreynol | Minor refactoring in preparation for datatypes node...
|
commit | commitdiff | tree |
| 2016-10-28 |
ajreynol | Add get instantiations utilities to API.
|
commit | commitdiff | tree |
| 2016-10-26 |
ajreynol | Enable bv2nat regressions
|
commit | commitdiff | tree |
| 2016-10-26 |
ajreynol | New implementation of sets+cardinality. Merge Paul...
|
commit | commitdiff | tree |
| 2016-10-21 |
ajreynol | Fix/add missing makefiles.
|
commit | commitdiff | tree |
| 2016-10-21 |
ajreynol | Move slow regress0 benchmarks to regress1, increment...
|
commit | commitdiff | tree |
| 2016-10-13 |
ajreynol | Merging bv parts of ajr/bvExt branch, minor additions...
|
commit | commitdiff | tree |
| 2016-10-01 |
ajreynol | Incorporate non-bv parts of ajr/bvExt branch
|
commit | commitdiff | tree |
| 2016-09-29 |
ajreynol | Address some coverity warnings, add another stat.
|
commit | commitdiff | tree |
| 2016-09-29 |
ajreynol | Minor cleanup and additions to quantifiers statistics.
|
commit | commitdiff | tree |
| 2016-09-21 |
ajreynol | Remove duplicate code from my last commit
|
commit | commitdiff | tree |
| 2016-09-20 |
ajreynol | Refactor, separate theory-specific counterexample-guided...
|
commit | commitdiff | tree |
| 2016-09-20 |
ajreynol | More refactoring of cbqi. Add a few regressions. Add...
|
commit | commitdiff | tree |
| 2016-09-18 |
ajreynol | Minor fix for strings
|
commit | commitdiff | tree |
| 2016-09-17 |
ajreynol | Use matching heuristics for EPR instantiation.
|
commit | commitdiff | tree |
| 2016-09-16 |
ajreynol | More refactoring of cbqi, start developing new interface.
|
commit | commitdiff | tree |
| 2016-09-15 |
ajreynol | Further refactor cbqi.
|
commit | commitdiff | tree |
| 2016-09-15 |
ajreynol | Begin refactoring of cbqi, remove a few dead options...
|
commit | commitdiff | tree |
| 2016-09-15 |
ajreynol | Make sep pto a trigger kind, track in equality engines...
|
commit | commitdiff | tree |
| 2016-09-15 |
ajreynol | Refactor setIncomplete in quantifiers.
|
commit | commitdiff | tree |
| 2016-09-14 |
ajreynol | Support for unique variable generation in node manager.
|
commit | commitdiff | tree |
| 2016-09-14 |
ajreynol | Lemma cache in theory sep. Minor optimization for sets...
|
commit | commitdiff | tree |
| 2016-09-13 |
ajreynol | Minor changes to sep logic, epr, quantifier splitting.
|
commit | commitdiff | tree |
| 2016-09-12 |
ajreynol | Refactor prenex modes.
|
commit | commitdiff | tree |
| 2016-09-12 |
ajreynol | Remove old implementation of cbqi
|
commit | commitdiff | tree |
| 2016-09-12 |
ajreynol | Prefer non-cardinality constants in term models for...
|
commit | commitdiff | tree |
| 2016-09-12 |
ajreynol | Ensure sep.nil is unique per type at NodeManager level...
|
commit | commitdiff | tree |
| 2016-09-09 |
ajreynol | Fix bug in unconstrained simplifier related to sep...
|
commit | commitdiff | tree |
| 2016-09-09 |
ajreynol | Support for separation logic + EPR. Refactor preprocessing...
|
commit | commitdiff | tree |
| 2016-09-08 |
ajreynol | Refactor seplog preprocess. Handle case where sep data...
|
commit | commitdiff | tree |
| 2016-09-03 |
ajreynol | Miniscope top level conjunctions for prenex normal...
|
commit | commitdiff | tree |
| 2016-09-03 |
ajreynol | Option for prenex normal form
|
commit | commitdiff | tree |
| 2016-09-01 |
ajreynol | Fix boolean term issue in invariants from sygus. Minor...
|
commit | commitdiff | tree |
| 2016-09-01 |
ajreynol | Cleanup quantifier elimination in smt engine.
|
commit | commitdiff | tree |
| 2016-09-01 |
ajreynol | Updates to cbqi. New strategy --cbqi-nested-qe to...
|
commit | commitdiff | tree |
| 2016-08-26 |
ajreynol | Basic support for EPR+CBQI. Minor cleanup.
|
commit | commitdiff | tree |
| 2016-08-25 |
ajreynol | Minor cleanup preprocessing, add ppNotifyAssertions.
|
commit | commitdiff | tree |
| next |
projects / cvc5.git / search