rusty-razor
rusty-razor copied to clipboard
salmans
Razor is a tool for constructing finite models for first-order theories
For example for theory: ``` P('c) ∀ x. (∃ y. (P(x) → Q(x, y))) ``` Print ``` 'c = e#0 P(e#0) Q(e#0, e#1) ``` instead of ``` 'c = e#0...
When possible, replace auto generated element names with user-defined constant names that denote them, if they exist. For example, given theory: ``` P('c); ``` Print ``` 'c = e#0 P('c)...
In `relational/evaluate.rs`, `mapping` in the `info!` call logs attribute debug string but just the name is enough. The fix should evaluate performance implications and whether any transformation on the original...
is it possible to generalize `Rewrite` to `Rewrite` such that `model.rewrites` is also of type `rewrite`? _Originally posted by @salmans in https://github.com/salmans/rusty-razor/pull/104#r519541569_
Currently the bounding a model in the relational implementation has two issues: - It doesn't apply the bound when adding every new observation: it keeps augmenting the new model fully...
With committing to the `relational` implementation and using `basic` as the reference implementation, other implementations of the chase are not needed.
probably don't need chase_all: move it to test modules _Originally posted by @salmans in https://github.com/salmans/rusty-razor/pull/104#r516751352_
The existing implementations (for example relational) clone the parent model at each evaluation step. This would create one extra cloned model and discard the original model. An idea is to...
The strategy would process sequents with fewer branches on right first: - failing sequents (with bottom on right) will fail first - sequents that clone the model will fail last