projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Fix getModelValue for arithmetic (#8316)
[cvc5.git] / src / theory / arith / nl / ext /
2022-02-03 Aina NiemetzRename kind PLUS -> ADD. (#8036) tree | commitdiff
2022-02-02 Aina NiemetzRename kinds MINUS -> SUB and UMINUS -> NEG. (#8035) tree | commitdiff
2021-12-22 Andrew ReynoldsRemove most uses of mkRationalNode (#7854) tree | commitdiff
2021-12-13 Andrew ReynoldsDistinguishing more uses of CONST_RATIONAL (#7802) tree | commitdiff
2021-12-08 Gereon KremerRemove rewrites from iand and pow2 solvers (#7775) tree | commitdiff
2021-11-17 Andrew ReynoldsPreparations for eliminating arithmetic subtyping ... tree | commitdiff
2021-11-12 Andres NoetzliRemove `ConstantMap<Rational>` (#7635) tree | commitdiff
2021-11-05 Andrew ReynoldsRemove many static calls to rewrite (#7580) tree | commitdiff
2021-10-29 Gereon KremerFix proof of nl lemma for a corner case (#7530) tree | commitdiff
2021-10-05 Gereon KremerFirst round of refactoring on NlModel (#7255) tree | commitdiff
2021-08-19 Gereon KremerStart using Options via Env in arithmetic (#7032) tree | commitdiff
2021-05-26 Andres Noetzli More precise includes of `Node` constants (#6617) tree | commitdiff
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611) tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-04-14 Aina NiemetzRename public and private headers in src/include. ... tree | commitdiff
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) tree | commitdiff
2021-04-09 Aina NiemetzRename CVC4__ header guards to CVC5__. (#6326) tree | commitdiff
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) tree | commitdiff
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) tree | commitdiff
2021-03-11 Alex Ozdemirarith proof rules shuffle & add ARITH_SUM_UB (#6118) tree | commitdiff
2021-03-10 Gereon KremerImprove arithmetic proofs (#6106) 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-02 Gereon KremerClean up includes to reduce compile times (#6031) 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-19 Gereon KremerCleanup of inferences in arithmetic theory (#5927) 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
2020-12-23 Gereon KremerAdd proofs for nonlinear sign lemmas. (#5707) tree | commitdiff
2020-12-21 Gereon Kremer(proof-new) Make nl-ext factoring lemmas proof producin... tree | commitdiff
2020-12-18 Gereon KremerAdd proof checker for nl tangent lemma (#5704) 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 Kremer(proof-new) Prepare nonlinear extension and nl-ext... tree | commitdiff
2020-12-03 Aina NiemetzUpdate copyright headers. tree | commitdiff
2020-11-20 Gereon KremerAllow to pass ProofGenerator to arithmetic inference... tree | commitdiff
2020-11-17 Gereon KremerFix tangent plane lemmas (#5455) tree | commitdiff
2020-11-16 Gereon KremerRefactor tangent plane lemmas (#5449) tree | commitdiff
2020-10-28 Gereon KremerSplit NlSolver in multiple subsolvers (#5315) tree | commitdiff