Refactored the define attribute on functions

Source/Core/Absy.cs

@@ -2671,8 +2671,10 @@ public override void Emit(TokenTextWriter stream, int level) { }
  public class Function : DeclWithFormals {
  public string Comment;
 
- // the body is only set if the function is declared with {:inline}
+ // Body is only set if the function is declared with {:inline}
  public Expr Body;
+ // DefBody is only set if the function is declared with {:define}
+ public NAryExpr DefBody;
  public Axiom DefinitionAxiom;
 
  public IList<Axiom> otherDefinitionAxioms;
@@ -2774,6 +2776,13 @@ public override void Emit(TokenTextWriter stream, int level) {
  Body.Emit(stream);
  stream.WriteLine();
  stream.WriteLine("}");
+ } else if (DefBody != null) {
+ stream.WriteLine();
+ stream.WriteLine("{");
+ stream.Write(level + 1, "");
+ DefBody.Args[1].Emit(stream);
+ stream.WriteLine();
+ stream.WriteLine("}");
  } else {
  stream.WriteLine(";");
  }
@@ -2791,11 +2800,14 @@ public override void Resolve(ResolutionContext rc) {
  RegisterFormals(InParams, rc);
  RegisterFormals(OutParams, rc);
  ResolveAttributes(rc);
- if (Body != null)
- {
+ if (Body != null) {
  rc.StateMode = ResolutionContext.State.StateLess;
  Body.Resolve(rc);
  rc.StateMode = ResolutionContext.State.Single;
+ } else if (DefBody != null) {
+ rc.StateMode = ResolutionContext.State.StateLess;
+ DefBody.Resolve(rc);
+ rc.StateMode = ResolutionContext.State.Single;
  }
  rc.PopVarContext();
  Type.CheckBoundVariableOccurrences(TypeParameters,
@@ -2819,6 +2831,15 @@ public override void Typecheck(TypecheckingContext tc) {
  tc.Error(Body,
  "function body with invalid type: {0} (expected: {1})",
  Body.Type, cce.NonNull(OutParams[0]).TypedIdent.Type);
+ } else if (DefBody != null) {
+ DefBody.Typecheck(tc);
+
+ // We are matching the type of the function body with output param, and not the type
+ // of DefBody, which is always going to be bool (since it is of the form func_call == func_body)
+ if (!cce.NonNull(DefBody.Args[1].Type).Unify(cce.NonNull(OutParams[0]).TypedIdent.Type))
+ tc.Error(DefBody.Args[1],
+ "function body with invalid type: {0} (expected: {1})",
+ DefBody.Args[1].Type, cce.NonNull(OutParams[0]).TypedIdent.Type);
  }
  }
 
@@ -2871,6 +2892,33 @@ public Axiom CreateDefinitionAxiom(Expr definition, QKeyValue kv = null) {
  DefinitionAxiom = new Axiom(tok, def);
  return DefinitionAxiom;
  }
+
+ // Generates function definition of the form func_call == func_body
+ // For example, for
+ // function {:define} foo(x:int) returns(int) { x + 1 }
+ // this will generate
+ // foo(x):int == x + 1
+ // We need the left hand call part later on to be able to generate
+ // the appropriate SMTlib style function definition.
+ public NAryExpr CreateFunctionDefinition(Expr body) {
+ Contract.Requires(body != null);
+
+ List<Expr> callArgs = new List<Expr>();
+ int i = 0;
+ foreach (Formal/*!*/ f in InParams) {
+ Contract.Assert(f != null);
+ string nm = f.TypedIdent.HasName ? f.TypedIdent.Name : "_" + i;
+ callArgs.Add(new IdentifierExpr(f.tok, nm));
+ i++;
+ }
+
+ Expr call = new NAryExpr(tok, new FunctionCall(new IdentifierExpr(tok, Name)), callArgs);
+ // specify the type of the function, because it might be that
+ // type parameters only occur in the output type
+ call = Expr.CoerceType(tok, call, (Type)OutParams[0].TypedIdent.Type.Clone());
+ NAryExpr def = Expr.Binary(tok, BinaryOperator.Opcode.Eq, call, body);
+ return def;
+ }
  }
 
  public class Macro : Function {

Source/Core/AbsyQuant.cs

@@ -593,29 +593,29 @@ public override int GetHashCode() {
 
  public class ForallExpr : QuantifierExpr {
  public ForallExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams,
- List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false)
+ List<Variable>/*!*/ dummies, QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable = false)
  : base(tok, typeParams, dummies, kv, triggers, body, immutable) {
  Contract.Requires(tok != null);
  Contract.Requires(typeParams != null);
  Contract.Requires(dummies != null);
  Contract.Requires(body != null);
  Contract.Requires(dummies.Count + typeParams.Count > 0);
  }
- public ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable=false)
+ public ForallExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable = false)
  : base(tok, new List<TypeVariable>(), dummies, null, triggers, body, immutable) {
  Contract.Requires(body != null);
  Contract.Requires(dummies != null);
  Contract.Requires(tok != null);
  Contract.Requires(dummies.Count > 0);
  }
- public ForallExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable=false)
+ public ForallExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable = false)
  : base(tok, new List<TypeVariable>(), dummies, null, null, body, immutable) {
  Contract.Requires(body != null);
  Contract.Requires(dummies != null);
  Contract.Requires(tok != null);
  Contract.Requires(dummies.Count > 0);
  }
