mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Wc++11-extensions
This commit is contained in:
parent
d01c3491a6
commit
4e59ba922b
|
@ -176,7 +176,7 @@ typedef enum
|
|||
Z3_PARAMETER_SYMBOL,
|
||||
Z3_PARAMETER_SORT,
|
||||
Z3_PARAMETER_AST,
|
||||
Z3_PARAMETER_FUNC_DECL,
|
||||
Z3_PARAMETER_FUNC_DECL
|
||||
} Z3_parameter_kind;
|
||||
|
||||
/**
|
||||
|
|
|
@ -1143,7 +1143,7 @@ typedef app proof; /* a proof is just an applicaton */
|
|||
|
||||
enum label_op_kind {
|
||||
OP_LABEL,
|
||||
OP_LABEL_LIT,
|
||||
OP_LABEL_LIT
|
||||
};
|
||||
|
||||
/**
|
||||
|
|
|
@ -37,7 +37,7 @@ class expr_pattern_match {
|
|||
CHECK_TERM,
|
||||
SET_BOUND,
|
||||
CHECK_BOUND,
|
||||
YIELD,
|
||||
YIELD
|
||||
};
|
||||
|
||||
struct instr {
|
||||
|
|
|
@ -65,7 +65,7 @@ enum case_split_strategy {
|
|||
CS_ACTIVITY_WITH_CACHE, // case split based on activity and cache the activity
|
||||
CS_RELEVANCY, // case split based on relevancy
|
||||
CS_RELEVANCY_ACTIVITY, // case split based on relevancy and activity
|
||||
CS_RELEVANCY_GOAL, // based on relevancy and the current goal
|
||||
CS_RELEVANCY_GOAL // based on relevancy and the current goal
|
||||
};
|
||||
|
||||
struct smt_params : public preprocessor_params,
|
||||
|
|
|
@ -28,7 +28,7 @@ namespace smt {
|
|||
enum config_mode {
|
||||
CFG_BASIC, // install theories based on user options
|
||||
CFG_LOGIC, // install theories and configure Z3 based on the value of the parameter set-logic.
|
||||
CFG_AUTO, // install theories based on static features of the input formula
|
||||
CFG_AUTO // install theories based on static features of the input formula
|
||||
};
|
||||
|
||||
class context;
|
||||
|
|
Loading…
Reference in a new issue