Skip to content

Commit 5473044

Browse files
ajreynolclaude
ajreynol
and
claude
committed
Document that QE does not support free variables
Also format unit tests. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
1 parent 5dcb5d9 commit 5473044

5 files changed

Lines changed: 64 additions & 16 deletions

File tree

‎include/cvc5/c/cvc5.h‎

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4900,6 +4900,12 @@ CVC5_EXPORT const char* cvc5_get_model(Cvc5* cvc5,
49004900
* (get-qe <q>)
49014901
* \endverbatim
49024902
*
4903+
* @note The formula @f$q@f$ must not contain free variables, i.e.,
4904+
* variables constructed via cvc5_mk_var() that are not bound by a
4905+
* quantifier in @f$q@f$. The symbols @f$y_1...y_j@f$ should be free
4906+
* constants constructed via cvc5_mk_const(). An error is raised if
4907+
* @f$q@f$ contains free variables.
4908+
*
49034909
* @note Quantifier Elimination is is only complete for logics such as LRA,
49044910
* LIA and BV.
49054911
*
@@ -4916,7 +4922,7 @@ CVC5_EXPORT const char* cvc5_get_model(Cvc5* cvc5,
49164922
* @f$A@f$ asserted to this solver:
49174923
* - @f$(A \wedge q)@f$ and @f$(A \wedge \phi)@f$ are equivalent
49184924
* - @f$\phi@f$ is quantifier-free formula containing only free
4919-
* variables in @f$y_1...y_n@f$.
4925+
* constants in @f$y_1...y_j@f$.
49204926
*/
49214927
CVC5_EXPORT Cvc5Term cvc5_get_quantifier_elimination(Cvc5* cvc5, Cvc5Term q);
49224928

@@ -4932,6 +4938,12 @@ CVC5_EXPORT Cvc5Term cvc5_get_quantifier_elimination(Cvc5* cvc5, Cvc5Term q);
49324938
* (get-qe-disjunct <q>)
49334939
* \endverbatim
49344940
*
4941+
* @note The formula @f$q@f$ must not contain free variables, i.e.,
4942+
* variables constructed via cvc5_mk_var() that are not bound by a
4943+
* quantifier in @f$q@f$. The symbols @f$y_1...y_j@f$ should be free
4944+
* constants constructed via cvc5_mk_const(). An error is raised if
4945+
* @f$q@f$ contains free variables.
4946+
*
49354947
* @note Quantifier Elimination is is only complete for logics such as LRA,
49364948
* LIA and BV.
49374949
*
@@ -4950,7 +4962,7 @@ CVC5_EXPORT Cvc5Term cvc5_get_quantifier_elimination(Cvc5* cvc5, Cvc5Term q);
49504962
* @f$\forall@f$, and @f$(A \wedge \phi \implies A \wedge q)@f$ if
49514963
* @f$Q@f$ is @f$\exists@f$
49524964
* - @f$\phi@f$ is quantifier-free formula containing only free
4953-
* variables in @f$y_1...y_n@f$
4965+
* constants in @f$y_1...y_j@f$
49544966
* - If @f$Q@f$ is @f$\exists@f$, let @f$(A \wedge Q_n)@f$ be the
49554967
* formula
49564968
* @f$(A \wedge \neg (\phi \wedge Q_1) \wedge ... \wedge

‎include/cvc5/cvc5.h‎

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6256,6 +6256,12 @@ class CVC5_EXPORT Solver
62566256
* @note Quantifier Elimination is is only complete for logics such as LRA,
62576257
* LIA and BV.
62586258
*
6259+
* @note The formula @f$q@f$ must not contain free variables, i.e.,
6260+
* variables constructed via TermManager::mkVar() that are not bound by a
6261+
* quantifier in @f$q@f$. The symbols @f$y_1...y_j@f$ should be free
6262+
* constants constructed via TermManager::mkConst(). An exception is thrown
6263+
* if @f$q@f$ contains free variables.
6264+
*
62596265
* @warning This function is experimental and may change in future versions.
62606266
*
62616267
* @param q A quantified formula of the form
@@ -6268,7 +6274,7 @@ class CVC5_EXPORT Solver
62686274
* @f$A@f$ asserted to this solver:
62696275
* - @f$(A \wedge q)@f$ and @f$(A \wedge \phi)@f$ are equivalent
62706276
* - @f$\phi@f$ is quantifier-free formula containing only free
6271-
* variables in @f$y_1...y_n@f$.
6277+
* constants in @f$y_1...y_j@f$.
62726278
*/
62736279
Term getQuantifierElimination(const Term& q) const;
62746280

@@ -6287,6 +6293,12 @@ class CVC5_EXPORT Solver
62876293
* @note Quantifier Elimination is is only complete for logics such as LRA,
62886294
* LIA and BV.
62896295
*
6296+
* @note The formula @f$q@f$ must not contain free variables, i.e.,
6297+
* variables constructed via TermManager::mkVar() that are not bound by a
6298+
* quantifier in @f$q@f$. The symbols @f$y_1...y_j@f$ should be free
6299+
* constants constructed via TermManager::mkConst(). An exception is thrown
6300+
* if @f$q@f$ contains free variables.
6301+
*
62906302
* @warning This function is experimental and may change in future versions.
62916303
*
62926304
* @param q A quantified formula of the form
@@ -6301,7 +6313,7 @@ class CVC5_EXPORT Solver
63016313
* @f$\forall@f$, and @f$(A \wedge \phi \implies A \wedge q)@f$ if
63026314
* @f$Q@f$ is @f$\exists@f$
63036315
* - @f$\phi@f$ is quantifier-free formula containing only free
6304-
* variables in @f$y_1...y_n@f$
6316+
* constants in @f$y_1...y_j@f$
63056317
* - If @f$Q@f$ is @f$\exists@f$, let @f$(A \wedge Q_n)@f$ be the
63066318
* formula
63076319
* @f$(A \wedge \neg (\phi \wedge Q_1) \wedge ... \wedge

‎src/api/java/io/github/cvc5/Solver.java‎

Lines changed: 14 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2912,6 +2912,12 @@ public String getModel(Sort[] sorts, Term[] vars)
29122912
* Quantifier Elimination is is only complete for logics such as LRA,
29132913
* LIA and BV.
29142914
*
2915+
* The formula {@code q} must not contain free variables, i.e., variables
2916+
* constructed via {@link TermManager#mkVar(Sort)} that are not bound by a
2917+
* quantifier in {@code q}. The symbols {@code y1...yn} should be free
2918+
* constants constructed via {@link TermManager#mkConst(Sort)}. An exception
2919+
* is thrown if {@code q} contains free variables.
2920+
*
29152921
* @api.note This method is experimental and may change in future versions.
29162922
*
29172923
* @param q A quantified formula of the form:
@@ -2921,7 +2927,7 @@ public String getModel(Sort[] sorts, Term[] vars)
29212927
* {@code A} asserted to this solver:
29222928
* - {@code ( A && q )} and {@code ( A && ret )} are equivalent
29232929
* - {@code ret} is quantifier-free formula containing only free
2924-
* variables in {@code y1...yn}.
2930+
* constants in {@code y1...yn}.
29252931
*/
29262932
public Term getQuantifierElimination(Term q)
29272933
{
@@ -2943,6 +2949,12 @@ public Term getQuantifierElimination(Term q)
29432949
* Quantifier Elimination is is only complete for logics such as LRA,
29442950
* LIA and BV.
29452951
*
2952+
* The formula {@code q} must not contain free variables, i.e., variables
2953+
* constructed via {@link TermManager#mkVar(Sort)} that are not bound by a
2954+
* quantifier in {@code q}. The symbols {@code y1...yn} should be free
2955+
* constants constructed via {@link TermManager#mkConst(Sort)}. An exception
2956+
* is thrown if {@code q} contains free variables.
2957+
*
29462958
* @api.note This method is experimental and may change in future versions.
29472959
*
29482960
* @param q A quantified formula of the form:
@@ -2952,7 +2964,7 @@ public Term getQuantifierElimination(Term q)
29522964
* asserted to this solver:
29532965
* - {@code (A ^ q) => (A ^ ret)} if {@code Q} is forall or
29542966
* {@code (A ^ ret) => (A ^ q)} if {@code Q} is exists,
2955-
* - ret is quantifier-free formula containing only free variables
2967+
* - ret is quantifier-free formula containing only free constants
29562968
* in {@code y1...yn},
29572969
* - If Q is exists, let {@code A && Q_n} be the formula
29582970
* {@code A && ~(ret && Q_1) && ... && ~(ret && Q_n)}

‎src/api/python/cvc5.pxi‎

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4296,6 +4296,13 @@ cdef class Solver:
42964296
Currently, the only logics supported by quantifier elimination
42974297
are LRA and LIA.
42984298
4299+
The formula :math:`q` must not contain free variables, i.e.,
4300+
variables constructed via :py:meth:`TermManager.mkVar()` that are
4301+
not bound by a quantifier in :math:`q`. The symbols
4302+
:math:`y_1...y_j` should be free constants constructed via
4303+
:py:meth:`TermManager.mkConst()`. An exception is thrown if
4304+
:math:`q` contains free variables.
4305+
42994306
.. warning::
43004307
43014308
This function is experimental and may change in future versions.
@@ -4313,7 +4320,7 @@ cdef class Solver:
43134320
- :math:`(A \\wedge q)` :math:`(A \\wedge \\phi)` are
43144321
equivalent
43154322
- :math:`\\phi` is quantifier-free formula containing only
4316-
free variables in :math:`y_1...y_n`.
4323+
free constants in :math:`y_1...y_j`.
43174324
"""
43184325
return _term(self.tm, self.csolver.getQuantifierElimination(term.cterm))
43194326

@@ -4332,6 +4339,13 @@ cdef class Solver:
43324339
Currently, the only logics supported by quantifier elimination
43334340
are LRA and LIA.
43344341
4342+
The formula :math:`q` must not contain free variables, i.e.,
4343+
variables constructed via :py:meth:`TermManager.mkVar()` that are
4344+
not bound by a quantifier in :math:`q`. The symbols
4345+
:math:`y_1...y_j` should be free constants constructed via
4346+
:py:meth:`TermManager.mkConst()`. An exception is thrown if
4347+
:math:`q` contains free variables.
4348+
43354349
.. warning::
43364350
43374351
This function is experimental and may change in future versions.
@@ -4350,7 +4364,7 @@ cdef class Solver:
43504364
:math:`(A \\wedge \\phi \\implies A \\wedge q)` if
43514365
:math:`Q` is :math:`\\exists`
43524366
- :math:`\\phi` is quantifier-free formula containing only
4353-
free variables in :math:`y_1...y_n`
4367+
free constants in :math:`y_1...y_j`
43544368
- If :math:`Q` is :math:`\\exists`, let :math:`(A \\wedge Q_n)`
43554369
be the formula
43564370
:math:`(A \\wedge \\neg (\\phi \\wedge Q_1) \\wedge ... \\wedge \\neg (\\phi \\wedge Q_n))`

‎test/unit/api/cpp/api_solver_black.cpp‎

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1575,10 +1575,9 @@ TEST_F(TestApiBlackSolver, getQuantifierElimination)
15751575
ASSERT_NO_THROW(d_solver->getQuantifierElimination(forall));
15761576
// free variables are not allowed
15771577
Term y = d_tm.mkVar(d_bool, "y");
1578-
Term forallFv =
1579-
d_tm.mkTerm(Kind::FORALL,
1580-
{d_tm.mkTerm(Kind::VARIABLE_LIST, {x}),
1581-
d_tm.mkTerm(Kind::OR, {x, y})});
1578+
Term forallFv = d_tm.mkTerm(
1579+
Kind::FORALL,
1580+
{d_tm.mkTerm(Kind::VARIABLE_LIST, {x}), d_tm.mkTerm(Kind::OR, {x, y})});
15821581
ASSERT_THROW(d_solver->getQuantifierElimination(forallFv), CVC5ApiException);
15831582

15841583
TermManager tm;
@@ -1602,10 +1601,9 @@ TEST_F(TestApiBlackSolver, getQuantifierEliminationDisjunct)
16021601
ASSERT_NO_THROW(d_solver->getQuantifierEliminationDisjunct(forall));
16031602
// free variables are not allowed
16041603
Term y = d_tm.mkVar(d_bool, "y");
1605-
Term forallFv =
1606-
d_tm.mkTerm(Kind::FORALL,
1607-
{d_tm.mkTerm(Kind::VARIABLE_LIST, {x}),
1608-
d_tm.mkTerm(Kind::OR, {x, y})});
1604+
Term forallFv = d_tm.mkTerm(
1605+
Kind::FORALL,
1606+
{d_tm.mkTerm(Kind::VARIABLE_LIST, {x}), d_tm.mkTerm(Kind::OR, {x, y})});
16091607
ASSERT_THROW(d_solver->getQuantifierEliminationDisjunct(forallFv),
16101608
CVC5ApiException);
16111609

0 commit comments

Comments
 (0)