From 5bd93b8a778139ce238d6dcc024db606855e8f9b Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Fri, 12 Oct 2018 23:38:53 +0700 Subject: [PATCH] Typo fixes. --- RELEASE_NOTES | 4 ++-- src/sat/sat_params.pyg | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/RELEASE_NOTES b/RELEASE_NOTES index 3337f098b..acdb627d8 100644 --- a/RELEASE_NOTES +++ b/RELEASE_NOTES @@ -21,7 +21,7 @@ Version 4.8.0 extracting models from apply_result have been replaced. - An optional mode handles xor constraints using a custom xor propagator. It is off by default and its value not demonstrated. - - The SAT solver includes new inprocessing technques that are available during simplification. + - The SAT solver includes new inprocessing techniques that are available during simplification. It performs asymmetric tautology elimination by default, and one can turn on more powerful inprocessing techniques (known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs. Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged @@ -318,7 +318,7 @@ First source code release (October 2, 2012) - Added support for numbers in scientific notation at Z3_ast Z3_mk_numeral(__in Z3_context c, __in Z3_string numeral, __in Z3_sort ty). -- New builtin symbols in the arithmetic theory: pi, euler, sin, cos, tan, asin, acos, atan, sinh, cosh, tanh, asinh, acosh, atanh. The first two are constants, and the others are unary functions. These symbols are not available if the a SMT 2.0 logic is specified (e.g., QF_LRA, QF_NRA, QF_LIA, etc) because these symbols are not defined in these logics. That is, the new symbols are only available if the logic is not specified. +- New builtin symbols in the arithmetic theory: pi, euler, sin, cos, tan, asin, acos, atan, sinh, cosh, tanh, asinh, acosh, atanh. The first two are constants, and the others are unary functions. These symbols are not available if a SMT 2.0 logic is specified (e.g., QF_LRA, QF_NRA, QF_LIA, etc) because these symbols are not defined in these logics. That is, the new symbols are only available if the logic is not specified. Version 4.1 =========== diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 6202ff155..3f0479707 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -15,7 +15,7 @@ def_module_params('sat', ('restart.margin', DOUBLE, 1.1, 'margin between fast and slow restart factors. For ema'), ('restart.emafastglue', DOUBLE, 3e-2, 'ema alpha factor for fast moving average'), ('restart.emaslowglue', DOUBLE, 1e-5, 'ema alpha factor for slow moving average'), - ('variable_decay', UINT, 110, 'multiplier (divided by 100) for the VSIDS activity increement'), + ('variable_decay', UINT, 110, 'multiplier (divided by 100) for the VSIDS activity increment'), ('inprocess.max', UINT, UINT_MAX, 'maximal number of inprocessing passes'), ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'), ('branching.anti_exploration', BOOL, False, 'apply anti-exploration heuristic for branch selection'), @@ -58,7 +58,7 @@ def_module_params('sat', # - psat: Let psat_heur := (Sum_{clause C} (psat.clause_base ^ {-|C|+1})) / |freevars|^psat.var_exp # Cut if the value of psat_heur exceeds psat.trigger # - adaptive_freevars: Cut if the number of current unassigned variables drops below a fraction of free variables - # at the time of the last conflict. The fraction is increased every time the a cutoff is created. + # at the time of the last conflict. The fraction is increased every time the cutoff is created. # - adative_psat: Cut based on psat_heur in an adaptive way. ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'), ('lookahead.cube.depth', UINT, 1, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'),