projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 75d47fd)
SyGuS: Add min/max (sub)normal constants to FP default grammar. (#5185)
authorAina Niemetz <aina.niemetz@gmail.com>
Fri, 2 Oct 2020 00:29:17 +0000 (17:29 -0700)
committerGitHub <noreply@github.com>
Fri, 2 Oct 2020 00:29:17 +0000 (19:29 -0500)
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp patch | blob | history

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index d924c0805bb17481a9193d169a7b5ca4d2454083..1b86afb85592516cc762219ce319525e7e3647ec 100644 (file)
--- 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)));
   }
 }