rm decision/relevancy

1 files changed, 0 insertions, 50 deletions

diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h
index 05d975ef1..44a623970 100644
--- a/src/decision/options_handlers.h
+++ b/src/decision/options_handlers.h
@@ -37,31 +37,8 @@ justification\n\
 justification-stoponly\n\
 + Use the justification heuristic only to stop early, not for decisions\n\
 ";
-/** Under-development options, commenting out from help for the release */
-/*
-\n\
-relevancy\n\
-+ Under development may-relevancy\n\
-\n\
-relevancy-leaves\n\
-+ May-relevancy, but decide only on leaves\n\
-\n\
-Developer modes:\n\
-\n\
-justification-rel\n\
-+ Use the relevancy code to do the justification stuff\n\
-+ (This should do exact same thing as justification)\n\
-\n\
-justification-must\n\
-+ Start deciding on literals close to root instead of those\n\
-+ near leaves (don't expect it to work well) [Unimplemented]\n\
-";*/
 
 inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  options::decisionRelevancyLeaves.set(false);
-  options::decisionMaxRelTimeAsPermille.set(1000);
-  options::decisionComputeRelevancy.set(true);
-  options::decisionMustRelevancy.set(false);
   options::decisionStopOnly.set(false);
 
   if(optarg == "internal") {
@@ -71,25 +48,6 @@ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg,
   } else if(optarg == "justification-stoponly") {
     options::decisionStopOnly.set(true);
     return DECISION_STRATEGY_JUSTIFICATION;
-  } else if(optarg == "relevancy") {
-    options::decisionRelevancyLeaves.set(false);
-    return DECISION_STRATEGY_RELEVANCY;
-  } else if(optarg == "relevancy-leaves") {
-    options::decisionRelevancyLeaves.set(true);
-    Trace("options") << "version is " << options::version() << std::endl;
-    return DECISION_STRATEGY_RELEVANCY;
-  } else if(optarg == "justification-rel") {
-    // relevancyLeaves : irrelevant
-    // maxRelTimeAsPermille : irrelevant
-    options::decisionComputeRelevancy.set(false);
-    options::decisionMustRelevancy.set(false);
-    return DECISION_STRATEGY_RELEVANCY;
-  } else if(optarg == "justification-must") {
-    // relevancyLeaves : irrelevant
-    // maxRelTimeAsPermille : irrelevant
-    options::decisionComputeRelevancy.set(false);
-    options::decisionMustRelevancy.set(true);
-    return DECISION_STRATEGY_RELEVANCY;
   } else if(optarg == "help") {
     puts(decisionModeHelp.c_str());
     exit(1);
@@ -99,14 +57,6 @@ inline DecisionMode stringToDecisionMode(std::string option, std::string optarg,
   }
 }
 
-inline void checkDecisionBudget(std::string option, unsigned short budget, SmtEngine* smt) throw(OptionException) {
-  if(budget == 0) {
-    Warning() << "Decision budget is 0. Consider using internal decision heuristic and "
-              << std::endl << " removing this option." << std::endl;
-              
-  }
-}
-
 inline DecisionWeightInternal stringToDecisionWeightInternal(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "off")
     return DECISION_WEIGHT_INTERNAL_OFF;