Merge branch 'master' into moveKindedmoveKinded

18 files changed, 571 insertions, 266 deletions

diff --git a/contrib/get-gmp b/contrib/get-gmp
new file mode 100755
index 000000000..02602e456
--- /dev/null
+++ b/contrib/get-gmp
@@ -0,0 +1,35 @@
+#!/bin/bash
+#
+# This script should only be used if your distribution does not ship with the
+# GMP configuration you need. For example, contrib/get-win-dependencies
+# cross-compiles GMP for Windows. You can also use the script if your
+# distribution does not ship with static GMP libraries (e.g., Arch Linux) and
+# you want to build CVC4 statically.
+# In most of the cases the GMP version installed on your system is the one you
+# want and should use.
+#
+
+source "$(dirname "$0")/get-script-header.sh"
+
+[ -z "${BUILD_TYPE}" ] && BUILD_TYPE="--disable-shared --enable-static"
+[ -n "$HOST" ] && HOST="--host=$HOST"
+[ -z "$GMPVERSION" ] && GMPVERSION=6.1.2
+
+echo =============================================================================
+echo
+echo "Setting up GMP $GMPVERSION..."
+echo
+( set -ex
+  mkdir gmp-$GMPVERSION
+  cd gmp-$GMPVERSION
+  gmpprefix=`pwd` &&
+  mkdir src &&
+  cd src &&
+  webget https://gmplib.org/download/gmp/gmp-$GMPVERSION.tar.bz2 gmp-$GMPVERSION.tar.bz2 &&
+  tar xfj gmp-$GMPVERSION.tar.bz2 &&
+  cd gmp-$GMPVERSION &&
+  ./configure ${HOST} --prefix="$gmpprefix" --enable-cxx ${BUILD_TYPE} &&
+  make CFLAGS="${MAKE_CFLAGS}" CXXFLAGS="${MAKE_CXXFLAGS}" LDFLAGS="${MAKE_LDFLAGS}" &&
+  make install
+) || exit 1
+echo
diff --git a/contrib/get-win-dependencies b/contrib/get-win-dependencies
index ee33391d7..5ca969f6b 100755
--- a/contrib/get-win-dependencies
+++ b/contrib/get-win-dependencies
@@ -74,23 +74,16 @@ echo
 MACHINE_TYPE="x86_64" ANTLR_CONFIGURE_ARGS="--host=$HOST" contrib/get-antlr-3.4 | grep -v 'Now configure CVC4 with' | grep -v '\./configure --with-antlr-dir='
 [ ${PIPESTATUS[0]} -eq 0 ] || reporterror
 echo
-echo =============================================================================
-echo
-echo "Setting up GMP $GMPVERSION..."
-echo
-( set -ex
-  mkdir gmp-$GMPVERSION
-  cd gmp-$GMPVERSION
-  gmpprefix=`pwd` &&
-  mkdir src &&
-  cd src &&
-  webget https://gmplib.org/download/gmp/gmp-$GMPVERSION.tar.bz2 gmp-$GMPVERSION.tar.bz2 &&
-  tar xfj gmp-$GMPVERSION.tar.bz2 &&
-  cd gmp-$GMPVERSION &&
-  ./configure --host=$HOST --prefix="$gmpprefix" --enable-cxx ${BUILD_TYPE} &&
-  make CFLAGS="${MAKE_CFLAGS}" CXXFLAGS="${MAKE_CXXFLAGS}" LDFLAGS="${MAKE_LDFLAGS}" &&
-  make install
-) || exit 1
+
+# Setup GMP
+HOST="$HOST" \
+BUILD_TYPE="$BUILD_TYPE" \
+MAKE_CFLAGS="$MAKE_CFLAGS" \
+MAKE_CXXFLAGS="$MAKE_CXXFLAGS" \
+MAKE_LDFLAGS="$MAKE_LDFLAGS" \
+GMPVERSION="$GMPVERSION" \
+  contrib/get-gmp || reporterror
+
 echo
 echo =============================================================================
 echo
diff --git a/src/Makefile.am b/src/Makefile.am
index 43aa70174..992f229d6 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -63,6 +63,8 @@ libcvc4_la_SOURCES = \
 	decision/justification_heuristic.h \
 	preprocessing/passes/apply_substs.cpp \
 	preprocessing/passes/apply_substs.h \
+	preprocessing/passes/apply_to_const.cpp \
+	preprocessing/passes/apply_to_const.h \
 	preprocessing/passes/bv_abstraction.cpp \
 	preprocessing/passes/bv_abstraction.h \
 	preprocessing/passes/bv_ackermann.cpp \
@@ -71,6 +73,8 @@ libcvc4_la_SOURCES = \
 	preprocessing/passes/bv_gauss.h \
 	preprocessing/passes/bv_intro_pow2.cpp \
 	preprocessing/passes/bv_intro_pow2.h \
+	preprocessing/passes/extended_rewriter_pass.cpp \
+	preprocessing/passes/extended_rewriter_pass.h \
 	preprocessing/passes/int_to_bv.cpp \
 	preprocessing/passes/int_to_bv.h \
 	preprocessing/passes/pseudo_boolean_processor.cpp \
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index aafe168ea..db6fb52a0 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -423,66 +423,23 @@ AttributeManager::setAttribute(NodeValue* nv,
   ah[std::make_pair(AttrKind::getId(), nv)] = mapping::convert(value);
 }
 
-/**
- * Search for the NodeValue in all attribute tables and remove it,
- * calling the cleanup function if one is defined.
- *
- * This cannot use nv as anything other than a pointer!
- */
+/** Search for the NodeValue in all attribute tables and remove it. */
 template <class T>
 inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
                                               NodeValue* nv) {
-  for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::getId(); ++id) {
-    typedef AttributeTraits<T, false> traits_t;
-    typedef AttrHash<T> hash_t;
-    std::pair<uint64_t, NodeValue*> pr = std::make_pair(id, nv);
-    if(traits_t::getCleanup()[id] != NULL) {
-      typename hash_t::iterator i = table.find(pr);
-      if(i != table.end()) {
-        traits_t::getCleanup()[id]((*i).second);
-        table.erase(pr);
-      }
-    } else {
-      table.erase(pr);
-    }
+  // This cannot use nv as anything other than a pointer!
+  const uint64_t last = attr::LastAttributeId<T, false>::getId();
+  for (uint64_t id = 0; id < last; ++id)
+  {
+    table.erase(std::make_pair(id, nv));
   }
 }
 
-/**
- * Remove all attributes from the table calling the cleanup function
- * if one is defined.
- */
+/** Remove all attributes from the table. */
 template <class T>
 inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
   Assert(!d_inGarbageCollection);
   d_inGarbageCollection = true;
-
-  bool anyRequireClearing = false;
-  typedef AttributeTraits<T, false> traits_t;
-  typedef AttrHash<T> hash_t;
-  for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::getId(); ++id) {
-    if(traits_t::getCleanup()[id] != NULL) {
-      anyRequireClearing = true;
-    }
-  }
-
-  if(anyRequireClearing) {
-    typename hash_t::iterator it = table.begin();
-    typename hash_t::iterator it_end = table.end();
-
-    while (it != it_end){
-      uint64_t id = (*it).first.first;
-      /*
-      Debug("attrgc") << "id " << id
-                      << " node_value: " << ((*it).first.second)
-                      << std::endl;
-      */
-      if(traits_t::getCleanup()[id] != NULL) {
-        traits_t::getCleanup()[id]((*it).second);
-      }
-      ++it;
-    }
-  }
   table.clear();
   d_inGarbageCollection = false;
   Assert(!d_inGarbageCollection);
@@ -499,7 +456,6 @@ AttributeUniqueId AttributeManager::getAttributeId(const AttrKind& attr){
 template <class T>
 void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){
   d_inGarbageCollection = true;
-  typedef AttributeTraits<T, false> traits_t;
   typedef AttrHash<T> hash_t;
 
   typename hash_t::iterator it = table.begin();
@@ -516,9 +472,6 @@ void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::
     if(std::binary_search(begin_ids, end_ids, id)){
       tmp = it;
       ++it;
-      if(traits_t::getCleanup()[id] != NULL) {
-        traits_t::getCleanup()[id]((*tmp).second);
-      }
       table.erase(tmp);
     }else{
       ++it;
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index ed1769740..e474c3dfb 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -332,45 +332,6 @@ public:
 
 }/* CVC4::expr::attr namespace */
 
-// ATTRIBUTE CLEANUP FUNCTIONS =================================================
-
-namespace attr {
-
-/** Default cleanup for unmanaged Attribute<> */
-struct NullCleanupStrategy {
-};/* struct NullCleanupStrategy */
-
-/**
- * Helper for Attribute<> class below to determine whether a cleanup
- * is defined or not.
- */
-template <class T, class C>
-struct getCleanupStrategy {
-  typedef T value_type;
-  typedef KindValueToTableValueMapping<value_type> mapping;
-  static void fn(typename mapping::table_value_type t) {
-    C::cleanup(mapping::convertBack(t));
-  }
-};/* struct getCleanupStrategy<> */
-
-/**
- * Specialization for NullCleanupStrategy.
- */
-template <class T>
-struct getCleanupStrategy<T, NullCleanupStrategy> {
-  typedef T value_type;
-  typedef KindValueToTableValueMapping<value_type> mapping;
-  static void (*const fn)(typename mapping::table_value_type);
-};/* struct getCleanupStrategy<T, NullCleanupStrategy> */
-
-// out-of-class initialization required (because it's a non-integral type)
-template <class T>
-void (*const getCleanupStrategy<T, NullCleanupStrategy>::fn)
-     (typename getCleanupStrategy<T, NullCleanupStrategy>::
-               mapping::table_value_type) = NULL;
-
-}/* CVC4::expr::attr namespace */
-
 // ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ====================================
 
 namespace attr {
@@ -381,39 +342,21 @@ namespace attr {
  */
 template <class T, bool context_dep>
 struct LastAttributeId {
-  static uint64_t& getId() {
-    static uint64_t s_id = 0;
-    return s_id;
+ public:
+  static uint64_t getNextId() {
+    uint64_t* id = raw_id();
+    const uint64_t next_id = *id;
+    ++(*id);
+    return next_id;
   }
-};
-
-}/* CVC4::expr::attr namespace */
-
-// ATTRIBUTE TRAITS ============================================================
-
-namespace attr {
-
-/**
- * This is the last-attribute-assigner.  IDs are not globally
- * unique; rather, they are unique for each table_value_type.
- */
-template <class T, bool context_dep>
-struct AttributeTraits {
-  typedef void (*cleanup_t)(T);
-  static std::vector<cleanup_t>& getCleanup() {
-    // Note: we do not destroy this vector on purpose. Instead, we rely on the
-    // OS to clean up our mess. The reason for that is that we need this vector
-    // to remain initialized at least as long as the ExprManager because
-    // ExprManager's destructor calls this method. The only way to guarantee
-    // this is to never destroy it. This is a common idiom [0]. In the past, we
-    // had an issue when `cleanup` wasn't a pointer and just an `std::vector`
-    // instead. CxxTest stores the test class in a static variable, which could
-    // lead to the ExprManager being destroyed after the destructor of the
-    // vector was called.
-    //
-    // [0] https://isocpp.org/wiki/faq/ctors#static-init-order-on-first-use
-    static std::vector<cleanup_t>* cleanup = new std::vector<cleanup_t>();
-    return *cleanup;
+  static uint64_t getId() {
+    return *raw_id();
+  }
+ private:
+  static uint64_t* raw_id()
+  {
+    static uint64_t s_id = 0;
+    return &s_id;
   }
 };
 
@@ -428,18 +371,12 @@ struct AttributeTraits {
  *
  * @param value_t the underlying value_type for the attribute kind
  *
- * @param CleanupStrategy Clean-up routine for associated values when the
- * Node goes away.  Useful, e.g., for pointer-valued attributes when
- * the values are "owned" by the table.
- *
  * @param context_dep whether this attribute kind is
  * context-dependent
  */
-template <class T,
-          class value_t,
-          class CleanupStrategy = attr::NullCleanupStrategy,
-          bool context_dep = false>
-class Attribute {
+template <class T, class value_t, bool context_dep = false>
+class Attribute
+{
   /**
    * The unique ID associated to this attribute.  Assigned statically,
    * at load time.
@@ -475,33 +412,16 @@ public:
   static inline uint64_t registerAttribute() {
     typedef typename attr::KindValueToTableValueMapping<value_t>::
                      table_value_type table_value_type;
-    typedef attr::AttributeTraits<table_value_type, context_dep> traits;
-    uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::getId()++;
-    Assert(traits::getCleanup().size() == id);// sanity check
-    traits::getCleanup().push_back(attr::getCleanupStrategy<value_t,
-                                                       CleanupStrategy>::fn);
-    return id;
+    return attr::LastAttributeId<table_value_type, context_dep>::getNextId();
   }
 };/* class Attribute<> */
 
 /**
- * An "attribute type" structure for boolean flags (special).  The
- * full one is below; the existence of this one disallows for boolean
- * flag attributes with a specialized cleanup function.
- */
-/* -- doesn't work; other specialization is "more specific" ??
-template <class T, class CleanupStrategy, bool context_dep>
-class Attribute<T, bool, CleanupStrategy, context_dep> {
-  template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions;
-  ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah;
-};
-*/
-
-/**
  * An "attribute type" structure for boolean flags (special).
  */
 template <class T, bool context_dep>
-class Attribute<T, bool, attr::NullCleanupStrategy, context_dep> {
+class Attribute<T, bool, context_dep>
+{
   /** IDs for bool-valued attributes are actually bit assignments. */
   static const uint64_t s_id;
 
@@ -538,7 +458,7 @@ public:
    * return the id.
    */
   static inline uint64_t registerAttribute() {
-    uint64_t id = attr::LastAttributeId<bool, context_dep>::getId()++;
+    const uint64_t id = attr::LastAttributeId<bool, context_dep>::getNextId();
     AlwaysAssert( id <= 63,
                   "Too many boolean node attributes registered "
                   "during initialization !" );
@@ -549,25 +469,15 @@ public:
 // ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
 
 /** Assign unique IDs to attributes at load time. */
-// Use of the comma-operator here forces instantiation (and
-// initialization) of the AttributeTraits<> structure and its
-// "cleanup" vector before registerAttribute() is called.  This is
-// important because otherwise the vector is initialized later,
-// clearing the first-pushed cleanup function.
-template <class T, class value_t, class CleanupStrategy, bool context_dep>
-const uint64_t Attribute<T, value_t, CleanupStrategy, context_dep>::s_id =
-  ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::
-                                   table_value_type,
-                          context_dep>::getCleanup().size(),
-    Attribute<T, value_t, CleanupStrategy, context_dep>::registerAttribute() );
+template <class T, class value_t, bool context_dep>
+const uint64_t Attribute<T, value_t, context_dep>::s_id =
+    Attribute<T, value_t,  context_dep>::registerAttribute();
+
 
 /** Assign unique IDs to attributes at load time. */
 template <class T, bool context_dep>
-const uint64_t Attribute<T,
-                         bool,
-                         attr::NullCleanupStrategy, context_dep>::s_id =
-  Attribute<T, bool, attr::NullCleanupStrategy, context_dep>::
-    registerAttribute();
+const uint64_t Attribute<T, bool, context_dep>::s_id =
+    Attribute<T, bool, context_dep>::registerAttribute();
 
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 8bbf905a9..7d1259fcc 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -128,10 +128,7 @@ class NodeManager {
    * contexts, like as a key in attribute tables), even though
    * normally it's an error to have a TNode to a node value with a
    * reference count of 0.  Being "under deletion" also enables
-   * assertions that inc() is not called on it.  (A poorly-behaving
-   * attribute cleanup function could otherwise create a "Node" that
-   * points to the node value that is in the process of being deleted,
-   * springing it back to life.)
+   * assertions that inc() is not called on it.
    */
   expr::NodeValue* d_nodeUnderDeletion;
 
diff --git a/src/preprocessing/passes/apply_to_const.cpp b/src/preprocessing/passes/apply_to_const.cpp
new file mode 100644
index 000000000..bbe4439ec
--- /dev/null
+++ b/src/preprocessing/passes/apply_to_const.cpp
@@ -0,0 +1,108 @@
+/*********************                                                        */
+/*! \file apply_to_const.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 ApplyToConst preprocessing pass
+ **
+ ** Rewrites applies to constants
+ **/
+
+#include "preprocessing/passes/apply_to_const.h"
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+ApplyToConst::ApplyToConst(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "apply-to-const"){};
+
+Node ApplyToConst::rewriteApplyToConst(TNode n, NodeMap& cache)
+{
+  Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n << std::endl;
+
+  if (n.getMetaKind() == kind::metakind::CONSTANT
+      || n.getMetaKind() == kind::metakind::VARIABLE
+      || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR)
+  {
+    return n;
+  }
+
+  if (cache.find(n) != cache.end())
+  {
+    Trace("rewriteApplyToConst") << "in cache :: " << cache[n] << std::endl;
+    return cache[n];
+  }
+
+  if (n.getKind() == kind::APPLY_UF)
+  {
+    if (n.getNumChildren() == 1 && n[0].isConst() && n[0].getType().isInteger())
+    {
+      stringstream ss;
+      ss << n.getOperator() << "_";
+      if (n[0].getConst<Rational>() < 0)
+      {
+        ss << "m" << -n[0].getConst<Rational>();
+      }
+      else
+      {
+        ss << n[0];
+      }
+      Node newvar =
+          NodeManager::currentNM()->mkSkolem(ss.str(),
+                                             n.getType(),
+                                             "rewriteApplyToConst skolem",
+                                             NodeManager::SKOLEM_EXACT_NAME);
+      cache[n] = newvar;
+      Trace("rewriteApplyToConst") << "made :: " << newvar << std::endl;
+      return newvar;
+    }
+    stringstream ss;
+    ss << "The rewrite-apply-to-const preprocessor is currently limited;\n"
+       << "it only works if all function symbols are unary and with Integer\n"
+       << "domain, and all applications are to integer values.\n"
+       << "Found application: " << n;
+    Unhandled(ss.str());
+  }
+
+  NodeBuilder<> builder(n.getKind());
+  if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+  {
+    builder << n.getOperator();
+  }
+  for (unsigned i = 0; i < n.getNumChildren(); ++i)
+  {
+    builder << rewriteApplyToConst(n[i], cache);
+  }
+  Node rewr = builder;
+  cache[n] = rewr;
+  Trace("rewriteApplyToConst") << "built :: " << rewr << std::endl;
+  return rewr;
+}
+
+PreprocessingPassResult ApplyToConst::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  NodeMap cache;
+  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+  {
+    assertionsToPreprocess->replace(i,
+                                    Rewriter::rewrite(rewriteApplyToConst(
+                                        (*assertionsToPreprocess)[i], cache)));
+  }
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/apply_to_const.h b/src/preprocessing/passes/apply_to_const.h
new file mode 100644
index 000000000..9d5072023
--- /dev/null
+++ b/src/preprocessing/passes/apply_to_const.h
@@ -0,0 +1,51 @@
+/*********************                                                        */
+/*! \file apply_to_const.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 ApplyToConst preprocessing pass
+ **
+ ** Rewrites applies to constants
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H
+#define __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H
+
+#include <unordered_map>
+
+#include "expr/node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+
+class ApplyToConst : public PreprocessingPass
+{
+ public:
+  ApplyToConst(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+ private:
+  Node rewriteApplyToConst(TNode n, NodeMap& cache);
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__APPLY_TO_CONST_H */
diff --git a/src/preprocessing/passes/extended_rewriter_pass.cpp b/src/preprocessing/passes/extended_rewriter_pass.cpp
new file mode 100644
index 000000000..572aaed7a
--- /dev/null
+++ b/src/preprocessing/passes/extended_rewriter_pass.cpp
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file extended_rewriter_pass.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 ExtRewPre preprocessing pass
+ **
+ ** Applies the extended rewriter to assertions
+ **/
+
+#include "preprocessing/passes/extended_rewriter_pass.h"
+
+#include "theory/quantifiers/extended_rewrite.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+ExtRewPre::ExtRewPre(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "ext-rew-pre"){};
+
+PreprocessingPassResult ExtRewPre::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg());
+  for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i)
+  {
+    assertionsToPreprocess->replace(
+        i, extr.extendedRewrite((*assertionsToPreprocess)[i]));
+  }
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/extended_rewriter_pass.h b/src/preprocessing/passes/extended_rewriter_pass.h
new file mode 100644
index 000000000..f604a1af5
--- /dev/null
+++ b/src/preprocessing/passes/extended_rewriter_pass.h
@@ -0,0 +1,43 @@
+/*********************                                                        */
+/*! \file extended_rewriter_pass.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Haniel Barbosa
+ ** 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 ExtRewPre preprocessing pass
+ **
+ ** Applies the extended rewriter to assertions
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
+#define __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class ExtRewPre : public PreprocessingPass
+{
+ public:
+  ExtRewPre(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__EXTENDED_REWRITER_PASS_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index db4efe89f..b5d758bca 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -70,12 +70,14 @@
 #include "options/theory_options.h"
 #include "options/uf_options.h"
 #include "preprocessing/passes/apply_substs.h"
+#include "preprocessing/passes/apply_to_const.h"
 #include "preprocessing/passes/bool_to_bv.h"
 #include "preprocessing/passes/bv_abstraction.h"
 #include "preprocessing/passes/bv_ackermann.h"
 #include "preprocessing/passes/bv_gauss.h"
 #include "preprocessing/passes/bv_intro_pow2.h"
 #include "preprocessing/passes/bv_to_bool.h"
+#include "preprocessing/passes/extended_rewriter_pass.h"
 #include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
 #include "preprocessing/passes/real_to_int.h"
@@ -897,66 +899,6 @@ public:
     return retval;
   }
 
-  NodeToNodeHashMap d_rewriteApplyToConstCache;
-  Node rewriteApplyToConst(TNode n) {
-    Trace("rewriteApplyToConst") << "rewriteApplyToConst :: " << n << std::endl;
-
-    if(n.getMetaKind() == kind::metakind::CONSTANT ||
-       n.getMetaKind() == kind::metakind::VARIABLE ||
-       n.getMetaKind() == kind::metakind::NULLARY_OPERATOR)
-    {
-      return n;
-    }
-
-    if(d_rewriteApplyToConstCache.find(n) != d_rewriteApplyToConstCache.end()) {
-      Trace("rewriteApplyToConst") << "in cache :: "
-                                   << d_rewriteApplyToConstCache[n]
-                                   << std::endl;
-      return d_rewriteApplyToConstCache[n];
-    }
-
-    if(n.getKind() == kind::APPLY_UF) {
-      if(n.getNumChildren() == 1 && n[0].isConst() &&
-         n[0].getType().isInteger())
-      {
-        stringstream ss;
-        ss << n.getOperator() << "_";
-        if(n[0].getConst<Rational>() < 0) {
-          ss << "m" << -n[0].getConst<Rational>();
-        } else {
-          ss << n[0];
-        }
-        Node newvar = NodeManager::currentNM()->mkSkolem(
-            ss.str(), n.getType(), "rewriteApplyToConst skolem",
-            NodeManager::SKOLEM_EXACT_NAME);
-        d_rewriteApplyToConstCache[n] = newvar;
-        Trace("rewriteApplyToConst") << "made :: " << newvar << std::endl;
-        return newvar;
-      } else {
-        stringstream ss;
-        ss << "The rewrite-apply-to-const preprocessor is currently limited;"
-           << std::endl
-           << "it only works if all function symbols are unary and with Integer"
-           << std::endl
-           << "domain, and all applications are to integer values." << std::endl
-           << "Found application: " << n;
-        Unhandled(ss.str());
-      }
-    }
-
-    NodeBuilder<> builder(n.getKind());
-    if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-      builder << n.getOperator();
-    }
-    for(unsigned i = 0; i < n.getNumChildren(); ++i) {
-      builder << rewriteApplyToConst(n[i]);
-    }
-    Node rewr = builder;
-    d_rewriteApplyToConstCache[n] = rewr;
-    Trace("rewriteApplyToConst") << "built :: " << rewr << std::endl;
-    return rewr;
-  }
-
   void addUseTheoryListListener(TheoryEngine* theoryEngine){
     Options& nodeManagerOptions = NodeManager::currentNM()->getOptions();
     d_listenerRegistrations->add(
@@ -2717,6 +2659,8 @@ void SmtEnginePrivate::finishInit()
   // actually assembling preprocessing pipelines).
   std::unique_ptr<ApplySubsts> applySubsts(
       new ApplySubsts(d_preprocessingPassContext.get()));
+  std::unique_ptr<ApplyToConst> applyToConst(
+      new ApplyToConst(d_preprocessingPassContext.get()));
   std::unique_ptr<BoolToBV> boolToBv(
       new BoolToBV(d_preprocessingPassContext.get()));
   std::unique_ptr<BvAbstraction> bvAbstract(
@@ -2729,6 +2673,8 @@ void SmtEnginePrivate::finishInit()
       new BvIntroPow2(d_preprocessingPassContext.get()));
   std::unique_ptr<BVToBool> bvToBool(
       new BVToBool(d_preprocessingPassContext.get()));
+  std::unique_ptr<ExtRewPre> extRewPre(
+      new ExtRewPre(d_preprocessingPassContext.get()));
   std::unique_ptr<IntToBV> intToBV(
       new IntToBV(d_preprocessingPassContext.get()));
   std::unique_ptr<PseudoBooleanProcessor> pbProc(
@@ -2750,6 +2696,8 @@ void SmtEnginePrivate::finishInit()
       new SepSkolemEmp(d_preprocessingPassContext.get()));
   d_preprocessingPassRegistry.registerPass("apply-substs",
                                            std::move(applySubsts));
+  d_preprocessingPassRegistry.registerPass("apply-to-const",
+                                           std::move(applyToConst));
   d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv));
   d_preprocessingPassRegistry.registerPass("bv-abstraction",
                                            std::move(bvAbstract));
@@ -2759,6 +2707,7 @@ void SmtEnginePrivate::finishInit()
   d_preprocessingPassRegistry.registerPass("bv-intro-pow2",
                                            std::move(bvIntroPow2));
   d_preprocessingPassRegistry.registerPass("bv-to-bool", std::move(bvToBool));
+  d_preprocessingPassRegistry.registerPass("ext-rew-pre", std::move(extRewPre));
   d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
   d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
                                            std::move(pbProc));
@@ -4211,19 +4160,14 @@ void SmtEnginePrivate::processAssertions() {
 
   if (options::extRewPrep())
   {
-    theory::quantifiers::ExtendedRewriter extr(options::extRewPrepAgg());
-    for (unsigned i = 0; i < d_assertions.size(); ++i)
-    {
-      Node a = d_assertions[i];
-      d_assertions.replace(i, extr.extendedRewrite(a));
-    }
+    d_preprocessingPassRegistry.getPass("ext-rew-pre")->apply(&d_assertions);
   }
 
   // Unconstrained simplification
   if(options::unconstrainedSimp()) {
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-unconstrained-simp" << endl;
     dumpAssertions("pre-unconstrained-simp", d_assertions);
-	d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions);
+    d_preprocessingPassRegistry.getPass("rewrite")->apply(&d_assertions);
     unconstrainedSimp();
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-unconstrained-simp" << endl;
     dumpAssertions("post-unconstrained-simp", d_assertions);
@@ -4476,9 +4420,7 @@ void SmtEnginePrivate::processAssertions() {
   if(options::rewriteApplyToConst()) {
     Chat() << "Rewriting applies to constants..." << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteApplyToConstTime);
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      d_assertions[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertions[i]));
-    }
+    d_preprocessingPassRegistry.getPass("apply-to-const")->apply(&d_assertions);
   }
   dumpAssertions("post-rewrite-apply-to-const", d_assertions);
 
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 8366fe4e1..a8e5d74b6 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -186,7 +186,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
   return RewriteResponse(REWRITE_DONE, in);
 }
 
-Kind getOperatorKindForSygusBuiltin(Node op)
+Kind DatatypesRewriter::getOperatorKindForSygusBuiltin(Node op)
 {
   Assert(op.getKind() != BUILTIN);
   if (op.getKind() == LAMBDA)
@@ -212,7 +212,7 @@ Kind getOperatorKindForSygusBuiltin(Node op)
   {
     return APPLY_UF;
   }
-  return NodeManager::operatorToKind(op);
+  return UNDEFINED_KIND;
 }
 
 Node DatatypesRewriter::mkSygusTerm(const Datatype& dt,
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 7d91544e1..a6c95b893 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -121,6 +121,13 @@ public:
   *   C( x, y ) and z
   */
  static bool checkClash(Node n1, Node n2, std::vector<Node>& rew);
+ /** get operator kind for sygus builtin
+  *
+  * This returns the Kind corresponding to applications of the operator op
+  * when building the builtin version of sygus terms. This is used by the
+  * function mkSygusTerm.
+  */
+ static Kind getOperatorKindForSygusBuiltin(Node op);
  /** make sygus term
   *
   * This function returns a builtin term f( children[0], ..., children[n] )
diff --git a/src/theory/quantifiers/fmf/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp
index 5def5fc95..f2b131f21 100644
--- a/src/theory/quantifiers/fmf/ambqi_builder.cpp
+++ b/src/theory/quantifiers/fmf/ambqi_builder.cpp
@@ -13,6 +13,8 @@
  **/
 
 #include "theory/quantifiers/fmf/ambqi_builder.h"
+
+#include "base/cvc4_check.h"
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/term_database.h"
@@ -367,8 +369,8 @@ void AbsDef::construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int cur
   }else{
     TypeNode tn = m->getVariable( q, depth ).getType();
     if( v==depth ){
-      unsigned numReps = m->getRepSet()->getNumRepresentatives(tn);
-      Assert( numReps>0 && numReps < 32 );
+      const unsigned numReps = m->getRepSet()->getNumRepresentatives(tn);
+      CVC4_CHECK(numReps > 0 && numReps < 32);
       for( unsigned i=0; i<numReps; i++ ){
         d_def[ 1 << i ].construct_var( m, q, v, i, depth+1 );
       }
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index cd79fe050..82f8f2c27 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -2,6 +2,7 @@
 equals = =
 
 REG0_TESTS = \
+	regress0/arith/apply2const-test.smt2 \
 	regress0/arith/arith.01.cvc \
 	regress0/arith/arith.02.cvc \
 	regress0/arith/arith.03.cvc \
@@ -437,6 +438,7 @@ REG0_TESTS = \
 	regress0/fmf/syn002-si-real-int.smt2 \
 	regress0/fmf/tail_rec.smt2 \
 	regress0/fp/simple.smt2 \
+	regress0/fp/ext-rew-test.smt2 \
 	regress0/fuzz_1.smt \
 	regress0/fuzz_3.smt \
 	regress0/get-value-incremental.smt2 \
@@ -495,6 +497,7 @@ REG0_TESTS = \
 	regress0/logops.04.cvc \
 	regress0/logops.05.cvc \
 	regress0/nl/coeff-sat.smt2 \
+	regress0/nl/ext-rew-aggr-test.smt2 \
 	regress0/nl/magnitude-wrong-1020-m.smt2 \
 	regress0/nl/mult-po.smt2 \
 	regress0/nl/nia-wrong-tl.smt2 \
diff --git a/test/regress/regress0/arith/apply2const-test.smt2 b/test/regress/regress0/arith/apply2const-test.smt2
new file mode 100644
index 000000000..e11878a74
--- /dev/null
+++ b/test/regress/regress0/arith/apply2const-test.smt2
@@ -0,0 +1,24 @@
+; COMMAND-LINE: --rewrite-apply-to-const
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_UFLIA)
+(set-info :source | MathSat group |)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun hash_1 (Int) Int)
+(declare-fun hash_2 (Int) Int)
+(declare-fun hash_3 (Int) Int)
+(declare-fun hash_4 (Int) Int)
+(declare-fun hash_5 (Int) Int)
+(declare-fun hash_6 (Int) Int)
+(declare-fun hash_7 (Int) Int)
+(declare-fun hash_8 (Int) Int)
+(declare-fun hash_9 (Int) Int)
+(declare-fun hash_10 (Int) Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(declare-fun x4 () Int)
+(assert (let ((?v_0 (hash_1 x1)) (?v_1 (hash_1 x2)) (?v_2 (hash_1 x3)) (?v_3 (hash_1 x4)) (?v_4 (hash_2 x1)) (?v_5 (hash_2 x2)) (?v_6 (hash_2 x3)) (?v_7 (hash_2 x4)) (?v_8 (hash_3 x1)) (?v_9 (hash_3 x2)) (?v_10 (hash_3 x3)) (?v_11 (hash_3 x4)) (?v_12 (hash_4 x1)) (?v_13 (hash_4 x2)) (?v_14 (hash_4 x3)) (?v_15 (hash_4 x4)) (?v_16 (hash_5 x1)) (?v_17 (hash_5 x2)) (?v_18 (hash_5 x3)) (?v_19 (hash_5 x4)) (?v_20 (hash_6 x1)) (?v_21 (hash_6 x2)) (?v_22 (hash_6 x3)) (?v_23 (hash_6 x4)) (?v_24 (hash_7 x1)) (?v_25 (hash_7 x2)) (?v_26 (hash_7 x3)) (?v_27 (hash_7 x4)) (?v_28 (hash_8 x1)) (?v_29 (hash_8 x2)) (?v_30 (hash_8 x3)) (?v_31 (hash_8 x4)) (?v_32 (hash_9 x1)) (?v_33 (hash_9 x2)) (?v_34 (hash_9 x3)) (?v_35 (hash_9 x4)) (?v_36 (hash_10 x1)) (?v_37 (hash_10 x2)) (?v_38 (hash_10 x3)) (?v_39 (hash_10 x4))) (let ((?v_40 (= ?v_0 ?v_4))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (distinct ?v_0 ?v_1) (distinct ?v_0 ?v_2)) (distinct ?v_0 ?v_3)) (distinct ?v_1 ?v_2)) (distinct ?v_1 ?v_3)) (distinct ?v_2 ?v_3)) (distinct ?v_4 ?v_5)) (distinct ?v_4 ?v_6)) (distinct ?v_4 ?v_7)) (distinct ?v_5 ?v_6)) (distinct ?v_5 ?v_7)) (distinct ?v_6 ?v_7)) (distinct ?v_8 ?v_9)) (distinct ?v_8 ?v_10)) (distinct ?v_8 ?v_11)) (distinct ?v_9 ?v_10)) (distinct ?v_9 ?v_11)) (distinct ?v_10 ?v_11)) (distinct ?v_12 ?v_13)) (distinct ?v_12 ?v_14)) (distinct ?v_12 ?v_15)) (distinct ?v_13 ?v_14)) (distinct ?v_13 ?v_15)) (distinct ?v_14 ?v_15)) (distinct ?v_16 ?v_17)) (distinct ?v_16 ?v_18)) (distinct ?v_16 ?v_19)) (distinct ?v_17 ?v_18)) (distinct ?v_17 ?v_19)) (distinct ?v_18 ?v_19)) (distinct ?v_20 ?v_21)) (distinct ?v_20 ?v_22)) (distinct ?v_20 ?v_23)) (distinct ?v_21 ?v_22)) (distinct ?v_21 ?v_23)) (distinct ?v_22 ?v_23)) (distinct ?v_24 ?v_25)) (distinct ?v_24 ?v_26)) (distinct ?v_24 ?v_27)) (distinct ?v_25 ?v_26)) (distinct ?v_25 ?v_27)) (distinct ?v_26 ?v_27)) (distinct ?v_28 ?v_29)) (distinct ?v_28 ?v_30)) (distinct ?v_28 ?v_31)) (distinct ?v_29 ?v_30)) (distinct ?v_29 ?v_31)) (distinct ?v_30 ?v_31)) (distinct ?v_32 ?v_33)) (distinct ?v_32 ?v_34)) (distinct ?v_32 ?v_35)) (distinct ?v_33 ?v_34)) (distinct ?v_33 ?v_35)) (distinct ?v_34 ?v_35)) (distinct ?v_36 ?v_37)) (distinct ?v_36 ?v_38)) (distinct ?v_36 ?v_39)) (distinct ?v_37 ?v_38)) (distinct ?v_37 ?v_39)) (distinct ?v_38 ?v_39)) (or (or (or (= ?v_0 x1) (= ?v_0 x2)) (= ?v_0 x3)) (= ?v_0 x4))) (or (or (or (= ?v_1 x1) (= ?v_1 x2)) (= ?v_1 x3)) (= ?v_1 x4))) (or (or (or (= ?v_2 x1) (= ?v_2 x2)) (= ?v_2 x3)) (= ?v_2 x4))) (or (or (or (= ?v_3 x1) (= ?v_3 x2)) (= ?v_3 x3)) (= ?v_3 x4))) (or (or (or (= ?v_4 x1) (= ?v_4 x2)) (= ?v_4 x3)) (= ?v_4 x4))) (or (or (or (= ?v_5 x1) (= ?v_5 x2)) (= ?v_5 x3)) (= ?v_5 x4))) (or (or (or (= ?v_6 x1) (= ?v_6 x2)) (= ?v_6 x3)) (= ?v_6 x4))) (or (or (or (= ?v_7 x1) (= ?v_7 x2)) (= ?v_7 x3)) (= ?v_7 x4))) (or (or (or (= ?v_8 x1) (= ?v_8 x2)) (= ?v_8 x3)) (= ?v_8 x4))) (or (or (or (= ?v_9 x1) (= ?v_9 x2)) (= ?v_9 x3)) (= ?v_9 x4))) (or (or (or (= ?v_10 x1) (= ?v_10 x2)) (= ?v_10 x3)) (= ?v_10 x4))) (or (or (or (= ?v_11 x1) (= ?v_11 x2)) (= ?v_11 x3)) (= ?v_11 x4))) (or (or (or (= ?v_12 x1) (= ?v_12 x2)) (= ?v_12 x3)) (= ?v_12 x4))) (or (or (or (= ?v_13 x1) (= ?v_13 x2)) (= ?v_13 x3)) (= ?v_13 x4))) (or (or (or (= ?v_14 x1) (= ?v_14 x2)) (= ?v_14 x3)) (= ?v_14 x4))) (or (or (or (= ?v_15 x1) (= ?v_15 x2)) (= ?v_15 x3)) (= ?v_15 x4))) (or (or (or (= ?v_16 x1) (= ?v_16 x2)) (= ?v_16 x3)) (= ?v_16 x4))) (or (or (or (= ?v_17 x1) (= ?v_17 x2)) (= ?v_17 x3)) (= ?v_17 x4))) (or (or (or (= ?v_18 x1) (= ?v_18 x2)) (= ?v_18 x3)) (= ?v_18 x4))) (or (or (or (= ?v_19 x1) (= ?v_19 x2)) (= ?v_19 x3)) (= ?v_19 x4))) (or (or (or (= ?v_20 x1) (= ?v_20 x2)) (= ?v_20 x3)) (= ?v_20 x4))) (or (or (or (= ?v_21 x1) (= ?v_21 x2)) (= ?v_21 x3)) (= ?v_21 x4))) (or (or (or (= ?v_22 x1) (= ?v_22 x2)) (= ?v_22 x3)) (= ?v_22 x4))) (or (or (or (= ?v_23 x1) (= ?v_23 x2)) (= ?v_23 x3)) (= ?v_23 x4))) (or (or (or (= ?v_24 x1) (= ?v_24 x2)) (= ?v_24 x3)) (= ?v_24 x4))) (or (or (or (= ?v_25 x1) (= ?v_25 x2)) (= ?v_25 x3)) (= ?v_25 x4))) (or (or (or (= ?v_26 x1) (= ?v_26 x2)) (= ?v_26 x3)) (= ?v_26 x4))) (or (or (or (= ?v_27 x1) (= ?v_27 x2)) (= ?v_27 x3)) (= ?v_27 x4))) (or (or (or (= ?v_28 x1) (= ?v_28 x2)) (= ?v_28 x3)) (= ?v_28 x4))) (or (or (or (= ?v_29 x1) (= ?v_29 x2)) (= ?v_29 x3)) (= ?v_29 x4))) (or (or (or (= ?v_30 x1) (= ?v_30 x2)) (= ?v_30 x3)) (= ?v_30 x4))) (or (or (or (= ?v_31 x1) (= ?v_31 x2)) (= ?v_31 x3)) (= ?v_31 x4))) (or (or (or (= ?v_32 x1) (= ?v_32 x2)) (= ?v_32 x3)) (= ?v_32 x4))) (or (or (or (= ?v_33 x1) (= ?v_33 x2)) (= ?v_33 x3)) (= ?v_33 x4))) (or (or (or (= ?v_34 x1) (= ?v_34 x2)) (= ?v_34 x3)) (= ?v_34 x4))) (or (or (or (= ?v_35 x1) (= ?v_35 x2)) (= ?v_35 x3)) (= ?v_35 x4))) (or (or (or (= ?v_36 x1) (= ?v_36 x2)) (= ?v_36 x3)) (= ?v_36 x4))) (or (or (or (= ?v_37 x1) (= ?v_37 x2)) (= ?v_37 x3)) (= ?v_37 x4))) (or (or (or (= ?v_38 x1) (= ?v_38 x2)) (= ?v_38 x3)) (= ?v_38 x4))) (or (or (or (= ?v_39 x1) (= ?v_39 x2)) (= ?v_39 x3)) (= ?v_39 x4))) (distinct x1 x2)) (distinct x1 x3)) (distinct x1 x4)) (distinct x2 x3)) (distinct x2 x4)) (distinct x3 x4)) (<= 0 x1)) (< x1 5)) (<= 0 x2)) (< x2 5)) (<= 0 x3)) (< x3 5)) (<= 0 x4)) (< x4 5)) (distinct (ite ?v_40 ?v_4 (+ ?v_0 ?v_0)) (ite ?v_40 ?v_4 (* 2 ?v_0)))))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/fp/ext-rew-test.smt2 b/test/regress/regress0/fp/ext-rew-test.smt2
new file mode 100644
index 000000000..785c654ef
--- /dev/null
+++ b/test/regress/regress0/fp/ext-rew-test.smt2
@@ -0,0 +1,86 @@
+; COMMAND-LINE: --ext-rew-prep
+; EXPECT: unsat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_FP)
+(set-info :category "crafted")
+(set-info :source |Alberto Griggio <griggio@fbk.eu>. These benchmarks were used for the evaluation in the following paper: L. Haller, A. Griggio, M. Brain, D. Kroening: Deciding floating-point logic with systematic abstraction. FMCAD 2012. Real-numbered literals have been automatically translated by MathSAT|)
+(set-info :status unknown)
+;; MathSAT API call trace
+;; generated on 05/20/15 17:24:51
+
+(declare-fun b13 () (_ FloatingPoint 11 53))
+(declare-fun b25 () (_ FloatingPoint 11 53))
+(declare-fun b22 () (_ FloatingPoint 11 53))
+(declare-fun b82 () (_ FloatingPoint 11 53))
+(declare-fun b14 () (_ FloatingPoint 11 53))
+(declare-fun b34 () (_ FloatingPoint 11 53))
+(declare-fun b43 () (_ FloatingPoint 11 53))
+(declare-fun b85 () (_ FloatingPoint 11 53))
+(declare-fun b16 () (_ FloatingPoint 11 53))
+(declare-fun b131 () (_ FloatingPoint 11 53))
+(declare-fun b126 () (_ FloatingPoint 11 53))
+(define-fun _t_3 () RoundingMode RNE)
+(define-fun _t_9 () (_ FloatingPoint 11 53) b131)
+(define-fun _t_10 () (_ FloatingPoint 11 53) b43)
+(define-fun _t_11 () Bool (= _t_9 _t_10))
+(define-fun _t_12 () Bool (not _t_11))
+(define-fun _t_13 () (_ FloatingPoint 11 53) b126)
+(define-fun _t_14 () (_ FloatingPoint 11 53) b34)
+(define-fun _t_15 () Bool (= _t_13 _t_14))
+(define-fun _t_16 () Bool (not _t_15))
+(define-fun _t_17 () (_ FloatingPoint 11 53) b13)
+(define-fun _t_18 () (_ FloatingPoint 11 53) b25)
+(define-fun _t_19 () (_ FloatingPoint 11 53) (fp.mul _t_3 _t_17 _t_18))
+(define-fun _t_20 () (_ FloatingPoint 11 53) b16)
+(define-fun _t_21 () (_ FloatingPoint 11 53) b22)
+(define-fun _t_22 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_20 _t_21))
+(define-fun _t_23 () Bool (fp.lt _t_22 _t_19))
+(define-fun _t_24 () Bool (not _t_23))
+(define-fun _t_25 () (_ FloatingPoint 11 53) b14)
+(define-fun _t_26 () (_ FloatingPoint 11 53) (fp.neg _t_25))
+(define-fun _t_27 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_17 _t_26))
+(define-fun _t_28 () Bool (fp.lt _t_27 _t_21))
+(define-fun _t_29 () Bool (not _t_28))
+(define-fun _t_30 () (_ FloatingPoint 11 53) (fp.mul _t_3 _t_17 _t_25))
+(define-fun _t_31 () Bool (fp.lt _t_30 _t_20))
+(define-fun _t_32 () Bool (not _t_31))
+(define-fun _t_33 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_17 _t_25))
+(define-fun _t_34 () Bool (fp.lt _t_33 _t_20))
+(define-fun _t_35 () Bool (not _t_34))
+(define-fun _t_36 () Bool (= _t_13 _t_20))
+(define-fun _t_37 () Bool (and _t_35 _t_36))
+(define-fun _t_38 () Bool (= _t_9 _t_21))
+(define-fun _t_39 () Bool (and _t_37 _t_38))
+(define-fun _t_40 () (_ FloatingPoint 11 53) b85)
+(define-fun _t_41 () Bool (fp.leq _t_40 _t_25))
+(define-fun _t_42 () Bool (and _t_39 _t_41))
+(define-fun _t_43 () (_ FloatingPoint 11 53) b82)
+(define-fun _t_44 () Bool (fp.leq _t_25 _t_43))
+(define-fun _t_45 () Bool (and _t_42 _t_44))
+(define-fun _t_46 () Bool (fp.leq _t_40 _t_17))
+(define-fun _t_47 () Bool (and _t_45 _t_46))
+(define-fun _t_48 () Bool (fp.leq _t_17 _t_43))
+(define-fun _t_49 () Bool (and _t_47 _t_48))
+(define-fun _t_50 () Bool (fp.leq _t_40 _t_20))
+(define-fun _t_51 () Bool (and _t_49 _t_50))
+(define-fun _t_52 () Bool (fp.leq _t_20 _t_43))
+(define-fun _t_53 () Bool (and _t_51 _t_52))
+(define-fun _t_54 () Bool (fp.leq _t_40 _t_21))
+(define-fun _t_55 () Bool (and _t_53 _t_54))
+(define-fun _t_56 () Bool (fp.leq _t_21 _t_43))
+(define-fun _t_57 () Bool (and _t_55 _t_56))
+(define-fun _t_58 () (_ FloatingPoint 11 53) (fp.add _t_3 _t_9 _t_13))
+(define-fun _t_59 () Bool (fp.lt _t_58 _t_19))
+(define-fun _t_60 () Bool (and _t_57 _t_59))
+(define-fun _t_61 () Bool (fp.lt _t_27 _t_9))
+(define-fun _t_62 () Bool (and _t_60 _t_61))
+(define-fun _t_63 () Bool (fp.lt _t_33 _t_13))
+(define-fun _t_64 () Bool (and _t_62 _t_63))
+(define-fun _t_65 () Bool (and _t_32 _t_64))
+(define-fun _t_66 () Bool (and _t_29 _t_65))
+(define-fun _t_67 () Bool (and _t_24 _t_66))
+(define-fun _t_68 () Bool (and _t_16 _t_67))
+(define-fun _t_69 () Bool (and _t_12 _t_68))
+(assert _t_69)
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/nl/ext-rew-aggr-test.smt2 b/test/regress/regress0/nl/ext-rew-aggr-test.smt2
new file mode 100644
index 000000000..d7a082304
--- /dev/null
+++ b/test/regress/regress0/nl/ext-rew-aggr-test.smt2
@@ -0,0 +1,105 @@
+; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_NIA)
+(set-info :source |
+Generated by: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio
+Generated on: 2017-04-27
+Generator: VeryMax
+Application: Termination proving
+Target solver: barcelogic
+|)
+(set-info :license "https://creativecommons.org/licenses/by/4.0/")
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun global_invc1_0 () Int)
+(declare-fun lam0n0 () Int)
+(declare-fun lam0n2 () Int)
+(declare-fun global_invc1_1 () Int)
+(declare-fun lam0n1 () Int)
+(declare-fun lam1n0 () Int)
+(declare-fun lam1n1 () Int)
+(declare-fun lam1n3 () Int)
+(declare-fun lam1n4 () Int)
+(declare-fun lam1n2 () Int)
+(declare-fun term_invc1_0 () Int)
+(declare-fun lam2n0 () Int)
+(declare-fun lam2n1 () Int)
+(declare-fun lam2n3 () Int)
+(declare-fun lam2n4 () Int)
+(declare-fun lam2n5 () Int)
+(declare-fun lam2n6 () Int)
+(declare-fun lam2n7 () Int)
+(declare-fun lam2n8 () Int)
+(declare-fun lam2n9 () Int)
+(declare-fun lam2n10 () Int)
+(declare-fun lam2n11 () Int)
+(declare-fun lam2n12 () Int)
+(declare-fun lam2n13 () Int)
+(declare-fun lam2n2 () Int)
+(declare-fun term_invc1_1 () Int)
+(declare-fun non_inc1_L () Bool)
+(declare-fun lam3n0 () Int)
+(declare-fun lam3n1 () Int)
+(declare-fun lam3n3 () Int)
+(declare-fun lam3n4 () Int)
+(declare-fun lam3n5 () Int)
+(declare-fun lam3n6 () Int)
+(declare-fun lam3n7 () Int)
+(declare-fun lam3n8 () Int)
+(declare-fun lam3n9 () Int)
+(declare-fun lam3n10 () Int)
+(declare-fun lam3n11 () Int)
+(declare-fun lam3n12 () Int)
+(declare-fun lam3n13 () Int)
+(declare-fun lam3n15 () Int)
+(declare-fun lam3n14 () Int)
+(declare-fun lam3n2 () Int)
+(declare-fun rfc0 () Int)
+(declare-fun disabled1_L () Bool)
+(declare-fun bounded1_L () Bool)
+(declare-fun lam4n0 () Int)
+(declare-fun lam4n1 () Int)
+(declare-fun lam4n3 () Int)
+(declare-fun lam4n4 () Int)
+(declare-fun lam4n5 () Int)
+(declare-fun lam4n6 () Int)
+(declare-fun lam4n7 () Int)
+(declare-fun lam4n8 () Int)
+(declare-fun lam4n9 () Int)
+(declare-fun lam4n10 () Int)
+(declare-fun lam4n11 () Int)
+(declare-fun lam4n12 () Int)
+(declare-fun lam4n13 () Int)
+(declare-fun lam4n14 () Int)
+(declare-fun lam4n2 () Int)
+(declare-fun rfc1 () Int)
+(declare-fun dec1_L () Bool)
+(declare-fun lam5n0 () Int)
+(declare-fun lam5n1 () Int)
+(declare-fun lam5n3 () Int)
+(declare-fun lam5n4 () Int)
+(declare-fun lam5n5 () Int)
+(declare-fun lam5n6 () Int)
+(declare-fun lam5n7 () Int)
+(declare-fun lam5n8 () Int)
+(declare-fun lam5n9 () Int)
+(declare-fun lam5n10 () Int)
+(declare-fun lam5n11 () Int)
+(declare-fun lam5n12 () Int)
+(declare-fun lam5n13 () Int)
+(declare-fun lam5n14 () Int)
+(declare-fun lam5n2 () Int)
+(declare-fun bnd_and_dec1_L () Bool)
+(declare-fun GLOBAL_NT_1 () Bool)
+(declare-fun global_V0_1 () Int)
+(declare-fun TERM_NT_1 () Bool)
+(declare-fun term_V0_1 () Int)
+(declare-fun ALL_NON_INC_0 () Bool)
+(declare-fun DIS_OR_ALL_NON_INC_0 () Bool)
+(declare-fun SOME_BND_AND_DEC_0 () Bool)
+(declare-fun V0_NIV () Int)
+(declare-fun V1_NIV () Int)
+(assert ( and ( >= global_invc1_0 ( - 1 ) ) ( <= global_invc1_0 1 ) ( and ( >= lam0n0 0 ) ( <= 0 lam0n2 ) ( < lam0n2 1 ) ( and ( = ( * ( - 1 ) lam0n0 ) ( + global_invc1_1 ( * ( - 1 ) lam0n2 ) ) ) ( = ( * lam0n1 1 ) 0 ) ( = ( * lam0n1 ( - 1 ) ) global_invc1_0 ) ) ) ( and ( >= lam1n0 0 ) ( >= lam1n1 0 ) ( >= lam1n3 0 ) ( <= 0 lam1n4 ) ( < lam1n4 1 ) ( and ( = ( + ( * ( - 1 ) lam1n0 ) ( * lam1n1 ( - 999 ) ) ( * lam1n2 1000 ) ( * lam1n3 global_invc1_1 ) ) ( + global_invc1_1 ( * ( - 1 ) lam1n4 ) ) ) ( = ( + ( * lam1n1 ( - 1 ) ) ( * lam1n2 1 ) ( * lam1n3 global_invc1_0 ) ) 0 ) ( = ( * lam1n2 ( - 1 ) ) global_invc1_0 ) ) ) ( >= term_invc1_0 ( - 1 ) ) ( <= term_invc1_0 1 ) ( and ( >= lam2n0 0 ) ( >= lam2n1 0 ) ( >= lam2n3 0 ) ( >= lam2n4 0 ) ( >= lam2n5 0 ) ( >= lam2n6 0 ) ( >= lam2n7 0 ) ( >= lam2n8 0 ) ( >= lam2n9 0 ) ( >= lam2n10 0 ) ( >= lam2n11 0 ) ( >= lam2n12 0 ) ( <= 0 lam2n13 ) ( < lam2n13 1 ) ( and ( = ( + ( * ( - 1 ) lam2n0 ) ( * lam2n1 ( - 999 ) ) ( * lam2n2 1000 ) ( * lam2n3 50001 ) ( * lam2n4 ( - 1 ) ) ( * lam2n5 1 ) ( * lam2n6 2 ) ( * lam2n7 3 ) ( * lam2n8 55 ) ( * lam2n9 58 ) ( * lam2n10 61 ) ( * lam2n11 62 ) ( * lam2n12 global_invc1_1 ) ) ( + term_invc1_1 ( * ( - 1 ) lam2n13 ) ) ) ( = ( + ( * lam2n1 ( - 1 ) ) ( * lam2n2 1 ) ( * lam2n3 ( - 1 ) ) ( * lam2n4 ( - 1 ) ) ( * lam2n5 ( - 1 ) ) ( * lam2n6 ( - 1 ) ) ( * lam2n7 ( - 1 ) ) ( * lam2n8 ( - 1 ) ) ( * lam2n9 ( - 1 ) ) ( * lam2n10 ( - 1 ) ) ( * lam2n11 ( - 1 ) ) ( * lam2n12 global_invc1_0 ) ) 0 ) ( = ( * lam2n2 ( - 1 ) ) term_invc1_0 ) ) ) ( = non_inc1_L ( and ( >= lam3n0 0 ) ( >= lam3n1 0 ) ( >= lam3n3 0 ) ( >= lam3n4 0 ) ( >= lam3n5 0 ) ( >= lam3n6 0 ) ( >= lam3n7 0 ) ( >= lam3n8 0 ) ( >= lam3n9 0 ) ( >= lam3n10 0 ) ( >= lam3n11 0 ) ( >= lam3n12 0 ) ( >= lam3n13 0 ) ( <= 0 lam3n15 ) ( < lam3n15 1 ) ( <= lam3n14 1 ) ( >= lam3n14 0 ) ( and ( > ( + ( * ( - 1 ) lam3n0 ) ( * lam3n1 ( - 999 ) ) ( * lam3n2 1000 ) ( * lam3n3 50001 ) ( * lam3n4 ( - 1 ) ) ( * lam3n5 1 ) ( * lam3n6 2 ) ( * lam3n7 3 ) ( * lam3n8 55 ) ( * lam3n9 58 ) ( * lam3n10 61 ) ( * lam3n11 62 ) ( * lam3n12 global_invc1_1 ) ( * lam3n13 term_invc1_1 ) ( * lam3n14 ( + 1 ( * ( - 1 ) lam3n15 ) ) ) ) 0 ) ( = ( + ( * lam3n1 ( - 1 ) ) ( * lam3n2 1 ) ( * lam3n3 ( - 1 ) ) ( * lam3n4 ( - 1 ) ) ( * lam3n5 ( - 1 ) ) ( * lam3n6 ( - 1 ) ) ( * lam3n7 ( - 1 ) ) ( * lam3n8 ( - 1 ) ) ( * lam3n9 ( - 1 ) ) ( * lam3n10 ( - 1 ) ) ( * lam3n11 ( - 1 ) ) ( * lam3n12 global_invc1_0 ) ( * lam3n13 term_invc1_0 ) ( * lam3n14 rfc0 ) ) 0 ) ( = ( + ( * lam3n2 ( - 1 ) ) ( * lam3n14 ( * ( - 1 ) rfc0 ) ) ) 0 ) ) ) ) ( = disabled1_L ( and ( = lam3n14 0 ) non_inc1_L ) ) ( = bounded1_L ( and ( >= lam4n0 0 ) ( >= lam4n1 0 ) ( >= lam4n3 0 ) ( >= lam4n4 0 ) ( >= lam4n5 0 ) ( >= lam4n6 0 ) ( >= lam4n7 0 ) ( >= lam4n8 0 ) ( >= lam4n9 0 ) ( >= lam4n10 0 ) ( >= lam4n11 0 ) ( >= lam4n12 0 ) ( >= lam4n13 0 ) ( <= 0 lam4n14 ) ( < lam4n14 1 ) ( and ( = ( + ( * ( - 1 ) lam4n0 ) ( * lam4n1 ( - 999 ) ) ( * lam4n2 1000 ) ( * lam4n3 50001 ) ( * lam4n4 ( - 1 ) ) ( * lam4n5 1 ) ( * lam4n6 2 ) ( * lam4n7 3 ) ( * lam4n8 55 ) ( * lam4n9 58 ) ( * lam4n10 61 ) ( * lam4n11 62 ) ( * lam4n12 global_invc1_1 ) ( * lam4n13 term_invc1_1 ) ) ( + ( * ( - 1 ) rfc1 ) ( * ( - 1 ) lam4n14 ) ) ) ( = ( + ( * lam4n1 ( - 1 ) ) ( * lam4n2 1 ) ( * lam4n3 ( - 1 ) ) ( * lam4n4 ( - 1 ) ) ( * lam4n5 ( - 1 ) ) ( * lam4n6 ( - 1 ) ) ( * lam4n7 ( - 1 ) ) ( * lam4n8 ( - 1 ) ) ( * lam4n9 ( - 1 ) ) ( * lam4n10 ( - 1 ) ) ( * lam4n11 ( - 1 ) ) ( * lam4n12 global_invc1_0 ) ( * lam4n13 term_invc1_0 ) ) ( * ( - 1 ) rfc0 ) ) ( = ( * lam4n2 ( - 1 ) ) 0 ) ) ) ) ( = dec1_L ( and ( >= lam5n0 0 ) ( >= lam5n1 0 ) ( >= lam5n3 0 ) ( >= lam5n4 0 ) ( >= lam5n5 0 ) ( >= lam5n6 0 ) ( >= lam5n7 0 ) ( >= lam5n8 0 ) ( >= lam5n9 0 ) ( >= lam5n10 0 ) ( >= lam5n11 0 ) ( >= lam5n12 0 ) ( >= lam5n13 0 ) ( <= 0 lam5n14 ) ( < lam5n14 1 ) ( and ( = ( + ( * ( - 1 ) lam5n0 ) ( * lam5n1 ( - 999 ) ) ( * lam5n2 1000 ) ( * lam5n3 50001 ) ( * lam5n4 ( - 1 ) ) ( * lam5n5 1 ) ( * lam5n6 2 ) ( * lam5n7 3 ) ( * lam5n8 55 ) ( * lam5n9 58 ) ( * lam5n10 61 ) ( * lam5n11 62 ) ( * lam5n12 global_invc1_1 ) ( * lam5n13 term_invc1_1 ) ) ( + 1 ( * ( - 1 ) lam5n14 ) ) ) ( = ( + ( * lam5n1 ( - 1 ) ) ( * lam5n2 1 ) ( * lam5n3 ( - 1 ) ) ( * lam5n4 ( - 1 ) ) ( * lam5n5 ( - 1 ) ) ( * lam5n6 ( - 1 ) ) ( * lam5n7 ( - 1 ) ) ( * lam5n8 ( - 1 ) ) ( * lam5n9 ( - 1 ) ) ( * lam5n10 ( - 1 ) ) ( * lam5n11 ( - 1 ) ) ( * lam5n12 global_invc1_0 ) ( * lam5n13 term_invc1_0 ) ) ( * ( - 1 ) rfc0 ) ) ( = ( * lam5n2 ( - 1 ) ) rfc0 ) ) ) ) ( = bnd_and_dec1_L ( and bounded1_L dec1_L ) ) ( = GLOBAL_NT_1 ( not ( = global_invc1_0 0 ) ) ) ( or ( not ( <= ( + global_invc1_1 ( * global_invc1_0 global_V0_1 ) ) 0 ) ) ( = global_invc1_0 0 ) ) ( = TERM_NT_1 ( not ( = term_invc1_0 0 ) ) ) ( or ( and ( not ( <= ( + term_invc1_1 ( * term_invc1_0 term_V0_1 ) ) 0 ) ) ( <= ( + ( * ( - 1 ) term_V0_1 ) ( - 1 ) ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 1 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 2 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 3 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 55 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 58 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 61 ) 0 ) ( <= ( + ( * ( - 1 ) term_V0_1 ) 62 ) 0 ) ) ( = term_invc1_0 0 ) ) ( = ALL_NON_INC_0 non_inc1_L ) ( = DIS_OR_ALL_NON_INC_0 ( or disabled1_L ALL_NON_INC_0 ) ) ( = SOME_BND_AND_DEC_0 bnd_and_dec1_L ) ( or ( not ALL_NON_INC_0 ) ( and ( >= rfc0 ( - 2 ) ) ( <= rfc0 2 ) ( not ( = rfc0 0 ) ) ( >= rfc1 0 ) ( or SOME_BND_AND_DEC_0 ( or ( and ( <= ( + ( * rfc0 V0_NIV ) 1 ) ( * rfc0 V1_NIV ) ) ( >= ( * ( - 1 ) V0_NIV ) ( * ( - 1 ) V1_NIV ) ) ) ( = rfc0 0 ) ) ) ) ) ( or GLOBAL_NT_1 TERM_NT_1 ALL_NON_INC_0 ) ))
+(check-sat)
+(exit)