projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Fix getModelValue for arithmetic (#8316)
[cvc5.git] / src / theory / arith /
2022-03-16 Andrew ReynoldsFix getModelValue for arithmetic (#8316) tree | commitdiff
2022-03-15 Andrew ReynoldsFix issues involving multiple sources of model substitu... tree | commitdiff
2022-03-11 Andrew ReynoldsFix reduction for arc trig functions (#8289) tree | commitdiff
2022-03-09 Gereon KremerClear obsolete pending lemmas in arithmetic (#8236) tree | commitdiff
2022-03-04 Gereon KremerRemove spurious assertion in linear solver (#8231) tree | commitdiff
2022-03-04 Gereon KremerGuard recursion into terms during substitution in arith... tree | commitdiff
2022-03-03 Andrew ReynoldsThrow logic exception if a transcendental function... tree | commitdiff
2022-03-03 Gereon KremerFix rewriting of mixed-integer atoms (#8214) tree | commitdiff
2022-03-02 Andrew ReynoldsFix issue with dropping non-reduced sine terms (#8211) tree | commitdiff
2022-03-02 Gereon KremerMove libpoly <-> CoCoA conversion to new utility (... tree | commitdiff
2022-03-02 Gereon KremerRefactor rewriting of arithmetic division (#8195) tree | commitdiff
2022-03-02 Gereon KremerPrune spurious roots in lazard evaluation of coverings... tree | commitdiff
2022-03-01 Andrew ReynoldsFix issue involving dropped purification lemmas for... tree | commitdiff
2022-03-01 Gereon KremerRename cad to coverings (#8187) tree | commitdiff
2022-02-28 Gereon KremerRefactor rewriting of arithmetic atoms (#8175) tree | commitdiff
2022-02-28 Andrew ReynoldsFix special casing for PI in model value (#8189) tree | commitdiff
2022-02-28 Andrew ReynoldsPreserve model values for exact sine points (#8188) tree | commitdiff
2022-02-28 Andrew ReynoldsAdd two reduction schemas for sin terms (#8171) tree | commitdiff
2022-02-28 Gereon KremerRefactor rewriting of arithmetic leafs (#8177) tree | commitdiff
2022-02-28 Gereon KremerRefactor rewriting of arithmetic addition (#8180) tree | commitdiff
2022-02-25 Gereon KremerAdd utilities to rewrite atoms for the arithmetic rewri... tree | commitdiff
2022-02-25 Gereon KremerRefactor rewriting of arithmetic negation and subtracti... tree | commitdiff
2022-02-25 Gereon KremerSlightly refactor arithmetic rewriting for extended... tree | commitdiff
2022-02-25 Andrew ReynoldsSimplify and fix how purified terms are managed in... tree | commitdiff
2022-02-25 Andrew ReynoldsFix dropped bounds on PI (#8164) tree | commitdiff
2022-02-25 Andrew ReynoldsRemove approximations infrastructure from model (#8166) tree | commitdiff
2022-02-24 Andrew ReynoldsEnsure variables are constrained in model when equal... tree | commitdiff
2022-02-24 Andrew ReynoldsMake sine solver sound with respect to region boundarie... tree | commitdiff
2022-02-24 Gereon KremerGet rid of some static objects in arithmetic theory... tree | commitdiff
2022-02-24 Andrew ReynoldsMake uninterpreted sort owner non-static (#8144) tree | commitdiff
2022-02-23 Gereon KremerFix icp candidate parsing (#8137) tree | commitdiff
2022-02-23 Gereon KremerFix pruning of covering intervals in proofs (#8084) tree | commitdiff
2022-02-23 Gereon KremerRefactor multiplication in arithmetic rewriter (#7965) tree | commitdiff
2022-02-22 Andrew ReynoldsChange inference scheme in transcendentals to rewrite... tree | commitdiff
2022-02-22 Andrew ReynoldsRelax what is generated in the model from NL (#8113) tree | commitdiff
2022-02-17 Andrew ReynoldsIntroduce skolem function to make transcendental functi... tree | commitdiff
2022-02-17 Andrew ReynoldsMissing ids for arith conflicts (#8108) tree | commitdiff
2022-02-08 Gereon KremerAdd addition utilities for the arithmetic rewriter... tree | commitdiff
2022-02-08 Andrew ReynoldsSimplify formalism of introduced arithmetic skolems... tree | commitdiff
2022-02-07 Andrew ReynoldsFix unsoundness in IAND solver (#8053) tree | commitdiff
2022-02-07 Gereon KremerImprove combination of NRA and transcendentals (#8075) tree | commitdiff
2022-02-05 Andrew ReynoldsFix another rewrite involving iand (#8054) tree | commitdiff
2022-02-03 Gereon KremerImprove theory combination over real algebraic models... tree | commitdiff
2022-02-03 Gereon KremerAdd node utils for the arithmetic rewriter (#8012) tree | commitdiff
2022-02-03 Aina NiemetzRename kind PLUS -> ADD. (#8036) tree | commitdiff
2022-02-02 Andrew ReynoldsFix rewrite for eliminating constant factors of PI... tree | commitdiff
2022-02-02 Aina NiemetzRename kinds MINUS -> SUB and UMINUS -> NEG. (#8035) tree | commitdiff
2022-02-02 Andrew ReynoldsFix invalid rewrite involving iand (#8026) tree | commitdiff
2022-02-02 Gereon KremerAdd additional check to avoid cyclic substitution ... tree | commitdiff
2022-02-01 Gereon KremerAdd new ordering utility (#8008) tree | commitdiff
2022-02-01 Gereon KremerConsider RANs in variable ordering (#7964) tree | commitdiff
2022-01-31 Gereon KremerAdd utilities for flattening nodes (#7961) tree | commitdiff
2022-01-24 Gereon KremerUse proper RAN nodes for nl model (#7939) tree | commitdiff
2022-01-24 Gereon KremerRefactor how arith rewriting checks for mult-by-zero... tree | commitdiff
2022-01-20 Gereon KremerRefactor abs rewriting (#7935) tree | commitdiff
2022-01-19 Gereon KremerFix a subtle issue with double negations in coverings... tree | commitdiff
2022-01-19 Gereon KremerMake tracing for arithmetic rewriter more consistent... tree | commitdiff
2022-01-14 Gereon Kremerrefactor div rewriter, add support for ran (#7941) tree | commitdiff
2022-01-14 Gereon KremerRefactor arithmetic pre-rewriter for multiplication... tree | commitdiff
2022-01-14 Gereon KremerAdd support for RANs in rewriter for `MULT` (#7940) tree | commitdiff
2022-01-14 Gereon KremerAdd RAN support in UMINUS rewriter (#7933) tree | commitdiff
2022-01-13 Gereon KremerAdd arithmetic rewriter for RAN (#7929) tree | commitdiff
2022-01-13 Gereon KremerRefactor post rewriter for addition (#7931) tree | commitdiff
2022-01-12 Gereon KremerRefactor atom rewriting to be RAN-aware (#7928) tree | commitdiff
2022-01-12 Gereon KremerRefactor rewriteMinus (#7932) tree | commitdiff
2022-01-12 Gereon KremerAdd mkRealAlgebraicNumber (#7923) tree | commitdiff
2022-01-12 Andrew ReynoldsAlways use partial function for sqrt (#7926) tree | commitdiff
2022-01-11 Gereon KremerAdds a kind to hold RealAlgebraicNumber constants ... tree | commitdiff
2022-01-06 Gereon KremerImprove theory combination in the presence of real... tree | commitdiff
2022-01-04 Andrew ReynoldsRemove unused shutdown infrastructure (#7872) tree | commitdiff
2021-12-22 Andrew ReynoldsRemove most uses of mkRationalNode (#7854) tree | commitdiff
2021-12-21 Andrew ReynoldsEliminate remaining calls to callExtendedRewrite (... tree | commitdiff
2021-12-21 yoni206Rewrite (pow2 x) to (pow 2 x) when x is a constant... tree | commitdiff
2021-12-20 Andrew ReynoldsEliminating some uses of const rational in arithmetic... tree | commitdiff
2021-12-17 Andrew ReynoldsEliminate more uses of CONST_RATIONAL (#7816) tree | commitdiff
2021-12-16 Andres NoetzliExplicitly disallow `mkConst(Rational)` (#7818) tree | commitdiff
2021-12-14 Gereon KremerFix issues with tracing builds (#7809) tree | commitdiff
2021-12-14 Andrew ReynoldsEliminate use of rewrite, CONST_RATIONAL in ArithMSum... tree | commitdiff
2021-12-13 Andrew ReynoldsDistinguishing more uses of CONST_RATIONAL (#7802) tree | commitdiff
2021-12-13 Andrew ReynoldsInitial cut at distinguishing uses of CONST_RATIONAL... tree | commitdiff
2021-12-13 Andrew ReynoldsFixes and additions for API for parametric datatypes... tree | commitdiff
2021-12-13 Gereon KremerImprove nonlinear solver (#7787) tree | commitdiff
2021-12-13 yoni206Integrate new int-blaster (#7781) tree | commitdiff
2021-12-10 Ying ShengArray-inspired Sequence Solver - Adding the ArrayCoreSo... tree | commitdiff
2021-12-10 Gereon KremerEliminate more static rewrites (#7786) tree | commitdiff
2021-12-09 Gereon KremerFix sine symmetry proof (#7783) tree | commitdiff
2021-12-08 Gereon KremerRemove rewrites from iand and pow2 solvers (#7775) tree | commitdiff
2021-12-08 Gereon KremerEliminate rewriter from transcendental solver (#7772) tree | commitdiff
2021-11-30 Andrew ReynoldsAdd rewrite for is_int pi (#7711) tree | commitdiff
2021-11-29 Gereon KremerFix minor issues (#7704) tree | commitdiff
2021-11-24 Andres NoetzliMinor fixes (#7691) tree | commitdiff
2021-11-18 Gereon KremerRefactor CAD option for linear model seed (#7657) tree | commitdiff
2021-11-17 Andrew ReynoldsPreparations for eliminating arithmetic subtyping ... tree | commitdiff
2021-11-17 Gereon KremerImplement aggressive pruning in CAD solver (#7650) tree | commitdiff
2021-11-12 Andres NoetzliRemove `ConstantMap<Rational>` (#7635) tree | commitdiff
2021-11-09 Gereon KremerMake secant points user context dependent (#7567) tree | commitdiff
2021-11-05 Andrew ReynoldsRemove many static calls to rewrite (#7580) tree | commitdiff
2021-11-05 Gereon KremerRemove quadratic solving in NlModel (#7542) tree | commitdiff
2021-11-05 Gereon KremerEliminate `Warning` macro in favor of `EnvObj::warning... tree | commitdiff
2021-11-05 Gereon KremerRemove a bunch of debugging/logging code from the linea... tree | commitdiff
next