- public ForallExpr(IToken tok, List<TypeVariable> typeParams, List<Variable> dummies, Expr body, bool immutable=false)
+ public ForallExpr(IToken tok, List<TypeVariable> typeParams, List<Variable> dummies, Expr body, bool immutable = false)
  : base(tok, typeParams, dummies, null, null, body, immutable) {
  Contract.Requires(body != null);
  Contract.Requires(dummies != null);
@@ -639,22 +639,22 @@ public override BinderKind Kind {
 
  public class ExistsExpr : QuantifierExpr {
  public ExistsExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParams, List<Variable>/*!*/ dummies,
- QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable=false)
+ QKeyValue kv, Trigger triggers, Expr/*!*/ body, bool immutable = false)
  : base(tok, typeParams, dummies, kv, triggers, body, immutable) {
  Contract.Requires(tok != null);
  Contract.Requires(typeParams != null);
  Contract.Requires(dummies != null);
  Contract.Requires(body != null);
  Contract.Requires(dummies.Count + typeParams.Count > 0);
  }
- public ExistsExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable=false)
+ public ExistsExpr(IToken tok, List<Variable> dummies, Trigger triggers, Expr body, bool immutable = false)
  : base(tok, new List<TypeVariable>(), dummies, null, triggers, body, immutable) {
  Contract.Requires(body != null);
  Contract.Requires(dummies != null);
  Contract.Requires(tok != null);
  Contract.Requires(dummies.Count > 0);
  }
- public ExistsExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable=false)
+ public ExistsExpr(IToken tok, List<Variable> dummies, Expr body, bool immutable = false)
  : base(tok, new List<TypeVariable>(), dummies, null, null, body, immutable) {
  Contract.Requires(body != null);
  Contract.Requires(dummies != null);
@@ -898,7 +898,7 @@ public override int GetHashCode() {
 
  public class LambdaExpr : BinderExpr {
  public LambdaExpr(IToken/*!*/ tok, List<TypeVariable>/*!*/ typeParameters,
- List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable=false)
+ List<Variable>/*!*/ dummies, QKeyValue kv, Expr/*!*/ body, bool immutable = false)
  : base(tok, typeParameters, dummies, kv, body, immutable) {
  Contract.Requires(tok != null);
  Contract.Requires(typeParameters != null);

Source/Core/BoogiePL.atg

@@ -521,6 +521,8 @@ Function<.out List<Declaration>/*!*/ ds.>
  // generate either an axiom or a function body
  if (QKeyValue.FindBoolAttribute(kv, "inline")) {
  func.Body = definition;
+ } else if (QKeyValue.FindBoolAttribute(kv, "define")) {
+ func.DefBody = func.CreateFunctionDefinition(definition);
  } else {
  ds.Add(func.CreateDefinitionAxiom(definition, kv));
  }

Source/Core/CommandLineOptions.cs

@@ -1621,6 +1621,11 @@ result caching (default: ""<impl. name>:0"").
  {:bvbuiltin ""spec""}
  Rewrite the function to built-in prover function symbol 'fn'.
 
+ {:define}
+ Turn this function into a definition (using the define-fun construct)
+ when using the SMT-LIB backend. Can only be used with non-recursive
+ functions.
+
  {:inline}
  {:inline true}
  Expand function according to its definition before going to the prover.

Source/Core/Parser.cs

@@ -428,6 +428,8 @@ void Function(out List<Declaration>/*!*/ ds) {
  // generate either an axiom or a function body
  if (QKeyValue.FindBoolAttribute(kv, "inline")) {
  func.Body = definition;
+ } else if (QKeyValue.FindBoolAttribute(kv, "define")) {
+ func.DefBody = func.CreateFunctionDefinition(definition);
  } else {
  ds.Add(func.CreateDefinitionAxiom(definition, kv));
  }
@@ -2430,4 +2432,4 @@ public FatalError(string m): base(m) {}
 }
 
 
-}
+}

Source/Core/StandardVisitor.cs

@@ -327,6 +327,8 @@ public virtual Function VisitFunction(Function node) {
  node = (Function)this.VisitDeclWithFormals(node);
  if (node.Body != null)
  node.Body = this.VisitExpr(node.Body);
+ if (node.DefBody != null)
+ node.DefBody = (NAryExpr)this.VisitExpr(node.DefBody);
  return node;
  }
  public virtual GlobalVariable VisitGlobalVariable(GlobalVariable node) {
@@ -894,6 +896,8 @@ public override Function VisitFunction(Function node)
  node = (Function)this.VisitDeclWithFormals(node);
  if (node.Body != null)
  this.VisitExpr(node.Body);
+ if (node.DefBody != null)
+ this.VisitExpr(node.DefBody);
  return node;
  }
  public override GlobalVariable VisitGlobalVariable(GlobalVariable node)