diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2020-10-03 13:18:45 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-10-03 13:18:45 -0700 |
| commit | d662d3321a46aac61973f7a90341ea870c0b1171 (patch) | |
| tree | a4a310ecc188316e68a61af7536b23ba6fda8f75 /src | |
| parent | 856d806d362b81bbf5a692d15d31f0161467bbd1 (diff) | |
sygus-inst: Add more special BV values. (#5191)
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/sygus_inst.cpp | 22 |
1 files changed, 22 insertions, 0 deletions
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(), |