Models, rebased (OCamlPro#530)

Add model generation to alt-ergo

* examples and initial draft report

* attempt to fix CI: Seq dep missing to compile lib_usage test file

* change version to models

* models generation: add some examples

* parent f3ad875
author OCamlPro-mattiasdrp <mattias@ocamlpro.com> 1591793503 +0200
committer OCamlPro-mattiasdrp <mattias@ocamlpro.com> 1593523267 +0200

Rebase from next

* check sat handled on the lowest possible level, need to work on unsat instead of valid as a result

* first prototype for models in Why3, lots of hard coded stuff that needs to be well understood before making it work for every case

* Change interpretation option, use mdl-formatter to compute but not print model and interpretation

* Style check

* Move the printing of counterexample from uf.ml to models.ml

* Prototype of printer for records in smt format

* Directly use rep of bool value for counterexamples

* fix destr list rev

* Clean choose_adequate_model for boolean constant

* Add `fast` option that disable greedier instantiation phase

* remove greedier and get_fast in fun_sat

* Prototype to output constraint as model if output is set to why3

* Remove `why3-counter-example` option, use `-o why3` instead

* Code cleaning and addition of functions printing with cascade of ite

* fix compatibility for ocaml version < 4.07

* Fix printing of some type in smtlib2 output format

* Add an example which test some ce

* Add support for record constuctor use in model

* Add option dummy-value for interpretation that output _ instead of dummy fresh value when no value is computed

* Fix pp_term and assert output prototype

* Add factorisation in ite when values or the same

* reeplace dummy_value with use_underscore option

* remove  fast option, use `--instantiation-heuristic=normal` instead

* Copy print expr code in models for better management of named expr

* [models] add case-split on internal bool terms

Useful when/if the SAT don't see/assign internal bool expression and/or
SAT assignement is not propagated to theories
(eg. because of CDCL(Tableaux) filtering)

* Type Expr.view should remain "private"

* fix intendation

* Expr.get_infos returns the view: to avoid uesless tuple allocation

* refactor the way model is output from fun_sat

it now goes through Theory instead of calling directly Uf

* Rename interpretation option values to None First Last and Every

* Fix interpretation_timelimit initialisation

* auto set option "fm_cross_limit = -1" (ie. infinity) if models-gen is set.

* Fix use_underscore_interpretation option

* Remove deadcode from models and mv models.ml in frontend

* Add some  documentation in options.ml for type model, instanciation_heuristic  and interpretation

* Fix no-term-like-pp option comment

* Fix model options

* remove unused models-generation code (all, complete and default models)

* remove functions related to old model

* clean unused code

* fix linter

* Fix frontend output in case of  timeout

* Clean models, remove old native output, and remove ref for records

* Move profile module from Models module to structures

* Fix printing of constraints in why3 output  when constraints are functions and not  just constants

* Fix declare-fun command in models

* Uses printer instead of format in models comments

* Better command line arguments

* Style fix

* Adding simple model option

* Rebase artifacts

* Putting model option in the right option list

* Poetry

* Fix parse command

* Poetry

* Adding a proper exception for unsupported features and removing 'at_exit' instruction

* Adding doc & some poetry

* Consistent inlining annotations

* Not updating instantiation heuristic in model option

* New name for Profile module

* Fix SMTLIB2 printer

* Poetry

* Rebase artifacts

Co-authored-by: OCamlPro-mattiasdrp <mattias@ocamlpro.com>
Co-authored-by: OriginLabs-Iguernlala <mohamed.iguernlala@origin-labs.com>
Co-authored-by: Albin Coquereau <albin.coquereau@ocamlpro.com>
Co-authored-by: Albin Coquereau <pro.acoquer@protonmail.com>
Co-authored-by: Albin Coquereau <6535385+ACoquereau@users.noreply.github.com>

docs/sphinx_docs/Input_file_formats/Native/00_summary.md

@@ -33,8 +33,9 @@ Reserved keywords are the following.
 
 The list of all reserved keywords, in alphabetical order, is:
 ```
-ac, and, axiom, bitv, bool, case_split, check, cut, distinct, else, end, exists, extends,
-false, forall, function, goal, if, in, int, let, logic, not, xor, predicate, prop, 
-real, rewriting, then, theory, true, type, unit, void, match, with, of
+ac, and, axiom, bitv, bool, case_split, check, check_sat, chevk_valid, cut,
+distinct, else, end, exists, extends, false, forall, function, goal, if, in,
+int, let, logic, not, xor, predicate, prop, real, rewriting, then, theory,
+true, type, unit, void, match, with, of
 ```
 Note that preludes (additional theories which may be loaded) may reserve more keywords.

docs/sphinx_docs/Input_file_formats/Native/04_setting_goals.md

@@ -49,4 +49,45 @@ In other word, `cut` and `check` allow to test if intermediate goals can be prov
 <check_declaration> ::= 'check' <expr>
 <cut_declaration>   ::= 'cut' <expr>
 ```
-
+
+## `check_valid`
+
+This keyword is an alias for `goal`.
+
+## `check_sat`
+
+This keyword is used just like `goal` and `check_valid`, but it describes a property that alt-ergo will
+try to prove invalid. This keywork has been introduced in the version 2.5.0 as a part of the model
+instanciation, and in this version `alt-ergo` never returns `SAT`, but `unknown` instead.
+
+### Example
+
+test.ae
+```
+logic x, y : int
+
+check_sat g: x = y
+```
+
+```
+$ alt-ergo test.ae --model
+
+unknown
+
+(model
+
+ ; Functions
+
+ ; Constants
+
+(define-fun x () int 0)
+
+(define-fun y () int 0)
+
+ ; Arrays not yet supported
+
+
+)
+File "test.ae", line 3, characters 14-19: I don't know (0.0030) (2 steps) (goal g)
+
+```

docs/sphinx_docs/Usage/index.md

@@ -26,6 +26,24 @@ Alt-Ergo supports file extensions:
 
 See the [Input section] for more information about the format of the input files
 
+### Generating models
+Since 2.5.0, Alt-Ergo also generates models in the case it concludes on the satisfiability of
+the formula.
+There is two ways to activate model generation:
+
+- with the `--model` option;
+
+- `with the --interpretation=VALUE`, where VALUE can be equal to:
+  * "none", and alt-ergo will not generate models (by default);
+  * "first", and alt-ergo will output the first model it finds;
+  * "every", alt alt-ergo will compute a model before each decision
+  * "last", and alt-ergo will output the last model it computes before returning 'unknown'.
+  Note that this mode only works with the option `--sat-solver tableaux`.
+
+NB: the `--model` option is equivalent to `--interpretation every --sat-solver tableaux`.
+
+The default model format is the SMT format.
+
 ### Output
 The results of an Alt-ergo's execution have the following form :
 ```

examples/smt2/arith/arith1.ae

@@ -0,0 +1,7 @@
+logic x : int
+logic f : int -> int
+
+(*axiom A1: forall x:int. f(x) < 100*)
+
+check_sat g :
+  x <= 42 and x >= 0 and f(x) >= 42 and x + f(x) = 50

examples/smt2/arith/arith1.smt2

@@ -0,0 +1,5 @@
+(set-logic ALL)
+(declare-const x Int)
+(assert (<= x 42))
+(check-sat)
+(get-model)

examples/smt2/arith/arith2.smt2

@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-const x Int)
+(declare-const y Int)
+(assert (and (<= x 42) (>= x 0) (>= y 42) (= (+ x y) 50)))
+(check-sat)
+(get-model)

