diff options
author | 2011-02-11 19:38:00 +0000 | |
---|---|---|
committer | 2011-02-11 19:38:00 +0000 | |
commit | 4760c55b4a09e4b11039e9537371a98f657d7704 (patch) | |
tree | 088536468e33d19829d25a86c56f57b460c1d402 /Source/Provers | |
parent | afb3de0ebf0539a89f2073a74f76bd811bee06c0 (diff) |
Add USE_PREDICATES option to TPTP and SMT provers
Diffstat (limited to 'Source/Provers')
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 16 | ||||
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 17 | ||||
-rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 22 | ||||
-rw-r--r-- | Source/Provers/TPTP/ProverInterface.cs | 16 | ||||
-rw-r--r-- | Source/Provers/TPTP/TPTPLineariser.cs | 15 |
5 files changed, 61 insertions, 25 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index f1c4efcd..fff7e1b3 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -20,14 +20,16 @@ using Microsoft.Boogie.Simplify; namespace Microsoft.Boogie.SMTLib
{
- class SMTLibProverOptions : ProverOptions
+ public class SMTLibProverOptions : ProverOptions
{
public string Output = "boogie-vc-@PROC@.smt";
+ public bool UsePredicates = false;
protected override bool Parse(string opt)
{
return
ParseString(opt, "OUTPUT", ref Output) ||
+ ParseBool(opt, "USE_PREDICATES", ref UsePredicates) ||
base.Parse(opt);
}
@@ -40,6 +42,7 @@ namespace Microsoft.Boogie.SMTLib SMT-specific options:
~~~~~~~~~~~~~~~~~~~~~
OUTPUT=<string> Store VC in named file. Defaults to boogie-vc-@PROC@.smt.
+USE_PREDICATES=<bool> Try to use SMT predicates for functions returning bool.
" + base.Help;
// DIST requires non-public binaries
@@ -96,7 +99,7 @@ void ObjectInvariant() UniqueNamer namer = new UniqueNamer ();
Namer = namer;
Namer.Spacer = "__";
- this.DeclCollector = new TypeDeclCollector (namer);
+ this.DeclCollector = new TypeDeclCollector ((SMTLibProverOptions)options, namer);
}
@@ -195,6 +198,11 @@ void ObjectInvariant() return Outcome.Undetermined;
}
+ protected SMTLibProverOptions Options
+ {
+ get { return (SMTLibProverOptions)this.options; }
+ }
+
protected string VCExpr2String(VCExpr expr, int polarity) {
Contract.Requires(expr != null);
Contract.Ensures(Contract.Result<string>() != null);
@@ -230,8 +238,8 @@ void ObjectInvariant() DeclCollector.Collect(sortedExpr);
FeedTypeDeclsToProver();
- AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer));
- string res = SMTLibExprLineariser.ToString(sortedExpr, Namer);
+ AddAxiom(SMTLibExprLineariser.ToString(sortedAxioms, Namer, Options));
+ string res = SMTLibExprLineariser.ToString(sortedExpr, Namer, Options);
Contract.Assert(res!=null);
if (CommandLineOptions.Clo.Trace) {
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 677ff296..7b5e51b0 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -54,13 +54,13 @@ void ObjectInvariant() // Lineariser for expressions. The result (bool) is currently not used for anything
public class SMTLibExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> {
- public static string ToString(VCExpr e, UniqueNamer namer) {
+ public static string ToString(VCExpr e, UniqueNamer namer, SMTLibProverOptions opts) {
Contract.Requires(e != null);
Contract.Requires(namer != null);
Contract.Ensures(Contract.Result<string>() != null);
StringWriter sw = new StringWriter();
- SMTLibExprLineariser lin = new SMTLibExprLineariser (sw, namer);
+ SMTLibExprLineariser lin = new SMTLibExprLineariser (sw, namer, opts);
Contract.Assert(lin!=null);
lin.Linearise(e, LineariserOptions.Default);
return cce.NonNull(sw.ToString());
@@ -86,11 +86,13 @@ void ObjectInvariant() } }
internal readonly UniqueNamer Namer;
+ internal readonly SMTLibProverOptions ProverOptions;
- public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer) {
+ public SMTLibExprLineariser(TextWriter wr, UniqueNamer namer, SMTLibProverOptions opts) {
Contract.Requires(wr != null);Contract.Requires(namer != null);
this.wr = wr;
this.Namer = namer;
+ this.ProverOptions = opts;
}
public void Linearise(VCExpr expr, LineariserOptions options) {
@@ -847,8 +849,13 @@ void ObjectInvariant() string printedName = ExprLineariser.Namer.GetName(op.Func, MakeIdPrintable(op.Func.Name));
Contract.Assert(printedName!=null);
- // arguments are always terms
- WriteApplicationTermOnly(printedName, node, options);
+ if (ExprLineariser.ProverOptions.UsePredicates && op.Func.OutParams[0].TypedIdent.Type.IsBool) {
+ WriteApplication(printedName, node, options, true);
+ } else {
+ // arguments are always terms
+ WriteApplicationTermOnly(printedName, node, options);
+ }
+
return true;
}
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index a60b01ee..f617e899 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -18,6 +18,8 @@ namespace Microsoft.Boogie.SMTLib public class TypeDeclCollector : BoundVarTraversingVCExprVisitor<bool, bool> {
private readonly UniqueNamer Namer;
+ private readonly SMTLibProverOptions Options;
+
[ContractInvariantMethod]
void ObjectInvariant()
{
@@ -29,9 +31,10 @@ void ObjectInvariant() }
- public TypeDeclCollector(UniqueNamer namer) {
+ public TypeDeclCollector(SMTLibProverOptions opts, UniqueNamer namer) {
Contract.Requires(namer != null);
this.Namer = namer;
+ this.Options = opts;
}
// not used
@@ -102,19 +105,24 @@ void ObjectInvariant() Contract.Assert(f != null);
string printedName = Namer.GetName(f, SMTLibExprLineariser.MakeIdPrintable(f.Name));
Contract.Assert(printedName != null);
- string decl = ":extrafuns ((" + printedName;
+
+ bool isPred = Options.UsePredicates && f.OutParams[0].TypedIdent.Type.IsBool;
+ string decl = (isPred ? ":extrapreds" : ":extrafuns") + " ((" + printedName;
foreach (Variable v in f.InParams) {
Contract.Assert(v != null);
RegisterType(v.TypedIdent.Type);
decl += " " + TypeToString(v.TypedIdent.Type);
}
+
+
Contract.Assert(f.OutParams.Length == 1);
- foreach (Variable v in f.OutParams) {
- Contract.Assert(v != null);
- RegisterType(v.TypedIdent.Type);
- decl += " " + TypeToString(v.TypedIdent.Type);
- }
+ if (!isPred)
+ foreach (Variable v in f.OutParams) {
+ Contract.Assert(v != null);
+ RegisterType(v.TypedIdent.Type);
+ decl += " " + TypeToString(v.TypedIdent.Type);
+ }
decl += "))";
diff --git a/Source/Provers/TPTP/ProverInterface.cs b/Source/Provers/TPTP/ProverInterface.cs index 4b710495..ba4e406b 100644 --- a/Source/Provers/TPTP/ProverInterface.cs +++ b/Source/Provers/TPTP/ProverInterface.cs @@ -20,14 +20,16 @@ using Microsoft.Boogie.Simplify; namespace Microsoft.Boogie.TPTP
{
- class TPTPProverOptions : ProverOptions
+ public class TPTPProverOptions : ProverOptions
{
public string Output = "boogie-vc-@PROC@.tptp";
+ public bool UsePredicates = false;
protected override bool Parse(string opt)
{
return
ParseString(opt, "OUTPUT", ref Output) ||
+ ParseBool(opt, "USE_PREDICATES", ref UsePredicates) ||
base.Parse(opt);
}
@@ -40,6 +42,7 @@ namespace Microsoft.Boogie.TPTP TPTP-specific options:
~~~~~~~~~~~~~~~~~~~~~~
OUTPUT=<string> Store VC in named file. Defaults to boogie-vc-@PROC@.tptp.
+USE_PREDICATES=<bool> Try to use SMT predicates for functions returning bool.
" + base.Help;
// DIST requires non-public binaries
@@ -166,12 +169,17 @@ OUTPUT=<string> Store VC in named file. Defaults to boogie-vc-@PROC@.t output.Close();
}
+ public TPTPProverOptions Options
+ {
+ get { return (TPTPProverOptions)this.options; }
+ }
+
private TextWriter OpenOutputFile(string descriptiveName)
{
Contract.Requires(descriptiveName != null);
Contract.Ensures(Contract.Result<TextWriter>() != null);
- string filename = ((TPTPProverOptions)options).Output;
+ string filename = Options.Output;
filename = Helpers.SubstituteAtPROC(descriptiveName, cce.NonNull(filename));
return new StreamWriter(filename, false);
}
@@ -228,8 +236,8 @@ OUTPUT=<string> Store VC in named file. Defaults to boogie-vc-@PROC@.t DeclCollector.Collect(exprWithoutLet);
FeedTypeDeclsToProver();
- AddAxiom(TPTPExprLineariser.ToString(axiomsWithoutLet, Namer));
- string res = TPTPExprLineariser.ToString(exprWithoutLet, Namer);
+ AddAxiom(TPTPExprLineariser.ToString(axiomsWithoutLet, Namer, Options));
+ string res = TPTPExprLineariser.ToString(exprWithoutLet, Namer, Options);
Contract.Assert(res != null);
if (CommandLineOptions.Clo.Trace) {
diff --git a/Source/Provers/TPTP/TPTPLineariser.cs b/Source/Provers/TPTP/TPTPLineariser.cs index 78b87590..a35d43f0 100644 --- a/Source/Provers/TPTP/TPTPLineariser.cs +++ b/Source/Provers/TPTP/TPTPLineariser.cs @@ -53,13 +53,13 @@ void ObjectInvariant() // Lineariser for expressions. The result (bool) is currently not used for anything
public class TPTPExprLineariser : IVCExprVisitor<bool, LineariserOptions/*!*/> {
- public static string ToString(VCExpr e, UniqueNamer namer) {
+ public static string ToString(VCExpr e, UniqueNamer namer, TPTPProverOptions opts) {
Contract.Requires(e != null);
Contract.Requires(namer != null);
Contract.Ensures(Contract.Result<string>() != null);
StringWriter sw = new StringWriter();
- TPTPExprLineariser lin = new TPTPExprLineariser (sw, namer);
+ TPTPExprLineariser lin = new TPTPExprLineariser (sw, namer, opts);
Contract.Assert(lin!=null);
lin.Linearise(e, LineariserOptions.Default);
return cce.NonNull(sw.ToString());
@@ -85,11 +85,13 @@ void ObjectInvariant() } }
internal readonly UniqueNamer Namer;
+ internal readonly TPTPProverOptions Options;
- public TPTPExprLineariser(TextWriter wr, UniqueNamer namer) {
+ public TPTPExprLineariser(TextWriter wr, UniqueNamer namer, TPTPProverOptions opts) {
Contract.Requires(wr != null);Contract.Requires(namer != null);
this.wr = wr;
this.Namer = namer;
+ this.Options = opts;
}
public void Linearise(VCExpr expr, LineariserOptions options) {
@@ -724,8 +726,11 @@ void ObjectInvariant() string printedName = ExprLineariser.Namer.GetName(op.Func, Lowercase(op.Func.Name));
Contract.Assert(printedName!=null);
- // arguments are always terms
- WriteApplicationTermOnly(printedName, node, options);
+ if (ExprLineariser.Options.UsePredicates && op.Func.OutParams[0].TypedIdent.Type.IsBool)
+ WriteApplication(printedName, node, options, true);
+ else
+ // arguments are always terms
+ WriteApplicationTermOnly(printedName, node, options);
return true;
}
|