From 6c8702ab5eb08466bf954e202241df39de680081 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 3 Jun 2020 08:47:46 -0500 Subject: Do not apply unconstrained simplification when quantifiers are present (#4532) Fixes #4437. This is a simpler fix that aborts the preprocessing pass when a quantifier is encountered. It also updates our smt2 parser to throw a logic exception when forall/exists is used in non-quantified logics. This is required to ensure that unconstrained simplification does not throw an exception to a user as a result of accidentally setting the wrong logic. --- src/parser/smt2/Smt2.g | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'src/parser') diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 081990a45..f29e03380 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1692,7 +1692,13 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2] std::vector argTypes; } : LPAREN_TOK quantOp[kind] - { PARSER_STATE->pushScope(true); } + { + if (!PARSER_STATE->isTheoryEnabled(theory::THEORY_QUANTIFIERS)) + { + PARSER_STATE->parseError("Quantifier used in non-quantified logic."); + } + PARSER_STATE->pushScope(true); + } boundVarList[bvl] term[f, f2] RPAREN_TOK { -- cgit v1.2.3