examples/smt2/array/array1.smt2

@@ -0,0 +1,8 @@
+(declare-const x Int)
+(declare-const y Int)
+(declare-const a1 (Array Int Int))
+(declare-const a2 (Array Int Int))
+(assert (= (select a1 x) x))
+(assert (= (store a1 x y) a1))
+(check-sat)
+(get-model)

examples/smt2/bool/bool1.smt2

@@ -0,0 +1,15 @@
+(set-logic QF_UF)
+; (set-option :produce-models true) ; enable model generation
+(declare-const p Bool)
+(declare-const q Bool)
+; (declare-const t Int)
+(define-fun nq () Bool q)
+(assert (=> (not p) (not nq)))
+(check-sat)
+(get-model)
+(get-assignment)
+(assert q)
+(check-sat)
+(get-model)
+(get-assignment)
+(exit)

examples/smt2/bool/bool2.ae

@@ -0,0 +1,10 @@
+logic x: bool
+logic y: bool
+goal ga1: x and y
+goal ga2: x and not x
+goal go1: x or y
+goal go2: x or not x
+check_sat ga1: x and y
+check_sat ga2: x and not x
+check_sat go1: x or y
+check_sat go2: x or not x

examples/smt2/bool/bool2.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_UF)
+(declare-const x Bool)
+(declare-const y Bool)
+(assert (or x (not x)))
+(check-sat)
+(get-model)
+(get-assignment)

