Skip to content

Formula Programs

Jump to bottom
Dan Ogles edited this page Jun 17, 2022 · 5 revisions

Introduction

Vertexy includes a high-level, declarative DSL. The grammar is based on Answer Set Programming, which is very similar to Prolog. It allows you to specify rules that must be satisfied for any generated content. This document describes how to create Rule Programs in Vertexy.

Formulas

Formulas in Vertexy are used to specify rules for generation. It is easiest to start with a simple example:

const int Bryan = 0;
const int Lloyd = 1;

VXY_FORMULA(motive, 1);
motive(Bryan);
motive(Lloyd);

Here we have defined a formula, called motive, that takes a single argument. Then we define two facts: motive(Bryan), and motive(Lloyd). This specifies that in any solution generated by Vertexy, these two statements will always be true. Note that formula arguments are always integers.

Let us define another formula:

VXY_FORMULA(alibi, 1);
alibi(Lloyd);

Here we have defined a new formula called alibi, again taking a single argument, and defined a fact: alibi(Lloyd).

From these statements, Vertexy will guarantee that in any solution it creates, motive(Bryan), motive(Lloyd), and alibi(Lloyd) will always exist.

Formulas aren't Functions

While their syntax is similar to a typical function call, formulas do not "return" values. Specifying motive(Bryan) simply indicates that a "thing" called motive(Bryan) exists. In Vertexy, we call the instantation of a formula an atom.

As an extension to traditional answer set programming languages, Vertexy formulas can have multiple states of existence, which will be covered later. By default however, a particular instantiation of a formula like alibi(Lloyd) can have two states: it either exists or it does not.

Rules

Providing facts is important for defining the broad outline of what you want to generate, but does not get you very far. Rules allow you to specify things that are conditionally true. For example:

VXY_FORMULA(guilty, 1);
guilty(Bryan) <<= motive(Bryan) && ~alibi(Bryan)

The <<= operator defines a conditional rule and can be read as "if". The ~ operator is used as negation. This statement can thus be read as "guilty(Bryan) must exist if motive(Bryan) exists and alibi(Bryan) does not exist". In this case, since we already defined motive(Bryan) as a fact, and alibi(Bryan) was not specified at all, guilty(Bryan) will exist in any generated solution.

When talking about rules, the part of the statement before the <<= is called the head of the rule, and the part after is called the body. The body is always a set of conjunctive terms, connected using the && operator. Facts can be thought of as simply rules with no body: the body is always true, so the head of the rule will always be true.

When Vertexy solves a rule program, it returns a value for every formula instantation wherein all rules hold. In this case, any solutions returned by Vertexy would include guilty(Bryan) and not guilty(Lloyd).

Closed Universe

Within a Vertexy program, the only atoms that can possibly exist are ones that are in the head of a rule (or are facts). If an atom does not appear in the head of any rule, the Vertexy compiler will assume the atom does not exist. In the prior example, alibi(Bryan) was never specified as either a fact or the head of a rule, so the Vertexy will assume it can never exist. This behavior is what allows Vertexy to make logical inferences: given a universe of atoms that can possibly exist, it will create an instantiation of the universe with atoms that exist and satisfy all rules defined for the universe (or report that there is no possible universe that satisfies all rules).

For more information on this property, see Stable Models.

Wildcards

Working with only discrete values like Bryan and Lloyd would be very limiting. Wildcards allow you to specify rules without specifying particular values. For example:

VXY_WILDCARD(SUSPECT);
guilty(SUSPECT) <<= motive(SUSPECT) && ~alibi(SUSPECT);

Here we defined a wildcard called SUSPECT. (Traditionally wildcards are specified in all-caps to differentiate them from formulas or variables, but this is not required.) When a wildcard is used, all of its values within the statement must "match up". The previous statement is equivalent to the two following statements:

guilty(LLoyd) <<= motive(LLoyd) && ~alibi(LLoyd);
guilty(Bryan) <<= motive(Bryan) && ~alibi(Bryan);

Note that SUSPECT is bound to the same value in each term.

NOTE! Wildcards can be used in multiple statements, but they don't keep their value between statements. For example:

guilty(SUSPECT) <<= motive(SUSPECT) && ~alibi(SUSPECT);
suspicious(SUSPECT) <<= motive(SUSPECT);

Solving this would return guilty(Bryan), suspicious(Bryan), and suspicious(Lloyd). In other words, SUSPECT in the first rule has no effect on SUSPECT in the second rule. Just think of them as named placeholders within a statement.

Wildcard Restrictions

Wildcards can be used for any formula argument, but a rule statement must be "safe". This, in part, is to ensure that no statement can create an infinite or unknown number of potential atoms. In order to make sure a rule is safe, one requirement must be followed: any wildcard must appear at least once in a non-negative term of the body.

Examples:

VXY_WILDCARD(X);
guilty(X); 					// NOT SAFE: X does not appear in body
guilty(X) <<= ~innocent(X); 			// NOT SAFE: X only appears in negative body terms
guilty(X) <<= suspect(X) && ~innocent(X);	// SAFE: X appears in at least one positive body term

If a statement is not safe, Vertexy will report an error at runtime.

Choices

Our example thus far does not lend Bryan a lot of credit: the guilty rule that we defined above ensures the guilty(Bryan) will always be true, because motive(Bryan) is true and alibi(Bryan) does not exist. Alternatively, we can specify the rule like so:

guilty(SUSPECT).choice() <<= motive(SUSPECT) && ~alibi(SUSPECT);

Appending .choice() to the rule's head means that guilty(SUSPECT) may be true if motive(SUSPECT) is true and alibi(SUSPECT) is false or doesn't exist. This is an essential ingredient to procedural content generation: it allows for multiple possibilities. The choice is determined by the Vertey runtime, based on the random seed supplied. However, all rules must still be simultaneously satisfied for in order for Vertexy to return a solution. In this case, the only two solutions are:

  • guilty(Bryan) and not guilty(Lloyd)
  • not guilty(Bryan) and not guilty(Lloyd)

Using choice() is actually shorthand notation for the following (equivalent) set of statements:

guilty(SUSPECT) <<= motive(SUSPECT) && ~alibi(SUSPECT) && ~not_guilty(SUSPECT);
not_guilty(SUSPECT) <<= ~guilty(SUSPECT);

However, this would fail to compile, because the second statement is not safe: the SUSPECT wildcard does not appear in any positive body term. Vertexy avoids this by transforming choices after all wildcards have been replaced.

Note that, absent of choices, all rules are effectively predetermined. When Vertexy compiles a rule program, it will identify all rules that can be statically determined, resulting in a list of fact atoms that always exist. The remaining atoms that possibly exist are fed to the constraint solver to decide.

Disjunctions

Disjunctions can only appear in a rule head and offer an alternative way of describing choices.

innocent(SUSPECT) | convicted(SUSPECT) | gotaway(SUSPECT) <<= motive(SUSPECT) && ~alibi(SUSPECT)

This specifies that if motive(SUSPECT) is true and alibi(SUSPECT) is false or does not exist, then either innocent(SUSPECT) is true, convicted(SUSPECT) is true, or gotaway(SUSPECT) is true. Vertexy ensures that if the rule's body is true, one and only one of the terms in the head's disjunction will be true.

Disallowing

In addition to rules, you can specify anti-rules. These are rule bodies that the Vertexy runtime will ensure will be false in any returned solution. Use the Program::disallow() function to specify an anti-rule, for example:

Program::disallow(convicted(SUSPECT) && judge(SUSPECT, JUDGE) && corrupt(JUDGE));

Vertexy will ensure that no solution is returned in which the specified statement holds true for any set of atoms.

Rule Programs

Rules must be specified within program blocks. In C++, these are (typically) lambda functions passed into the Vertexy::Program::define() function. Here is the previous example in a format that can be compiled:

auto prg = Program::define([]() {
	const int Bryan = 0;
	const int Lloyd = 1;

	VXY_FORMULA(motive, 1);
	motive(Bryan);
	motive(Lloyd);

	VXY_FORMULA(alibi, 1);
	alibi(Lloyd);

	VXY_FORMULA(innocent, 1);
	VXY_FORMULA(convicted, 1);
	VXY_FORMULA(gotaway, 1);

	VXY_WILDCARD(SUSPECT);
	innocent(SUSPECT) | convicted(SUSPECT) | gotaway(SUSPECT) <<= motive(SUSPECT) && ~alibi(SUSPECT)
});

In order for a program to be solved, it must be added to a Vertexy constraint solver:

ConstraintSolver solver;
solver.addProgram(prg());
solver.solve();

A program block can even take arguments, return values, and multiple program instances can be added to a single solver. This will be covered in a later section.

Hello (Procedural) World

Now that we've covered the basics, let's see how this works in action! Here is a simple program that creates random mazes.

auto prg = Program::define([](int width, int height) {
	// declare column(X) fact for each column
	VXY_FORMULA(column, 1);
	column = Program::range(0, width-1);
	// declare row(X) fact for each row
	VXY_FORMULA(row, 1);
	row = Program::range(0, height-1);

	// Specify the entrance coordinate, near top-left of the maze.
	VXY_FORMULA(entrance, 2);
	entrance(1, 2);
	
	// Specify the exist, near bottom-center of the maze.
	VXY_FORMULA(exit, 2);
	exit(width/2, height-1);

	// define some wildcards we'll (re)use
	VXY_WILDCARD(X);
	VXY_WILDCARD(Y);

	// make a formula defining the borders of the maze
	VXY_FORMULA(border, 2);
	border(X,0) 			<<= column(X);
	border(X,height-1) 		<<= column(X);
	border(0,Y) 			<<= row(Y);
	border(width-1,Y) 		<<= row(Y);
	
	// a tile may be either solid or blank.
	VXY_FORMULA(blank, 2);
	VXY_FORMULA(solid, 2);

	// A tile on the border should be solid, unless it's the entrance/exit.
	solid(X,Y) <<= border(X,Y) && ~entrance(X,Y) && ~exit(X,Y);
	// Otherwise, a tile could be solid or blank
	solid(X,Y) | blank(X,Y) <<= ~border(X,Y);

	// specify what tiles are traversable
	VXY_FORMULA(passable, 2);
	passable(X,Y) <<= entrance(X,Y);
	passable(X,Y) <<= exit(X,Y);
	passable(X,Y) <<= blank(X,Y);

	// Ensure the exit can be reached from the entrance.		
	VXY_FORMULA(reach, 2);
	// We can always reach the entrance.
	reach(X,Y) <<= entrance(X,Y);
	// We can reach a tile if it is passable, and we reach an adjacent tile.
	reach(X,Y) <<= passable(X,Y) && reach(X-1, Y);
	reach(X,Y) <<= passable(X,Y) && reach(X+1, Y);
	reach(X,Y) <<= passable(X,Y) && reach(X, Y-1);
	reach(X,Y) <<= passable(X,Y) && reach(X, Y+1);

	// Ensure that the exit is always reachable.
	Program::disallow(exit(X,Y) && ~reach(X,Y));
});

ConstraintSolver solver;
solver.addProgram(prg(10, 10)); // instantiate the program with width/height set to 10.
solver.solve();

There are several things worth noting in here:

  • This program block takes two arguments, width and height. This allows the program to be instantiated with different inputs. You could, for example, call prg(100,100) to generate a 100x100 maze instead of a 10x10 maze.
  • The Program::range() function is a convenience method for defining multiple facts. The column = Program::range(0,width-1) statement is equivalent to specifying column(0); column(1); ... column(width-1);.
  • A formula may appear in the head of a rule multiple times. This is how you encode "or" constraints. For example, passable(X,Y) is defined to exist if the tile is an entrance or an exit or blank.
  • You can perform simple math operations against wildcards, as seen with reach. Supported operations are addition, subtraction, multiplication, and division.
  • reach is defined recursively: the entrance is defined as always reachable, and other tiles are defined as reachable if an adjacent tile is reachable. This is a very powerful feature with rules allowing you to express quite complicated custom constraints. (Note: the Vertexy solver includes a ReachabilityConstraint that is more efficient for ensuring reachability between points. We avoid using that here for purposes of demonstration.)

Once solve() is called, Vertexy will search for a solution that satisfies all rules in all programs added to it (as well as any additional constraints added to the solver). In this case, atoms like border(0,4) are pre-established as facts. Meanwhile, atoms like wall(4,3), blank(9,9), or reach(4,2) only possibly exist. Vertexy will search to find a set of atoms that exist and also satisfy all rules.

Binding

To actually get access to the solution, it is necessary to bind formulas to variables. This allows you to query their values after solving has completed. Expanding on the previous example:

struct MazeResult
{
	FormulaResult<2> entrance, exit, blank, solid;
};

auto prg = Program::define([](int width, int height) {
	.
	.
	.
	return MazeResult{entrance, exit, blank, solid};
});

Program blocks can return values. Here, we return the entrance, exit, blank, and solid formulas. Note that the type returned is a FormulaResult class, where the template parameter is the number of arguments for the formula (2 for all of them, in this case).

You can get access to the return value of a program block by instantiating the program:

auto prgInstance = prg(10, 10);
// access return value e.g. prgInstance->getResult().entrance;

FormulaResult allows you to bind variables to atoms created for the formula. Here we bind each potential blank atom to a unique variable, prior to solving:

auto prgInstance = prg(10, 10);

ConstraintSolver solver;
solver.addProgram(prgInstance);

vector<VarID> blankVars(10*10);
prgInstance.getResult().blank.bind([&](const ProgramSymbol& X, const ProgramSymbol& Y) {
	VarID newVar = solver.makeBoolean();
	blankVars[X.getInt() + Y.getInt()*10] = newVar;
	return newVar;
});

solver.solve();

// Get the value of blank(4,3)
bool isBlank = solver.getSolvedValue(blankVars[4 + 3*10]) != 0;

Note that formulas must be bound prior to calling solve(). Also note that formulas do not need to be bound in order for them to be solved: all rules are always satisfied by the solver; binding simply allows you to retrieve the results for atoms you care about.

Formula Scope and Multiple Program Instances

It is entirely possible to add multiple program instances to the solver. The solver will solve every instance added to it, and will only return a solution if all instances are satisfied. For example, this will tell the solver to find a solution for a 10x10 maze, and also a 100x100 maze:

ConstraintSolver solver;
solver.addProgram(prg(10,10));
solver.addProgram(prg(100,100));

Note that each instance of a program has its own unique formulas. That is to say, blank(X,Y) in the first program instance has no relation to blank(X,Y) in the second program instance (for any X or Y). In order to retreive the results of each maze, you would need to bind to the program instance of both:

auto smallMaze = prg(10,10);
auto largeMaze = prg(100, 100);
smallMaze.getResult().blank.bind([&](...) { ... });
largeMaze.getResult().blank.bind([&](...) { ... });

In some cases it is desirable to share a formula between multiple program instances. For example, to improve modularity or to have a program that defines "global" rules and multiple smaller programs to define "local" rules. To allow for this, formulas can be defined outside of program blocks:

// define some global formulas, outside of a program block.
VXY_FORMULA(blank, 1);
VXY_FORMULA(solid, 1);
auto prg = Program::define([&](int width, int height) { ... }); // as before
// create a new program:
auto wallRules = Program::define([&](int width, int height) {
	// ensure that there is no 2x2 all-solid block.
	Program::disallow(solid(X,Y) && solid(X+1,Y) && solid(X,Y+1) && solid(X+1,Y+1));
});

ConstraintSolver solver;
// add base rules:
solver.addProgram(prg(10,10));
// add additional rules:
solver.addProgram(wallRules());

Since solid and blank are defined outside of a Program::define() block, they are considered global: all uses of the formula refer to the same one. Note that although formulas can be defined globally, rules (or Program::disallow() statements) must be defined with a program block.

Global formulas do not need to be returned as FormulaResult's from program blocks; they can be bound directly:

// outside of a program block...
VXY_FORMULA(blank, 1);
blank.bind(solver, [&](const ProgramSymbol& X, const ProgramSymbol& Y) { ... });

The only difference versus binding a program instance's FormulaResult is that the solver must be passed in as an argument when binding global formulas.

The C++ type of a global formula is Formula<ARITY>, where ARITY is the formula's number of arguments. You can store these and pass them along in functions.

Formula Domains

Thus far we have discussed atoms that have a boolean status: they either exist or they do not. As an extension of typical answer set programming languages, we allow formulas to have more than one "existence state", called the formula's domain. Every atom created from the formula will have exactly one value in its domain. Instead of having a separate formula for blank, empty, etc., we can define a formula domain like so:

// either inside or outside of a program block...
VXY_DOMAIN_BEGIN(TileDomain)
	VXY_DOMAIN_VALUE(blank);
	VXY_DOMAIN_VALUE(solid);
	VXY_DOMAIN_VALUE(entrance);
	VXY_DOMAIN_VALUE(exit);
VXY_DOMAIN_END()

To declare a formula using a domain, use the VXY_DOMAIN_FORMULA macro instead of VXY_FORMULA:

VXY_DOMAIN_FORMULA(tileType, TileDomain, 2); // define tileType with 2 arguments, using TileDomain.

Now, every tileType(X,Y) atom will have a value blank, solid, exit, or entrance. Note that this does not include non-existence of the atom: for example, tileType(-1,-1) will not exist as it is outside of the map bounds, so will not have any value in its domain.

When binding to a domain formula, you must create a Vertexy variable with a domain size that is large enough to include the domain:

tileType.bind(solver, [&](const ProgramSymbol& X, const ProgramSymbol& Y) {
	// return a variable that can have values 0, 1, 2, or 3.
	return solver.makeVariable(TEXT("tileVar"), SolverVariableDomain(0, 3));
});

Here we are creating variables with a domain size of 4, which is enough to hold all values in TileDomain. However, there are no values to indicate the atom does not exist. Recall in the earlier examples without formula domains, we bound atoms to boolean variables. The boolean would be set to to true if the atom exists, and false if it did not. With our domain formula, we have implicity specified that any possible tileVar atom must exist (since all solver variables in a solution must always have exactly one value).

In this case we know that every tile should have an associated atom, so that is fine. However, it is possible to allow for non-existence, by creating a variable with a larger domain and passing a domain mapping to bind:

tileType.bind(
	solver, 
	[&](const ProgramSymbol& X, const ProgramSymbol& Y) {
		// 5 potential values now, instead of 4.
		return solver.makeVariable(TEXT("tileVar"), SolverVariableDomain(0, 4));
	}, 
	// map the TileDomain values to corresponding value of the bound variables.
	vector{1, 2, 3, 4} 
);

Now, if a tileVar atom doesn't exist, the corresponding variable will be set to 0. Note that the domain mapping can also remap values from the formula domain to different values of the variable. In this case if the tile is blank, the corresponding variable will be set to 1.

Using Domains in Rules

Domain formulas can optionally specify subsets ("masks") of values in both head and body terms of rules, using the is() function. For example:

tileVar(X,Y).is(tileVar.solid) <<= border(X,Y);

Note that values from the domain are preceded with the formula name, e.g. tileVar.solid, tileVar.blank, etc.

You can specify multiple domain values inside of an is() clause, using the | operator:

tileVar(X,Y).is(tileVar.empty | tileVar.solid) <<= ~border(X,Y) && ~tileVar(X,Y).is(tileVar.entrance | tileVar.exit);

In this case, we have specified that the tileVar must be either empty or solid if it's not a border tile, and it's not the entrance or exit.

Formula Domain Arrays

Formula domains can include (statically-sized) arrays:

VXY_DOMAIN_BEGIN(TileDomain)
	VXY_DOMAIN_VALUE(blank);
	VXY_DOMAIN_VALUE(solid);
	VXY_DOMAIN_VALUE(entrance);
	VXY_DOMAIN_VALUE(exit);
	VXY_DOMAIN_VALUE_ARRAY(keys, 2);  	// defines domain values keys[0] and keys[1]
	VXY_DOMAIN_VALUE_ARRAY(doors, 2);	// defines domain values doors[0] and doors[1]
VXY_DOMAIN_END()

In this case, TileDomain's size is now 8: there are four non-array values, and 2 array values with 2 elements each.

Domain array values can be used with or without subscripts:

is_key(X,Y) <<= tileType(X,Y).is(tileType.keys); 			// matches both key[0] and key[1]
is_first_key(X,Y) <<= tileType(X,Y).is(tileType.keys[0]);   // matches only key[0]

You can even use wildcards as subscripts:

VXY_WILDCARD(N);
is_nth_key(X,Y,N) <<= tileType(X,Y).is(tileType.keys[N]);

Formula Domain Advantages

In many cases, boolean-domain formulas suffice, but formula domains require fewer rules and are more efficient when you have a set of atoms that are mutually distinct. In this case of our maze example, using a formula domain for the tile type makes sense because each tile can only be one type. With boolean formulas, mutual exclusivity must be manually defined.

For example, the original maze program sample specified a rule with blank(X,Y) | solid(X,Y) as its head. Head disjunctions define mutual exclusivity: blank(X,Y) or solid(X,Y) may be true if the body is true, but not both. Another way to manually define mutual exclusivity is with Program::disallow() statements e.g. Program::disallow(blank(X,Y) && solid(X,Y)). While this works, it is not nearly as efficient as using domain formulas. With normal formulas, each formula needs its own unique solver variable, and rules are manually checked during solving to ensure any mutual exclusivity between variables. Meanwhile, with domain formulas, a single solver variable is created, and mutual exclusivity is implicitly handled without constraints.

Graph Programs

One of the major features of Vertexy is its ability to reason about graphs. As it is searching for solutions to a problem, it can take advantage of knowledge about the interconnections between vertices in a graph to learn new constraints, accelerating its search. Rule programs can be written to take advantage of this.

In order to create a graph-aware rule program, a ITopologyPtr must be passed into the program's arguments, and the program definition should take ProgramVertex as its first argument:

// define a graph program.
auto graphPrg = Program::define([&](ProgramVertex vertex) {...});
// create the graph topology.
auto grid = make_shared<PlanarGridTopology>(10, 10);
// pass the topology in as the first argument
auto graphPrgInst = graphPrg(ITopology::adapt(grid));

This gives the program the information it needs to be able to create graph rules.

Requirements for Graph Rules

For a graph rule to be generated, the following requirements must be met:

  1. The head of the rule must include the vertex argument. (Not applicable for Program::disallow() statements.)
  2. Each body term must include either the vertex argument, or a wildcard that can be derived in terms of the vertex argument.

The vertex parameter passed to the program block is a special identifier. You can think of it as a wildcard that represents any individual vertex on the graph, but it only matches against itself. It is what provides the "thread" to weave together a rule into constraints that can be applied to the entire graph.

To make graph rules of any consequence, it is typically necessary to refer to other vertices. There are three Program functions that can be used to identify vertices relative to another vertex:

  • Program::graphEdge(X,Y) exists for any pair of vertices where vertex X has an outgoing edge to vertex Y.
  • Program::hasGraphLink(X, const TopologyLink&) exists for any vertex X where the supplied TopologyLink points to a valid vertex.
  • Program::graphLink(const TopologyLink&) returns a formula that takes two arguments (X,Y) where X is a vertex and Y is the vertex on the other side of the supplied TopologyLink.

We can redefine some of our maze formulas to take advantage of these:

VXY_FORMULA(border, 1); // now only takes one argument
// This vertex is on the border if there is no adjacent vertex in any of the 4 cardinal directions.
border(vertex) <<= ~Program::hasGraphLink(vertex, PlanarGridTopology::moveUp());
border(vertex) <<= ~Program::hasGraphLink(vertex, PlanarGridTopology::moveDown());
border(vertex) <<= ~Program::hasGraphLink(vertex, PlanarGridTopology::moveLeft());
border(vertex) <<= ~Program::hasGraphLink(vertex, PlanarGridTopology::moveRight());

// any non-border tile should be either solid or blank.
tileType(vertex).is(tileType.solid|tileType.blank) <<= ~border(vertex);

// Define hasAdjacentWall(X) for every vertex where an adjacent vertex's tileType is solid.
VXY_FORMULA(hasAdjacentWall, 1);
hasAdjacentWall(vertex) <<= Program::graphEdge(vertex, X) && tileType(X).is(tileType.solid);

// create formulas for determining the adjacent vertex in each direction.
auto up    = Program::graphLink(PlanarGridTopology::moveUp());
auto down  = Program::graphLink(PlanarGridTopology::moveDown());
auto left  = Program::graphLink(PlanarGridTopology::moveLeft());
auto right = Program::graphLink(PlanarGridTopology::moveRight());

// disallow a 2x2 solid block of walls
VXY_WILDCARD(RIGHT);
VXY_WILDCARD(DOWN);
VXY_WILDCARD(DOWN_RIGHT);
Program::disallow(
	right(vertex, RIGHT) && 
	down(vertex, DOWN) && 
	down(RIGHT, DOWN_RIGHT) &&
	tileType(vertex).is(tileType.solid) &&
	tileType(RIGHT).is(tileType.solid) &&
	tileType(DOWN).is(tileType.solid) &&
	tileType(DOWN_RIGHT).is(tileType.solid)
);

Note that unlike hasGraphLink and graphEdge, Program::graphLink() is not a formula, it returns a formula.

Derivation of graph rules

Let's look at this statement more closely:

hasAdjacentWall(vertex) <<= Program::graphEdge(vertex, X) && tileType(X).is(tileType.solid);

