salmans/rusty-razor

Razor is a tool for constructing finite models for first-order theories

rusty-razor's Issues

rename `PreProcessorEx`

In general, all the traits in the chase module don't have the best names.

Originally posted by @salmans in #104 (comment)

Razor displays colorful models with --no-color

panic when terminal cannot be opened

Hi, I was trying to run the example in the readme, but I'm seeing a panic:

$ git rev-parse --short HEAD
63e11b4
$ env RUST_BACKTRACE=1 cargo run -- solve -i theories/examples/toy.raz
    Finished dev [unoptimized + debuginfo] target(s) in 0.06s
     Running `target/debug/razor solve -i theories/examples/toy.raz`
thread 'main' panicked at 'called `Option::unwrap()` on a `None` value', src/libcore/option.rs:378:21
stack backtrace:
   0: backtrace::backtrace::libunwind::trace
             at /cargo/registry/src/github.com-1ecc6299db9ec823/backtrace-0.3.40/src/backtrace/libunwind.rs:88
   1: backtrace::backtrace::trace_unsynchronized
             at /cargo/registry/src/github.com-1ecc6299db9ec823/backtrace-0.3.40/src/backtrace/mod.rs:66
   2: std::sys_common::backtrace::_print_fmt
             at src/libstd/sys_common/backtrace.rs:77
   3: <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt
             at src/libstd/sys_common/backtrace.rs:61
   4: core::fmt::write
             at src/libcore/fmt/mod.rs:1028
   5: std::io::Write::write_fmt
             at src/libstd/io/mod.rs:1412
   6: std::sys_common::backtrace::_print
             at src/libstd/sys_common/backtrace.rs:65
   7: std::sys_common::backtrace::print
             at src/libstd/sys_common/backtrace.rs:50
   8: std::panicking::default_hook::{{closure}}
             at src/libstd/panicking.rs:188
   9: std::panicking::default_hook
             at src/libstd/panicking.rs:205
  10: std::panicking::rust_panic_with_hook
             at src/libstd/panicking.rs:464
  11: std::panicking::continue_panic_fmt
             at src/libstd/panicking.rs:373
  12: rust_begin_unwind
             at src/libstd/panicking.rs:302
  13: core::panicking::panic_fmt
             at src/libcore/panicking.rs:139
  14: core::panicking::panic
             at src/libcore/panicking.rs:70
  15: core::option::Option<T>::unwrap
             at /rustc/73528e339aae0f17a15ffa49a8ac608f50c6cf14/src/libcore/macros.rs:41
  16: razor::utils::terminal::Terminal::new
             at razor/src/utils/terminal.rs:21
  17: razor::main
             at razor/src/main.rs:133
  18: std::rt::lang_start::{{closure}}
             at /rustc/73528e339aae0f17a15ffa49a8ac608f50c6cf14/src/libstd/rt.rs:61
  19: std::rt::lang_start_internal::{{closure}}
             at src/libstd/rt.rs:48
  20: std::panicking::try::do_call
             at src/libstd/panicking.rs:287
  21: __rust_maybe_catch_panic
             at src/libpanic_unwind/lib.rs:78
  22: std::panicking::try
             at src/libstd/panicking.rs:265
  23: std::panic::catch_unwind
             at src/libstd/panic.rs:396
  24: std::rt::lang_start_internal
             at src/libstd/rt.rs:47
  25: std::rt::lang_start
             at /rustc/73528e339aae0f17a15ffa49a8ac608f50c6cf14/src/libstd/rt.rs:61
  26: main
  27: __libc_start_main
  28: _start
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.

Improve documentation

• Document the internal components and their interfaces.
• Provide a high level description of the model-finding algorithm.

