projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Use Env class in nonlinear extension (#7039)
[cvc5.git] / src / theory / arith / nl / nonlinear_extension.cpp
2021-08-20 Gereon KremerUse Env class in nonlinear extension (#7039) blob | commitdiff | raw
2021-08-19 Gereon KremerStart using Options via Env in arithmetic (#7032) blob | commitdiff | raw | diff to current
2021-08-16 Gereon KremerUse InferenceManager in ExtTheory (#7006) blob | commitdiff | raw | diff to current
2021-06-26 yoni206pow2 -- final changes (#6800) blob | commitdiff | raw | diff to current
2021-06-02 Gereon KremerFix issues when poly is disabled (#6668) blob | commitdiff | raw | diff to current
2021-05-17 Gereon KremerImprove integration of CAD with nl-Ext (#6542) blob | commitdiff | raw | diff to current
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... blob | commitdiff | raw | diff to current
2021-04-12 Aina NiemetzRefactor and update copyright headers. (#6316) blob | commitdiff | raw | diff to current
2021-04-09 Andrew ReynoldsAdd identifiers for extended function reductions (... blob | commitdiff | raw | diff to current
2021-04-08 Andrew ReynoldsAdd identifiers for sources of incompleteness (#6311) blob | commitdiff | raw | diff to current
2021-04-01 Aina NiemetzRename namespace CVC5 to cvc5. (#6258) blob | commitdiff | raw | diff to current
2021-04-01 Andrew ReynoldsFix non-linear for unknown case (#6252) blob | commitdiff | raw | diff to current
2021-03-31 Aina NiemetzRename namespace CVC4 to CVC5. (#6249) blob | commitdiff | raw | diff to current
2021-03-25 Gereon KremerEnsure nonlinear extensions properly reconsiders its... blob | commitdiff | raw | diff to current
2021-03-15 Andrew ReynoldsMake nonlinear extension account for relevant term... blob | commitdiff | raw | diff to current
2021-03-11 Gereon KremerMake linear arithmetic use its inference manager (... blob | commitdiff | raw | diff to current
2021-03-09 Gereon KremerSome more cleanup of includes (#6083) blob | commitdiff | raw | diff to current
2021-03-09 Aina NiemetzUpdate copyright headers to 2021. (#6081) blob | commitdiff | raw | diff to current
2021-03-02 Gereon KremerClean up includes to reduce compile times (#6031) blob | commitdiff | raw | diff to current
2021-02-24 Gereon Kremer(proof-new) Add proofs for CAD solver (#5981) blob | commitdiff | raw | diff to current
2021-02-19 Gereon KremerCleanup of inferences in arithmetic theory (#5927) blob | commitdiff | raw | diff to current
2021-02-15 Gereon KremerRemove now obsolete sendLemmas and inferences stat... blob | commitdiff | raw | diff to current
2021-02-11 Gereon KremerAdd InferenceId member to TheoryInference, adapt all... blob | commitdiff | raw | diff to current
2021-02-11 Gereon KremerMerge InferenceIds into one enum (#5892) blob | commitdiff | raw | diff to current
2021-02-08 Andrew ReynoldsAvoid spurious traversal of terms during preregistratio... blob | commitdiff | raw | diff to current
2021-02-02 Andrew ReynoldsImprovements for NL traces (#5846) blob | commitdiff | raw | diff to current
2020-12-21 Gereon Kremer(proof-new) Make nl-ext factoring lemmas proof producin... blob | commitdiff | raw | diff to current
2020-12-18 Gereon Kremer(proof-new) Setup proof infrastructure for transcendent... blob | commitdiff | raw | diff to current
2020-12-18 Gereon KremerAdd proof for split zero check. (#5699) blob | commitdiff | raw | diff to current
2020-12-17 Gereon Kremer(proof-new) Prepare nonlinear extension and nl-ext... blob | commitdiff | raw | diff to current
2020-12-10 Gereon KremerFixed a bunch of clang warnings. (#5637) blob | commitdiff | raw | diff to current
2020-12-07 Gereon KremerRefactor initial phase of transcendental solver (#5599) blob | commitdiff | raw | diff to current
2020-11-16 Gereon KremerImprove accuracy of resource limitation (#4763) blob | commitdiff | raw | diff to current
2020-11-05 mudathirmahgoubRemove mkSingleton from the API (#5366) blob | commitdiff | raw | diff to current
2020-11-03 Andrew ReynoldsReset built model flag at presolve in nonlinear (#5386) blob | commitdiff | raw | diff to current
2020-10-30 Gereon KremerUse BoundInference in nonlinear extension (#5359) blob | commitdiff | raw | diff to current
2020-10-28 Andrew ReynoldsFixes for unconstrained variables in nonlinear model... blob | commitdiff | raw | diff to current
2020-10-28 Gereon KremerSplit NlSolver in multiple subsolvers (#5315) blob | commitdiff | raw | diff to current
2020-09-30 Gereon KremerAdd strategy for nonlinear extension (#5160) blob | commitdiff | raw | diff to current
2020-09-29 Gereon KremerClean up nonlinear extension (#5149) blob | commitdiff | raw | diff to current
2020-09-26 Gereon KremerUse inference manager for nl_solver (#5125) blob | commitdiff | raw | diff to current
2020-09-23 Gereon KremerMake IAND solver use inference manager. (#5126) blob | commitdiff | raw | diff to current
2020-09-22 Mathias PreinerUpdate copyright header script to support CMake and... blob | commitdiff | raw | diff to current
2020-09-22 Gereon KremerICP-based solver for nonlinear arithmetic (#5017) blob | commitdiff | raw | diff to current
2020-09-17 Gereon KremerUse new inference manager in transcendental solver... blob | commitdiff | raw | diff to current
2020-09-04 Gereon KremerUse arith::InferenceManager for CAD lemmas (#5015) blob | commitdiff | raw | diff to current
2020-09-03 Gereon KremerBasic integration of arith::InferenceManager (#4999) blob | commitdiff | raw | diff to current
2020-09-03 Gereon KremerMake nonlinear extension (more) deterministic (#4996) blob | commitdiff | raw | diff to current
2020-09-03 Andrew ReynoldsMake ExtTheory independent of Theory (#5010) blob | commitdiff | raw | diff to current
2020-09-02 Gereon KremerAdd ArithLemma and arith::InferenceManager (#4960) blob | commitdiff | raw | diff to current
2020-08-24 Andrew ReynoldsDo not use relevance during non-linear check model... blob | commitdiff | raw | diff to current
2020-08-21 Andrew ReynoldsConnect the relevance manager to TheoryEngine and use... blob | commitdiff | raw | diff to current
2020-08-04 Gereon KremerAdd CAD-based solver (#4834) blob | commitdiff | raw | diff to current
2020-07-28 Andrew ReynoldsUse lemma property enum for OutputChannel::lemma (... blob | commitdiff | raw | diff to current
2020-07-21 Gereon KremerPreparations for a CAD-based arithmetic solver (#4762) blob | commitdiff | raw | diff to current
2020-07-16 Andrew ReynoldsMake ExtTheory a utility and not a member of Theory... blob | commitdiff | raw | diff to current
2020-07-09 Andrew ReynoldsAssociate all lemmas in non-linear arithmetic with... blob | commitdiff | raw | diff to current
2020-07-01 Andrew ReynoldsAdd solver for integer AND (#4681) blob | commitdiff | raw | diff to current
2020-06-25 Andrew ReynoldsUpdate option --nl-ext to enable/disable incremental... blob | commitdiff | raw | diff to current
2020-06-16 Aina NiemetzUpdate copyright headers. blob | commitdiff | raw | diff to current
2020-06-06 Andrew ReynoldsUse NlLemma utility for all lemmas in non-linear. ... blob | commitdiff | raw | diff to current
2020-06-01 Andrew ReynoldsMove non-linear files to src/theory/arith/nl (#4548) blob | commitdiff | raw | diff to current