summaryrefslogtreecommitdiff
path: root/src/theory/sets
AgeCommit message (Collapse)Author
2020-02-07Univeset Cardinality constraints for infinite types (#3712)mudathirmahgoub
2020-02-03Fix 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-07Universe set cardinality for finite types with finite cardinality (#3392)mudathirmahgoub
* rewrote set cardinality for finite-types * small changes and format
2019-12-13Add support for set comprehension (#3312)Andrew Reynolds
2019-12-12Use the node-level datatypes API (#3556)Andrew Reynolds
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-11-09Fixes in relations related to datatypes not passed by reference (#3449)Andrew Reynolds
The current code is creating/destroying datatypes unnecessarily.
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-10-22Refactoring 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-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-16Initialize fields in sets inference manager (#3289)Andrew Reynolds
2019-09-13Split, refactor and document the theory of sets (#3085)Andrew Reynolds
2019-08-28Removing comments related to issues (#3232)Andrew Reynolds
2019-07-08Towards refactoring relations (#3078)Andrew Reynolds
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-04-01Modify strategy in sets+cardinality (#2909)Andrew Reynolds
2019-03-29Apply empty splits more aggressively in sets+cardinality (#2907)Andrew Reynolds
2019-03-26Update 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-27Make (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-19Remove autotools build system. (#2639)Mathias Preiner
2018-10-03Fix stale op list in sets (#2572)Andrew Reynolds
2018-09-22cmake: Remove unused CMakeLists.txtMathias Preiner
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-24 Fix more simple coverity warnings (#2372)Andrew Reynolds
2018-08-22Wrapping TheorySetsPrivate in a unique_ptr. (#2356)Tim King
2018-08-22Fix invalid iterator comparisons (#2349)Andrew Reynolds
2018-08-17Remove miscellaneous unused code (#2333)Andrew Reynolds
2018-08-16Move node algorithms to separate file (#2311)Andres Noetzli
2018-07-25Removing support for CDHashMap::iterator's postfix increment. (#2208)Tim King
2018-07-24Improvements to sets + cardinality + quantifiers (#2200)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-05-03Sets 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-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
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
2017-12-06Remove CDChunkList (#1414)Andres Noetzli
2017-10-17Fixing 2 instances of an unused variable. (#1253)Tim King
2017-09-10Ensure 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-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-14Removing BOOST_FOREACH usage.Tim King
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-10Merge 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-07Update copyright headers.Mathias Preiner
2017-07-07Use new copyright header format.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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback