| .. |
|
params
|
User control over more arith options
|
2018-06-14 16:08:49 -07:00 |
|
proto_model
|
sometimes comments are worth reading
|
2018-06-19 10:43:51 -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
|
Fix memory leak in asserted_formulas
|
2018-06-14 16:08:50 -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
|
improvements to arithmetic preprocessing simplificaiton and axiom generation for #1683
|
2018-06-19 07:04:39 -07: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
|
Restore assertion in smt_clause
|
2018-06-14 16:08:50 -07:00 |
|
smt_clause.h
|
check with cube and clause
|
2018-06-14 16:08:49 -07:00 |
|
smt_conflict_resolution.cpp
|
fixes to clause proof tracking
|
2018-06-14 16:08:50 -07:00 |
|
smt_conflict_resolution.h
|
fixes to clause proof tracking
|
2018-06-14 16:08:50 -07:00 |
|
smt_consequences.cpp
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
smt_context.cpp
|
fix #1681
|
2018-06-18 21:53:45 -07:00 |
|
smt_context.h
|
merge while skyping
|
2018-06-14 16:08:52 -07:00 |
|
smt_context_inv.cpp
|
revert fix to #1677
|
2018-06-18 21:23:13 -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
|
move to list of clauses
|
2018-06-14 16:08:50 -07:00 |
|
smt_kernel.h
|
move to list of clauses
|
2018-06-14 16:08:50 -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
|
debug model evaluator
|
2018-06-15 14:58:02 -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
|
fix #1681
|
2018-06-18 21:53:45 -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
|
fix a few build regressions
|
2018-06-14 16:08:52 -07:00 |
|
smt_setup.h
|
add QF_DT
|
2017-09-17 01:39:39 +02:00 |
|
smt_solver.cpp
|
first eufi example running
|
2018-06-14 16:08:52 -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
|
improvements to arithmetic preprocessing simplificaiton and axiom generation for #1683
|
2018-06-19 07:04:39 -07: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
|
add default method for fresh fp value, try to address OsX build
|
2018-06-19 10:02:31 -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
|
revert fix to #1677
|
2018-06-18 21:23:13 -07:00 |
|
theory_seq.h
|
selective expansion of strings for canonizer to fix #1690 regression
|
2018-06-18 20:37:39 -07:00 |
|
theory_seq_empty.h
|
Use nullptr.
|
2018-02-12 14:05:55 +07:00 |
|
theory_str.cpp
|
fix #1677
|
2018-06-18 11:22:01 -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 |
