Merge branch 'master' into fixSetInfoNamefixSetInfoName

4 files changed, 301 insertions, 89 deletions

diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp
index 12c1c5c21..26785f15b 100644
--- a/src/preprocessing/passes/bv_ackermann.cpp
+++ b/src/preprocessing/passes/bv_ackermann.cpp
@@ -23,12 +23,9 @@
 
 #include "preprocessing/passes/bv_ackermann.h"
 
-#include "expr/node.h"
 #include "options/bv_options.h"
 #include "theory/bv/theory_bv_utils.h"
 
-#include <unordered_set>
-
 using namespace CVC4;
 using namespace CVC4::theory;
 
@@ -41,55 +38,142 @@ namespace passes {
 namespace
 {
 
-void storeFunction(
-    TNode func,
-    TNode term,
-    FunctionToArgsMap& fun_to_args,
-    SubstitutionMap& fun_to_skolem)
+void addLemmaForPair(TNode args1,
+                     TNode args2,
+                     const TNode func,
+                     AssertionPipeline* assertionsToPreprocess,
+                     NodeManager* nm)
 {
-  if (fun_to_args.find(func) == fun_to_args.end())
+  Node args_eq;
+
+  if (args1.getKind() == kind::APPLY_UF)
   {
-    fun_to_args.insert(make_pair(func, NodeSet()));
+    Assert(args1.getOperator() == func);
+    Assert(args2.getKind() == kind::APPLY_UF && args2.getOperator() == func);
+    Assert(args1.getNumChildren() == args2.getNumChildren());
+
+    std::vector<Node> eqs(args1.getNumChildren());
+
+    for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i)
+    {
+      eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
+    }
+    args_eq = bv::utils::mkAnd(eqs);
   }
-  NodeSet& set = fun_to_args[func];
-  if (set.find(term) == set.end())
+  else
   {
-    set.insert(term);
-    TypeNode tn = term.getType();
-    Node skolem = NodeManager::currentNM()->mkSkolem(
-        "BVSKOLEM$$",
-        tn,
-        "is a variable created by the ackermannization "
-        "preprocessing pass for theory BV");
-    fun_to_skolem.addSubstitution(term, skolem);
+    Assert(args1.getKind() == kind::SELECT && args1[0] == func);
+    Assert(args2.getKind() == kind::SELECT && args2[0] == func);
+    Assert(args1.getNumChildren() == 2);
+    Assert(args2.getNumChildren() == 2);
+    args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]);
   }
+  Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
+  Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
+  assertionsToPreprocess->push_back(lemma);
 }
 
