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: [PATCH]  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.
---
 src/smt/smt_engine.cpp                        |  6 ++-
 .../quantifiers/sygus/sygus_grammar_norm.cpp  | 38 ++++++++++++++++++-
 test/regress/Makefile.tests                   |  1 +
 test/regress/regress1/sygus/bvudiv-by-2.sy    | 27 +++++++++++++
 4 files changed, 70 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress1/sygus/bvudiv-by-2.sy

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 34a5a6d5b..418028d09 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1216,8 +1216,12 @@ void SmtEngine::setDefaults() {
   // Language-based defaults
   if (!options::bitvectorDivByZeroConst.wasSetByUser())
   {
+    // Bitvector-divide-by-zero changed semantics in SMT LIB 2.6, thus we
+    // set this option if the input format is SMT LIB 2.6. We also set this
+    // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus.
     options::bitvectorDivByZeroConst.set(
-        language::isInputLang_smt2_6(options::inputLanguage()));
+        language::isInputLang_smt2_6(options::inputLanguage())
+        || options::inputLanguage() == language::input::LANG_SYGUS);
   }
   bool is_sygus = false;
   if (options::inputLanguage() == language::input::LANG_SYGUS)
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()
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 82f8f2c27..e43f6675d 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1509,6 +1509,7 @@ REG1_TESTS = \
 	regress1/sygus/array_search_2.sy \
 	regress1/sygus/array_search_5-Q-easy.sy \
 	regress1/sygus/array_sum_2_5.sy \
+	regress1/sygus/bvudiv-by-2.sy \
 	regress1/sygus/cegar1.sy \
 	regress1/sygus/cegisunif-depth1.sy \
 	regress1/sygus/cegis-unif-inv-eq-fair.sy \
diff --git a/test/regress/regress1/sygus/bvudiv-by-2.sy b/test/regress/regress1/sygus/bvudiv-by-2.sy
new file mode 100644
index 000000000..d6491972a
--- /dev/null
+++ b/test/regress/regress1/sygus/bvudiv-by-2.sy
@@ -0,0 +1,27 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic BV)
+
+(synth-fun f ((x (BitVec 32))) (BitVec 32) 
+((Start (BitVec 32)
+   (
+             (bvudiv Start Start)
+             (bvurem Start Start)
+             (bvsdiv Start Start)
+             #x00000001
+             #x00000000
+             #x00000002 x
+             (ite StartBool Start Start)))
+    (StartBool Bool (( bvult Start Start)
+    			(bvugt Start Start)
+    			(= Start Start)
+             ))))
+(declare-var x (BitVec 32) )
+
+; property
+(constraint (= (f #x00000008) #x00000004))
+(constraint (= (f #x00000010) #x00000008))
+(constraint (not (= (f x) #xffffffff)))
+
+
+(check-synth)
-- 
2.30.2