projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
Track instantiation reasons in proofs (#6935)
[cvc5.git]
/
src
/
theory
/
quantifiers
/
instantiate.h
2021-07-27
Andrew Reynolds
Track instantiation reasons in proofs (#6935)
blob
|
commitdiff
|
raw
2021-07-01
Andrew Reynolds
Add option to limit the number of instantiation rounds...
blob
|
commitdiff
|
raw
|
diff to current
2021-05-24
Andrew Reynolds
Move proof utilities to src/proof/ (#6611)
blob
|
commitdiff
|
raw
|
diff to current
2021-05-13
Mathias Preiner
Add std::hash overloads for Node, TNode and TypeNode...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-14
Gereon Kremer
Refactor / reimplement statistics (#6162)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-14
Aina Niemetz
Rename public and private headers in src/include. ...
blob
|
commitdiff
|
raw
|
diff to current
2021-04-12
Aina Niemetz
Refactor and update copyright headers. (#6316)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-09
Aina Niemetz
Rename CVC4__ header guards to CVC5__. (#6326)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-08
Andrew Reynolds
Add identifiers for sources of incompleteness (#6311)
blob
|
commitdiff
|
raw
|
diff to current
2021-04-01
Aina Niemetz
Rename namespace CVC5 to cvc5. (#6258)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-31
Aina Niemetz
Rename namespace CVC4 to CVC5. (#6249)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-30
Andrew Reynolds
Implement simple tracking of instantiation lemmas ...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-23
Andrew Reynolds
Passing term registry to ematching utilities (#6190)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-23
Andrew Reynolds
Moving instantiate and skolemize into quantifiers infer...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-11
Andrew Reynolds
Introduce inference ids for quantifier instantiation...
blob
|
commitdiff
|
raw
|
diff to current
2021-03-09
Gereon Kremer
Some more cleanup of includes (#6083)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
blob
|
commitdiff
|
raw
|
diff to current
2021-03-02
Gereon Kremer
Clean up includes to reduce compile times (#6031)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-23
Andrew Reynolds
Explanation of failure for instantiate, use in enumerat...
blob
|
commitdiff
|
raw
|
diff to current
2021-02-19
Andrew Reynolds
Simplify interface to instantiate (#5926)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-17
Andrew Reynolds
Move methods from term util to quantifiers registry...
blob
|
commitdiff
|
raw
|
diff to current
2021-02-10
Andrew Reynolds
Remove track instantiations infrastructure (#5883)
blob
|
commitdiff
|
raw
|
diff to current
2021-02-08
Andrew Reynolds
Use quantifiers inference manager for lemma management...
blob
|
commitdiff
|
raw
|
diff to current
2021-01-27
Andrew Reynolds
(proof-new) Improvements to quantifiers engine and...
blob
|
commitdiff
|
raw
|
diff to current
2021-01-26
Andrew Reynolds
Refactor quantifiers engine initialization (#5813)
blob
|
commitdiff
|
raw
|
diff to current
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-03
Andrew Reynolds
(proof-new) Support proofs of quantifier instantiation...
blob
|
commitdiff
|
raw
|
diff to current
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
blob
|
commitdiff
|
raw
|
diff to current
2020-08-11
Andrew Reynolds
Remove instantiation model true option (#4861)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-14
Andrew Reynolds
Debug instantiations output (#4739)
blob
|
commitdiff
|
raw
|
diff to current
2020-07-13
Andrew Reynolds
Statistics on instantiations per quantified formula...
blob
|
commitdiff
|
raw
|
diff to current
2020-06-16
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2020-04-14
Andrew Reynolds
Fix relevant domain computation for nested quantifiers...
blob
|
commitdiff
|
raw
|
diff to current
2020-03-10
Andrew Reynolds
Remove instantiation propagator infrastructure (#3975)
blob
|
commitdiff
|
raw
|
diff to current
2019-09-11
Andrew Reynolds
Infrastructure for instantiation rewriter (#3262)
blob
|
commitdiff
|
raw
|
diff to current
2019-08-05
Andrew Reynolds
Remove forward declarations in quantifiers engine ...
blob
|
commitdiff
|
raw
|
diff to current
2019-04-24
Mathias Preiner
Do not use __ prefix for header guards. (#2974)
blob
|
commitdiff
|
raw
|
diff to current
2019-03-26
Aina Niemetz
Update copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2018-06-25
Aina Niemetz
Updated copyright headers.
blob
|
commitdiff
|
raw
|
diff to current
2018-03-05
Mathias Preiner
Enable -Wsuggest-override by default. (#1643)
blob
|
commitdiff
|
raw
|
diff to current
2017-11-25
Andrew Reynolds
(Refactor) Instantiate utility (#1387)
blob
|
commitdiff
|
raw
|
diff to current