projects
/
cvc5.git
/ search
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅ next
google test: expr: Migrate node_white. (#5869)
2021-01-27
Alex Ozdemir
Thread proofs through arith channels & similar (#5818)
commit
|
commitdiff
|
tree
2021-01-26
Alex Ozdemir
Add proofs to TheoryArithPrivate::propagate (#5812)
commit
|
commitdiff
|
tree
2021-01-21
Alex Ozdemir
arith: Proofs for Diophantine cuts (#5792)
commit
|
commitdiff
|
tree
2021-01-19
Alex Ozdemir
Implement proofs for arith BRAB lemmas (#5784)
commit
|
commitdiff
|
tree
2020-12-18
Alex Ozdemir
Bugfix: proofs for props of non-normal arith lits ...
commit
|
commitdiff
|
tree
2020-12-04
Alex Ozdemir
Use NodeDfsIterable for makeBinary (#5595)
commit
|
commitdiff
|
tree
2020-11-10
Alex Ozdemir
Pin LFSC version (#5412)
commit
|
commitdiff
|
tree
2020-10-21
Alex Ozdemir
(proof-new) Add arith proof macros file to CMake (...
commit
|
commitdiff
|
tree
2020-10-21
Alex Ozdemir
(proof-new) arith: dedup literals in flattenImpl (...
commit
|
commitdiff
|
tree
2020-10-15
Alex Ozdemir
(proof-new) TheoryArithPrivate: farkas lemma proof...
commit
|
commitdiff
|
tree
2020-10-14
Alex Ozdemir
(proof-new) debug statements & docs for INT_TRUST ...
commit
|
commitdiff
|
tree
2020-10-14
Alex Ozdemir
(proof-new) pfs in TheoryArith(Private) explainations...
commit
|
commitdiff
|
tree
2020-10-14
Alex Ozdemir
(proof-new) pfs for conflicts in TheoryArithPrivate...
commit
|
commitdiff
|
tree
2020-10-14
Alex Ozdemir
(proof-new) Prove lemmas in Constraint (#5254)
commit
|
commitdiff
|
tree
2020-10-09
Alex Ozdemir
use right arith explanation fn to fix regressions ...
commit
|
commitdiff
|
tree
2020-10-09
Alex Ozdemir
(proof-new) proofs for arith-constraint explanations...
commit
|
commitdiff
|
tree
2020-10-07
Alex Ozdemir
(proof-new) proofs in ee -> arith pipeline (#5215)
commit
|
commitdiff
|
tree
2020-10-06
Alex Ozdemir
(proof-new) proofs for ArithCongMan -> ee facts (#5207)
commit
|
commitdiff
|
tree
2020-10-02
Alex Ozdemir
(proof-new) New proofs in arith::Constraint::externalExplain...
commit
|
commitdiff
|
tree
2020-10-02
Alex Ozdemir
Remove duplicate declarations in th_bv.plf (#5183)
commit
|
commitdiff
|
tree
2020-09-29
Alex Ozdemir
(proof-new) Add proof managers and eager gens to arith...
commit
|
commitdiff
|
tree
2020-09-29
Alex Ozdemir
Add utilities for arith/proof_checker and build it...
commit
|
commitdiff
|
tree
2020-09-01
Alex Ozdemir
Add arithmetic-specific, runtime, proof-macros. (#4992)
commit
|
commitdiff
|
tree
2020-08-17
Alex Ozdemir
Add identifier name for side condition. (#4902)
commit
|
commitdiff
|
tree
2020-07-27
Alex Ozdemir
Consider negation's proof before triggering arith pfs...
commit
|
commitdiff
|
tree
2020-07-20
Alex Ozdemir
Fix a deadlock in the signature tests. (#4772)
commit
|
commitdiff
|
tree
2020-06-28
Alex Ozdemir
Proof Rules and Checker for Arithmetic (#4665)
commit
|
commitdiff
|
tree
2020-06-20
Alex Ozdemir
Use traversal iterators in IntToBv (#4169)
commit
|
commitdiff
|
tree
2020-04-11
Alex Ozdemir
Add skip predicate to node traversal. (#4222)
commit
|
commitdiff
|
tree
2020-03-28
Alex Ozdemir
Node traversal iterator (#3845)
commit
|
commitdiff
|
tree
2020-03-18
Alex Ozdemir
Move node visitor class from smt_util/ to expr/ (#4110)
commit
|
commitdiff
|
tree
2020-03-16
Alex Ozdemir
Remove AlwaysAssert(false) for hole.
commit
|
commitdiff
|
tree
2020-03-16
Alex Ozdemir
clang-format
commit
|
commitdiff
|
tree
2020-03-16
Alex Ozdemir
Fix simplicity check in prop
commit
|
commitdiff
|
tree
2020-03-16
Alex Ozdemir
Fix antecedent loop. Whoops
commit
|
commitdiff
|
tree
2020-03-16
Alex Ozdemir
Only save farkas+tightening proofs. Error on holes
commit
|
commitdiff
|
tree
2020-03-16
Alex Ozdemir
Expand the definition of a "simple" farkas proof.
commit
|
commitdiff
|
tree
2020-03-10
Alex Ozdemir
Document bv-to-bool recursion (#3848)
commit
|
commitdiff
|
tree
2020-03-05
Alex Ozdemir
Add a new arith constraint proof rule: IntTightenAP...
commit
|
commitdiff
|
tree
2020-03-05
Alex Ozdemir
Revert "Add a new arith constraint proof rule: IntTightenAP...
commit
|
commitdiff
|
tree
2020-02-22
Alex Ozdemir
RIP th_lra.plf (#3796)
commit
|
commitdiff
|
tree
2020-02-22
Alex Ozdemir
Switch to th_lira.plf (#3741)
commit
|
commitdiff
|
tree
2020-02-21
Alex Ozdemir
Remove IntReal tightening axioms from th_lira.plf ...
commit
|
commitdiff
|
tree
2020-02-11
Alex Ozdemir
Implement LFSCArithProof::equalityType. (#3740)
commit
|
commitdiff
|
tree
2020-02-10
Alex Ozdemir
Add function for tightening literals (#3732)
commit
|
commitdiff
|
tree
2020-02-10
Alex Ozdemir
Add more IntReal predicates (#3731)
commit
|
commitdiff
|
tree
2020-02-07
Alex Ozdemir
Propagate expected types through UF arguments (#3717)
commit
|
commitdiff
|
tree
2020-02-07
Alex Ozdemir
Add `ArithProof::{printInteger,getLfscFunction}` (...
commit
|
commitdiff
|
tree
2020-02-04
Alex Ozdemir
Articulate proof-related debug statements in arith...
commit
|
commitdiff
|
tree
2020-02-04
Alex Ozdemir
Regression tests for arithmetic proofs. (#3701)
commit
|
commitdiff
|
tree
2020-02-01
Alex Ozdemir
Handle `expectedType` in TheoryProofEngine (#3691)
commit
|
commitdiff
|
tree
2020-01-30
Alex Ozdemir
expectedType in proof-printing code (#3665)
commit
|
commitdiff
|
tree
2020-01-26
Alex Ozdemir
Axioms for affine function bounds. Tests. (#3632)
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Types and side conditions for affine bounds (#3631)
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Affine Axioms (#3630)
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Types & side-conditions for linear and affine fns ...
commit
|
commitdiff
|
tree
2020-01-21
Alex Ozdemir
Axioms (and side conditions) for tightening bounds...
commit
|
commitdiff
|
tree
2020-01-18
Alex Ozdemir
LIRA proof: Arithmetic predicates & reification thereof...
commit
|
commitdiff
|
tree
2020-01-17
Alex Ozdemir
LIRA sig: int, real terms, and conversions (#3610)
commit
|
commitdiff
|
tree
2019-12-31
Alex Ozdemir
[proof] ITE translation fix (#3484)
commit
|
commitdiff
|
tree
2019-12-06
Alex Ozdemir
[proof] Eliminate side-condition from ER signature...
commit
|
commitdiff
|
tree
2019-11-19
Alex Ozdemir
Add a few comments to ProofManager (#3477)
commit
|
commitdiff
|
tree
2019-11-19
Alex Ozdemir
Signature documentation update (#3476)
commit
|
commitdiff
|
tree
2019-11-14
Alex Ozdemir
Use Shebang in cxxtestgen when appropriate (#3458)
commit
|
commitdiff
|
tree
2019-07-02
Alex Ozdemir
Optimize DRAT optimization: clause matching (#3074)
commit
|
commitdiff
|
tree
2019-06-05
Alex Ozdemir
DRAT-Optimization (#2971)
commit
|
commitdiff
|
tree
2019-04-23
Alex Ozdemir
[BV] An option for SAT proof optimization (#2915)
commit
|
commitdiff
|
tree
2019-04-05
Alex Ozdemir
SatClauseSetHashFunction (#2916)
commit
|
commitdiff
|
tree
2019-03-16
Alex Ozdemir
Enable CryptoMiniSat-backed BV proofs (#2847)
commit
|
commitdiff
|
tree
2019-03-01
Alex Ozdemir
ErProof class with LFSC output (#2812)
commit
|
commitdiff
|
tree
2019-01-24
Alex Ozdemir
Extended DRAT signature to operational DRAT (#2815)
commit
|
commitdiff
|
tree
2019-01-18
Alex Ozdemir
Extract DIMACS Printing (#2800)
commit
|
commitdiff
|
tree
2019-01-16
Alex Ozdemir
Bugfix: LFSC clause equality (#2801)
commit
|
commitdiff
|
tree
2019-01-16
Alex Ozdemir
Extended Resolution Signature (#2788)
commit
|
commitdiff
|
tree
2019-01-14
Alex Ozdemir
ClausalBitvectorProof (#2786)
commit
|
commitdiff
|
tree
2019-01-13
Alex Ozdemir
LFSC LRAT Output (#2787)
commit
|
commitdiff
|
tree
2019-01-12
Alex Ozdemir
LratInstruction inheritance (#2784)
commit
|
commitdiff
|
tree
2019-01-11
Alex Ozdemir
Fixed linking against drat2er, and use drat2er (#2785)
commit
|
commitdiff
|
tree
2019-01-09
Alex Ozdemir
[BV Proofs] Option for proof format (#2777)
commit
|
commitdiff
|
tree
2019-01-09
Alex Ozdemir
Clause proof printing (#2779)
commit
|
commitdiff
|
tree
2019-01-09
Alex Ozdemir
LFSC drat output (#2776)
commit
|
commitdiff
|
tree
2019-01-06
Alex Ozdemir
[DRAT] DRAT data structure (#2767)
commit
|
commitdiff
|
tree
2019-01-04
Alex Ozdemir
[LRAT] A C++ data structure for LRAT. (#2737)
commit
|
commitdiff
|
tree
2019-01-03
Alex Ozdemir
[LRA proof] Recording & Printing LRA Proofs (#2758)
commit
|
commitdiff
|
tree
2018-12-17
Alex Ozdemir
Configured for linking against drat2er (#2754)
commit
|
commitdiff
|
tree
2018-12-17
Alex Ozdemir
DRAT Signature (#2757)
commit
|
commitdiff
|
tree
2018-12-15
Alex Ozdemir
[LRA Proof] Storage for LRA proofs (#2747)
commit
|
commitdiff
|
tree
2018-12-12
Alex Ozdemir
[LRA proof] More complete LRA example proofs. (#2722)
commit
|
commitdiff
|
tree
2018-12-12
Alex Ozdemir
[LRAT] signature robust against duplicate literals...
commit
|
commitdiff
|
tree
2018-12-11
Alex Ozdemir
LRAT signature (#2731)
commit
|
commitdiff
|
tree
2018-12-07
Alex Ozdemir
Arith Constraint Proof Loggin (#2732)
commit
|
commitdiff
|
tree
2018-12-07
Alex Ozdemir
Enable BV proofs when using an eager bitblaster (#2733)
commit
|
commitdiff
|
tree
2018-12-03
Alex Ozdemir
Bit vector proof superclass (#2599)
commit
|
commitdiff
|
tree
2018-11-27
Alex Ozdemir
LRA proof signature fixes and a first proof for linear...
commit
|
commitdiff
|
tree
2018-11-20
Alex Ozdemir
Change lemma proof step storage & iterators (#2712)
commit
|
commitdiff
|
tree
2018-10-02
Alex Ozdemir
Fix documentation for `make regress`. (#2557)
commit
|
commitdiff
|
tree