projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Reimplement support for relational triggers (#7063)
[cvc5.git] / src / theory / sets /
2021-10-04 Andrew ReynoldsMove isFiniteType from theory engine to Env (#7287) tree | commitdiff
2021-09-13 Andres NoetzliRemove context getters from `TheoryState` (#7174) tree | commitdiff
2021-09-07 Andres NoetzliUse `EnvObj` methods instead of `Theory` methods (... tree | commitdiff
2021-09-03 Aina NiemetzEnvObj: Add options(), context(), userContext(). (... tree | commitdiff
2021-08-17 Gereon KremerPush Env class into TheoryState (#7012) tree | commitdiff
2021-08-16 Gereon KremerMake Theory class use Env (#7011) tree | commitdiff
2021-08-04 Andrew ReynoldsAdd missing inference identifiers (#6962) tree | commitdiff
2021-07-26 Andrew ReynoldsEnable default equality proofs for sets (#6931) tree | commitdiff
2021-07-22 Andrew ReynoldsMiscellaneous changes in preparation for central equali... tree | commitdiff
2021-07-09 Andrew ReynoldsFix sets cardinality inference involving equivalent... tree | commitdiff
2021-06-22 Andrew ReynoldsSet up fine grained equality notifications (#6734) tree | commitdiff
2021-05-26 Andres Noetzli More precise includes of `Node` constants (#6617) tree | commitdiff
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611) tree | commitdiff
2021-05-19 Andrew ReynoldsAdd more missing inference ids (#6313) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-04-23 Andrew Reynolds(proof-new) Proofs for sets purification lemmas (#6416) tree | commitdiff
2021-04-22 Andrew ReynoldsMove expand definition from Theory to TheoryRewriter... tree | commitdiff
2021-04-21 Mathias PreinerGoodbye CVC4, hello cvc5! (#6371) tree | commitdiff
2021-04-21 Aina NiemetzSets: Move implementation of type rules to cpp. (#6401) tree | commitdiff
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) tree | commitdiff
2021-04-14 Andrew ReynoldsFix type rule for relations join image (#6349) tree | commitdiff
2021-04-14 Gereon KremerRefactor / reimplement statistics (#6162) tree | commitdiff
2021-04-14 Aina NiemetzRename public and private headers in src/include. ... tree | commitdiff
2021-04-12 Andrew ReynoldsFix computation of whether a type is finite (#6312) tree | commitdiff
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) tree | commitdiff
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326) tree | commitdiff
2021-04-08 Andrew ReynoldsAdd identifiers for sources of incompleteness (#6311) tree | commitdiff
2021-04-07 Andrew ReynoldsReplace calls to NodeManager::mkSkolem with SkolemManag... tree | commitdiff
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290) tree | commitdiff
2021-04-06 Andrew ReynoldsFix issue with lemma during equality engine iterator... tree | commitdiff
2021-04-05 Haniel Barbosa[proof-new] Registering proof checkers uniformly from... tree | commitdiff
2021-04-05 Andrew ReynoldsFix subtyping for sets care graph (#6278) tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-31 Andrew ReynoldsAdd missing inference ids (#6242) tree | commitdiff
2021-03-16 Mathias Preinercmake: Generate cvc4_export.h and set visibility to... tree | commitdiff
2021-03-11 Aina NiemetzDelete Expr layer. (#6117) tree | commitdiff
2021-03-11 Andrew Reynolds(proof-new) Clean up uses of witness with skolem lemmas... tree | commitdiff
2021-03-10 Andrew Reynolds(proof-new) Update ppRewrite to use skolem lemmas ... tree | commitdiff
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-19 Andrew ReynoldsRefactoring theory inference process (#5920) tree | commitdiff
2021-02-18 Gereon KremerAdd statistic for InferenceId to TheoryInferenceManager... tree | commitdiff
2021-02-18 Gereon KremerAdd InferenceIds for sets theory. (#5900) tree | commitdiff
2021-02-17 Gereon KremerAdd InferenceId to buffered inference manager (#5911) tree | commitdiff
2021-02-11 Gereon KremerMake most methods of TheoryInferenceManager expect... tree | commitdiff
2021-02-06 Andrew ReynoldsDo not combine theories if theory engine needs check... tree | commitdiff
2020-12-15 Andrew ReynoldsProper expand definitions for sets (#5676) tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-11-06 mudathirmahgoubFix issue #5342 (#5349) tree | commitdiff
2020-10-24 mudathirmahgoubFix issue 5271 (#5335) tree | commitdiff
2020-10-22 mudathirmahgoubFix issue 5309 (#5327) tree | commitdiff
2020-10-14 mudathirmahgoubFix issue #5269 (#5270) tree | commitdiff
2020-10-06 Andrew Reynolds(proof-new) Add interface for trusted substitution... tree | commitdiff
2020-10-06 mudathirmahgoubRemove subtyping for sets (#5205) tree | commitdiff
2020-10-04 mudathirmahgoubRemove subtyping for sets theory (#5179) tree | commitdiff
2020-10-03 Andrew ReynoldsStandardization of Theory (#5181) tree | commitdiff
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... tree | commitdiff
2020-09-19 Andrew ReynoldsStandardize equality engine notifications in sets ... tree | commitdiff
2020-09-15 Andrew ReynoldsMove sets member propagation to SolverState (#5045) tree | commitdiff
2020-09-14 Andrew ReynoldsRefactoring the rewriter of sets (#4856) tree | commitdiff
2020-09-09 mudathirmahgoubAdd is_singleton operator to the theory of sets (#5033) tree | commitdiff
2020-09-09 Andrew ReynoldsSplit term registry from theory state in sets (#5037) tree | commitdiff
2020-09-04 Gereon KremerUse arith::InferenceManager for CAD lemmas (#5015) tree | commitdiff
2020-09-03 Andrew ReynoldsUpdate sets inference manager to inherit from Inference... tree | commitdiff
2020-09-02 Andrew Reynolds(new theory) Update TheorySets to the new interface... tree | commitdiff
2020-08-31 Andrew ReynoldsSimplify interface for computing relevant terms. (... tree | commitdiff
2020-08-28 Andrew ReynoldsReplace Theory::Set with TheoryIdSet (#4959) tree | commitdiff
2020-08-26 Andrew ReynoldsReplace Expr-level datatype with Node-level DType ... tree | commitdiff
2020-08-24 Andrew ReynoldsExtend the standard Theory template based on equality... tree | commitdiff
2020-08-21 Andrew ReynoldsRemove spurious theory methods calls (#4931) tree | commitdiff
2020-08-20 Andrew ReynoldsSimplify trigger notifications in equality engine ... tree | commitdiff
2020-08-19 Andrew ReynoldsMake sets and strings solver states inherit from Theory... tree | commitdiff
2020-08-19 Gereon KremerChanges assertion (about maximum set cardinality) to... tree | commitdiff
2020-08-17 Andrew ReynoldsDynamic allocation of equality engine in Theory (#4890) tree | commitdiff
2020-08-14 Andrew ReynoldsSimplify equality engine notifications (#4896) tree | commitdiff
2020-08-12 Andrew ReynoldsFix connection to master equality engine in sets (... tree | commitdiff
2020-08-12 Andrew ReynoldsPrepare theory of sets for dynamic allocation of equali... tree | commitdiff
2020-08-09 Andrew ReynoldsMake valuation class more robust to null underlying... tree | commitdiff
2020-07-28 Andrew ReynoldsUse lemma property enum for OutputChannel::lemma (... tree | commitdiff
2020-07-14 Andres NoetzliUse TypeNode in EmptySet (#4740) tree | commitdiff
2020-07-11 Andrew Reynolds(proof-new) Update Theory interface for proof-new ... tree | commitdiff
2020-06-16 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-05-23 mudathirmahgoubremove unused field d_emp_exp in TheorySetsPrivate... tree | commitdiff
2020-05-20 Andrew ReynoldsDo not eliminate variables that are equal to unevaluata... tree | commitdiff
2020-05-19 mudathirmahgoubRenamed operator CHOICE to WITNESS (#4207) tree | commitdiff
2020-04-26 Andrew Reynolds Fix sets cardinality cycle rule (#4392) tree | commitdiff
2020-04-15 Andrew ReynoldsAlways flush lemmas from downwards closure in sets... tree | commitdiff
2020-04-08 mudathirmahgoubAdded CHOOSE operator for sets (#4211) tree | commitdiff
2020-04-08 Andres NoetzliPerform theory widening eagerly (#4044) tree | commitdiff
2020-04-03 Andres NoetzliUpdate theory rewriter ownership, add stats to strings... tree | commitdiff
2020-04-02 Andres NoetzliInitialize theory rewriters in theories (#4197) tree | commitdiff
2020-03-06 Andrew ReynoldsMinor refactor for theory of sets (#3924) tree | commitdiff
2020-03-05 Mathias PreinerEnable -Wshadow and fix warnings. (#3909) tree | commitdiff
2020-03-03 mudathirmahgoubRefactoring and cleaning the type enumerator for sets... tree | commitdiff
2020-03-03 Andres NoetzliFix `TheorySetsPrive::eqNotifyPostMerge()` (#3901) tree | commitdiff
2020-03-03 Mathias PreinerFix variable shadowing bug in sets. (#3898) tree | commitdiff
next