Nikolaj Bjorner 0e6b3a922a Add commands for forcing preferences during search ... Add commands: (prefer <formula>) - will instruct case split queue to assign formula to true. - prefer commands added within a scope are forgotten after leaving the scope. (reset-preferences) - resets asserted preferences. Has to be invoked at base level. This provides functionality related to MathSAT and based on an ask by Tomáš Kolárik who is integrating the functionality with OpenSMT2		2025-10-02 10:47:10 -07:00
..
proto_model	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
tactic	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00
arith_eq_adapter.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
arith_eq_adapter.h	booyah	2020-07-04 15:56:30 -07:00
arith_eq_solver.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
arith_eq_solver.h	booyah	2020-07-04 15:56:30 -07:00
CMakeLists.txt	remove theory_str and classes that are only used by it	2025-08-07 21:05:12 -07:00
database.h	Make sure all headers do #pragma once. (#6188)	2022-07-23 10:41:14 -07:00
database.smt	Tabs, whitespace	2017-09-17 18:10:06 +01:00
diff_logic.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
dyn_ack.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
dyn_ack.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
expr_context_simplifier.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
expr_context_simplifier.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
fingerprints.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
fingerprints.h	remove a few default constructors	2024-09-23 08:17:58 +01:00
mam.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
mam.h	Use = default for virtual constructors.	2022-08-05 18:11:46 +03:00
old_interval.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
old_interval.h	Use noexcept more. (#7058)	2023-12-16 12:14:53 +00:00
qi_queue.cpp	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00
qi_queue.h	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00
seq_axioms.cpp	add options for logging learned lemmas and theory axioms	2022-08-08 11:18:56 +03:00
seq_axioms.h	na	2022-01-01 17:59:31 -08:00
seq_eq_solver.cpp	debug under defined calls	2025-08-07 08:33:04 -07:00
seq_ne_solver.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
seq_offset_eq.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
seq_offset_eq.h	fix misspelled \brief for doxygen (#5632)	2021-10-29 15:34:28 +02:00
seq_regex.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
seq_regex.h	fix co-factoring'	2021-12-14 10:12:38 -08:00
smt2_extra_cmds.cpp	merge with Z3Prover/master	2018-06-25 19:44:46 +08:00
smt2_extra_cmds.h	booyah	2020-07-04 15:56:30 -07:00
smt_almost_cg_table.cpp	streamline pb solver interface and naming after removal of xor	2021-02-28 12:32:04 -08:00
smt_almost_cg_table.h	booyah	2020-07-04 15:56:30 -07:00
smt_arith_value.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_arith_value.h	enable ranges for bit-vectors	2020-08-13 10:53:37 -07:00
smt_b_justification.h	remove unneeded constructors (last round)	2020-07-12 17:41:57 +01:00
smt_bool_var_data.h	booyah	2020-07-04 15:56:30 -07:00
smt_case_split_queue.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_case_split_queue.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
smt_cg_table.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_cg_table.h	booyah	2020-07-04 15:56:30 -07:00
smt_checker.cpp	call it data instead of c_ptr for approaching C++11 std::vector convention.	2021-04-13 18:17:35 -07:00
smt_checker.h	booyah	2020-07-04 15:56:30 -07:00
smt_clause.cpp	consolidate literals	2021-05-20 12:58:27 -07:00
smt_clause.h	Use = default for virtual constructors.	2022-08-05 18:11:46 +03:00
smt_clause_proof.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_clause_proof.h	merging master to unit_prop_on_monomials	2023-10-02 16:42:59 -07:00
smt_conflict_resolution.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_conflict_resolution.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
smt_consequences.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_context.cpp	propagate value initialization to atoms	2025-09-24 11:01:24 +03:00
smt_context.h	propagate value initialization to atoms	2025-09-24 11:01:24 +03:00
smt_context_inv.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_context_pp.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_context_stat.cpp	remove '#include <iostream>' from headers and from unneeded places	2022-06-17 14:10:19 +01:00
smt_enode.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_enode.h	remove unneeded iterator functions	2024-09-23 12:59:04 +01:00
smt_eq_justification.h	booyah	2020-07-04 15:56:30 -07:00
smt_failure.h	fix crash reported by Nikhil on F* due to unhandled exception while using the rewriter during search	2025-01-28 16:27:28 -08:00
smt_farkas_util.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_farkas_util.h	booyah	2020-07-04 15:56:30 -07:00
smt_for_each_relevant_expr.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_for_each_relevant_expr.h	Use = default for virtual constructors.	2022-08-05 18:11:46 +03:00
smt_implied_equalities.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_implied_equalities.h	booyah	2020-07-04 15:56:30 -07:00
smt_induction.cpp.disabled	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_induction.h.disabled	remove dependencies on stale component	2021-08-16 17:52:36 -07:00
smt_internalizer.cpp	Par (#7945)	2025-09-21 10:11:04 +03:00
smt_justification.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_justification.h	add options for logging learned lemmas and theory axioms	2022-08-08 11:18:56 +03:00
smt_kernel.cpp	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00
smt_kernel.h	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00
smt_literal.cpp	consolidate literals	2021-05-20 12:58:27 -07:00
smt_literal.h	consolidate literals	2021-05-20 12:58:27 -07:00
smt_lookahead.cpp	disable pre-processing during cubing	2025-07-31 20:58:58 -07:00
smt_lookahead.h	Revert "Parallel solving (#7775)" (#7777)	2025-08-14 18:16:35 -07:00
smt_model_checker.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_model_checker.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
smt_model_finder.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_model_finder.h	fix compiler warnings #4727	2020-10-18 11:31:21 +01:00
smt_model_generator.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_model_generator.h	fix #7584	2025-03-15 13:33:08 -07:00
smt_parallel.cpp	remove stale comment	2025-09-22 04:43:41 +03:00
smt_parallel.h	household cleanup	2025-09-22 03:58:04 +03:00
smt_quantifier.cpp	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00
smt_quantifier.h	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00
smt_quantifier_instances.h	booyah	2020-07-04 15:56:30 -07:00
smt_quick_checker.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_quick_checker.h	booyah	2020-07-04 15:56:30 -07:00
smt_relevancy.cpp	allow for internalize implies	2025-07-31 20:48:15 -07:00
smt_relevancy.h	allow for internalize implies	2025-07-31 20:48:15 -07:00
smt_setup.cpp	remove theory_str and classes that are only used by it	2025-08-07 21:05:12 -07:00
smt_setup.h	remove theory_str and classes that are only used by it	2025-08-07 21:05:12 -07:00
smt_solver.cpp	display assumptions used	2025-09-11 10:20:55 -07:00
smt_solver.h	booyah	2020-07-04 15:56:30 -07:00
smt_statistics.cpp	make include paths uniformly use path relative to src. #534	2017-07-31 13:24:11 -07:00
smt_statistics.h	remove '#include <iostream>' from headers and from unneeded places	2022-06-17 14:10:19 +01:00
smt_theory.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
smt_theory.h	remove ref to theory_str	2025-08-07 21:21:35 -07:00
smt_types.h	signed	2021-05-21 15:51:27 -07:00
smt_value_sort.cpp	refactor get_sort	2021-02-02 04:45:54 -08:00
smt_value_sort.h	booyah	2020-07-04 15:56:30 -07:00
spanning_tree.h	booyah	2020-07-04 15:56:30 -07:00
spanning_tree_base.h	booyah	2020-07-04 15:56:30 -07:00
spanning_tree_def.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_arith.cpp	make include paths uniformly use path relative to src. #534	2017-07-31 13:24:11 -07:00
theory_arith.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
theory_arith_aux.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_arith_core.h	add option to control epsilon #7791	2025-08-17 16:51:00 -07:00
theory_arith_def.h	booyah	2020-07-04 15:56:30 -07:00
theory_arith_eq.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_arith_int.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_arith_inv.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_arith_nl.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_arith_pp.h	fix #7053	2023-12-13 19:25:18 -08:00
theory_array.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_array.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
theory_array_bapa.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_array_bapa.h	booyah	2020-07-04 15:56:30 -07:00
theory_array_base.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_array_base.h	add option to select with folding	2022-08-04 16:59:26 +03:00
theory_array_full.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_array_full.h	remove some uneeded constructors	2024-12-22 15:06:58 +00:00
theory_bv.cpp	Add commands for forcing preferences during search	2025-10-02 10:47:10 -07:00
theory_bv.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
theory_char.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_char.h	bv2char and char2bv with Clemens	2021-09-13 16:09:03 +02:00
theory_datatype.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_datatype.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
theory_dense_diff_logic.cpp	make include paths uniformly use path relative to src. #534	2017-07-31 13:24:11 -07:00
theory_dense_diff_logic.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
theory_dense_diff_logic_def.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_diff_logic.cpp	make include paths uniformly use path relative to src. #534	2017-07-31 13:24:11 -07:00
theory_diff_logic.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
theory_diff_logic_def.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_dl.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_dl.h	booyah	2020-07-04 15:56:30 -07:00
theory_dummy.cpp	remove template Context dependency in every trail object	2021-02-08 15:41:57 -08:00
theory_dummy.h	Remove empty leaf destructors. (#6211)	2022-07-30 10:07:03 +01:00
theory_fpa.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_fpa.h	Revert unsound NaN constraints in theory_fpa (#6993)	2023-11-14 14:28:30 -08:00
theory_intblast.cpp	fix #7572 and fix #7574	2025-03-07 10:46:29 -08:00
theory_intblast.h	Sls (#7439)	2024-11-02 12:32:48 -07:00
theory_lra.cpp	fix unsound axiom for lower-bounding	2025-09-21 19:24:13 +03:00
theory_lra.h	Add (updated and general) solve_for functionality for arithmetic, add congruence_explain to API to retrieve explanation for why two terms are congruent Tweak handling of smt.qi.max_instantations	2024-12-19 23:27:57 +01:00
theory_opt.cpp	make include paths uniformly use path relative to src. #534	2017-07-31 13:24:11 -07:00
theory_opt.h	Add and fix a few general compiler warnings. (#5628)	2021-10-29 15:42:32 +02:00
theory_pb.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_pb.h	move smt params to params directory, update release.yml	2025-06-09 10:47:22 -07:00
theory_polymorphism.h	wip - alpha support for polymorphism	2023-07-12 18:09:02 -07:00
theory_recfun.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_recfun.h	rename function	2025-04-04 18:40:15 -07:00
theory_seq.cpp	avoid interferring side-effects in function calls	2025-08-07 14:40:07 -07:00
theory_seq.h	add sequential option for SLS, fixes to import/export methods SLS<->SMT	2024-11-14 21:43:40 -08:00
theory_seq_empty.h	remove template Context dependency in every trail object	2021-02-08 15:41:57 -08:00
theory_sls.cpp	deal with compiler warnings and include value exchange prior to final check.	2025-01-24 09:40:33 -08:00
theory_sls.h	deal with compiler warnings and include value exchange prior to final check.	2025-01-24 09:40:33 -08:00
theory_special_relations.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_special_relations.h	handle ac-op in legacy special relations procedure by adding warning	2023-12-03 12:55:37 -08:00
theory_user_propagator.cpp	Add commands for forcing preferences during search	2025-10-02 10:47:10 -07:00
theory_user_propagator.h	add an option to register callback on quantifier instantiation	2025-08-06 21:11:55 -07:00
theory_utvpi.cpp	Fix some typos. (#7115)	2024-02-07 23:06:43 -08:00
theory_utvpi.h	remove a hundred implicit constructors/destructors	2021-05-23 14:25:01 +01:00
theory_utvpi_def.h	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_wmaxsat.cpp	Centralize and document TRACE tags using X-macros (#7657)	2025-05-28 14:31:25 +01:00
theory_wmaxsat.h	move model and proof converters to self-contained module	2022-11-03 05:23:01 -07:00
uses_theory.cpp	remove unused file & hide a few symbols	2020-01-31 17:13:28 +00:00
uses_theory.h	booyah	2020-07-04 15:56:30 -07:00
watch_list.cpp	fix #4856	2020-12-06 14:06:08 -08:00
watch_list.h	enable ranges for bit-vectors	2020-08-13 10:53:37 -07:00