summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Collapse)Author
2016-02-11More aggressive conditional rewriting for quantified formulas. Bug fix set ↵ajreynol
incomplete for fmc.
2016-02-10Fix model postprocessor for tuples, add regression.ajreynol
2016-02-09Fix regression, minor change to output.ajreynol
2016-02-08Updates related to finite model finding and (co)datatypes. Bug fix ↵ajreynol
enumerator and codatatype rewriter, further simplify fmc.
2016-02-01Simplify fmc model construction, add regression. Improve FMF debug assertions.ajreynol
2016-01-26Merged bit-vector and uf proof branch.Liana Hadarean
2016-01-20Fix bug in fmc mbqi where modelscomputed for mbqi could involve non-constant ↵ajreynol
values. Add regression.
2016-01-19Bug fixes for model construction with codatatypes, add regressions.ajreynol
2016-01-18Bug fix rewriter for fun defs.ajreynol
2016-01-15Ensure model construction for parametric sorts involving uninterpreted sorts ↵ajreynol
respect cardinality bounds on when finite model finding is enabled.
2016-01-06Improving the documentation of the CVC command CONTINUE.Tim King
2015-12-22Always split on constructor types for datatypes involving uninterpreted ↵ajreynol
sorts when finite model finding is enabled, add regressions.
2015-12-22Bug fix for cbqi, do not use model values for terms involving non-enumerable ↵ajreynol
sorts.
2015-11-25Infrastructure for partially single invocation properties. Bug fix for ↵ajreynol
unconstrained functions in sygus solver.
2015-11-11Minor fixes to cbqi, purify-quant. Better error checking in addInstantiation.ajreynol
2015-11-10Fix infinite loop in datatype enumerator. Minor fixes and improvements to ↵ajreynol
cbqi, full saturate. Add option --purify-quant. Use disequality triggers when using relational triggers. Add regressions.
2015-11-06Changing file permissions to add or remove executable tag as appropriate.Tim King
2015-11-05Merging the google branch back into master.Tim King
2015-11-05Fixes 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-04Better combination of UF with cbqi, refactor quantifiers intialization.ajreynol
2015-10-31Improvements to handling of mixed Int/Real quantifiers.ajreynol
2015-10-26Extend counterexample-guided instantiation to extended theory of Int/Real, ↵ajreynol
mixed Int/Real. Bug fixes. Updates to quantifiers rewriter.
2015-10-22Enable 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-20Clean up explanations involving string length. Add regression.ajreynol
2015-10-19Improve stratification of strings extended function reductions, add ↵ajreynol
regressions. Eliminate preprocess for regexp.
2015-10-16Fix for codatatype constant rewrite, add regression.ajreynol
2015-10-15Fix congruence check in strings, fixes bug 686.ajreynol
2015-10-11fix regression tests, support fallback mode for proofsKshitij Bansal
2015-10-11Fix strings preprocessing + incremental, fixes bug 682. Add initial ↵ajreynol
infrastructure for str.contains inferences.
2015-10-06More 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-02Improvements 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-29Fix for fmf+incremental. Restrict cbqi to literals from ce body. Add ↵ajreynol
regressions.
2015-09-28Improve quantifiers engine wrt incremental presolve. Add regressions.ajreynol
2015-09-28Minor fixes to strings, add regressions.ajreynol
2015-09-28Add missing regressionajreynol
2015-09-28Fix bug for trivial extf inferences in strings. Improve caching for splits ↵ajreynol
in strings. Other improvements.
2015-09-27Improved handling of extended operators. Do preprocess on memberships ↵ajreynol
eagerly, only process contains/memberships that have non-constant arguments. Cleanup.
2015-09-26Lazy preprocessing of extended operators in strings. Add regressions. Fixes ↵ajreynol
bug 613.
2015-09-25Clear term caches for quantifiers + incremental, fixes bug 674. Refactoring ↵ajreynol
of term database, other refactoring. Bug fixes for cbqi+datatypes.
2015-09-24Counterexample-guided instantiation for datatypes. Make sygus parsing more ↵ajreynol
liberal.
2015-09-18Allow most smt2 commands as sygus commands. Fix bug in fmf-fun regarding ↵ajreynol
quantified formulas with non-constant polarity.
2015-09-15Fix bug related to quantifiers + incremental, thanks John Backes for the bug ↵ajreynol
report. Other minor cleanup.
2015-09-10Models for codatatypes. Fixes bug 662.ajreynol
2015-09-09Fix bug in strings rewriter regarding lengths of substr terms.ajreynol
2015-09-05Fix 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-04Fix bugs 605 and 667.ajreynol
2015-09-02fix regressionsKshitij Bansal
2015-08-27Modify slow regressions.ajreynol
2015-08-24Improvements 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-21Fix disequality bounds in cbqi, record literals for ITE skolems in cbqi. ↵ajreynol
Enable redundant ITE branch elimination in quantifiers rewriter.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback