Global negate (#1466)

7 files changed, 342 insertions, 77 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 098fe4025..a6c58e281 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -401,6 +401,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/fun_def_engine.h \
 	theory/quantifiers/fun_def_process.cpp \
 	theory/quantifiers/fun_def_process.h \
+	theory/quantifiers/global_negate.cpp \
+	theory/quantifiers/global_negate.h \
 	theory/quantifiers/ho_trigger.cpp \
 	theory/quantifiers/ho_trigger.h \
 	theory/quantifiers/instantiate.cpp \
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index 27671fd82..2166f0add 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -58,6 +58,8 @@ option elimExtArithQuant --elim-ext-arith-quant bool :read-write :default true
  eliminate extended arithmetic symbols in quantified formulas
 option condRewriteQuant --cond-rewrite-quant bool :default true
  conditional rewriting of quantified formulas
+option globalNegate --global-negate bool :read-write :default false
+ do global negation of input formula
  
 #### E-matching options
  
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 9b4837d43..b3eaec1fd 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -95,6 +95,7 @@
 #include "theory/logic_info.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/fun_def_process.h"
+#include "theory/quantifiers/global_negate.h"
 #include "theory/quantifiers/macros.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/single_inv_partition.h"
@@ -982,38 +983,39 @@ public:
 
 }/* namespace CVC4::smt */
 
