diff options
author | Ken McMillan <unknown> | 2014-10-08 13:44:14 -0700 |
---|---|---|
committer | Ken McMillan <unknown> | 2014-10-08 13:44:14 -0700 |
commit | 09152de1a52555aa8a41b245dfddd2be56dd2734 (patch) | |
tree | 5a880b747e3762d5d9685663ff79476ccf280840 /Source/Provers | |
parent | e7ca01b8f249c39cdb7ae7d78908f8dab2addff7 (diff) | |
parent | 1cca1f3efef31b9eee79bb26a5032da2620a8365 (diff) |
Merge FixpointVC changes with mainline
Diffstat (limited to 'Source/Provers')
-rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 1b52d797..845f859f 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -895,7 +895,8 @@ namespace Microsoft.Boogie.SMTLib public override Outcome CheckRPFP(string descriptiveName, RPFP _rpfp, ErrorHandler handler,
out RPFP.Node cex,
- Dictionary<int,Dictionary<string,string>> varSubst)
+ Dictionary<int, Dictionary<string, string>> varSubst,
+ Dictionary<string, int> extra_bound)
{
//Contract.Requires(descriptiveName != null);
//Contract.Requires(vc != null);
@@ -923,9 +924,15 @@ namespace Microsoft.Boogie.SMTLib LineariserOptions.Default.LabelsBelowQuantifiers = true;
List<string> ruleStrings = new List<string>();
+ var recursion_bound = CommandLineOptions.Clo.RecursionBound;
foreach (var edge in rpfp.edges)
{
- string ruleString = "(rule " + QuantifiedVCExpr2String(rpfp.GetRule(edge)) + "\n)";
+ string node_name = (edge.Parent.Name as VCExprBoogieFunctionOp).Func.Name;
+ string rule_name = "rule_" + edge.number.ToString();
+ string rec_bound = "";
+ if(extra_bound != null && extra_bound.ContainsKey(node_name))
+ rec_bound = (recursion_bound + extra_bound[node_name]).ToString();
+ string ruleString = "(rule " + QuantifiedVCExpr2String(rpfp.GetRule(edge)) + " " + rule_name + " " + rec_bound + "\n)";
ruleStrings.Add(ruleString);
}
string queryString = "(query " + QuantifiedVCExpr2String(rpfp.GetQuery()) + "\n :engine duality\n :print-certificate true\n";
|