Advanced Search

sursumCorda

1284 Reputation

15 Badges

3 years, 82 days
Contact sursumCorda

MaplePrimes Activity


These are questions asked by sursumCorda

Why is the SMTLIB['Satisfy'] command inc...

sursumCorda 1284 Maple 2023
windows compatibility smtlib
April 04 2023
0 0

Here is a demonstration involving two decision problems (where evalf is applied to the output for better readability): 
 

> 

interface(version);
> 

restart;

`Standard Worksheet Interface, Maple 2023.0, Windows 10, March 6 2023 Build ID 1689885`

 (1)
> 

RealDomain:-solve({x*y = 3*z^5+4, x^2*y^2-3*x^2*z^2 = 1., x^3+y^3+z^3 = 12})

{x = 2.948903259, y = -2.257458014, z = -1.288554964}, {x = -.7294615910, y = 2.402430460, z = -1.139060479}, {x = .6177631401, y = 2.331476708, z = -.9687540923}, {x = 2.113678892, y = 1.450731881, z = -.7917893433}

 (2)
> 

SMTLIB:-Satisfy({x*y = 3*z^5+4, x^2*y^2-3*x^2*z^2 = 1, x^3+y^3+z^3 = 12}, showsmtlib)

(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(assert (and (= (* x y) (+ (* (* z z z z z) 3) 4)) (= (+ (* (* x x) (* y y)) (* (* (* x x) (* z z)) (- 3))) 1) (= (+ (* x x x) (* y y y) (* z z z)) 12)))
(check-sat)
(exit)

  

Error, (in SMTLIB:-smtlib_execute) external linking: error loading external library mplsmtlib.dll: �Ҳ���ָ����ģ�顣

  
> 

RealDomain:-solve({(x^2-2*y*z)*(x^3-y+z) = 0, x^4-y*z^3 = 2., z^4+x^3-2*x*y+3*y*z = 0})

{x = -1.130532018, y = -.1818551573, z = 1.263080805}, {x = 1.123233144, y = .4467032548, z = -.9704268675}, {x = 1.250562423, y = 2.517328867, z = .5615663246}, {x = 2.489770959, y = 16.73009962, z = 1.296110460}, {x = -1.336432744, y = -.7736167557, z = -1.154352246}, {x = 1.209937072, y = 1.655230257, z = .4422187526}

 (3)
> 

SMTLIB:-Satisfy({(x^2-2*y*z)*(x^3-y+z) = 0, x^4-y*z^3 = 2, z^4+x^3-2*x*y+3*y*z = 0}, showsmtlib)

(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(assert (and (= (* (+ (* x x) (* (* y z) (- 2))) (+ (* x x x) (* y (- 1)) z)) 0) (= (- (* x x x x) (* y (* z z z))) 2) (= (+ (* z z z z) (* x x x) (* (* x y) (- 2)) (* (* y z) 3)) 0)))
(check-sat)
(exit)

  

Error, (in SMTLIB:-smtlib_execute) external linking: error loading external library mplsmtlib.dll: �Ҳ���ָ����ģ�顣

  

?SMTLIB:-Satisfy


 

Download SMTLIB[Satisfy].mw

As you can see, the SMTLIB:-Satisfy command fails to work in Maple 2023, and I have to install the Visual Studio 2013 (VC++ 12.0) manually. But unfortunately, even if I have installed the vcredist_x64.exe beforehand, the computation still cannot be done in 1000 seconds! (Please note that I just require one real instance rather than all solutions.) Does anyone know why? 
By the way, since the default SMT solver (in Maple 2023) is Z3, will another SMT solver (like cvc5) be supported in future Maple releases?

Is there any bug in the new Quantifier E...

sursumCorda 1284 Maple 2023
quantifierelimination
April 01 2023
0 2

The QuantifierElimination package has been added in Maple 2023.
However, in the following example, the old (yet not obsolete) RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination command can solve the problem, but strangely, the new QuantifierElimination:-QuantifierEliminate command simply returns an error. 
 

> 

restart;
> 

RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination(:-`&A`([x, y, t]), :-`&implies`(:-`&and`(x^3+y^2-x = t, t^2 = 4/27, t < 0), x^2+y^2 >= rho), output = rootof)

rho <= 1/3

 (1)
> 

QuantifierElimination:-QuantifierEliminate(:-forall([x, y, t], :-Implies(:-And(x^3+y^2-x = t, t^2 = 4/27, t < 0), x^2+y^2 >= rho)))

Error, (in CADCell:-CCHILD) intervals the same at this precision

  
> 

Digits += 5:
> 

RegularChains:-SemiAlgebraicSetTools:-QuantifierElimination(:-`&A`([x, y, t]), :-`&implies`(:-`&and`(x^3+y^2-x = t, t^2 = 4/27, t < 0), x^2+y^2 >= rho), output = rootof)

rho <= 1/3

 (2)
> 

QuantifierElimination:-QuantifierEliminate(:-forall([x, y, t], :-Implies(:-And(x^3+y^2-x = t, t^2 = 4/27, t < 0), x^2+y^2 >= rho)))

Error, (in convert/RootOf) there is no root of 3*_Z^2-1 in -348986823692397556565591/604462909807314587353088 .. -174493411846198778282755/302231454903657293676544

  
> 

NULL


 

Download QEbug.mw

Code: 

QuantifierElimination[QuantifierEliminate](forall([x, y, t], Implies(And(x^3 + y^2 - x = t, And(t^2 = 4/27, t < 0)), x^2 + y^2 >= rho)));

So, is there any bug in Maple's QuantifierElimination package?

"Error, (in simplify/size/collect_and_re...

sursumCorda 1284 Maple 2023
simplify
March 31 2023
1 5

As you can see, if I want to simplify the following expression, I shall have to run the simplify command three times, and if I add some assumptions, the global simplify command will no longer work! 

:-simplify(2*(x^2+1)^(1/2)*(x+y+(x+y)/(x*y-1))^2/(((1/2)*(x+y+(x+y)/(x*y-1))*(2*x+(x+y)/(x*y-1)+y)/(x^2+1)^(1/2)-(1/2)*(2*x+(x+y)/(x*y-1)+y)*(y+(x+y)/(x*y-1))/(x^2+1)^(1/2)+(x+y+(x+y)/(x*y-1))/x)^2*x));


Download collect_and_recurse)_invalid_arguments_to_coeffs_.mws

But here either Physics[Simplify] or evala@Simplify works (with a slightly different result, though). Does anyone know why?

Why does the procedure maximize still re...

sursumCorda 1284 Maple 2023
minimize maximize
March 21 2023
1 17

Here is an apparent instance: 

> 

interface(version);
> 

maximize((1+20230321)*x*y-(x^2+y^2)*(1/2))``

`Standard Worksheet Interface, Maple 2023.0, Windows 10, March 6 2023 Build ID 1689885`

  

0

 (1)
> 

NULL

Download incorrectAgain.mw

Why???
Quite evidently, its supremum cannot be 0. (There are, of course, other approaches to compute it symbolically, yet I just wonder about the cause of this bug.)

Why is zip slower than `~`?...

sursumCorda 1284 Maple 2023
performance zip elementwise
March 16 2023
0 6

For two nonempty lists (of the same length), 

F~(list1, ` $`, list2); # space-dollarsign

is (almost) equivalent to 

zip(F, list1, list2);

However, it appears that in practice, using `~` can be faster than its equivalent zip version.
Here is a typical test: 

> 

restart;
> 

x := combinat:-randperm(10^7):
y := combinat:-randperm(10^7):
> 

undefine(f);
> 

t2 := CodeTools[Usage](`~`[f](x, ` $`, y), iterations = 10)

memory used=0.62GiB, alloc change=1.21GiB, cpu time=51.35s, real time=14.77s, gc time=42.55s

  
> 

t4 := CodeTools[Usage](zip(f, x, y), iterations = 10)

memory used=0.52GiB, alloc change=-4.00MiB, cpu time=53.88s, real time=16.25s, gc time=44.51s

  
> 

evalb(t2 = t4)

true

 (1)
> 

NULL


 

Download `~`_and_zip.mw

But I cannot find any explanations in the documentation (as well as What is Maple's equivalent to Mathematica's MapThread?). Does anyone know why?

First 17 18 19 20 21 22 23 Page 19 of 24