projects / cvc5.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Rename namespace CVC4 to CVC5. (#6249)
2021-03-11 Alex Ozdemirarith proof rules shuffle & add ARITH_SUM_UB (#6118)
 commit | commitdiff | tree
2021-01-27 Alex OzdemirThread proofs through arith channels & similar (#5818)
 commit | commitdiff | tree
2021-01-26 Alex OzdemirAdd proofs to TheoryArithPrivate::propagate (#5812)
 commit | commitdiff | tree
2021-01-21 Alex Ozdemirarith: Proofs for Diophantine cuts (#5792)
 commit | commitdiff | tree
2021-01-19 Alex OzdemirImplement proofs for arith BRAB lemmas (#5784)
 commit | commitdiff | tree
2020-12-18 Alex OzdemirBugfix: proofs for props of non-normal arith lits ...
commit | commitdiff | tree
2020-12-04 Alex OzdemirUse NodeDfsIterable for makeBinary (#5595)
 commit | commitdiff | tree
2020-11-10 Alex OzdemirPin 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 Ozdemiruse 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 OzdemirRemove 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 OzdemirAdd utilities for arith/proof_checker and build it...
commit | commitdiff | tree
2020-09-01 Alex OzdemirAdd arithmetic-specific, runtime, proof-macros. (#4992)
 commit | commitdiff | tree
2020-08-17 Alex OzdemirAdd identifier name for side condition. (#4902)
 commit | commitdiff | tree
2020-07-27 Alex OzdemirConsider negation's proof before triggering arith pfs...
commit | commitdiff | tree
2020-07-20 Alex OzdemirFix a deadlock in the signature tests. (#4772)
 commit | commitdiff | tree
2020-06-28 Alex OzdemirProof Rules and Checker for Arithmetic (#4665)
 commit | commitdiff | tree
2020-06-20 Alex OzdemirUse traversal iterators in IntToBv (#4169)
 commit | commitdiff | tree
2020-04-11 Alex OzdemirAdd skip predicate to node traversal. (#4222)
 commit | commitdiff | tree
2020-03-28 Alex OzdemirNode traversal iterator (#3845)
 commit | commitdiff | tree
2020-03-18 Alex OzdemirMove node visitor class from smt_util/ to expr/ (#4110)
 commit | commitdiff | tree
2020-03-16 Alex OzdemirRemove AlwaysAssert(false) for hole.
 commit | commitdiff | tree
2020-03-16 Alex Ozdemirclang-format
 commit | commitdiff | tree
2020-03-16 Alex OzdemirFix simplicity check in prop
 commit | commitdiff | tree
2020-03-16 Alex OzdemirFix antecedent loop. Whoops
 commit | commitdiff | tree
2020-03-16 Alex OzdemirOnly save farkas+tightening proofs. Error on holes
 commit | commitdiff | tree
2020-03-16 Alex OzdemirExpand the definition of a "simple" farkas proof.
 commit | commitdiff | tree
2020-03-10 Alex OzdemirDocument bv-to-bool recursion (#3848)
 commit | commitdiff | tree
2020-03-05 Alex OzdemirAdd a new arith constraint proof rule: IntTightenAP...
commit | commitdiff | tree
2020-03-05 Alex OzdemirRevert "Add a new arith constraint proof rule: IntTightenAP...
commit | commitdiff | tree
2020-02-22 Alex OzdemirRIP th_lra.plf (#3796)
 commit | commitdiff | tree
2020-02-22 Alex OzdemirSwitch to th_lira.plf (#3741)
 commit | commitdiff | tree
2020-02-21 Alex OzdemirRemove IntReal tightening axioms from th_lira.plf ...
commit | commitdiff | tree
2020-02-11 Alex OzdemirImplement LFSCArithProof::equalityType. (#3740)
 commit | commitdiff | tree
2020-02-10 Alex OzdemirAdd function for tightening literals (#3732)
 commit | commitdiff | tree
2020-02-10 Alex OzdemirAdd more IntReal predicates (#3731)
 commit | commitdiff | tree
2020-02-07 Alex OzdemirPropagate expected types through UF arguments (#3717)
 commit | commitdiff | tree
2020-02-07 Alex OzdemirAdd `ArithProof::{printInteger,getLfscFunction}` (...
commit | commitdiff | tree
2020-02-04 Alex OzdemirArticulate proof-related debug statements in arith...
commit | commitdiff | tree
2020-02-04 Alex OzdemirRegression tests for arithmetic proofs. (#3701)
 commit | commitdiff | tree
2020-02-01 Alex OzdemirHandle `expectedType` in TheoryProofEngine (#3691)
 commit | commitdiff | tree
2020-01-30 Alex OzdemirexpectedType in proof-printing code (#3665)
 commit | commitdiff | tree
2020-01-26 Alex OzdemirAxioms for affine function bounds. Tests. (#3632)
 commit | commitdiff | tree
2020-01-21 Alex OzdemirTypes and side conditions for affine bounds (#3631)
 commit | commitdiff | tree
2020-01-21 Alex OzdemirAffine Axioms (#3630)
 commit | commitdiff | tree
2020-01-21 Alex OzdemirTypes & side-conditions for linear and affine fns ...
commit | commitdiff | tree
2020-01-21 Alex OzdemirAxioms (and side conditions) for tightening bounds...
commit | commitdiff | tree
2020-01-18 Alex OzdemirLIRA proof: Arithmetic predicates & reification thereof...
commit | commitdiff | tree
2020-01-17 Alex OzdemirLIRA 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 OzdemirAdd a few comments to ProofManager (#3477)
 commit | commitdiff | tree
2019-11-19 Alex OzdemirSignature documentation update (#3476)
 commit | commitdiff | tree
2019-11-14 Alex OzdemirUse Shebang in cxxtestgen when appropriate (#3458)
 commit | commitdiff | tree
2019-07-02 Alex OzdemirOptimize DRAT optimization: clause matching (#3074)
 commit | commitdiff | tree
2019-06-05 Alex OzdemirDRAT-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 OzdemirSatClauseSetHashFunction (#2916)
 commit | commitdiff | tree
2019-03-16 Alex OzdemirEnable CryptoMiniSat-backed BV proofs (#2847)
 commit | commitdiff | tree
2019-03-01 Alex OzdemirErProof class with LFSC output (#2812)
 commit | commitdiff | tree
2019-01-24 Alex OzdemirExtended DRAT signature to operational DRAT (#2815)
 commit | commitdiff | tree
2019-01-18 Alex OzdemirExtract DIMACS Printing (#2800)
 commit | commitdiff | tree
2019-01-16 Alex OzdemirBugfix: LFSC clause equality (#2801)
 commit | commitdiff | tree
2019-01-16 Alex OzdemirExtended Resolution Signature (#2788)
 commit | commitdiff | tree
2019-01-14 Alex OzdemirClausalBitvectorProof (#2786)
 commit | commitdiff | tree
2019-01-13 Alex OzdemirLFSC LRAT Output (#2787)
 commit | commitdiff | tree
2019-01-12 Alex OzdemirLratInstruction inheritance (#2784)
 commit | commitdiff | tree
2019-01-11 Alex OzdemirFixed 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 OzdemirClause proof printing (#2779)
 commit | commitdiff | tree
2019-01-09 Alex OzdemirLFSC 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 OzdemirDRAT 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 OzdemirLRAT signature (#2731)
 commit | commitdiff | tree
2018-12-07 Alex OzdemirArith Constraint Proof Loggin (#2732)
 commit | commitdiff | tree
2018-12-07 Alex OzdemirEnable BV proofs when using an eager bitblaster (#2733)
 commit | commitdiff | tree
2018-12-03 Alex OzdemirBit vector proof superclass (#2599)
 commit | commitdiff | tree
2018-11-27 Alex OzdemirLRA proof signature fixes and a first proof for linear...
commit | commitdiff | tree
2018-11-20 Alex OzdemirChange lemma proof step storage & iterators (#2712)
 commit | commitdiff | tree
2018-10-02 Alex OzdemirFix documentation for `make regress`. (#2557)
 commit | commitdiff | tree