|
||||||||||
PREV NEXT | FRAMES NO FRAMES |
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. |
|
||||||||||
PREV NEXT | FRAMES NO FRAMES |