Structure containing all the command line and other options. More...

#include <Parameters.hpp>

Static Public Member Functions
static void	set_default_schedule ()

static void	set_default_schedule_parameters ()
	Self-explanatory.

static void	set_complete_parameters ()
	Change the parameters to make the search complete.

static bool	search_is_complete ()
	Self-explanatory.

static void	set_all_backtrack ()
	Self-explanatory.

static bool	no_start_options ()
	Self-explanatory.

static void	correct_missing_start_options ()
	Self-explanatory.

static void	set_all_start ()
	Self-explanatory.

static void	show_search_parameter_settings ()
	Give a detailed indication of what the parameters affecting the search are currently set to.

Static Public Attributes
static uint8_t	verbosity = 2

static bool	use_colours = true

static uint8_t	indent_size = 4

static uint8_t	output_width = 7

static uint32_t	output_frequency = 500000

static bool	output_terms_with_substitution = false

static std::string	problem_name = "Unknown"

static bool	write_output_summary = false

static std::string	definitional_predicate_prefix = "def"

static std::string	unique_var_prefix = "_u"

static std::string	unique_skolem_prefix = "skolem"

static bool	show_full_stats = true

static bool	first_parse = true

static bool	miniscope = true

static bool	all_definitional = false

static bool	no_definitional = false

static bool	add_equality_axioms = true

static bool	equality_axioms_at_start = true

static bool	all_distinct_objects = false

static bool	no_distinct_objects = false

static unsigned	random_seed = 0

static uint32_t	boost_random_seed = 0

static bool	deterministic_reorder = false

static uint32_t	number_of_reorders = 0

static bool	random_reorder = false

static bool	random_reorder_literals = false

static bool	timeout = false

static uint32_t	timeout_value = UINT32_MAX

static bool	use_schedule = false

static bool	positive_representation = false

static uint32_t	start_depth = 2

static uint32_t	depth_limit = UINT32_MAX

static uint32_t	depth_increment = 1

static bool	limit_by_tree_depth = false

static bool	depth_limit_all = false

static bool	all_start = false

static bool	all_pos_neg_start = false

static bool	conjecture_start = false

static bool	restrict_start = false

static bool	use_regularity_test = true

static bool	use_lemmata = true

static bool	limit_lemmata = true

static bool	limit_reductions = true

static bool	limit_extensions = true

static bool	limit_bt_all = true

static bool	limit_bt_lemmas = true

static bool	limit_bt_reductions = true

static bool	limit_bt_extensions = true

static bool	limit_bt_extensions_left_tree = true

static uint32_t	switch_to_complete = UINT32_MAX

static bool	poly_unification = false

static bool	verify_proof_verbose = false

static bool	verify_proof = false

static bool	build_proof = false

static bool	generate_LaTeX_proof = false

static bool	sub_LaTeX_proof = false

static int	latex_truncation_length = 25

static bool	latex_tiny_proof = false

static bool	latex_include_matrix = true

static bool	generate_Prolog_proof = false

static bool	generate_tptp_proof = false

static std::filesystem::path	LaTeX_proof_path = "latex_proof.tex"

static std::filesystem::path	Prolog_matrix_path = "matrix.pl"

static std::filesystem::path	Prolog_proof_path = "proof.pl"

static std::filesystem::path	output_summary_path = "output_summary.txt"

static std::filesystem::path	schedule_path = "."

static std::filesystem::path	tptp_path = "."

static std::filesystem::path	pwd_path = "."

static std::filesystem::path	connectpp_path = "."

static std::filesystem::path	full_problem_path

static std::string	default_schedule

static bool	show_clauses = false

Detailed Description

Structure containing all the command line and other options.

Pretty much everything is static, because that makes sense.

There are also a small number of methods for setting defaults and testing for whether the configuration used leads to a complete search.

In most cases the name of the parameter should make it self-explanatory. So parameters are only explicitly documented where necessary.

Definition at line 49 of file Parameters.hpp.

Member Function Documentation

◆ correct_missing_start_options()

void params::correct_missing_start_options ( )

static

Self-explanatory.

Definition at line 254 of file Parameters.cpp.

                                           {
  all_start = false;
  all_pos_neg_start = true;
  conjecture_start = false;
  restrict_start = false;
}

◆ no_start_options()

bool params::no_start_options ( )

static

Self-explanatory.

