Age | Commit message (Collapse) | Author | |
---|---|---|---|
2020-02-07 | Univeset Cardinality constraints for infinite types (#3712) | mudathirmahgoub | |
2020-02-03 | Fix cardinality of uninterpreted types when univset is not used (#3663) | mudathirmahgoub | |
* Fixed bug 3662 * format * small change * added bug3663.smt2 file * throw Logic Exception * throw Logic Exception * ;EXIT: 1 Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com> | |||
2020-01-07 | Universe set cardinality for finite types with finite cardinality (#3392) | mudathirmahgoub | |
* rewrote set cardinality for finite-types * small changes and format | |||
2019-12-13 | Add support for set comprehension (#3312) | Andrew Reynolds | |
2019-12-12 | Use the node-level datatypes API (#3556) | Andrew Reynolds | |
2019-12-09 | Make 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-11-09 | Fixes in relations related to datatypes not passed by reference (#3449) | Andrew Reynolds | |
The current code is creating/destroying datatypes unnecessarily. | |||
2019-10-30 | Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366) | Mathias Preiner | |
2019-10-22 | Refactoring skolems for sets (#3381) | Andrew Reynolds | |
This refactors skolems introduced in the theory of sets. This is analogous to how skolems are treated for the theory of strings. A key change that this commit enables is to identify "variable" sets based on those that weren't introduced by the SkolemCache (instead of via a check that their kind is `VARIABLE`, which is done currently and is error prone). | |||
2019-10-08 | prefer prefix ++ operator for iterators | Piotr 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-16 | Initialize fields in sets inference manager (#3289) | Andrew Reynolds | |
2019-09-13 | Split, refactor and document the theory of sets (#3085) | Andrew Reynolds | |
2019-08-28 | Removing comments related to issues (#3232) | Andrew Reynolds | |
2019-07-08 | Towards refactoring relations (#3078) | Andrew Reynolds | |
2019-04-24 | Do not use __ prefix for header guards. (#2974) | Mathias Preiner | |
Fixes 2887. | |||
2019-04-01 | Modify strategy in sets+cardinality (#2909) | Andrew Reynolds | |
2019-03-29 | Apply empty splits more aggressively in sets+cardinality (#2907) | Andrew Reynolds | |
2019-03-26 | Update copyright headers. | Aina Niemetz | |
2018-12-14 | Fix extended rewriter for binary associative operators. (#2751) | Andrew Reynolds | |
This was causing assertion failures when using Sets + Sygus. | |||
2018-12-03 | Skip non-cardinality types in sets min card inference (#2734) | Andrew Reynolds | |
2018-11-27 | Make (T)NodeTrie a general utility (#2489) | Andrew Reynolds | |
This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it. | |||
2018-10-19 | Remove autotools build system. (#2639) | Mathias Preiner | |
2018-10-03 | Fix stale op list in sets (#2572) | Andrew Reynolds | |
2018-09-22 | cmake: Remove unused CMakeLists.txt | Mathias Preiner | |
2018-09-22 | cmake: Added initial build infrastructure. | Aina Niemetz | |
2018-08-24 | Fix more simple coverity warnings (#2372) | Andrew Reynolds | |
2018-08-22 | Wrapping TheorySetsPrivate in a unique_ptr. (#2356) | Tim King | |
2018-08-22 | Fix invalid iterator comparisons (#2349) | Andrew Reynolds | |
2018-08-17 | Remove miscellaneous unused code (#2333) | Andrew Reynolds | |
2018-08-16 | Move node algorithms to separate file (#2311) | Andres Noetzli | |
2018-07-25 | Removing support for CDHashMap::iterator's postfix increment. (#2208) | Tim King | |
2018-07-24 | Improvements to sets + cardinality + quantifiers (#2200) | Andrew Reynolds | |
2018-06-25 | Updated copyright headers. | Aina Niemetz | |
2018-05-03 | Sets subtypes (#1095) | Andrew Reynolds | |
Make sets theory properly handle equalities between (Set T1) and (Set T2) whenever equalities between T1 and T2 are also handled. Generalizes previous approach for type correctness conditions. Add regression. | |||
2018-03-06 | Make 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-05 | Enable -Wsuggest-override by default. (#1643) | Mathias Preiner | |
Adds missing override keywords. | |||
2018-02-06 | Resolving warnings from -Winconsistent-missing-override on clang. (#1563) | Tim King | |
2018-01-10 | Removing throw specifiers for TypeRules. (#1501) | Tim King | |
2018-01-10 | Removing throw specifiers from type enumerators. (#1502) | Tim King | |
2017-12-08 | Make collect model info return a Bool (#1421) | Andrew Reynolds | |
2017-12-06 | Remove CDChunkList (#1414) | Andres Noetzli | |
2017-10-17 | Fixing 2 instances of an unused variable. (#1253) | Tim King | |
2017-09-10 | Ensure that expand definitions is called on all non-variable expressi… (#1070) | Andrew Reynolds | |
* Ensure that expand definitions is called on all non-variable expressions. In particular, it is necessary that the sets theory is notified when a set universe term occurs in the input to ensure options are set correctly. The commit moves this check from within check() to expandDefinitions(), and also adds the check for join image which relies on universe set. This fixes a bug reported by Arjun. Add and update regressions. * Add comments concerning expandDefinitions * Expand comment, move to .h | |||
2017-07-20 | Moving from the gnu extensions for hash maps to the c++11 hash maps | Tim 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-14 | Removing BOOST_FOREACH usage. | Tim King | |
2017-07-12 | Make 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-10 | Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵ | ajreynol | |
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions. | |||
2017-07-07 | Update copyright headers. | Mathias Preiner | |
2017-07-07 | Use new copyright header format. | Mathias Preiner | |
2017-06-30 | Minor 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. |