z3-src 503.2.0

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

/*++
Copyright (c) 2024 Microsoft Corporation

Module Name:

    model_params.hpp

Abstract:

    Parameters for the 'model' module.

--*/
#pragma once

#include "util/params.h"
#include "util/gparams.h"

#define MODEL_PARAMS_LIST(UINT_, BOOL_, DOUBLE_, STRING_, SYMBOL_) \
  BOOL_(partial,         "partial",         false,  "enable/disable partial function interpretations") \
  BOOL_(v1,              "v1",              false,  "use Z3 version 1.x pretty printer") \
  BOOL_(v2,              "v2",              false,  "use Z3 version 2.x (x <= 16) pretty printer") \
  BOOL_(compact,         "compact",         true,   "try to compact function graph (i.e., function interpretations that are lookup tables)") \
  BOOL_(inline_def,      "inline_def",      false,  "inline local function definitions ignoring possible expansion") \
  BOOL_(user_functions,  "user_functions",  true,   "include user defined functions in model") \
  BOOL_(completion,      "completion",      false,  "enable/disable model completion")

Z3_DEFINE_MODULE_PARAMS(model_params, "model", MODEL_PARAMS_LIST, nullptr);

#undef MODEL_PARAMS_LIST