Reduced direct carl calls - #1042
Open
volkm wants to merge 12 commits into
Open
Conversation
…umber/RationalFunctionCoefficient
Contributor
Author
Remaining direct
|
| File:line | Usage |
|---|---|
BigStep.cpp:33 |
using UniPoly = carl::UnivariatePolynomial<RationalFunctionCoefficient>; |
BinaryDtmcTransformer.cpp:7 |
#include <carl/formula/Constraint.h> |
BinaryDtmcTransformer.cpp:103,110,128,132 |
carl::makePolynomial<Polynomial>(…) (x4) |
2. Real-root isolation — storm-pars/transformer/RobustParameterLifter.cpp
| Line | Usage |
|---|---|
| 3 | #include <carl/core/rootfinder/RootFinder.h> |
| 251 | carl::rootfinder::realRoots<CoefficientType, CoefficientType>(…) |
| 252 | carl::Interval<CoefficientType>(…) |
| 253 | carl::rootfinder::SplittingStrategy::ABERTH |
| 255 | carl::RealAlgebraicNumber<CoefficientType> |
3. carl::Formula — storm/analysis/GraphConditions
| File:line | Usage |
|---|---|
GraphConditions.h:11 |
#include <carl/formula/Formula.h> |
GraphConditions.h:27 |
typedef carl::Formula<typename storm::RationalFunction::PolyType::PolyType> val; |
GraphConditions.cpp:51,97,130,171 |
carl::FormulaType::ITE (x4) |
4. Cache-needing-polynomial SFINAE
| File:line | Usage |
|---|---|
builder/DdJaniModelBuilder.cpp:200,206 |
carl::EnableIf<carl::needs_cache<TP>> = carl::dummy / carl::DisableIf<…> |
builder/DdPrismModelBuilder.cpp:58,64 |
same |
storage/expressions/ToRationalFunctionVisitor.h:36,41 |
same (in a header) |
5. l3pp container streaming — storm/utility/logging.h
| Line | Usage |
|---|---|
| 4 | #include <carl/io/streamingOperators.h> |
| 6 | using carl::operator<<; (in namespace l3pp) |
carl's operators are pulled in project-wide via the polynomial headers anyway, so removing this achieves no real decoupling.
6. Test code
| File:line | Usage |
|---|---|
test/storm-pars/modelchecker/region/monotonicity/MonotonicityHelperTest.cpp:8,58 |
#include <carl/util/stringparser.h>, carl::StringParser parser; |
test/storm/storage/SylvanDdTest.cpp:8,141 |
same |
test/storm-pars/transformer/BinaryDtmcTransformerTest.cpp:104,106 |
carl::makePolynomial<storm::Polynomial>(…) |
test/storm-pars/transformer/IntervalEndComponentPreserverTest.cpp:8 |
#include <carl/formula/Constraint.h> |
There was a problem hiding this comment.
🟡 Changes recommended
It introduces at least one compile-breaking include issue and a test correctness issue that should be fixed before approval.
Once you've addressed the issues Copilot identified, you can request another Copilot review.
Pull request overview
This PR reduces direct dependencies on carl by routing common operations through Storm adapters (RationalFunctionAdapter, IntervalAdapter) and storm::utility::constants, while also consolidating numeric type usage around storm::RationalNumber / storm::RationalFunctionCoefficient.
Changes:
- Introduces rational-function variable pool helpers (
createRFVariable,findRFVariable,clearRFVariablePool) and updates tests/callers to use them. - Replaces several direct
carlutilities (hash combine, parsing, pow/sqrt/abs, bound types) with Storm utility/adapters. - Adds integer
gcd/lcmwrappers and updatesvector::toIntegralVectorto operate on integer numerators/denominators.
File summaries
| File | Description |
|---|---|
| src/test/storm-pars/utility/ModelInstantiatorTest.cpp | Switches RF variable handling to Storm adapter helpers in instantiation tests. |
| src/test/storm-pars/modelchecker/SparseRobustDtmcParameterLiftingTest.cpp | Resets RF variable pool via Storm helper in test setup/teardown. |
| src/test/storm-pars/modelchecker/SparseMdpParameterLiftingTest.cpp | Resets RF variable pool via Storm helper in test setup/teardown. |
| src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingTest.cpp | Resets RF variable pool via Storm helper in test setup/teardown. |
| src/test/storm-pars/modelchecker/SparseDtmcParameterLiftingMonotonicityTest.cpp | Resets RF variable pool via Storm helper in test setup/teardown. |
| src/test/storm-pars/derivative/SparseDerivativeInstantiationModelCheckerTest.cpp | Uses Storm RF variable lookup and pool reset in derivative instantiation tests. |
| src/test/storm-pars/derivative/GradientDescentInstantiationSearcherTest.cpp | Uses Storm RF variable pool reset and Storm RF variable type in test code. |
| src/test/storm-dft/transformations/DftInstantiatorTest.cpp | Uses Storm RF variable pool reset and Storm RF variable lookup in DFT instantiation tests. |
| src/storm/utility/vector.h | Updates toIntegralVector to compute lcm/gcd on integer representations via Storm utilities. |
| src/storm/utility/RationalApproximation.cpp | Moves number-traits include to the implementation file. |
| src/storm/utility/random.cpp | Replaces carl::rationalize usage with storm::utility::convertNumber. |
| src/storm/utility/Extremum.cpp | Consolidates explicit instantiations to storm::RationalNumber/coefficient with a build-time guard. |
| src/storm/utility/constants.h | Adds tryParseNumber plus integer gcd/lcm declarations; removes asFraction declaration. |
| src/storm/utility/constants.cpp | Adds gcd/lcm implementations (std + CLN/GMP specializations) and routes parsing through tryParseNumber. |
| src/storm/storage/SparseMatrix.cpp | Replaces CLN/GMP-specific explicit instantiations with storm::RationalNumber and adjusts instantiation ordering. |
| src/storm/storage/jani/visitor/JSONExporter.cpp | Replaces fraction extraction via asFraction with explicit numerator/denominator utilities. |
| src/storm/storage/geometry/nativepolytopeconversion/HyperplaneCollector.h | Replaces carl::hash_add with boost::hash_combine. |
| src/storm/storage/expressions/ToRationalNumberVisitor.cpp | Uses storm::utility::convertNumber for integer literal conversion. |
| src/storm/storage/expressions/ToRationalFunctionVisitor.cpp | Uses int_fast64_t for exponent conversion and Storm conversion utilities. |
| src/storm/storage/expressions/BinaryNumericalFunctionExpression.cpp | Routes integer checks/pow/mod through Storm utilities. |
| src/storm/solver/stateelimination/EquationSystemEliminator.cpp | Adds adapter includes to avoid direct carl dependencies. |
| src/storm/solver/SolveGoal.h | Moves configureLinearEquationSolver definition out-of-line (declaration only in header). |
| src/storm/solver/SolveGoal.cpp | Reintroduces configureLinearEquationSolver with if constexpr filtering and explicit instantiations. |
| src/storm/models/symbolic/Model.cpp | Adds NumberTraits include for numeric trait access. |
| src/storm/modelchecker/results/ParetoCurveCheckResult.cpp | Adds NumberTraits include and keeps vector utilities usage consistent. |
| src/storm/logic/Bound.cpp | Updates explicit instantiations to storm::RationalNumber (+ coefficient guard). |
| src/storm/generator/PrismNextStateGenerator.cpp | Uses storm::BoundType alias instead of carl::BoundType. |
| src/storm/builder/DdJaniModelBuilder.cpp | Creates RF variables via Storm adapter rather than carl::freshRealVariable. |
| src/storm/adapters/RationalFunctionForward.h | Introduces STORM_RATIONAL_NUMBER_DIFFERS_FROM_COEFFICIENT configuration macro. |
| src/storm/adapters/RationalFunctionAdapter.h | Adds RF variable pool helper API (findRFVariable, clearRFVariablePool). |
| src/storm/adapters/RationalFunctionAdapter.cpp | Implements the new RF variable pool helper functions. |
| src/storm/adapters/IntervalAdapter.h | Adds storm::BoundType alias to avoid direct carl exposure at call sites. |
| src/storm/adapters/EigenAdapter.h | Replaces carl::hash_add with boost::hash_combine for Eigen vector hashing. |
| src/storm/adapters/eigen.h | Ensures Eigen-accessible numeric helpers by including the rational-function forward header. |
| src/storm-pomdp/analysis/WinningRegion.cpp | Routes exponentiation through storm::utility::pow. |
| src/storm-parsers/parser/ValueParser.cpp | Uses storm::BoundType and storm::utility::tryParseNumber for parsing. |
| src/storm-pars/utility/parametric.cpp | Consolidates evaluation specializations to storm::RationalNumber and (optionally) coefficient type. |
| src/storm-pars/transformer/RobustParameterLifter.cpp | Replaces carl::hash_add with boost::hash_combine for hashing. |
| src/storm-pars/transformer/ParameterLifter.h | Replaces carl::hash_add with boost::hash_combine for hashing. |
| src/storm-pars/transformer/ParameterLifter.cpp | Updates hashing logic to use boost::hash_combine. |
| src/storm-pars/transformer/BigStep.h | Routes pow usage through storm::utility::pow. |
| src/storm-pars/transformer/BigStep.cpp | Replaces direct carl factorized-polynomial usage with Storm polynomial typedefs. |
| src/storm-pars/derivative/GradientDescentInstantiationSearcher.h | Simplifies sqrt handling to storm::utility::sqrt for all constant types. |
| src/storm-pars/api/export.cpp | Removes hard dependency on carl::Formula<...> in lambdas by switching to auto. |
| src/storm-pars-cli/sampling.h | Uses Storm RF variable lookup and adds validation/error reporting for missing parameters. |
| src/storm-dft/storage/OrderDFTElementsById.cpp | Fixes includes and aligns template instantiation type spelling with storm::RationalFunction. |
| src/storm-dft/storage/DFT.h | Adds rational-function forward include for type availability. |
| resources/3rdparty/sylvan/src/storm_wrapper.cpp | Routes numeric ops (pow/mod/floor/ceil/abs) through Storm utilities and updates exponent conversion types. |
Review details
- Files reviewed: 48/48 changed files
- Comments generated: 2
- Review effort level: Lite
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The goal is to reduce the direct calls to
carlin the code and instead go through either an adapter orconstants.h.Some notable changes:
storm::RationalNumberandstorm::RationalFunctionCoefficientinstead ofCln/GmpRationalNumber, because the type of value (exact or from rational function) is more relevant than the underlying library. Introduced defineSTORM_RATIONAL_NUMBER_DIFFERS_FROM_COEFFICIENTto disable instantiations if both number types coincide.carl:hash_addbyboost::hash_combine. Carl still uses an older version of the hash which has issues.gcdandlcmfor Integers and revisedvector::toIntegralVector. The function now performs the operations on integers instead of rational representations of integers.