summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/synth_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/synth_engine.cpp')
-rw-r--r--src/theory/quantifiers/sygus/synth_engine.cpp6
1 files changed, 2 insertions, 4 deletions
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 1d71af6b4..811730d4a 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -21,18 +21,16 @@
#include "theory/quantifiers/term_registry.h"
using namespace CVC4::kind;
-using namespace std;
namespace CVC4 {
namespace theory {
namespace quantifiers {
-SynthEngine::SynthEngine(QuantifiersEngine* qe,
- QuantifiersState& qs,
+SynthEngine::SynthEngine(QuantifiersState& qs,
QuantifiersInferenceManager& qim,
QuantifiersRegistry& qr,
TermRegistry& tr)
- : QuantifiersModule(qs, qim, qr, tr, qe), d_conj(nullptr), d_sqp()
+ : QuantifiersModule(qs, qim, qr, tr), d_conj(nullptr), d_sqp()
{
d_conjs.push_back(std::unique_ptr<SynthConjecture>(
new SynthConjecture(qs, qim, qr, tr, d_statistics)));
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback