diff options
| author | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-09 05:17:50 -0800 |
|---|---|---|
| committer | Bruno Schmitt <bruno@oschmitt.com> | 2017-02-09 05:17:50 -0800 |
| commit | 871899dceac294f2b76c055a42d87176224028f2 (patch) | |
| tree | be960be285aeeee82adb0de91f0e60022b835bf8 /src/sat/satoko/types.h | |
| parent | 040b88a7c6bc437f6f9dc792510d5d905b516eb5 (diff) | |
| download | abc-871899dceac294f2b76c055a42d87176224028f2.tar.gz abc-871899dceac294f2b76c055a42d87176224028f2.tar.bz2 abc-871899dceac294f2b76c055a42d87176224028f2.zip | |
- Adding a compile time option to use floats for var activity (now it can be either ‘double’, ‘float’ or ‘unsigned’ (default))
- Adding vector of ‘float’
- Adding an option to configure the ratio of learnt clauses to be kept in clause database at each reduction (0 means no reduction).
- Other small changes.
Diffstat (limited to 'src/sat/satoko/types.h')
| -rw-r--r-- | src/sat/satoko/types.h | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/src/sat/satoko/types.h b/src/sat/satoko/types.h index 2811c2c6..ee9363bc 100644 --- a/src/sat/satoko/types.h +++ b/src/sat/satoko/types.h @@ -10,23 +10,40 @@ #define satoko__types_h #include "utils/vec/vec_dble.h" +#include "utils/vec/vec_flt.h" #include "utils/vec/vec_uint.h" #include "misc/util/abc_global.h" ABC_NAMESPACE_HEADER_START -#define SATOKO_ACT_VAR_DBLE -#define SATOKO_ACT_CLAUSE_FLOAT +// #define SATOKO_ACT_VAR_DBLE +// #define SATOKO_ACT_VAR_FLOAT +// #define SATOKO_ACT_CLAUSE_FLOAT #ifdef SATOKO_ACT_VAR_DBLE #define VAR_ACT_INIT_INC 1.0 + #define VAR_ACT_LIMIT (double)1e100 + #define VAR_ACT_RESCALE (double)1e-100 typedef double act_t; typedef vec_dble_t vec_act_t ; #define vec_act_alloc(size) vec_dble_alloc(size) #define vec_act_free(vec) vec_dble_free(vec) #define vec_act_size(vec) vec_dble_size(vec) + #define vec_act_data(vec) vec_dble_data(vec) #define vec_act_at(vec, idx) vec_dble_at(vec, idx) #define vec_act_push_back(vec, value) vec_dble_push_back(vec, value) +#elif defined(SATOKO_ACT_VAR_FLOAT) + #define VAR_ACT_INIT_INC 1.0 + #define VAR_ACT_LIMIT (float)1e20 + #define VAR_ACT_RESCALE (float)1e-20 + typedef float act_t; + typedef vec_flt_t vec_act_t ; + #define vec_act_alloc(size) vec_flt_alloc(size) + #define vec_act_free(vec) vec_flt_free(vec) + #define vec_act_size(vec) vec_flt_size(vec) + #define vec_act_data(vec) vec_flt_data(vec) + #define vec_act_at(vec, idx) vec_flt_at(vec, idx) + #define vec_act_push_back(vec, value) vec_flt_push_back(vec, value) #else #define VAR_ACT_INIT_INC (1 << 5) typedef unsigned act_t; @@ -34,6 +51,7 @@ ABC_NAMESPACE_HEADER_START #define vec_act_alloc(size) vec_uint_alloc(size) #define vec_act_free(vec) vec_uint_free(vec) #define vec_act_size(vec) vec_uint_size(vec) + #define vec_act_data(vec) vec_uint_data(vec) #define vec_act_at(vec, idx) vec_uint_at(vec, idx) #define vec_act_push_back(vec, value) vec_uint_push_back(vec, value) #endif /* SATOKO_ACT_VAR_DBLE */ |