diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-06-04 11:16:44 -0700 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-06-04 11:16:44 -0700 |
| commit | f285ae58005b268014902059b2f9becc2d17ac59 (patch) | |
| tree | 1c6b889fdaf2649a325564bbaccfd25031663164 /Source/Provers/SMTLib | |
| parent | 2bb78e1a89bd0c8cda370cfc5d6f2060aa768733 (diff) | |
moved class Macro to Absy
cleanup up DefineMacro
Changed SI to use macros for reach info
Diffstat (limited to 'Source/Provers/SMTLib')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 65c4e130..31afbdfa 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -770,12 +770,13 @@ namespace Microsoft.Boogie.SMTLib SendThisVC(a);
}
- public override void DefineMacro(Function fun, VCExpr vc) {
- DeclCollector.AddFunction(fun);
- string name = Namer.GetName(fun, fun.Name);
- string a = "(define-fun " + name + "() Bool " + VCExpr2String(vc, 1) + ")";
+ public override void DefineMacro(Macro f, VCExpr vc) {
+ DeclCollector.AddFunction(f);
+ string printedName = Namer.GetQuotedName(f, f.Name);
+ var argTypes = f.InParams.Cast<Variable>().MapConcat(p => DeclCollector.TypeToStringReg(p.TypedIdent.Type), " ");
+ string decl = "(define-fun " + printedName + " (" + argTypes + ") " + DeclCollector.TypeToStringReg(f.OutParams[0].TypedIdent.Type) + " " + VCExpr2String(vc, 1) + ")";
AssertAxioms();
- SendThisVC(a);
+ SendThisVC(decl);
}
public override void AssertAxioms()
|