diff options
| author |  MichalMoskal <unknown> | 2011-02-17 19:00:30 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-17 19:00:30 +0000 |
| commit | 6b85a0f0d4f88b6ad57812175354acf3a2947a0e (patch) | |
| tree | c214ed7a953471eaf2689a6b7517cd0ead5fb9bf /Source/Provers/SMTLib/SMTLibProverOptions.cs | |
| parent | 12027267b93833110c0a1a044e1bc80ebf6e7b29 (diff) | |
Provide /p: as the short form of /proverOpt:.
Add /p:O:<name>=<value> and /p:C:<solver-argument> prover options in SMT.
Add default Z3 options when using Z3.
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibProverOptions.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 115 |
1 files changed, 115 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs new file mode 100644 index 00000000..0565e677 --- /dev/null +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -0,0 +1,115 @@ +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>();
+
+ // 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 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, "USE_WEIGHTS", ref UseWeights) ||
+ ParseBool(opt, "USE_Z3", ref UseZ3) ||
+ ParseString(opt, "INSPECTOR", ref Inspector) ||
+ ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
+ 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.
+
+Z3-specific options:
+~~~~~~~~~~~~~~~~~~~~
+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;
+ }
+ }
+ }
+}
|