diff options
author | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
---|---|---|
committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-06-28 01:44:30 +0100 |
commit | 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d (patch) | |
tree | 27d5f9b0d130c6c1a6758bc0b7456b0aa51e34e0 /Source/Provers/SMTLib/SMTLibProverOptions.cs | |
parent | e11d65009d0b4ba1327f5f5dd6b26367330611f0 (diff) |
Normalise line endings using a .gitattributes file. Unfortunately
this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibProverOptions.cs')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibProverOptions.cs | 316 |
1 files changed, 158 insertions, 158 deletions
diff --git a/Source/Provers/SMTLib/SMTLibProverOptions.cs b/Source/Provers/SMTLib/SMTLibProverOptions.cs index 0cfa65d8..5c3bed3e 100644 --- a/Source/Provers/SMTLib/SMTLibProverOptions.cs +++ b/Source/Provers/SMTLib/SMTLibProverOptions.cs @@ -1,158 +1,158 @@ -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 enum SolverKind { Z3, CVC4 };
-
- public class SMTLibProverOptions : ProverOptions
- {
- public bool UseWeights = true;
- public bool SupportsLabels { get { return Solver == SolverKind.Z3; } }
- public bool UseTickleBool { get { return Solver == SolverKind.Z3; } }
- public SolverKind Solver = SolverKind.Z3;
- 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 string Inspector = null;
- public bool OptimizeForBv = false;
- public bool SMTLib2Model = false;
-
- public bool ProduceModel() {
- return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini || CommandLineOptions.Clo.UseProverEvaluate ||
- ExpectingModel();
- }
-
- public bool ExpectingModel()
- {
- return CommandLineOptions.Clo.PrintErrorModel >= 1 ||
- CommandLineOptions.Clo.EnhancedErrorMessages == 1 ||
- CommandLineOptions.Clo.ModelViewFile != null ||
- (CommandLineOptions.Clo.StratifiedInlining > 0 && !CommandLineOptions.Clo.StratifiedInliningWithoutModels);
- }
-
- 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)
- {
- string SolverStr = null;
- if (ParseString(opt, "SOLVER", ref SolverStr)) {
- switch (SolverStr) {
- case "Z3":
- case "z3":
- Solver = SolverKind.Z3;
- break;
- case "CVC4":
- case "cvc4":
- Solver = SolverKind.CVC4;
- if (Logic.Equals("")) Logic = "ALL_SUPPORTED";
- break;
- default:
- ReportError("Invalid SOLVER value; must be 'Z3' or 'CVC4'");
- return false;
- }
- return true;
- }
-
- 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) ||
- ParseString(opt, "INSPECTOR", ref Inspector) ||
- ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) ||
- ParseBool(opt, "SMTLIB2_MODEL", ref SMTLib2Model) ||
- ParseString(opt, "LOGIC", ref Logic) ||
- base.Parse(opt);
- }
-
- public override void PostParse()
- {
- base.PostParse();
- if (Solver == SolverKind.Z3)
- Z3.SetupOptions(this);
- }
-
- public override string Help
- {
- get
- {
- return
-@"
-SMT-specific options:
-~~~~~~~~~~~~~~~~~~~~~
-SOLVER=<string> Use the given SMT solver (z3 or cvc4; default: z3)
-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, 'ALL_SUPPORTED' for CVC4)
-
-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.
-SMTLIB2_MODEL=<bool> Use the SMTLIB2 output model. Defaults to false.
-" + base.Help;
- }
- }
- }
-}
+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 enum SolverKind { Z3, CVC4 }; + + public class SMTLibProverOptions : ProverOptions + { + public bool UseWeights = true; + public bool SupportsLabels { get { return Solver == SolverKind.Z3; } } + public bool UseTickleBool { get { return Solver == SolverKind.Z3; } } + public SolverKind Solver = SolverKind.Z3; + 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 string Inspector = null; + public bool OptimizeForBv = false; + public bool SMTLib2Model = false; + + public bool ProduceModel() { + return !CommandLineOptions.Clo.UseLabels || CommandLineOptions.Clo.ExplainHoudini || CommandLineOptions.Clo.UseProverEvaluate || + ExpectingModel(); + } + + public bool ExpectingModel() + { + return CommandLineOptions.Clo.PrintErrorModel >= 1 || + CommandLineOptions.Clo.EnhancedErrorMessages == 1 || + CommandLineOptions.Clo.ModelViewFile != null || + (CommandLineOptions.Clo.StratifiedInlining > 0 && !CommandLineOptions.Clo.StratifiedInliningWithoutModels); + } + + 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) + { + string SolverStr = null; + if (ParseString(opt, "SOLVER", ref SolverStr)) { + switch (SolverStr) { + case "Z3": + case "z3": + Solver = SolverKind.Z3; + break; + case "CVC4": + case "cvc4": + Solver = SolverKind.CVC4; + if (Logic.Equals("")) Logic = "ALL_SUPPORTED"; + break; + default: + ReportError("Invalid SOLVER value; must be 'Z3' or 'CVC4'"); + return false; + } + return true; + } + + 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) || + ParseString(opt, "INSPECTOR", ref Inspector) || + ParseBool(opt, "OPTIMIZE_FOR_BV", ref OptimizeForBv) || + ParseBool(opt, "SMTLIB2_MODEL", ref SMTLib2Model) || + ParseString(opt, "LOGIC", ref Logic) || + base.Parse(opt); + } + + public override void PostParse() + { + base.PostParse(); + if (Solver == SolverKind.Z3) + Z3.SetupOptions(this); + } + + public override string Help + { + get + { + return +@" +SMT-specific options: +~~~~~~~~~~~~~~~~~~~~~ +SOLVER=<string> Use the given SMT solver (z3 or cvc4; default: z3) +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, 'ALL_SUPPORTED' for CVC4) + +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. +SMTLIB2_MODEL=<bool> Use the SMTLIB2 output model. Defaults to false. +" + base.Help; + } + } + } +} |