summaryrefslogtreecommitdiff
path: root/src/theory/arrays
AgeCommit message (Collapse)Author
2020-04-01Initialize theory rewriters in theories (#4197)Andres Noetzli
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).
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
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>
2020-02-26Initial work towards -Wshadow (#3817)Andrew Reynolds
2020-02-19resource manager: Add statistic for every resource. (#3772)Mathias Preiner
This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`). Fixes #3751.
2020-02-03Fix corner case - might need to REWRITE_AGAIN (#3706)Clark Barrett
2019-12-09Make theory rewriters non-static (#3547)Andres Noetzli
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.
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-08prefer prefix ++ operator for iteratorsPiotr Trojanek
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>
2019-09-19Support context-(in)dependent decision strategies. (#3281)Andrew Reynolds
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2018-09-22cmake: Remove unused CMakeLists.txtMathias Preiner
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-09-19Decision strategy: incorporate arrays. (#2495)Andrew Reynolds
2018-08-16Move node algorithms to separate file (#2311)Andres Noetzli
2018-08-15Remove unused tuple classes (#2313)Andres Noetzli
Since we are using C++11, we can replace the triple and quad classes with std::tuple.
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-04Move assertion. (#2051)Andrew Reynolds
2018-05-30Fix for issue #2002 (#2012)Andres Noetzli
2018-03-06Make statistics output consistent. (#1647)Mathias Preiner
* 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").
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-02-06Resolving warnings from -Winconsistent-missing-override on clang. (#1563)Tim King
2018-01-10Removing throw specifiers for TypeRules. (#1501)Tim King
2018-01-10Removing throw specifiers from type enumerators. (#1502)Tim King
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
Removing more miscellaneous throw specifiers.
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-10-25Switching EqProof to use shared_ptr everywhere. (#1217)Tim King
This clarifies the memory ownership of EqProofs.
2017-10-11Cleaning up ProofArray class. (#1208)Tim King
2017-07-20Moving from the gnu extensions for hash maps to the c++11 hash mapsTim King
* 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.
2017-07-12Make type rules more strict for operators whose type rules involve subtypes. ↵ajreynol
Disable support for subrange and predicate subtypes (which were only partially supported previously).
2017-07-07Update copyright headers.Mathias Preiner
2017-06-30Minor change to trigger selection, fixes related to subtypes (in macros, ↵ajreynol
cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
2017-06-15Fix for bug 639.Clark Barrett
2017-04-28Partial fix for bug 717.experimentClark Barrett
2017-04-21Fix for bug 681 (now gives reasonable error message about using constantClark Barrett
arrays).
2017-04-18Fix for bug 639.Clark Barrett
2017-04-04Simplify Theory::collectModelInfo interface to not take deprecated fullModel ↵ajreynol
argument.
2017-03-27Remove throw qualifiers in type enumeratorsAndres Notzli
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
2017-03-18Fix to help with bug 717Clark Barrett
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ajreynol
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
2017-01-18Fix non-idempotent rewrite in Array rewriterAndres Noetzli
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.
2016-11-03Add priorities to getNextDecision. Properly handle case for finite types + ↵ajreynol
unbounded heaps in sep logic. Fix another simple memory leak in sygus.
2016-09-16In a ROW guard proof, if the transitivity proof does not have a disequality, ↵guykatzz
we can deduce that it is a constant-disequality proof and process it accordingly
2016-09-16Handling a corner case where a ROW's guard is a constant disequality.Guy
If this is a simple proof (e.g., just 1 != 2), change the d_id from Transitivity to ConstantDisequality
2016-07-06A few proof bugs fixedGuy
2016-06-01Merge from proof branchGuy
2016-06-01Revert "Merging proof branch"Guy
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
2016-06-01Merging proof branchGuy
2016-04-15Rolling back the rewrite codeGuy
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback