C++ (Cpp) ini_params Example


The c++ (cpp) ini_params example is extracted from the most popular open source projects, you can refer to the following example for usage.

Programming language: C++ (Cpp)

Class/type: ini_params

File: order_params.cppProject: CharudattaSChitale/sygus-comp14

void order_params::register_params(ini_params & p) {
    p.register_symbol_list_param("PRECEDENCE", m_order_precedence, "describe a (partial) precedence for the term ordering used in the Superposition Calculus module. The precedence is lists of function symbols. Example: PRECEDENCE=\"(f, g, h)\"");
    p.register_symbol_list_param("PRECEDENCE_GEN", m_order_precedence_gen, "describe how a total precedence order is generated. The generator is a sequence of simple (partial) orders with an optional '-' (indicating the next (partial) order should be inverted). The available simple (partial) orders are: user (the order specified by precedence); arity; interpreted (interpreted function symbols are considered smaller); definition (defined function symbols are considered bigger); frequency; arbitrary (total arbitrary order generated by Z3). Example: PRECEDENCE_GEN=\"user interpreted - arity arbitraty\"");
    p.register_symbol_nat_list_param("ORDER_WEIGHTS", m_order_weights, "describe a (partial) assignment of weights to function symbols for term orderings (e.g., KBO). The assigment is a list of pairs of the form f:n where f is a string and n is a natural. Example: WEIGHTS=\"(f:1, g:2, h:3)\"");
    p.register_unsigned_param("ORDER_VAR_WEIGHT", m_order_var_weight, "weight of variables in term orderings (e.g., KBO)");
    p.register_int_param("ORDER", 0, 1, reinterpret_cast<int&>(m_order_kind), "Term ordering: 0 - KBO, 1 - LPO");

File: smt_params.cppProject: Moondee/Artemis

void smt_params::register_params(ini_params & p) {

    p.register_bool_param("CHECK_PROOF", m_check_proof);
    p.register_bool_param("DISPLAY_PROOF", m_display_proof);
    p.register_bool_param("DISPLAY_DOT_PROOF", m_display_dot_proof);
    p.register_bool_param("DISPLAY_UNSAT_CORE", m_display_unsat_core);
    p.register_bool_param("INTERNALIZER_NNF", m_internalizer_nnf);
    p.register_bool_param("EQ_PROPAGATION", m_eq_propagation);
    p.register_bool_param("BIN_CLAUSES", m_binary_clause_opt);
    p.register_unsigned_param("RELEVANCY", m_relevancy_lvl, "relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant", true);
    p.register_bool_param("RELEVANCY_LEMMA", m_relevancy_lemma, "true if lemmas are used to propagate relevancy");
    p.register_unsigned_param("RANDOM_SEED", m_random_seed, "random seed for Z3");
    p.register_percentage_param("RANDOM_CASE_SPLIT_FREQ", m_random_var_freq, "frequency of random case splits");
    p.register_int_param("PHASE_SELECTION", 0, 6, reinterpret_cast<int&>(m_phase_selection), "phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences");
    p.register_bool_param("MINIMIZE_LEMMAS", m_minimize_lemmas, "enable/disable lemma minimization algorithm");
    p.register_unsigned_param("MAX_CONFLICTS", m_max_conflicts, "maximum number of conflicts");

    p.register_unsigned_param("RECENT_LEMMA_THRESHOLD", m_recent_lemmas_size);
    p.register_unsigned_param("TICK", m_tick);

            p.register_bool_param("THEORY_RESOLVE", m_theory_resolve, "Apply theory resolution to produce auxiliary conflict clauses", true);