Displaying 20 results from an estimated 247 matches for "z3".
2006 Jul 08
2
String mathematical function to R-function
...( R
function ).
thanks for any tips.
cleber
#e.g.
fun_String = "-100*x1 + 0*x2 + 100*x3"
fun <- function(x1,x2,x3){
return(
############
evaluation( fun_String )
############
)
True String mathematical function :-( :-(
> nomes
[1] "8.49*x1*z1 + 6.13*x1*z2 + 6.4*x1*z3 + 6.9*x2*z1 +
4.54*x2*z2 + 3.99*x2*z3 + 19.31*x3*z1 + 12.49*x3*z2 +
3.86*x3*z3 + 5.25*x1*z1*z2 + -6.2*x1*z1*z3 +
9.07*x1*z2*z3 + 10.87*x2*z1*z2 + 9.78*x2*z1*z3 +
49.05*x2*z2*z3 + 4.56*x1*x2*z1 + -4.9*x1*x2*z2 +
4.01*x1*x2*z3 + -0.39*x3*z1*z2 + 14.34*x3*z1*z3 +
0.7*x3*z2*z3 + -2.84*x1*x3*z1 + 20.25*...
2009 Nov 09
3
How to transform the Matrix into the way I want it ???
Hi, R users,
I'm trying to transform a matrix A into B (see below). Anyone knows how to
do it in R? Thanks.
Matrix A (zone to zone travel time)
zone z1 z2 z3 z1 0 2.9 4.3 z2 2.9 0 2.5 z3 4.3 2.5 0
B:
from to time z1 z1 0 z1 z2 2.9 z1 z3 4.3 z2 z1 2.9 z2 z2 0 z2 z3 2.5 z3 z1
4.3 z3 z2 2.5 z3 z3 0
The real matrix I have is much larger, with more than 2000 zones. But I
think it should be the same thing if I can transform A into B.
Thanks.
Garry
[...
2019 Feb 12
2
[cfe-dev] clang in official apt repo built without z3 support
I _think_ there is a problem with the license as well: Z3 is MIT, so clang
would have to be released with Z3's license.
On Tue, 12 Feb 2019, 09:24 Roman Lebedev via cfe-dev <cfe-dev at lists.llvm.org
wrote:
> On Tue, Feb 12, 2019 at 4:13 PM Paulo Matos via cfe-dev
> <cfe-dev at lists.llvm.org> wrote:
> >
> > Hello,
> &g...
2019 Feb 12
2
[cfe-dev] clang in official apt repo built without z3 support
On Tue, 12 Feb 2019, 14:32 Paulo Matos <pmatos at linki.tools wrote:
>
>
> On 12 February 2019 18:59:21 CET, Mikhail Ramalho <
> mikhail.ramalho at gmail.com> wrote:
> >I _think_ there is a problem with the license as well: Z3 is MIT, so
> >clang
> >would have to be released with Z3's license.
>
> I don't think that's a problem. You are not releasing z3 with clang. This
> is an apt repo.
Well, I'm not an expert, but building clang linked with z3 and offering it
online for people to...
2010 Feb 05
1
String Manipulation- Extract numerical and alphanumerical segment
I am currently attempting to split a long list of strings (let's call it
"string.list") that is of the format:
"1234567.z3.abcdef-gh.12"
I have gotten it to:
"1234567" "z3" "abcdef-gh" "12"
by use of the strsplit function.
This leaves me with each element of "string.list" having a split string of
the above format. What I'd like to do now is extract the fir...
2017 Jul 28
3
problem with "unique" function
I have the joint distribution of three discrete random variables z1, z2 and
z3 which is captured by "z"
and "prob" as described below.
For example, the probability for z1=0.46667, z2=-1 and z3=-1 is 2.752e-13.
Also, the probability adds up to 1.
> head(z) z1 z2 z3
[1,] -0.46667 -1.0000 -1.0000
[2,] -0.33333 -0.9333 -0.9333
[3,] -0....
2016 Feb 09
3
Buildling with/without AddressSanitizer causes divergent execution behaviour
...g a
heap-use-after-free which Valgrind is not reporting, which makes me
wonder if it is a false positive.
Any hints on how I might determine this? Building with UBSan doesn't
turn up anything.
# Longer version (if you are interested in the specific details)
The application of interest is the Z3 constraint solver [1].
Much of what I'm going to say is covered in [2] which is a bug report
I opened (including a heap-use-after-free AddressSanitizer finds, I'm
not sure if this a false positive or not) but here are the basics of
what I found.
Build Z3 as follows
```
git clone https://...
2006 Jun 14
3
A question about stepwise procedures: step function
...I don't understand is that data as data.frame worked well for my other programs, how come I cannot make it run this time. Could you please tell me how I can fix it?
***************************************************************************************************
>all<-data.frame(z1,z2,z3)
>fit.model.all<- coxph(Surv(t,cen) ~z1+z2+z3,data=all)
> reg.model.all<-step(fit.model.all)
Start: AIC= 689.1
Surv(t, cen) ~ z1 + z2 + z3
Error in as.data.frame.default(data) : cannot coerce class "function" into a data.frame
********************************************...
2013 Apr 05
2
[LLVMdev] Z3 and loadable optimization
I created a loadable optimization following the tutorial at
http://llvm.org/docs/WritingAnLLVMPass.html. I want to use the Z3 library,
installed in my system, in my optimization. When I include z3++.h (the name
of the library) in the code and use its classes, it compiles well, but when
I try to run it it says:
> opt: symbol lookup error: /home/giacomo/llvm/Debug+Asserts/lib/Acsl.so:
> undefined symbol: Z3_mk_config...
2006 Jan 27
1
about lm restrictions...
...0000 0.7454 -6.708 8.77e-05 ***
z1:x2 0.5000 0.7454 0.671 0.519177
z1:x3 -3.0000 0.7454 -4.025 0.002996 **
z2:x1 -6.0000 0.7454 -8.050 2.11e-05 ***
z2:x2 -5.0000 0.7454 -6.708 8.77e-05 ***
z2:x3 -4.5000 0.7454 -6.037 0.000193 ***
z3:x1 1.0000 0.7454 1.342 0.212580
z3:x2 1.5000 0.7454 2.012 0.075029 .
z3:x3 NA NA NA NA
Analysis of Variance Table
Response: y
Df Sum Sq Mean Sq F value Pr(>F)
z1:x1 1 16.674 16.674 30.0125 0.0003910 ***
z1:...
2013 Apr 05
0
[LLVMdev] Z3 and loadable optimization
On 4/5/13 3:16 PM, Giacomo Tagliabue wrote:
> I created a loadable optimization following the tutorial at
> http://llvm.org/docs/WritingAnLLVMPass.html. I want to use the Z3
> library, installed in my system, in my optimization. When I include
> z3++.h (the name of the library) in the code and use its classes, it
> compiles well, but when I try to run it it says:
>
> opt: symbol lookup error:
> /home/giacomo/llvm/Debug+Asserts/lib/Acsl.so:...
2013 Apr 05
1
[LLVMdev] Z3 and loadable optimization
I think I am in the first case, but I don't understand something, the -load
option during which command? opt? and which file should I load? libz3.so?
On 5 April 2013 15:32, John Criswell <criswell at illinois.edu> wrote:
> On 4/5/13 3:16 PM, Giacomo Tagliabue wrote:
>
> I created a loadable optimization following the tutorial at
> http://llvm.org/docs/WritingAnLLVMPass.html. I want to use the Z3
> library, installed...
2018 Mar 15
1
[GSoC 2018] Integrate with Z3 SMT solver to reduce false positives.
...lers. I have taken the only compilers course offered in my school and
did an independent study with my CS professor. Although I'll begin to work
in a couple of months, I definitely want to pursue my interest in compiler
design and optimization as a PhD in the future. I am very interested in the
z3 SMT solver project detailed on the LLVM website and have been doing some
research about it.
>From what I understand, the current analyzer traces the program, and at
each branch, it branches out into the true branch and the false branch. The
true and false branch causes certain constraints on th...
2009 Jul 02
1
lpSolve: how to allow variables to become negative
Dear all,
I am interested in solving a MIP problem with binary outcomes and
continuous variables, which ARE NOT RESTRICTED TO BE NEGATIVE. In
particular,
Max {z1,z2,z3,b1} z1 + z2 + z3
(s.t.)
# 7 z1 + 0 z2 + 0 z3 + b1 <= 5
# 0 z1 + 8 z2 + 0 z3 - b1 <= 5
# 0 z1 + 0 z2 + 6 z3 + b1 <= 7
# z1, z2, z3 BINARY {0,1}
# -5<= b1 <=5 (i.e. b1 <= 5; -b1 <= 5 )
Using the lpSolve package of R, I wrote:
library (lpSolve)
f.obj <- c(1, 1,...
2013 May 16
2
A function that can modify an object? Or at least shows principles how to modify an object?
...mmm ggg gindex map Info
aaa123 U1 1 1 1
aaa124 U1 1 2 1
bbb1378 U2 2 1 1
bbb8888 U2 2 2 0
bbb1389 U2 2 3 1
ccc2222 Z3 3 1 1
ccc33333 Z3 3 2 0
ccc4444 Z3 3 3 1
ccc55555 Z3 3 4 0
Before (see Before) the analysis I had dropped those "mmm" rows from
my.table of UUU that had Info==0, th...
2006 Mar 16
2
Using of LME function in non-replicate data
Hello all R-users!
In Jun-2005, I find the follow discussion about using
of
LME function ( in NLME library ) for fitting
non-replicate data
The thread: ANOVA vs REML approach to variance
component estimation
http://tolstoy.newcastle.edu.au/R/help/05/06/6498.html
Someone expose the follow problem:
# non-replicate data
y <- c(2.2, -1.4, -0.5, -0.3, -2.1, 1.5, 1.3, -0.3,
0.5, -1.4,
2017 Jul 28
0
problem with "unique" function
...case, it seems like all numbers are multiples of 1/30, so another idea could be to multiply by 30, round, and divide by 30.
-pd
> On 28 Jul 2017, at 17:17 , li li <hannah.hlx at gmail.com> wrote:
>
> I have the joint distribution of three discrete random variables z1, z2 and
> z3 which is captured by "z"
> and "prob" as described below.
>
> For example, the probability for z1=0.46667, z2=-1 and z3=-1 is 2.752e-13.
> Also, the probability adds up to 1.
>
>> head(z) z1 z2 z3
> [1,] -0.46667 -1.0000 -1.0000
>...
2018 Feb 25
3
include
...the data as you suggested but I could not find K1 in col1.
rbind(preval,mydat) Col1 Col2 col3
1 <NA> <NA> <NA>
2 X1 <NA> <NA>
3 Y1 <NA> <NA>
4 K2 <NA> <NA>
5 W1 <NA> <NA>
6 Z1 K1 K2
7 Z2 <NA> <NA>
8 Z3 X1 <NA>
9 Z4 Y1 W1
On Sat, Feb 24, 2018 at 6:18 PM, Jim Lemon <drjimlemon at gmail.com> wrote:
> hi Val,
> Your problem seems to be that the data are read in as a factor. The
> simplest way I can think of to get around this is:
>
> mydat <- read.table(textC...
2018 Feb 25
2
include
HI Jim and all,
I want to put one more condition. Include col2 and col3 if they are not
in col1.
Here is the data
mydat <- read.table(textConnection("Col1 Col2 col3
K2 X1 NA
Z1 K1 K2
Z2 NA NA
Z3 X1 NA
Z4 Y1 W1"),header = TRUE,stringsAsFactors=FALSE)
The desired out put would be
Col1 Col2 col3
1 X1 0 0
2 K1 0 0
3 Y1 0 0
4 W1 0 0
6 K2 X1 0
7 Z1 K1 K2
8 Z2 0 0
9 Z3 X1 0
10 Z4 Y1 W1
K2 is already is already in...
2016 Feb 11
3
Buildling with/without AddressSanitizer causes divergent execution behaviour
...;> relying on memory layout, etc.). I'm also observing ASan reporting a
>> heap-use-after-free which Valgrind is not reporting, which makes me
>> wonder if it is a false positive.
>
>
> Let us start from this heap-use-after-free report. The one in
> https://github.com/Z3Prover/z3/issues/436 looks legitimate.
> Unless the application does something extremely weird and tricky,
> heap-use-after-free reports are usually true positives.
The developers tell me they are doing some unusual things and they
believe that this might the cause of the report.
> Can yo...