Age | Commit message (Collapse) | Author |
|
Until now, the `Rewriter` was responsible for creating `TheoryRewriter`
instances. This commit adds a method `mkTheoryRewriter()` that theories
override to create an instance of their corresponding theory rewriter.
The advantage is that the theories can pass additional information to
their theory rewriter (e.g. a statistics object).
|
|
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally.
Co-authored-by: Clark Barrett <barrett@cs.stanford.edu>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>
Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
Co-authored-by: makaimann <makaim@stanford.edu>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: AleksandarZeljic <zeljic@stanford.edu>
Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com>
Co-authored-by: Amalee <amaleewilson@gmail.com>
Co-authored-by: Scott Kovach <dskovach@gmail.com>
Co-authored-by: ntsis <nekuna@gmail.com>
|
|
|
|
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).
Fixes #3751.
|
|
|
|
This commit changes theory rewriters to be non-static. This refactoring
is needed as a stepping stone to making our rewriter configurable: If we
have multiple solver objects with different rewrite configurations, we
cannot use `static` variables for the rewriter table in the BV rewriter
for example. It is also in line with our goal of getting rid of
singletons in general. Note that the `Rewriter` class is still a
singleton, which will be changed in a future commit.
|
|
|
|
Detected with cppcheck static analyser, which said: (performance) Prefer
prefix ++/-- operators for non-primitive types. Reformat with clang-format
as needed.
Signed-off-by: Piotr Trojanek <piotr.trojanek@gmail.com>
|
|
|
|
Fixes 2887.
|
|
|
|
|
|
|
|
|
|
|
|
Since we are using C++11, we can replace the triple and quad classes
with std::tuple.
|
|
|
|
|
|
|
|
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
|
|
Adds missing override keywords.
|
|
|
|
|
|
|
|
Removing more miscellaneous throw specifiers.
|
|
|
|
|
|
This clarifies the memory ownership of EqProofs.
|
|
|
|
* Replacing __gnu_cxx::hash_map with std::unordered_map.
* Replacing __gnu_cxx::hash_set with std::unordered_set.
* Replacing __gnu_cxx::hash with std::hash.
* Adding missing includes.
|
|
Disable support for subrange and predicate subtypes (which were only partially supported previously).
|
|
|
|
cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
|
|
|
|
|
|
arrays).
|
|
|
|
argument.
|
|
This addresses Coverity issues:
- 1172154
- 1172156
- 1172157
- 1172158
- 1172159
- 1379612
- 1379612
- 1421430
- 1172166
- 1172144
- 1362709
- 1362696
- 1172145
- 1172147
- 1172148
- 1379610
- 1362772
- 1362676
- 1362704
- 1362749
- 1362876
- 1362843
- 1362837
- 1362881
- 1172223
- 1172155
|
|
|
|
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
|
|
This commit fixes bug 637 (
http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as
proposed in Bugzilla and adds the minified test case to the
regression tests.
|
|
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
|
|
we can deduce that it is a constant-disequality proof and process it accordingly
|
|
If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality
|
|
|
|
|
|
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
|
|
|
|
|