projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix another rewrite involving iand (#8054)
[cvc5.git]
/
src
/
proof
/
2022-02-03
Aina Niemetz
Rename kind PLUS -> ADD. (#8036)
tree
|
commitdiff
2022-02-02
Aina Niemetz
Rename kinds MINUS -> SUB and UMINUS -> NEG. (#8035)
tree
|
commitdiff
2022-02-02
Andrew Reynolds
Fix printing of re.loop as an operator in LFSC (#8029)
tree
|
commitdiff
2022-02-02
Andrew Reynolds
Add missing null terminators for regexp (#8027)
tree
|
commitdiff
2022-02-02
Andrew Reynolds
Extend proof step buffer to optionally ensure unique...
tree
|
commitdiff
2022-01-10
Andrew Reynolds
Fix internal type error when printing lambdas with...
tree
|
commitdiff
2021-12-20
Andrew Reynolds
Updates to LFSC signatures (#7840)
tree
|
commitdiff
2021-12-13
Andrew Reynolds
Distinguishing more uses of CONST_RATIONAL (#7802)
tree
|
commitdiff
2021-12-13
Andrew Reynolds
Initial cut at distinguishing uses of CONST_RATIONAL...
tree
|
commitdiff
2021-12-10
Haniel Barbosa
[proofs] Make LazyCDProofChain extend CDProof (#7726)
tree
|
commitdiff
2021-12-09
Andrew Reynolds
Remove a few static access to options in proof code...
tree
|
commitdiff
2021-12-07
Gereon Kremer
Remove more static accesses to options (#7764)
tree
|
commitdiff
2021-12-07
Andrew Reynolds
Add proof annotation option (#7750)
tree
|
commitdiff
2021-12-07
Lachnitt
[proofs] Alethe: Add ARITH_TRICHOTOMY to updater (...
tree
|
commitdiff
2021-12-07
Lachnitt
[proofs] Alethe: Fix Bug in Finalize (#7746)
tree
|
commitdiff
2021-12-03
Lachnitt
[proofs] Alethe: Implementation of Process Function...
tree
|
commitdiff
2021-12-01
Haniel Barbosa
[proofs] Add method to CDProof to obtain number of...
tree
|
commitdiff
2021-12-01
Lachnitt
[proofs] Alethe: Add finalize function to insert missin...
tree
|
commitdiff
2021-12-01
Lachnitt
Alethe: Add function that adds final steps to proof...
tree
|
commitdiff
2021-11-30
Lachnitt
Alethe: Further Printer Implementation (#7675)
tree
|
commitdiff
2021-11-30
Lachnitt
[proofs] Alethe: Implementation of Printer (#7674)
tree
|
commitdiff
2021-11-30
Lachnitt
[proofs] Alethe: Printer Specification (#7673)
tree
|
commitdiff
2021-11-23
Gereon Kremer
Push output language inside the printing code (#7683)
tree
|
commitdiff
2021-11-22
Gereon Kremer
Refactor IO stream manipulators (#7555)
tree
|
commitdiff
2021-11-18
Lachnitt
[proofs] Alethe: Rename DUPLICATED_LITERALS (#7661)
tree
|
commitdiff
2021-11-17
Andrew Reynolds
Preparations for eliminating arithmetic subtyping ...
tree
|
commitdiff
2021-11-12
mudathirmahgoub
bags: Rename kinds with a more consistent naming scheme...
tree
|
commitdiff
2021-11-12
Andrew Reynolds
[proofs] Cancel SYMM in CDProof, throw an error for...
tree
|
commitdiff
2021-11-12
Andres Noetzli
Remove `ConstantMap<Rational>` (#7635)
tree
|
commitdiff
2021-11-10
Lachnitt
[proofs] Alethe: Translate of Arithmetic rules (#7613)
tree
|
commitdiff
2021-11-10
Lachnitt
[proofs] Alethe: Translate INSTANTIATE rule (#7607)
tree
|
commitdiff
2021-11-09
Lachnitt
[proofs] Alethe: Translate Further Equality rules ...
tree
|
commitdiff
2021-11-09
Lachnitt
[proofs] Alethe: Translate Equality rules (#7605)
tree
|
commitdiff
2021-11-09
Haniel Barbosa
[proofs] Generalize trivial cycle detection in LazyCDPr...
tree
|
commitdiff
2021-11-09
Lachnitt
[proofs] Alethe: Translate REORDERING rule (#7533)
tree
|
commitdiff
2021-11-08
Andrew Reynolds
Add lambda lift utility (#7601)
tree
|
commitdiff
2021-11-08
Aina Niemetz
sets: Rename kinds with a more consistent naming scheme...
tree
|
commitdiff
2021-11-08
Haniel Barbosa
[proofs] Adding NoSubtype node converter to Alethe...
tree
|
commitdiff
2021-11-08
Haniel Barbosa
[proofs] Method to convert node representation of Aleth...
tree
|
commitdiff
2021-11-06
Gereon Kremer
Remove `Notice()` in favor of new `verbose()` (#7588)
tree
|
commitdiff
2021-11-05
Haniel Barbosa
[proofs] Fix open sat proof (#7509)
tree
|
commitdiff
2021-11-05
Lachnitt
Alethe: Translate CNF rules (#7532)
tree
|
commitdiff
2021-10-29
Andrew Reynolds
Minor cleanup of proof messages (#7494)
tree
|
commitdiff
2021-10-29
Andrew Reynolds
Add PfRule ARITH_POLY_NORM (#7501)
tree
|
commitdiff
2021-10-29
Andrew Reynolds
Improvements for LFSC proof conversion (#7524)
tree
|
commitdiff
2021-10-26
Haniel Barbosa
[proofs] Modularize check for whether a clause is singl...
tree
|
commitdiff
2021-10-26
Andrew Reynolds
Disable automatic symmetry in proofs of theory explanat...
tree
|
commitdiff
2021-10-26
Lachnitt
[proofs] Alethe: Translate Block of clause pattern...
tree
|
commitdiff
2021-10-26
Lachnitt
[proofs] Alethe: Translate AND_INTRO rule (#7405)
tree
|
commitdiff
2021-10-26
Lachnitt
[proofs] Alethe: Translate AND_ELIM rule (#7404)
tree
|
commitdiff
2021-10-26
Lachnitt
[proofs] Alethe: Translate CONTRA rule (#7403)
tree
|
commitdiff
2021-10-26
Lachnitt
[proofs] Alethe: Translate NOT_NOT_ELIM rule (#7402)
tree
|
commitdiff
2021-10-25
Lachnitt
[proofs] Alethe: Translate MODUS_PONENS rule (#7401)
tree
|
commitdiff
2021-10-25
Lachnitt
[proofs] Alethe: Translate EQ_RESOLVE rule (#7400)
tree
|
commitdiff
2021-10-25
Lachnitt
[proofs] Alethe: Translate SPLIT rule (#7399)
tree
|
commitdiff
2021-10-22
Gereon Kremer
Fix out-of-sync pruning in CDCAC proofs (#7470)
tree
|
commitdiff
2021-10-22
Lachnitt
[proofs] Alethe: Translate FACTORING rule (#7398)
tree
|
commitdiff
2021-10-22
Lachnitt
[proofs] Alethe: Translate CHAIN_RESOLUTION rule (...
tree
|
commitdiff
2021-10-20
Andrew Reynolds
Eliminate last static calls to rewriter from smt layer...
tree
|
commitdiff
2021-10-20
Lachnitt
[proofs] Alethe: Documentation on Translation (#7394)
tree
|
commitdiff
2021-10-11
Aina Niemetz
Rename SmtScope to SolverEngineScope. (#7284)
tree
|
commitdiff
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
next