Would it be possible to add generic versions of the following concrete types to smt2parser::visitors similar to how Identifier, Index, and the *Dec types are defined?

• SExpr (generic over Constant, Symbol, Keyword)
• QualIdentifier (generic over Identifier, Sort)
• Command (generic over Symbol, Sort, Keyword, Term)

Made the following types generic over the values they contain:

• SExpr
• Sort
• QualIdentifier
• Term
• Command

Replaced type aliases filling in standard type parameters with default type parameters in the definitions.

Fixes #36

• The charts are similar to Jupyter notebooks.
• Code is (mostly) shared between the tool and the notebook(s).

z3 trace=true proof=true path/to/file.smt2
cargo run --release -p z3tracer -- --plot-all z3.log
# Creates several z3.log.*.png files

Improve renaming::SymbolNormalizer:

• add a configuration object and support the randomization of variables (up to a maximum number of variables per kind, after which indices are just sequential).
• expose the number of distinct variables of each kind after normalization
• update the demo tool smt2bin
• update the tool smt2proxy

Examples:

# Demo tool in this repo:
cargo run --release -p smt2parser -- print --normalize-symbols --max-randomized-symbols 1024 --symbol-randomization-seed 5 path/to/file.smt2

# Proxy in the diem repo:
SMT2PROXY_NORMALIZE_SYMBOLS=true SMT2PROXY_LOG_PATH=logs.smt2 \
SMT2PROXY_MAX_RANDOMIZED_SYMBOLS=1024 SMT2PROXY_SYMBOL_RANDOMIZATION_SEED=1 \
BOOGIE_EXE=`which boogie` Z3_EXE=path/to/target/release/smt2proxy \
cargo run --release -p move-prover -- --cores 1 -d language/diem-framework/modules -d language/move-stdlib/modules language/diem-framework/modules/DiemSystem.move

This allows reusing symbol names after a (push) or a (reset) and is generally more correct in case of name clashes with globals.

Additionally, we now use a different prefix for each symbol kind: "f" for functions, "T" for datatypes, etc.

Enable normalization of symbols on the fly in the SMT2 proxy.

Note:

• Symbols are renamed x0, x1, etc disregarding their kind (type, function name),
• Names are assigned in order (no random shuffle yet).

Assuming that smt2proxy is in the PATH, the proxy can be tested from in the Diem repo like this:

SMT2PROXY_NORMALIZE_SYMBOLS=true SMT2PROXY_LOG_PATH=logs.smt2 BOOGIE_EXE=`which boogie` Z3_EXE=`which smt2proxy` \
cargo run --release -p move-prover -- --cores 1 -d language/diem-framework/modules -d language/move-stdlib/modules language/diem-framework/modules/DiemSystem.move

# Replay logs.
z3 logs.smt2

Note that --cores 1 is important for the logs to be meaningful.

Provide a working implementation of name resolution and name normalization for SMT2 files with the following caveats:

• The old syntax for testers is-Foo is not compatible with name resolution. One needs to replace is-Foo into (_ is Foo) first using the given rewriter renaming::TesterModernizer (see unit tests).
• Error handling is not fully satisfying yet: visitor APIs do not use Result yet and will panic! in case of unknown symbol. (However, this only affects people using the new name-resolution callbacks, not the parsing.)
• The LALR parser will attempt to call some of the new callbacks but proper name resolution requires to use SyntaxBuilder first, then visit the concrete syntax again. See the unit test of the utility type renaming::SymbolNormalizer.

This PR substantially extends the Model abstraction of z3tracer to track dependencies:

• between conflicts and Quantifier Instantiations (QIs)
• between QIs.

Contrary to the algorithm suggested in the Axiom Profiler documentation:

• We do not ignore [push] and [pop] commands and try to account for backtracking in a precise way (e.g. proofs discovered at one point may go out of scope);
• The logs do not tell when equations were discovered (only when they are used). To allow limit backtracking, we try to reconstruct a plausible backtracking level for them using their dependencies.
• We try to model the QI dependencies that caused a conflict. Because conflicts can be seen as progress when trying to prove UNSAT, this could be used to distinguish "useful" QIs.
• We do not do anything special about "rewrite" and "monotonicity" proofs yet. (EDIT: This should be fine. We propagate dependencies for all proof terms already.)

See the main notebook for new charts and some examples.

Explore a new tool to make changes to an SMT2 file. Current features include:

• tagging asserts with names and inserting a call to get-unsat-core
• being able to remove clauses not in the unsat core
• tagging quantified expressions with a QID
• setting the weight of quantified expressions

cargo run -p smt2patch -- --get-unsat-core FILE | z3 -in | tail -n 1 > unsat_core.txt

cargo run -p smt2patch -- --keep-only-clauses "$(cat unsat_core.txt)" -- FILE | z3 -in

