Hello, Is there something like array expression in GiNaC? I want to do symbolic computation involving array expressions related to program verification. I would like to implement a theorem prover on top of GiNaC. So I also need conditional expressions. For example: x = mem[2] + 2; y = mem[i] -3; x >= 3; Can GiNaC represent these expressions? Note that array index might be a symbolic value. Thank you. - Zhongxing Xu
--- Zhongxing Xu <xuzhongxing@gmail.com> escribió:
Hello, Is there something like array expression in GiNaC? I want to do symbolic computation involving array expressions related to program verification. I would like to implement a theorem prover on top of GiNaC. So I also need conditional expressions.
For example: x = mem[2] + 2; y = mem[i] -3; x >= 3; Can GiNaC represent these expressions? Note that array index might be a symbolic value.
I assume you already considered +CAL? not that you can't do it with ginac, im sure its possible, but this is a language specific for the purpose of algorithm verification __________________________________________________ Preguntá. Respondé. Descubrí. Todo lo que querías saber, y lo que ni imaginabas, está en Yahoo! Respuestas (Beta). ¡Probalo ya! http://www.yahoo.com.ar/respuestas
I need something that can be compiled with my existing c++ code. So I think GiNaC is more suitable for me. After checking out the reference manual of GiNaC, I guess class idx and varidx and indexed() is the thing for me. Is it right? 2007/1/31, Charlls Quarra <charlls_quarra@yahoo.com.ar>:
--- Zhongxing Xu <xuzhongxing@gmail.com> escribió:
Hello, Is there something like array expression in GiNaC? I want to do symbolic computation involving array expressions related to program verification. I would like to implement a theorem prover on top of GiNaC. So I also need conditional expressions.
For example: x = mem[2] + 2; y = mem[i] -3; x >= 3; Can GiNaC represent these expressions? Note that array index might be a symbolic value.
I assume you already considered +CAL? not that you can't do it with ginac, im sure its possible, but this is a language specific for the purpose of algorithm verification
__________________________________________________ Preguntá. Respondé. Descubrí. Todo lo que querías saber, y lo que ni imaginabas, está en Yahoo! Respuestas (Beta). ¡Probalo ya! http://www.yahoo.com.ar/respuestas
_______________________________________________ GiNaC-list mailing list GiNaC-list@ginac.de https://www.cebix.net/mailman/listinfo/ginac-list
Dear Zhongxin Xu, On Wed, 31 Jan 2007, Zhongxing Xu wrote:
I need something that can be compiled with my existing c++ code. So I think GiNaC is more suitable for me. After checking out the reference manual of GiNaC, I guess class idx and varidx and indexed() is the thing for me. Is it right?
I think this is not such a good idea. The problem is that you get automatic dummy index renaming that may not be what you want. Best wishes, Chris
Hi! On Wed, Jan 31, 2007 at 10:16:56PM +0800, Zhongxing Xu wrote:
Is there something like array expression in GiNaC?
Could you elaborate, please? What is exactly "array expression"?
For example: x = mem[2] + 2; y = mem[i] -3; Can GiNaC represent these expressions? Note that array index might be a symbolic value.
GiNaC supports associative arrays with expressions as keys, i.e. symbol x("x"), y("y"), z("z"); exmap m; // nothing really magic: std::map<ex, ex, ex_is_less> m[z] = 2*x + y; m[1] = sin(y);
x >= 3;
Syntactically, this is correct GiNaC code. It creates object of the GiNaC::relational type. But I wonder what is _your_ interpretation...
After checking out the reference manual of GiNaC, I guess class idx and varidx and indexed() is the thing for me. Is it right?
I don't think so. Best regards, Alexei -- All science is either physics or stamp collecting.
Thank you for tips. Let me try to figure it out myself first. 2007/2/1, Sheplyakov Alexei <varg@theor.jinr.ru>:
Hi!
On Wed, Jan 31, 2007 at 10:16:56PM +0800, Zhongxing Xu wrote:
Is there something like array expression in GiNaC?
Could you elaborate, please? What is exactly "array expression"?
For example: x = mem[2] + 2; y = mem[i] -3; Can GiNaC represent these expressions? Note that array index might be a symbolic value.
GiNaC supports associative arrays with expressions as keys, i.e.
symbol x("x"), y("y"), z("z"); exmap m; // nothing really magic: std::map<ex, ex, ex_is_less> m[z] = 2*x + y; m[1] = sin(y);
x >= 3;
Syntactically, this is correct GiNaC code. It creates object of the GiNaC::relational type. But I wonder what is _your_ interpretation...
After checking out the reference manual of GiNaC, I guess class idx and varidx and indexed() is the thing for me. Is it right?
I don't think so.
Best regards, Alexei
-- All science is either physics or stamp collecting.
-----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.3 (GNU/Linux)
iQIVAwUBRcDJebL3rFoFceCwAQLvdw//cTzW84BkgGzzrBxXDdLFnlD+2I3+JYL+ qtAd9oJdr16XRF68GAFJa8fYgDFuiymKspaHzoxwkPQhTUeclezjNNR3NMGiSSxG xpSNfEYXuPSQ+W6dgbmgAtScCTYl0hALgqEh9llE8zNT4K56iKW4U4D7k5Aw2YND 9NNlQk8jbqgtzHYO0ip92a0XJ/Y2iIIGGL7hdR9UWIzjqQF7sa1oTBhb/itRr48l Bx3DoC7NtBqDJqjN4ZjZXIEVQ40ZRy6GimJMcph4pVND3ax3YmUMRmSlrL8OCFCJ 3mLXf1zBvJljo2LwyfRFUWEmcf4UGkYSINrTdVUpiU6RBobA6IEVZP2IkEYtmr0w vt/oeqiL7oIANNe72JGFVqIqExCLUNHtMTUx69rKjNd8FZn2hU31osRvFAIsfMbM ClGBBjf1l19ZTGUGLkcPzWhK3sVLxIOHwuy5bAPyXllehZhI5AYS+4jigGxvsdap S/iYDi+HVhteBygTXTUrBRyJY5CiV/Clwx5pTZnM1lgASRUoUM7dukF3BjwPgVVl VOtYdyC2+jOpW+dE0nXhdatHi4rce1WBhsZ67Ak/vcbWgGfK14K+6dV7VpLxaIU5 PQSTH0UBpTCzquhsxjVmmHcg9XdhxsfcKTsKlJvzTVRVdK/C44KcA81ebqyGE60l fnOg5IER/CI= =66N+ -----END PGP SIGNATURE-----
_______________________________________________ GiNaC-list mailing list GiNaC-list@ginac.de https://www.cebix.net/mailman/listinfo/ginac-list
Dear Zhongxing Xu, On Wed, 31 Jan 2007, Zhongxing Xu wrote:
Is there something like array expression in GiNaC?
[...]
x = mem[2] + 2; y = mem[i] -3; x >= 3; Can GiNaC represent these expressions? Note that array index might be a symbolic value.
It depends what kind of properties and automatic simplifications you want. If you simply want to type expressions of the form mem[something], defining your own symbolic function may already be sufficient. If you need more than that, you might have to define your own class that derives from the type basic. GiNaC can already represent expressions like x>=3. Good luck, Chris
participants (4)
-
Charlls Quarra
-
Chris Dams
-
varg＠theor.jinr.ru
-
Zhongxing Xu