Removing deprecated file. (#1270)

diff --git a/src/Makefile.am b/src/Makefile.am
index 76d95ea4b9eae08cbefc52f8f1648a63089ce909..7f9d5a84bbafb27d7725cb3bac4bfb5d654638c2 100644 (file)
--- 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 3349492a217a98718201ab9a2f7a855b9f054bff..9d2d2fe9842dc95db9b675edf7dc112acaf9e5d2 100644 (file)
--- 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 (file)
index 1d0dc7b..0000000
--- 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 (file)
index 9964d32..0000000
--- 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