zipperposition

zipperposition copied to clipboard

Can't parse TIP v0.3

4

Apparently, the [TIP language](https://tip-org.github.io/) has incorporated SMT-LIB 2.6 changes (https://github.com/tip-org/tools/commit/2995668c6e0d3fb68ec71a494992f74f3c96b877) and is therefore no longer compatible with zipperposition's current parser: ``` $ zipperposition benchmarks/tip2015/list_elem_map.smt2 parse error at at file 'benchmarks/tip2015/list_elem_map.smt2':...

TpmKranz

`./zipperposition.exe -bt --dot /tmp/truc.dot examples/data/length.zf --check -d 5` gets an error in proof checking

c-cube

on: ``` (declare-datatypes () ((List (nil) (cons (head Int) (tail List))))) (define-fun-rec append ((l1 List) (l2 List)) List (match l1 (case nil l2) (case (cons hd tl) (cons hd (append...

c-cube

see some problems that are easy with `--ord=rpo6`: - `pelletier_problems/pb47.zf` (which is normally easy) - `examples/sledgehammer/prob_e_1.p` even when KBO finds a proof, it's weirdly long and convoluted

c-cube

`./zipperposition.exe -o none --dot /tmp/truc.dot -t 10 examples/ARI184=1.p --int-semantic-tauto -p` blocks at step 8. See if we can use a simpler, more correct simplex (funarith?).

c-cube

mix of negation in head and argument positions?

c-cube

not sure what it is exactly.

c-cube

$TPTP/Axioms/CSR003+0.ax contains mixed integers/symbols and I think we're a bit too strict in assuming "integer numeral => type is $int" there. It makes some problems fail with an error (e.g....

c-cube

(longer term) - [ ] make `'a flex_state.key` json serializable - [ ] have a set of configurations as json files, embedded into the binary by build system magic -...

c-cube

Proof checking: Issue with lambda-expressions and sidekick

1

Sidekick currently does not support lambda-expressions or other binders. It seems to me that adding support for them into sidekick is the only clean way to implement the proof checker....

abentkamp