sygus-inst: Add more special BV values. (#5191)

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 4192ca746c5341eaabb4566aa752c4160a932ee5..e2aeee1b69b4490b33a71df901085a2303fd532a 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -18,6 +18,7 @@
 #include <unordered_set>
 
 #include "expr/node_algorithm.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/sygus_enumerator.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
@@ -157,6 +158,26 @@ void getMinGroundTerms(
   } while (!visit.empty());
 }
 
+/*
+ * Add special values for a given type.
+ *
+ * @param tn: The type node.
+ * @param extra_cons: A map of TypeNode to constants, which are added in
+ *                    addition to the default grammar.
+ */
+void addSpecialValues(
+    const TypeNode& tn,
+    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& extra_cons)
+{
+  if (tn.isBitVector())
+  {
+    uint32_t size = tn.getBitVectorSize();
+    extra_cons[tn].insert(bv::utils::mkOnes(size));
+    extra_cons[tn].insert(bv::utils::mkMinSigned(size));
+    extra_cons[tn].insert(bv::utils::mkMaxSigned(size));
+  }
+}
+
 }  // namespace
 
 SygusInst::SygusInst(QuantifiersEngine* qe)
@@ -361,6 +382,7 @@ void SygusInst::registerQuantifier(Node q)
   std::vector<TypeNode> types;
   for (const Node& var : q[0])
   {
+    addSpecialValues(var.getType(), extra_cons);
     TypeNode tn = CegGrammarConstructor::mkSygusDefaultType(var.getType(),
                                                             Node(),
                                                             var.toString(),