projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Reimplement support for relational triggers (#7063)
[cvc5.git]
/
src
/
theory
/
sets
/
2021-10-04
Andrew Reynolds
Move isFiniteType from theory engine to Env (#7287)
tree
|
commitdiff
2021-09-13
Andres Noetzli
Remove context getters from `TheoryState` (#7174)
tree
|
commitdiff
2021-09-07
Andres Noetzli
Use `EnvObj` methods instead of `Theory` methods (...
tree
|
commitdiff
2021-09-03
Aina Niemetz
EnvObj: Add options(), context(), userContext(). (...
tree
|
commitdiff
2021-08-17
Gereon Kremer
Push Env class into TheoryState (#7012)
tree
|
commitdiff
2021-08-16
Gereon Kremer
Make Theory class use Env (#7011)
tree
|
commitdiff
2021-08-04
Andrew Reynolds
Add missing inference identifiers (#6962)
tree
|
commitdiff
2021-07-26
Andrew Reynolds
Enable default equality proofs for sets (#6931)
tree
|
commitdiff
2021-07-22
Andrew Reynolds
Miscellaneous changes in preparation for central equali...
tree
|
commitdiff
2021-07-09
Andrew Reynolds
Fix sets cardinality inference involving equivalent...
tree
|
commitdiff
2021-06-22
Andrew Reynolds
Set 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 Reynolds
Move proof utilities to src/proof/ (#6611)
tree
|
commitdiff
2021-05-19
Andrew Reynolds
Add more missing inference ids (#6313)
tree
|
commitdiff
2021-05-13
Mathias Preiner
Add 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 Reynolds
Move expand definition from Theory to TheoryRewriter...
tree
|
commitdiff
2021-04-21
Mathias Preiner
Goodbye CVC4, hello cvc5! (#6371)
tree
|
commitdiff
2021-04-21
Aina Niemetz
Sets: Move implementation of type rules to cpp. (#6401)
tree
|
commitdiff
2021-04-15
Aina Niemetz
Rename occurrences of CVC4 to CVC5. (#6351)
tree
|
commitdiff
2021-04-14
Andrew Reynolds
Fix type rule for relations join image (#6349)
tree
|
commitdiff
2021-04-14
Gereon Kremer
Refactor / reimplement statistics (#6162)
tree
|
commitdiff
2021-04-14
Aina Niemetz
Rename public and private headers in src/include. ...
tree
|
commitdiff
2021-04-12
Andrew Reynolds
Fix computation of whether a type is finite (#6312)
tree
|
commitdiff
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
tree
|
commitdiff
2021-04-09
Aina Niemetz
Rename CVC4__ header guards to CVC5__. (#6326)
tree
|
commitdiff
2021-04-08
Andrew Reynolds
Add identifiers for sources of incompleteness (#6311)
tree
|
commitdiff
2021-04-07
Andrew Reynolds
Replace calls to NodeManager::mkSkolem with SkolemManag...
tree
|
commitdiff
2021-04-06
Andres Noetzli
Remove template argument from `NodeBuilder` (#6290)
tree
|
commitdiff
2021-04-06
Andrew Reynolds
Fix 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 Reynolds
Fix subtyping for sets care graph (#6278)
tree
|
commitdiff
2021-04-01
Aina Niemetz
Rename namespace CVC5 to cvc5. (#6258)
tree
|
commitdiff
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
tree
|
commitdiff
2021-03-31
Andrew Reynolds
Add missing inference ids (#6242)
tree
|
commitdiff
2021-03-16
Mathias Preiner
cmake: Generate cvc4_export.h and set visibility to...
tree
|
commitdiff
2021-03-11
Aina Niemetz
Delete 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 Kremer
Some more cleanup of includes (#6083)
tree
|
commitdiff
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
tree
|
commitdiff
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
tree
|
commitdiff
2021-02-19
Andrew Reynolds
Refactoring theory inference process (#5920)
tree
|
commitdiff
2021-02-18
Gereon Kremer
Add statistic for InferenceId to TheoryInferenceManager...
tree
|
commitdiff
2021-02-18
Gereon Kremer
Add InferenceIds for sets theory. (#5900)
tree
|
commitdiff
2021-02-17
Gereon Kremer
Add InferenceId to buffered inference manager (#5911)
tree
|
commitdiff
2021-02-11
Gereon Kremer
Make most methods of TheoryInferenceManager expect...
tree
|
commitdiff
2021-02-06
Andrew Reynolds
Do not combine theories if theory engine needs check...
tree
|
commitdiff
2020-12-15
Andrew Reynolds
Proper expand definitions for sets (#5676)
tree
|
commitdiff
2020-12-10
Gereon Kremer
Fixed a bunch of clang warnings. (#5637)
tree
|
commitdiff
2020-12-07
Andrew Reynolds
Do not expand theory definitions at the beginning of...
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-11-06
mudathirmahgoub
Fix issue #5342 (#5349)
tree
|
commitdiff
2020-10-24
mudathirmahgoub
Fix issue 5271 (#5335)
tree
|
commitdiff
2020-10-22
mudathirmahgoub
Fix issue 5309 (#5327)
tree
|
commitdiff
2020-10-14
mudathirmahgoub
Fix issue #5269 (#5270)
tree
|
commitdiff
2020-10-06
Andrew Reynolds
(proof-new) Add interface for trusted substitution...
tree
|
commitdiff
2020-10-06
mudathirmahgoub
Remove subtyping for sets (#5205)
tree
|
commitdiff
2020-10-04
mudathirmahgoub
Remove subtyping for sets theory (#5179)
tree
|
commitdiff
2020-10-03
Andrew Reynolds
Standardization of Theory (#5181)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-19
Andrew Reynolds
Standardize equality engine notifications in sets ...
tree
|
commitdiff
2020-09-15
Andrew Reynolds
Move sets member propagation to SolverState (#5045)
tree
|
commitdiff
2020-09-14
Andrew Reynolds
Refactoring the rewriter of sets (#4856)
tree
|
commitdiff
2020-09-09
mudathirmahgoub
Add is_singleton operator to the theory of sets (#5033)
tree
|
commitdiff
2020-09-09
Andrew Reynolds
Split term registry from theory state in sets (#5037)
tree
|
commitdiff
2020-09-04
Gereon Kremer
Use arith::InferenceManager for CAD lemmas (#5015)
tree
|
commitdiff
2020-09-03
Andrew Reynolds
Update 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 Reynolds
Simplify interface for computing relevant terms. (...
tree
|
commitdiff
2020-08-28
Andrew Reynolds
Replace Theory::Set with TheoryIdSet (#4959)
tree
|
commitdiff
2020-08-26
Andrew Reynolds
Replace Expr-level datatype with Node-level DType ...
tree
|
commitdiff
2020-08-24
Andrew Reynolds
Extend the standard Theory template based on equality...
tree
|
commitdiff
2020-08-21
Andrew Reynolds
Remove spurious theory methods calls (#4931)
tree
|
commitdiff
2020-08-20
Andrew Reynolds
Simplify trigger notifications in equality engine ...
tree
|
commitdiff
2020-08-19
Andrew Reynolds
Make sets and strings solver states inherit from Theory...
tree
|
commitdiff
2020-08-19
Gereon Kremer
Changes assertion (about maximum set cardinality) to...
tree
|
commitdiff
2020-08-17
Andrew Reynolds
Dynamic allocation of equality engine in Theory (#4890)
tree
|
commitdiff
2020-08-14
Andrew Reynolds
Simplify equality engine notifications (#4896)
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Fix connection to master equality engine in sets (...
tree
|
commitdiff
2020-08-12
Andrew Reynolds
Prepare theory of sets for dynamic allocation of equali...
tree
|
commitdiff
2020-08-09
Andrew Reynolds
Make valuation class more robust to null underlying...
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Use lemma property enum for OutputChannel::lemma (...
tree
|
commitdiff
2020-07-14
Andres Noetzli
Use 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 Niemetz
Update copyright headers.
tree
|
commitdiff
2020-05-23
mudathirmahgoub
remove unused field d_emp_exp in TheorySetsPrivate...
tree
|
commitdiff
2020-05-20
Andrew Reynolds
Do not eliminate variables that are equal to unevaluata...
tree
|
commitdiff
2020-05-19
mudathirmahgoub
Renamed operator CHOICE to WITNESS (#4207)
tree
|
commitdiff
2020-04-26
Andrew Reynolds
Fix sets cardinality cycle rule (#4392)
tree
|
commitdiff
2020-04-15
Andrew Reynolds
Always flush lemmas from downwards closure in sets...
tree
|
commitdiff
2020-04-08
mudathirmahgoub
Added CHOOSE operator for sets (#4211)
tree
|
commitdiff
2020-04-08
Andres Noetzli
Perform theory widening eagerly (#4044)
tree
|
commitdiff
2020-04-03
Andres Noetzli
Update theory rewriter ownership, add stats to strings...
tree
|
commitdiff
2020-04-02
Andres Noetzli
Initialize theory rewriters in theories (#4197)
tree
|
commitdiff
2020-03-06
Andrew Reynolds
Minor refactor for theory of sets (#3924)
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-03-03
mudathirmahgoub
Refactoring and cleaning the type enumerator for sets...
tree
|
commitdiff
2020-03-03
Andres Noetzli
Fix `TheorySetsPrive::eqNotifyPostMerge()` (#3901)
tree
|
commitdiff
2020-03-03
Mathias Preiner
Fix variable shadowing bug in sets. (#3898)
tree
|
commitdiff
next