Definition at line 247 of file Parameters.cpp.

                              {
  return !all_start &&
  !all_pos_neg_start &&
  !conjecture_start && 
  !restrict_start;
}

◆ search_is_complete()

bool params::search_is_complete ( )

static

Self-explanatory.

Definition at line 227 of file Parameters.cpp.

                                {
  bool start_conditions_ok =
    (all_pos_neg_start || all_start) && !restrict_start && !conjecture_start;
 
  // You don't care about lemmas.
  bool backtracking_ok =
    !limit_bt_all && !limit_bt_reductions && !limit_bt_extensions &&
    !limit_bt_extensions_left_tree;
 
  return start_conditions_ok && backtracking_ok;
}

◆ set_all_backtrack()

void params::set_all_backtrack ( )

static

Self-explanatory.

Definition at line 239 of file Parameters.cpp.

                               {
  limit_bt_all = false;
  limit_bt_lemmas = false;
  limit_bt_reductions = false;
  limit_bt_extensions = false;
  limit_bt_extensions_left_tree = false;
}

◆ set_all_start()

void params::set_all_start ( )

static

Self-explanatory.

Definition at line 261 of file Parameters.cpp.

                           {
  all_start = true;
  all_pos_neg_start = false;
  conjecture_start = false;
  restrict_start = false;
}

◆ set_complete_parameters()

void params::set_complete_parameters ( )

static

Change the parameters to make the search complete.

Definition at line 215 of file Parameters.cpp.

                                     {
  all_start = false;
  all_pos_neg_start = true;
  conjecture_start = false;
  restrict_start = false;
 
  limit_bt_all = false;
  limit_bt_reductions = false;
  limit_bt_extensions = false;
  limit_bt_extensions_left_tree = false;
}

◆ set_default_schedule()

void params::set_default_schedule ( )

static

Definition at line 147 of file Parameters.cpp.

                                  {
  default_schedule =  "10  --complete 7                                                                                                           ;\n";
  default_schedule += "15  --conjecture-start --all-definitional                                                                                  ;\n";
  default_schedule += "15  --no-definitional  --restrict-start                                                                                    ;\n";
  default_schedule += "10  --restrict-start   --all-backtrack                                                                                     ;\n";
  default_schedule += "5   --all-definitional                                                                                                     ;\n";
  default_schedule += "4   --conjecture-start --no-definitional                                                                                   ;\n";
  default_schedule += "2   --all-definitional --restrict-start                                                                                    ;\n";
  default_schedule += "2   --restrict-start                                                                                                       ;\n";
  default_schedule += "1   --conjecture-start --all-definitional          --all-backtrack                                                         ;\n";
  default_schedule += "4   --random-reorder   --random-reorder-literals   --conjecture-start --no-definitional   --restrict-start                 ;\n"; 
  default_schedule += "4   --random-reorder   --random-reorder-literals   --all-definitional --restrict-start                                     ;\n";
  default_schedule += "2   --random-reorder   --random-reorder-literals   --all-definitional --restrict-start                                     ;\n";
  default_schedule += "2   --random-reorder   --random-reorder-literals   --all-definitional --restrict-start                                     ;\n";
  default_schedule += "2   --random-reorder   --random-reorder-literals   --no-definitional                                                       ;\n";
  default_schedule += "2   --random-reorder   --random-reorder-literals   --conjecture-start --all-definitional                                   ;\n";
  default_schedule += "2   --random-reorder   --random-reorder-literals   --conjecture-start --all-definitional                                   ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --conjecture-start --all-definitional                                   ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --conjecture-start --all-definitional                                   ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --conjecture-start --no-definitional   --restrict-start                 ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --conjecture-start --no-definitional   --restrict-start                 ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --conjecture-start --no-definitional   --restrict-start                 ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --conjecture-start --no-definitional   --restrict-start --all-backtrack ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --conjecture-start --no-definitional   --restrict-start --all-backtrack ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --all-definitional --restrict-start    --all-backtrack                  ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --all-definitional --restrict-start                                     ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --all-definitional --restrict-start                                     ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --no-definitional                                                       ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --no-definitional                                                       ;\n";
  default_schedule += "1   --random-reorder   --random-reorder-literals   --no-definitional  --restrict-start    --all-backtrack                  ;\n";
  default_schedule += "0   --all-definitional --all-backtrack                                                                                     ;\n";
}

◆ set_default_schedule_parameters()

