sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

multi-dimensional time bounds

tempestpy_adaptions
Sebastian Junges 7 years ago
parent
defcd7d5d7
commit
241fc88077
4 changed files with 199 additions and 115 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 190
      src/storm/logic/BoundedUntilFormula.cpp
  2. 38
      src/storm/logic/BoundedUntilFormula.h
  3. 30
      src/storm/logic/VariableSubstitutionVisitor.cpp
  4. 56
      src/storm/parser/JaniParser.cpp

190
src/storm/logic/BoundedUntilFormula.cpp
View File

@ -11,10 +11,20 @@
namespace storm {
namespace logic {
BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::optional<TimeBound> const& lowerBound, boost::optional<TimeBound> const& upperBound, TimeBoundReference const& timeBoundReference) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference(timeBoundReference), lowerBound(lowerBound), upperBound(upperBound) {
BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::optional<TimeBound> const& lowerBound, boost::optional<TimeBound> const& upperBound, TimeBoundReference const& timeBoundReference) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference({timeBoundReference}), lowerBound({lowerBound}), upperBound({upperBound}) {
STORM_LOG_THROW(lowerBound || upperBound, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound.");
}
BoundedUntilFormula::BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula,std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> const& timeBoundReferences) : BinaryPathFormula(leftSubformula, rightSubformula), timeBoundReference(timeBoundReferences), lowerBound(lowerBounds), upperBound(upperBounds) {
assert(timeBoundReferences.size() == upperBound.size());
assert(timeBoundReferences.size() == lowerBound.size());
STORM_LOG_THROW(this->getDimension() != 0, storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one dimension.");
for(unsigned i = 0; i < timeBoundReferences.size(); ++i) {
STORM_LOG_THROW(hasLowerBound(i) || hasUpperBound(i), storm::exceptions::InvalidArgumentException, "Bounded until formula requires at least one bound in each dimension.");
}
}
bool BoundedUntilFormula::isBoundedUntilFormula() const {
return true;
}
@ -28,111 +38,141 @@ namespace storm {
}
void BoundedUntilFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
if (this->getTimeBoundReference().isRewardBound()) {
referencedRewardModels.insert(this->getTimeBoundReference().getRewardName());
for (unsigned i = 0; i < this->getDimension(); ++i) {
if (this->getTimeBoundReference(i).isRewardBound()) {
referencedRewardModels.insert(this->getTimeBoundReference().getRewardName());
}
}
this->getLeftSubformula().gatherReferencedRewardModels(referencedRewardModels);
this->getRightSubformula().gatherReferencedRewardModels(referencedRewardModels);
}
TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference() const {
return timeBoundReference;
TimeBoundReference const& BoundedUntilFormula::getTimeBoundReference(unsigned i) const {
assert(i < timeBoundReference.size());
return timeBoundReference.at(i);
}
bool BoundedUntilFormula::isMultiDimensional() const {
assert(timeBoundReference.size() != 0);
return timeBoundReference.size() > 1;
}
unsigned BoundedUntilFormula::getDimension() const {
return timeBoundReference.size();
}
bool BoundedUntilFormula::isLowerBoundStrict() const {
return lowerBound.get().isStrict();
bool BoundedUntilFormula::isLowerBoundStrict(unsigned i) const {
assert(i < lowerBound.size());
return lowerBound.at(i).get().isStrict();
}
bool BoundedUntilFormula::hasLowerBound() const {
return static_cast<bool>(lowerBound);
for(auto const& lb : lowerBound) {
if (static_cast<bool>(lb)) {
return true;
}
}
return false;
}
bool BoundedUntilFormula::hasLowerBound(unsigned i) const {
return static_cast<bool>(lowerBound.at(i));
}
bool BoundedUntilFormula::hasIntegerLowerBound() const {
return lowerBound.get().getBound().hasIntegerType();
bool BoundedUntilFormula::hasIntegerLowerBound(unsigned i) const {
return lowerBound.at(i).get().getBound().hasIntegerType();
}
bool BoundedUntilFormula::isUpperBoundStrict() const {
return upperBound.get().isStrict();
bool BoundedUntilFormula::isUpperBoundStrict(unsigned i) const {
return upperBound.at(i).get().isStrict();
}
bool BoundedUntilFormula::hasUpperBound() const {
return static_cast<bool>(upperBound);
for(auto const& ub : upperBound) {
if (static_cast<bool>(ub)) {
return true;
}
}
return false;
}
bool BoundedUntilFormula::hasIntegerUpperBound() const {
return upperBound.get().getBound().hasIntegerType();
bool BoundedUntilFormula::hasUpperBound(unsigned i) const {
return static_cast<bool>(upperBound.at(i));
}
storm::expressions::Expression const& BoundedUntilFormula::getLowerBound() const {
return lowerBound.get().getBound();
bool BoundedUntilFormula::hasIntegerUpperBound(unsigned i) const {
return upperBound.at(i).get().getBound().hasIntegerType();
}
storm::expressions::Expression const& BoundedUntilFormula::getLowerBound(unsigned i) const {
return lowerBound.at(i).get().getBound();
}
storm::expressions::Expression const& BoundedUntilFormula::getUpperBound() const {
return upperBound.get().getBound();
storm::expressions::Expression const& BoundedUntilFormula::getUpperBound(unsigned i) const {
return upperBound.at(i).get().getBound();
}
template <>
double BoundedUntilFormula::getLowerBound() const {
double BoundedUntilFormula::getLowerBound(unsigned i) const {
checkNoVariablesInBound(this->getLowerBound());
double bound = this->getLowerBound().evaluateAsDouble();
double bound = this->getLowerBound(i).evaluateAsDouble();
STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return bound;
}
template <>
double BoundedUntilFormula::getUpperBound() const {
double BoundedUntilFormula::getUpperBound(unsigned i) const {
checkNoVariablesInBound(this->getUpperBound());
double bound = this->getUpperBound().evaluateAsDouble();
double bound = this->getUpperBound(i).evaluateAsDouble();
STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return bound;
}
template <>
storm::RationalNumber BoundedUntilFormula::getLowerBound() const {
checkNoVariablesInBound(this->getLowerBound());
storm::RationalNumber bound = this->getLowerBound().evaluateAsRational();
storm::RationalNumber BoundedUntilFormula::getLowerBound(unsigned i) const {
checkNoVariablesInBound(this->getLowerBound(i));
storm::RationalNumber bound = this->getLowerBound(i).evaluateAsRational();
STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return bound;
}
template <>
storm::RationalNumber BoundedUntilFormula::getUpperBound() const {
checkNoVariablesInBound(this->getUpperBound());
storm::RationalNumber bound = this->getUpperBound().evaluateAsRational();
storm::RationalNumber BoundedUntilFormula::getUpperBound(unsigned i) const {
checkNoVariablesInBound(this->getUpperBound(i));
storm::RationalNumber bound = this->getUpperBound(i).evaluateAsRational();
STORM_LOG_THROW(bound >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return bound;
}
template <>
uint64_t BoundedUntilFormula::getLowerBound() const {
checkNoVariablesInBound(this->getLowerBound());
int_fast64_t bound = this->getLowerBound().evaluateAsInt();
uint64_t BoundedUntilFormula::getLowerBound(unsigned i) const {
checkNoVariablesInBound(this->getLowerBound(i));
int_fast64_t bound = this->getLowerBound(i).evaluateAsInt();
STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return static_cast<uint64_t>(bound);
}
template <>
uint64_t BoundedUntilFormula::getUpperBound() const {
checkNoVariablesInBound(this->getUpperBound());
int_fast64_t bound = this->getUpperBound().evaluateAsInt();
uint64_t BoundedUntilFormula::getUpperBound(unsigned i) const {
checkNoVariablesInBound(this->getUpperBound(i));
int_fast64_t bound = this->getUpperBound(i).evaluateAsInt();
STORM_LOG_THROW(bound >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
return static_cast<uint64_t>(bound);
}
template <>
double BoundedUntilFormula::getNonStrictUpperBound() const {
double bound = getUpperBound<double>();
STORM_LOG_THROW(!isUpperBoundStrict() || bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
double BoundedUntilFormula::getNonStrictUpperBound(unsigned i) const {
double bound = getUpperBound<double>(i);
STORM_LOG_THROW(!isUpperBoundStrict(i) || bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
return bound;
}
template <>
uint64_t BoundedUntilFormula::getNonStrictUpperBound() const {
int_fast64_t bound = getUpperBound<uint64_t>();
if (isUpperBoundStrict()) {
uint64_t BoundedUntilFormula::getNonStrictUpperBound(unsigned i) const {
int_fast64_t bound = getUpperBound<uint64_t>(i);
if (isUpperBoundStrict(i)) {
STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
return bound - 1;
} else {
@ -148,41 +188,53 @@ namespace storm {
this->getLeftSubformula().writeToStream(out);
out << " U";
if (this->getTimeBoundReference().isRewardBound()) {
out << "{\"" << this->getTimeBoundReference().getRewardName() << "\"}";
if (this->isMultiDimensional()) {
out << "[";
}
if (this->hasLowerBound()) {
if (this->hasUpperBound()) {
if (this->isLowerBoundStrict()) {
out << "(";
} else {
out << "[";
}
out << this->getLowerBound();
out << ", ";
out << this->getUpperBound();
if (this->isUpperBoundStrict()) {
out << ")";
for(unsigned i = 0; i < this->getDimension(); ++i) {
if (i > 0) {
out << ",";
}
if (this->getTimeBoundReference(i).isRewardBound()) {
out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}";
}
if (this->hasLowerBound(i)) {
if (this->hasUpperBound(i)) {
if (this->isLowerBoundStrict(i)) {
out << "(";
} else {
out << "[";
}
out << this->getLowerBound(i);
out << ", ";
out << this->getUpperBound(i);
if (this->isUpperBoundStrict(i)) {
out << ")";
} else {
out << "]";
}
} else {
out << "]";
if (this->isLowerBoundStrict(i)) {
out << ">";
} else {
out << ">=";
}
out << getLowerBound(i);
}
} else {
if (this->isLowerBoundStrict()) {
out << ">";
if (this->isUpperBoundStrict(i)) {
out << "<";
} else {
out << ">=";
out << "<=";
}
out << getLowerBound();
out << this->getUpperBound(i);
}
} else {
if (this->isUpperBoundStrict()) {
out << "<";
} else {
out << "<=";
}
out << this->getUpperBound();
out << " ";
}
if (this->isMultiDimensional()) {
out << "]";
}
out << " ";
this->getRightSubformula().writeToStream(out);
return out;

38
src/storm/logic/BoundedUntilFormula.h
View File

@ -1,5 +1,4 @@
#ifndef STORM_LOGIC_BOUNDEDUNTILFORMULA_H_
#define STORM_LOGIC_BOUNDEDUNTILFORMULA_H_
#pragma once
#include <boost/optional.hpp>
@ -13,7 +12,8 @@ namespace storm {
class BoundedUntilFormula : public BinaryPathFormula {
public:
BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, boost::optional<TimeBound> const& lowerBound, boost::optional<TimeBound> const& upperBound, TimeBoundReference const& timeBoundReference);
BoundedUntilFormula(std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula, std::vector<boost::optional<TimeBound>> const& lowerBounds, std::vector<boost::optional<TimeBound>> const& upperBounds, std::vector<TimeBoundReference> const& timeBoundReferences);
virtual bool isBoundedUntilFormula() const override;
virtual bool isProbabilityPathFormula() const override;
@ -22,39 +22,43 @@ namespace storm {
virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
TimeBoundReference const& getTimeBoundReference() const;
TimeBoundReference const& getTimeBoundReference(unsigned i = 0) const;
bool isLowerBoundStrict() const;
bool isLowerBoundStrict(unsigned i = 0) const;
bool hasLowerBound() const;
bool hasIntegerLowerBound() const;
bool hasLowerBound(unsigned i) const;
bool hasIntegerLowerBound(unsigned i = 0) const;
bool isUpperBoundStrict() const;
bool isUpperBoundStrict(unsigned i = 0) const;
bool hasUpperBound() const;
bool hasIntegerUpperBound() const;
bool hasUpperBound(unsigned i) const;
bool hasIntegerUpperBound(unsigned i = 0) const;
bool isMultiDimensional() const;
unsigned getDimension() const;
storm::expressions::Expression const& getLowerBound() const;
storm::expressions::Expression const& getUpperBound() const;
storm::expressions::Expression const& getLowerBound(unsigned i = 0) const;
storm::expressions::Expression const& getUpperBound(unsigned i = 0) const;
template <typename ValueType>
ValueType getLowerBound() const;
ValueType getLowerBound(unsigned i = 0) const;
template <typename ValueType>
ValueType getUpperBound() const;
ValueType getUpperBound(unsigned i = 0) const;
template <typename ValueType>
ValueType getNonStrictUpperBound() const;
ValueType getNonStrictUpperBound(unsigned i = 0) const;
virtual std::ostream& writeToStream(std::ostream& out) const override;
private:
static void checkNoVariablesInBound(storm::expressions::Expression const& bound);
TimeBoundReference timeBoundReference;
boost::optional<TimeBound> lowerBound;
boost::optional<TimeBound> upperBound;
std::vector<TimeBoundReference> timeBoundReference;
std::vector<boost::optional<TimeBound>> lowerBound;
std::vector<boost::optional<TimeBound>> upperBound;
};
}
}
#endif /* STORM_LOGIC_BOUNDEDUNTILFORMULA_H_ */

30
src/storm/logic/VariableSubstitutionVisitor.cpp
View File

@ -37,17 +37,29 @@ namespace storm {
boost::any VariableSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
auto left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
auto right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
boost::optional<TimeBound> lowerBound;
if (f.hasLowerBound()) {
lowerBound = TimeBound(f.isLowerBoundStrict(), f.getLowerBound().substitute(substitution));
}
boost::optional<TimeBound> upperBound;
if (f.hasUpperBound()) {
upperBound = TimeBound(f.isUpperBoundStrict(), f.getUpperBound().substitute(substitution));
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds;
std::vector<boost::optional<storm::logic::TimeBound>> upperBounds;
std::vector<storm::logic::TimeBoundReference> tbReferences;
for (unsigned i = 0; i < f.getDimension(); ++i) {
std::cout << f.hasLowerBound(i) << std::endl;
if (f.hasLowerBound(i)) {
lowerBounds.push_back(TimeBound(f.isLowerBoundStrict(i), f.getLowerBound(i).substitute(substitution)));
} else {
lowerBounds.push_back(boost::none);
}
if (f.hasUpperBound(i)) {
upperBounds.push_back(TimeBound(f.isUpperBoundStrict(i), f.getUpperBound(i).substitute(substitution)));
} else {
lowerBounds.push_back(boost::none);
}
tbReferences.push_back(f.getTimeBoundReference(i));
}
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBound, upperBound, f.getTimeBoundReference()));
return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, lowerBounds, upperBounds, tbReferences));
}
boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {

56
src/storm/parser/JaniParser.cpp
View File

@ -165,9 +165,8 @@ namespace storm {
if (piStructure.count("lower") > 0) {
pi.lowerBound = parseExpression(piStructure.at("lower"), "Lower bound for property interval", {}, {});
// TODO substitute constants.
std::cout << "have lower bound" << std::endl;
STORM_LOG_THROW(!pi.lowerBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as lower bounds");
}
if (piStructure.count("lower-exclusive") > 0) {
STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present");
@ -175,16 +174,17 @@ namespace storm {
}
if (piStructure.count("upper") > 0) {
std::cout << "have upper bound" << std::endl;
pi.upperBound = parseExpression(piStructure.at("upper"), "Upper bound for property interval", {}, {});
// TODO substitute constants.
STORM_LOG_THROW(!pi.upperBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as upper bounds");
}
if (piStructure.count("upper-exclusive") > 0) {
STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present");
pi.lowerBoundStrict = piStructure.at("upper-exclusive");
STORM_LOG_THROW(pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present");
pi.upperBoundStrict = piStructure.at("upper-exclusive");
}
STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operators must be bounded");
STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operator must have a bounded interval, but no bounds found in '" << piStructure << "'");
return pi;
@ -367,22 +367,38 @@ namespace storm {
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time));
} else if (propertyStructure.count("reward-bounds") > 0 ) {
storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("reward-bounds"));
STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound.");
STORM_LOG_THROW(propertyStructure.at("reward-bounds").count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context);
storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("reward-bounds").at("exp"), "Reward expression in " + context, globalVars, constants);
STORM_LOG_THROW(!rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions.");
std::string rewardName = rewExpr.getVariables().begin()->getName();
STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type.");
double lowerBound = 0.0;
if(pi.hasLowerBound()) {
lowerBound = pi.lowerBound.evaluateAsDouble();
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds;
std::vector<boost::optional<storm::logic::TimeBound>> upperBounds;
std::vector<storm::logic::TimeBoundReference> tbReferences;
for (auto const& rbStructure : propertyStructure.at("reward-bounds")) {
storm::jani::PropertyInterval pi = parsePropertyInterval(rbStructure.at("bounds"));
STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound.");
STORM_LOG_THROW(rbStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context);
storm::expressions::Expression rewExpr = parseExpression(rbStructure.at("exp"), "Reward expression in " + context, globalVars, constants);
STORM_LOG_THROW(rewExpr.isVariable(), storm::exceptions::NotSupportedException, "Storm currently does not support complex reward expressions.");
std::string rewardName = rewExpr.getVariables().begin()->getName();
STORM_LOG_WARN("Reward-type (steps, time) is deduced from model type.");
double lowerBound = 0.0;
if(pi.hasLowerBound()) {
lowerBound = pi.lowerBound.evaluateAsDouble();
}
double upperBound = pi.upperBound.evaluateAsDouble();
STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative");
STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative");
if (pi.hasLowerBound()) {
lowerBounds.push_back(storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound));
} else {
lowerBounds.push_back(boost::none);
}
if (pi.hasUpperBound()) {
upperBounds.push_back(storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound));
} else {
upperBounds.push_back(boost::none);
}
tbReferences.push_back(storm::logic::TimeBoundReference(rewardName));
}
double upperBound = pi.upperBound.evaluateAsDouble();
STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative");
STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative");
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by storm");
return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], storm::logic::TimeBound(pi.lowerBoundStrict, pi.lowerBound), storm::logic::TimeBound(pi.upperBoundStrict, pi.upperBound), storm::logic::TimeBoundReference(rewardName));
auto res = std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], lowerBounds, upperBounds, tbReferences);
return res;
}
if (args[0]->isTrueFormula()) {

Write Preview
Loading…
Cancel
Save