diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-12 19:18:42 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-12 19:18:42 -0500 |
commit | 60ed666d657bfcd69f48821c78a34696796df5fb (patch) | |
tree | c6138be63cc1c3104d355ef38d874c7d294c0a72 /src/theory/quantifiers | |
parent | 08f6f8cc6118b1e6c057a294d1ddb60e2e45b5ed (diff) |
Move sygus datatype utility functions to their own file (#4595)
Separates them from the core datatype utilities.
Code move only.
Diffstat (limited to 'src/theory/quantifiers')
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_abduct.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_eval_unfold.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/synth_conjecture.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/term_database_sygus.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/type_info.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus_inst.cpp | 2 |
7 files changed, 8 insertions, 7 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index ef2e7e445..1508267c3 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -19,7 +19,8 @@ #include "expr/dtype.h" #include "expr/node_algorithm.h" #include "expr/sygus_datatype.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "printer/sygus_print_callback.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/quantifiers_rewriter.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index 9d327bfe1..b8c867934 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -16,7 +16,7 @@ #include "expr/sygus_datatype.h" #include "options/quantifiers_options.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace std; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index f15b6780c..ea129803b 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -20,7 +20,7 @@ #include "options/quantifiers_options.h" #include "printer/sygus_print_callback.h" #include "theory/bv/theory_bv_utils.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" #include "theory/quantifiers/sygus/sygus_process_conj.h" #include "theory/quantifiers/sygus/synth_conjecture.h" diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index bb5307c79..91911e1f0 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -21,7 +21,7 @@ #include "printer/printer.h" #include "prop/prop_engine.h" #include "smt/smt_statistics_registry.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quantifiers_attributes.h" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index f53637ebb..293048e8c 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -21,7 +21,7 @@ #include "options/quantifiers_options.h" #include "printer/printer.h" #include "theory/arith/arith_msum.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/term_util.h" diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp index 7235fd65c..f5a708c8e 100644 --- a/src/theory/quantifiers/sygus/type_info.cpp +++ b/src/theory/quantifiers/sygus/type_info.cpp @@ -17,7 +17,7 @@ #include "base/check.h" #include "expr/dtype.h" #include "expr/sygus_datatype.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/term_database_sygus.h" using namespace CVC4::kind; diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp index 696860302..e927ac249 100644 --- a/src/theory/quantifiers/sygus_inst.cpp +++ b/src/theory/quantifiers/sygus_inst.cpp @@ -18,7 +18,7 @@ #include <unordered_set> #include "expr/node_algorithm.h" -#include "theory/datatypes/theory_datatypes_utils.h" +#include "theory/datatypes/sygus_datatype_utils.h" #include "theory/quantifiers/sygus/sygus_enumerator.h" #include "theory/quantifiers/sygus/sygus_grammar_cons.h" #include "theory/quantifiers/sygus/synth_engine.h" |