projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Refactor and update copyright headers. (#6316)
[cvc5.git] / src / theory / arith /
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) tree | commitdiff
2021-04-10 Aina NiemetzRename CVC4_ macros to CVC5_. (#6327) tree | commitdiff
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326) tree | commitdiff
2021-04-09 Andrew ReynoldsAdd identifiers for extended function reductions (... tree | commitdiff
2021-04-08 Andrew ReynoldsAdd identifiers for sources of incompleteness (#6311) tree | commitdiff
2021-04-07 Andrew ReynoldsReplace calls to NodeManager::mkSkolem with SkolemManag... tree | commitdiff
2021-04-06 Andres NoetzliRemove template argument from `NodeBuilder` (#6290) tree | commitdiff
2021-04-05 Haniel Barbosa[proof-new] Registering proof checkers uniformly from... tree | commitdiff
2021-04-05 Andrew ReynoldsAdd interface for skolem functions in SkolemManager... tree | commitdiff
2021-04-01 Andrew ReynoldsFix type rule for to_real (#6257) tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-04-01 Andrew ReynoldsFix non-linear for unknown case (#6252) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-31 Andrew ReynoldsAdd missing inference ids (#6242) tree | commitdiff
2021-03-25 Gereon KremerEnsure nonlinear extensions properly reconsiders its... tree | commitdiff
2021-03-25 Gereon KremerAdd missing includes. (#6207) tree | commitdiff
2021-03-24 Gereon KremerOnly consider relevant terms for integer branches ... tree | commitdiff
2021-03-23 Andrew ReynoldsRemove unused code for axioms (#6197) tree | commitdiff
2021-03-21 Andrew ReynoldsClean up remaining raw uses of output channel (#6161) tree | commitdiff
2021-03-16 Haniel Barbosa[proof-new] Renaming proof option to be in sync with... tree | commitdiff
2021-03-15 Gereon KremerReplace HistogramStat by IntegralHistogramStat (#6126) tree | commitdiff
2021-03-15 Andrew ReynoldsMake nonlinear extension account for relevant term... tree | commitdiff
2021-03-11 Gereon KremerMake linear arithmetic use its inference manager (... tree | commitdiff
2021-03-11 Alex Ozdemirarith proof rules shuffle & add ARITH_SUM_UB (#6118) tree | commitdiff
2021-03-11 Gereon KremerFirst refactoring of statistics classes (#6105) tree | commitdiff
2021-03-11 Andrew Reynolds(proof-new) Clean up uses of witness with skolem lemmas... tree | commitdiff
2021-03-11 Mathias PreinerFix compile warnings when compiling with GLPK. (#6115) tree | commitdiff
2021-03-11 Mathias PreinerUse CVC4_ASSERTIONS instead of NDEBUG. (#6099) tree | commitdiff
2021-03-10 Gereon KremerImprove arithmetic proofs (#6106) tree | commitdiff
2021-03-10 Andrew Reynolds(proof-new) Update ppRewrite to use skolem lemmas ... tree | commitdiff
2021-03-10 Andrew ReynoldsFix term registration and non-theory-preprocessed terms... tree | commitdiff
2021-03-09 Andrew ReynoldsRemove logic request (#6089) tree | commitdiff
2021-03-09 Gereon KremerAdd missing include if GLPK is enabled. (#6084) tree | commitdiff
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) tree | commitdiff
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) tree | commitdiff
2021-03-08 Andrew Reynolds(proof-new) Prepare arithmetic for changes to ppRewrite... tree | commitdiff
2021-03-04 Gereon KremerAdd proper define for libpoly usage (#6050) tree | commitdiff
2021-03-03 Andrew Reynolds(proof-new) Simplifications to arithmetic operator... tree | commitdiff
2021-03-03 Gereon KremerMore cleanup of includes to reduce compilation times... tree | commitdiff
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) tree | commitdiff
2021-02-25 Mathias PreinerEnable -Werror. (#5969) tree | commitdiff
2021-02-24 Gereon Kremer(proof-new) Add proofs for CAD solver (#5981) tree | commitdiff
2021-02-23 Gereon KremerAdd proof for mult sign lemma (#5966) tree | commitdiff
2021-02-23 Gereon KremerAdd proof for monomial bounds check (#5965) tree | commitdiff
2021-02-23 Gereon Kremer(proof-new) Add proof generator for CAD solver (#5964) tree | commitdiff
2021-02-23 Gereon KremerAdd trans secant proofs. (#5957) tree | commitdiff
2021-02-22 Andrew Reynolds(proof-new) Change proof-new option to proof (#5955) tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add proofs for exponential functions (... tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDIC... tree | commitdiff
2021-02-22 Gereon Kremer(proof-new) Add proofs for sine lemmas in the transcend... tree | commitdiff
2021-02-22 Gereon KremerCleanup in transcendental solver, add ApproximationBoun... tree | commitdiff
2021-02-22 Gereon Kremeradd pruneRedundantIntervals (#5950) tree | commitdiff
2021-02-19 Andrew ReynoldsRefactoring theory inference process (#5920) tree | commitdiff
2021-02-19 Gereon KremerCleanup of inferences in arithmetic theory (#5927) tree | commitdiff
2021-02-18 Gereon KremerAdd statistic for InferenceId to TheoryInferenceManager... tree | commitdiff
2021-02-15 Gereon KremerRemove now obsolete sendLemmas and inferences stat... tree | commitdiff
2021-02-11 Gereon KremerMake most methods of TheoryInferenceManager expect... tree | commitdiff
2021-02-11 Gereon KremerAdd InferenceId member to TheoryInference, adapt all... tree | commitdiff
2021-02-11 Gereon KremerMerge InferenceIds into one enum (#5892) tree | commitdiff
2021-02-10 Andrew ReynoldsFix open proof for factoring lemma (#5885) tree | commitdiff
2021-02-08 Andrew ReynoldsAvoid spurious traversal of terms during preregistratio... tree | commitdiff
2021-02-02 Andrew ReynoldsImprovements for NL traces (#5846) tree | commitdiff
2021-02-01 Andrew ReynoldsEliminate PREPROCESS lemma property (#5827) tree | commitdiff
2021-01-27 Alex OzdemirThread proofs through arith channels & similar (#5818) tree | commitdiff
2021-01-26 Alex OzdemirAdd proofs to TheoryArithPrivate::propagate (#5812) tree | commitdiff
2021-01-21 Alex Ozdemirarith: Proofs for Diophantine cuts (#5792) tree | commitdiff
2021-01-19 Alex OzdemirImplement proofs for arith BRAB lemmas (#5784) tree | commitdiff
2021-01-14 Andrew ReynoldsUpdates to theory preprocess equality (#5776) tree | commitdiff
2021-01-07 Gereon KremerMake sure polynomials are properly factorized in nl... tree | commitdiff
2020-12-23 Gereon KremerAdd proofs for nonlinear sign lemmas. (#5707) tree | commitdiff
2020-12-22 Andrew ReynoldsMake theory preprocess rewrite equalities a preprocessi... tree | commitdiff
2020-12-21 Gereon KremerAdd proof for pi bound lemma (#5709) tree | commitdiff
2020-12-21 Gereon KremerAdd proof for sine shift lemmas. (#5710) tree | commitdiff
2020-12-21 Gereon Kremer(proof-new) Make nl-ext factoring lemmas proof producin... tree | commitdiff
2020-12-18 Gereon Kremer(proof-new) Setup proof infrastructure for transcendent... tree | commitdiff
2020-12-18 Gereon KremerAdd proof checker for nl tangent lemma (#5704) tree | commitdiff
2020-12-18 Alex OzdemirBugfix: proofs for props of non-normal arith lits ... tree | commitdiff
2020-12-18 Gereon Kremer(proof-new) Add proof for tangent plane lemmas (#5700) tree | commitdiff
2020-12-18 Gereon KremerAdd proof for split zero check. (#5699) tree | commitdiff
2020-12-17 Gereon KremerAlways consider rewritten lemmas for caching. (#5696) tree | commitdiff
2020-12-17 Gereon Kremer(proof-new) Prepare nonlinear extension and nl-ext... tree | commitdiff
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) tree | commitdiff
2020-12-09 Gereon KremerSplit initial exp lemma into separate lemmas. (#5622) tree | commitdiff
2020-12-07 makaimannAdd bitwise refinement mode for IAND (#5328) tree | commitdiff
2020-12-07 Gereon KremerRefactor initial phase of transcendental solver (#5599) tree | commitdiff
2020-12-07 Andrew ReynoldsDo not expand theory definitions at the beginning of... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-12-02 Aina NiemetzRename macro Message to CVC4Message. (#5576) tree | commitdiff
2020-12-01 Gereon KremerRefactor transcendental solver (#5539) tree | commitdiff
2020-11-30 Andrew ReynoldsRemove includes for old API from internal code (#5536) tree | commitdiff
2020-11-26 Gereon KremerMake CAD solver work for empty set of assertions (... tree | commitdiff
2020-11-25 Gereon KremerFix transcendental secant plane lemmas (#5525) tree | commitdiff
2020-11-25 Gereon KremerRefactor transcendental solver (#5514) tree | commitdiff
2020-11-20 Aina NiemetzFix #5493. (#5495) tree | commitdiff
2020-11-20 Aina NiemetzFix compiler warnings. (#5493) tree | commitdiff
2020-11-20 Gereon KremerAllow to pass ProofGenerator to arithmetic inference... tree | commitdiff
2020-11-19 Aina NiemetzInclude stddef.h (needed for size_t) in cvc4_public... tree | commitdiff
2020-11-19 Andrew ReynoldsFix issues related to eliminating extended arithmetic... tree | commitdiff
2020-11-18 Andrew ReynoldsDo not expand definitions of extended arithmetic operat... tree | commitdiff
2020-11-17 Gereon KremerFix tangent plane lemmas (#5455) tree | commitdiff
next