From 86cc730908085942f4df19e3b24ebddc7557396f Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 1 Oct 2020 17:29:17 -0700 Subject: [PATCH] SyGuS: Add min/max (sub)normal constants to FP default grammar. (#5185) --- src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index d924c0805..1b86afb85 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -439,6 +439,14 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, ops.push_back(nm->mkConst(FloatingPoint::makeInf(fp_size, false))); ops.push_back(nm->mkConst(FloatingPoint::makeZero(fp_size, true))); ops.push_back(nm->mkConst(FloatingPoint::makeZero(fp_size, false))); + ops.push_back(nm->mkConst(FloatingPoint::makeMinSubnormal(fp_size, true))); + ops.push_back(nm->mkConst(FloatingPoint::makeMinSubnormal(fp_size, false))); + ops.push_back(nm->mkConst(FloatingPoint::makeMaxSubnormal(fp_size, true))); + ops.push_back(nm->mkConst(FloatingPoint::makeMaxSubnormal(fp_size, false))); + ops.push_back(nm->mkConst(FloatingPoint::makeMinNormal(fp_size, true))); + ops.push_back(nm->mkConst(FloatingPoint::makeMinNormal(fp_size, false))); + ops.push_back(nm->mkConst(FloatingPoint::makeMaxNormal(fp_size, true))); + ops.push_back(nm->mkConst(FloatingPoint::makeMaxNormal(fp_size, false))); } } -- 2.30.2