| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
flag. This resulted in user code seeing a different size for the SmtEngine class than what was compiled in the library. Proofs are enabled by default again. See http://cvc4.cs.nyu.edu/bugs/show_bug.cgi?id=688 for more information.
|
|
file. This also rearranges generation of the file so that one .subdirs file is generated once per Makefile.am file. This keeps using relative paths clean.
|
|
|
|
mixed Int/Real. Bug fixes. Updates to quantifiers rewriter.
|
|
|
|
vector using a stale reference in the unconstrained simplifier.
|
|
quantified logics that include at least one relevant theory. Enforce restriction on model building to last call. Update options, refactor. Update regressions.
|
|
|
|
|
|
|
|
regressions. Eliminate preprocess for regexp.
|
|
for string contains, refactoring.
|
|
|
|
|
|
|
|
empty string for error conditions. Improve rewriter for str.substr.
|
|
|
|
infrastructure for str.contains inferences.
|
|
multiple sorts in UF finite model finding by default.
|
|
|
|
|
|
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.
|
|
improvements.
|
|
fixes for reduction of indexof. Fixes bugs 612 and 615. Fix bug in find+offset in strings util. Add regressions.
|
|
rewriting. Bug fix explanations for inferences. Avoid spurious cardinality splits. Do not do disequality splits for non-disequal terms. Work towards non-recursive handling of flat forms.
|
|
reductions based on congruence, precheck for cycles.
|
|
|
|
regressions.
|
|
|
|
|
|
|
|
in strings. Other improvements.
|
|
eagerly, only process contains/memberships that have non-constant arguments. Cleanup.
|
|
bug 613.
|
|
module. Add heuristics for cbqi LIA instantiation with coefficients.
|
|
of term database, other refactoring. Bug fixes for cbqi+datatypes.
|
|
liberal.
|
|
|
|
fix involves sets getModelValue handling the case when element theory
doesn't have model
|
|
|
|
|
|
quantified formulas with non-constant polarity.
|
|
|
|
report. Other minor cleanup.
|
|
|
|
|
|
|
|
|
