summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus
diff options
context:
space:
mode:
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>2021-03-25 18:34:39 +0100
committerGitHub <noreply@github.com>2021-03-25 18:34:39 +0100
commitdc764ce250f0d63714dab76f98bc556f00afb9f0 (patch)
tree8b9fe0825debb75f36b7d48fe09926ebffe99349 /src/theory/quantifiers/sygus
parentb3c6975af6354eb027aa52d6a23386b5dd0ef1cd (diff)
Add missing includes. (#6207)
This PR adds includes that are missing from source files, but currently provided by other includes. This mostly concerns <sstream> which is currently included by the statistics, which will change in the future.
Diffstat (limited to 'src/theory/quantifiers/sygus')
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_cons.cpp1
-rw-r--r--src/theory/quantifiers/sygus/sygus_grammar_norm.cpp2
-rw-r--r--src/theory/quantifiers/sygus/sygus_process_conj.cpp1
-rw-r--r--src/theory/quantifiers/sygus/term_database_sygus.cpp2
4 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 1e58a1f24..7645cc237 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -14,6 +14,7 @@
**/
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include <sstream>
#include <stack>
#include "expr/dtype_cons.h"
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index c72ad20d9..964d64655 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -15,6 +15,8 @@
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
+#include <sstream>
+
#include "expr/dtype_cons.h"
#include "expr/node_manager_attributes.h" // for VarNameAttr
#include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
index 66e322efe..93474b4ae 100644
--- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp
+++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp
@@ -14,6 +14,7 @@
**/
#include "theory/quantifiers/sygus/sygus_process_conj.h"
+#include <sstream>
#include <stack>
#include "options/quantifiers_options.h"
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 50c522d95..e7bbc947a 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -14,6 +14,8 @@
#include "theory/quantifiers/sygus/term_database_sygus.h"
+#include <sstream>
+
#include "base/check.h"
#include "expr/dtype_cons.h"
#include "expr/sygus_datatype.h"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback