mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
Typo fixes.
This commit is contained in:
parent
a58bc72dfb
commit
5bd93b8a77
|
@ -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
|
||||
===========
|
||||
|
|
|
@ -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.'),
|
||||
|
|
Loading…
Reference in a new issue