UF models in MCSAT

[dddejan]

Currently there is no model created in MCSAT for uninterpreted functions.

[dddejan]

I started working on this and got some basic models running. It seems to be different from the default Yices behaviour, so I might change it. For example

dejan@surface:~/workspace/yices2-nl$ ./build/x86_64-unknown-linux-gnu-debug/bin/yices_smt2 ./uf-model.smt2 
sat
(= z0 0)
(= x1 0)
(= y0 0)
(= x2 1)
(= x0 0)
(= f @fun_5)
(function @fun_5
 (type (-> s s))
 (= (@fun_5 0) 1)
 (= (@fun_5 1) 0))
dejan@surface:~/workspace/yices2-nl$ ./build/x86_64-unknown-linux-gnu-debug/bin/yices_smt2 ./uf-model-uflra.smt2
sat
(= x1 @const_1)
(= z0 @const_1)
(= y0 @const_5)
(= x2 @const_3)
(= x0 @const_1)
(= f @fun_9)
(function @fun_9
 (type (-> s s))
 (= (@fun_9 @const_1) @const_2)
 (= (@fun_9 @const_3) @const_4))

The first one is from MCSAT, the second one is from default Yices2. @BrunoDutertre, do you prefer models with "constants", i.e. the second way? The way I started constructing them is commit 1a68f0d.