Advanced Search

sursumCorda

922 Reputation

13 Badges

2 years, 207 days
Contact sursumCorda

MaplePrimes Activity


These are questions asked by sursumCorda

Is the use of `solvefor` less reliable?...

sursumCorda 922 Maple 2023
solve
April 08 2023
1 3

Certainly, ½ cannot be a root of the following equations: 
 

> 

interface(version)
> 

restart;

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

 (1)
> 

solvefor[x]((x-RealDomain:-`^`(2, -1))*RealDomain:-`^`(x-2*RealDomain:-`^`(3, -1), -1)*(1-sqrt(1-x*(x-2*RealDomain:-`^`(3, -1))*RealDomain:-`^`(RealDomain:-`^`(x-RealDomain:-`^`(2, -1), 2), -1))) = 0)

Warning, solvefor is deprecated. Please use solve command.

  

[x = 0, x = 1/2]

 (2)
> 

`~`[limit]((x-1/2)*(1-sqrt(1-x*(x-2/3)/(x-1/2)^2))/(x-2/3), [x = 0, x = 1/2])

[0, undefined]

 (3)
> 

solvefor[x]((x-RealDomain:-`^`(2, -1))*RealDomain:-`^`(x-2*RealDomain:-`^`(3, -1), -1)*(1-sqrt(1+3*x*(x-2*RealDomain:-`^`(3, -1))*RealDomain:-`^`(5*RealDomain:-`^`(x-RealDomain:-`^`(2, -1), 2), -1))) = 0)

Warning, solvefor is deprecated. Please use solve command.

  

[x = 0, x = 1/2]

 (4)
> 

`~`[limit]((x-1/2)*(1-sqrt(1+3*x*(x-2/3)/(5*(x-1/2)^2)))/(x-2/3), [x = 0, x = 1/2])

[0, undefined]

 (5)
> 

``


 

Download solvefor_BUG.mw

But why can't Maple's solvefor rigorously verify (or at least try to check) the solution by itself?
Please note that this issue is irrelevant to the alleged deprecated command. You may reproduce these via :-solve, Degrees:-solve, RealDomain:-solve, PDEtools:-Solve, etc.

Why can't Maple check if 'm' is positive...

sursumCorda 922 Maple 2023
assuming coulditbe duplicate-question
April 06 2023
1 8

The following results should be true or false, but unfortunately, both of them become FAIL (in Maple 2023): 

> 

interface(version)
> 

_EnvTry := hard:

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

 (1)
> 

assume(`or`(n < 0, n >= 1), m > (1/2)*n*(n-1))
> 

is(m < 0);
> 

is(m > 0)

false

  

FAIL

 (2)
> 

coulditbe(m, 0)

FAIL

 (3)
> 

NULL


Download Unable_to_prove.mw

Does anyone know why?

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

sursumCorda 922 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 922 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 922 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?

First 12 13 14 15 16 17 18 Page 14 of 19