### 1 unstable release

0.1.0 | Jan 3, 2020 |
---|

#**15** in #theorem-proving

**MIT**license

385KB

7.5K
SLoC

# rusty-razor

Rusty Razor is a tool for constructing finite models for first-order theories. The model-finding algorithm is inspired
by the chase for database systems. Given a first-order theory,
Razor constructs a set of *homomorphically minimal* models for the theory.

Check out Razor's documentation for more information about the project and introductory examples.

## Build

rusty-razor is written in Rust, so you will need Rust 1.48.0 or newer to compile it. To build rusty-razor:

`git`` clone https://github.com/salmans/rusty-razor.git`
`cd`` rusty-razor`
`cargo`` build`` --`release

This puts rusty-razor's executable in

.`/target/release`

## Run

`solve`

`solve`

Use the

command to find models for a theory written in an `solve`

file:`<``input``>`

`razor solve ``-`i `<`input`>`

The

parameter limits the number of models to construct:`--count`

`razor solve ``-`i `<`input`>` `-``-`count `<`number`>`

#### Bounded Model-Finding

Unlike conventional model-finders such as Alloy, Razor doesn't require the user to provide a bound on the size of the models that it constructs. However, Razor may never terminate when running on theories with non-finite models -- it can be shown that a run of Razor on an unsatisfiable theory (i.e., a theory with no models) is guaranteed to terminate (although it might take a very very long time).This is a direct consequence of semi-decidability of first-order logic.

To guarantee termination, limit the size of the resulting models by the number of their elements using the

option with a value for the `--bound`

parameter:`domain`

`razor solve ``-`i `<`input`>` `-``-`bound domain`=``<`number`>`

#### Model-Finding Scheduler

Use the

option to choose how Razor processes search branches. The `--scheduler`

scheduler (the default scheduler)
schedules new branches last and is a more suitable option for processing theories with few small satisfying models.
The `fifo`

scheduler schedules new branches first, and is more suitable for processing theories with many large models.`lifo`

`razor solve ``-`i `<`input`>` `-``-`scheduler `<`fifo`/`lifo`>`

## Toy Example

Consider the following example:

`//` All cats love all toys:
forall c`,` t `.` `(`Cat`(`c`)` and Toy`(`t`)` implies Loves`(`c`,` t`)``)``;`
`//` All squishies are toys:
forall s `.` `(`Squishy`(`s`)` implies Toy`(`s`)``)``;`
Cat`(``'duchess``)``;` `//` Duchess is a cat
Squishy`(``'ducky``)``;` `//` Ducky is a squishy

You can download the example file here and run the

command-line tool on it:`razor`

`razor solve ``-`i theories`/`examples`/`toy`.`raz

Razor returns only one model with

and `e #0`

`e``#``1`

as elements that denote `'duchess`

and
`'ducky`

respectively. The facts `Cat``(`e`#``0``)`

, `Squishy``(`e`#``1``)`

, and `Toy``(`e`#``1``)`

in the model
are directly forced by the last two formula in the input theory. The fact `Loves``(`e`#``0``,` e`#``1``)`

is deduced by Razor:`Domain``:` e`#``0``,` e`#``1`
Elements`:` `'duchess` `->` e`#``0``,` `'ducky` `->` e`#``1`
Facts`:` Cat`(`e`#``0``)``,` Loves`(`e`#``0``,` e`#``1``)``,` Squishy`(`e`#``1``)``,` Toy`(`e`#``1``)`

Razor's documentation describes the syntax of Razor's input and contains more examples.

#### Dependencies

~8MB

~152K SLoC