diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-10-01 17:29:17 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-01 19:29:17 -0500 |
| commit | 86cc730908085942f4df19e3b24ebddc7557396f (patch) | |
| tree | 56c9f3e1b8a8cf016111eefa6a1645ebac0e7b64 /src/theory/quantifiers/sygus | |
| parent | 75d47fd5b65c3fe6dff3ef591d8331f737ca1cea (diff) | |
SyGuS: Add min/max (sub)normal constants to FP default grammar. (#5185)
Diffstat (limited to 'src/theory/quantifiers/sygus')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
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))); } } |