remove BFNT

CMakeLists.txt

@@ -508,8 +508,6 @@ source_group(saturation_source_files FILES ${VAMPIRE_SATURATION_SOURCES})
 set(VAMPIRE_SHELL_SOURCES
     Shell/AnswerExtractor.cpp
     #Shell/AxiomGenerator.cpp
-    Shell/BFNT.cpp
-    Shell/BFNTMainLoop.cpp
     Shell/CommandLine.cpp
     Shell/CNF.cpp
     Shell/NewCNF.cpp
@@ -579,8 +577,6 @@ set(VAMPIRE_SHELL_SOURCES
     #Shell/SubsumptionRemover.cpp
     Shell/AnswerExtractor.hpp
     #Shell/AxiomGenerator.hpp
-    Shell/BFNT.hpp
-    Shell/BFNTMainLoop.hpp
     Shell/CommandLine.hpp
     Shell/CNF.hpp
     Shell/NewCNF.hpp

FMB/ClauseFlattening.cpp

@@ -71,8 +71,6 @@ bool ClauseFlattening::isShallow(Literal* lit)
  * Apply equality resolution to all negative equalities between variables
  * in cl and return the result. If cl contains no such inequalities, return cl
  * itself.
- *
- * Copied from BFNT, put here in case we remove BFNT 
  */
 Clause* ClauseFlattening::resolveNegativeVariableEqualities(Clause* cl)
 {
@@ -126,8 +124,6 @@ Clause* ClauseFlattening::resolveNegativeVariableEqualities(Clause* cl)
 /**
  * Flatten clauses
  *
- * Largely based on BFNT::apply
- *
  * @author Giles
  */
 Clause* ClauseFlattening::flatten(Clause* cl)

Kernel/Inference.cpp

@@ -853,12 +853,6 @@ vstring Kernel::ruleName(InferenceRule rule)
     return "external";
   case InferenceRule::CLAIM_DEFINITION:
     return "claim definition";
-  case InferenceRule::BFNT_FLATTENING:
-    return "bfnt flattening";
-  case InferenceRule::BFNT_DISTINCT:
-    return "bfnt distinct";
-  case InferenceRule::BFNT_TOTALITY:
-    return "bfnt totality";
   case InferenceRule::FMB_FLATTENING:
     return "flattening (finite model building)";
   case InferenceRule::FMB_FUNC_DEF:

Kernel/Inference.hpp

@@ -329,13 +329,6 @@ enum class InferenceRule : unsigned char {
   /** inference coming from outside of Vampire */
   EXTERNAL,
 
-  /** BNFT flattening */
-  BFNT_FLATTENING,
-  /** BNFT axioms m != n */
-  BFNT_DISTINCT,
-  /** BNFT totality axioms R(x,1) \/ ... \/ R(x,n) */
-  BFNT_TOTALITY,
-
   /* FMB flattening */
   FMB_FLATTENING,
   /* Functional definition for FMB */
@@ -745,7 +738,7 @@ class Inference
    * - integer/rational/real theory axioms are internal theory axioms
    * - term algebra axioms are internal theory axioms
    * - FOOL axioms are internal theory axioms
-   * - equality-proxy-axioms, SimplifyProver’s-distinct-number-axioms, and BFNT-axioms
+   * - equality-proxy-axioms
    *   are not treated as internal theory axioms, since they are not generated in TheoryAxioms
    *   (these axioms should probably be refactored into TheoryAxioms at some point)
    * - consequences of theory axioms are not theory axioms

Kernel/MainLoop.cpp

@@ -38,7 +38,6 @@
 
 #include "SAT/Z3MainLoop.hpp"
 
-#include "Shell/BFNTMainLoop.hpp"
 #include "Shell/Options.hpp"
 #include "Shell/UIHelper.hpp"
 
@@ -111,10 +110,6 @@ MainLoop* MainLoop::createFromOptions(Problem& prb, const Options& opt)
 {
   CALL("MainLoop::createFromOptions");
 
-  if(opt.bfnt()) {
-    return new BFNTMainLoop(prb, opt);
-  }
-
 #if VZ3
   bool isComplete = false; // artificially prevent smtForGround from running
 

Kernel/Signature.cpp

@@ -133,7 +133,7 @@ void Signature::Symbol::addToDistinctGroup(unsigned group,unsigned this_number)
   env.signature->_distinctGroupsAddedTo=true;
 
   Signature::DistinctGroupMembers members = env.signature->_distinctGroupMembers[group];
-  if(members->size() <= DistinctGroupExpansion::EXPAND_UP_TO_SIZE || env.options->bfnt()
+  if(members->size() <= DistinctGroupExpansion::EXPAND_UP_TO_SIZE
                        || env.options->saturationAlgorithm()==Options::SaturationAlgorithm::FINITE_MODEL_BUILDING){
     // we add one more than EXPAND_UP_TO_SIZE to signal to DistinctGroupExpansion::apply not to expand
     // ... instead DistinctEqualitySimplifier will take over

Makefile

@@ -343,8 +343,6 @@ VST_OBJ= Saturation/AWPassiveClauseContainer.o\
          Saturation/ManCSPassiveClauseContainer.o\
 
 VS_OBJ = Shell/AnswerExtractor.o\
-         Shell/BFNT.o\
-         Shell/BFNTMainLoop.o\
          Shell/CommandLine.o\
          Shell/CNF.o\
          Shell/NewCNF.o\
@@ -532,7 +530,7 @@ VAMP_DIRS := Api Debug DP Lib Lib/Sys Kernel FMB Indexing Inferences InstGen She
 
 VAMP_BASIC := $(MINISAT_OBJ) $(VD_OBJ) $(VL_OBJ) $(VLS_OBJ) $(VK_OBJ) $(BP_VD_OBJ) $(BP_VL_OBJ) $(BP_VLS_OBJ) $(BP_VSOL_OBJ) $(BP_VT_OBJ) $(BP_MPS_OBJ) $(ALG_OBJ) $(VI_OBJ) $(VINF_OBJ) $(VIG_OBJ) $(VSAT_OBJ) $(DP_OBJ) $(VST_OBJ) $(VS_OBJ) $(PARSE_OBJ) $(VFMB_OBJ)
 #VCLAUSIFY_BASIC := $(VD_OBJ) $(VL_OBJ) $(VLS_OBJ) $(VK_OBJ) $(ALG_OBJ) $(VI_OBJ) $(VINF_OBJ) $(VSAT_OBJ) $(VST_OBJ) $(VS_OBJ) $(VT_OBJ)
-VCLAUSIFY_BASIC := $(VD_OBJ) $(VL_OBJ) $(VLS_OBJ) $(filter-out Shell/InterpolantMinimizer.o Shell/AnswerExtractor.o Shell/BFNTMainLoop.o, $(VS_OBJ)) $(PARSE_OBJ) $(LIB_DEP) $(OTHER_CL_DEP) 
+VCLAUSIFY_BASIC := $(VD_OBJ) $(VL_OBJ) $(VLS_OBJ) $(filter-out Shell/InterpolantMinimizer.o Shell/AnswerExtractor.o, $(VS_OBJ)) $(PARSE_OBJ) $(LIB_DEP) $(OTHER_CL_DEP)
 VSAT_BASIC := $(VD_OBJ) $(VL_OBJ) $(VLS_OBJ) $(VSAT_OBJ) Test/CheckedSatSolver.o $(LIB_DEP)
 #VGROUND_BASIC := $(VD_OBJ) $(VL_OBJ) $(VK_OBJ) $(VI_OBJ) $(VSAT_OBJ) $(VS_OBJ) $(VT_OBJ)