summaryrefslogtreecommitdiff
path: root/src/theory/arith/theory_arith_private.h
AgeCommit message (Expand)Author
2021-05-13Add std::hash overloads for Node, TNode and TypeNode. (#6534)Mathias Preiner
2021-04-14Refactor / reimplement statistics (#6162)Gereon Kremer
2021-04-12Refactor and update copyright headers. (#6316)Aina Niemetz
2021-04-07Replace calls to NodeManager::mkSkolem with SkolemManager::mkDummySkolem (#6291)Andrew Reynolds
2021-04-06Remove template argument from `NodeBuilder` (#6290)Andres Noetzli
2021-04-05[proof-new] Registering proof checkers uniformly from the SMT solver (#6275)Haniel Barbosa
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-24Only consider relevant terms for integer branches (#6181)Gereon Kremer
2021-03-23Remove unused code for axioms (#6197)Andrew Reynolds
2021-03-15Replace HistogramStat by IntegralHistogramStat (#6126)Gereon Kremer
2021-03-11Make linear arithmetic use its inference manager (#5934)Gereon Kremer
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
2021-01-26Thread proofs through arith channels & similar (#5818)Alex Ozdemir
2021-01-20arith: Proofs for Diophantine cuts (#5792)Alex Ozdemir
2021-01-19Implement proofs for arith BRAB lemmas (#5784)Alex Ozdemir
2020-11-19Include stddef.h (needed for size_t) in cvc4_public.h (#5476)Aina Niemetz
2020-10-14(proof-new) pfs in TheoryArith(Private) explainations (#5258)Alex Ozdemir
2020-10-14(proof-new) pfs for conflicts in TheoryArithPrivate (#5257)Alex Ozdemir
2020-10-13(proof-new) Prove lemmas in Constraint (#5254)Alex Ozdemir
2020-10-07(proof-new) proofs in ee -> arith pipeline (#5215)Alex Ozdemir
2020-10-06(proof-new) Add interface for trusted substitution and update ppAssert (#5193)Andrew Reynolds
2020-10-02Decouple modules from TheoryArithPrivate (#5184)Andrew Reynolds
2020-10-01Update theory of arithmetic to standard check (#5178)Andrew Reynolds
2020-09-29(proof-new) Add proof managers and eager gens to arith (#5159)Alex Ozdemir
2020-09-22Update copyright header script to support CMake and Python files (#5067)Mathias Preiner
2020-09-16Refactor collectModelInfo in TheoryArith (#5027)Andrew Reynolds
2020-09-02Make ExtTheory independent of Theory (#5010)Andrew Reynolds
2020-08-20Add TheoryState objects to each Theory (#4920)Andrew Reynolds
2020-08-17Dynamic allocation of equality engine in Theory (#4890)Andrew Reynolds
2020-07-27(proof-new) Arithmetic operator elim proof producing (#4783)Andrew Reynolds
2020-06-19(proof-new) Split operator elimination from arithmetic (#4581)Andrew Reynolds
2020-06-16Update copyright headers.Aina Niemetz
2020-06-01Move non-linear files to src/theory/arith/nl (#4548)Andrew Reynolds
2020-05-22Refactor operator elimination in arithmetic (#4519)Andrew Reynolds
2020-04-08Perform theory widening eagerly (#4044)Andres Noetzli
2020-04-03Update theory rewriter ownership, add stats to strings (#4202)Andres Noetzli
2020-02-04Articulate proof-related debug statements in arith (#3700)Alex Ozdemir
2019-11-18Fix reduction of `sqrt` (#3478)Andres Noetzli
2019-03-26Update copyright headers.Aina Niemetz
2018-09-13 Decision strategy: incorporate CEGQI (#2460)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-02-27Option to not use partial function semantics for arithmetic div by zero (#1620)Andrew Reynolds
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2018-01-23Commenting out throw specifiers for DeltaRationExceptions. These functions ca...Tim King
2018-01-09Cleaning up throw specifiers on Exception and subclasses. (#1475)Tim King
2018-01-07Removes RationalFromDoubleException. Replaces this with an explicit M… (#1476)Tim King
2017-12-08Make collect model info return a Bool (#1421)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback