From c1d9bed7f73db9567f635f59cde134795e65c9ba Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 1 Aug 2019 09:26:26 -0500
Subject: Move some generic utilities out of quantifiers (#3139)

---
 src/preprocessing/passes/symmetry_detect.h   | 4 ++--
 src/preprocessing/passes/synth_rew_rules.cpp | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/preprocessing')

diff --git a/src/preprocessing/passes/symmetry_detect.h b/src/preprocessing/passes/symmetry_detect.h
index 07a545723..deb1accd7 100644
--- a/src/preprocessing/passes/symmetry_detect.h
+++ b/src/preprocessing/passes/symmetry_detect.h
@@ -21,7 +21,7 @@
 #include <string>
 #include <vector>
 #include "expr/node.h"
-#include "theory/quantifiers/term_canonize.h"
+#include "expr/term_canonize.h"
 
 namespace CVC4 {
 namespace preprocessing {
@@ -242,7 +242,7 @@ class SymmetryDetect
   Node d_falseNode;
 
   /** term canonizer (for quantified formulas) */
-  theory::quantifiers::TermCanonize d_tcanon;
+  expr::TermCanonize d_tcanon;
 
   /** Cache for partitions */
   std::map<Node, Partition> d_term_partition;
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 3eb27c2f7..6d6e8fb27 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -15,6 +15,7 @@
 
 #include "preprocessing/passes/synth_rew_rules.h"
 
+#include "expr/term_canonize.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -22,7 +23,6 @@
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
-#include "theory/quantifiers/term_canonize.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
@@ -218,7 +218,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
   std::vector<Node> cterms;
   // canonical terms for each type
   std::map<TypeNode, std::vector<Node> > t_cterms;
-  theory::quantifiers::TermCanonize tcanon;
+  expr::TermCanonize tcanon;
   for (unsigned i = 0, nterms = terms.size(); i < nterms; i++)
   {
     Node n = terms[i];
-- 
cgit v1.2.3