diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-17 02:48:22 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-17 00:48:22 -0700 |
commit | 29ae7d5ec0a73b90529e2200d948e6f4051099f1 (patch) | |
tree | a9dcb7074a2e79b35e17f2c4483638cf91ea1093 /src/theory/quantifiers | |
parent | 4d303b5e6de8a3b963357a3c0238ffe81d36f766 (diff) |
Eliminate partial operators in sygus grammar normalization (#2323)
This corrects a bug that was introduced in #2266 (the hack removed there was necessary).
This ensures that we handle operators like bvudiv, bvsdiv, bvurem, div, rem, / properly in sygus.
This also enables total semantics for BV div-by-zero for sygus.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_norm.cpp | 38 |
1 files changed, 37 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 8a415cc10..5a87c8ebd 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -74,8 +74,44 @@ void SygusGrammarNorm::TypeObject::addConsInfo(SygusGrammarNorm* sygus_norm, Trace("sygus-grammar-normalize") << "...for " << cons.getName() << "\n"; /* Recover the sygus operator to not lose reference to the original * operator (NOT, ITE, etc) */ + Node sygus_op = Node::fromExpr(cons.getSygusOp()); Node exp_sop_n = Node::fromExpr( - smt::currentSmtEngine()->expandDefinitions(cons.getSygusOp())); + smt::currentSmtEngine()->expandDefinitions(sygus_op.toExpr())); + if (exp_sop_n.getKind() == kind::BUILTIN) + { + Kind ok = NodeManager::operatorToKind(sygus_op); + Kind nk = ok; + Trace("sygus-grammar-normalize-debug") + << "...builtin operator is " << ok << std::endl; + // We also must ensure that builtin operators which are eliminated + // during expand definitions are replaced by the proper operator. + if (ok == kind::BITVECTOR_UDIV) + { + nk = kind::BITVECTOR_UDIV_TOTAL; + } + else if (ok == kind::BITVECTOR_UREM) + { + nk = kind::BITVECTOR_UREM_TOTAL; + } + else if (ok == kind::DIVISION) + { + nk = kind::DIVISION_TOTAL; + } + else if (ok == kind::INTS_DIVISION) + { + nk = kind::INTS_DIVISION_TOTAL; + } + else if (ok == kind::INTS_MODULUS) + { + nk = kind::INTS_MODULUS_TOTAL; + } + if (nk != ok) + { + Trace("sygus-grammar-normalize-debug") + << "...replace by builtin operator " << nk << std::endl; + exp_sop_n = NodeManager::currentNM()->operatorOf(nk); + } + } d_ops.push_back(Rewriter::rewrite(exp_sop_n)); Trace("sygus-grammar-normalize-defs") << "\tOriginal op: " << cons.getSygusOp() |