From a33e9e4400b924f031100a9e498b2180bb025665 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 24 Oct 2017 17:58:58 -0500 Subject: [PATCH] Removing deprecated file. (#1270) --- src/Makefile.am | 2 - .../quantifiers/ce_guided_single_inv.cpp | 1 - .../quantifiers/ce_guided_single_inv_ei.cpp | 47 ------------------- .../quantifiers/ce_guided_single_inv_ei.h | 43 ----------------- 4 files changed, 93 deletions(-) delete mode 100644 src/theory/quantifiers/ce_guided_single_inv_ei.cpp delete mode 100644 src/theory/quantifiers/ce_guided_single_inv_ei.h diff --git a/src/Makefile.am b/src/Makefile.am index 76d95ea4b..7f9d5a84b 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -358,8 +358,6 @@ libcvc4_la_SOURCES = \ theory/quantifiers/ce_guided_instantiation.h \ theory/quantifiers/ce_guided_single_inv.cpp \ theory/quantifiers/ce_guided_single_inv.h \ - theory/quantifiers/ce_guided_single_inv_ei.cpp \ - theory/quantifiers/ce_guided_single_inv_ei.h \ theory/quantifiers/ce_guided_pbe.cpp \ theory/quantifiers/ce_guided_pbe.h \ theory/quantifiers/ce_guided_single_inv_sol.cpp \ diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp index 3349492a2..9d2d2fe98 100644 --- a/src/theory/quantifiers/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/ce_guided_single_inv.cpp @@ -17,7 +17,6 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" #include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/ce_guided_single_inv_ei.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quant_util.h" #include "theory/quantifiers/term_database_sygus.h" diff --git a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp deleted file mode 100644 index 1d0dc7bd4..000000000 --- a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp +++ /dev/null @@ -1,47 +0,0 @@ -/********************* */ -/*! \file ce_guided_single_inv_ei.cpp - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, Tim King - ** 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 utility for inferring entailments for cegqi - ** - **/ - -#include "options/quantifiers_options.h" -#include "theory/quantifiers/ce_guided_instantiation.h" -#include "theory/quantifiers/ce_guided_single_inv_ei.h" -#include "theory/quantifiers/quant_util.h" -#include "theory/quantifiers/term_database.h" -#include "theory/theory_engine.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::theory; -using namespace CVC4::theory::quantifiers; -using namespace std; - -namespace CVC4 { - -CegEntailmentInfer::CegEntailmentInfer( QuantifiersEngine * qe, SingleInvocationPartition * sip ) : d_qe( qe ), d_sip( sip ) { - -} - -bool CegEntailmentInfer::getEntailedConjecture( Node& conj, Node& exp ) { - if( Trace.isOn("cegqi-ei") ){ - Trace("cegqi-ei") << "Infer new conjecture from : " << std::endl; - d_sip->debugPrint( "cegqi-ei" ); - Trace("cegqi-ei") << "Current assertions : " << std::endl; - d_qe->getTheoryEngine()->printAssertions("cegqi-ei"); - } - - - return false; -} - -} diff --git a/src/theory/quantifiers/ce_guided_single_inv_ei.h b/src/theory/quantifiers/ce_guided_single_inv_ei.h deleted file mode 100644 index 9964d32f2..000000000 --- a/src/theory/quantifiers/ce_guided_single_inv_ei.h +++ /dev/null @@ -1,43 +0,0 @@ -/********************* */ -/*! \file ce_guided_single_inv_ei.h - ** \verbatim - ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng - ** 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 utility for inferring entailments for cegqi - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_ENTAILMENT_INFERENCE_H -#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_ENTAILMENT_INFERENCE_H - - -#include "theory/quantifiers/ce_guided_single_inv.h" - -namespace CVC4 { -namespace theory { -namespace quantifiers { - -class CegEntailmentInfer { -private: - QuantifiersEngine * d_qe; - SingleInvocationPartition * d_sip; -public: - CegEntailmentInfer( QuantifiersEngine * qe, SingleInvocationPartition * sip ); - virtual ~CegEntailmentInfer(){} - - bool getEntailedConjecture( Node& conj, Node& exp ); -}; - - -} -} -} - -#endif -- 2.30.2