cargo run -p smt2patch -- --tag-quantifiers  FILE | z3 trace=true -in  # z3.log now contains quant!N names

cargo run -p smt2patch -- --set-weights quant!0=100 -- FILE

Example of output using --get-unsat-core and --tag-quantifiers:

(set-option :produce-unsat-cores true)
(set-info :smt-lib-version  2.6)
(set-logic ALIA)
(set-info :source  piVC)
(set-info :category  "industrial")
(set-info :status  unsat)
(declare-fun V_9 () Int)
(declare-fun a () (Array Int Int))
(assert (! (let ((?v_0 (and true (>= V_9 0)))) (and (and ?v_0 ?v_0) (and (forall ((?V_7 Int)) (! (=> (and (<= 0 ?V_7) (<= ?V_7 5)) (forall ((?V_8 Int)) (! (let ((?v_1 (store (store a 0 5) 5 7))) (=> (and (<= 0 ?V_8) (<= ?V_8 ?V_7)) (<= (select ?v_1 ?V_8) (select ?v_1 ?V_7)))) :qid quant!0))) :qid quant!1)) (forall ((?V_5 Int)) (! (=> (and (<= 0 ?V_5) (<= ?V_5 5)) (forall ((?V_6 Int)) (! (let ((?v_2 (store (store a 0 1) 5 3))) (=> (and (<= 0 ?V_6) (<= ?V_6 ?V_5)) (<= (select ?v_2 ?V_6) (select ?v_2 ?V_5)))) :qid quant!2))) :qid quant!3))))) :named clause!0))
(check-sat)
(get-unsat-core)
(exit)

Original file:

(set-info :smt-lib-version 2.6)
(set-logic ALIA)
(set-info :source |piVC|)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun V_9 () Int)
(declare-fun a () (Array Int Int))
(assert (let ((?v_0 (and true (>= V_9 0)))) (and (and ?v_0 ?v_0) (and (forall ((?V_7 Int)) (=> (and (<= 0 ?V_7) (<= ?V_7 5)) (forall ((?V_8 Int)) (let ((?v_1 (store (store a 0 5) 5 7))) (=> (and (<= 0 ?V_8) (<= ?V_8 ?V_7)) (<= (select ?v_1 ?V_8) (select ?v_1 ?V_7))))))) (forall ((?V_5 Int)) (=> (and (<= 0 ?V_5) (<= ?V_5 5)) (forall ((?V_6 Int)) (let ((?v_2 (store (store a 0 1) 5 3))) (=> (and (<= 0 ?V_6) (<= ?V_6 ?V_5)) (<= (select ?v_2 ?V_6) (select ?v_2 ?V_5)))))))))))
(check-sat)
(exit)

• make parser options ParserConfig accessible from CLI tool and existing library API
• revert to not skipping incorrect lines by default in Model::process
• make version check the default at the parser level
• add option to skip version check
• fix --help: Work around annoying bug with structopt(flatten)
• fix endless loop on truncated files when skipping incorrect lines

This PR contains two commits:

• Add a ParserConfig which currently only contains one field: ignore_invalid_lines. When this boolean is true, the parser will ignore lines which don't start with '['.
• Replace field instantiation_data_len with instantiation_timestamps in struct TermData to store timestamps information. And the length of the instantiation_timestamps is used to sort the terms in most_instantiated_terms. The notebooks have been updated too.

Hi,

We've just found a bug in your parser related to the get-value command. The SMT-LIB syntax for get-value is

(get-value ( <terms>+ ))

(cf. SMT-LIB 2.6 page 45).

Your rule in get-value in parser.rs is missing the inner parentheses:

    command ::= LeftParen GetValue terms(xs) RightParen { extra.0.visit_get_value(xs)? }

It should be like this instead:

    command ::= LeftParen GetValue LeftParen terms(xs) RightParen RightParen { extra.0.visit_get_value(xs)? }

Thanks (and thanks for producing this parser!).

Bruno

Hi, I wanted to take a crack at getting theory parsing working to fix https://github.com/facebookincubator/smt2utils/issues/15.

Before I went to the trouble of implementing all the parser rules and concrete syntax types, I wanted to validate the approach I'm taking.

Basically it amounts to:

• Parser returns an enum ParseResult which could be either a Command or a Theory. (currently, no modesetting is done, we rely on upstream consumers like CommandStream, to provide errors if the parser returns an unexpected result)
• Extend SmtVisitor with TheoryVisitor. I'm not sure I like this because I imagine there are a lot of tools that will only operate on Commands and not on Theorys but it seemed the least invasive choice. I would welcome some guidance on this point.

It should not be too hard to add support for theory and logic definitions. Two options:

1. add callbacks for "fake" commands: (theory ..) and (logic ..)
2. modify the Pomelo parser to be multimodal. ~~This can be done by accepting a first token Mode(m) that sets the mode.~~ (EDIT: not needed)

https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf