From 5eafdb88526da64b60009e30bb45b7e0e47d360b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 1 Mar 2018 21:32:11 -0600 Subject: Create infrastructure for sygus modules (#1632) --- src/theory/quantifiers/sygus/sygus_module.cpp | 28 +++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 src/theory/quantifiers/sygus/sygus_module.cpp (limited to 'src/theory/quantifiers/sygus/sygus_module.cpp') diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp new file mode 100644 index 000000000..19e064350 --- /dev/null +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -0,0 +1,28 @@ +/********************* */ +/*! \file sygus_module.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of sygus_module + **/ + +#include "theory/quantifiers/sygus/sygus_module.h" + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +SygusModule::SygusModule(QuantifiersEngine* qe, CegConjecture* p) + : d_qe(qe), d_parent(p) +{ +} + +} /* CVC4::theory::quantifiers namespace */ +} /* CVC4::theory namespace */ +} /* CVC4 namespace */ -- cgit v1.2.3