8 files changed, 28 insertions, 139 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index a26947ed1..f7f7f9ddd 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -19,20 +19,19 @@
 
 #pragma once
 
-#include <queue>
 #include <deque>
-#include <vector>
 #include <ext/hash_map>
+#include <queue>
+#include <vector>
 
-#include "expr/node.h"
-#include "expr/kind_map.h"
-#include "context/cdo.h"
+#include "base/output.h"
 #include "context/cdhashmap.h"
-#include "util/output.h"
-#include "util/statistics_registry.h"
+#include "context/cdo.h"
+#include "expr/kind_map.h"
+#include "expr/node.h"
+#include "expr/statistics_registry.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
-
 #include "theory/uf/equality_engine_types.h"
 
 namespace CVC4 {
diff --git a/src/theory/uf/options b/src/theory/uf/options
deleted file mode 100644
index cb6ddc0fa..000000000
--- a/src/theory/uf/options
+++ /dev/null
@@ -1,42 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module UF "theory/uf/options.h" Uninterpreted functions theory
-
-option ufSymmetryBreaker uf-symmetry-breaker --symmetry-breaker bool :read-write :default true
- use UF symmetry breaker (Deharbe et al., CADE 2011)
-
-option condenseFunctionValues condense-function-values --condense-function-values bool :default true
- condense models for functions rather than explicitly representing them
-
-option ufssRegions /--disable-uf-ss-regions bool :default true
- disable region-based method for discovering cliques and splits in uf strong solver
-option ufssEagerSplits --uf-ss-eager-split bool :default false
- add splits eagerly for uf strong solver
-option ufssTotality --uf-ss-totality bool :default false
- always use totality axioms for enforcing cardinality constraints
-option ufssTotalityLimited --uf-ss-totality-limited=N int :default -1
- apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)
-option ufssTotalitySymBreak --uf-ss-totality-sym-break bool :default false
- apply symmetry breaking for totality axioms
-option ufssAbortCardinality --uf-ss-abort-card=N int :default -1
- tells the uf strong solver a cardinality to abort at (-1 == no limit, default)
-option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
- use explained clique lemmas for uf strong solver
-option ufssSimpleCliques --uf-ss-simple-cliques bool :default true
- always use simple clique lemmas for uf strong solver
-option ufssDiseqPropagation --uf-ss-deq-prop bool :default false
- eagerly propagate disequalities for uf strong solver
-option ufssMode --uf-ss=MODE CVC4::theory::uf::UfssMode :default CVC4::theory::uf::UF_SS_FULL :include "theory/uf/options_handlers.h" :handler CVC4::theory::uf::stringToUfssMode :handler-include "theory/uf/options_handlers.h"
- mode of operation for uf strong solver.
-option ufssCliqueSplits --uf-ss-clique-splits bool :default false
- use cliques instead of splitting on demand to shrink model
-
-option ufssSymBreak --uf-ss-sym-break bool :default false
- finite model finding symmetry breaking techniques
-option ufssFairness --uf-ss-fair bool :default true
- use fair strategy for finite model finding multiple sorts
-
-endmodule
diff --git a/src/theory/uf/options_handlers.h b/src/theory/uf/options_handlers.h
deleted file mode 100644
index 8c072e232..000000000
--- a/src/theory/uf/options_handlers.h
+++ /dev/null
@@ -1,70 +0,0 @@
-/*********************                                                        */
-/*! \file options_handlers.h
- ** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Andrew Reynolds
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Custom handlers and predicates for TheoryUF options
- **
- ** Custom handlers and predicates for TheoryUF options.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__UF__OPTIONS_HANDLERS_H
-#define __CVC4__THEORY__UF__OPTIONS_HANDLERS_H
-
-namespace CVC4 {
-namespace theory {
-namespace uf {
-  
-typedef enum {
-  /** default, use uf strong solver to find minimal models for uninterpreted sorts */
-  UF_SS_FULL,
-  /** use uf strong solver to shrink model sizes, but do no enforce minimality */
-  UF_SS_NO_MINIMAL,
-  /** do not use uf strong solver */
-  UF_SS_NONE,
-} UfssMode;
-  
-static const std::string ufssModeHelp = "\
-UF strong solver options currently supported by the --uf-ss option:\n\
-\n\
-full \n\
-+ Default, use uf strong solver to find minimal models for uninterpreted sorts.\n\
-\n\
-no-minimal \n\
-+ Use uf strong solver to shrink model sizes, but do no enforce minimality.\n\
-\n\
-none \n\
-+ Do not use uf strong solver to shrink model sizes. \n\
-\n\
-";
-
-inline UfssMode stringToUfssMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg ==  "default" || optarg == "full" ) {
-    return UF_SS_FULL;
-  } else if(optarg == "no-minimal") {
-    return UF_SS_NO_MINIMAL;
-  } else if(optarg == "none") {
-    return UF_SS_NONE;
-  } else if(optarg ==  "help") {
-    puts(ufssModeHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --uf-ss: `") +
-                          optarg + "'.  Try --uf-ss help.");
-  }
-}
-
-}/* CVC4::theory::uf namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__UF__OPTIONS_HANDLERS_H */
-
diff --git a/src/theory/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index d07ef64e0..e49b4652a 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -48,11 +48,11 @@
 #include <list>
 #include <vector>
 
+#include "context/cdlist.h"
+#include "context/context.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "context/context.h"
-#include "context/cdlist.h"
-#include "util/statistics_registry.h"
+#include "expr/statistics_registry.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 6679b5dc2..31bee316a 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -16,12 +16,13 @@
  **/
 
 #include "theory/uf/theory_uf.h"
-#include "theory/uf/options.h"
-#include "smt/options.h"
-#include "theory/quantifiers/options.h"
-#include "theory/uf/theory_uf_strong_solver.h"
+
+#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "options/uf_options.h"
 #include "theory/theory_model.h"
 #include "theory/type_enumerator.h"
+#include "theory/uf/theory_uf_strong_solver.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index 64f06ceb7..6d0123a19 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -12,16 +12,18 @@
  ** \brief Implementation of Theory UF Model
  **/
 
+#include "theory/uf/theory_uf_model.h"
+
+#include <stack>
+#include <vector>
+
 #include "expr/attribute.h"
+#include "options/quantifiers_options.h"
+#include "theory/quantifiers/term_database.h"
 #include "theory/theory_engine.h"
-#include "theory/uf/theory_uf_model.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/uf/theory_uf.h"
-#include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/options.h"
 
-#include <vector>
-#include <stack>
 
 #define RECONSIDER_FUNC_DEFAULT_VALUE
 #define USE_PARTIAL_DEFAULT_VALUES
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 29e726da7..d617207cf 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -13,12 +13,13 @@
  **/
 
 #include "theory/uf/theory_uf_strong_solver.h"
+
+#include "options/uf_options.h"
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/equality_engine.h"
 #include "theory/theory_engine.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/quantifiers/term_database.h"
-#include "theory/uf/options.h"
 #include "theory/theory_model.h"
 #include "theory/quantifiers/symmetry_breaking.h"
 
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 3e612ff1f..dd32154d9 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -17,14 +17,12 @@
 #ifndef __CVC4__THEORY_UF_STRONG_SOLVER_H
 #define __CVC4__THEORY_UF_STRONG_SOLVER_H
 
-#include "theory/theory.h"
-
+#include "context/cdchunk_list.h"
+#include "context/cdhashmap.h"
 #include "context/context.h"
 #include "context/context_mm.h"
-#include "context/cdhashmap.h"
-#include "context/cdchunk_list.h"
-
-#include "util/statistics_registry.h"
+#include "expr/statistics_registry.h"
+#include "theory/theory.h"
 
 namespace CVC4 {