Regarding Statics

[AnkitMU]

How to get Statics of a model?

[pruemmer]

Could you be more specific, what kind of information about models would you like to query?

[AnkitMU]

like total-time ?

[pruemmer]

There are several options to get those kinds of statistics:

+logo -logging=counters -logging=stats

[AnkitMU]

This is my sample smt.2 file foe which im trying to get the total time .

(set-logic ALL) (set-option :produce-models true)

(declare-fun first_name (Int) String) (declare-fun last_name (Int) String) (declare-fun email (Int) String) (declare-fun address (Int) String) (declare-fun Account_number (Int) Int) (define-fun Person ((o Int)) Bool true)

(assert (forall ((o Int)) (=> (Person o) (and (> (str.len (first_name o)) 5) (str.in_re (first_name o) (re.* (re.range "a" "z"))) ) )) )

(assert (forall ((o Int)) (=> (Person o) (and (> (str.len (last_name o)) 5) (str.in_re (last_name o) (re.* (re.union (re.range "A" "Z") (re.range "a" "z")))) ) )) )

(assert (forall ((o Int)) (=> (Person o) (not (= (first_name o) (last_name o))) )) )

(assert (forall ((o Int)) (=> (Person o) (= (email o) (str.++ (first_name o) "." (last_name o) "@mu.ie")) )) )

(assert (forall ((o Int)) (=> (Person o) (str.suffixof "mu.ie" (email o)) )) )

(assert (forall ((o Int)) (=> (Person o) (and (<= (Account_number o) 9999999999) (>= (Account_number o) 1000000000) ) )) )

(assert (exists ((o Int)) (Person o))) (check-sat) (get-value ((first_name 1)(last_name 1)(email 1)(Account_number 1)))

when I run the above file as ./ostrich file.smt2 -logging=stats it is not giving me anything. Loading file.smt2 ...

Loading OSTRICH 1.3, a solver for string constraints (c) Matthew Hague, Denghang Hu, Philipp Rümmer, 2018-2023 With contributions by Riccardo De Masellis, Zhilei Han, Oliver Markgraf. For more information, see https://github.com/uuverifiers/ostrich

Warning: get-value is only supported in incremental mode (option +incremental), ignoring it Preprocessing ... Proving ...

[pruemmer]

Thanks for the example; indeed, the provided options did not work correctly in combination with the incremental mode, +incremental. I have fixed this now in the newest Ostrich version.