From fe14d9b1fd7bd816f91f58e44314b5c0772227cb Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 28 Dec 2012 07:38:50 -0800 Subject: extended Evaluate to handle more types --- Source/Provers/SMTLib/ProverInterface.cs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'Source/Provers') diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index ec91dcbc..ca0e811b 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -816,12 +816,12 @@ namespace Microsoft.Boogie.SMTLib SendThisVC("(set-option :SOFT_TIMEOUT " + ms.ToString() + ")\n"); } - public override int Evaluate(VCExpr expr) + public override object Evaluate(VCExpr expr) { string vcString = VCExpr2String(expr, 1); SendThisVC("(get-value (" + vcString + "))"); var resp = Process.GetProverResponse(); - if (resp == null) throw new VCExprEvaluationException(); + if (resp == null) throw new VCExprEvaluationException(); if (!(resp.Name == "" && resp.ArgCount == 1)) throw new VCExprEvaluationException(); resp = resp.Arguments[0]; if (resp.Name == "") @@ -842,8 +842,12 @@ namespace Microsoft.Boogie.SMTLib } if (resp.ArgCount != 0) throw new VCExprEvaluationException(); - var v = int.Parse(resp.Name); - return v; + if (expr.Type.Equals(Boogie.Type.Bool)) + return bool.Parse(resp.Name); + else if (expr.Type.Equals(Boogie.Type.Int)) + return int.Parse(resp.Name); + else + return resp.Name; } /// -- cgit v1.2.3