From ca1b17c8bba3681643a1a3de19d32b038c38aceb Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 12 Sep 2016 15:48:11 -0500 Subject: Refactor prenex modes. --- src/options/options_handler.cpp | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) (limited to 'src/options/options_handler.cpp') diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 8cd651da5..1d7355d9f 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -385,15 +385,18 @@ max \n\ const std::string OptionsHandler::s_prenexQuantModeHelp = "\ Prenex quantifiers modes currently supported by the --prenex-quant option:\n\ \n\ -default \n\ -+ Default, prenex all nested quantifiers except those with user patterns.\n\ -\n\ -all \n\ -+ Prenex all nested quantifiers.\n\ -\n\ none \n\ + Do no prenex nested quantifiers. \n\ \n\ +default | simple \n\ ++ Default, do simple prenexing of same sign quantifiers.\n\ +\n\ +dnorm \n\ ++ Prenex to disjunctive prenex normal form.\n\ +\n\ +norm \n\ ++ Prenex to prenex normal form.\n\ +\n\ "; const std::string OptionsHandler::s_cegqiFairModeHelp = "\ @@ -679,12 +682,14 @@ theory::quantifiers::TriggerActiveSelMode OptionsHandler::stringToTriggerActiveS } theory::quantifiers::PrenexQuantMode OptionsHandler::stringToPrenexQuantMode(std::string option, std::string optarg) throw(OptionException) { - if(optarg == "default" ) { - return theory::quantifiers::PRENEX_NO_USER_PAT; - } else if(optarg == "all") { - return theory::quantifiers::PRENEX_ALL; + if(optarg== "default" || optarg== "simple" ) { + return theory::quantifiers::PRENEX_QUANT_SIMPLE; } else if(optarg == "none") { - return theory::quantifiers::PRENEX_NONE; + return theory::quantifiers::PRENEX_QUANT_NONE; + } else if(optarg == "dnorm") { + return theory::quantifiers::PRENEX_QUANT_DISJ_NORMAL; + } else if(optarg == "norm") { + return theory::quantifiers::PRENEX_QUANT_NORMAL; } else if(optarg == "help") { puts(s_prenexQuantModeHelp.c_str()); exit(1); -- cgit v1.2.3