-void collectFunctionSymbols(
-    TNode term,
-    FunctionToArgsMap& fun_to_args,
-    SubstitutionMap& fun_to_skolem,
-    std::unordered_set<TNode, TNodeHashFunction>& seen)
+void storeFunctionAndAddLemmas(TNode func,
+                               TNode term,
+                               FunctionToArgsMap& fun_to_args,
+                               SubstitutionMap& fun_to_skolem,
+                               AssertionPipeline* assertions,
+                               NodeManager* nm,
+                               std::vector<TNode>* vec)
 {
-  if (seen.find(term) != seen.end()) return;
-  if (term.getKind() == kind::APPLY_UF)
-  {
-    storeFunction(term.getOperator(), term, fun_to_args, fun_to_skolem);
-  }
-  else if (term.getKind() == kind::SELECT)
+  if (fun_to_args.find(func) == fun_to_args.end())
   {
-    storeFunction(term[0], term, fun_to_args, fun_to_skolem);
+    fun_to_args.insert(make_pair(func, TNodeSet()));
   }
-  else
+  TNodeSet& set = fun_to_args[func];
+  if (set.find(term) == set.end())
   {
-    AlwaysAssert(term.getKind() != kind::STORE,
-                 "Cannot use eager bitblasting on QF_ABV formula with stores");
+    TypeNode tn = term.getType();
+    Node skolem = nm->mkSkolem("BVSKOLEM$$",
+                               tn,
+                               "is a variable created by the ackermannization "
+                               "preprocessing pass for theory BV");
+    for (const auto& t : set)
+    {
+      addLemmaForPair(t, term, func, assertions, nm);
+    }
+    fun_to_skolem.addSubstitution(term, skolem);
+    set.insert(term);
+    /* Add the arguments of term (newest element in set) to the vector, so that
+     * collectFunctionsAndLemmas will process them as well.
+     * This is only needed if the set has at least two elements
+     * (otherwise, no lemma is generated).
+     * Therefore, we defer this for term in case it is the first element in the
+     * set*/
+    if (set.size() == 2)
+    {
+      for (TNode elem : set)
+      {
+        vec->insert(vec->end(), elem.begin(), elem.end());
+      }
+    }
+    else if (set.size() > 2)
+    {
+      vec->insert(vec->end(), term.begin(), term.end());
+    }
   }
-  for (const TNode& n : term)
+}
+
+/* We only add top-level applications of functions.
+ * For example: when we see "f(g(x))", we do not add g as a function and x as a
+ * parameter.
+ * Instead, we only include f as a function and g(x) as a parameter.
+ * However, if we see g(x) later on as a top-level application, we will add it
+ * as well.
+ * Another example: for the formula f(g(x))=f(g(y)),
+ * we first only add f as a function and g(x),g(y) as arguments.
+ * storeFunctionAndAddLemmas will then add the constraint g(x)=g(y) ->
+ * f(g(x))=f(g(y)).
+ * Now that we see g(x) and g(y), we explicitly add them as well. */
+void collectFunctionsAndLemmas(FunctionToArgsMap& fun_to_args,
+                               SubstitutionMap& fun_to_skolem,
+                               std::vector<TNode>* vec,
+                               AssertionPipeline* assertions)
+{
+  TNodeSet seen;
+  NodeManager* nm = NodeManager::currentNM();
+  TNode term;
+  while (!vec->empty())
   {
-    collectFunctionSymbols(n, fun_to_args, fun_to_skolem, seen);
+    term = vec->back();
+    vec->pop_back();
+    if (seen.find(term) == seen.end())
+    {
+      TNode func;
+      if (term.getKind() == kind::APPLY_UF)
+      {
+        storeFunctionAndAddLemmas(term.getOperator(),
+                                  term,
+                                  fun_to_args,
+                                  fun_to_skolem,
+                                  assertions,
+                                  nm,
+                                  vec);
+      }
+      else if (term.getKind() == kind::SELECT)
+      {
+        storeFunctionAndAddLemmas(
+            term[0], term, fun_to_args, fun_to_skolem, assertions, nm, vec);
+      }
+      else
+      {
+        AlwaysAssert(
+            term.getKind() != kind::STORE,
+            "Cannot use eager bitblasting on QF_ABV formula with stores");
+        /* add children to the vector, so that they are processed later */
+        for (TNode n : term)
+        {
+          vec->push_back(n);
+        }
+      }
+      seen.insert(term);
+    }
   }
-  seen.insert(term);
 }
 
 }  // namespace
@@ -108,57 +192,15 @@ PreprocessingPassResult BVAckermann::applyInternal(
   Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER);
   AlwaysAssert(!options::incrementalSolving());
 
-  std::unordered_set<TNode, TNodeHashFunction> seen;
-
+  /* collect all function applications and generate consistency lemmas
+   * accordingly */
+  std::vector<TNode> to_process;
   for (const Node& a : assertionsToPreprocess->ref())
   {
-    collectFunctionSymbols(a, d_funcToArgs, d_funcToSkolem, seen);
-  }
-
-  NodeManager* nm = NodeManager::currentNM();
-  for (const auto& p : d_funcToArgs)
-  {
-    TNode func = p.first;
-    const NodeSet& args = p.second;
-    NodeSet::const_iterator it1 = args.begin();
-    for (; it1 != args.end(); ++it1)
-    {
-      for (NodeSet::const_iterator it2 = it1; it2 != args.end(); ++it2)
-      {
-        TNode args1 = *it1;
-        TNode args2 = *it2;
-        Node args_eq;
-
-        if (args1.getKind() == kind::APPLY_UF)
-        {
-          AlwaysAssert(args1.getKind() == kind::APPLY_UF
-                       && args1.getOperator() == func);
-          AlwaysAssert(args2.getKind() == kind::APPLY_UF
-                       && args2.getOperator() == func);
-          AlwaysAssert(args1.getNumChildren() == args2.getNumChildren());
-
-          std::vector<Node> eqs(args1.getNumChildren());
-
-          for (unsigned i = 0, n = args1.getNumChildren(); i < n; ++i)
-          {
-            eqs[i] = nm->mkNode(kind::EQUAL, args1[i], args2[i]);
-          }
-          args_eq = bv::utils::mkAnd(eqs);
-        }
-        else
-        {
-          AlwaysAssert(args1.getKind() == kind::SELECT && args1[0] == func);
-          AlwaysAssert(args2.getKind() == kind::SELECT && args2[0] == func);
-          AlwaysAssert(args1.getNumChildren() == 2);
-          AlwaysAssert(args2.getNumChildren() == 2);
-          args_eq = nm->mkNode(kind::EQUAL, args1[1], args2[1]);
-        }
-        Node func_eq = nm->mkNode(kind::EQUAL, args1, args2);
-        Node lemma = nm->mkNode(kind::IMPLIES, args_eq, func_eq);
-        assertionsToPreprocess->push_back(lemma);
-      }
-    }
+    to_process.push_back(a);
   }
+  collectFunctionsAndLemmas(
+      d_funcToArgs, d_funcToSkolem, &to_process, assertionsToPreprocess);
 
   /* replace applications of UF by skolems */
   // FIXME for model building, github issue #1901
diff --git a/src/preprocessing/passes/bv_ackermann.h b/src/preprocessing/passes/bv_ackermann.h
index 197e92178..5f799ffe4 100644
--- a/src/preprocessing/passes/bv_ackermann.h
+++ b/src/preprocessing/passes/bv_ackermann.h
@@ -26,16 +26,18 @@
 #ifndef __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
 #define __CVC4__PREPROCESSING__PASSES__BV_ACKERMANN_H
 
+#include <unordered_map>
+#include "expr/node.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 
-#include <unordered_map>
-
 namespace CVC4 {
 namespace preprocessing {
 namespace passes {
 
-typedef std::unordered_map<Node, NodeSet, NodeHashFunction> FunctionToArgsMap;
+using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>;
+using FunctionToArgsMap =
+    std::unordered_map<TNode, TNodeSet, TNodeHashFunction>;
 
 class BVAckermann : public PreprocessingPass
 {
diff --git a/src/preprocessing/passes/global_negate.cpp b/src/preprocessing/passes/global_negate.cpp
new file mode 100644
index 000000000..ddebf961f
--- /dev/null
+++ b/src/preprocessing/passes/global_negate.cpp
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/*! \file global_negate.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 "preprocessing/passes/global_negate.h"
+#include <vector>
+#include "expr/node.h"
+#include "theory/rewriter.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm)
+{
+  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;
+  return body;
+}
+
+GlobalNegate::GlobalNegate(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "global-negate"){};
+
+PreprocessingPassResult GlobalNegate::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Node simplifiedNode = simplify(assertionsToPreprocess->ref(), nm);
+  Node trueNode = nm->mkConst(true);
+  for (unsigned i = 0; i < assertionsToPreprocess->size(); ++i)
+  {
+    assertionsToPreprocess->replace(i, trueNode);
+  }
+  assertionsToPreprocess->push_back(simplifiedNode);
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h
new file mode 100644
index 000000000..0330aa10e
--- /dev/null
+++ b/src/preprocessing/passes/global_negate.h
@@ -0,0 +1,52 @@
+/*********************                                                        */
+/*! \file global_negate.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 the global_negate preprocessing pass
+  * Updates a set of assertions 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.
+ * When this is done, d_globalNegation flag is marked, so that the solver checks
+ *for unsat instead of sat.
+**/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
+#define __CVC4__PREPROCESSING__PASSES__GLOBAL_NEGATE_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class GlobalNegate : public PreprocessingPass
+{
+ public:
+  GlobalNegate(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  Node simplify(std::vector<Node>& assertions, NodeManager* nm);
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING_PASSES__GLOBAL_NEGATE_H */