| .. |
|
params
|
User control over more arith options
|
2018-06-14 16:08:49 -07:00 |
|
proto_model
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
tactic
|
fix build
|
2018-05-01 10:53:36 -07:00 |
|
arith_eq_adapter.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
arith_eq_adapter.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
arith_eq_solver.cpp
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
arith_eq_solver.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
asserted_formulas.cpp
|
remove iff
|
2018-06-14 16:08:48 -07:00 |
|
asserted_formulas.h
|
delay updating parameters to ensure rewriting in asserted_formulas is applied using configuration overrides. Fixes build regression for tree_interpolation documentation test
|
2018-03-04 21:57:08 -08:00 |
|
cached_var_subst.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
cached_var_subst.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
CMakeLists.txt
|
added facility to persist model transformations
|
2017-11-02 00:05:52 -05:00 |
|
cost_evaluator.cpp
|
remove iff
|
2018-06-14 16:08:48 -07:00 |
|
cost_evaluator.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
database.h
|
added missing Copyright forms
|
2015-06-10 11:54:02 -07:00 |
|
database.smt
|
Tabs, whitespace
|
2017-09-17 18:10:06 +01:00 |
|
diff_logic.h
|
Tabs, formatting.
|
2017-09-17 14:54:09 +01:00 |
|
dyn_ack.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
dyn_ack.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
elim_term_ite.cpp
|
removing dependencies on simplifier
|
2017-08-26 11:23:41 -07:00 |
|
elim_term_ite.h
|
removing dependencies on simplifier
|
2017-08-26 11:23:41 -07:00 |
|
expr_context_simplifier.cpp
|
remove iff
|
2018-06-14 16:08:48 -07:00 |
|
expr_context_simplifier.h
|
removing dependencies on simplifier
|
2017-08-26 11:23:41 -07:00 |
|
fingerprints.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
fingerprints.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
mam.cpp
|
delay updating parameters to ensure rewriting in asserted_formulas is applied using configuration overrides. Fixes build regression for tree_interpolation documentation test
|
2018-03-04 21:57:08 -08:00 |
|
mam.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
old_interval.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
old_interval.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
qi_queue.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
qi_queue.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt2_extra_cmds.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt2_extra_cmds.h
|
Added (include ...) SMT2 command.
|
2017-01-16 15:05:58 +00:00 |
|
smt_almost_cg_table.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_almost_cg_table.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_b_justification.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_bool_var_data.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_case_split_queue.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_case_split_queue.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_cg_table.cpp
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_cg_table.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_checker.cpp
|
remove iff
|
2018-06-14 16:08:48 -07:00 |
|
smt_checker.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_clause.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_clause.h
|
check with cube and clause
|
2018-06-14 16:08:49 -07:00 |
|
smt_conflict_resolution.cpp
|
remove iff
|
2018-06-14 16:08:48 -07:00 |
|
smt_conflict_resolution.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_consequences.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_context.cpp
|
check with cube and clause
|
2018-06-14 16:08:49 -07:00 |
|
smt_context.h
|
check with cube and clause
|
2018-06-14 16:08:49 -07:00 |
|
smt_context_inv.cpp
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_context_pp.cpp
|
check with cube and clause
|
2018-06-14 16:08:49 -07:00 |
|
smt_context_stat.cpp
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_enode.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_enode.h
|
n/a
|
2018-05-01 07:13:03 -07:00 |
|
smt_eq_justification.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_failure.h
|
add n-ary disjunction and conjunction
|
2016-07-01 08:15:50 -07:00 |
|
smt_farkas_util.cpp
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_farkas_util.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_for_each_relevant_expr.cpp
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_for_each_relevant_expr.h
|
Use override rather than virtual.
|
2018-02-10 09:56:33 +07:00 |
|
smt_implied_equalities.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_implied_equalities.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_internalizer.cpp
|
remove iff
|
2018-06-14 16:08:48 -07:00 |
|
smt_justification.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_justification.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_kernel.cpp
|
check with cube and clause
|
2018-06-14 16:08:49 -07:00 |
|
smt_kernel.h
|
check with cube and clause
|
2018-06-14 16:08:49 -07:00 |
|
smt_literal.cpp
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_literal.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
smt_model_checker.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_model_checker.h
|
fix #1365. Filter MBQI instantiations for as-array terms that lead the array theory to return unknown and therefore block further instantiations. as-array terms are at this point almost always created from internal model values so quantifier instantiations with these have little value, other than instantiations of other paraameters that may indepdendently help
|
2017-11-23 11:17:41 -08:00 |
|
smt_model_finder.cpp
|
remove iff
|
2018-06-14 16:08:48 -07:00 |
|
smt_model_finder.h
|
reducing dependencies on simplifier
|
2017-08-22 15:09:34 -07:00 |
|
smt_model_generator.cpp
|
merge with master
|
2018-03-25 14:57:01 -07:00 |
|
smt_model_generator.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_quantifier.cpp
|
fix #1545
|
2018-03-17 17:49:33 -07:00 |
|
smt_quantifier.h
|
Typo fixes.
|
2018-01-02 22:48:06 +07:00 |
|
smt_quantifier_instances.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
smt_quantifier_stat.cpp
|
remove iff
|
2018-06-14 16:08:48 -07:00 |
|
smt_quantifier_stat.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_quick_checker.cpp
|
remove iff
|
2018-06-14 16:08:48 -07:00 |
|
smt_quick_checker.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_relevancy.cpp
|
delay updating parameters to ensure rewriting in asserted_formulas is applied using configuration overrides. Fixes build regression for tree_interpolation documentation test
|
2018-03-04 21:57:08 -08:00 |
|
smt_relevancy.h
|
Use override rather than virtual.
|
2018-02-10 09:56:33 +07:00 |
|
smt_setup.cpp
|
Remove dead m_propagate_booleans param
|
2018-06-14 16:08:49 -07:00 |
|
smt_setup.h
|
add QF_DT
|
2017-09-17 01:39:39 +02:00 |
|
smt_solver.cpp
|
silence clang warning
|
2018-06-14 16:08:49 -07:00 |
|
smt_solver.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -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
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
smt_theory.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_theory.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_theory_var_list.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_types.h
|
perf(datatype): whole-graph implementation of occurs_check
|
2018-04-06 17:20:04 -05:00 |
|
smt_value_sort.cpp
|
support for smtlib2.6 datatype parsing
|
2017-09-04 21:12:43 -07:00 |
|
smt_value_sort.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
spanning_tree.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
spanning_tree_base.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
spanning_tree_def.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07: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
|
merge with 4.7.1
|
2018-05-22 17:10:36 -07:00 |
|
theory_arith_aux.h
|
merge with master
|
2018-03-25 14:57:01 -07:00 |
|
theory_arith_core.h
|
remove references to deprecated uses of PROOF_MODE #1531
|
2018-03-10 13:55:01 -05:00 |
|
theory_arith_def.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
theory_arith_eq.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_arith_int.h
|
merge with master
|
2018-03-25 14:57:01 -07:00 |
|
theory_arith_inv.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
theory_arith_nl.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_arith_pp.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_array.cpp
|
additional array functions exposed over API, ping #1223
|
2017-10-19 11:08:48 -07:00 |
|
theory_array.h
|
Use override rather than virtual.
|
2018-02-10 09:56:33 +07:00 |
|
theory_array_base.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_array_base.h
|
Use override rather than virtual.
|
2018-02-10 09:56:33 +07:00 |
|
theory_array_full.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_array_full.h
|
Use override rather than virtual.
|
2018-02-10 09:56:33 +07:00 |
|
theory_bv.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_bv.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_datatype.cpp
|
Fancy dots are not allowed here!!
|
2018-04-23 17:17:51 -04:00 |
|
theory_datatype.h
|
move some methods from header to cpp, format fixing, remove special characters
|
2018-04-07 17:34:46 -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
|
merge with master
|
2018-03-25 14:57:01 -07:00 |
|
theory_dense_diff_logic_def.h
|
merge with master
|
2018-03-25 14:57:01 -07: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
|
merge with master
|
2018-03-25 14:57:01 -07:00 |
|
theory_diff_logic_def.h
|
merge with master
|
2018-03-25 14:57:01 -07:00 |
|
theory_dl.cpp
|
Remove int64, uint64 typedefs in favor of int64_t / uint64_t.
|
2018-03-31 14:45:04 +07:00 |
|
theory_dl.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
theory_dummy.cpp
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
theory_dummy.h
|
Use override rather than virtual.
|
2018-02-10 09:56:33 +07:00 |
|
theory_fpa.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_fpa.h
|
Use override rather than virtual.
|
2018-02-10 09:56:33 +07:00 |
|
theory_lra.cpp
|
merge with master
|
2018-03-25 14:57:01 -07:00 |
|
theory_lra.h
|
merge with master
|
2018-03-25 14:57:01 -07: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 stubs for converting assertions, consolidate filter_model_converter
|
2017-11-17 14:51:13 -08:00 |
|
theory_pb.cpp
|
check with cube and clause
|
2018-06-14 16:08:49 -07:00 |
|
theory_pb.h
|
merge with master
|
2018-03-25 14:57:01 -07:00 |
|
theory_seq.cpp
|
tune for unit test, delay initialize re-solver
|
2018-05-13 11:49:33 -07:00 |
|
theory_seq.h
|
fix #1592 #1587
|
2018-04-25 11:18:24 +02:00 |
|
theory_seq_empty.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_str.cpp
|
fix #1662
|
2018-05-30 16:47:17 -07:00 |
|
theory_str.h
|
fix regex automata leaked memory
|
2018-04-12 14:35:29 -04:00 |
|
theory_utvpi.cpp
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
theory_utvpi.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_utvpi_def.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_wmaxsat.cpp
|
merge with master
|
2018-03-25 14:57:01 -07:00 |
|
theory_wmaxsat.h
|
merge with master
|
2018-03-25 14:57:01 -07:00 |
|
uses_theory.cpp
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
uses_theory.h
|
make include paths uniformly use path relative to src. #534
|
2017-07-31 13:24:11 -07:00 |
|
watch_list.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
watch_list.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
