| 2022-02-02 |
Alex Ozdemir | Change name of Python API's package from pycvc5 to...
|
commit | commitdiff | tree |
| 2022-01-14 |
Alex Ozdemir | Rename python APIs (#7950)
|
commit | commitdiff | tree |
| 2022-01-11 |
Alex Ozdemir | Add new idiomatic examples (#7912)
|
commit | commitdiff | tree |
| 2022-01-07 |
Alex Ozdemir | Python Idomatic API: Document solver, results, utilities...
|
commit | commitdiff | tree |
| 2022-01-07 |
Alex Ozdemir | Document quantifiers in idiomatic python API (#7880)
|
commit | commitdiff | tree |
| 2022-01-05 |
Alex Ozdemir | Py idiomatic API: Doc sets, datatypes, FP (#7877)
|
commit | commitdiff | tree |
| 2022-01-05 |
Alex Ozdemir | Don't use python's collections.Set (#7875)
|
commit | commitdiff | tree |
| 2021-12-17 |
Alex Ozdemir | More documentation for idiomatic python API (#7798)
|
commit | commitdiff | tree |
| 2021-11-30 |
Alex Ozdemir | Scaffold the idiomatic API's documentation (#7715)
|
commit | commitdiff | tree |
| 2021-11-17 |
Alex Ozdemir | Update Python packaging infrastructure (#7654)
|
commit | commitdiff | tree |
| 2021-11-17 |
Alex Ozdemir | Remove documentation for --lib-only (#7648)
|
commit | commitdiff | tree |
| 2021-10-15 |
Alex Ozdemir | Fix bad cast in the python API (#7359)
|
commit | commitdiff | tree |
| 2021-09-20 |
Alex Ozdemir | Start python API Solver documentation (#7064)
|
commit | commitdiff | tree |
| 2021-08-05 |
Alex Ozdemir | Normalize val in BitVector(val_str, base) (#6955)
|
commit | commitdiff | tree |
| 2021-08-04 |
Alex Ozdemir | Add IEEE-BV-to-FP to external-to-internal mapping in...
|
commit | commitdiff | tree |
| 2021-06-08 |
Alex Ozdemir | Change output of getRealValue to a fraction. (#6692)
|
commit | commitdiff | tree |
| 2021-05-20 |
Alex Ozdemir | Expand arith's farkas lemma rule as a macro (#6577)
|
commit | commitdiff | tree |
| 2021-05-14 |
Alex Ozdemir | Add getId function to python API (#6523)
|
commit | commitdiff | tree |
| 2021-05-13 |
Alex Ozdemir | Fix error message in toPythonObj (#6524)
|
commit | commitdiff | tree |
| 2021-03-11 |
Alex Ozdemir | arith proof rules shuffle & add ARITH_SUM_UB (#6118)
|
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / search