Opened 16 years ago

Closed 15 years ago

#178 closed enhancement (wontfix)

Number of bound variables in a symbolic quantifier expression

Reported by: ywei Owned by: Stephen Siegel
Priority: minor Milestone:
Component: symbolic Version: 1.0
Keywords: Cc:

Description

Currently, only one bound variable is allowed in each symbolic quantifier expression. In CVC3 API, a quantifier (forall or exists) expression takes a list of bound variables. Do we need to change the symbolic quantifier expression to allow multiple bound variables?

Change History (1)

comment:1 by Stephen Siegel, 15 years ago

Resolution: → wontfix
Status: new → closed

Don't see advantage in this at this moment. Equivalent to forall x forall y ....

Note: See TracTickets for help on using tickets.