From 7d9165d6b61e7475b973d3bf86d063dcc4a454d1 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 26 May 2014 14:33:08 -0700 Subject: Conjecture printing for duality and child user time tracking. --- Source/Provers/SMTLib/ProverInterface.cs | 134 +++++++++++++++++++++------ Source/Provers/SMTLib/SExpr.cs | 150 +++++++++++++++++++++++++++++++ Source/Provers/SMTLib/SMTLibProcess.cs | 3 + Source/Provers/SMTLib/Z3.cs | 16 +++- 4 files changed, 271 insertions(+), 32 deletions(-) (limited to 'Source/Provers/SMTLib') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 4e895931..56907a89 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -66,6 +66,12 @@ namespace Microsoft.Boogie.SMTLib ctx.parent = this; this.DeclCollector = new TypeDeclCollector((SMTLibProverOptions)options, Namer); + if (CommandLineOptions.Clo.PrintFixedPoint != null || CommandLineOptions.Clo.PrintConjectures != null) + { + declHandler = new MyDeclHandler(); + DeclCollector.SetDeclHandler(declHandler); + } + SetupProcess(); if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer) @@ -82,6 +88,7 @@ namespace Microsoft.Boogie.SMTLib } PrepareCommon(); } + } private void SetupAxiomBuilder(VCExpressionGenerator gen) @@ -677,27 +684,9 @@ namespace Microsoft.Boogie.SMTLib // get all the predicate definitions for (int i = 0; i < lines.Length; i++) { var line = lines [i]; - if(line.Name != "define-fun"){ - HandleProverError ("Prover error: expected define-fun but got:" + line.Name); - throw new BadExprFromProver (); - } - if(line.ArgCount != 4){ - HandleProverError ("Prover error: define-fun has wrong number of arguments"); - throw new BadExprFromProver (); - } - var pname = StripCruft(line.Arguments[0].Name); - var pvars = line.Arguments[1]; - var pbody = line.Arguments[3]; // range has to be Bool - var binding = new Dictionary(); - var pvs = new List(); - foreach(var b in pvars.Arguments){ - var e = SExprToVar (b); - pvs.Add (e); - binding.Add (b.Name,e); - } - VCExpr bexpr = SExprToVCExpr(pbody,binding); - - var annot = rpfp.CreateRelation(pvs.ToArray(),bexpr); + string pname; + RPFP.Transformer annot; + GetDefun(line, out pname, out annot); if(pmap.ContainsKey(pname)){ var node = pmap[pname]; @@ -710,6 +699,34 @@ namespace Microsoft.Boogie.SMTLib } } + + private void GetDefun(SExpr line, out string pname, out RPFP.Transformer annot) + { + if (line.Name != "define-fun") + { + HandleProverError("Prover error: expected define-fun but got:" + line.Name); + throw new BadExprFromProver(); + } + if (line.ArgCount != 4) + { + HandleProverError("Prover error: define-fun has wrong number of arguments"); + throw new BadExprFromProver(); + } + pname = StripCruft(line.Arguments[0].Name); + var pvars = line.Arguments[1]; + var pbody = line.Arguments[3]; // range has to be Bool + var binding = new Dictionary(); + var pvs = new List(); + foreach (var b in pvars.Arguments) + { + var e = SExprToVar(b); + pvs.Add(e); + binding.Add(StripCruft(b.Name), e); + } + VCExpr bexpr = SExprToVCExpr(pbody, binding); + + annot = rpfp.CreateRelation(pvs.ToArray(), bexpr); + } private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler, Dictionary> varSubst) @@ -887,10 +904,6 @@ namespace Microsoft.Boogie.SMTLib rpfp = _rpfp; cex = null; - if(CommandLineOptions.Clo.PrintFixedPoint != null){ - declHandler = new MyDeclHandler(); - DeclCollector.SetDeclHandler(declHandler); - } if (options.SeparateLogFiles) CloseLogFile(); // shouldn't really happen @@ -900,6 +913,8 @@ namespace Microsoft.Boogie.SMTLib currentLogFile.Write(common.ToString()); } + PrepareCommon(); + Push(); SendThisVC("(fixedpoint-push)"); foreach (var node in rpfp.nodes) @@ -907,8 +922,6 @@ namespace Microsoft.Boogie.SMTLib DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func); } - PrepareCommon(); - LineariserOptions.Default.LabelsBelowQuantifiers = true; List ruleStrings = new List(); foreach (var edge in rpfp.edges) @@ -1047,11 +1060,74 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(fixedpoint-pop)"); Pop(); AxiomsAreSetup = false; - DeclCollector.SetDeclHandler(null); - declHandler = null; // just so we can GC it + + if (CommandLineOptions.Clo.PrintConjectures != null) + { + ReadConjectures(CommandLineOptions.Clo.PrintConjectures); + } + return result; } + class MyFileParser : SExpr.Parser + { + SMTLibProcessTheoremProver parent; + + public MyFileParser(System.IO.StreamReader _sr, SMTLibProcessTheoremProver _parent) + : base(_sr) + { + parent = _parent; + } + public override void ParseError(string msg) + { + parent.HandleProverError("Error in conjecture file from prover: " + msg); + } + } + + void ReadConjectures(string filename) + { + try + { + System.IO.StreamReader sr = new StreamReader(filename + ".tmp"); + SExpr.Parser p = new MyFileParser(sr, this); + var sexps = p.ParseSExprs(false); + Dictionary pmap = GetNodeMap(); + foreach (var e in sexps) + { + string pname; + RPFP.Transformer annot; + GetDefun(e, out pname, out annot); + + if (pmap.ContainsKey(pname)) + { + var c = new RPFP.Conjecture(); + c.node = pmap[pname]; + c.bound = annot; + rpfp.conjectures.Add(c); + } + else if (pname[0] != '@') + { // if not an internal symbol + HandleProverError("Prover error: got unknown predicate:" + pname); + throw new BadExprFromProver(); + } + } + sr.Close(); + } + catch (Exception) + { + HandleProverError("No conjecture file from prover"); + throw new BadExprFromProver(); + } + } + + private Dictionary GetNodeMap() + { + Dictionary pmap = new Dictionary(); + foreach (var node in rpfp.nodes) + pmap.Add((node.Name as VCExprBoogieFunctionOp).Func.Name, node); + return pmap; + } + private static HashSet usedLogNames = new HashSet(); private TextWriter OpenOutputFile(string descriptiveName) diff --git a/Source/Provers/SMTLib/SExpr.cs b/Source/Provers/SMTLib/SExpr.cs index 461e1ee8..ba07ec27 100644 --- a/Source/Provers/SMTLib/SExpr.cs +++ b/Source/Provers/SMTLib/SExpr.cs @@ -106,6 +106,156 @@ namespace Microsoft.Boogie } #endregion + #region parsing + + public abstract class Parser + { + System.IO.StreamReader sr; + int linePos = 0; + string currLine = null; + + public Parser(System.IO.StreamReader _sr) + { + sr = _sr; + } + string Read() + { + return sr.ReadLine(); + } + char SkipWs() + { + while (true) + { + if (currLine == null) + { + currLine = Read(); + if (currLine == null) + return '\0'; + } + + while (linePos < currLine.Length && char.IsWhiteSpace(currLine[linePos])) + linePos++; + + if (linePos < currLine.Length) + return currLine[linePos]; + else + { + currLine = null; + linePos = 0; + } + } + } + + void Shift() + { + linePos++; + } + + string ParseId() + { + var sb = new StringBuilder(); + + var beg = SkipWs(); + + var quoted = beg == '"' || beg == '|'; + if (quoted) + Shift(); + while (true) + { + if (linePos >= currLine.Length) + { + if (quoted) + { + sb.Append("\n"); + currLine = Read(); + linePos = 0; + if (currLine == null) + break; + } + else break; + } + + var c = currLine[linePos++]; + if (quoted && c == beg) + break; + if (!quoted && (char.IsWhiteSpace(c) || c == '(' || c == ')')) + { + linePos--; + break; + } + if (quoted && c == '\\' && linePos < currLine.Length && currLine[linePos] == '"') + { + sb.Append('"'); + linePos++; + continue; + } + sb.Append(c); + } + + return sb.ToString(); + } + + public abstract void ParseError(string msg); + + public IEnumerable ParseSExprs(bool top) + { + while (true) + { + var c = SkipWs(); + if (c == '\0') + break; + + if (c == ')') + { + if (top) + ParseError("stray ')'"); + break; + } + + string id; + + if (c == '(') + { + Shift(); + c = SkipWs(); + if (c == '\0') + { + ParseError("expecting something after '('"); + break; + } + else if (c == '(') + { + id = ""; + } + else + { + id = ParseId(); + } + + var args = ParseSExprs(false).ToArray(); + + c = SkipWs(); + if (c == ')') + { + Shift(); + } + else + { + ParseError("unclosed '(" + id + "'"); + } + yield return new SExpr(id, args); + } + else + { + id = ParseId(); + yield return new SExpr(id); + } + + if (top) break; + } + } + } + #endregion } } diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 2374a157..439557c0 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -175,8 +175,11 @@ namespace Microsoft.Boogie.SMTLib } } + public static System.TimeSpan TotalUserTime = System.TimeSpan.Zero; + public void Close() { + TotalUserTime += prover.UserProcessorTime; try { prover.Kill(); } catch { diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index ed8f0908..c8f49603 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -4,6 +4,7 @@ // //----------------------------------------------------------------------------- + using System; using System.Collections.Generic; using System.Linq; @@ -200,6 +201,7 @@ namespace Microsoft.Boogie.SMTLib // options that work only on the command line static string[] commandLineOnly = { "TRACE", "PROOF_MODE" }; + public static void SetupOptions(SMTLibProverOptions options) { FindExecutable(); @@ -208,8 +210,10 @@ namespace Microsoft.Boogie.SMTLib if (major > 4 || major == 4 && minor >= 3) { + bool fp = false; // CommandLineOptions.Clo.FixedPointEngine != null; + // don't bother with auto-config - it would disable explicit settings for eager threshold and so on - options.AddWeakSmtOption("AUTO_CONFIG", "false"); + if(!fp) options.AddWeakSmtOption("AUTO_CONFIG", "false"); //options.AddWeakSmtOption("MODEL_PARTIAL", "true"); //options.WeakAddSmtOption("MODEL_VALUE_COMPLETION", "false"); @@ -232,7 +236,8 @@ namespace Microsoft.Boogie.SMTLib // The left-to-right structural case-splitting strategy. //options.AddWeakSmtOption("SORT_AND_OR", "false"); // always false now - options.AddWeakSmtOption("smt.CASE_SPLIT", "3"); + + if (!fp) options.AddWeakSmtOption("smt.CASE_SPLIT", "3"); // In addition delay adding unit conflicts. options.AddWeakSmtOption("smt.DELAY_UNITS", "true"); @@ -251,7 +256,7 @@ namespace Microsoft.Boogie.SMTLib // Complex proof attempts in VCC (and likely elsewhere) require matching depth of 20 or more. // the following will make the :weight option more usable - options.AddWeakSmtOption("smt.QI.COST", "|\"(+ weight generation)\"|"); // TODO: this doesn't seem to work + if (!fp) options.AddWeakSmtOption("smt.QI.COST", "|\"(+ weight generation)\"|"); // TODO: this doesn't seem to work //if (options.Inspector != null) // options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100"); @@ -275,6 +280,11 @@ namespace Microsoft.Boogie.SMTLib options.AddWeakSmtOption("smt.array.weak", "true"); options.AddWeakSmtOption("smt.array.extensional", "false"); } + + if (CommandLineOptions.Clo.PrintConjectures != null) + { + options.AddWeakSmtOption("fixedpoint.conjecture_file", CommandLineOptions.Clo.PrintConjectures + ".tmp"); + } } else { -- cgit v1.2.3