| .. |
|
add_bounds_tactic.cpp
|
address race condition in cleanup methods
|
2014-09-05 11:18:34 -07:00 |
|
add_bounds_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
arith_bounds_tactic.cpp
|
added missing Copyright forms
|
2015-06-10 11:54:02 -07:00 |
|
arith_bounds_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
bound_manager.cpp
|
using a consistent naming convention for naming tactic subfolders
|
2012-10-24 15:11:44 -07:00 |
|
bound_manager.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
bound_propagator.cpp
|
saved params work
|
2012-11-29 17:19:12 -08:00 |
|
bound_propagator.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
bv2int_rewriter.cpp
|
fix quantifier elimination bugs reported by Berdine and Bornat
|
2014-07-14 15:38:22 +02:00 |
|
bv2int_rewriter.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
bv2real_rewriter.cpp
|
using a consistent naming convention for naming tactic subfolders
|
2012-10-24 15:11:44 -07:00 |
|
bv2real_rewriter.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
card2bv_tactic.cpp
|
revising pd-maxres
|
2015-08-23 10:53:39 -07:00 |
|
card2bv_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
degree_shift_tactic.cpp
|
address race condition in cleanup methods
|
2014-09-05 11:18:34 -07:00 |
|
degree_shift_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
diff_neq_tactic.cpp
|
address race condition in cleanup methods
|
2014-09-05 11:18:34 -07:00 |
|
diff_neq_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
elim01_tactic.cpp
|
create proof object in elim01. Codeplex issue 158
|
2015-01-03 11:04:08 -08:00 |
|
elim01_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
eq2bv_tactic.cpp
|
fix for mising handling of quantifiers in tactic. Bug #324
|
2015-11-17 18:38:37 -08:00 |
|
eq2bv_tactic.h
|
add tactic to recognize small discrete domains and convert them into bit-vectors
|
2015-08-20 06:39:11 -07:00 |
|
factor_tactic.cpp
|
address race condition in cleanup methods
|
2014-09-05 11:18:34 -07:00 |
|
factor_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
fix_dl_var_tactic.cpp
|
fix crash reported by Jojanovich, github issue 45'
|
2015-04-20 00:55:30 +02:00 |
|
fix_dl_var_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
fm_tactic.cpp
|
use signed character type declarations for cross platform compilation. Fixes issue #210
|
2015-09-05 16:30:58 -07:00 |
|
fm_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
lia2card_tactic.cpp
|
Fix for #343. Optimizations introduced on 8-10-2015 were too agressive. Remove unreferened variable
|
2015-12-01 13:43:47 -08:00 |
|
lia2card_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
lia2pb_tactic.cpp
|
populate proofs in opt specific tactics
|
2015-01-05 16:44:33 -08:00 |
|
lia2pb_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
linear_equation.cpp
|
using a consistent naming convention for naming tactic subfolders
|
2012-10-24 15:11:44 -07:00 |
|
linear_equation.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
nla2bv_tactic.cpp
|
Add get_sort(expr * n) function that does not depend on ast_manager. Move power_of_two to rational class. Add arith_recognizers and bv_recognizers classes. The two new classes contain the 'read-only' methods from arith_util and bv_util.
|
2012-12-18 14:44:51 -08:00 |
|
nla2bv_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
normalize_bounds_tactic.cpp
|
address race condition in cleanup methods
|
2014-09-05 11:18:34 -07:00 |
|
normalize_bounds_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
pb2bv_model_converter.cpp
|
using a consistent naming convention for naming tactic subfolders
|
2012-10-24 15:11:44 -07:00 |
|
pb2bv_model_converter.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
pb2bv_tactic.cpp
|
Fixed collect_param_descrs in pb2bv tactic.
|
2015-06-08 15:36:00 +01:00 |
|
pb2bv_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
probe_arith.cpp
|
fix regressions in nl/smt
|
2015-05-16 19:08:37 +01:00 |
|
probe_arith.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
propagate_ineqs_tactic.cpp
|
Revert "propagate_ineqs synchronization fix"
|
2015-02-08 15:16:24 +00:00 |
|
propagate_ineqs_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
purify_arith_tactic.cpp
|
debugging opt
|
2014-03-17 10:34:32 -07:00 |
|
purify_arith_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
|
recover_01_tactic.cpp
|
address race condition in cleanup methods
|
2014-09-05 11:18:34 -07:00 |
|
recover_01_tactic.h
|
update header guards to be C++ style. Fixes issue #9
|
2015-07-08 23:18:40 -07:00 |