void params::set_default_schedule_parameters ( )

static

Self-explanatory.

IMPORTANT: these should match the values set in Parameters.cpp, as the assumption is that a schedule modifies them using commands mimicking the command line options.

Definition at line 182 of file Parameters.cpp.

                                             {
  all_definitional = false;
  no_definitional = false;
 
  deterministic_reorder = false;
  number_of_reorders = 0;
  random_reorder = false;
  random_reorder_literals = false;
 
  start_depth = 2;
  depth_increment = 1;
  limit_by_tree_depth = false;
 
  all_start = false;
  all_pos_neg_start = false;
  conjecture_start = false;
  restrict_start = false;
 
  use_regularity_test = true;
  
  use_lemmata = true;
  limit_lemmata = true;
  limit_reductions = true;
  limit_extensions = true;
  limit_bt_all = true;
  limit_bt_lemmas = true;
  limit_bt_reductions = true;
  limit_bt_extensions = true;
  limit_bt_extensions_left_tree = true;
 
  switch_to_complete = UINT32_MAX;
}

◆ show_search_parameter_settings()

void params::show_search_parameter_settings ( )

static

Give a detailed indication of what the parameters affecting the search are currently set to.

Definition at line 268 of file Parameters.cpp.

                                            {
 cout << std::boolalpha 
      << "all_definitional:   " << all_definitional << endl
      << "no_definitional:    " << no_definitional << endl
      << "all_start:          " << all_start << endl
      << "all_pos_neg_start:  " << all_pos_neg_start << endl
      << "conjecture_start:   " << conjecture_start << endl
      << "restrict_start:     " << restrict_start << endl
      << "limit_bt_all:       " << limit_bt_all << endl
      << "switch_to_complete: " << switch_to_complete 
      << std::noboolalpha;
}

Member Data Documentation

◆ add_equality_axioms

bool params::add_equality_axioms = true

static

Definition at line 76 of file Parameters.hpp.

◆ all_definitional

bool params::all_definitional = false

static

Definition at line 71 of file Parameters.hpp.

◆ all_distinct_objects

bool params::all_distinct_objects = false

static

Definition at line 78 of file Parameters.hpp.

◆ all_pos_neg_start

bool params::all_pos_neg_start = false

static

Definition at line 114 of file Parameters.hpp.

◆ all_start

bool params::all_start = false

static

Definition at line 113 of file Parameters.hpp.

◆ boost_random_seed

uint32_t params::boost_random_seed = 0

static

Definition at line 84 of file Parameters.hpp.

◆ build_proof

bool params::build_proof = false

static

Definition at line 146 of file Parameters.hpp.

◆ conjecture_start

bool params::conjecture_start = false

static

Definition at line 115 of file Parameters.hpp.

◆ connectpp_path

std::filesystem::path params::connectpp_path = "."

static

Definition at line 164 of file Parameters.hpp.

◆ default_schedule

std::string params::default_schedule

static

Definition at line 169 of file Parameters.hpp.

◆ definitional_predicate_prefix

std::string params::definitional_predicate_prefix = "def"

static

Definition at line 62 of file Parameters.hpp.

◆ depth_increment

uint32_t params::depth_increment = 1

static

Definition at line 107 of file Parameters.hpp.

◆ depth_limit

uint32_t params::depth_limit = UINT32_MAX

static

Definition at line 106 of file Parameters.hpp.

◆ depth_limit_all

bool params::depth_limit_all = false

static

Definition at line 109 of file Parameters.hpp.

◆ deterministic_reorder

bool params::deterministic_reorder = false

static

Definition at line 85 of file Parameters.hpp.

◆ equality_axioms_at_start

bool params::equality_axioms_at_start = true

static

Definition at line 77 of file Parameters.hpp.

◆ first_parse

bool params::first_parse = true

static

Definition at line 66 of file Parameters.hpp.

◆ full_problem_path

std::filesystem::path params::full_problem_path

static

Definition at line 165 of file Parameters.hpp.

◆ generate_LaTeX_proof

bool params::generate_LaTeX_proof = false

static

Definition at line 147 of file Parameters.hpp.

◆ generate_Prolog_proof

bool params::generate_Prolog_proof = false

static

Definition at line 152 of file Parameters.hpp.

◆ generate_tptp_proof

bool params::generate_tptp_proof = false

static

Definition at line 153 of file Parameters.hpp.

