Zenna Tavares
Zenna Tavares
Often Auxiliary variables may help make a problem more concise, less vulnerable to the dependency problem and hence easier to solve by a solver. They may also make it much...
Implement both the forward and backwards operators, e.g. we should be able to do `quantile(Normal, Interval(0,1), Interval(0,1))`
We should be able to access values of a RandArray with Integer-valued RandomVariable. This should result in an abstraction of the elements, for example a disjunction The following should work...
Suppose the initial box is all full, we won't split it and we won't accept it, which is just wrong.. ``` using Sigma X = Sigma.uniform(0,1) condition = (X
Running the following example gives different bounds for z3 and dReal ``` julia A = ifelse(Sigma.flipsmt(0.4),Sigma.discreteuniformsmt(0,1),1) prob(A==1) julia> prob(A==1;solver=Sigma.z3) Reached Max iterations - 1000 [0.7990226745605464 0.800918579101562] julia> prob(A==1;solver=Sigma.dreal) Reached Max...
The mechanism for RandVars whose rangetype is some arbitrary Julia type, needs to be fleshed out. This, surprisingly, hasn't been much of an issue before because we could just use...
I think I am losing floating points in the refinement or somewhere. e.g. ``` prob(flipsmt(0.4)) => [0.3999999999999986 0.3999999999999986] ``` One way to see what is going on would be to...
When we call to the solver there is the possibility that it may not terminate. In this situation, one correct thing to do is assume it is a `TF` set,...
Some quantile functions such as the normal family's return positive of negative infinity. When refining, this **will** happen, for example `quantile(Normal(0,1), Omega) = [-Inf, Inf]`. Typically this doesn't cause a...