Global negate (#1466)

3 files changed, 215 insertions, 28 deletions

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 8313abd68..0e1dc62e1 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4878,47 +4878,71 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
 
   switch(node.getKind()) {
   case kind::DIVISION: {
-    // 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);
-    }
     TNode num = node[0], den = node[1];
-    Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-    Node divByZeroNum = nm->mkNode(kind::APPLY_UF, d_divByZero, num);
-    Node divTotalNumDen = nm->mkNode(kind::DIVISION_TOTAL, num, den);
-    return nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen);
+    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 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;
     break;
   }
 
   case kind::INTS_DIVISION: {
     // partial function: integer div
-    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);
-    }
     TNode num = node[0], den = node[1];
-    Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-    Node intDivByZeroNum = nm->mkNode(kind::APPLY_UF, d_intDivByZero, num);
-    Node intDivTotalNumDen = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
-    return nm->mkNode(kind::ITE, den_eq_0, intDivByZeroNum, intDivTotalNumDen);
+    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 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;
     break;
   }
 
   case kind::INTS_MODULUS: {
     // partial function: mod
-    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);
-    }
     TNode num = node[0], den = node[1];
-    Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
-    Node modZeroNum = nm->mkNode(kind::APPLY_UF, d_modZero, num);
-    Node modTotalNumDen = nm->mkNode(kind::INTS_MODULUS_TOTAL, num, den);
-    return nm->mkNode(kind::ITE, den_eq_0, modZeroNum, modTotalNumDen);
+    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 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;
     break;
   }
 
diff --git a/src/theory/quantifiers/global_negate.cpp b/src/theory/quantifiers/global_negate.cpp
new file mode 100644
index 000000000..01925ec43
--- /dev/null
+++ b/src/theory/quantifiers/global_negate.cpp
@@ -0,0 +1,110 @@
+/*********************                                                        */
+/*! \file global_negate.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of global_negate
+ **/
+
+#include "theory/quantifiers/global_negate.h"
+#include "theory/rewriter.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+void GlobalNegate::simplify(std::vector<Node>& assertions)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Assert(!assertions.empty());
+
+  Trace("cbqi-gn") << "Global negate : " << std::endl;
+  // collect free variables in all assertions
+  std::vector<Node> free_vars;
+  std::vector<TNode> visit;
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  for (const Node& as : assertions)
+  {
+    Trace("cbqi-gn") << "  " << as << std::endl;
+    TNode cur = as;
+    // compute free variables
+    visit.push_back(cur);
+    do
+    {
+      cur = visit.back();
+      visit.pop_back();
+      if (visited.find(cur) == visited.end())
+      {
+        visited.insert(cur);
+        if (cur.isVar() && cur.getKind() != BOUND_VARIABLE)
+        {
+          free_vars.push_back(cur);
+        }
+        for (const TNode& cn : cur)
+        {
+          visit.push_back(cn);
+        }
+      }
+    } while (!visit.empty());
+  }
+
+  Node body;
+  if (assertions.size() == 1)
+  {
+    body = assertions[0];
+  }
+  else
+  {
+    body = nm->mkNode(AND, assertions);
+  }
+
+  // do the negation
+  body = body.negate();
+
+  if (!free_vars.empty())
+  {
+    std::vector<Node> bvs;
+    for (const Node& v : free_vars)
+    {
+      Node bv = nm->mkBoundVar(v.getType());
+      bvs.push_back(bv);
+    }
+
+    body = body.substitute(
+        free_vars.begin(), free_vars.end(), bvs.begin(), bvs.end());
+
+    Node bvl = nm->mkNode(BOUND_VAR_LIST, bvs);
+
+    body = nm->mkNode(FORALL, bvl, body);
+  }
+
+  Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl;
+  body = Rewriter::rewrite(body);
+  Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl;
+
+  Node truen = nm->mkConst(true);
+  for (unsigned i = 0, size = assertions.size(); i < size; i++)
+  {
+    if (i == 0)
+    {
+      assertions[i] = body;
+    }
+    else
+    {
+      assertions[i] = truen;
+    }
+  }
+}
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/quantifiers/global_negate.h b/src/theory/quantifiers/global_negate.h
new file mode 100644
index 000000000..814b0014c
--- /dev/null
+++ b/src/theory/quantifiers/global_negate.h
@@ -0,0 +1,53 @@
+/*********************                                                        */
+/*! \file global_negate.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief global_negate
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H
+#define __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H
+
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/** GlobalNegate
+ *
+ * This class updates a set of assertions to be equivalent to the negation of
+ * these assertions. In detail, if assertions is:
+ *    F1, ..., Fn
+ * then we update this vector to:
+ *    forall x1...xm. ~( F1 ^ ... ^ Fn ), true, ..., true
+ * where x1...xm are the free variables of F1...Fn.
+ */
+class GlobalNegate
+{
+ public:
+  GlobalNegate() {}
+  ~GlobalNegate() {}
+  /** simplify assertions
+   *
+   * Replaces assertions with a set of assertions that is equivalent to its
+   * negation.
+   */
+  void simplify(std::vector<Node>& assertions);
+};
+
+} /* CVC4::theory::quantifiers namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__QUANTIFIERS__GLOBAL_NEGATE_H */