◆ indent_size

uint8_t params::indent_size = 4

static

Definition at line 55 of file Parameters.hpp.

◆ latex_include_matrix

bool params::latex_include_matrix = true

static

Definition at line 151 of file Parameters.hpp.

◆ LaTeX_proof_path

std::filesystem::path params::LaTeX_proof_path = "latex_proof.tex"

static

Definition at line 157 of file Parameters.hpp.

◆ latex_tiny_proof

bool params::latex_tiny_proof = false

static

Definition at line 150 of file Parameters.hpp.

◆ latex_truncation_length

int params::latex_truncation_length = 25

static

Definition at line 149 of file Parameters.hpp.

◆ limit_bt_all

bool params::limit_bt_all = true

static

Definition at line 128 of file Parameters.hpp.

◆ limit_bt_extensions

bool params::limit_bt_extensions = true

static

Definition at line 131 of file Parameters.hpp.

◆ limit_bt_extensions_left_tree

bool params::limit_bt_extensions_left_tree = true

static

Definition at line 132 of file Parameters.hpp.

◆ limit_bt_lemmas

bool params::limit_bt_lemmas = true

static

Definition at line 129 of file Parameters.hpp.

◆ limit_bt_reductions

bool params::limit_bt_reductions = true

static

Definition at line 130 of file Parameters.hpp.

◆ limit_by_tree_depth

bool params::limit_by_tree_depth = false

static

Definition at line 108 of file Parameters.hpp.

◆ limit_extensions

bool params::limit_extensions = true

static

Definition at line 127 of file Parameters.hpp.

◆ limit_lemmata

bool params::limit_lemmata = true

static

Definition at line 125 of file Parameters.hpp.

◆ limit_reductions

bool params::limit_reductions = true

static

Definition at line 126 of file Parameters.hpp.

◆ miniscope

bool params::miniscope = true

static

Definition at line 70 of file Parameters.hpp.

◆ no_definitional

bool params::no_definitional = false

static

Definition at line 72 of file Parameters.hpp.

◆ no_distinct_objects

bool params::no_distinct_objects = false

static

Definition at line 79 of file Parameters.hpp.

◆ number_of_reorders

uint32_t params::number_of_reorders = 0

static

Definition at line 86 of file Parameters.hpp.

◆ output_frequency

uint32_t params::output_frequency = 500000

static

Definition at line 57 of file Parameters.hpp.

◆ output_summary_path

std::filesystem::path params::output_summary_path = "output_summary.txt"

static

Definition at line 160 of file Parameters.hpp.

◆ output_terms_with_substitution

bool params::output_terms_with_substitution = false

static

Definition at line 58 of file Parameters.hpp.

◆ output_width

uint8_t params::output_width = 7

static

Definition at line 56 of file Parameters.hpp.

◆ poly_unification

bool params::poly_unification = false

static

Definition at line 140 of file Parameters.hpp.

◆ positive_representation

bool params::positive_representation = false

static

Definition at line 101 of file Parameters.hpp.

◆ problem_name

std::string params::problem_name = "Unknown"

static

Definition at line 60 of file Parameters.hpp.

◆ Prolog_matrix_path

std::filesystem::path params::Prolog_matrix_path = "matrix.pl"

static

Definition at line 158 of file Parameters.hpp.

◆ Prolog_proof_path

std::filesystem::path params::Prolog_proof_path = "proof.pl"

static

Definition at line 159 of file Parameters.hpp.

◆ pwd_path

std::filesystem::path params::pwd_path = "."

static

Definition at line 163 of file Parameters.hpp.

◆ random_reorder

bool params::random_reorder = false

static

Definition at line 87 of file Parameters.hpp.

◆ random_reorder_literals

bool params::random_reorder_literals = false

static

Definition at line 88 of file Parameters.hpp.

◆ random_seed

unsigned params::random_seed = 0

static

Definition at line 83 of file Parameters.hpp.

◆ restrict_start

bool params::restrict_start = false

static

Definition at line 116 of file Parameters.hpp.

◆ schedule_path

std::filesystem::path params::schedule_path = "."

static

Definition at line 161 of file Parameters.hpp.

◆ show_clauses

bool params::show_clauses = false

static

Definition at line 174 of file Parameters.hpp.

◆ show_full_stats

bool params::show_full_stats = true

static

Definition at line 65 of file Parameters.hpp.

