Age | Commit message (Collapse) | Author |
|
linebreaks.
|
|
[LFSC] Minor fixes/improvements
|
|
Fix dependency tracing for fewerPreprocessingHoles
|
|
[LFSC] Fix memory leaks when creating CExprs
|
|
ref count of the TNodes in the set can become 0. Set operations containing garbage collected TNodes could then fail.
|
|
|
|
options::tearDownIncremental.
|
|
|
|
|
|
|
|
- Avoid mixing new/delete with malloc/free
- Remove reimplementation of strcmp
- Add assertions
|
|
In certain cases, LFSC was creating CExprs with the single-argument
constructor, which allocates an array of one child, only to immediately
replace it with a new array (without deleting the old one).
Additionally, this commit fixes the construction of TYPE/KIND/MPZ/MPQ
expressions (the null pointer is appended automatically by the single
argument constructor, an array with two null pointer entries should not
be necessary).
|
|
Previously, dependency tracing in `ite_removal.cpp` was only done with
the `unsatCores` option but `fewerPreprocessingHoles` requires
dependencies, too. This lead to errors during proof construction when
`fewerPreprocessingHoles` was active. This commit fixes the condition
and includes a test case that previously failed. Additionally, it fixes
a similar issue in the theory engine.
NOTE: this commit might not fix all instances of this problem.
`smt_engine.cpp` turns certain flags off with `unsatCores`.
Compatibility between those flags and `fewerPreprocessingHoles` needs to
be checked separately.
|
|
Switch from SMT-LIB v2.0 to v2.5 for smt2 files
|
|
As mentioned in bug 741, CVC4 was parsing `.smt2` files using the
SMT-LIB v2.0 standard by default. This commit switches to v2.5.
|
|
is 1, it does not automatically enable incremental mode.
|
|
Fix split-find-unsat-w-emp test
|
|
Fix initialization order
|
|
Commit 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa did not update the
split-find-unsat-w-emp test, this commit fixes that.
|
|
|
|
Fix (inactive) `MultSlice` rewrite
|
|
|
|
This commit addresses the following warning:
```
warning: field 'd_negOne' will be initialized after field 'd_pivots'
[-Wreorder]
```
|
|
The `MultSlice` rewrite was previously accepting multiplications of
three and more variables even though it was designed for multiplications
of two variables only. Fortunately, the rewrite was not actively used in
the bitvector solver. This commit strengthens the condition in
`applies()` and adds a unit test that checks that x * y * z and x * y do
not get rewritten to the same term.
|
|
|
|
|
|
|
|
using cardinality on sets with finite element type.
|
|
|
|
|
|
It was turned off for unsatCores, and fewerPreprocessingHoles using the same infrastructure.
|
|
rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions.
|
|
|
|
improvement to sets.
|
|
received.
|
|
|
|
|
|
|
|
|
|
Revert "Removing the CVC4_NEEDS_REPLACEMENT_FUNCTIONS guard to have a…
|
|
Remove wrong `ExtractMultLeadingBit` rule
|
|
|
|
--fmf-fun-rlv, fixes bug 723.
|
|
Before this fix, the build died with `ar: no archive members specified
when linking the empty libreplacements.la.` because macOS Sierra does
not require the replacements anymore. With this fix, `ffs.c` and
`strtok_r.c` are always getting compiled (even when they are empty) to
prevent the error. Also removed the unused
`CVC4_NEEDS_REPLACEMENT_FUNCTIONS` from `configure.ac` and added an
`#ifndef HAVE_FFS` to `ffs.c` for consistency with `strtok_r.c`.
|
|
and 763.
|
|
minor changes.
|
|
The rule `ExtractMultLeadingBit` estimated the number of leading zeros
wrong: when there were ones in the leading constant parts of the
factors, it was using the length of the non-zero part instead of the
length of the zero part. This commit includes an example for which the
previous version of the rule would cause a wrong answer.
|
|
Fix parsing of BVROTR by CVC parser
|
|
Add unit test for `MultDistrib` rule
|
|
This commit fixes Bugzilla bug 766 as proposed by jacobly.alt@gmail.com.
|