From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Sat, 3 Oct 2020 20:18:45 +0000 (-0700)
Subject: sygus-inst: Add more special BV values. (#5191)
X-Git-Tag: cvc5-1.0.0~2758
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d662d3321a46aac61973f7a90341ea870c0b1171;p=cvc5.git

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 4192ca746..e2aeee1b6 100644
--- 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(),