Reusing output of QEPCAD

qepcad

asked 2021-07-01 08:58:27 +0100

philipp7
391 ●6 ●11 ●28

Suppose we get a quantifier-free formula as an output from QEPCAD and we want to use that formula as an input for another call to QEPCAD. How can this be done? The naive approach does not work as the following example shows (a very trivial example as the first qepcad call does not actually do much):

sage: var("a,b")
sage: formula = qepcad(a+b==0)
sage: print(formula)
b + a = 0
sage: qepcad_formula.exists(b,formula)

yields the error

ValueError: Attempting to quantify variable which does not occur in formula

edit retag flag offensive close merge delete

add a comment

1 Answer

Sort by » oldest newest most voted

answered 2021-07-01 09:10:10 +0100

philipp7
391 ●6 ●11 ●28

Sorry, already got it. For anyone else needing this at some point, there is the function qformula which can be used. The example above then yields

sage: from sage.interfaces.qepcad import qformula
sage: var("a,b")
sage: formula = qepcad(a+b==0)
sage: qepcad_formula.exists(b,qformula(formula,frozenset(['a','b'])))
(E b)[b + a = 0]

edit flag offensive delete link

Comments

Well done. You can accept your own answer to mark the question as solved.

slelievre ( 2021-07-01 15:27:56 +0100 )edit

add a comment

Your Answer

Please start posting anonymously - your entry will be published after you log in or create a new account.

Add Answer

Question Tools

1 follower

Stats

Asked: 2021-07-01 08:58:27 +0100

Seen: 183 times

Last updated: Jul 01 '21

Reusing output of QEPCAD edit