Uses of Class
edu.mit.csail.sdg.alloy4compiler.ast.Expr

Packages that use Expr
edu.mit.csail.sdg.alloy4compiler.ast This package contains the definition of AST nodes. 
edu.mit.csail.sdg.alloy4compiler.parser This package contains the compiler 
edu.mit.csail.sdg.alloy4compiler.sim This package contains a pure-Java evaluator/simulator for Alloy4 instances. 
edu.mit.csail.sdg.alloy4compiler.translator This package contains the translator from Alloy4 to CNF (using kodkod). 
 

Uses of Expr in edu.mit.csail.sdg.alloy4compiler.ast
 

Subclasses of Expr in edu.mit.csail.sdg.alloy4compiler.ast
 class ExprBad
          Immutable; represents an illegal node.
 class ExprBadCall
          Immutable; represents an illegal pred/fun call.
 class ExprBadJoin
          Immutable; represents an illegal relation join.
 class ExprBinary
          Immutable; represents an expression of the form (x OP y).
 class ExprCall
          Immutable; represents a call.
 class ExprChoice
          Immutable; represents an unresolved node that has several possibilities.
 class ExprConstant
          Immutable; represents a constant in the AST.
 class ExprCustom
          Immutable; represents a custom node.
 class ExprHasName
          Immutable; represents a named entity (such as a Field, or a LET or QUANTIFICATION variable, or a function/predicate parameter).
 class ExprITE
          Immutable; represents an if-then-else expression.
 class ExprLet
          Immutable; represents an expression of the form (let a=b | x).
 class ExprList
          Immutable; represents disjoint[] or pred/totalOrder[] or (...
 class ExprQt
          Immutable; represents a quantified expression.
 class ExprUnary
          Immutable; represents a unary expression of the form "(OP subexpression)"
 class ExprVar
          Immutable; represents a LET or QUANTIFICATION variable in the AST.
 class Sig
          Mutable; represents a signature.
static class Sig.Field
          Mutable; represents a field.
static class Sig.PrimSig
          Mutable; reresents a non-subset signature.
static class Sig.SubsetSig
          Mutable; reresents a subset signature.
 

Fields in edu.mit.csail.sdg.alloy4compiler.ast declared as Expr
 Expr ExprITE.cond
          The condition formula.
static Expr ExprConstant.EMPTYNESS
          The "emptyness" constant.
 Expr Decl.expr
          The value that the list of names are bound to.
 Expr ExprLet.expr
          The expression bound to the LET variable.
static Expr ExprConstant.FALSE
          The "FALSE" boolean value.
 Expr Command.formula
          The formula associated with this command.
static Expr ExprConstant.IDEN
          The "iden" relation.
 Expr ExprBadJoin.left
          The left-hand-side expression.
 Expr ExprITE.left
          The then-clause.
 Expr ExprBinary.left
          The left-hand-side expression.
static Expr ExprConstant.MAX
          The largest integer value allowed by the current bitwidth.
static Expr ExprConstant.MIN
          The smallest integer value allowed by the current bitwidth.
static Expr ExprConstant.NEXT
          The "next" relation relating each integer to its next larger integer.
static Expr ExprConstant.ONE
          The "1" integer.
 Expr Func.returnDecl
          The declared return type; never null.
 Expr ExprBadJoin.right
          The right-hand-side expression.
 Expr ExprITE.right
          The else-clause.
 Expr ExprBinary.right
          The right-hand-side expression.
 Expr ExprQt.sub
          The body of the quantified expression.
 Expr ExprUnary.sub
          The subexpression.
 Expr ExprLet.sub
          The body of the LET expression.
static Expr ExprConstant.TRUE
          The "TRUE" boolean value.
static Expr ExprConstant.ZERO
          The "0" integer.
 

Fields in edu.mit.csail.sdg.alloy4compiler.ast with type parameters of type Expr
 ConstList<Expr> ExprBadCall.args
          The unmodifiable list of arguments.
 ConstList<Expr> ExprList.args
          The unmodifiable list of arguments.
 ConstList<Expr> ExprCall.args
          The list of arguments to the call.
 ConstList<Expr> ExprChoice.choices
          The unmodifiable list of Expr(s) from that this ExprChoice can refer to.
 

Methods in edu.mit.csail.sdg.alloy4compiler.ast that return Expr
 Expr Expr.and(Expr x)
          Returns the formula (this and x)
 Expr Expr.any_arrow_lone(Expr x)
          Returns the multiplicity constraint (this set->lone x)
 Expr Expr.any_arrow_one(Expr x)
          Returns the multiplicity constraint (this set->one x)
 Expr Expr.any_arrow_some(Expr x)
          Returns the multiplicity constraint (this set->some x)
 Expr Func.call(Expr... args)
          Convenience method that calls this function with the given list of arguments.
 Expr Expr.cardinality()
          Returns the integer expression (#this) truncated to the current integer bitwidth.
 Expr Expr.cast2int()
          Returns the integer expression "int[this]"
 Expr Expr.cast2sigint()
          Returns the singleton set "Int[this]"
 Expr Expr.closure()
          Returns the expression (^this)
 Expr Expr.comprehensionOver(Decl firstDecl, Decl... moreDecls)
          Returns the comprehension expression {...|this}
 Expr Expr.deNOP()
          Remove the "NOP" in front of an expression (if any).
 Expr ExprQt.desugar()
          This method desugars away the "disjoint" keyword by prefixing the subexpression with the appropriate disjointness guard condition.
 Expr Expr.div(Expr x)
          Returns the formula "this.div[x]" (the quotient of dividing this by x)
 Expr Expr.domain(Expr x)
          Returns the expression (this <: x)
 Expr Expr.equal(Expr x)
          Returns the formula (this==x)
 Expr Expr.forAll(Decl firstDecl, Decl... moreDecls)
          Returns the formula (all...| this)
 Expr Expr.forLone(Decl firstDecl, Decl... moreDecls)
          Returns the formula (lone...| this)
 Expr Expr.forNo(Decl firstDecl, Decl... moreDecls)
          Returns the formula (no...| this)
 Expr Expr.forOne(Decl firstDecl, Decl... moreDecls)
          Returns the formula (one ...| this)
 Expr Expr.forSome(Decl firstDecl, Decl... moreDecls)
          Returns the formula (some...| this)
 Expr Module.getAllReachableFacts()
          Return the conjunction of all facts in this module and all reachable submodules (not including field constraints, nor including sig appended constraints)
 Expr Func.getBody()
          Return the body of this predicate/function.
 Expr ExprQt.getBound(int i)
          Return the i-th variable's bound.
 Expr Expr.gt(Expr x)
          Returns the formula (this > x)
 Expr Expr.gte(Expr x)
          Returns the formula (this >= x)
 Expr Expr.iff(Expr x)
          Returns the formula (this iff x)
 Expr Expr.iminus(Expr x)
           
 Expr Expr.implies(Expr x)
          Returns the formula (this implies x)
 Expr Expr.in(Expr x)
          Returns the formula (this in x)
 Expr Expr.intersect(Expr x)
          Returns the expression (this intersects x)
 Expr Expr.iplus(Expr x)
           
 Expr Expr.isSeq_arrow_lone(Expr x)
          Returns the multiplicity constraint (this isSeq->lone x)
 Expr Expr.ite(Expr x, Expr y)
          Returns the expression/integer/formula (this => x else y)
 Expr Expr.join(Expr x)
          Returns the expression (this.x)
 Expr Expr.lone_arrow_any(Expr x)
          Returns the multiplicity constraint (this lone->set x)
 Expr Expr.lone_arrow_lone(Expr x)
          Returns the multiplicity constraint (this lone->lone x)
 Expr Expr.lone_arrow_one(Expr x)
          Returns the multiplicity constraint (this lone->one x)
 Expr Expr.lone_arrow_some(Expr x)
          Returns the multiplicity constraint (this lone->some x)
 Expr Expr.lone()
          Returns the formula (lone this)
 Expr Expr.loneOf()
          Return the multiplicity expression "lone this"
 Expr Expr.lt(Expr x)
          Returns the formula (this < x)
 Expr Expr.lte(Expr x)
          Returns the formula (this <= x)
static Expr ExprChoice.make(Pos pos, ConstList<Expr> choices, ConstList<java.lang.String> reasons)
          Construct an ExprChoice node.
 Expr ExprUnary.Op.make(Pos pos, Expr sub)
          Construct an ExprUnary node.
 Expr ExprUnary.Op.make(Pos pos, Expr sub, Err extraError, long extraWeight)
          Construct an ExprUnary node.
static Expr ExprITE.make(Pos pos, Expr cond, Expr left, Expr right)
          Constructs a ExprITE expression.
static Expr ExprLet.make(Pos pos, ExprVar var, Expr expr, Expr sub)
          Constructs a LET expression.
static Expr ExprBadJoin.make(Pos pos, Pos closingBracket, Expr left, Expr right)
          Constructs an ExprBadJoin node.
 Expr ExprBinary.Op.make(Pos pos, Pos closingBracket, Expr left, Expr right)
          Constructs a new ExprBinary node.
static Expr ExprBadCall.make(Pos pos, Pos closingBracket, Func fun, ConstList<Expr> args, long extraPenalty)
          Constructs an ExprBadCall object.
static Expr ExprCall.make(Pos pos, Pos closingBracket, Func fun, java.util.List<Expr> args, long extraPenalty)
          Constructs an ExprCall node with the given predicate/function "fun" and the list of arguments "args".
 Expr ExprQt.Op.make(Pos pos, Pos closingBracket, java.util.List<Decl> decls, Expr sub)
          Constructs a quantification expression with "this" as the operator.
static Expr ExprConstant.makeNUMBER(int n)
          Constructs the integer "n"
 Expr Expr.minus(Expr x)
          Returns the expression (this-x)
 Expr Expr.mul(Expr x)
          Returns the formula "this.mul[x]" (the result of multiplying this by x)
 Expr Expr.no()
          Returns the formula (no this)
 Expr Expr.not()
          Returns the formula (not this)
 Expr Expr.one_arrow_any(Expr x)
          Returns the multiplicity constraint (this one->set x)
 Expr Expr.one_arrow_lone(Expr x)
          Returns the multiplicity constraint (this one->lone x)
 Expr Expr.one_arrow_one(Expr x)
          Returns the multiplicity constraint (this one->one x)
 Expr Expr.one_arrow_some(Expr x)
          Returns the multiplicity constraint (this one->some x)
 Expr Expr.one()
          Returns the formula (one this)
 Expr Expr.oneOf()
          Return the multiplicity expression "one this"
 Expr Expr.or(Expr x)
          Returns the formula (this or x)
 Expr Expr.override(Expr x)
          Returns the expression (this++x)
 Expr Module.parseOneExpressionFromString(java.lang.String input)
          Parse one expression by starting fromt this module as the root module.
 Expr Expr.plus(Expr x)
          Returns the expression (this+x)
 Expr Expr.product(Expr x)
          Returns the expression (this -> x) which can also be regarded as a multiplicity constraint (this set->set x)
 Expr Expr.range(Expr x)
          Returns the expression (this :> x)
 Expr Expr.reflexiveClosure()
          Returns the expression (*this)
 Expr Expr.rem(Expr x)
          Returns the formula "this.rem[x]" (the remainder of dividing this by x)
 Expr Expr.resolve_as_formula(java.util.Collection<ErrorWarning> warnings)
          Converts this into a "formula" if possible, then resolves it if ambiguous.
 Expr Expr.resolve_as_int(java.util.Collection<ErrorWarning> warnings)
          Converts this into an "integer expression" if possible, then resolves it if ambiguous.
 Expr Expr.resolve_as_set(java.util.Collection<ErrorWarning> warnings)
          Converts this into a "set or relation" if possible, then resolves it if ambiguous.
 Expr Sig.resolve(Type t, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr Sig.Field.resolve(Type t, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprBadJoin.resolve(Type t, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprQt.resolve(Type unused, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprUnary.resolve(Type p, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprCustom.resolve(Type t, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprVar.resolve(Type p, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprBadCall.resolve(Type t, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprConstant.resolve(Type type, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprLet.resolve(Type p, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprITE.resolve(Type p, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprBad.resolve(Type t, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
abstract  Expr Expr.resolve(Type t, java.util.Collection<ErrorWarning> warnings)
          Resolves this expression if ambiguous.
 Expr ExprBinary.resolve(Type p, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprChoice.resolve(Type t, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprList.resolve(Type p, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr ExprCall.resolve(Type t, java.util.Collection<ErrorWarning> warns)
          Resolves this expression if ambiguous.
 Expr Expr.setOf()
          Return the multiplicity expression "set this"
 Expr Expr.sha(Expr x)
          Returns the integer expression (this >> x)
 Expr Expr.shl(Expr x)
          Returns the integer expression (this << x)
 Expr Expr.shr(Expr x)
          Returns the integer expression (this >>> x)
 Expr Expr.some_arrow_any(Expr x)
          Returns the multiplicity constraint (this some->set x)
 Expr Expr.some_arrow_lone(Expr x)
          Returns the multiplicity constraint (this some->lone x)
 Expr Expr.some_arrow_one(Expr x)
          Returns the multiplicity constraint (this some->one x)
 Expr Expr.some_arrow_some(Expr x)
          Returns the multiplicity constraint (this some->some x)
 Expr Expr.some()
          Returns the formula (some this)
 Expr Expr.someOf()
          Return the multiplicity expression "some this"
 Expr Expr.sumOver(Decl firstDecl, Decl... moreDecls)
          Returns the integer (sum...| this)
 Expr Type.toExpr()
          Convert this type into a UNION of PRODUCT of sigs.
 Expr Expr.transpose()
          Returns the expression (~this)
 Expr Expr.typecheck_as_formula()
          Converts this into a "formula" if possible; otherwise, returns an Expr with a nonempty error list
 Expr Expr.typecheck_as_int()
          Converts this into an "integer expression" if possible; otherwise, returns an Expr with a nonempty error list
 Expr Expr.typecheck_as_set()
          Converts this into a "set or relation" if possible; otherwise, returns an Expr with a nonempty error list
 

Methods in edu.mit.csail.sdg.alloy4compiler.ast that return types with arguments of type Expr
 ConstList<Pair<java.lang.String,Expr>> Module.getAllAssertions()
          Return an unmodifiable list of all assertions in this module.
 SafeList<Pair<java.lang.String,Expr>> Module.getAllFacts()
          Return an unmodifiable list of all facts in this module.
 SafeList<Expr> Sig.getFacts()
          Return the list of per-atom facts; each expression is allowed to refer to this.decl.get()
 

Methods in edu.mit.csail.sdg.alloy4compiler.ast with parameters of type Expr
 ExprList ExprList.addArg(Expr x)
          Return a new ExprList object that is the same as this one except with one additional argument.
 Sig.Field Sig.addDefinedField(Pos pos, Pos isPrivate, Pos isMeta, java.lang.String label, Expr bound)
          Add then return a new field F where this.F is bound to an exact "definition" expression.
 void Sig.addFact(Expr fact)
          Add a new per-atom fact; this expression is allowed to refer to this.decl.get()
 Sig.Field Sig.addField(java.lang.String label, Expr bound)
          Add then return a new field, where "all x: ThisSig | x.F in bound"
 void Module.addGlobal(java.lang.String name, Expr value)
          Add a global expression; if the name already exists, it is removed first.
 Sig.Field[] Sig.addTrickyField(Pos pos, Pos isPrivate, Pos isDisjoint, Pos isDisjoint2, Pos isMeta, java.lang.String[] labels, Expr bound)
          Add then return a new field, where "all x: ThisSig | x.F in bound"
 Expr Expr.and(Expr x)
          Returns the formula (this and x)
 Expr Expr.any_arrow_lone(Expr x)
          Returns the multiplicity constraint (this set->lone x)
 Expr Expr.any_arrow_one(Expr x)
          Returns the multiplicity constraint (this set->one x)
 Expr Expr.any_arrow_some(Expr x)
          Returns the multiplicity constraint (this set->some x)
 Expr Func.call(Expr... args)
          Convenience method that calls this function with the given list of arguments.
 Command Command.change(Expr newFormula)
          Constructs a new Command object where it is the same as the current object, except with a different formula.
 Expr Expr.div(Expr x)
          Returns the formula "this.div[x]" (the quotient of dividing this by x)
 Expr Expr.domain(Expr x)
          Returns the expression (this <: x)
 Expr Expr.equal(Expr x)
          Returns the formula (this==x)
 Expr Expr.gt(Expr x)
          Returns the formula (this > x)
 Expr Expr.gte(Expr x)
          Returns the formula (this >= x)
 Expr Expr.iff(Expr x)
          Returns the formula (this iff x)
 Expr Expr.iminus(Expr x)
           
 Expr Expr.implies(Expr x)
          Returns the formula (this implies x)
 Expr Expr.in(Expr x)
          Returns the formula (this in x)
 Expr Expr.intersect(Expr x)
          Returns the expression (this intersects x)
 Expr Expr.iplus(Expr x)
           
 boolean Sig.isSame(Expr obj)
          Returns true if we can determine the two expressions are equivalent; may sometimes return false.
 boolean ExprUnary.isSame(Expr obj)
          Returns true if we can determine the two expressions are equivalent; may sometimes return false.
 boolean ExprConstant.isSame(Expr obj)
          Returns true if we can determine the two expressions are equivalent; may sometimes return false.
 boolean ExprITE.isSame(Expr obj)
          Returns true if we can determine the two expressions are equivalent; may sometimes return false.
 boolean Expr.isSame(Expr obj)
          Returns true if we can determine the two expressions are equivalent; may sometimes return false.
 boolean ExprBinary.isSame(Expr obj)
          Returns true if we can determine the two expressions are equivalent; may sometimes return false.
 boolean ExprHasName.isSame(Expr obj)
          Returns true if we can determine the two expressions are equivalent; may sometimes return false.
 boolean ExprCall.isSame(Expr obj)
          Returns true if we can determine the two expressions are equivalent; may sometimes return false.
 Expr Expr.isSeq_arrow_lone(Expr x)
          Returns the multiplicity constraint (this isSeq->lone x)
 Expr Expr.ite(Expr x, Expr y)
          Returns the expression/integer/formula (this => x else y)
 Expr Expr.join(Expr x)
          Returns the expression (this.x)
 Expr Expr.lone_arrow_any(Expr x)
          Returns the multiplicity constraint (this lone->set x)
 Expr Expr.lone_arrow_lone(Expr x)
          Returns the multiplicity constraint (this lone->lone x)
 Expr Expr.lone_arrow_one(Expr x)
          Returns the multiplicity constraint (this lone->one x)
 Expr Expr.lone_arrow_some(Expr x)
          Returns the multiplicity constraint (this lone->some x)
 Expr Expr.lt(Expr x)
          Returns the formula (this < x)
 Expr Expr.lte(Expr x)
          Returns the formula (this <= x)
 Expr ExprUnary.Op.make(Pos pos, Expr sub)
          Construct an ExprUnary node.
 Expr ExprUnary.Op.make(Pos pos, Expr sub, Err extraError, long extraWeight)
          Construct an ExprUnary node.
static Expr ExprITE.make(Pos pos, Expr cond, Expr left, Expr right)
          Constructs a ExprITE expression.
static Expr ExprLet.make(Pos pos, ExprVar var, Expr expr, Expr sub)
          Constructs a LET expression.
static Expr ExprBadJoin.make(Pos pos, Pos closingBracket, Expr left, Expr right)
          Constructs an ExprBadJoin node.
 Expr ExprBinary.Op.make(Pos pos, Pos closingBracket, Expr left, Expr right)
          Constructs a new ExprBinary node.
 Expr ExprQt.Op.make(Pos pos, Pos closingBracket, java.util.List<Decl> decls, Expr sub)
          Constructs a quantification expression with "this" as the operator.
static ExprList ExprList.makeAND(Pos pos, Pos closingBracket, Expr a, Expr b)
          Generates the expression (arg1 and arg2)
static ExprList ExprList.makeOR(Pos pos, Pos closingBracket, Expr a, Expr b)
          Generates the expression (arg1 || arg2)
 Expr Expr.minus(Expr x)
          Returns the expression (this-x)
 Expr Expr.mul(Expr x)
          Returns the formula "this.mul[x]" (the result of multiplying this by x)
 Expr Expr.one_arrow_any(Expr x)
          Returns the multiplicity constraint (this one->set x)
 Expr Expr.one_arrow_lone(Expr x)
          Returns the multiplicity constraint (this one->lone x)
 Expr Expr.one_arrow_one(Expr x)
          Returns the multiplicity constraint (this one->one x)
 Expr Expr.one_arrow_some(Expr x)
          Returns the multiplicity constraint (this one->some x)
 Expr Expr.or(Expr x)
          Returns the formula (this or x)
 Expr Expr.override(Expr x)
          Returns the expression (this++x)
 Expr Expr.plus(Expr x)
          Returns the expression (this+x)
 Expr Expr.product(Expr x)
          Returns the expression (this -> x) which can also be regarded as a multiplicity constraint (this set->set x)
 Expr Expr.range(Expr x)
          Returns the expression (this :> x)
 Expr Expr.rem(Expr x)
          Returns the formula "this.rem[x]" (the remainder of dividing this by x)
 void Func.setBody(Expr newBody)
          Changes the method body.
 Expr Expr.sha(Expr x)
          Returns the integer expression (this >> x)
 Expr Expr.shl(Expr x)
          Returns the integer expression (this << x)
 Expr Expr.shr(Expr x)
          Returns the integer expression (this >>> x)
 Expr Expr.some_arrow_any(Expr x)
          Returns the multiplicity constraint (this some->set x)
 Expr Expr.some_arrow_lone(Expr x)
          Returns the multiplicity constraint (this some->lone x)
 Expr Expr.some_arrow_one(Expr x)
          Returns the multiplicity constraint (this some->one x)
 Expr Expr.some_arrow_some(Expr x)
          Returns the multiplicity constraint (this some->some x)
 T VisitReturn.visitThis(Expr x)
          This is the start method that begins a traversal over the given expression.
 

Method parameters in edu.mit.csail.sdg.alloy4compiler.ast with type arguments of type Expr
static Expr ExprChoice.make(Pos pos, ConstList<Expr> choices, ConstList<java.lang.String> reasons)
          Construct an ExprChoice node.
static ExprList ExprList.make(Pos pos, Pos closingBracket, ExprList.Op op, java.util.List<? extends Expr> args)
          Generates a call to a builtin predicate
static Expr ExprBadCall.make(Pos pos, Pos closingBracket, Func fun, ConstList<Expr> args, long extraPenalty)
          Constructs an ExprBadCall object.
static Expr ExprCall.make(Pos pos, Pos closingBracket, Func fun, java.util.List<Expr> args, long extraPenalty)
          Constructs an ExprCall node with the given predicate/function "fun" and the list of arguments "args".
static ExprList ExprList.makeDISJOINT(Pos pos, Pos closingBracket, java.util.List<? extends Expr> args)
          Generates the expression disj[arg1, args2, arg3...]
static ExprList ExprList.makeTOTALORDER(Pos pos, Pos closingBracket, java.util.List<? extends Expr> args)
          Generates the expression pred/totalOrder[arg1, args2, arg3...]
 

Constructors in edu.mit.csail.sdg.alloy4compiler.ast with parameters of type Expr
Command(boolean check, int overall, int bitwidth, int maxseq, Expr formula)
          Constructs a new Command object.
Command(Pos pos, java.lang.String label, boolean check, int overall, int bitwidth, int maxseq, int expects, java.lang.Iterable<CommandScope> scope, java.lang.Iterable<Sig> additionalExactSig, Expr formula, Command parent)
          Constructs a new Command object.
Decl(Pos isPrivate, Pos disjoint, Pos disjoint2, java.util.List<? extends ExprHasName> names, Expr expr)
          This constructs a declaration; the list of names must not be empty.
Func(Pos pos, Pos isPrivate, java.lang.String label, java.util.List<Decl> decls, Expr returnDecl, Expr body)
          Constructs a new predicate/function.
Func(Pos pos, java.lang.String label, java.util.List<Decl> decls, Expr returnDecl, Expr body)
          Constructs a new predicate/function.
 

Uses of Expr in edu.mit.csail.sdg.alloy4compiler.parser
 

Methods in edu.mit.csail.sdg.alloy4compiler.parser that return Expr
 Expr CompModule.getAllReachableFacts()
          Return the conjunction of all facts in this module and all reachable submodules (not including field constraints, nor including sig appended constraints)
static Expr CompUtil.parseOneExpression_fromString(Module world, java.lang.String input)
          Parses then typecheck the given input String as an Alloy expression from that world
 Expr CompModule.parseOneExpressionFromString(java.lang.String input)
          Parse one expression by starting fromt this module as the root module.
 

Methods in edu.mit.csail.sdg.alloy4compiler.parser that return types with arguments of type Expr
 ConstList<Pair<java.lang.String,Expr>> CompModule.getAllAssertions()
          Return an unmodifiable list of all assertions in this module.
 SafeList<Pair<java.lang.String,Expr>> CompModule.getAllFacts()
          Return an unmodifiable list of all facts in this module.
 

Methods in edu.mit.csail.sdg.alloy4compiler.parser with parameters of type Expr
 void CompModule.addGlobal(java.lang.String name, Expr value)
          Add a global expression; if the name already exists, it is removed first.
 

Uses of Expr in edu.mit.csail.sdg.alloy4compiler.sim
 

Methods in edu.mit.csail.sdg.alloy4compiler.sim with parameters of type Expr
 boolean SimInstance.cform(Expr x)
          Convenience method that evalutes x and casts the result to be a boolean.
 int SimInstance.cint(Expr x)
          Convenience method that evalutes x and cast the result to be a int.
 SimTupleset SimInstance.cset(Expr x)
          Convenience method that evalutes x and cast the result to be a tupleset
 boolean SimInstance.equal(Expr a, Expr b)
          Helper method that evaluates the formula "a = b"
 boolean SimInstance.isIn(Expr a, Expr b)
          Helper method that evaluates the formula "a in b"
 boolean SimInstance.isIn(SimTuple a, Expr b)
          Helper method that evaluates the formula "a in b" where b.mult==0
 

Uses of Expr in edu.mit.csail.sdg.alloy4compiler.translator
 

Methods in edu.mit.csail.sdg.alloy4compiler.translator with parameters of type Expr
static java.lang.Object TranslateAlloyToKodkod.alloy2kodkod(A4Solution sol, Expr expr)
          Translate the Alloy expression into an equivalent Kodkod Expression or IntExpression or Formula object.
 java.lang.Object A4Solution.eval(Expr expr)
          If this solution is solved and satisfiable, evaluates the given expression and returns an A4TupleSet, a java Integer, or a java Boolean.