◆ start_depth

uint32_t params::start_depth = 2

static

Definition at line 105 of file Parameters.hpp.

◆ sub_LaTeX_proof

bool params::sub_LaTeX_proof = false

static

Definition at line 148 of file Parameters.hpp.

◆ switch_to_complete

uint32_t params::switch_to_complete = UINT32_MAX

static

Definition at line 136 of file Parameters.hpp.

◆ timeout

bool params::timeout = false

static

Definition at line 92 of file Parameters.hpp.

◆ timeout_value

uint32_t params::timeout_value = UINT32_MAX

static

Definition at line 93 of file Parameters.hpp.

◆ tptp_path

std::filesystem::path params::tptp_path = "."

static

Definition at line 162 of file Parameters.hpp.

◆ unique_skolem_prefix

std::string params::unique_skolem_prefix = "skolem"

static

Definition at line 64 of file Parameters.hpp.

◆ unique_var_prefix

std::string params::unique_var_prefix = "_u"

static

Definition at line 63 of file Parameters.hpp.

◆ use_colours

bool params::use_colours = true

static

Definition at line 54 of file Parameters.hpp.

◆ use_lemmata

bool params::use_lemmata = true

static

Definition at line 124 of file Parameters.hpp.

◆ use_regularity_test

bool params::use_regularity_test = true

static

Definition at line 120 of file Parameters.hpp.

◆ use_schedule

bool params::use_schedule = false

static

Definition at line 97 of file Parameters.hpp.

◆ verbosity

uint8_t params::verbosity = 2

static

Definition at line 53 of file Parameters.hpp.

◆ verify_proof

bool params::verify_proof = false

static

Definition at line 145 of file Parameters.hpp.

◆ verify_proof_verbose

bool params::verify_proof_verbose = false

static

Definition at line 144 of file Parameters.hpp.

◆ write_output_summary

bool params::write_output_summary = false

static

Definition at line 61 of file Parameters.hpp.

The documentation for this struct was generated from the following files:

/Users/sbh11/Desktop/connection-prover/c++/connect++/source/Parameters.hpp
/Users/sbh11/Desktop/connection-prover/c++/connect++/source/Parameters.cpp

Static Public Member Functions

Static Public Attributes

Detailed Description

Member Function Documentation

◆ correct_missing_start_options()

◆ no_start_options()

◆ search_is_complete()

◆ set_all_backtrack()

◆ set_all_start()

◆ set_complete_parameters()

◆ set_default_schedule()

◆ set_default_schedule_parameters()

◆ show_search_parameter_settings()

Member Data Documentation

◆ add_equality_axioms

◆ all_definitional

◆ all_distinct_objects

◆ all_pos_neg_start

◆ all_start

◆ boost_random_seed

◆ build_proof

◆ conjecture_start

◆ connectpp_path

◆ default_schedule

◆ definitional_predicate_prefix

◆ depth_increment

◆ depth_limit

◆ depth_limit_all

◆ deterministic_reorder

◆ equality_axioms_at_start

◆ first_parse

◆ full_problem_path

◆ generate_LaTeX_proof

◆ generate_Prolog_proof

◆ generate_tptp_proof

◆ indent_size

◆ latex_include_matrix

◆ LaTeX_proof_path

◆ latex_tiny_proof

◆ latex_truncation_length

◆ limit_bt_all

◆ limit_bt_extensions

◆ limit_bt_extensions_left_tree

◆ limit_bt_lemmas

◆ limit_bt_reductions

◆ limit_by_tree_depth

◆ limit_extensions

◆ limit_lemmata

◆ limit_reductions

◆ miniscope

◆ no_definitional

◆ no_distinct_objects

◆ number_of_reorders

◆ output_frequency

◆ output_summary_path

◆ output_terms_with_substitution

◆ output_width

◆ poly_unification

◆ positive_representation

◆ problem_name

◆ Prolog_matrix_path

◆ Prolog_proof_path

◆ pwd_path

◆ random_reorder

◆ random_reorder_literals

◆ random_seed

◆ restrict_start

◆ schedule_path

◆ show_clauses

◆ show_full_stats

◆ start_depth

◆ sub_LaTeX_proof

◆ switch_to_complete

◆ timeout

◆ timeout_value

◆ tptp_path

◆ unique_skolem_prefix

◆ unique_var_prefix

◆ use_colours

◆ use_lemmata