1def_module_params('fp', 2 description='fixedpoint parameters', 3 export=True, 4 params=(('engine', SYMBOL, 'auto-config', 5 'Select: auto-config, datalog, bmc, spacer'), 6 ('datalog.default_table', SYMBOL, 'sparse', 7 'default table implementation: sparse, hashtable, bitvector, interval'), 8 ('datalog.default_relation', SYMBOL, 'pentagon', 9 'default relation implementation: external_relation, pentagon'), 10 ('datalog.generate_explanations', BOOL, False, 11 'produce explanations for produced facts when using the datalog engine'), 12 ('datalog.use_map_names', BOOL, True, 13 "use names from map files when displaying tuples"), 14 ('datalog.magic_sets_for_queries', BOOL, False, 15 "magic set transformation will be used for queries"), 16 ('datalog.explanations_on_relation_level', BOOL, False, 17 'if true, explanations are generated as history of each relation, ' + 18 'rather than per fact (generate_explanations must be set to true for ' + 19 'this option to have any effect)'), 20 ('datalog.unbound_compressor', BOOL, True, 21 "auxiliary relations will be introduced to avoid unbound variables " + 22 "in rule heads"), 23 ('datalog.similarity_compressor', BOOL, True, 24 "rules that differ only in values of constants will be merged into " + 25 "a single rule"), 26 ('datalog.similarity_compressor_threshold', UINT, 11, 27 "if similarity_compressor is on, this value determines how many " + 28 "similar rules there must be in order for them to be merged"), 29 ('datalog.all_or_nothing_deltas', BOOL, False, 30 "compile rules so that it is enough for the delta relation in " + 31 "union and widening operations to determine only whether the " + 32 "updated relation was modified or not"), 33 ('datalog.compile_with_widening', BOOL, False, 34 "widening will be used to compile recursive rules"), 35 ('datalog.default_table_checked', BOOL, False, "if true, the default " + 36 'table will be default_table inside a wrapper that checks that its results ' + 37 'are the same as of default_table_checker table'), 38 ('datalog.default_table_checker', SYMBOL, 'null', "see default_table_checked"), 39 ('datalog.check_relation',SYMBOL,'null', "name of default relation to check. " + 40 "operations on the default relation will be verified using SMT solving"), 41 ('datalog.initial_restart_timeout', UINT, 0, 42 "length of saturation run before the first restart (in ms), " + 43 "zero means no restarts"), 44 ('datalog.timeout', UINT, 0, "Time limit used for saturation"), 45 ('datalog.output_profile', BOOL, False, 46 "determines whether profile information should be " + 47 "output when outputting Datalog rules or instructions"), 48 ('datalog.print.tuples', BOOL, True, 49 "determines whether tuples for output predicates should be output"), 50 ('datalog.profile_timeout_milliseconds', UINT, 0, 51 "instructions and rules that took less than the threshold " + 52 "will not be printed when printed the instruction/rule list"), 53 ('datalog.dbg_fpr_nonempty_relation_signature', BOOL, False, 54 "if true, finite_product_relation will attempt to avoid creating " + 55 "inner relation with empty signature by putting in half of the " + 56 "table columns, if it would have been empty otherwise"), 57 ('datalog.subsumption', BOOL, True, 58 "if true, removes/filters predicates with total transitions"), 59 ('generate_proof_trace', BOOL, False, "trace for 'sat' answer as proof object"), 60 ('spacer.push_pob', BOOL, False, "push blocked pobs to higher level"), 61 ('spacer.push_pob_max_depth', UINT, UINT_MAX, 62 'Maximum depth at which push_pob is enabled'), 63 ('validate', BOOL, False, 64 "validate result (by proof checking or model checking)"), 65 ('spacer.simplify_lemmas_pre', BOOL, False, 66 "simplify derived lemmas before inductive propagation"), 67 ('spacer.simplify_lemmas_post', BOOL, False, 68 "simplify derived lemmas after inductive propagation"), 69 ('spacer.use_inductive_generalizer', BOOL, True, 70 "generalize lemmas using induction strengthening"), 71 ('spacer.max_num_contexts', UINT, 500, "maximal number of contexts to create"), 72 ('print_fixedpoint_extensions', BOOL, True, 73 "use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, " + 74 "when printing rules"), 75 ('print_low_level_smt2', BOOL, False, 76 "use (faster) low-level SMT2 printer (the printer is scalable " + 77 "but the result may not be as readable)"), 78 ('print_with_variable_declarations', BOOL, True, 79 "use variable declarations when displaying rules " + 80 "(instead of attempting to use original names)"), 81 ('print_answer', BOOL, False, 'print answer instance(s) to query'), 82 ('print_certificate', BOOL, False, 83 'print certificate for reachability or non-reachability'), 84 ('print_boogie_certificate', BOOL, False, 85 'print certificate for reachability or non-reachability using a ' + 86 'format understood by Boogie'), 87 ('print_aig', SYMBOL, '', 88 'Dump clauses in AIG text format (AAG) to the given file name'), 89 ('print_statistics', BOOL, False, 'print statistics'), 90 ('tab.selection', SYMBOL, 'weight', 91 'selection method for tabular strategy: weight (default), first, var-use'), 92 ('xform.bit_blast', BOOL, False, 93 'bit-blast bit-vectors'), 94 ('xform.magic', BOOL, False, 95 "perform symbolic magic set transformation"), 96 ('xform.scale', BOOL, False, 97 "add scaling variable to linear real arithmetic clauses"), 98 ('xform.inline_linear', BOOL, True, "try linear inlining method"), 99 ('xform.inline_eager', BOOL, True, "try eager inlining of rules"), 100 ('xform.inline_linear_branch', BOOL, False, 101 "try linear inlining method with potential expansion"), 102 ('xform.compress_unbound', BOOL, True, "compress tails with unbound variables"), 103 ('xform.fix_unbound_vars', BOOL, False, "fix unbound variables in tail"), 104 ('xform.unfold_rules', UINT, 0, 105 "unfold rules statically using iterative squaring"), 106 ('xform.slice', BOOL, True, "simplify clause set using slicing"), 107 ('spacer.use_euf_gen', BOOL, False, 'Generalize lemmas and pobs using implied equalities'), 108 ('xform.transform_arrays', BOOL, False, 109 "Rewrites arrays equalities and applies select over store"), 110 ('xform.instantiate_arrays', BOOL, False, 111 "Transforms P(a) into P(i, a[i] a)"), 112 ('xform.instantiate_arrays.enforce', BOOL, False, 113 "Transforms P(a) into P(i, a[i]), discards a from predicate"), 114 ('xform.instantiate_arrays.nb_quantifier', UINT, 1, 115 "Gives the number of quantifiers per array"), 116 ('xform.instantiate_arrays.slice_technique', SYMBOL, "no-slicing", 117 "<no-slicing>=> GetId(i) = i, <smash> => GetId(i) = true"), 118 ('xform.quantify_arrays', BOOL, False, 119 "create quantified Horn clauses from clauses with arrays"), 120 ('xform.instantiate_quantifiers', BOOL, False, 121 "instantiate quantified Horn clauses using E-matching heuristic"), 122 ('xform.coalesce_rules', BOOL, False, "coalesce rules"), 123 ('xform.tail_simplifier_pve', BOOL, True, "propagate_variable_equivalences"), 124 ('xform.subsumption_checker', BOOL, True, "Enable subsumption checker (no support for model conversion)"), 125 ('xform.coi', BOOL, True, "use cone of influence simplification"), 126 ('spacer.order_children', UINT, 0, 'SPACER: order of enqueuing children in non-linear rules : 0 (original), 1 (reverse), 2 (random)'), 127 ('spacer.use_lemma_as_cti', BOOL, False, 'SPACER: use a lemma instead of a CTI in flexible_trace'), 128 ('spacer.reset_pob_queue', BOOL, True, 'SPACER: reset pob obligation queue when entering a new level'), 129 ('spacer.use_array_eq_generalizer', BOOL, True, 'SPACER: attempt to generalize lemmas with array equalities'), 130 ('spacer.use_derivations', BOOL, True, 'SPACER: using derivation mechanism to cache intermediate results for non-linear rules'), 131 ('xform.array_blast', BOOL, False, "try to eliminate local array terms using Ackermannization -- some array terms may remain"), 132 ('xform.array_blast_full', BOOL, False, "eliminate all local array variables by QE"), 133 ('xform.elim_term_ite', BOOL, False, 'Eliminate term-ite expressions'), 134 ('xform.elim_term_ite.inflation', UINT, 3, 'Maximum inflation for non-Boolean ite-terms blasting: 0 (none), k (multiplicative)'), 135 ('spacer.propagate', BOOL, True, 'Enable propagate/pushing phase'), 136 ('spacer.max_level', UINT, UINT_MAX, "Maximum level to explore"), 137 ('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"), 138 ('spacer.blast_term_ite_inflation', UINT, 3, 'Maximum inflation for non-Boolean ite-terms expansion: 0 (none), k (multiplicative)'), 139 ('spacer.reach_dnf', BOOL, True, "Restrict reachability facts to DNF"), 140 ('bmc.linear_unrolling_depth', UINT, UINT_MAX, "Maximal level to explore"), 141 ('spacer.iuc.split_farkas_literals', BOOL, False, "Split Farkas literals"), 142 ('spacer.native_mbp', BOOL, True, "Use native mbp of Z3"), 143 ('spacer.eq_prop', BOOL, True, "Enable equality and bound propagation in arithmetic"), 144 ('spacer.weak_abs', BOOL, True, "Weak abstraction"), 145 ('spacer.restarts', BOOL, False, "Enable resetting obligation queue"), 146 ('spacer.restart_initial_threshold', UINT, 10, "Initial threshold for restarts"), 147 ('spacer.random_seed', UINT, 0, "Random seed to be used by SMT solver"), 148 149 ('spacer.mbqi', BOOL, True, 'Enable mbqi'), 150 ('spacer.keep_proxy', BOOL, True, 'keep proxy variables (internal parameter)'), 151 ('spacer.q3', BOOL, True, 'Allow quantified lemmas in frames'), 152 ('spacer.q3.instantiate', BOOL, True, 'Instantiate quantified lemmas'), 153 ('spacer.q3.use_qgen', BOOL, False, 'use quantified lemma generalizer'), 154 ('spacer.q3.qgen.normalize', BOOL, True, 'normalize cube before quantified generalization'), 155 ('spacer.iuc', UINT, 1, 156 '0 = use old implementation of unsat-core-generation, ' + 157 '1 = use new implementation of IUC generation, ' + 158 '2 = use new implementation of IUC + min-cut optimization'), 159 ('spacer.iuc.arith', UINT, 1, 160 '0 = use simple Farkas plugin, ' + 161 '1 = use simple Farkas plugin with constant from other partition (like old unsat-core-generation),' + 162 '2 = use Gaussian elimination optimization (broken), 3 = use additive IUC plugin'), 163 ('spacer.iuc.old_hyp_reducer', BOOL, False, 'use old hyp reducer instead of new implementation, for debugging only'), 164 ('spacer.validate_lemmas', BOOL, False, 'Validate each lemma after generalization'), 165 ('spacer.ground_pobs', BOOL, True, 'Ground pobs by using values from a model'), 166 ('spacer.iuc.print_farkas_stats', BOOL, False, 'prints for each proof how many Farkas lemmas it contains and how many of these participate in the cut (for debugging)'), 167 ('spacer.iuc.debug_proof', BOOL, False, 'prints proof used by unsat-core-learner for debugging purposes (debugging)'), 168 ('spacer.simplify_pob', BOOL, False, 'simplify pobs by removing redundant constraints'), 169 ('spacer.p3.share_lemmas', BOOL, False, 'Share frame lemmas'), 170 ('spacer.p3.share_invariants', BOOL, False, "Share invariants lemmas"), 171 ('spacer.min_level', UINT, 0, 'Minimal level to explore'), 172 ('spacer.print_json', SYMBOL, '', 'Print pobs tree in JSON format to a given file'), 173 ('spacer.trace_file', SYMBOL, '', 'Log file for progress events'), 174 ('spacer.ctp', BOOL, True, 'Enable counterexample-to-pushing'), 175 ('spacer.use_inc_clause', BOOL, True, 'Use incremental clause to represent trans'), 176 ('spacer.dump_benchmarks', BOOL, False, 'Dump SMT queries as benchmarks'), 177 ('spacer.dump_threshold', DOUBLE, 5.0, 'Threshold in seconds on dumping benchmarks'), 178 ('spacer.gpdr', BOOL, False, 'Use GPDR solving strategy for non-linear CHC'), 179 ('spacer.gpdr.bfs', BOOL, True, 'Use BFS exploration strategy for expanding model search'), 180 ('spacer.use_bg_invs', BOOL, False, 'Enable external background invariants'), 181 ('spacer.use_lim_num_gen', BOOL, False, 'Enable limit numbers generalizer to get smaller numbers'), 182 ('spacer.logic', SYMBOL, '', 'SMT-LIB logic to configure internal SMT solvers'), 183 ('spacer.arith.solver', UINT, 2, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), 184 )) 185