projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
A few more miscellaneous uses of EnvObj (#7325)
[cvc5.git]
/
src
/
proof
/
2021-10-07
Andrew Reynolds
Finish the LFSC printer (#7285)
tree
|
commitdiff
2021-10-01
Andrew Reynolds
Add the LFSC printer (#7158)
tree
|
commitdiff
2021-09-23
Lachnitt
[proofs[ Alethe: Fix Order of Arguments of addAletheSte...
tree
|
commitdiff
2021-09-23
Lachnitt
[proofs] Alethe: Translate THEORY_REWRITE (#7236)
tree
|
commitdiff
2021-09-23
Lachnitt
[proofs] Alethe: Add Alethe Files to be Compiled ...
tree
|
commitdiff
2021-09-23
Lachnitt
[proofs] Alethe: Translate SCOPE rule (#7224)
tree
|
commitdiff
2021-09-23
Andrew Reynolds
Implement alpha equivalence proofs (#7066)
tree
|
commitdiff
2021-09-21
Lachnitt
[Proofs] Alethe: Translate ASSUME rule (#7213)
tree
|
commitdiff
2021-09-21
Lachnitt
[proofs] Alethe: Implementation of AletheProofPostproce...
tree
|
commitdiff
2021-09-20
Haniel Barbosa
[proofs] Alethe: adds a node converter
tree
|
commitdiff
2021-09-20
Andrew Reynolds
Add the LFSC proof post-processor (#7134)
tree
|
commitdiff
2021-09-17
Lachnitt
[proofs] Alethe: Added Proof Postprocessor to alethe_pr...
tree
|
commitdiff
2021-09-17
Lachnitt
[proofs] Alethe: Added Final Callback Function to aleth...
tree
|
commitdiff
2021-09-15
Lachnitt
[proofs] Alethe: Added Callback Function to alethe_proo...
tree
|
commitdiff
2021-09-15
Lachnitt
[proof] Added printer for proof rule names (#7185)
tree
|
commitdiff
2021-09-15
Lachnitt
[proof] Alethe proof rules (#7180)
tree
|
commitdiff
2021-09-08
Andrew Reynolds
Add Lfsc print channel utilities (#7123)
tree
|
commitdiff
2021-09-08
Andrew Reynolds
Improve pre-skolemization, move quantifiers preprocess...
tree
|
commitdiff
2021-09-08
Andrew Reynolds
Add LFSC side condition conversion utility for list...
tree
|
commitdiff
2021-09-08
Andrew Reynolds
Use rewriteViaMethod instead of accessing builtin proof...
tree
|
commitdiff
2021-09-02
Andrew Reynolds
Add LFSC node converter (#6944)
tree
|
commitdiff
2021-09-02
Andrew Reynolds
Implement lazy proof checking modes (#7106)
tree
|
commitdiff
2021-09-01
Andrew Reynolds
Fix issues with cyclic proofs due to double SYMM applic...
tree
|
commitdiff
2021-09-01
Andrew Reynolds
Lazy proof reconstruction for strings theory solver...
tree
|
commitdiff
2021-08-30
Andrew Reynolds
Fix proof equality engine for "no-explain" premises...
tree
|
commitdiff
2021-08-24
Andrew Reynolds
Uniform treatment of trusted theory inferences in proof...
tree
|
commitdiff
2021-08-24
Andrew Reynolds
Miscellaneous changes from proof-new (#7042)
tree
|
commitdiff
2021-08-04
Andrew Reynolds
Proper printing of proofs in the internal calculus...
tree
|
commitdiff
2021-08-04
Andrew Reynolds
Fix policy for merging subproofs (#6981)
tree
|
commitdiff
2021-08-04
Diego Della Rocca...
[proof] [dot] Fix comments on dot printer (#6983)
tree
|
commitdiff
2021-08-04
Andrew Reynolds
Add containsAssumption proof utility (#6953)
tree
|
commitdiff
2021-07-27
Mathias Preiner
proof: Add eqrange expansion rule. (#6936)
tree
|
commitdiff
2021-07-27
Andrew Reynolds
Track instantiation reasons in proofs (#6935)
tree
|
commitdiff
2021-07-27
Andrew Reynolds
Add basic LFSC utilities (#6879)
tree
|
commitdiff
2021-07-27
Andrew Reynolds
Add print expression utility (#6880)
tree
|
commitdiff
2021-07-27
Andrew Reynolds
Add proof letify utility (#6881)
tree
|
commitdiff
2021-07-26
Andrew Reynolds
Enable default equality proofs for sets (#6931)
tree
|
commitdiff
2021-07-22
Andrew Reynolds
Preparation for carry the rewrite rule database in...
tree
|
commitdiff
2021-07-15
Andrew Reynolds
Distinguish quantifiers preprocess as its own proof...
tree
|
commitdiff
2021-07-13
Mathias Preiner
bv: Simplify BV_BITBLAST_* proof rules. (#6871)
tree
|
commitdiff
2021-07-08
Haniel Barbosa
[proof] [dot] Print let map (of terms in proof) as...
tree
|
commitdiff
2021-06-30
Andrew Reynolds
Fix pre vs. post-rewrite in proofs for theory preproces...
tree
|
commitdiff
2021-06-28
Haniel Barbosa
[proof] [dot] Make dot printer stateful (#6799)
tree
|
commitdiff
2021-06-23
Haniel Barbosa
[proofs] [dot] Adding a counter for subproofs (#6735)
tree
|
commitdiff
2021-06-21
Haniel Barbosa
[proof] Fix documentation of array rule (#6770)
tree
|
commitdiff
2021-06-07
Andrew Reynolds
(proof-new) Fix missing connection in trust substitutio...
tree
|
commitdiff
2021-06-07
Andrew Reynolds
(proof-new) Lazy proof chain debug names (#6680)
tree
|
commitdiff
2021-05-27
Andrew Reynolds
Update proof namespaces (#6614)
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-20
Haniel Barbosa
Remove old unsat cores (#6581)
tree
|
commitdiff
2021-05-13
Mathias Preiner
Add std::hash overloads for Node, TNode and TypeNode...
tree
|
commitdiff
2021-04-26
Diego Della Rocca...
New design in DOT representation, nodes colored based...
tree
|
commitdiff
2021-04-22
Haniel Barbosa
Reconciling proofs and unsat cores (#6405)
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-14
Haniel Barbosa
[proof-new] Miscellaneous improvements to dot printer...
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-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-15
Gereon Kremer
Replace HistogramStat by IntegralHistogramStat (#6126)
tree
|
commitdiff
2021-03-14
Diego Della Rocca...
[proof-new] Adding a dot printer for proof nodes (...
tree
|
commitdiff
2021-03-11
Gereon Kremer
First refactoring of statistics classes (#6105)
tree
|
commitdiff
2021-03-11
Aina Niemetz
Delete Expr layer. (#6117)
tree
|
commitdiff
2021-03-09
Aina Niemetz
Update copyright headers to 2021. (#6081)
tree
|
commitdiff
2021-03-03
Gereon Kremer
More cleanup of includes to reduce compilation times...
tree
|
commitdiff
2021-01-05
Andrew Reynolds
Remove a few miscellaneous references to the expr layer...
tree
|
commitdiff
2020-12-03
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-11-19
Aina Niemetz
Include stddef.h (needed for size_t) in cvc4_public...
tree
|
commitdiff
2020-11-19
Andrew Reynolds
Use symbol manager for unsat cores (#5468)
tree
|
commitdiff
2020-10-28
Andrew Reynolds
Remove more uses of Expr (#5357)
tree
|
commitdiff
2020-09-22
Mathias Preiner
Update copyright header script to support CMake and...
tree
|
commitdiff
2020-09-16
Abdalrhman Mohamed
Dump commands in internal code using command printing...
tree
|
commitdiff
2020-09-01
Haniel Barbosa
Removes old proof code (#4964)
tree
|
commitdiff
2020-08-17
Andrew Reynolds
Dynamic allocation of equality engine in Theory (#4890)
tree
|
commitdiff
2020-07-28
Andrew Reynolds
Use lemma property enum for OutputChannel::lemma (...
tree
|
commitdiff
2020-07-11
Andrew Reynolds
(proof-new) Update Theory interface for proof-new ...
tree
|
commitdiff
2020-07-03
Andres Noetzli
Remove SWIG bindings (#4683)
tree
|
commitdiff
2020-06-19
Haniel Barbosa
Generalize atom collection in old proof code (#4626)
tree
|
commitdiff
2020-06-18
Andres Noetzli
Improve memory management in Java bindings (#4629)
tree
|
commitdiff
2020-06-16
Aina Niemetz
Update copyright headers.
tree
|
commitdiff
2020-03-27
Andres Noetzli
Fix issues with unsat cores and reset-assertions (...
tree
|
commitdiff
2020-03-18
Alex Ozdemir
Move node visitor class from smt_util/ to expr/ (#4110)
tree
|
commitdiff
2020-03-16
Alex Ozdemir
Remove AlwaysAssert(false) for hole.
tree
|
commitdiff
2020-03-16
Alex Ozdemir
Only save farkas+tightening proofs. Error on holes
tree
|
commitdiff
2020-03-11
Andres Noetzli
Set assertion in `CnfStream::ensureLiteral()` (#3927)
tree
|
commitdiff
2020-03-05
Mathias Preiner
Enable -Wshadow and fix warnings. (#3909)
tree
|
commitdiff
2020-02-27
Andres Noetzli
Fix -Wshadow warnings in common headers (#3826)
tree
|
commitdiff
2020-02-22
Alex Ozdemir
Switch to th_lira.plf (#3741)
tree
|
commitdiff
2020-02-20
Andrew Reynolds
Remove front-end support for Chain (#3767)
tree
|
commitdiff
2020-02-12
Andres Noetzli
Rename Java package to edu.stanford.CVC4 (#3752)
tree
|
commitdiff
2020-02-11
Alex Ozdemir
Implement LFSCArithProof::equalityType. (#3740)
tree
|
commitdiff
2020-02-10
Alex Ozdemir
Add function for tightening literals (#3732)
tree
|
commitdiff
2020-02-07
Alex Ozdemir
Propagate expected types through UF arguments (#3717)
tree
|
commitdiff
2020-02-07
Alex Ozdemir
Add `ArithProof::{printInteger,getLfscFunction}` (...
tree
|
commitdiff
2020-02-01
Alex Ozdemir
Handle `expectedType` in TheoryProofEngine (#3691)
tree
|
commitdiff
2020-01-30
Alex Ozdemir
expectedType in proof-printing code (#3665)
tree
|
commitdiff
2019-12-31
Alex Ozdemir
[proof] ITE translation fix (#3484)
tree
|
commitdiff
2019-12-17
Mathias Preiner
Generate code for options with modes. (#3561)
tree
|
commitdiff
next