| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-11-05 | Merging the google branch back into master. | Tim King | |
| 2015-11-05 | Fixes some initialization and desctruction problems in quantifiers. Also ↵ | Tim King | |
| restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts. | |||
| 2015-11-04 | Better combination of UF with cbqi, refactor quantifiers intialization. | ajreynol | |
| 2015-10-31 | Improvements to handling of mixed Int/Real quantifiers. | ajreynol | |
| 2015-10-26 | Extend counterexample-guided instantiation to extended theory of Int/Real, ↵ | ajreynol | |
| mixed Int/Real. Bug fixes. Updates to quantifiers rewriter. | |||
| 2015-10-22 | Enable counterexample-guided quantifier instantiation by default for ↵ | ajreynol | |
| quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions. | |||
| 2015-10-20 | Clean up explanations involving string length. Add regression. | ajreynol | |
| 2015-10-19 | Improve stratification of strings extended function reductions, add ↵ | ajreynol | |
| regressions. Eliminate preprocess for regexp. | |||
| 2015-10-16 | Fix for codatatype constant rewrite, add regression. | ajreynol | |
| 2015-10-15 | Fix congruence check in strings, fixes bug 686. | ajreynol | |
| 2015-10-11 | fix regression tests, support fallback mode for proofs | Kshitij Bansal | |
| 2015-10-11 | Fix strings preprocessing + incremental, fixes bug 682. Add initial ↵ | ajreynol | |
| infrastructure for str.contains inferences. | |||
| 2015-10-06 | More improvements to strings rewriter for regexps, contains, indexof, ↵ | ajreynol | |
| replace and others. Enable non-recursive flat form inferences in strings theory solver. Refactor extf reductions. Use non-constant length terms when checking length equality. Add option --strings-eager-len. | |||
| 2015-10-02 | Improvements to rewriter for regexp, contains, indexof. Improvements and ↵ | ajreynol | |
| fixes for reduction of indexof. Fixes bugs 612 and 615. Fix bug in find+offset in strings util. Add regressions. | |||
| 2015-09-29 | Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add ↵ | ajreynol | |
| regressions. | |||
| 2015-09-28 | Improve quantifiers engine wrt incremental presolve. Add regressions. | ajreynol | |
| 2015-09-28 | Minor fixes to strings, add regressions. | ajreynol | |
| 2015-09-28 | Add missing regression | ajreynol | |
| 2015-09-28 | Fix bug for trivial extf inferences in strings. Improve caching for splits ↵ | ajreynol | |
| in strings. Other improvements. | |||
| 2015-09-27 | Improved handling of extended operators. Do preprocess on memberships ↵ | ajreynol | |
| eagerly, only process contains/memberships that have non-constant arguments. Cleanup. | |||
| 2015-09-26 | Lazy preprocessing of extended operators in strings. Add regressions. Fixes ↵ | ajreynol | |
| bug 613. | |||
| 2015-09-25 | Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ↵ | ajreynol | |
| of term database, other refactoring. Bug fixes for cbqi+datatypes. | |||
| 2015-09-24 | Counterexample-guided instantiation for datatypes. Make sygus parsing more ↵ | ajreynol | |
| liberal. | |||
| 2015-09-18 | Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding ↵ | ajreynol | |
| quantified formulas with non-constant polarity. | |||
| 2015-09-15 | Fix bug related to quantifiers + incremental, thanks John Backes for the bug ↵ | ajreynol | |
| report. Other minor cleanup. | |||
| 2015-09-10 | Models for codatatypes. Fixes bug 662. | ajreynol | |
| 2015-09-09 | Fix bug in strings rewriter regarding lengths of substr terms. | ajreynol | |
| 2015-09-05 | Fix bugs related to fmf with incremental. Reinitialize sorts on user pop, ↵ | ajreynol | |
| bug fix enumeration for uninitialized sorts, do not decide combined cardinality constraints that have not been allocated in user context. Fixes bug 654. | |||
| 2015-09-04 | Fix bugs 605 and 667. | ajreynol | |
| 2015-09-02 | fix regressions | Kshitij Bansal | |
| 2015-08-27 | Modify slow regressions. | ajreynol | |
| 2015-08-24 | Improvements to vts in cbqi, bug fix vts for non-atomic terms containing vts ↵ | ajreynol | |
| symbols. Move presolve for sygus to cbqi. Enable --cbqi-recurse by default, add option --cbqi-min-bound. Enable qcf for finite model finding by default. | |||
| 2015-08-21 | Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. ↵ | ajreynol | |
| Enable redundant ITE branch elimination in quantifiers rewriter. | |||
| 2015-08-19 | fix bug 605 | Kshitij Bansal | |
| 2015-08-19 | Implementation of model-based projection in cbqi, cleanup, add regressions. | ajreynol | |
| 2015-08-16 | More optimizations to --macros-quant, add --macros-quant-mode=ground-uf. ↵ | ajreynol | |
| Cleanup varContains caches in term db. Fix bug related to macros in non-tracing builds. | |||
| 2015-08-12 | Improvements to --macros-quant. Enable --clause-split by default. Bug fix ↵ | ajreynol | |
| for cbqi regarding instantiations with free skolems, extend to boolean quantification. Infrastructure for congruence closure with free variables. | |||
| 2015-08-01 | Support for default grammar for datatypes in sygus. Support vts for infinity. | ajreynol | |
| 2015-08-01 | Make --fmf-fun and --macros-quant work in incremental mode. Add regressions. | ajreynol | |
| 2015-07-31 | Sygus support for inductive datatypes. | ajreynol | |
| 2015-07-30 | Implement virtual term substitution for non-nested quantifiers. Fix ↵ | ajreynol | |
| soundness bug in strings related to explaining length terms. | |||
| 2015-07-27 | Disable bug590.smt2 | Tianyi Liang | |
| 2015-07-25 | Add option --sygus-inv-templ for synthesizing strengthening/weakening of ↵ | ajreynol | |
| pre/post conditions. Dump synth by default in sygus, update regressions. Set better defaults for induction. Fix bug in related to IFF and EQUAL in sygus grammar. | |||
| 2015-07-20 | Squashed merge of SygusComp 2015 branch. | ajreynol | |
| 2015-06-27 | Refactor various corner cases of fmf, quantifiers modules. Enable cbqi2 by ↵ | ajreynol | |
| default on pure quantified arithmetic. Fix bug in sort inference related to mixed real/int, add regression. | |||
| 2015-06-11 | Avoid naming conflicts in sygus, refactor. Add missing regression. Detect ↵ | ajreynol | |
| Start grammar. Add regression. | |||
| 2015-06-11 | Handle duplicate operators in sygus grammars. Parse sygus quoted literals. ↵ | ajreynol | |
| Add regression. | |||
| 2015-06-11 | Update experimental scripts. Support top-level non-terminals in sygus ↵ | ajreynol | |
| grammars. Allow -N in sygus terms. Minor bug fix in datatypes_sygus. Add regression. | |||
| 2015-06-10 | Support for printing solutions involving LetGTerm sygus. Bug fix define-fun ↵ | ajreynol | |
| within LetGTerm sygus. Bug fix sygus argument generalization. Add regressions. | |||
| 2015-06-02 | Flatten sygus grammars during parsing. Remove duplicate operators from grammars. | ajreynol | |
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback