Models, rebased

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)