Drop Skolem functions and constants when printing models

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
P(e#0)
Q(e#0, e#1)
f#0(e#0) = e#1

Consider removing `reference` and `batch` implementation

With committing to the relational implementation and using basic as the reference implementation, other implementations of the chase are not needed.

Provide an option for disabling Razor's logo

--no-color will also be used to disable the logo.
@ramsdell

Differential Matching for Chase

Current implementations of the chase in Razor is naive and are meant to serve as a reference implementations. Particularly, all existing implementations evaluate a sequent in all possible environments, containing all possible mappings from free variables in the sequent to all possible elements in the model. This is a huge space that grows exponentially with the number of free variables.

For example, evaluating P(x, y) & Q(x, z) -> R(y, z) in a model with 10 elements involves 10^3 possible environments, where x, y, and z pick elements in the model in each assignment.

But this is a known problem and there are relatively simple solutions to dramatically improve the performance:

Matching

This approach solves a matching problem between the atomic formulae in the body of a sequent and the facts that are already true in the model. The sequent is then evaluated for every solution to the matching problem. Any variable that appears freely in the head of the sequent can pick any element in the model.

For example, consider evaluating the previous sequent in the following model:

Domain: e#0, e#1, ..., e#10
Facts: P(e#0, e#1), P(e#0, e#2), Q(e#0, e#3)

With P(x, y) and Q(z) in the body of the sequent, the matching problem has only two solutions: x -> e#0, y -> e#1, z -> e#3 or x -> e#0, y -> e#2, z -> e#3. This is a huge improvement over the 10^3 choices mentioned before.

Equality: This solution is compatible with the current approach to equational reasoning, that is, identifying equal elements. Notice that in the matching problem equalities in the body of the sequent enforce additional constraints. For example, evaluating P(x, y) & Q(x, z) & x = z -> R(y, z) also requires x to be equal to z in every solution.

Differential Matching

An enhancement to the previous solution involves matching the sequent against unprocessed facts that have been added to the model since the last time the sequent was evaluated. That is, adding new facts after evaluating a sequent would trigger other sequents.

Equality: Differential matching requires a special treatment for equality:

1. A conservative implementation would treat equality as a binary predicate, in pretense of additional sequents that encode equality axioms; i.e., reflectivity, symmetry, transitivity, function substitution (for all functions), and predicate substitution (for all predicates). Equality reasoning by evaluating additional sequents is expected to be expensive (this must be verified).
2. Compatibility of differential matching and the current approach to equality reasoning based on identifying elements should be investigated. The core idea is as follows:

• Disallow a variable to appear in more than one position in the sequent's body. For example, rewrite P(x) & Q(x, y) -> R(y) to P(x) & Q(x0, y) & x = x0 -> R(y).
• When collapsing two elements because of an equality in the head of a sequent, keep track of all consecutive collapses (due to equational reasoning). Next, trigger all sequents with equalities in the body.

Relational Algebra

Razor can take advantage of relational algebra for evaluating sequents in a model. Matching against the model maps to query evaluation and differential matching to differential view-update. Some of the tricks implemented in DataFrog can be applied: https://github.com/frankmcsherry/blog/blob/master/posts/2018-05-19.md

Moving forward

At least three new chase implementations are needed. These implementations are going to be benchmarked against each other and against all existing implementations:

• Matching with equality axioms encoded as sequents
• Matching with identifying equal elements
• Relational algebra (with either equality axioms or identification)

Benchmark Razor against Alloy

1. How does Alloy's bounds translate to Razor's?
2. Maybe the comparison should be done after implementing sorted logic for Razor?

Add an option for reusing existing elements when possible

The core idea is to avoid introducing new elements to the model when possible. Here is an example for the simple case:

P('a);
exists x. P(x);

Razor currently builds the following model for this theory:

Domain: e#0, e#1
Elements: 'a -> e#0, 'sk#0 -> e#1
Facts: P(e#0), P(e#1)

However, it could reuse e#0 (denoting 'a in place of e#1 (denoting the existential quantifier). This would introduce an unnecessary identification between e#0 and e#1, resulting in a model that is not homomorphically minimal:

Domain: e#0
Elements: 'a -> e#0, 'sk#0 -> e#0
Facts: P(e#0)

However, this kind of element reuse often helps avoid constructing infinite models as for the case for the grandpa example.

Pretty print instrumentation of tracing in relational implementation

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 tuple is evaluated lazily or not.

Produce trace information for models

tokio-trace is a promising option.

Create `as_...` methods on `Term` to convert the term to `Var`, `App`, and `Const`

Originally posted by @salmans in #104 (comment)

strategy for evaluating relevant sequents

The existing implementations of StrategyTrait do not take advantage of information about the previously evaluated sequents.

Definitions

Unbalanced Sequent: is a sequent whose body is true in the model evaluated by the chase step but its head is false in the model.

Consider the following example:

(1) P('a);
(2) Q(x) -> R(x);
(3) P(x) -> Q(x);

After evaluating (1), the only unbalanced sequent that should be processed by the consequent chase step is (3).
A more efficient instance of StrategyTrait should skip (2) since it can never be unbalanced after running a chase step on (1).

In general, the evaluation strategy should always schedule (syntactically) relevant sequents. Considering the expensive cost of evaluating sequents in models, this evaluation strategy is expected to dramatically improve performance.

Disadvantage

This approach is inherently in conflict with congruence closure for equality reasoning as unified elements might unbalance sequents that are not syntactically relevant:

(1) P(`a);
(2) Q(`b);
(3) `a = `b;
(4) Q(x) -> R(x);

After evaluating (1) and (2) followed by (3), sequent (4) should be processed, although it is not syntactically relevant to (3).

Due to complications arising from congruence closure for equality reasoning, equality must be evaluated as a unique first-order predicate (namely =) in presence of equality axioms, processed as sequents.

With this disadvantage, it's not clear under what conditions, the suggested solution improves the performance of the chase.

Non-deterministic behavior when running on grandpa.raz

When evaluating sequents in the reference implementation here, the iterator on the underlying HashSet is created non-deterministically. This would change the order by which sequents are instantiated.

• There is another (less frequent) source of non-determinism.
• Changing this behavior to gain deterministic behavior is not worth the performance penalty.

replace documentation hyperlinks with intera-doc linking

also update the minimum Rust version in README

document `show_incomplete` parameter

implement a strategy that prioritizes sequents with fewer branches first

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

Software license

Now that it's not so private anymore, perhaps it's a good idea to think about which one to use.

Add examples to the readme

It's hard to tell what kind of model this tool will generate without any examples in the readme. It would also help to explain which syntax the tool uses (e.g. && vs & vs + vs 'and' etc.)

remove `chase_all`: move it to test modules

probably don't need chase_all: move it to test modules

Originally posted by @salmans in #104 (comment)

Use `Rewrite` for `rewrite` in relational model

is it possible to generalize Rewrite<T> to Rewrite<K, V> such that model.rewrites is also of type rewrite?

Originally posted by @salmans in #104 (comment)

Add examples to the readme

make `pre_process` of `PreProcessorEx` return a `Result` type

... and get rid of panic!.

Consider using LALRPOP

I've been recently contributing to chalk, the traits solver for rustc and they're currently using LALRPOP for their parsing needs. It has a separate file in which you define your grammar, which has a Rust-like syntax and looks almost like an ABNF form for your language. Maybe we can look into it so that you can easily add more tokens and production rules for razor in the future?

Converting theories to geometric form produces duplicate Skolem functions

The transformation should use ToSNF::snf_with and avoid using ToGNF::gnf directly.

Support reading theories form code blocks of markdown files

When passing an input file with .md extension as the input theory, Razor parses all code blocks between ``` for the input theory.

@ramsdell tagging you here for tracking

support comments in the parser

Replace elements with user-defined constants when pretty printing models

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)

or even don't mention e#0

P('c)

Enforce the bounds more accurately on the `relational` implementation

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 at every chase-step.
• It doesn't take the equivalence classes of elements into account when calculating the "size" of the model.

Idea:

• keep track of model rewrites by references to elements (in Rc<RefCell<E>>).
• compute the size of models based on the values of rewrites.
• check the bound before adding every new observation (add the observation to the model if that particular observation doesn't violate the bound)

Originally posted by @salmans in #104 (comment)

Change the precedence and associativity of implication

per conversation with @dandougherty and @ramsdell : implication should take precedence over quantifiers and should be right associative

Accept theories that are piped into the razor through stdin

razor solve without a -i argument reads its input theory directly from the standard input.

@dandougherty @ramsdell

support block comments

Generate structured output

There are some obvious choices:

• JSON
• S-Expression

Avoid unnecessary cloning of the parent model when evaluating

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 clone the original model as many times as possible before extending each branch.

Implement sorts in the core model-finding algorithm

Collecting some thoughts:

• Sorted chase seems to be pretty straight forward
• Sorted chase would dramatically improve performance (restricting the possible ways of instantiating sequents)
• Requires change in the syntax of the parser
• Reasoning about languages with types inherently requires a performant support for sorts

Questions

• Do we want to preserve a non-sorted mode?

panics on hodor-time-loop example

The following theory causes panic:

HoldTheDoor(t) -> Hodor(next(t));

Hodor(t) -> exists tt . HoldTheDoor(tt) & After(t, tt);

next(t0) = t1 -> After(t0, t1);
After(t0, t1) -> (next(t0) = t1) | exists t2 . next(t0) = t2 & After(t2, t1);

// Hold the door moment only happens at 't_hodor
HoldTheDoor(t) -> t = 't_hodor;
Hodor('t_hodor);

error:

thread 'main' panicked at 'called `Option::unwrap()` on a `None` value', libcore/option.rs:355:21
stack backtrace:
   0: std::sys::unix::backtrace::tracing::imp::unwind_backtrace
   1: std::sys_common::backtrace::print
   2: std::panicking::default_hook::{{closure}}
   3: std::panicking::default_hook
   4: std::panicking::rust_panic_with_hook
   5: std::panicking::continue_panic_fmt
   6: rust_begin_unwind
   7: core::panicking::panic_fmt
   8: core::panicking::panic
   9: rusty_razor::chase::impl::reference::Model::record
  10: <core::iter::Map<I, F> as core::iter::iterator::Iterator>::fold
  11: <alloc::vec::Vec<T> as alloc::vec::SpecExtend<T, I>>::from_iter
  12: rusty_razor::chase::impl::reference::Model::record
  13: <core::iter::Map<I, F> as core::iter::iterator::Iterator>::fold
  14: <alloc::vec::Vec<T> as alloc::vec::SpecExtend<T, I>>::from_iter
  15: <rusty_razor::chase::impl::reference::Model as rusty_razor::chase::ModelTrait>::observe
  16: <core::iter::FilterMap<I, F> as core::iter::iterator::Iterator>::next
  17: <alloc::vec::Vec<T> as alloc::vec::SpecExtend<T, I>>::from_iter
  18: <rusty_razor::chase::impl::reference::Evaluator as rusty_razor::chase::EvaluatorTrait<'s, Sel, B>>::evaluate
  19: rusty_razor::chase::solve
  20: razor::main
  21: std::rt::lang_start::{{closure}}
  22: std::panicking::try::do_call
  23: __rust_maybe_catch_panic
  24: std::rt::lang_start_internal
  25: main

Bug introduced by removing Skolem function tables from sequent queries

The bug is introduced when optimizing queries in the head of sequents. Although the optimization might be unsound in a general case, the current transformation to GNF does not guarantee unique Skolem functions for each sequent; so a Skolem table (corresponding to a Skolem function) may be populated by evaluating other sequents, thus is not guaranteed to evaluate to true (full table) when evaluating another sequent. The initial thought relied on uniqueness of Skolem functions that appear in a sequent to guarantee truth (if they are already populated) or falsehood (if they are not).

document razor-for syntax

Support TPTP library

See http://www.tptp.org
The goal is to use the TPTP library as test cases.

A TPTP parser must be developed as a separate project. Consider LALRPOP as an option (#40).

create a rule for converting Razor's syntax to Geolog

This must be done as a separate tool, using Razor's syntactic library.