From 2c2f05c96e021006275a2bc70b9ede70b280616d Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Wed, 16 Sep 2020 12:45:01 -0500
Subject: Dump commands in internal code using command printing functions.
 (#5040)

This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
---
 src/theory/quantifiers/skolemize.h                        | 3 +++
 src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp | 1 +
 2 files changed, 4 insertions(+)

(limited to 'src/theory/quantifiers')

diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index f5c13b183..0e1c5f6ce 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -26,6 +26,9 @@
 #include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
+
+class DTypeConstructor;
+
 namespace theory {
 namespace quantifiers {
 
diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
index b89015b00..bd9697084 100644
--- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp
@@ -17,6 +17,7 @@
 #include "expr/dtype.h"
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
+#include "smt/command.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/ematching/trigger.h"
 #include "theory/quantifiers/first_order_model.h"
-- 
cgit v1.2.3