Added function to select the next variable to split on (User-Propagator) #6096
Conversation
CEisenhofer
changed the title
| @@ -93,7 +93,7 @@ def is_fn(ty): | |||
| # Mapping to ML types | |||
| Type2ML = { VOID : 'unit', VOID_PTR : 'ptr', INT : 'int', UINT : 'int', INT64 : 'int', UINT64 : 'int', DOUBLE : 'float', | |||
| FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**', | |||
| BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string', LBOOL : 'uint' } | |||
| BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string', LBOOL : 'int' } | |||
There was a problem hiding this comment.
Z3_lbool is defined as an enum in z3_api.h. All enum types are translated uniformly. Is there an issue with this approach?
There was a problem hiding this comment.
Probably not. I thought it would be more consistent with the existing code, as PRINT_MODE and ERROR_CODE also have their own definitions.
There was a problem hiding this comment.
Correction: It seems to be necessary. I cannot use UINT/INT as the Python script does not add a cast otherwise. It works for the other enums that do not have definitions in the Python script, as they are only used as return types and not as arguments
scripts/update_api.py
Outdated
| } | ||
|
|
||
| # Mapping to .NET types | ||
| Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double', | ||
| FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'byte', SYMBOL : 'IntPtr', | ||
| PRINT_MODE : 'uint', ERROR_CODE : 'uint', CHAR : 'char', CHAR_PTR : 'IntPtr' } | ||
| PRINT_MODE : 'uint', ERROR_CODE : 'uint', CHAR : 'char', CHAR_PTR : 'IntPtr', LBOOL : 'uint' } |
| @@ -4871,7 +4871,7 @@ extern "C" { | |||
| /** | |||
| \brief Return \c Z3_L_TRUE if \c a is true, \c Z3_L_FALSE if it is false, and \c Z3_L_UNDEF otherwise. | |||
|
|
|||
| def_API('Z3_get_bool_value', INT, (_in(CONTEXT), _in(AST))) | |||
| def_API('Z3_get_bool_value', LBOOL, (_in(CONTEXT), _in(AST))) | |||
There was a problem hiding this comment.
before LBOOL was an INT. Should it ever be a UINT?
There was a problem hiding this comment.
All other enums are casted to uint but right; int makes more sense
src/sat/smt/user_solver.h
Outdated
| @@ -94,7 +98,7 @@ namespace user_solver { | |||
| void propagate_consequence(prop_info const& prop); | |||
| void propagate_new_fixed(prop_info const& prop); | |||
|
|
|||
| void validate_propagation(); | |||
| void validate_propagation(); | |||
No description provided.