From 342d2d9f5cd3f89289d84e2dc695516ec959e252 Mon Sep 17 00:00:00 2001 From: Bruno Schmitt Date: Fri, 10 Feb 2017 17:26:45 -0800 Subject: New fixed point data type. Expose all options to command line. Expose search statistics to users. --- src/base/abci/abc.c | 218 ++++++++++++++++++++++++++++++++++++++++++- src/sat/satoko/act_var.h | 38 +++++++- src/sat/satoko/satoko.h | 27 +++++- src/sat/satoko/solver.h | 13 --- src/sat/satoko/solver_api.c | 11 ++- src/sat/satoko/types.h | 32 ++++--- src/sat/satoko/utils/fixed.h | 67 +++++++++++++ 7 files changed, 363 insertions(+), 43 deletions(-) create mode 100644 src/sat/satoko/utils/fixed.h (limited to 'src') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 26e9c0f8..ea0ed377 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -23326,7 +23326,11 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv ) satoko_default_opts(&opts); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Chv" ) ) != EOF ) +#ifdef SATOKO_ACT_VAR_FIXED + while ( ( c = Extra_UtilGetopt( argc, argv, "CPDEFGHIJKLMNOQRSTUhv" ) ) != EOF ) +#else + while ( ( c = Extra_UtilGetopt( argc, argv, "CPDEFGHIJKLMNOQRShv" ) ) != EOF ) +#endif { switch ( c ) { @@ -23341,6 +23345,184 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( opts.conf_limit < 0 ) goto usage; break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + opts.prop_limit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( opts.prop_limit < 0 ) + goto usage; + break; + case 'D': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-D\" should be followed by an float.\n" ); + goto usage; + } + opts.f_rst = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( opts.f_rst < 0 ) + goto usage; + break; + case 'E': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-E\" should be followed by an float.\n" ); + goto usage; + } + opts.b_rst = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( opts.b_rst < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + opts.fst_block_rst = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + opts.sz_lbd_bqueue = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'H': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" ); + goto usage; + } + opts.sz_trail_bqueue = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + opts.n_conf_fst_reduce = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'J': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" ); + goto usage; + } + opts.inc_reduce = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" ); + goto usage; + } + opts.inc_special_reduce = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'L': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + opts.lbd_freeze_clause = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + opts.learnt_ratio = atof(argv[globalUtilOptind]) / 100; + globalUtilOptind++; + if ( opts.learnt_ratio < 0 ) + goto usage; + break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + opts.garbage_max_ratio = atof(argv[globalUtilOptind]) / 100; + globalUtilOptind++; + if ( opts.garbage_max_ratio < 0 ) + goto usage; + break; + case 'O': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); + goto usage; + } + opts.clause_max_sz_bin_resol = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'Q': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); + goto usage; + } + opts.clause_min_lbd_bin_resol = (unsigned)atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an float.\n" ); + goto usage; + } + opts.clause_decay = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( opts.clause_decay < 0 ) + goto usage; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an float.\n" ); + goto usage; + } + opts.var_decay = atof(argv[globalUtilOptind]); + globalUtilOptind++; + if ( opts.var_decay < 0 ) + goto usage; + break; +#ifdef SATOKO_ACT_VAR_FIXED + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an float.\n" ); + goto usage; + } + opts.var_act_limit = (unsigned)strtol(argv[globalUtilOptind], NULL, 16); + globalUtilOptind++; + break; + case 'U': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-U\" should be followed by an float.\n" ); + goto usage; + } + opts.var_act_rescale = (unsigned)strtol(argv[globalUtilOptind], NULL, 16); + globalUtilOptind++; + break; +#endif case 'h': goto usage; case 'v': @@ -23379,9 +23561,37 @@ int Abc_CommandSatoko( Abc_Frame_t * pAbc, int argc, char ** argv ) } usage: - Abc_Print( -2, "usage: satoko [-CILDE num] [-hv].cnf\n" ); +#ifdef SATOKO_ACT_VAR_FIXED + Abc_Print( -2, "usage: satoko [-CPDEFGHIJKLMNOQRSTU num] [-hv].cnf\n" ); +#else + Abc_Print( -2, "usage: satoko [-CPDEFGHIJKLMNOQRS num] [-hv].cnf\n" ); +#endif Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", opts.conf_limit ); - Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" ); + Abc_Print( -2, "\t-P num : limit on the number of propagations [default = %d]\n", opts.conf_limit ); + Abc_Print( -2, "\n\tConstants used for restart heuristic:\n"); + Abc_Print( -2, "\t-D num : Constant value used by restart heuristics in forcing restarts [default = %f]\n", opts.f_rst ); + Abc_Print( -2, "\t-E num : Constant value used by restart heuristics in blocking restarts [default = %f]\n", opts.b_rst ); + Abc_Print( -2, "\t-F num : Lower bound n.of conflicts for start blocking restarts [default = %d]\n", opts.fst_block_rst ); + Abc_Print( -2, "\t-G num : Size of the moving avarege queue for LBD (force restart) [default = %d]\n", opts.sz_lbd_bqueue ); + Abc_Print( -2, "\t-H num : Size of the moving avarege queue for Trail size (block restart) [default = %d]\n", opts.sz_trail_bqueue ); + Abc_Print( -2, "\n\tConstants used for clause database reduction heuristic:\n"); + Abc_Print( -2, "\t-I num : N.of conflicts before first clause databese reduction [default = %d]\n", opts.n_conf_fst_reduce ); + Abc_Print( -2, "\t-J num : Increment to reduce [default = %d]\n", opts.inc_reduce ); + Abc_Print( -2, "\t-K num : Special increment to reduce [default = %d]\n", opts.inc_special_reduce ); + Abc_Print( -2, "\t-L num : Protecs clauses from deletion for one turn if its LBD is lower [default = %d]\n", opts.lbd_freeze_clause ); + Abc_Print( -2, "\t-M num : Percentage of learned clauses to remove [default = %d]\n", ( int )( 100 * opts.learnt_ratio ) ); + Abc_Print( -2, "\t-N num : Max percentage of garbage in clause database [default = %d]\n", ( int )( 100 * opts.garbage_max_ratio ) ); + Abc_Print( -2, "\n\tConstants used for binary resolution (clause minimization):\n"); + Abc_Print( -2, "\t-O num : Max clause size for binary resolution [default = %d]\n", opts.clause_max_sz_bin_resol ); + Abc_Print( -2, "\t-Q num : Min clause LBD for binary resolution [default = %d]\n", opts.clause_min_lbd_bin_resol ); + Abc_Print( -2, "\n\tConstants used for branching (VSIDS heuristic):\n"); + Abc_Print( -2, "\t-R num : Clause activity decay factor (when using float clause activity) [default = %f]\n", opts.clause_decay ); + Abc_Print( -2, "\t-S num : Varibale activity decay factor [default = %f]\n", opts.var_decay ); +#ifdef SATOKO_ACT_VAR_FIXED + Abc_Print( -2, "\t-T num : Variable activity limit valeu [default = 0x%08X]\n", opts.var_act_limit ); + Abc_Print( -2, "\t-U num : Variable activity re-scale factor [default = 0x%08X]\n", opts.var_act_rescale ); +#endif + Abc_Print( -2, "\n\t-v : prints verbose information [default = %s]\n", opts.verbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -38219,7 +38429,7 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fExtractAll ) { char Buffer[1000]; - Gia_Obj_t * pObj; + Gia_Obj_t * pObj; int i, nDigits = Abc_Base10Log(Gia_ManPoNum(pAbc->pGia)); Gia_ManForEachPo( pAbc->pGia, pObj, i ) { diff --git a/src/sat/satoko/act_var.h b/src/sat/satoko/act_var.h index aa8a76ab..b1fdb756 100644 --- a/src/sat/satoko/act_var.h +++ b/src/sat/satoko/act_var.h @@ -16,7 +16,7 @@ #include "misc/util/abc_global.h" ABC_NAMESPACE_HEADER_START -#if defined SATOKO_ACT_VAR_DBLE || defined SATOKO_ACT_VAR_FLOAT +#if defined SATOKO_ACT_VAR_DBLE /** Re-scale the activity value for all variables. */ static inline void var_act_rescale(solver_t *s) @@ -25,8 +25,8 @@ static inline void var_act_rescale(solver_t *s) act_t *activity = vec_act_data(s->activity); for (i = 0; i < vec_act_size(s->activity); i++) - activity[i] *= VAR_ACT_RESCALE; - s->var_act_inc *= VAR_ACT_RESCALE; + activity[i] *= s->opts.var_act_rescale; + s->var_act_inc *= s->opts.var_act_rescale; } /** Increment the activity value of one variable ('var') @@ -36,7 +36,7 @@ static inline void var_act_bump(solver_t *s, unsigned var) act_t *activity = vec_act_data(s->activity); activity[var] += s->var_act_inc; - if (activity[var] > VAR_ACT_LIMIT) + if (activity[var] > s->opts.var_act_limit) var_act_rescale(s); if (heap_in_heap(s->var_order, var)) heap_decrease(s->var_order, var); @@ -49,6 +49,34 @@ static inline void var_act_decay(solver_t *s) s->var_act_inc *= (1 / s->opts.var_decay); } +#elif defined(SATOKO_ACT_VAR_FIXED) + +static inline void var_act_rescale(solver_t *s) +{ + unsigned i; + act_t *activity = (act_t *)vec_act_data(s->activity); + + for (i = 0; i < vec_act_size(s->activity); i++) + activity[i] = fixed_mult(activity[i], VAR_ACT_RESCALE); + s->var_act_inc = fixed_mult(s->var_act_inc, VAR_ACT_RESCALE); +} + +static inline void var_act_bump(solver_t *s, unsigned var) +{ + act_t *activity = (act_t *)vec_act_data(s->activity); + + activity[var] = fixed_add(activity[var], s->var_act_inc); + if (activity[var] > VAR_ACT_LIMIT) + var_act_rescale(s); + if (heap_in_heap(s->var_order, var)) + heap_decrease(s->var_order, var); +} + +static inline void var_act_decay(solver_t *s) +{ + s->var_act_inc = fixed_mult(s->var_act_inc, dble2fixed(1 / s->opts.var_decay)); +} + #else static inline void var_act_rescale(solver_t *s) @@ -77,7 +105,7 @@ static inline void var_act_decay(solver_t *s) s->var_act_inc += (s->var_act_inc >> 4); } -#endif /* SATOKO_ACT_VAR_DBLE || SATOKO_ACT_VAR_FLOAT */ +#endif /* SATOKO_ACT_VAR_DBLE || SATOKO_ACT_VAR_FIXED */ ABC_NAMESPACE_HEADER_END #endif /* satoko__act_var_h */ diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h index fb07c6f9..363fe2fd 100644 --- a/src/sat/satoko/satoko.h +++ b/src/sat/satoko/satoko.h @@ -32,7 +32,7 @@ typedef struct satoko_opts satoko_opts_t; struct satoko_opts { /* Limits */ long conf_limit; /* Limit on the n.of conflicts */ - long prop_limit; /* Limit on the n.of implications */ + long prop_limit; /* Limit on the n.of propagations */ /* Constants used for restart heuristic */ double f_rst; /* Used to force a restart */ @@ -42,7 +42,7 @@ struct satoko_opts { unsigned sz_trail_bqueue; /* Size of the moving avarege queue for Trail size (block restart) */ /* Constants used for clause database reduction heuristic */ - unsigned n_conf_fst_reduce; /* N.of conflicts before first reduction */ + unsigned n_conf_fst_reduce; /* N.of conflicts before first clause databese reduction */ unsigned inc_reduce; /* Increment to reduce */ unsigned inc_special_reduce; /* Special increment to reduce */ unsigned lbd_freeze_clause; @@ -50,7 +50,9 @@ struct satoko_opts { /* VSIDS heuristic */ float clause_decay; - act_t var_decay; + double var_decay; + act_t var_act_limit; + act_t var_act_rescale; /* Binary resolution */ unsigned clause_max_sz_bin_resol; @@ -59,6 +61,21 @@ struct satoko_opts { char verbose; }; +typedef struct satoko_stats satoko_stats_t; +struct satoko_stats { + unsigned n_starts; + unsigned n_reduce_db; + + long n_decisions; + long n_propagations; + long n_inspects; + long n_conflicts; + + long n_original_lits; + long n_learnt_lits; +}; + + //===------------------------------------------------------------------------=== extern satoko_t *satoko_create(void); extern void satoko_destroy(satoko_t *); @@ -81,7 +98,9 @@ extern int satoko_solve(satoko_t *); * - The return value is either the size of the array or -1 in case the final * conflict cluase was not generated. */ -extern int satoko_final_conflict(satoko_t *, unsigned *); +extern int satoko_final_conflict(satoko_t *, unsigned *); + +extern satoko_stats_t satoko_stats(satoko_t *); ABC_NAMESPACE_HEADER_END #endif /* satoko__satoko_h */ diff --git a/src/sat/satoko/solver.h b/src/sat/satoko/solver.h index fe1d1ef5..a46b0c9d 100644 --- a/src/sat/satoko/solver.h +++ b/src/sat/satoko/solver.h @@ -38,19 +38,6 @@ enum { #define UNDEF 0xFFFFFFFF -struct satoko_stats { - unsigned n_starts; - unsigned n_reduce_db; - - long n_decisions; - long n_propagations; - long n_inspects; - long n_conflicts; - - long n_original_lits; - long n_learnt_lits; -}; - typedef struct solver_t_ solver_t; struct solver_t_ { /* User data */ diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c index 980cc160..ccab7685 100644 --- a/src/sat/satoko/solver_api.c +++ b/src/sat/satoko/solver_api.c @@ -12,8 +12,8 @@ #include #include "act_var.h" -#include "utils/misc.h" #include "solver.h" +#include "utils/misc.h" #include "misc/util/abc_global.h" ABC_NAMESPACE_IMPL_START @@ -167,7 +167,9 @@ void satoko_default_opts(satoko_opts_t *opts) opts->lbd_freeze_clause = 30; opts->learnt_ratio = 0.5; /* VSIDS heuristic */ - opts->var_decay = (act_t) 0.95; + opts->var_act_limit = VAR_ACT_LIMIT; + opts->var_act_rescale = VAR_ACT_RESCALE; + opts->var_decay = VAR_ACT_DECAY; opts->clause_decay = (clause_act_t) 0.995; /* Binary resolution */ opts->clause_max_sz_bin_resol = 30; @@ -308,4 +310,9 @@ int satoko_final_conflict(solver_t *s, unsigned *out) } +satoko_stats_t satoko_stats(satoko_t *s) +{ + return s->stats; +} + ABC_NAMESPACE_IMPL_END diff --git a/src/sat/satoko/types.h b/src/sat/satoko/types.h index ee9363bc..7865ab0e 100644 --- a/src/sat/satoko/types.h +++ b/src/sat/satoko/types.h @@ -9,21 +9,22 @@ #ifndef satoko__types_h #define satoko__types_h +#include "utils/fixed.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_VAR_FLOAT +#define SATOKO_ACT_VAR_DBLE +// #define SATOKO_ACT_VAR_FIXED // #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 + #define VAR_ACT_DECAY (double)0.95 typedef double act_t; typedef vec_dble_t vec_act_t ; #define vec_act_alloc(size) vec_dble_alloc(size) @@ -32,18 +33,19 @@ ABC_NAMESPACE_HEADER_START #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) +#elif defined(SATOKO_ACT_VAR_FIXED) + #define VAR_ACT_INIT_INC FIXED_ONE + #define VAR_ACT_LIMIT (fixed_t)0xDFFFFFFF + #define VAR_ACT_RESCALE (fixed_t)0x00000012 + #define VAR_ACT_DECAY (double)0.96 + typedef fixed_t act_t; + typedef vec_uint_t vec_act_t; + #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) #else #define VAR_ACT_INIT_INC (1 << 5) typedef unsigned act_t; diff --git a/src/sat/satoko/utils/fixed.h b/src/sat/satoko/utils/fixed.h new file mode 100644 index 00000000..91fc9b79 --- /dev/null +++ b/src/sat/satoko/utils/fixed.h @@ -0,0 +1,67 @@ +//===--- sort.h -------------------------------------------------------------=== +// +// satoko: Satisfiability solver +// +// This file is distributed under the BSD 2-Clause License. +// See LICENSE for details. +// +//===------------------------------------------------------------------------=== +#ifndef satoko__utils__fixed_h +#define satoko__utils__fixed_h + +#include "misc.h" + +#include "misc/util/abc_global.h" +ABC_NAMESPACE_HEADER_START + +typedef unsigned fixed_t; +static const int FIXED_W_BITS = 16; /* */ +static const int FIXED_F_BITS = 32 - FIXED_W_BITS; +static const int FIXED_F_MASK = (1 << FIXED_F_BITS) - 1; +static const fixed_t FIXED_MAX = 0xFFFFFFFF; +static const fixed_t FIXED_MIN = 0x00000000; +static const fixed_t FIXED_ONE = (1 << FIXED_F_BITS); + +/* Conversion functions */ +static inline fixed_t uint2fixed(unsigned a) { return a * FIXED_ONE; } +static inline unsigned fixed2uint(fixed_t a) +{ + return (a + (FIXED_ONE >> 1)) / FIXED_ONE; +} + +static inline float fixed2float(fixed_t a) { return (float)a / FIXED_ONE; } +static inline fixed_t float2fixed(float a) +{ + float temp = a * FIXED_ONE; + temp += (temp >= 0) ? 0.5f : -0.5f; + return (fixed_t)temp; +} + +static inline double fixed2dble(fixed_t a) { return (double)a / FIXED_ONE; } +static inline fixed_t dble2fixed(double a) +{ + double temp = a * FIXED_ONE; + temp += (temp >= 0) ? 0.5f : -0.5f; + return (fixed_t)temp; +} + +static inline fixed_t fixed_add(fixed_t a, fixed_t b) { return (a + b); } +static inline fixed_t fixed_mult(fixed_t a, fixed_t b) +{ + unsigned hi_a = (a >> FIXED_F_BITS), lo_a = (a & FIXED_F_MASK); + unsigned hi_b = (b >> FIXED_F_BITS), lo_b = (b & FIXED_F_MASK); + unsigned lo_ab = lo_a * lo_b; + unsigned ab_ab = (hi_a * lo_b) + (lo_a * hi_b); + unsigned hi_ret = (hi_a * hi_b) + (ab_ab >> FIXED_F_BITS); + unsigned lo_ret = lo_ab + (ab_ab << FIXED_W_BITS); + + /* Carry */ + if (lo_ret < lo_ab) + hi_ret++; + + return (hi_ret << FIXED_F_BITS) | (lo_ret >> FIXED_W_BITS); +} + +ABC_NAMESPACE_HEADER_END + +#endif /* satoko__utils__fixed_h */ -- cgit v1.2.3