| 2016-03-22 |
ajreynol | Bug fix for define functions + incremental. Minor work... |
tree | commitdiff |
| 2016-03-22 |
Tim King | New version of the recursive options parsing strategy. |
tree | commitdiff |
| 2016-03-18 |
ajreynol | Limit duplicate propagating instances to avoid exponent... |
tree | commitdiff |
| 2016-03-12 |
ajreynol | Add options related to interleaving quantifiers and... |
tree | commitdiff |
| 2016-03-08 |
ajreynol | Extend synthesis solver to handle single invocation... |
tree | commitdiff |
| 2016-03-07 |
ajreynol | Minor change to F-Length inference in strings. No inter... |
tree | commitdiff |
| 2016-03-02 |
ajreynol | Work towards complete instantiation for datatypes. |
tree | commitdiff |
| 2016-03-01 |
ajreynol | Shorter explanations for strings based on tracking... |
tree | commitdiff |
| 2016-02-26 |
ajreynol | Refactoring of inferences in strings. Add several options. |
tree | commitdiff |
| 2016-02-23 |
ajreynol | Fix term database for non-equal, congruent terms in... |
tree | commitdiff |
| 2016-02-19 |
ajreynol | Fixes and improvements for datatypes properties and... |
tree | commitdiff |
| 2016-02-19 |
ajreynol | Implement dynamic splitting for quantified formulas... |
tree | commitdiff |
| 2016-02-18 |
ajreynol | Correct subtyping for arrays, disable subtyping for... |
tree | commitdiff |
| 2016-02-15 |
ajreynol | Eliminate most of the internal representation infrastru... |
tree | commitdiff |
| 2016-02-11 |
ajreynol | More aggressive conditional rewriting for quantified... |
tree | commitdiff |
| 2016-02-10 |
ajreynol | Fix model postprocessor for tuples, add regression. |
tree | commitdiff |
| 2016-02-09 |
ajreynol | Fix regression, minor change to output. |
tree | commitdiff |
| 2016-02-08 |
ajreynol | Updates related to finite model finding and (co)datatyp... |
tree | commitdiff |
| 2016-02-02 |
Tim King | Moving dump.*, command.*, model.*, and ite_removal... |
tree | commitdiff |
| 2016-02-01 |
ajreynol | Simplify fmc model construction, add regression. Improv... |
tree | commitdiff |
| 2016-01-28 |
Tim King | Adding listeners to Options. |
tree | commitdiff |
| 2016-01-27 |
Liana Hadarean | Merged bit-vector and uf proof branch. |
tree | commitdiff |
| 2016-01-20 |
ajreynol | Fix bug in fmc mbqi where modelscomputed for mbqi could... |
tree | commitdiff |
| 2016-01-19 |
ajreynol | Bug fixes for model construction with codatatypes,... |
tree | commitdiff |
| 2016-01-18 |
ajreynol | Bug fix rewriter for fun defs. |
tree | commitdiff |
| 2016-01-14 |
ajreynol | Ensure model construction for parametric sorts involvin... |
tree | commitdiff |
| 2016-01-09 |
Tim King | Adding a new Listener utility class. Changing the Resou... |
tree | commitdiff |
| 2016-01-09 |
Tim King | Removing StatisticsRegistry's static functions current... |
tree | commitdiff |
| 2016-01-06 |
Tim King | Improving the documentation of the CVC command CONTINUE. |
tree | commitdiff |
| 2016-01-06 |
Tim King | Removing dead code. StackingMap only appeared in unit... |
tree | commitdiff |
| 2016-01-06 |
Tim King | Moving sexpr.{cpp,h,i} from expr/ back into util/. |
tree | commitdiff |
| 2016-01-06 |
Tim King | Add SmtGlobals Class |
tree | commitdiff |
| 2015-12-30 |
Tim King | Shuffling around public vs. private headers |
tree | commitdiff |
| 2015-12-27 |
Clark Barrett | Merged my changes from experimental branch (new array... |
tree | commitdiff |
| 2015-12-24 |
Tim King | Miscellaneous fixes |
tree | commitdiff |
| 2015-12-22 |
ajreynol | Always split on constructor types for datatypes involvi... |
tree | commitdiff |
| 2015-12-22 |
ajreynol | Bug fix for cbqi, do not use model values for terms... |
tree | commitdiff |
| 2015-12-19 |
Tim King | Modifying emptyset.h and sexpr. Adding SetLanguage. |
tree | commitdiff |
| 2015-12-15 |
Tim King | Refactoring Options Handler & Library Cycle Breaking |
tree | commitdiff |
| 2015-11-25 |
ajreynol | Infrastructure for partially single invocation properti... |
tree | commitdiff |
| 2015-11-24 |
Tim King | Adding a missing delete to smt2_compliance. |
tree | commitdiff |
| 2015-11-11 |
ajreynol | Minor fixes to cbqi, purify-quant. Better error checkin... |
tree | commitdiff |
| 2015-11-10 |
ajreynol | Fix infinite loop in datatype enumerator. Minor fixes... |
tree | commitdiff |
| 2015-11-07 |
Tim King | Changing file permissions to add or remove executable... |
tree | commitdiff |
| 2015-11-05 |
Tim King | Merging the google branch back into master. |
tree | commitdiff |
| 2015-11-05 |
Tim King | Fixes some initialization and desctruction problems... |
tree | commitdiff |
| 2015-11-04 |
ajreynol | Better combination of UF with cbqi, refactor quantifier... |
tree | commitdiff |
| 2015-10-31 |
ajreynol | Improvements to handling of mixed Int/Real quantifiers. |
tree | commitdiff |
| 2015-10-26 |
ajreynol | Extend counterexample-guided instantiation to extended... |
tree | commitdiff |
| 2015-10-22 |
ajreynol | Enable counterexample-guided quantifier instantiation... |
tree | commitdiff |
| 2015-10-19 |
ajreynol | Clean up explanations involving string length. Add... |
tree | commitdiff |
| 2015-10-19 |
ajreynol | Improve stratification of strings extended function... |
tree | commitdiff |
| 2015-10-16 |
ajreynol | Fix for codatatype constant rewrite, add regression. |
tree | commitdiff |
| 2015-10-15 |
ajreynol | Fix congruence check in strings, fixes bug 686. |
tree | commitdiff |
| 2015-10-12 |
Kshitij Bansal | Merge pull request #76 from CVC4/proofs |
tree | commitdiff |
| 2015-10-11 |
Kshitij Bansal | fix regression tests, support fallback mode for proofs |
tree | commitdiff |
| 2015-10-11 |
ajreynol | Fix strings preprocessing + incremental, fixes bug... |
tree | commitdiff |
| 2015-10-06 |
ajreynol | More improvements to strings rewriter for regexps,... |
tree | commitdiff |
| 2015-10-02 |
ajreynol | Improvements to rewriter for regexp, contains, indexof... |
tree | commitdiff |
| 2015-09-29 |
ajreynol | Fix for fmf+incremental. Restrict cbqi to literals... |
tree | commitdiff |
| 2015-09-28 |
ajreynol | Improve quantifiers engine wrt incremental presolve... |
tree | commitdiff |
| 2015-09-28 |
ajreynol | Minor fixes to strings, add regressions. |
tree | commitdiff |
| 2015-09-28 |
ajreynol | Add missing regression |
tree | commitdiff |
| 2015-09-28 |
ajreynol | Fix bug for trivial extf inferences in strings. Improve... |
tree | commitdiff |
| 2015-09-27 |
ajreynol | Improved handling of extended operators. Do preprocess... |
tree | commitdiff |
| 2015-09-26 |
ajreynol | Lazy preprocessing of extended operators in strings... |
tree | commitdiff |
| 2015-09-25 |
ajreynol | Clear term caches for quantifiers + incremental, fixes... |
tree | commitdiff |
| 2015-09-24 |
ajreynol | Counterexample-guided instantiation for datatypes.... |
tree | commitdiff |
| 2015-09-17 |
ajreynol | Allow most smt2 commands as sygus commands. Fix bug... |
tree | commitdiff |
| 2015-09-15 |
ajreynol | Fix bug related to quantifiers + incremental, thanks... |
tree | commitdiff |
| 2015-09-10 |
ajreynol | Models for codatatypes. Fixes bug 662. |
tree | commitdiff |
| 2015-09-09 |
ajreynol | Fix bug in strings rewriter regarding lengths of substr... |
tree | commitdiff |
| 2015-09-05 |
ajreynol | Fix bugs related to fmf with incremental. Reinitialize... |
tree | commitdiff |
| 2015-09-04 |
ajreynol | Fix bugs 605 and 667. |
tree | commitdiff |
| 2015-09-02 |
Kshitij Bansal | fix regressions |
tree | commitdiff |
| 2015-09-02 |
Kshitij Bansal | Merge remote-tracking branch 'origin/master' |
tree | commitdiff |
| 2015-08-27 |
ajreynol | Modify slow regressions. |
tree | commitdiff |
| 2015-08-24 |
ajreynol | Improvements to vts in cbqi, bug fix vts for non-atomic... |
tree | commitdiff |
| 2015-08-21 |
ajreynol | Fix disequality bounds in cbqi, record literals for... |
tree | commitdiff |
| 2015-08-19 |
Kshitij Bansal | fix bug 605 |
tree | commitdiff |
| 2015-08-19 |
ajreynol | Implementation of model-based projection in cbqi, clean... |
tree | commitdiff |
| 2015-08-16 |
ajreynol | More optimizations to --macros-quant, add --macros... |
tree | commitdiff |
| 2015-08-12 |
ajreynol | Improvements to --macros-quant. Enable --clause-split... |
tree | commitdiff |
| 2015-08-01 |
ajreynol | Support for default grammar for datatypes in sygus... |
tree | commitdiff |
| 2015-07-31 |
ajreynol | Make --fmf-fun and --macros-quant work in incremental... |
tree | commitdiff |
| 2015-07-31 |
ajreynol | Sygus support for inductive datatypes. |
tree | commitdiff |
| 2015-07-30 |
ajreynol | Implement virtual term substitution for non-nested... |
tree | commitdiff |
| 2015-07-28 |
Tianyi Liang | Disable bug590.smt2 |
tree | commitdiff |
| 2015-07-28 |
Tianyi Liang | Merge branch 'master' of https://github.com/CVC4/CVC4 |
tree | commitdiff |
| 2015-07-25 |
ajreynol | Add option --sygus-inv-templ for synthesizing strengthe... |
tree | commitdiff |
| 2015-07-20 |
ajreynol | Squashed merge of SygusComp 2015 branch. |
tree | commitdiff |
| 2015-06-27 |
ajreynol | Refactor various corner cases of fmf, quantifiers modul... |
tree | commitdiff |
| 2015-06-11 |
ajreynol | Avoid naming conflicts in sygus, refactor. Add missing... |
tree | commitdiff |
| 2015-06-11 |
ajreynol | Handle duplicate operators in sygus grammars. Parse... |
tree | commitdiff |
| 2015-06-11 |
ajreynol | Update experimental scripts. Support top-level non... |
tree | commitdiff |
| 2015-06-10 |
ajreynol | Support for printing solutions involving LetGTerm sygus... |
tree | commitdiff |
| 2015-06-02 |
ajreynol | Flatten sygus grammars during parsing. Remove duplicate... |
tree | commitdiff |
| 2015-06-01 |
ajreynol | When proof enabled, disable uf sym break. Add regression. |
tree | commitdiff |
| 2015-05-27 |
lianah | Merge pull request #75 from Dunedune/master |
tree | commitdiff |
| 2015-05-25 |
ajreynol | Add missing regression |
tree | commitdiff |
| next |
projects / cvc5.git / history