From 4760c55b4a09e4b11039e9537371a98f657d7704 Mon Sep 17 00:00:00 2001 From: MichalMoskal Date: Fri, 11 Feb 2011 19:38:00 +0000 Subject: Add USE_PREDICATES option to TPTP and SMT provers --- Source/Provers/SMTLib/ProverInterface.cs | 16 ++++++++++++---- Source/Provers/SMTLib/SMTLibLineariser.cs | 17 ++++++++++++----- Source/Provers/SMTLib/TypeDeclCollector.cs | 22 +++++++++++++++------- 3 files changed, 39 insertions(+), 16 deletions(-) (limited to 'Source/Provers/SMTLib') 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= Store VC in named file. Defaults to boogie-vc-@PROC@.smt. +USE_PREDICATES= 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() != 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 { - 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() != 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 { 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 += "))"; -- cgit v1.2.3