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
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Diagnostics.Contracts;
namespace Microsoft.Boogie.SMTLib
{
public class OptionValue
{
public readonly string Option;
public readonly string Value;
[ContractInvariantMethod]
void ObjectInvariant()
{
Contract.Invariant(Option != null);
Contract.Invariant(Value != null);
}
public OptionValue(string option, string value)
{
Contract.Requires(option != null);
Contract.Requires(value != null);
Option = option;
Value = value;
}
}
public class SMTLibProverOptions : ProverOptions
{
public bool UseWeights = true;
public bool UseLabels { get { return UseZ3; } }
public List<OptionValue> SmtOptions = new List<OptionValue>();
public List<string> SolverArguments = new List<string>();
public bool MultiTraces = false;
public string Logic = "";
// Z3 specific (at the moment; some of them make sense also for other provers)
public bool UseZ3 = true;
public string Inspector = null;
public bool OptimizeForBv = false;
public bool ExpectingModel()
{
return CommandLineOptions.Clo.PrintErrorModel >= 1 ||
CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
CommandLineOptions.Clo.ModelViewFile != null ||
CommandLineOptions.Clo.ContractInfer ||
CommandLineOptions.Clo.LazyInlining > 0 ||
CommandLineOptions.Clo.StratifiedInlining > 0;
}
public void AddSolverArgument(string s)
{
SolverArguments.Add(s);
}
public void AddSmtOption(string name, string val)
{
SmtOptions.Add(new OptionValue(name, val));
}
public void AddWeakSmtOption(string name, string val)
{
if (!SmtOptions.Any(o => o.Option == name))
SmtOptions.Add(new OptionValue(name, val));
}
public void AddSmtOption(string opt)
{
var idx = opt.IndexOf('=');
if (idx <= 0 || idx == opt.Length - 1)
ReportError("Options to be passed to the prover should have the format: O:<name>=<value>, got '" + opt + "'");
AddSmtOption(opt.Substring(0, idx), opt.Substring(idx + 1));
}
protected override bool Parse(string opt)
{
if (opt.StartsWith("O:")) {
AddSmtOption(opt.Substring(2));
return true;
}
if (opt.StartsWith("C:")) {
AddSolverArgument(opt.Substring(2));
return true;
}
return
ParseBool(opt, "MULTI_TRACES", ref MultiTraces) ||
ParseBool(opt, "USE_WEIGHTS", ref UseWeights) ||
ParseBool(opt, "USE_Z3", ref UseZ3) ||
ParseString(opt, "INSPECTOR", ref Inspector) ||
ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
ParseString(opt, "LOGIC", ref Logic) ||
base.Parse(opt);
}
public override void PostParse()
{
base.PostParse();
if (UseZ3)
Z3.SetupOptions(this);
}
public override string Help
{
get
{
return
@"
SMT-specific options:
~~~~~~~~~~~~~~~~~~~~~
USE_WEIGHTS=<bool> Pass :weight annotations on quantified formulas (default: true)
VERBOSITY=<int> 1 - print prover output (default: 0)
O:<name>=<value> Pass (set-option :<name> <value>) to the SMT solver.
C:<string> Pass <string> to the SMT on the command line.
LOGIC=<string> Pass (set-logic <string>) to the prover (default: empty)
Z3-specific options:
~~~~~~~~~~~~~~~~~~~~
MULTI_TRACES=<bool> Report errors with multiple paths leading to the same assertion.
INSPECTOR=<string> Use the specified Z3Inspector binary.
OPTIMIZE_FOR_BV=<bool> Optimize Z3 options for bitvector reasoning, and not quantifier instantiation. Defaults to false.
USE_Z3=<bool> Use z3.exe as the prover, and use Z3 extensions (default: true)
" + base.Help;
}
}
}
}
|
