alt-ergo

alt-ergo copied to clipboard

add a new PSMT2 frontend that directly produces assertions of type Expr.t

1

Current PSMT2 frontend generates a native Alt-Ergo parsed AST that is (re-)typechecked before generating assertions of type `Expr.t`. However, since triggers are now computed in module `Expr`, a better PSMT2...

iguerNL

iguerNL

iguerNL

iguerNL

For this example: ``` (declare-const s Bool) (declare-const a Bool) (declare-const b Bool) (assert (not (= (= s (or a b)) (= (not a) (or (not s) b)) ) )...

iguerNL

Currently, given an example: ``` logic f : int -> int logic g : int, int -> int logic P : int, int, int -> prop axiom a: forall x,...

iguerNL

In particular, this is the case for variables appearing inside hypotheses. As a result, filter_good_triggers removes the triggers provided by the user. For instance, in the example: ``` axiom rounding_operator_1...

iguerNL

iguerNL

Should re-implement the way multi-triggers are computed in `Triggers.ml`. It currently uses `power-set`, which does not scale in some situations

iguerNL

unsound answer on wintersteiger

1

Hi, benchmark wintersteiger/min/min-has-solution-13472.smt2 produces the wrong answer when using the benchmark conversion script from https://gitlab.com/OCamlPro-Iguernlala/Three-Tier-FPA-Benchs/tree/master/translators/fp-smt2-to-why3 I am not sure if its an issue with the translator or alt-ergo as I...

florianschanda