summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/ProverInterface.cs
diff options
context:
space:
mode:
authorGravatar Ken McMillan <unknown>2014-12-08 17:02:02 -0800
committerGravatar Ken McMillan <unknown>2014-12-08 17:02:02 -0800
commit07d28c62b758bc16fa4d1c4eae5659514097d8d5 (patch)
tree9cb85da5a02fec0a8dfbef0d5e60297ba12f99f7 /Source/Provers/SMTLib/ProverInterface.cs
parent575d226a8e15efc111bfaf57f188261e12f7ef95 (diff)
parent09152de1a52555aa8a41b245dfddd2be56dd2734 (diff)
Merge some FixpointVC changes that got left behind
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs11
1 files changed, 9 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index d838360d..c433e84c 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -900,7 +900,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);
@@ -928,9 +929,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";