From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 24 Oct 2017 22:58:58 +0000 (-0500)
Subject: Removing deprecated file. (#1270)
X-Git-Tag: cvc5-1.0.0~5539
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a33e9e4400b924f031100a9e498b2180bb025665;p=cvc5.git

Removing deprecated file. (#1270)
---

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