ContrainSubtypes and ExpandingDefinitions classes

6 files changed, 1499 insertions, 49 deletions

diff --git a/src/' b/src/'
new file mode 100644
index 000000000..4fbbca322
--- /dev/null
+++ b/src/'
@@ -0,0 +1,779 @@
+/*********************                                                        */
+/*! \file smt_engine.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2016 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 SmtEngine: the main public entry point of libcvc4.
+ **
+ ** SmtEngine: the main public entry point of libcvc4.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT_ENGINE_H
+#define __CVC4__SMT_ENGINE_H
+
+#include <string>
+#include <vector>
+
+#include "base/modal_exception.h"
+#include "context/cdhashmap_forward.h"
+#include "context/cdhashset_forward.h"
+#include "context/cdlist_forward.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "expr/expr_stream.h"
+#include "options/options.h"
+#include "proof/unsat_core.h"
+#include "smt/logic_exception.h"
+#include "smt_util/lemma_channels.h"
+#include "theory/logic_info.h"
+#include "util/hash.h"
+#include "util/proof.h"
+#include "util/result.h"
+#include "util/sexpr.h"
+#include "util/statistics.h"
+#include "util/unsafe_interrupt_exception.h"
+
+// In terms of abstraction, this is below (and provides services to)
+// ValidityChecker and above (and requires the services of)
+// PropEngine.
+
+namespace CVC4 {
+
+template <bool ref_count> class NodeTemplate;
+typedef NodeTemplate<true> Node;
+typedef NodeTemplate<false> TNode;
+struct NodeHashFunction;
+
+class Command;
+class GetModelCommand;
+
+class SmtEngine;
+class DecisionEngine;
+class TheoryEngine;
+
+class ProofManager;
+
+class Model;
+class LogicRequest;
+class StatisticsRegistry;
+
+namespace context {
+  class Context;
+  class UserContext;
+}/* CVC4::context namespace */
+
+namespace prop {
+  class PropEngine;
+}/* CVC4::prop namespace */
+
+namespace expr {
+  namespace attr {
+    class AttributeManager;
+    struct SmtAttributes;
+  }/* CVC4::expr::attr namespace */
+}/* CVC4::expr namespace */
+
+namespace smt {
+  /**
+   * Representation of a defined function.  We keep these around in
+   * SmtEngine to permit expanding definitions late (and lazily), to
+   * support getValue() over defined functions, to support user output
+   * in terms of defined functions, etc.
+   */
+  class DefinedFunction;
+
+  struct SmtEngineStatistics;
+  class SmtEnginePrivate;
+  class SmtScope;
+  class BooleanTermConverter;
+
+  ProofManager* currentProofManager();
+
+  struct CommandCleanup;
+  typedef context::CDList<Command*, CommandCleanup> CommandList;
+}/* CVC4::smt namespace */
+
+namespace theory {
+  class TheoryModel;
+}/* CVC4::theory namespace */
+
+namespace preproc{
+//  class DefinedFunction;
+  class DoStaticLearningPass; 
+  class QuantifiedPass;
+  class SimplifyAssertionsPass;
+  class ExpandingDefinitionsPass;
+  class ConstrainSubtypesPass;
+}/* CVC4::preproc namespace */
+
+// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
+// hood): use a type parameter and have check() delegate, or subclass
+// SmtEngine and override check()?
+//
+// Probably better than that is to have a configuration object that
+// indicates which passes are desired.  The configuration occurs
+// elsewhere (and can even occur at runtime).  A simple "pass manager"
+// of sorts determines check()'s behavior.
+//
+// The CNF conversion can go on in PropEngine.
+
+class CVC4_PUBLIC SmtEngine {
+  /** The type of our internal map of defined functions */
+  typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>
+    DefinedFunctionMap;
+  /** The type of our internal assertion list */
+  typedef context::CDList<Expr> AssertionList;
+  /** The type of our internal assignment set */
+  typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet;
+  /** The types for the recursive function definitions */
+  typedef context::CDList<Node> NodeList;
+
+  /** Expr manager context */
+  context::Context* d_context;
+
+  /** The context levels of user pushes */
+  std::vector<int> d_userLevels;
+  /** User level context */
+  context::UserContext* d_userContext;
+
+  /** Our expression manager */
+  ExprManager* d_exprManager;
+  /** Our internal expression/node manager */
+  NodeManager* d_nodeManager;
+  /** The decision engine */
+  DecisionEngine* d_decisionEngine;
+  /** The theory engine */
+  TheoryEngine* d_theoryEngine;
+  /** The propositional engine */
+  prop::PropEngine* d_propEngine;
+  /** The proof manager */
+  ProofManager* d_proofManager;
+  /** An index of our defined functions */
+  DefinedFunctionMap* d_definedFunctions;
+  /** recursive function definition abstractions for --fmf-fun */
+  std::map< Node, TypeNode > d_fmfRecFunctionsAbs;
+  std::map< Node, std::vector< Node > > d_fmfRecFunctionsConcrete;
+  NodeList* d_fmfRecFunctionsDefined;
+
+  /**
+   * The assertion list (before any conversion) for supporting
+   * getAssertions().  Only maintained if in interactive mode.
+   */
+  AssertionList* d_assertionList;
+
+  /**
+   * List of items for which to retrieve values using getAssignment().
+   */
+  AssignmentSet* d_assignments;
+
+  /**
+   * A list of commands that should be in the Model globally (i.e.,
+   * regardless of push/pop).  Only maintained if produce-models option
+   * is on.
+   */
+  std::vector<Command*> d_modelGlobalCommands;
+
+  /**
+   * A list of commands that should be in the Model locally (i.e.,
+   * it is context-dependent on push/pop).  Only maintained if
+   * produce-models option is on.
+   */
+  smt::CommandList* d_modelCommands;
+
+  /**
+   * A vector of declaration commands waiting to be dumped out.
+   * Once the SmtEngine is fully initialized, we'll dump them.
+   * This ensures the declarations come after the set-logic and
+   * any necessary set-option commands are dumped.
+   */
+  std::vector<Command*> d_dumpCommands;
+
+  /**
+   *A vector of command definitions to be imported in the new
+   *SmtEngine when checking unsat-cores.
+   */
+  std::vector<Command*> d_defineCommands;
+
+  /**
+   * The logic we're in.
+   */
+  LogicInfo d_logic;
+
+  /**
+   * Keep a copy of the original option settings (for reset()).
+   */
+  Options d_originalOptions;
+
+  /**
+   * Number of internal pops that have been deferred.
+   */
+  unsigned d_pendingPops;
+
+  /**
+   * Whether or not this SmtEngine has been fully initialized (that is,
+   * the ).  This post-construction initialization is automatically
+   * triggered by the use of the SmtEngine; e.g. when setLogic() is
+   * called, or the first assertion is made, etc.
+   */
+  bool d_fullyInited;
+
+  /**
+   * Whether or not we have added any assertions/declarations/definitions,
+   * or done push/pop, since the last checkSat/query, and therefore we're
+   * not responsible for models or proofs.
+   */
+  bool d_problemExtended;
+
+  /**
+   * Whether or not a query() or checkSat() has already been made through
+   * this SmtEngine.  If true, and incrementalSolving is false, then
+   * attempting an additional query() or checkSat() will fail with a
+   * ModalException.
+   */
+  bool d_queryMade;
+
+  /**
+   * Internal status flag to indicate whether we've sent a theory
+   * presolve() notification and need to match it with a postsolve().
+   */
+  bool d_needPostsolve;
+
+  /*
+   * Whether to call theory preprocessing during simplification - on
+   * by default* but gets turned off if arithRewriteEq is on
+   */
+  bool d_earlyTheoryPP;
+
+  /**
+   * Most recent result of last checkSat/query or (set-info :status).
+   */
+  Result d_status;
+
+  /**
+   * The name of the input (if any).
+   */
+  std::string d_filename;
+
+  /**
+   * Verbosity of various commands.
+   */
+  std::map<std::string, Integer> d_commandVerbosity;
+
+  /** ReplayStream for the solver. */
+  ExprStream* d_replayStream;
+
+  /**
+   * A private utility class to SmtEngine.
+   */
+  smt::SmtEnginePrivate* d_private;
+
+  /**
+   * Check that a generated proof (via getProof()) checks.
+   */
+  void checkProof();
+
+  /**
+   * Check that an unsatisfiable core is indeed unsatisfiable.
+   */
+  void checkUnsatCore();
+
+  /**
+   * Check that a generated Model (via getModel()) actually satisfies
+   * all user assertions.
+   */
+  void checkModel(bool hardFailure = true);
+
+  /**
+   * Postprocess a value for output to the user.  Involves doing things
+   * like turning datatypes back into tuples, length-1-bitvectors back
+   * into booleans, etc.
+   */
+  Node postprocess(TNode n, TypeNode expectedType) const;
+
+  /**
+   * This is something of an "init" procedure, but is idempotent; call
+   * as often as you like.  Should be called whenever the final options
+   * and logic for the problem are set (at least, those options that are
+   * not permitted to change after assertions and queries are made).
+   */
+  void finalOptionsAreSet();
+
+  /**
+   * Apply heuristics settings and other defaults.  Done once, at
+   * finishInit() time.
+   */
+  void setDefaults();
+
+  /**
+   * Create theory engine, prop engine, decision engine. Called by
+   * finalOptionsAreSet()
+   */
+  void finishInit();
+
+  /**
+   * This is called by the destructor, just before destroying the
+   * PropEngine, TheoryEngine, and DecisionEngine (in that order).  It
+   * is important because there are destruction ordering issues
+   * between PropEngine and Theory.
+   */
+  void shutdown();
+
+  /**
+   * Full check of consistency in current context.  Returns true iff
+   * consistent.
+   */
+  Result check();
+
+  /**
+   * Quick check of consistency in current context: calls
+   * processAssertionList() then look for inconsistency (based only on
+   * that).
+   */
+  Result quickCheck();
+
+  /**
+   * Fully type-check the argument, and also type-check that it's
+   * actually Boolean.
+   */
+  void ensureBoolean(const Expr& e) throw(TypeCheckingException);
+
+  void internalPush();
+
+  void internalPop(bool immediate = false);
+
+  void doPendingPops();
+
+  /**
+   * Internally handle the setting of a logic.  This function should always
+   * be called when d_logic is updated.
+   */
+  void setLogicInternal() throw();
+  
+  friend class ::CVC4::preproc::DoStaticLearningPass;
+  friend class ::CVC4::preproc::QuantifiedPass; 
+  friend class ::CVC4::preproc::SimplifyAssertionsPass;
+  friend class ::CVC4::preproc::ExpandingDefinitionsPass;
+  friend class ::CVC4::preproc::ConstrainSubtypesPass;
+  friend class ::CVC4::smt::SmtEnginePrivate;
+  friend class ::CVC4::smt::SmtScope;
+  friend class ::CVC4::smt::BooleanTermConverter;
+  friend ProofManager* ::CVC4::smt::currentProofManager();
+  friend class ::CVC4::LogicRequest;
+  // to access d_modelCommands
+  friend class ::CVC4::Model;
+  friend class ::CVC4::theory::TheoryModel;
+  // to access SmtAttributes
+  friend class expr::attr::AttributeManager;
+  // to access getModel(), which is private (for now)
+  friend class GetModelCommand;
+
+  /**
+   * There's something of a handshake between the expr package's
+   * AttributeManager and the SmtEngine because the expr package
+   * doesn't have a Context on its own (that's owned by the
+   * SmtEngine).  Thus all context-dependent attributes are stored
+   * here.
+   */
+  expr::attr::SmtAttributes* d_smtAttributes;
+
+  StatisticsRegistry* d_statisticsRegistry;
+
+  smt::SmtEngineStatistics* d_stats;
+
+  /** Container for the lemma input and output channels for this SmtEngine.*/
+  LemmaChannels* d_channels;
+
+  /**
+   * Add to Model command.  This is used for recording a command
+   * that should be reported during a get-model call.
+   */
+  void addToModelCommandAndDump(const Command& c, uint32_t flags = 0, bool userVisible = true, const char* dumpTag = "declarations");
+
+  /**
+   * Get the model (only if immediately preceded by a SAT
+   * or INVALID query).  Only permitted if CVC4 was built with model
+   * support and produce-models is on.
+   */
+  Model* getModel();
+
+  // disallow copy/assignment
+  SmtEngine(const SmtEngine&) CVC4_UNDEFINED;
+  SmtEngine& operator=(const SmtEngine&) CVC4_UNDEFINED;
+
+  //check satisfiability (for query and check-sat)
+  Result checkSatisfiability(const Expr& e, bool inUnsatCore, bool isQuery);
+public:
+
+  /**
+   * Construct an SmtEngine with the given expression manager.
+   */
+  SmtEngine(ExprManager* em) throw();
+
+  /**
+   * Destruct the SMT engine.
+   */
+  ~SmtEngine() throw();
+
+  /**
+   * Set the logic of the script.
+   */
+  void setLogic(const std::string& logic) throw(ModalException, LogicException);
+
+  /**
+   * Set the logic of the script.
+   */
+  void setLogic(const char* logic) throw(ModalException, LogicException);
+
+  /**
+   * Set the logic of the script.
+   */
+  void setLogic(const LogicInfo& logic) throw(ModalException);
+
+  /**
+   * Get the logic information currently set
+   */
+  LogicInfo getLogicInfo() const;
+
+  /**
+   * Set information about the script executing.
+   */
+  void setInfo(const std::string& key, const CVC4::SExpr& value)
+    throw(OptionException, ModalException);
+
+  /**
+   * Query information about the SMT environment.
+   */
+  CVC4::SExpr getInfo(const std::string& key) const;
+
+  /**
+   * Set an aspect of the current SMT execution environment.
+   */
+  void setOption(const std::string& key, const CVC4::SExpr& value)
+    throw(OptionException, ModalException);
+
+  /**
+   * Get an aspect of the current SMT execution environment.
+   */
+  CVC4::SExpr getOption(const std::string& key) const
+    throw(OptionException);
+
+  /**
+   * Add a formula to the current context: preprocess, do per-theory
+   * setup, use processAssertionList(), asserting to T-solver for
+   * literals and conjunction of literals.  Returns false if
+   * immediately determined to be inconsistent.
+   */
+  void defineFunction(Expr func,
+                      const std::vector<Expr>& formals,
+                      Expr formula);
+
+  /** is defined function */
+  bool isDefinedFunction(Expr func);
+
+  /**
+   * Add a formula to the current context: preprocess, do per-theory
+   * setup, use processAssertionList(), asserting to T-solver for
+   * literals and conjunction of literals.  Returns false if
+   * immediately determined to be inconsistent.  This version
+   * takes a Boolean flag to determine whether to include this asserted
+   * formula in an unsat core (if one is later requested).
+   */
+  Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
+
+  /**
+   * Check validity of an expression with respect to the current set
+   * of assertions by asserting the query expression's negation and
+   * calling check().  Returns valid, invalid, or unknown result.
+   */
+  Result query(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException);
+
+  /**
+   * Assert a formula (if provided) to the current context and call
+   * check().  Returns sat, unsat, or unknown result.
+   */
+  Result checkSat(const Expr& e = Expr(), bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException);
+
+  /**
+   * Assert a synthesis conjecture to the current context and call
+   * check().  Returns sat, unsat, or unknown result.
+   */
+  Result checkSynth(const Expr& e) throw(TypeCheckingException, ModalException, LogicException);
+
+  /**
+   * Simplify a formula without doing "much" work.  Does not involve
+   * the SAT Engine in the simplification, but uses the current
+   * definitions, assertions, and the current partial model, if one
+   * has been constructed.  It also involves theory normalization.
+   *
+   * @todo (design) is this meant to give an equivalent or an
+   * equisatisfiable formula?
+   */
+  Expr simplify(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
+
+  /**
+   * Expand the definitions in a term or formula.  No other
+   * simplification or normalization is done.
+   */
+  Expr expandDefinitions(const Expr& e) throw(TypeCheckingException, LogicException, UnsafeInterruptException);
+
+  /**
+   * Get the assigned value of an expr (only if immediately preceded
+   * by a SAT or INVALID query).  Only permitted if the SmtEngine is
+   * set to operate interactively and produce-models is on.
+   */
+  Expr getValue(const Expr& e) const throw(ModalException, TypeCheckingException, LogicException, UnsafeInterruptException);
+
+  /**
+   * Add a function to the set of expressions whose value is to be
+   * later returned by a call to getAssignment().  The expression
+   * should be a Boolean zero-ary defined function or a Boolean
+   * variable.  Rather than throwing a ModalException on modal
+   * failures (not in interactive mode or not producing assignments),
+   * this function returns true if the expression was added and false
+   * if this request was ignored.
+   */
+  bool addToAssignment(const Expr& e);
+
+  /**
+   * Get the assignment (only if immediately preceded by a SAT or
+   * INVALID query).  Only permitted if the SmtEngine is set to
+   * operate interactively and produce-assignments is on.
+   */
+  CVC4::SExpr getAssignment();
+
+  /**
+   * Get the last proof (only if immediately preceded by an UNSAT
+   * or VALID query).  Only permitted if CVC4 was built with proof
+   * support and produce-proofs is on.
+   */
+  Proof* getProof();
+
+  /**
+   * Print all instantiations made by the quantifiers module.
+   */
+  void printInstantiations( std::ostream& out );
+
+  /**
+   * Print solution for synthesis conjectures found by ce_guided_instantiation module
+   */
+  void printSynthSolution( std::ostream& out );
+
+  /**
+   * Do quantifier elimination, doFull false means just output one disjunct, strict is whether to output warnings.
+   */
+  Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict=true) throw(TypeCheckingException, ModalException, LogicException);
+
+  /**
+   * Get list of quantified formulas that were instantiated
+   */
+  void getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs );
+   
+  /**
+   * Get instantiations
+   */
+  void getInstantiations( Expr q, std::vector< Expr >& insts );
+  void getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs );
+
+  /**
+   * Get an unsatisfiable core (only if immediately preceded by an
+   * UNSAT or VALID query).  Only permitted if CVC4 was built with
+   * unsat-core support and produce-unsat-cores is on.
+   */
+  UnsatCore getUnsatCore();
+
+  /**
+   * Get the current set of assertions.  Only permitted if the
+   * SmtEngine is set to operate interactively.
+   */
+  std::vector<Expr> getAssertions();
+
+  /**
+   * Push a user-level context.
+   */
+  void push() throw(ModalException, LogicException, UnsafeInterruptException);
+
+  /**
+   * Pop a user-level context.  Throws an exception if nothing to pop.
+   */
+  void pop();
+
+  /**
+   * Completely reset the state of the solver, as though destroyed and
+   * recreated.  The result is as if newly constructed (so it still
+   * retains the same options structure and ExprManager).
+   */
+  void reset() throw();
+
+  /**
+   * Reset all assertions, global declarations, etc.
+   */
+  void resetAssertions() throw();
+
+  /**
+   * Interrupt a running query.  This can be called from another thread
+   * or from a signal handler.  Throws a ModalException if the SmtEngine
+   * isn't currently in a query.
+   */
+  void interrupt() throw(ModalException);
+
+  /**
+   * Set a resource limit for SmtEngine operations.  This is like a time
+   * limit, but it's deterministic so that reproducible results can be
+   * obtained.  Currently, it's based on the number of conflicts.
+   * However, please note that the definition may change between different
+   * versions of CVC4 (as may the number of conflicts required, anyway),
+   * and it might even be different between instances of the same version
+   * of CVC4 on different platforms.
+   *
+   * A cumulative and non-cumulative (per-call) resource limit can be
+   * set at the same time.  A call to setResourceLimit() with
+   * cumulative==true replaces any cumulative resource limit currently
+   * in effect; a call with cumulative==false replaces any per-call
+   * resource limit currently in effect.  Time limits can be set in
+   * addition to resource limits; the SmtEngine obeys both.  That means
+   * that up to four independent limits can control the SmtEngine
+   * at the same time.
+   *
+   * When an SmtEngine is first created, it has no time or resource
+   * limits.
+   *
+   * Currently, these limits only cause the SmtEngine to stop what its
+   * doing when the limit expires (or very shortly thereafter); no
+   * heuristics are altered by the limits or the threat of them expiring.
+   * We reserve the right to change this in the future.
+   *
+   * @param units the resource limit, or 0 for no limit
+   * @param cumulative whether this resource limit is to be a cumulative
+   * resource limit for all remaining calls into the SmtEngine (true), or
+   * whether it's a per-call resource limit (false); the default is false
+   */
+  void setResourceLimit(unsigned long units, bool cumulative = false);
+
+  /**
+   * Set a time limit for SmtEngine operations.
+   *
+   * A cumulative and non-cumulative (per-call) time limit can be
+   * set at the same time.  A call to setTimeLimit() with
+   * cumulative==true replaces any cumulative time limit currently
+   * in effect; a call with cumulative==false replaces any per-call
+   * time limit currently in effect.  Resource limits can be set in
+   * addition to time limits; the SmtEngine obeys both.  That means
+   * that up to four independent limits can control the SmtEngine
+   * at the same time.
+   *
+   * Note that the cumulative timer only ticks away when one of the
+   * SmtEngine's workhorse functions (things like assertFormula(),
+   * query(), checkSat(), and simplify()) are running.  Between calls,
+   * the timer is still.
+   *
+   * When an SmtEngine is first created, it has no time or resource
+   * limits.
+   *
+   * Currently, these limits only cause the SmtEngine to stop what its
+   * doing when the limit expires (or very shortly thereafter); no
+   * heuristics are altered by the limits or the threat of them expiring.
+   * We reserve the right to change this in the future.
+   *
+   * @param millis the time limit in milliseconds, or 0 for no limit
+   * @param cumulative whether this time limit is to be a cumulative
+   * time limit for all remaining calls into the SmtEngine (true), or
+   * whether it's a per-call time limit (false); the default is false
+   */
+  void setTimeLimit(unsigned long millis, bool cumulative = false);
+
+  /**
+   * Get the current resource usage count for this SmtEngine.  This
+   * function can be used to ascertain reasonable values to pass as
+   * resource limits to setResourceLimit().
+   */
+  unsigned long getResourceUsage() const;
+
+  /**
+   * Get the current millisecond count for this SmtEngine.
+   */
+  unsigned long getTimeUsage() const;
+
+  /**
+   * Get the remaining resources that can be consumed by this SmtEngine
+   * according to the currently-set cumulative resource limit.  If there
+   * is not a cumulative resource limit set, this function throws a
+   * ModalException.
+   */
+  unsigned long getResourceRemaining() const throw(ModalException);
+
+  /**
+   * Get the remaining number of milliseconds that can be consumed by
+   * this SmtEngine according to the currently-set cumulative time limit.
+   * If there is not a cumulative resource limit set, this function
+   * throws a ModalException.
+   */
+  unsigned long getTimeRemaining() const throw(ModalException);
+
+  /**
+   * Permit access to the underlying ExprManager.
+   */
+  ExprManager* getExprManager() const {
+    return d_exprManager;
+  }
+
+  /**
+   * Export statistics from this SmtEngine.
+   */
+  Statistics getStatistics() const throw();
+
+  /**
+   * Get the value of one named statistic from this SmtEngine.
+   */
+  SExpr getStatistic(std::string name) const throw();
+
+  /**
+   * Flush statistic from this SmtEngine. Safe to use in a signal handler.
+   */
+  void safeFlushStatistics(int fd) const;
+
+  /**
+   * Returns the most recent result of checkSat/query or (set-info :status).
+   */
+  Result getStatusOfLastCommand() const throw() {
+    return d_status;
+  }
+
+  /**
+   * Set user attribute.
+   * This function is called when an attribute is set by a user.
+   * In SMT-LIBv2 this is done via the syntax (! expr :attr)
+   */
+  void setUserAttribute(const std::string& attr, Expr expr, std::vector<Expr> expr_values, std::string str_value);
+
+  /**
+   * Set print function in model
+   */
+  void setPrintFuncInModel(Expr f, bool p);
+
+
+  /** Throws a ModalException if the SmtEngine has been fully initialized. */
+  void beforeSearch() throw(ModalException);
+
+  LemmaChannels* channels() { return d_channels; }
+
+
+  /**
+   * Expermintal feature: Sets the sequence of decisions.
+   * This currently requires very fine grained knowledge about literal
+   * translation.
+   */
+  void setReplayStream(ExprStream* exprStream);
+
+};/* class SmtEngine */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__SMT_ENGINE_H */
diff --git a/src/preproc/preprocessing_pass.h b/src/preproc/preprocessing_pass.h
index d956993aa..739db58ff 100644
--- a/src/preproc/preprocessing_pass.h
+++ b/src/preproc/preprocessing_pass.h
@@ -11,6 +11,8 @@
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 
+using namespace std;
+
 namespace CVC4 {
 
 namespace preproc {
@@ -28,6 +30,23 @@ public:
   }
 };
 
+class DefinedFunction {
+  Node d_func;
+  vector<Node> d_formals;
+  Node d_formula;
+public:
+  DefinedFunction() {}
+  DefinedFunction(Node func, vector<Node> formals, Node formula) :
+    d_func(func),
+    d_formals(formals),
+    d_formula(formula) {
+  }
+  Node getFunction() const { return d_func; }
+  vector<Node> getFormals() const { return d_formals; }
+  Node getFormula() const { return d_formula; }
+};
+/* class DefinedFunction */
+
 class AssertionPipeline {
   std::vector<Node> d_nodes;
 
diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp
index 669607a1c..9c23340db 100644
--- a/src/preproc/preprocessing_passes_core.cpp
+++ b/src/preproc/preprocessing_passes_core.cpp
@@ -2,6 +2,8 @@
 
 #include <unordered_map>
 #include <string>
+#include <stack>
+#include "expr/node_manager_attributes.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/fun_def_process.h"
@@ -14,21 +16,188 @@
 #include "options/bv_bitblast_mode.h"
 #include "options/bv_options.h"
 #include "options/uf_options.h"
+#include "options/proof_options.h"
+#include "util/ntuple.h"
+
+using namespace std;
 
 namespace CVC4 {
 namespace preproc {
 
-ExpandingDefinitionsPass::ExpandingDefinitionsPass(ResourceManager* resourceManager, TimerStat definitionExpansionTime) : PreprocessingPass(resourceManager), d_definitionExpansionTime(definitionExpansionTime){
+ExpandingDefinitionsPass::ExpandingDefinitionsPass(ResourceManager* resourceManager, SmtEngine* smt, TimerStat definitionExpansionTime) : PreprocessingPass(resourceManager), d_smt(smt), d_definitionExpansionTime(definitionExpansionTime){
+}
+
+Node ExpandingDefinitionsPass::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
+  throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
+  stack< triple<Node, Node, bool> > worklist;
+  stack<Node> result;
+  worklist.push(make_triple(Node(n), Node(n), false));
+  // The worklist is made of triples, each is input / original node then the output / rewritten node
+  // and finally a flag tracking whether the children have been explored (i.e. if this is a downward
+  // or upward pass).
+
+  do {
+    spendResource(options::preprocessStep());
+    n = worklist.top().first;                      // n is the input / original
+    Node node = worklist.top().second;             // node is the output / result
+    bool childrenPushed = worklist.top().third;
+    worklist.pop();
+
+    // Working downwards
+    if(!childrenPushed) {
+      Kind k = n.getKind();
+
+      // Apart from apply, we can short circuit leaves
+      if(k != kind::APPLY && n.getNumChildren() == 0) {
+        SmtEngine::DefinedFunctionMap::const_iterator i = d_smt->d_definedFunctions->find(n);
+        if(i != d_smt->d_definedFunctions->end()) {
+          // replacement must be closed
+          if((*i).second.getFormals().size() > 0) {
+            result.push(d_smt->d_nodeManager->mkNode(kind::LAMBDA, d_smt->d_nodeManager->mkNode(kind::BOUND_VAR_LIST, (*i).second.getFormals()), (*i).second.getFormula()));
+            continue;
+          }
+          // don't bother putting in the cache
+          result.push((*i).second.getFormula());
+          continue;
+        }
+        // don't bother putting in the cache
+        result.push(n);
+        continue;
+      }
+
+      // maybe it's in the cache
+      unordered_map<Node, Node, NodeHashFunction>::iterator cacheHit = cache.find(n);
+      if(cacheHit != cache.end()) {
+        TNode ret = (*cacheHit).second;
+        result.push(ret.isNull() ? n : ret);
+        continue;
+      }
+
+      // otherwise expand it
+      bool doExpand = k == kind::APPLY;
+      if( !doExpand ){
+        if( options::macrosQuant() ){
+          //expand if we have inferred an operator corresponds to a defined function
+          doExpand = k==kind::APPLY_UF && d_smt->isDefinedFunction( n.getOperator().toExpr() );
+        }
+      }
+      if (doExpand) {
+        vector<Node> formals;
+        TNode fm;
+        if( n.getOperator().getKind() == kind::LAMBDA ){
+          TNode op = n.getOperator();
+          // lambda
+          for( unsigned i=0; i<op[0].getNumChildren(); i++ ){
+            formals.push_back( op[0][i] );
+          }
+          fm = op[1];
+        }else{
+          // application of a user-defined symbol
+          TNode func = n.getOperator();
+          SmtEngine::DefinedFunctionMap::const_iterator i = d_smt->d_definedFunctions->find(func);
+          if(i == d_smt->d_definedFunctions->end()) {
+            throw TypeCheckingException(n.toExpr(), string("Undefined function: `") + func.toString() + "'");
+          }
+          DefinedFunction def = (*i).second;
+          formals = def.getFormals();
+
+          if(Debug.isOn("expand")) {
+            Debug("expand") << "found: " << n << endl;
+            Debug("expand") << " func: " << func << endl;
+            string name = func.getAttribute(expr::VarNameAttr());
+            Debug("expand") << "     : \"" << name << "\"" << endl;
+          }
+          if(Debug.isOn("expand")) {
+            Debug("expand") << " defn: " << def.getFunction() << endl
+                            << "       [";
+            if(formals.size() > 0) {
+              copy( formals.begin(), formals.end() - 1,
+                    ostream_iterator<Node>(Debug("expand"), ", ") );
+              Debug("expand") << formals.back();
+            }
+            Debug("expand") << "]" << endl
+                            << "       " << def.getFunction().getType() << endl
+                            << "       " << def.getFormula() << endl;
+          }
+
+          fm = def.getFormula();
+        }
+
+        Node instance = fm.substitute(formals.begin(), formals.end(),
+                                      n.begin(), n.end());
+        Debug("expand") << "made : " << instance << endl;
+
+        Node expanded = expandDefinitions(instance, cache, expandOnly);
+        cache[n] = (n == expanded ? Node::null() : expanded);
+        result.push(expanded);
+        continue;
+
+      } else if(! expandOnly) {
+        // do not do any theory stuff if expandOnly is true
+
+        theory::Theory* t = d_smt->d_theoryEngine->theoryOf(node);
+
+        Assert(t != NULL);
+        LogicRequest req(*d_smt);
+        node = t->expandDefinition(req, n);
+      }
+
+      // there should be children here, otherwise we short-circuited a result-push/continue, above
+      if (node.getNumChildren() == 0) {
+        Debug("expand") << "Unexpectedly no children..." << node << endl;
+      }
+      // This invariant holds at the moment but it is concievable that a new theory
+      // might introduce a kind which can have children before definition expansion but doesn't
+      // afterwards.  If this happens, remove this assertion.
+      Assert(node.getNumChildren() > 0);
+
+      // the partial functions can fall through, in which case we still
+      // consider their children
+      worklist.push(make_triple(Node(n), node, true));            // Original and rewritten result
+
+      for(size_t i = 0; i < node.getNumChildren(); ++i) {
+        worklist.push(make_triple(node[i], node[i], false));      // Rewrite the children of the result only
+      }
+
+    } else {
+      // Working upwards
+      // Reconstruct the node from it's (now rewritten) children on the stack
+
+      Debug("expand") << "cons : " << node << endl;
+      //cout << "cons : " << node << endl;
+      NodeBuilder<> nb(node.getKind());
+      if(node.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        Debug("expand") << "op   : " << node.getOperator() << endl;
+        //cout << "op   : " << node.getOperator() << endl;
+        nb << node.getOperator();
+      }
+      for(size_t i = 0; i < node.getNumChildren(); ++i) {
+        Assert(!result.empty());
+        Node expanded = result.top();
+        result.pop();
+        //cout << "exchld : " << expanded << endl;
+        Debug("expand") << "exchld : " << expanded << endl;
+        nb << expanded;
+      }
+      node = nb;
+      cache[n] = n == node ? Node::null() : node;           // Only cache once all subterms are expanded
+      result.push(node);
+    }
+  } while(!worklist.empty());
+
+  AlwaysAssert(result.size() == 1);
+
+  return result.top();
 }
 
 PreprocessingPassResult ExpandingDefinitionsPass::apply(AssertionPipeline* assertionsToPreprocess){
-/*  Chat() << "expanding definitions..." << std::endl;
+  Chat() << "expanding definitions..." << std::endl;
     Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
     TimerStat::CodeTimer codeTimer(d_definitionExpansionTime);
     hash_map<Node, Node, NodeHashFunction> cache;
     for(unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
       assertionsToPreprocess->replace(i, expandDefinitions((*assertionsToPreprocess)[i], cache));
-    }*/
+    }
   return PreprocessingPassResult(true);
 }
 
@@ -501,6 +670,78 @@ PreprocessingPassResult BVAbstractionPass::apply(AssertionPipeline* assertionsTo
  return PreprocessingPassResult(true);
 } 
 
+ConstrainSubtypesPass::ConstrainSubtypesPass(ResourceManager* resourceManager, SmtEngine* smt) : PreprocessingPass(resourceManager), d_smt(smt) {
+}
+
+void ConstrainSubtypesPass::constrainSubtypes(TNode top, AssertionPipeline& assertions)
+  throw() {
+  Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
+
+  set<TNode> done;
+  stack<TNode> worklist;
+  worklist.push(top);
+  done.insert(top);
+
+  do {
+    TNode n = worklist.top();
+    worklist.pop();
+
+    TypeNode t = n.getType();
+    if(t.isPredicateSubtype()) {
+      WarningOnce() << "Warning: CVC4 doesn't yet do checking that predicate subtypes are nonempty domains" << endl;
+      Node pred = t.getSubtypePredicate();
+      Kind k;
+      // pred can be a LAMBDA, a function constant, or a datatype tester
+      Trace("constrainSubtypes") << "constrainSubtypes(): pred.getType() == " << pred.getType() << endl;
+      if(d_smt->d_definedFunctions->find(pred) != d_smt->d_definedFunctions->end()) {
+        k = kind::APPLY;
+      } else if(pred.getType().isTester()) {
+        k = kind::APPLY_TESTER;
+      } else {
+        k = kind::APPLY_UF;
+      }
+      Node app = NodeManager::currentNM()->mkNode(k, pred, n);
+      Trace("constrainSubtypes") << "constrainSubtypes(): assert(" << k << ") " << app << endl;
+      assertions.push_back(app);
+    } else if(t.isSubrange()) {
+      SubrangeBounds bounds = t.getSubrangeBounds();
+      Trace("constrainSubtypes") << "constrainSubtypes(): got bounds " << bounds << endl;
+      if(bounds.lower.hasBound()) {
+        Node c = NodeManager::currentNM()->mkConst(Rational(bounds.lower.getBound()));
+        Node lb = NodeManager::currentNM()->mkNode(kind::LEQ, c, n);
+        Trace("constrainSubtypes") << "constrainSubtypes(): assert " << lb << endl;
+        assertions.push_back(lb);
+      }
+      if(bounds.upper.hasBound()) {
+        Node c = NodeManager::currentNM()->mkConst(Rational(bounds.upper.getBound()));
+        Node ub = NodeManager::currentNM()->mkNode(kind::LEQ, n, c);
+        Trace("constrainSubtypes") << "constrainSubtypes(): assert " << ub << endl;
+        assertions.push_back(ub);
+      }
+    }
+
+    for(TNode::iterator i = n.begin(); i != n.end(); ++i) {
+      if(done.find(*i) == done.end()) {
+        worklist.push(*i);
+        done.insert(*i);
+      }
+    }
+  } while(! worklist.empty());
+}
+
+PreprocessingPassResult ConstrainSubtypesPass::apply(AssertionPipeline* assertionsToPreprocess){
+    // Any variables of subtype types need to be constrained properly.
+    // Careful, here: constrainSubtypes() adds to the back of
+    // d_assertions, but we don't need to reprocess those.
+    // We also can't use an iterator, because the vector may be moved in
+    // memory during this loop.
+    Chat() << "constraining subtypes..." << endl;
+    for(unsigned i = 0, i_end = assertionsToPreprocess->size(); i != i_end; ++i) {
+      constrainSubtypes((*assertionsToPreprocess)[i], *assertionsToPreprocess);
+    }
+  return PreprocessingPassResult(true);
+}
+
 UnconstrainedSimpPass::UnconstrainedSimpPass(ResourceManager* resourceManager,
       TimerStat unconstrainedSimpTime, TheoryEngine* theoryEngine) :
       PreprocessingPass(resourceManager), 
@@ -833,6 +1074,7 @@ PreprocessingPassResult NoConflictPass::apply(AssertionPipeline* assertionsToPre
  return PreprocessingPassResult(true);
 }
 
+/**
 RepeatSimpPass::RepeatSimpPass(ResourceManager* resourceManager, 
     theory::SubstitutionMap* topLevelSubstitutions,
     unsigned simplifyAssertionsDepth, bool* noConflict, 
@@ -904,7 +1146,7 @@ void RepeatSimpPass::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Nod
 
 
 PreprocessingPassResult RepeatSimpPass::apply(AssertionPipeline* assertionsToPreprocess){
-   /* Chat() << "re-simplifying assertions..." << std::endl;
+    Chat() << "re-simplifying assertions..." << std::endl;
     ScopeCounter depth(d_simplifyAssertionsDepth);
   //  *noConflict &= simplifyAssertions();
     if (*noConflict) {
@@ -969,21 +1211,391 @@ PreprocessingPassResult RepeatSimpPass::apply(AssertionPipeline* assertionsToPre
       removeITEs();
       //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
     }
-  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << std::endl;*/
+  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << std::endl;
  return PreprocessingPassResult(true);
 }
 
 SimplifyAssertionsPass::SimplifyAssertionsPass(
-   ResourceManager* resourceManager, unsigned simplifyAssertionsDepth) : 
+   ResourceManager* resourceManager, unsigned simplifyAssertionsDepth, 
+   SmtEngine* smt, bool propagatorNeedsFinish, 
+   theory::booleans::CircuitPropagator propagator,
+   context::CDO<unsigned> substitutionsIndex,
+   std::vector<Node> nonClausalLearnedLiterals, Node dtrue, 
+   TimerStat nonclausalSimplificationTime) : 
    PreprocessingPass(resourceManager),
-   d_simplifyAssertionsDepth(simplifyAssertionsDepth){
+   d_simplifyAssertionsDepth(simplifyAssertionsDepth),
+   d_smt(smt), d_propagatorNeedsFinish(propagatorNeedsFinish), 
+   d_propagator(propagator), d_substitutionsIndex(substitutionsIndex), 
+   d_nonClausalLearnedLiterals(nonClausalLearnedLiterals),
+   d_true(dtrue), d_nonclausalSimplificationTime(nonclausalSimplificationTime) {
+}
+
+void SimplifyAssertionsPass::addFormula(TNode n, bool inUnsatCore, bool inInput, AssertionPipeline d_assertions)
+  throw(TypeCheckingException, LogicException) {
+
+  if (n == d_true) {
+    // nothing to do
+    return;
+  }
+
+  Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << endl;
+
+  // Give it to proof manager
+  PROOF(
+    if( inInput ){
+      // n is an input assertion
+      if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
+
+        ProofManager::currentPM()->addCoreAssertion(n.toExpr());
+      }
+    }else{
+      // n is the result of an unknown preprocessing step, add it to dependency map to null
+      ProofManager::currentPM()->addDependence(n, Node::null());
+    }
+    // rewrite rules are by default in the unsat core because
+    // they need to be applied until saturation
+    if(options::unsatCores() &&
+       n.getKind() == kind::REWRITE_RULE ){
+      ProofManager::currentPM()->addUnsatCore(n.toExpr());
+    }
+  );
+
+  // Add the normalized formula to the queue
+  d_assertions.push_back(n);
+  //d_assertions.push_back(Rewriter::rewrite(n));
+}
+
+// returns false if it learns a conflict
+bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions) {
+  spendResource(options::preprocessStep());
+  d_smt->finalOptionsAreSet();
+
+  if(options::unsatCores() || options::fewerPreprocessingHoles()) {
+    return true;
+  }
+
+  TimerStat::CodeTimer nonclausalTimer(d_nonclausalSimplificationTime);
+
+  Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl;
+  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    Trace("simplify") << "Assertion #" << i << " : " << d_assertions[i] << std::endl;
+  }
+
+  if(d_propagatorNeedsFinish) {
+    d_propagator.finish();
+    d_propagatorNeedsFinish = false;
+  }
+  d_propagator.initialize();
+
+  // Assert all the assertions to the propagator
+  Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                    << "asserting to propagator" << endl;
+  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
+    // Don't reprocess substitutions
+    if (d_substitutionsIndex > 0 && i == d_substitutionsIndex) {
+      continue;
+    }
+    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions[i] << endl;
+    Debug("cores") << "d_propagator assertTrue: " << d_assertions[i] << std::endl;
+    d_propagator.assertTrue(d_assertions[i]);
+  }
+
+  Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                    << "propagating" << endl;
+  if (d_propagator.propagate()) {
+    // If in conflict, just return false
+    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                      << "conflict in non-clausal propagation" << endl;
+    Node falseNode = NodeManager::currentNM()->mkConst<bool>(false);
+    Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
+    d_assertions.clear();
+    addFormula(falseNode, false, false, d_assertions);
+    d_propagatorNeedsFinish = true;
+    return false;
+  }
+
+
+  Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals.size() << " learned literals." << std::endl;
+  // No conflict, go through the literals and solve them
+  theory::SubstitutionMap constantPropagations(d_smt->d_context);
+  theory::SubstitutionMap newSubstitutions(d_smt->d_context);
+  theory::SubstitutionMap::iterator pos;
+  unsigned j = 0;
+  for(unsigned i = 0, i_end = d_nonClausalLearnedLiterals.size(); i < i_end; ++ i) {
+    // Simplify the literal we learned wrt previous substitutions
+    Node learnedLiteral = d_nonClausalLearnedLiterals[i];
+    Assert(theory::Rewriter::rewrite(learnedLiteral) == learnedLiteral);
+    Assert(d_topLevelSubstitutions.apply(learnedLiteral) == learnedLiteral);
+    Trace("simplify") << "Process learnedLiteral : " << learnedLiteral << std::endl;
+    Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral);
+    if (learnedLiteral != learnedLiteralNew) {
+      learnedLiteral = theory::Rewriter::rewrite(learnedLiteralNew);
+    }
+    Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral << std::endl;
+    for (;;) {
+      learnedLiteralNew = constantPropagations.apply(learnedLiteral);
+      if (learnedLiteralNew == learnedLiteral) {
+        break;
+      }
+      ++d_smt->d_stats->d_numConstantProps;
+      learnedLiteral = theory::Rewriter::rewrite(learnedLiteralNew);
+    }
+    Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral << std::endl;
+    // It might just simplify to a constant
+    if (learnedLiteral.isConst()) {
+      if (learnedLiteral.getConst<bool>()) {
+        // If the learned literal simplifies to true, it's redundant
+        continue;
+      } else {
+        // If the learned literal simplifies to false, we're in conflict
+        Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                          << "conflict with "
+                          << d_nonClausalLearnedLiterals[i] << endl;
+        Assert(!options::unsatCores());
+        d_assertions.clear();
+        addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false, d_assertions);
+        d_propagatorNeedsFinish = true;
+        return false;
+      }
+    }
+
+    // Solve it with the corresponding theory, possibly adding new
+    // substitutions to newSubstitutions
+    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                      << "solving " << learnedLiteral << endl;
+
+    Theory::PPAssertStatus solveStatus =
+      d_smt->d_theoryEngine->solve(learnedLiteral, newSubstitutions);
+
+    switch (solveStatus) {
+      case Theory::PP_ASSERT_STATUS_SOLVED: {
+        // The literal should rewrite to true
+        Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                          << "solved " << learnedLiteral << endl;
+        Assert(theory::Rewriter::rewrite(newSubstitutions.apply(learnedLiteral)).isConst());
+        //        vector<pair<Node, Node> > equations;
+        //        constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true);
+        //        if (equations.empty()) {
+        //          break;
+        //        }
+        //        Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
+        // else fall through
+        break;
+      }
+      case Theory::PP_ASSERT_STATUS_CONFLICT:
+        // If in conflict, we return false
+        Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                          << "conflict while solving "
+                          << learnedLiteral << endl;
+        Assert(!options::unsatCores());
+        d_assertions.clear();
+        addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false, d_assertions);
+        d_propagatorNeedsFinish = true;
+        return false;
+      default:
+        if (d_doConstantProp && learnedLiteral.getKind() == kind::EQUAL && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst())) {
+          // constant propagation
+          TNode t;
+          TNode c;
+          if (learnedLiteral[0].isConst()) {
+            t = learnedLiteral[1];
+            c = learnedLiteral[0];
+          }
+          else {
+            t = learnedLiteral[0];
+            c = learnedLiteral[1];
+          }
+          Assert(!t.isConst());
+          Assert(constantPropagations.apply(t) == t);
+          Assert(d_topLevelSubstitutions.apply(t) == t);
+          Assert(newSubstitutions.apply(t) == t);
+          constantPropagations.addSubstitution(t, c);
+          // vector<pair<Node,Node> > equations;
+          // constantPropagations.simplifyLHS(t, c, equations, true);
+          // if (!equations.empty()) {
+          //   Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
+          //   d_assertions.clear();
+          //   addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
+          //   return;
+          // }
+          // d_topLevelSubstitutions.simplifyRHS(constantPropagations);
+        }
+        else {
+          // Keep the literal
+          d_nonClausalLearnedLiterals[j++] = d_nonClausalLearnedLiterals[i];
+        }
+        break;
+    }
+  }
+
+#ifdef CVC4_ASSERTIONS
+  // NOTE: When debugging this code, consider moving this check inside of the
+  // loop over d_nonClausalLearnedLiterals. This check has been moved outside
+  // because it is costly for certain inputs (see bug 508).
+  //
+  // Check data structure invariants:
+  // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations
+  // 2. each lhs of constantPropagations rewrites to itself
+  // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a
+  //    constant propagation too
+  // 4. each lhs of constantPropagations is different from each rhs
+  for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
+    Assert((*pos).first.isVar());
+    Assert(d_topLevelSubstitutions.apply((*pos).first) == (*pos).first);
+    Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
+    Assert(newSubstitutions.apply(newSubstitutions.apply((*pos).second)) == newSubstitutions.apply((*pos).second));
+  }
+  for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
+    Assert((*pos).second.isConst());
+    Assert(theory::Rewriter::rewrite((*pos).first) == (*pos).first);
+    // Node newLeft = d_topLevelSubstitutions.apply((*pos).first);
+    // if (newLeft != (*pos).first) {
+    //   newLeft = Rewriter::rewrite(newLeft);
+    //   Assert(newLeft == (*pos).second ||
+    //          (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
+    // }
+    // newLeft = constantPropagations.apply((*pos).first);
+    // if (newLeft != (*pos).first) {
+    //   newLeft = Rewriter::rewrite(newLeft);
+    //   Assert(newLeft == (*pos).second ||
+    //          (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second));
+    // }
+    Assert(constantPropagations.apply((*pos).second) == (*pos).second);
+  }
+//#endif  CVC4_ASSERTIONS 
+
+  // Resize the learnt
+  Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl;
+  d_nonClausalLearnedLiterals.resize(j);
+
+  hash_set<TNode, TNodeHashFunction> s;
+  Trace("debugging") << "NonClausal simplify pre-preprocess\n";
+  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    Node assertion = d_assertions[i];
+    Node assertionNew = newSubstitutions.apply(assertion);
+    Trace("debugging") << "assertion = " << assertion << endl;
+    Trace("debugging") << "assertionNew = " << assertionNew << endl;
+    if (assertion != assertionNew) {
+      assertion = theory::Rewriter::rewrite(assertionNew);
+      Trace("debugging") << "rewrite(assertion) = " << assertion << endl;
+    }
+    Assert(theory::Rewriter::rewrite(assertion) == assertion);
+    for (;;) {
+      assertionNew = constantPropagations.apply(assertion);
+      if (assertionNew == assertion) {
+        break;
+      }
+      ++d_smt->d_stats->d_numConstantProps;
+      Trace("debugging") << "assertionNew = " << assertionNew << endl;
+      assertion = theory::Rewriter::rewrite(assertionNew);
+      Trace("debugging") << "assertionNew = " << assertionNew << endl;
+    }
+    Trace("debugging") << "\n";
+    s.insert(assertion);
+    d_assertions.replace(i, assertion);
+    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                      << "non-clausal preprocessed: "
+                      << assertion << endl;
+  }
+
+  // If in incremental mode, add substitutions to the list of assertions
+  if (d_substitutionsIndex > 0) {
+    NodeBuilder<> substitutionsBuilder(kind::AND);
+    substitutionsBuilder << d_assertions[d_substitutionsIndex];
+    pos = newSubstitutions.begin();
+    for (; pos != newSubstitutions.end(); ++pos) {
+      // Add back this substitution as an assertion
+      TNode lhs = (*pos).first, rhs = newSubstitutions.apply((*pos).second);
+      Node n = NodeManager::currentNM()->mkNode(kind::EQUAL, lhs, rhs);
+      substitutionsBuilder << n;
+      Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
+    }
+    if (substitutionsBuilder.getNumChildren() > 1) {
+      d_assertions.replace(d_substitutionsIndex,
+        theory::Rewriter::rewrite(Node(substitutionsBuilder)));
+    }
+  } else {
+    // If not in incremental mode, must add substitutions to model
+    TheoryModel* m = d_smt->d_theoryEngine->getModel();
+    if(m != NULL) {
+      for(pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
+        Node n = (*pos).first;
+        Node v = newSubstitutions.apply((*pos).second);
+        Trace("model") << "Add substitution : " << n << " " << v << endl;
+        m->addSubstitution( n, v );
+      }
+    }
+  }
+
+  NodeBuilder<> learnedBuilder(kind::AND);
+  Assert(d_realAssertionsEnd <= d_assertions.size());
+  learnedBuilder << d_assertions[d_realAssertionsEnd - 1];
+
+  for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
+    Node learned = d_nonClausalLearnedLiterals[i];
+    Assert(d_topLevelSubstitutions.apply(learned) == learned);
+    Node learnedNew = newSubstitutions.apply(learned);
+    if (learned != learnedNew) {
+      learned = theory::Rewriter::rewrite(learnedNew);
+    }
+    Assert(theory::Rewriter::rewrite(learned) == learned);
+    for (;;) {
+      learnedNew = constantPropagations.apply(learned);
+      if (learnedNew == learned) {
+        break;
+      }
+      ++d_smt->d_stats->d_numConstantProps;
+      learned = theory::Rewriter::rewrite(learnedNew);
+    }
+    if (s.find(learned) != s.end()) {
+      continue;
+    }
+    s.insert(learned);
+    learnedBuilder << learned;
+    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                      << "non-clausal learned : "
+                      << learned << endl;
+  }
+  d_nonClausalLearnedLiterals.clear();
+
+  for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
+    Node cProp = (*pos).first.eqNode((*pos).second);
+    Assert(d_topLevelSubstitutions.apply(cProp) == cProp);
+    Node cPropNew = newSubstitutions.apply(cProp);
+    if (cProp != cPropNew) {
+      cProp = theory::Rewriter::rewrite(cPropNew);
+      Assert(theory::Rewriter::rewrite(cProp) == cProp);
+    }
+    if (s.find(cProp) != s.end()) {
+      continue;
+    }
+    s.insert(cProp);
+    learnedBuilder << cProp;
+    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                      << "non-clausal constant propagation : "
+                      << cProp << endl;
+  }
+
+  // Add new substitutions to topLevelSubstitutions
+  // Note that we don't have to keep rhs's in full solved form
+  // because SubstitutionMap::apply does a fixed-point iteration when substituting
+  d_topLevelSubstitutions.addSubstitutions(newSubstitutions);
+
+  if(learnedBuilder.getNumChildren() > 1) {
+    d_assertions.replace(d_realAssertionsEnd - 1,
+      theory::Rewriter::rewrite(Node(learnedBuilder)));
+  }
+
+  d_propagatorNeedsFinish = true;
+  return true;
 }
 
 // returns false if simplification led to "false"
 PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* assertionsToPreprocess)
   throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
- /* spendResource(options::preprocessStep());
-  Assert(d_smt.d_pendingPops == 0);
+  spendResource(options::preprocessStep());
+  Assert(d_smt->d_pendingPops == 0);
   try {
     ScopeCounter depth(d_simplifyAssertionsDepth);
 
@@ -996,7 +1608,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti
       Chat() << "...performing nonclausal simplification..." << endl;
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
                         << "performing non-clausal simplification" << endl;
-      bool noConflict = nonClausalSimplify();
+      bool noConflict = nonClausalSimplify(*assertionsToPreprocess);
       if(!noConflict) {
         return false;
       }
@@ -1008,7 +1620,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti
           // miplib rewrites aren't safe in incremental mode
           ! options::incrementalSolving() &&
           // only useful in arith
-          d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) &&
+          d_smt->d_logic.isTheoryEnabled(THEORY_ARITH) &&
           // we add new assertions and need this (in practice, this
           // restriction only disables miplib processing during
           // re-simplification, which we don't expect to be useful anyway)
@@ -1017,7 +1629,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti
         Trace("simplify") << "SmtEnginePrivate::simplify(): "
                           << "looking for miplib pseudobooleans..." << endl;
 
-        TimerStat::CodeTimer miplibTimer(d_smt.d_stats->d_miplibPassTime);
+        TimerStat::CodeTimer miplibTimer(d_smt->d_stats->d_miplibPassTime);
 
         doMiplibTrick();
       } else {
@@ -1031,20 +1643,20 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti
     Debug("smt") << " d_assertions     : " << assertionsToPreprocess->size() << endl;
 
     // before ppRewrite check if only core theory for BV theory
-    d_smt.d_theoryEngine->staticInitializeBVOptions(assertionsToPreprocess->ref());
+    d_smt->d_theoryEngine->staticInitializeBVOptions(assertionsToPreprocess->ref());
 
     dumpAssertions("pre-theorypp", *assertionsToPreprocess);
 
     // Theory preprocessing
-    if (d_smt.d_earlyTheoryPP) {
+    if (d_smt->d_earlyTheoryPP) {
       Chat() << "...doing early theory preprocessing..." << endl;
-      TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
+      TimerStat::CodeTimer codeTimer(d_smt->d_stats->d_theoryPreprocessTime);
       // Call the theory preprocessors
-      d_smt.d_theoryEngine->preprocessStart();
+      d_smt->d_theoryEngine->preprocessStart();
       for (unsigned i = 0; i < assertionsToPreprocess->size(); ++ i) {
-        Assert(Rewriter::rewrite((*assertionsToPreprocess)[i]) == (*assertionsTopreprocess)[i]);
-        assertionsToPreprocess->replace(i, d_smt.d_theoryEngine->preprocess((*assertionsToPreprocess)[i]));
-        Assert(Rewriter::rewrite((*assertionsToPreprocess)[i]) == (*assertionsToPreprocess)[i]);
+        Assert(theory::Rewriter::rewrite((*assertionsToPreprocess)[i]) == (*assertionsTopreprocess)[i]);
+        assertionsToPreprocess->replace(i, d_smt->d_theoryEngine->preprocess((*assertionsToPreprocess)[i]));
+        Assert(theory::Rewriter::rewrite((*assertionsToPreprocess)[i]) == (*assertionsToPreprocess)[i]);
       }
     }
 
@@ -1070,7 +1682,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti
     // Unconstrained simplification
     if(options::unconstrainedSimp()) {
       Chat() << "...doing unconstrained simplification..." << endl;
-      preproc::UnconstrainedSimpPass pass(d_resourceManager, d_smt.d_stats->d_unconstrainedSimpTime, d_smt.d_theoryEngine);
+      preproc::UnconstrainedSimpPass pass(d_resourceManager, d_smt->d_stats->d_unconstrainedSimpTime, d_smt->d_theoryEngine);
       pass.apply(assertionsToPreprocess);
    }
 
@@ -1082,7 +1694,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti
       Chat() << "...doing another round of nonclausal simplification..." << endl;
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
                         << " doing repeated simplification" << endl;
-      bool noConflict = nonClausalSimplify();
+      bool noConflict = nonClausalSimplify(*assertionsToPreprocess);
       if(!noConflict) {
         return false;
       }
@@ -1102,10 +1714,10 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti
     ss << "A bad expression was produced.  Original exception follows:\n"
        << tcep;
     InternalError(ss.str().c_str());
-  }*/
+  }
   return PreprocessingPassResult(true); 
 }
-
+**/
 
 }  // namespace preproc
 }  // namespace CVC4
diff --git a/src/preproc/preprocessing_passes_core.h b/src/preproc/preprocessing_passes_core.h
index c27890853..0e113a761 100644
--- a/src/preproc/preprocessing_passes_core.h
+++ b/src/preproc/preprocessing_passes_core.h
@@ -6,6 +6,7 @@
 #include "preproc/preprocessing_pass.h"
 #include "theory/substitutions.h"
 #include "theory/arith/pseudoboolean_proc.h"
+#include "theory/booleans/circuit_propagator.h"
 #include "smt/smt_engine.h"
 #include "smt/term_formula_removal.h"
 #include "decision/decision_engine.h"
@@ -20,10 +21,13 @@ typedef context::CDList<Node> NodeList;
 class ExpandingDefinitionsPass : public PreprocessingPass {
  public:   
   virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess);
-  ExpandingDefinitionsPass(ResourceManager* resourceManager, TimerStat definitionExpansionTime);
+  ExpandingDefinitionsPass(ResourceManager* resourceManager, SmtEngine* smt, TimerStat definitionExpansionTime);
  private:
+  SmtEngine* d_smt;
   TimerStat d_definitionExpansionTime;
-  Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly);
+  Node expandDefinitions(TNode n, NodeToNodeHashMap& cache,
+                         bool expandOnly = false)
+      throw(TypeCheckingException, LogicException, UnsafeInterruptException);
 };
  
 class NlExtPurifyPass : public PreprocessingPass {
@@ -82,6 +86,16 @@ class BVAbstractionPass : public PreprocessingPass {
   void bvAbstraction(AssertionPipeline* assertionsToPreprocess);  
 };
 
+class ConstrainSubtypesPass : public PreprocessingPass {
+ public:
+  virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess);
+  ConstrainSubtypesPass(ResourceManager* resourceManager, SmtEngine* smt);
+ private:
+  SmtEngine* d_smt;
+  void constrainSubtypes(TNode n, AssertionPipeline& assertions)
+    throw();
+};
+
 class UnconstrainedSimpPass : public PreprocessingPass {
  public:
   virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess);
@@ -201,7 +215,8 @@ class NoConflictPass : public PreprocessingPass {
      unsigned d_realAssertionsEnd;
      IteSkolemMap* d_iteSkolemMap;
 }; 
- 
+
+/* 
 class RepeatSimpPass : public PreprocessingPass {
   public:
      virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess);
@@ -221,11 +236,21 @@ class SimplifyAssertionsPass : public PreprocessingPass {
   public:
      virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess) throw(TypeCheckingException, LogicException,
                                   UnsafeInterruptException);
-     SimplifyAssertionsPass(ResourceManager* resourceManager, unsigned simplifyAssertionsDepth);
+     SimplifyAssertionsPass(ResourceManager* resourceManager, unsigned simplifyAssertionsDepth, SmtEngine* smt, bool propagatorNeedsFinish, theory::booleans::CircuitPropagator propagator, context::CDO<unsigned> substitutionsIndex, std::vector<Node> nonClausalLearnedLiterals, Node dtrue, TimerStat nonclausalSimplificationTime);
   private:
-     unsigned d_simplifyAssertionsDepth;
- 
+   unsigned d_simplifyAssertionsDepth;
+   SmtEngine* d_smt;
+   bool d_propagatorNeedsFinish;
+   theory::booleans::CircuitPropagator d_propagator;
+   context::CDO<unsigned> d_substitutionsIndex;
+   std::vector<Node> d_nonClausalLearnedLiterals;
+   Node d_true;
+   TimerStat d_nonclausalSimplificationTime;
+   bool nonClausalSimplify(AssertionPipeline &d_assertions);
+   void addFormula(TNode n, bool inUnsatCore, bool inInput = true, AssertionPipeline d_assertions)
+    throw(TypeCheckingException, LogicException);
 };
+*/
  
 }  // namespace preproc
 }  // namespace CVC4
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d61639ad0..f43e6533e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -144,7 +144,8 @@ public:
  * support getValue() over defined functions, to support user output
  * in terms of defined functions, etc.
  */
-class DefinedFunction {
+
+/*class DefinedFunction {
   Node d_func;
   vector<Node> d_formals;
   Node d_formula;
@@ -158,7 +159,8 @@ public:
   Node getFunction() const { return d_func; }
   vector<Node> getFormals() const { return d_formals; }
   Node getFormula() const { return d_formula; }
-};/* class DefinedFunction */
+};*/
+/* class DefinedFunction */
 
 /*class AssertionPipeline {
   vector<Node> d_nodes;
@@ -1014,7 +1016,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_userContext->push();
   d_context->push();
 
-  d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
+  d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); 
   d_fmfRecFunctionsDefined = new(true) NodeList(d_userContext);
   d_modelCommands = new(true) smt::CommandList(d_userContext);
 }
@@ -3498,16 +3500,10 @@ void SmtEnginePrivate::processAssertions() {
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-definition-expansion" << endl;
   dumpAssertions("pre-definition-expansion", d_assertions);
   {
-/*   preproc::ExpandingDefinitionsPass pass(d_resourceManager, d_smt.d_stats->d_definitionExpansionTime);
-   pass.apply(&d_assertions);*/
-    Chat() << "expanding definitions..." << endl;
-    Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
-    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
-    unordered_map<Node, Node, NodeHashFunction> cache;
-    for(unsigned i = 0; i < d_assertions.size(); ++ i) {
-      d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
-    }
-  }
+  preproc::ExpandingDefinitionsPass pass(d_resourceManager, &d_smt, d_smt.d_stats->d_definitionExpansionTime);
+   pass.apply(&d_assertions);
+ }
+
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-definition-expansion" << endl;
   dumpAssertions("post-definition-expansion", d_assertions);
 
@@ -3567,6 +3563,18 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
+<<<<<<< e79fa19f8eacdeab55089cdfec717574b9b7af34
+=======
+  dumpAssertions("pre-constrain-subtypes", d_assertions);
+  {
+    preproc::ConstrainSubtypesPass pass(d_resourceManager, &d_smt);
+    pass.apply(&d_assertions);
+ }
+  dumpAssertions("post-constrain-subtypes", d_assertions);
+
+  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
+
+>>>>>>> ContrainSubtypes and ExpandingDefinitions classes
   bool noConflict = true;
 
   // Unconstrained simplification
@@ -3690,12 +3698,12 @@ void SmtEnginePrivate::processAssertions() {
 
   dumpAssertions("pre-repeat-simplify", d_assertions);
   if(options::repeatSimp()) {
-     preproc::SimplifyAssertionsPass pass(d_resourceManager, d_simplifyAssertionsDepth);
+/*     preproc::SimplifyAssertionsPass pass(d_resourceManager, d_simplifyAssertionsDepth, &d_smt, d_propagatorNeedsFinish, d_propagator, d_substitutionsIndex, d_nonClausalLearnedLiterals, d_true, d_smt.d_stats->d_nonclausalSimplificationTime);
      noConflict &= pass.apply(&d_assertions).d_noConflict;
 
      preproc::RepeatSimpPass pass1(d_resourceManager, &d_topLevelSubstitutions, d_simplifyAssertionsDepth, &noConflict, d_iteSkolemMap, d_realAssertionsEnd); 
-     pass1.apply(&d_assertions);
-/*    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl;
+     pass1.apply(&d_assertions);*/
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl;
     Chat() << "re-simplifying assertions..." << endl;
     ScopeCounter depth(d_simplifyAssertionsDepth);
     noConflict &= simplifyAssertions();
@@ -3761,7 +3769,7 @@ void SmtEnginePrivate::processAssertions() {
       removeITEs();
       //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
     }
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;*/
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;
   }
   dumpAssertions("post-repeat-simplify", d_assertions);
 
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 1202b4ff6..dd4906aad 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -81,7 +81,7 @@ namespace smt {
    * support getValue() over defined functions, to support user output
    * in terms of defined functions, etc.
    */
-  class DefinedFunction;
+//  class DefinedFunction;
 
   struct SmtEngineStatistics;
   class SmtEnginePrivate;
@@ -99,8 +99,12 @@ namespace theory {
 }/* CVC4::theory namespace */
 
 namespace preproc{
+  class DefinedFunction;
   class DoStaticLearningPass; 
   class QuantifiedPass;
+  class SimplifyAssertionsPass;
+  class ExpandingDefinitionsPass;
+  class ConstrainSubtypesPass;
 }/* CVC4::preproc namespace */
 
 // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the
@@ -116,7 +120,7 @@ namespace preproc{
 
 class CVC4_PUBLIC SmtEngine {
   /** The type of our internal map of defined functions */
-  typedef context::CDHashMap<Node, smt::DefinedFunction, NodeHashFunction>
+  typedef context::CDHashMap<Node, preproc::DefinedFunction, NodeHashFunction>
     DefinedFunctionMap;
   /** The type of our internal assertion list */
   typedef context::CDList<Expr> AssertionList;
@@ -345,9 +349,12 @@ class CVC4_PUBLIC SmtEngine {
    * be called when d_logic is updated.
    */
   void setLogicInternal() throw();
-  
+  friend class ::CVC4::preproc::DefinedFunction; 
   friend class ::CVC4::preproc::DoStaticLearningPass;
   friend class ::CVC4::preproc::QuantifiedPass; 
+  friend class ::CVC4::preproc::SimplifyAssertionsPass;
+  friend class ::CVC4::preproc::ExpandingDefinitionsPass;
+  friend class ::CVC4::preproc::ConstrainSubtypesPass;
   friend class ::CVC4::smt::SmtEnginePrivate;
   friend class ::CVC4::smt::SmtScope;
   friend class ::CVC4::smt::BooleanTermConverter;