examples/smt2/complete.smt2

@@ -0,0 +1,93 @@
+(set-logic ALL)
+(set-option :produce-models true)
+
+;; Constants
+;; Bools
+(declare-const b Bool)
+(assert b)
+(check-sat)
+
+;; Ints
+(declare-const i Int)
+(assert (> i 0))
+(check-sat)
+
+;; Reals
+(declare-const r Real)
+(assert (> r 0.0))
+(check-sat)
+
+;; UF
+;; Bools
+(declare-const fb_cst Bool)
+(declare-const fb_cst2 Bool)
+(declare-fun fb (Bool) Bool)
+(declare-fun fb_b (Bool Bool) Bool)
+(assert (and (fb fb_cst) (fb_b fb_cst fb_cst2)))
+(check-sat)
+
+;; Ints
+(declare-const fi_cst Int)
+(declare-fun fi (Int) Bool)
+(declare-fun fii (Int) Int)
+(declare-fun fii_i (Int Int) Int)
+(assert (and (fi fi_cst) (= (fii fi_cst) 0) (= (fii_i 1 2) fi_cst)))  
+(check-sat)
+
+;; Reals
+(declare-const fr_cst Real)
+(declare-fun fr (Real) Bool)
+(declare-fun frr (Real) Real)
+(declare-fun frr_r (Real Real) Real)
+(assert (and (fr fr_cst) (= (frr fr_cst) 1.0) (= (frr_r 1.0 2.0) fr_cst)))
+(check-sat)
+
+;; Sorts
+(declare-sort S0 0)
+(declare-const sa S0)
+(declare-const sb S0)
+(assert (= sa sb))
+(check-sat)
+
+(declare-sort S1 1)
+(declare-const s1a (S1 S0))
+(declare-const s1b (S1 S0))
+(assert (= s1a s1b))
+(check-sat)
+
+;; Arrays
+(declare-const a (Array Int Int))
+(assert (= a (store a 1 1)))
+(assert (= (select a 1) 1))
+
+(declare-const ai_cst Int)
+(define-fun ai () (Array Int Int) (store a ai_cst 1))
+(assert (= (select ai ai_cst) 1))
+(check-sat)
+(get-model)
+
+;; Sums
+(declare-datatype s ((A) (B) (C)))
+(declare-const s_cst s)
+(assert (or (= s_cst A) (= s_cst B)))
+(check-sat)
+(get-model)
+
+;; Records
+(declare-datatype r ((mk_r (r0 Int) (r1  Int))))
+(declare-const r_cst r)
+(assert (> (r0 r_cst) 1))
+(check-sat)
+
+(define-fun r_fun () r (mk_r 1 2))
+(assert (= (r1 r_fun) 2))
+(check-sat)
+(get-model)
+
+;; Adts
+(declare-datatype IntList ((Cons (hd Int) (tl IntList)) (Nil)))
+(declare-const l_cst IntList)
+; not yet supported
+;(assert (= (hd l_cst) 1))
+;(assert (= l_cst Nil))
+(check-sat)