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.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 34a5a6d5b6cd3f7a981b83e15168b5de451cb1ee..418028d09f37b2e163bdb532f6c8cbf277282688 100644 (file)
--- 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 8a415cc10a79fed8c0e7718b3977b5194d87d721..5a87c8ebdc0911283405959bbcbb6583baf02fee 100644 (file)
--- 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 82f8f2c27eadf4f10680ef70b3e3b401c5dd46d9..e43f6675d79844074cb4764a63cfb26a7c8316ac 100644 (file)
--- 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 (file)
index 0000000..d649197
--- /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)