Option to not use partial function semantics for arithmetic div by zero (#1620)

3 files changed, 100 insertions, 45 deletions

diff --git a/src/options/arith_options b/src/options/arith_options
index e6f7fd6d0..722af1fa1 100644
--- a/src/options/arith_options
+++ b/src/options/arith_options
@@ -155,6 +155,8 @@ option ppAssertMaxSubSize --pp-assert-max-sub-size unsigned :default 2
 option maxReplayTree --max-replay-tree int :default 512
  threshold for attempting to replay a tree
 
+option arithNoPartialFun --arith-no-partial-fun bool :default false
+ do not use partial function semantics for arithmetic (not SMT LIB compliant)
 
 option pbRewrites --pb-rewrites bool :default false
  apply pseudo boolean rewrites
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index da17dd2f5..a990e008c 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4902,18 +4902,9 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
       Node ret = nm->mkNode(kind::DIVISION_TOTAL, num, den);
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
-        // partial function: division
-        if (d_divByZero.isNull())
-        {
-          d_divByZero =
-              nm->mkSkolem("divByZero",
-                           nm->mkFunctionType(nm->realType(), nm->realType()),
-                           "partial real division",
-                           NodeManager::SKOLEM_EXACT_NAME);
-          logicRequest.widenLogic(THEORY_UF);
-        }
+        Node divByZeroNum =
+            getArithSkolemApp(logicRequest, num, arith_skolem_div_by_zero);
         Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-        Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num);
         ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret);
       }
       return ret;
@@ -4927,17 +4918,9 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
       Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
-        if (d_intDivByZero.isNull())
-        {
-          d_intDivByZero = nm->mkSkolem(
-              "intDivByZero",
-              nm->mkFunctionType(nm->integerType(), nm->integerType()),
-              "partial integer division",
-              NodeManager::SKOLEM_EXACT_NAME);
-          logicRequest.widenLogic(THEORY_UF);
-        }
+        Node intDivByZeroNum =
+            getArithSkolemApp(logicRequest, num, arith_skolem_int_div_by_zero);
         Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-        Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num);
         ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret);
       }
       return ret;
@@ -4951,17 +4934,9 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
       Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den);
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
-        if (d_modZero.isNull())
-        {
-          d_modZero = nm->mkSkolem(
-              "modZero",
-              nm->mkFunctionType(nm->integerType(), nm->integerType()),
-              "partial modulus",
-              NodeManager::SKOLEM_EXACT_NAME);
-          logicRequest.widenLogic(THEORY_UF);
-        }
+        Node modZeroNum =
+            getArithSkolemApp(logicRequest, num, arith_skolem_mod_by_zero);
         Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-        Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num);
         ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret);
       }
       return ret;
@@ -5062,8 +5037,68 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
   Unreachable();
 }
 
+Node TheoryArithPrivate::getArithSkolem(LogicRequest& logicRequest,
+                                        ArithSkolemId asi)
+{
+  std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi);
+  if (it == d_arith_skolem.end())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+
+    TypeNode tn;
+    std::string name;
+    std::string desc;
+    if (asi == arith_skolem_div_by_zero)
+    {
+      tn = nm->realType();
+      name = std::string("divByZero");
+      desc = std::string("partial real division");
+    }
+    else if (asi == arith_skolem_int_div_by_zero)
+    {
+      tn = nm->integerType();
+      name = std::string("intDivByZero");
+      desc = std::string("partial int division");
+    }
+    else if (asi == arith_skolem_mod_by_zero)
+    {
+      tn = nm->integerType();
+      name = std::string("modZero");
+      desc = std::string("partial modulus");
+    }
 
+    Node skolem;
+    if (options::arithNoPartialFun())
+    {
+      // partial function: division
+      skolem = nm->mkSkolem(name, tn, desc, NodeManager::SKOLEM_EXACT_NAME);
+    }
+    else
+    {
+      // partial function: division
+      skolem = nm->mkSkolem(name,
+                            nm->mkFunctionType(tn, tn),
+                            desc,
+                            NodeManager::SKOLEM_EXACT_NAME);
+      logicRequest.widenLogic(THEORY_UF);
+    }
+    d_arith_skolem[asi] = skolem;
+    return skolem;
+  }
+  return it->second;
+}
 
+Node TheoryArithPrivate::getArithSkolemApp(LogicRequest& logicRequest,
+                                           Node n,
+                                           ArithSkolemId asi)
+{
+  Node skolem = getArithSkolem(logicRequest, asi);
+  if (!options::arithNoPartialFun())
+  {
+    skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
+  }
+  return skolem;
+}
 
 // InferBoundsResult TheoryArithPrivate::inferBound(TNode term, const InferBoundsParameters& param){
 //   Node t = Rewriter::rewrite(term);
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 23712016d..af0012304 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -829,25 +829,43 @@ private:
 
   Statistics d_statistics;
 
+  enum ArithSkolemId
+  {
+    arith_skolem_div_by_zero,
+    arith_skolem_int_div_by_zero,
+    arith_skolem_mod_by_zero,
+  };
 
   /**
-   * Function symbol used to implement uninterpreted division-by-zero
-   * semantics.  Needed to deal with partial division function ("/").
+   * Function symbols used to implement:
+   * (1) Uninterpreted division-by-zero semantics.  Needed to deal with partial
+   * division function ("/"),
+   * (2) Uninterpreted int-division-by-zero semantics.  Needed to deal with
+   * partial function "div",
+   * (3) Uninterpreted mod-zero semantics.  Needed to deal with partial
+   * function "mod".
+   *
+   * If the option arithNoPartialFun() is enabled, then the range of this map
+   * stores Skolem constants instead of Skolem functions, meaning that the
+   * function-ness of e.g. division by zero is ignored.
    */
-  Node d_divByZero;
-
-  /**
-   * Function symbol used to implement uninterpreted
-   * int-division-by-zero semantics.  Needed to deal with partial
-   * function "div".
+  std::map<ArithSkolemId, Node> d_arith_skolem;
+  /** get arithmetic skolem
+   *
+   * Returns the Skolem in the above map for the given id, creating it if it
+   * does not already exist. If a Skolem function is created, the logic is
+   * widened to include UF.
    */
-  Node d_intDivByZero;
-
-  /**
-   * Function symbol used to implement uninterpreted mod-zero
-   * semantics.  Needed to deal with partial function "mod".
+  Node getArithSkolem(LogicRequest& logicRequest, ArithSkolemId asi);
+  /** get arithmetic skolem application
+   *
+   * By default, this returns the term f( n ), where f is the Skolem function
+   * for the identifier asi.
+   *
+   * If the option arithNoPartialFun is enabled, this returns f, where f is
+   * the Skolem constant for the identifier asi.
    */
-  Node d_modZero;
+  Node getArithSkolemApp(LogicRequest& logicRequest, Node n, ArithSkolemId asi);
 
   /**
    *  Maps for Skolems for to-integer, real/integer div-by-k, and inverse