From 29ae7d5ec0a73b90529e2200d948e6f4051099f1 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 17 Aug 2018 02:48:22 -0500
Subject:  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.
---
 .../quantifiers/sygus/sygus_grammar_norm.cpp       | 38 +++++++++++++++++++++-
 1 file changed, 37 insertions(+), 1 deletion(-)

(limited to 'src/theory/quantifiers')

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()
-- 
cgit v1.2.3