projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Updates to theory preprocess equality (#5776)
[cvc5.git]
/
src
/
theory
/
uf
/
2020-12-10
Gereon Kremer
Refactor KindMap (#5646)
tree
|
commitdiff
2020-12-10
Gereon Kremer
Fixed a bunch of clang warnings. (#5637)
tree
|
commitdiff
2020-12-03
Gereon Kremer
Use mkAnd where the number of children may be less...
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-12-02
Aina Niemetz
Rename macro Message to CVC4Message. (#5576)
tree
|
commitdiff
2020-11-23
Andrew Reynolds
Change UF ho to ppRewrite instead of expand definition...
tree
|
commitdiff
2020-11-12
Andrew Reynolds
(proof-new) Separate explanation stages in proof equali...
tree
|
commitdiff
2020-11-12
Andrew Reynolds
(proof-new) Fix true explanations of propagations in...
tree
|
commitdiff
2020-10-24
Haniel Barbosa
[proof-new] Fix n-ary kind handling in EqEngine explana...
tree
|
commitdiff
2020-10-23
Andrew Reynolds
Fix related to preregistering boolean term variables...
tree
|
commitdiff
2020-10-22
Andrew Reynolds
Remove unused equality engine types (#5319)
tree
|
commitdiff
2020-10-20
Aina Niemetz
Fix compiler warnings. (#5305)
tree
|
commitdiff
2020-10-20
Andrew Reynolds
(proof-new) Update add lazy step interface in LazyCDPro...
tree
|
commitdiff
2020-10-20
Andrew Reynolds
Fix miscellaneous warnings (#5256)
tree
|
commitdiff
2020-10-12
Andrew Reynolds
Remove uf-ss-totality option (#5251)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-16
Haniel Barbosa
[proof-new] Extending eqproof conversion to HO congruen...
tree
|
commitdiff
2020-09-16
Haniel Barbosa
[proof-new] A simple proof generator for buffered proof...
tree
|
commitdiff
2020-09-16
Andrew Reynolds
(proof-new) Make proofs mandatory in proof equality...
tree
|
commitdiff
2020-09-15
Andrew Reynolds
Standard equality engine notify class for Theory (...
tree
|
commitdiff
2020-09-14
Andrew Reynolds
Standardize uses of inference manager in datatypes...
tree
|
commitdiff
2020-09-11
Andrew Reynolds
Move finite model minimization to UF last call effort...
tree
|
commitdiff
2020-09-11
Andrew Reynolds
(proof-new) Handle mismatched assumptions in proof...
tree
|
commitdiff
2020-09-11
Andrew Reynolds
(proof-new) Use deep copy for final lemma step in proof...
tree
|
commitdiff
2020-09-10
Andrew Reynolds
Use state and inference manager in UF CardinalityExtens...
tree
|
commitdiff
2020-09-04
Andrew Reynolds
Add interfaces for making trust nodes in TheoryInferenc...
tree
|
commitdiff
2020-09-02
Andrew Reynolds
(proof-new) Add proof support in TheoryUF (#5002)
tree
|
commitdiff
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
tree
|
commitdiff
2020-08-31
Andrew Reynolds
Basic proof support in inference manager (#4975)
tree
|
commitdiff
2020-08-28
Andrew Reynolds
Replace Theory::Set with TheoryIdSet (#4959)
tree
|
commitdiff
2020-08-27
Andrew Reynolds
(proof-new) Add the proof equality engine (#4881)
tree
|
commitdiff
2020-08-27
Andrew Reynolds
(new theory) Update TheoryUF to new interface (#4944)
tree
|
commitdiff
2020-08-24
Andrew Reynolds
Add a few basic extensions for equality engine (#4937)
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-21
Andrew Reynolds
Simplify and fix care graph for ufHo (#4924)
tree
|
commitdiff
2020-08-20
Andrew Reynolds
Add TheoryState objects to each Theory (#4920)
tree
|
commitdiff
2020-08-20
Andrew Reynolds
Simplify trigger notifications in equality engine ...
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-13
Haniel Barbosa
[proof-new] Adding support for corner case of transitiv...
tree
|
commitdiff
2020-08-12
Haniel Barbosa
generalize handling MERGED_THROUGH_CONSTANST in EqProof...
tree
|
commitdiff
2020-08-12
Andrew Reynolds
(proof-new) Improve robustness of CONG rule (#4882)
tree
|
commitdiff
2020-08-12
Haniel Barbosa
(proof-new) Improving proof-production in Equality...
tree
|
commitdiff
2020-08-09
Andrew Reynolds
Make valuation class more robust to null underlying...
tree
|
commitdiff
2020-08-09
Andrew Reynolds
Splitting a few utility classes from EqualityEngine...
tree
|
commitdiff
2020-07-18
Haniel Barbosa
Improving equality engine tracing (#4770)
tree
|
commitdiff
2020-07-17
Haniel Barbosa
Fix EqProof to ProofNode conversion (#4760)
tree
|
commitdiff
2020-07-16
Haniel Barbosa
(proof-new) Implements the conversion between EqProof...
tree
|
commitdiff
2020-07-16
Haniel Barbosa
(proof-new) Adding API for converting EqProof into...
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-06-03
Haniel Barbosa
(proof-new) Adding rules and proof checker for EUF...
tree
|
commitdiff
2020-04-18
Haniel Barbosa
Improving EqProof printing (#4329)
tree
|
commitdiff
2020-04-14
Andrew Reynolds
Remove mergePredicates from EqualityEngine interface...
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-20
Andrew Reynolds
Guard cases of sort inference in quantifier free logics...
tree
|
commitdiff
2020-03-16
Andres Noetzli
Create master equality engine at context level 0 (...
tree
|
commitdiff
2020-03-12
Andrew Reynolds
Fix double notify in equality engine (#4036)
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-02-27
Andrew Reynolds
Initial work towards -Wshadow (#3817)
tree
|
commitdiff
2020-02-25
yoni206
remove redundant includes (#3815)
tree
|
commitdiff
2020-02-20
Mathias Preiner
resource manager: Add statistic for every resource...
tree
|
commitdiff
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
tree
|
commitdiff
2019-12-09
Andres Noetzli
Make theory rewriters non-static (#3547)
tree
|
commitdiff
2019-11-18
Andres Noetzli
Use -Wimplicit-fallthrough (#3464)
tree
|
commitdiff
2019-11-04
Andrew Reynolds
Fix ho extensionality in collect model info (#3435)
tree
|
commitdiff
2019-10-31
Mathias Preiner
Fix Unimplemented() macros missed in #3366. (#3424)
tree
|
commitdiff
2019-10-30
Mathias Preiner
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. ...
tree
|
commitdiff
2019-10-27
Andrew Reynolds
Fix collect model info for higher-order (#3409)
tree
|
commitdiff
2019-09-19
Andrew Reynolds
Support context-(in)dependent decision strategies....
tree
|
commitdiff
2019-09-13
Andrew Reynolds
Move higher-order matching predicate (#3280)
tree
|
commitdiff
2019-09-12
Andrew Reynolds
Rename UF with cardinality extension (#3241)
tree
|
commitdiff
2019-07-08
Andrew Reynolds
Towards refactoring relations (#3078)
tree
|
commitdiff
2019-07-02
Andrew Reynolds
Use unique_ptr for UF modules (#3080)
tree
|
commitdiff
2019-07-01
Andrew Reynolds
Split higher-order UF solver (#2890)
tree
|
commitdiff
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
tree
|
commitdiff
2019-04-18
Andrew Reynolds
Less aggressive caching in equality engine when proofs...
tree
|
commitdiff
2019-04-17
Andrew Reynolds
Cache explanations in the equality engine (#2937)
tree
|
commitdiff
2019-04-17
Andrew Reynolds
More use of isClosure (#2959)
tree
|
commitdiff
2019-03-26
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2019-03-15
Haniel Barbosa
New beta-reduction for HOL solving (#2869)
tree
|
commitdiff
2019-03-15
Andrew Reynolds
Fix non-variable function head elimination in UF. ...
tree
|
commitdiff
2018-12-11
Andrew Reynolds
Remove alternate versions of mbqi (#2742)
tree
|
commitdiff
2018-11-27
Andrew Reynolds
Make (T)NodeTrie a general utility (#2489)
tree
|
commitdiff
2018-09-22
Mathias Preiner
cmake: Remove unused CMakeLists.txt
tree
|
commitdiff
2018-09-22
Aina Niemetz
cmake: Added initial build infrastructure.
tree
|
commitdiff
2018-09-17
Andrew Reynolds
Decision strategy: incorporate UF with cardinality...
tree
|
commitdiff
2018-08-22
Andrew Reynolds
More unused code elimination (#2358)
tree
|
commitdiff
2018-08-21
Andrew Reynolds
More unused code elimination (#2339)
tree
|
commitdiff
2018-08-08
Andrew Reynolds
Move uf model code from uf to quantifiers (#2095)
tree
|
commitdiff
2018-08-02
Andrew Reynolds
Remove references to deprecated propagate as decision...
tree
|
commitdiff
2018-07-06
Andrew Reynolds
sygusComp2018: simplify beta reduction in uf rewriter...
tree
|
commitdiff
2018-06-25
Aina Niemetz
Updated copyright headers.
tree
|
commitdiff
2018-05-23
Andrew Reynolds
Add notions of evaluated kinds in TheoryModel (#1947)
tree
|
commitdiff
2018-04-30
Andrew Reynolds
Remove subsort symmetry breaking (#1807)
tree
|
commitdiff
2018-04-11
Andrew Reynolds
Properly implement function extensionality based on...
tree
|
commitdiff
2018-04-10
Andrew Reynolds
Fix higher-order term indexing. (#1754)
tree
|
commitdiff
next