From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 2 Oct 2020 00:29:17 +0000 (-0700)
Subject: SyGuS: Add min/max (sub)normal constants to FP default grammar. (#5185)
X-Git-Tag: cvc5-1.0.0~2769
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=86cc730908085942f4df19e3b24ebddc7557396f;p=cvc5.git

SyGuS: Add min/max (sub)normal constants to FP default grammar. (#5185)
---

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)));
   }
 }