Note that tileType(X) does not include vertex in its arguments. However, the value of the X wildcard can be derived from Program::graphEdge(vertex, X), so the graph rule is generated. Constrast that with this statement:

VXY_FORMULA(twoAdjacentWalls, 1);
twoAdjacentWalls(vertex) <<= tileType(vertex).is(tileType.solid) && tileType(X).is(tileType.solid)

In this case, X can not be derived from anything other than tileType(X), so it will not participate in graph rule generation. This is still a legal statement however; it is equivalent to the following:

twoAdjacentWalls(vertex) <<= tileType(vertex).is(tileType.solid) && tileType(0).is(tileType.solid);
twoAdjacentWalls(vertex) <<= tileType(vertex).is(tileType.solid) && tileType(1).is(tileType.solid);
.
.
.
twoAdjacentWalls(vertex) <<= tileType(vertex).is(tileType.solid) && tileType(<NumVertices-1>).is(tileType.solid);

Matching "vertex"

One caveat mentioned before that bears repeating is that vertex (i.e. the ProgramVertex variable passed into the program block) will only match with itself. This can cause unexpected issues. For example, imagine we're encoding the moves of a knight on a chessboard:

// move left one tile, then up two tiles.
auto moveOne = Program::graphLink(PlanarGridTopology::moveLeft(1).combine(PlanarGridTopology::moveUp(2))),

VXY_FORMULA(validMove, 2);
validMove(vertex, X) <<= moveOne(vertex, X);
// ... specify validMove(vertex, X) for all other valid movements...

// Specify the starting position on the board as top-left most vertex
VXY_FORMULA(startingPosition, 1);
startingPosition(0);

// Define what vertices the Knight can reach from its starting position.
VXY_FORMULA(canReach, 1);
canReach(vertex) <<= startingPosition(X) && validMove(X, vertex); // Uh oh!

In this case, no canReach atoms will be created. That is because we defined validMove(vertex, *), but no definitions of validMove(*, vertex) exist in any rule head. For this to function as intended, you must also define a validMove(X, vertex) rule for every valid move.

Integrating with Constraints

As we have already seen, it is possible to bind formula atoms to solver variables. It is also possible to add any other built-in constraints like e.g. AllDifferentConstraint, CardinalityConstraint or ReachabilityConstraint to further constrain these variables and possible solutions. In many cases this can be more efficient due the optimized specialized implementation of these constraints. There is one important caveat though, following the "closed universe" paradigm: rule programs determine both possible and impossible atoms. Ignoring this can create unexpected or unsatisfiable results.

For example, let's take our original guilty program:

const int Bryan = 0;
const int Lloyd = 1;
auto prg = Program::define([]() {
	VXY_FORMULA(motive, 1);
	motive(Bryan);
	motive(Lloyd);

	VXY_FORMULA(alibi, 1);
	alibi(Lloyd);

	VXY_WILDCARD(SUSPECT);

	VXY_FORMULA(guilty, 1);
	guilty(SUSPECT) <<= motive(SUSPECT) && ~alibi(SUSPECT)
	return alibi;
});

ConstraintSolver solver;
vector alibiVars { solver.makeBoolean(TEXT("alibi(Bryan)")), solver.makeBoolean(TEXT("alibi(Lloyd)")) };

auto prgInst = prg();
// Bind alibi(X)
prgInst->getResult().bind([&](const ProgramSymbol& person) {
	return alibiVars[person.getInt()];
});

// Also give Bryan an alibi, but outside of a rule program:
// (We're doing so explicitly here, but could also be implicit due to external constraints)
solver.setInitialValues(alibiVars[0], {1});
solver.addProgram(prgInst);
solver.solve();

In this example, guilty(Bryan) will always be true, even though the guilty rule explicitly requires that alibi(Bryan) is false and we explicitly set the variable to true before solving via setInitialValues. The reason for this is that, as far as the rule program block is concerned, alibi(Bryan) does not exist: it is not defined as a fact or in a rule head anywhere. In fact, the bind callback will only be called for Person == 1.

When mixing constraints and rule programs, consider the following requirements:

  • There needs to be at least one corresponding rule head for every possible atom that you wish to bind to a variable.
  • For formula domains, a domain value must appear in some rule head, or it will be excluded from the all the formula's atom's potential values.

Clone this wiki locally