def_module_params('fixedpoint', description='fixedpoint parameters', export=True, params=(('timeout', UINT, UINT_MAX, 'set timeout'), ('engine', SYMBOL, 'auto-config', 'Select: auto-config, datalog, duality, pdr, bmc'), ('datalog.default_table', SYMBOL, 'sparse', 'default table implementation: sparse, hashtable, bitvector, interval'), ('datalog.default_relation', SYMBOL, 'pentagon', 'default relation implementation: external_relation, pentagon'), ('datalog.generate_explanations', BOOL, False, 'produce explanations for produced facts when using the datalog engine'), ('datalog.use_map_names', BOOL, True, "use names from map files when displaying tuples"), ('datalog.magic_sets_for_queries', BOOL, False, "magic set transformation will be used for queries"), ('datalog.explanations_on_relation_level', BOOL, False, 'if true, explanations are generated as history of each relation, ' + 'rather than per fact (generate_explanations must be set to true for ' + 'this option to have any effect)'), ('datalog.unbound_compressor', BOOL, True, "auxiliary relations will be introduced to avoid unbound variables " + "in rule heads"), ('datalog.similarity_compressor', BOOL, True, "rules that differ only in values of constants will be merged into " + "a single rule"), ('datalog.similarity_compressor_threshold', UINT, 11, "if similarity_compressor is on, this value determines how many " + "similar rules there must be in order for them to be merged"), ('datalog.all_or_nothing_deltas', BOOL, False, "compile rules so that it is enough for the delta relation in " + "union and widening operations to determine only whether the " + "updated relation was modified or not"), ('datalog.compile_with_widening', BOOL, False, "widening will be used to compile recursive rules"), ('datalog.default_table_checked', BOOL, False, "if true, the detault " + 'table will be default_table inside a wrapper that checks that its results ' + 'are the same as of default_table_checker table'), ('datalog.default_table_checker', SYMBOL, 'null', "see default_table_checked"), ('datalog.check_relation',SYMBOL,'null', "name of default relation to check. " + "operations on the default relation will be verified using SMT solving"), ('datalog.initial_restart_timeout', UINT, 0, "length of saturation run before the first restart (in ms), " + "zero means no restarts"), ('datalog.output_profile', BOOL, False, "determines whether profile information should be " + "output when outputting Datalog rules or instructions"), ('datalog.print.tuples', BOOL, True, "determines whether tuples for output predicates should be output"), ('datalog.profile_timeout_milliseconds', UINT, 0, "instructions and rules that took less than the threshold " + "will not be printed when printed the instruction/rule list"), ('datalog.dbg_fpr_nonempty_relation_signature', BOOL, False, "if true, finite_product_relation will attempt to avoid creating " + "inner relation with empty signature by putting in half of the " + "table columns, if it would have been empty otherwise"), ('duality.full_expand', BOOL, False, 'Fully expand derivation trees'), ('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'), ('duality.feasible_edges', BOOL, True, 'Don\'t expand definitley infeasible edges'), ('duality.use_underapprox', BOOL, False, 'Use underapproximations'), ('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'), ('duality.recursion_bound', UINT, UINT_MAX, 'Recursion bound for stratified inlining'), ('duality.profile', BOOL, False, 'profile run time'), ('duality.mbqi', BOOL, True, 'use model-based quantifier instantiation'), ('duality.batch_expand', BOOL, False, 'use batch expansion'), ('duality.conjecture_file', STRING, '', 'save conjectures to file'), ('pdr.bfs_model_search', BOOL, True, "use BFS strategy for expanding model search"), ('pdr.farkas', BOOL, True, "use lemma generator based on Farkas (for linear real arithmetic)"), ('generate_proof_trace', BOOL, False, "trace for 'sat' answer as proof object"), ('pdr.flexible_trace', BOOL, False, "allow PDR generate long counter-examples " + "by extending candidate trace within search area"), ('pdr.use_model_generalizer', BOOL, False, "use model for backwards propagation (instead of symbolic simulation)"), ('pdr.validate_result', BOOL, False, "validate result (by proof checking or model checking)"), ('pdr.simplify_formulas_pre', BOOL, False, "simplify derived formulas before inductive propagation"), ('pdr.simplify_formulas_post', BOOL, False, "simplify derived formulas after inductive propagation"), ('pdr.use_multicore_generalizer', BOOL, False, "extract multiple cores for blocking states"), ('pdr.use_inductive_generalizer', BOOL, True, "generalize lemmas using induction strengthening"), ('pdr.use_arith_inductive_generalizer', BOOL, False, "generalize lemmas using arithmetic heuristics for induction strengthening"), ('pdr.use_convex_closure_generalizer', BOOL, False, "generalize using convex closures of lemmas"), ('pdr.use_convex_interior_generalizer', BOOL, False, "generalize using convex interiors of lemmas"), ('pdr.cache_mode', UINT, 0, "use no (0), symbolic (1) or explicit " + "cache (2) for model search"), ('pdr.inductive_reachability_check', BOOL, False, "assume negation of the cube on the previous level when " + "checking for reachability (not only during cube weakening)"), ('pdr.max_num_contexts', UINT, 500, "maximal number of contexts to create"), ('pdr.try_minimize_core', BOOL, False, "try to reduce core size (before inductive minimization)"), ('pdr.utvpi', BOOL, True, 'Enable UTVPI strategy'), ('print_fixedpoint_extensions', BOOL, True, "use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, " + "when printing rules"), ('print_low_level_smt2', BOOL, False, "use (faster) low-level SMT2 printer (the printer is scalable " + "but the result may not be as readable)"), ('print_with_variable_declarations', BOOL, True, "use variable declarations when displaying rules " + "(instead of attempting to use original names)"), ('print_answer', BOOL, False, 'print answer instance(s) to query'), ('print_certificate', BOOL, False, 'print certificate for reachability or non-reachability'), ('print_boogie_certificate', BOOL, False, 'print certificate for reachability or non-reachability using a ' + 'format understood by Boogie'), ('print_statistics', BOOL, False, 'print statistics'), ('print_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'), ('tab.selection', SYMBOL, 'weight', 'selection method for tabular strategy: weight (default), first, var-use'), ('xform.bit_blast', BOOL, False, 'bit-blast bit-vectors'), ('xform.magic', BOOL, False, "perform symbolic magic set transformation"), ('xform.scale', BOOL, False, "add scaling variable to linear real arithemtic clauses"), ('xform.inline_linear', BOOL, True, "try linear inlining method"), ('xform.inline_eager', BOOL, True, "try eager inlining of rules"), ('xform.inline_linear_branch', BOOL, False, "try linear inlining method with potential expansion"), ('xform.compress_unbound', BOOL, True, "compress tails with unbound variables"), ('xform.fix_unbound_vars', BOOL, False, "fix unbound variables in tail"), ('xform.unfold_rules', UINT, 0, "unfold rules statically using iterative squarring"), ('xform.slice', BOOL, True, "simplify clause set using slicing"), ('xform.karr', BOOL, False, "Add linear invariants to clauses using Karr's method"), ('xform.quantify_arrays', BOOL, False, "create quantified Horn clauses from clauses with arrays"), ('xform.instantiate_quantifiers', BOOL, False, "instantiate quantified Horn clauses using E-matching heuristic"), ('xform.coalesce_rules', BOOL, False, "coalesce rules"), ('xform.coi', BOOL, True, "use cone of influence simplificaiton"), ('duality.enable_restarts', BOOL, False, 'DUALITY: enable restarts'), ))