-SmtEngine::SmtEngine(ExprManager* em) throw() :
-  d_context(new Context()),
-  d_userLevels(),
-  d_userContext(new UserContext()),
-  d_exprManager(em),
-  d_nodeManager(d_exprManager->getNodeManager()),
-  d_decisionEngine(NULL),
-  d_theoryEngine(NULL),
-  d_propEngine(NULL),
-  d_proofManager(NULL),
-  d_definedFunctions(NULL),
-  d_fmfRecFunctionsDefined(NULL),
-  d_assertionList(NULL),
-  d_assignments(NULL),
-  d_modelGlobalCommands(),
-  d_modelCommands(NULL),
-  d_dumpCommands(),
-  d_defineCommands(),
-  d_logic(),
-  d_originalOptions(),
-  d_pendingPops(0),
-  d_fullyInited(false),
-  d_problemExtended(false),
-  d_queryMade(false),
-  d_needPostsolve(false),
-  d_earlyTheoryPP(true),
-  d_status(),
-  d_replayStream(NULL),
-  d_private(NULL),
-  d_statisticsRegistry(NULL),
-  d_stats(NULL),
-  d_channels(new LemmaChannels())
+SmtEngine::SmtEngine(ExprManager* em) throw()
+    : d_context(new Context()),
+      d_userLevels(),
+      d_userContext(new UserContext()),
+      d_exprManager(em),
+      d_nodeManager(d_exprManager->getNodeManager()),
+      d_decisionEngine(NULL),
+      d_theoryEngine(NULL),
+      d_propEngine(NULL),
+      d_proofManager(NULL),
+      d_definedFunctions(NULL),
+      d_fmfRecFunctionsDefined(NULL),
+      d_assertionList(NULL),
+      d_assignments(NULL),
+      d_modelGlobalCommands(),
+      d_modelCommands(NULL),
+      d_dumpCommands(),
+      d_defineCommands(),
+      d_logic(),
+      d_originalOptions(),
+      d_pendingPops(0),
+      d_fullyInited(false),
+      d_problemExtended(false),
+      d_queryMade(false),
+      d_needPostsolve(false),
+      d_earlyTheoryPP(true),
+      d_globalNegation(false),
+      d_status(),
+      d_replayStream(NULL),
+      d_private(NULL),
+      d_statisticsRegistry(NULL),
+      d_stats(NULL),
+      d_channels(new LemmaChannels())
 {
   SmtScope smts(this);
   d_originalOptions.copyValues(em->getOptions());
@@ -1434,6 +1436,17 @@ void SmtEngine::setDefaults() {
       Notice() << "SmtEngine: turning off repeat-simp to support unsat-cores" << endl;
       setOption("repeat-simp", false);
     }
+
+    if (options::globalNegate())
+    {
+      if (options::globalNegate.wasSetByUser())
+      {
+        throw OptionException("global-negate not supported with unsat cores");
+      }
+      Notice() << "SmtEngine: turning off global-negate to support unsat-cores"
+               << endl;
+      setOption("global-negate", false);
+    }
   }
 
   if (options::cbqiBv()) {
@@ -1743,6 +1756,7 @@ void SmtEngine::setDefaults() {
     options::sortInference.set( false );
     options::ufssFairnessMonotone.set( false );
     options::quantEpr.set( false );
+    options::globalNegate.set(false);
   }
   if( d_logic.hasCardinalityConstraints() ){
     //must have finite model finding on
@@ -1931,7 +1945,8 @@ void SmtEngine::setDefaults() {
     if( !options::rewriteDivk.wasSetByUser()) {
       options::rewriteDivk.set( true );
     }
-    if( d_logic.isPure(THEORY_ARITH) ){
+    if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
+    {
       options::cbqiAll.set( false );
       if( !options::quantConflictFind.wasSetByUser() ){
         options::quantConflictFind.set( false );
@@ -1945,9 +1960,23 @@ void SmtEngine::setDefaults() {
       }
     }else{
       // only supported in pure arithmetic or pure BV
-      if (!d_logic.isPure(THEORY_BV))
+      options::cbqiNestedQE.set(false);
+    }
+    // prenexing
+    if (options::cbqiNestedQE()
+        || options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL)
+    {
+      // only complete with prenex = disj_normal or normal
+      if (options::prenexQuant() <= quantifiers::PRENEX_QUANT_DISJ_NORMAL)
       {
-        options::cbqiNestedQE.set(false);
+        options::prenexQuant.set(quantifiers::PRENEX_QUANT_DISJ_NORMAL);
+      }
+    }
+    else if (options::globalNegate())
+    {
+      if (!options::prenexQuant.wasSetByUser())
+      {
+        options::prenexQuant.set(quantifiers::PRENEX_QUANT_NONE);
       }
     }
   }
@@ -1960,13 +1989,6 @@ void SmtEngine::setDefaults() {
   if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
     options::quantConflictFind.set( true );
   }
-  if( options::cbqi() && 
-      ( options::cbqiNestedQE() || options::decisionMode()==decision::DECISION_STRATEGY_INTERNAL ) ){
-    //only complete with prenex = disj_normal or normal
-    if( options::prenexQuant()<=quantifiers::PRENEX_QUANT_DISJ_NORMAL ){
-      options::prenexQuant.set( quantifiers::PRENEX_QUANT_DISJ_NORMAL );
-    }
-  }
   if( options::cbqiNestedQE() ){
     options::prenexQuantUser.set( true );
     if( !options::preSkolemQuant.wasSetByUser() ){
@@ -2057,26 +2079,40 @@ void SmtEngine::setDefaults() {
   }
 
   // Non-linear arithmetic does not support models unless nlExt is enabled
-  if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear() && !options::nlExt() ) {
+  if ((d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()
+       && !options::nlExt())
+      || options::globalNegate())
+  {
+    std::string reason =
+        options::globalNegate() ? "--global-negate" : "nonlinear arithmetic";
     if (options::produceModels()) {
       if(options::produceModels.wasSetByUser()) {
-        throw OptionException("produce-model not supported with nonlinear arith");
+        throw OptionException(
+            std::string("produce-model not supported with " + reason));
       }
-      Warning() << "SmtEngine: turning off produce-models because unsupported for nonlinear arith" << endl;
+      Warning()
+          << "SmtEngine: turning off produce-models because unsupported for "
+          << reason << endl;
       setOption("produce-models", SExpr("false"));
     }
     if (options::produceAssignments()) {
       if(options::produceAssignments.wasSetByUser()) {
-        throw OptionException("produce-assignments not supported with nonlinear arith");
+        throw OptionException(
+            std::string("produce-assignments not supported with " + reason));
       }
-      Warning() << "SmtEngine: turning off produce-assignments because unsupported for nonlinear arith" << endl;
+      Warning() << "SmtEngine: turning off produce-assignments because "
+                   "unsupported for "
+                << reason << endl;
       setOption("produce-assignments", SExpr("false"));
     }
     if (options::checkModels()) {
       if(options::checkModels.wasSetByUser()) {
-        throw OptionException("check-models not supported with nonlinear arith");
+        throw OptionException(
+            std::string("check-models not supported with " + reason));
       }
-      Warning() << "SmtEngine: turning off check-models because unsupported for nonlinear arith" << endl;
+      Warning()
+          << "SmtEngine: turning off check-models because unsupported for "
+          << reason << endl;
       setOption("check-models", SExpr("false"));
     }
   }
@@ -4170,6 +4206,14 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
+  // global negation of the formula
+  if (options::globalNegate())
+  {
+    quantifiers::GlobalNegate gn;
+    gn.simplify(d_assertions.ref());
+    d_smt.d_globalNegation = !d_smt.d_globalNegation;
+  }
+
   if( options::nlExtPurify() ){
     unordered_map<Node, Node, NodeHashFunction> cache;
     unordered_map<Node, Node, NodeHashFunction> bcache;
@@ -4660,6 +4704,9 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ
     // Note that a query has been made
     d_queryMade = true;
 
+    // reset global negation
+    d_globalNegation = false;
+
     // Add the formula
     if(!e.isNull()) {
       d_problemExtended = true;
@@ -4676,6 +4723,28 @@ Result SmtEngine::checkSatisfiability(const Expr& ex, bool inUnsatCore, bool isQ
     if ( ( options::solveRealAsInt() || options::solveIntAsBV() > 0 ) && r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
       r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
     }
+    // flipped if we did a global negation
+    if (d_globalNegation)
+    {
+      Trace("smt") << "SmtEngine::process global negate " << r << std::endl;
+      if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
+      {
+        r = Result(Result::SAT);
+      }
+      else if (r.asSatisfiabilityResult().isSat() == Result::SAT)
+      {
+        // only if satisfaction complete
+        if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
+        {
+          r = Result(Result::UNSAT);
+        }
+        else
+        {
+          r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
+        }
+      }
+      Trace("smt") << "SmtEngine::global negate returned " << r << std::endl;
+    }
 
     d_needPostsolve = true;
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c628a1952..6d648ccda 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -241,6 +241,11 @@ class CVC4_PUBLIC SmtEngine {
    */
   bool d_earlyTheoryPP;
 
+  /*
+   * Whether we did a global negation of the formula.
+   */
+  bool d_globalNegation;
+
   /**
    * Most recent result of last checkSat/query or (set-info :status).
    */
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 */