search

SRI-CSL / yices2

The Yices SMT Solver
https://yices.csl.sri.com/
GNU General Public License v3.0
368 stars 46 forks source link

`get-value` on array does not inline function #402

Closed ekiwi closed 2 years ago

ekiwi commented 2 years ago

I have a satisfiable SMT query and I am interested in the value of an array constant. I understand that yices internally models arrays as functions and I don't mind getting a function back from a get-value query. However, currently the answer includes an internal function @fun_3 which is impossible access unless one is calling get-model. It would be great if functions like this could be inlined into the response to a get-value query.

Current response:

((m@0 @fun_3))

Expected response:

(function m@0
 (type (Array (_ BitVec 5) (_ BitVec 8)))
 (default #b10000000))

Ideal response:

((as const (Array (_ BitVec 5) (_ BitVec 8))) #b10000000)

I know that as const is non-standard, however, I am not sure if there is any clear standard on how responses are formulated and using as const would be more similar to how CVC4 and Z3 report the value.

This is the query which can be executed with yices-smt2:

(set-option :produce-models true)
(set-logic QF_ABV)
(declare-fun m@0 () (Array (_ BitVec 5) (_ BitVec 8)))
(declare-fun m_readValue_data_pipe_0@0 () (_ BitVec 8))
(declare-fun _cycles@0 () Bool)
(declare-fun m_readValue_do_rand_r1@0 () Bool)
(declare-fun out_1@0 () (_ BitVec 8))
(define-fun _resetCount@0 () Bool false)
(declare-fun reset@0 () Bool)
(declare-fun writeAddr@0 () (_ BitVec 5))
(declare-fun readAddr@0 () (_ BitVec 5))
(declare-fun in@0 () (_ BitVec 8))
(declare-fun m_readValue_rand_data@0 () (_ BitVec 8))
(define-fun m.readValue.addr@0 () (_ BitVec 5) readAddr@0)
(define-fun m.readValue.data@0 () (_ BitVec 8) (select m@0 m.readValue.addr@0))
(define-fun _cycles_active@0 () Bool (not (bvuge (ite _cycles@0 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun _after_1@0 () Bool (not _cycles_active@0))
(define-fun _GEN_1@0 () Bool true)
(define-fun m_readValue_rand_data.en@0 () Bool m_readValue_do_rand_r1@0)
(define-fun _T@0 () Bool (= readAddr@0 writeAddr@0))
(define-fun _T_2@0 () Bool (not reset@0))
(define-fun _T_3@0 () Bool (not _T@0))
(define-fun out@0 () (_ BitVec 8) (ite m_readValue_do_rand_r1@0 m_readValue_rand_data@0 m_readValue_data_pipe_0@0))
(define-fun _T_4@0 () Bool (= out@0 out_1@0))
(define-fun _T_7@0 () Bool (not _T_4@0))
(define-fun _resetPhase@0 () Bool (not (bvuge (ite _resetCount@0 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun assume@0 () Bool (=> _T_2@0 _T@0))
(define-fun assert@0 () Bool (not (=> (and _T_2@0 _after_1@0) _T_4@0)))
(define-fun _resetActive@0 () Bool (=> _resetPhase@0 reset@0))
(define-fun m.readValue.en@0 () Bool true)
(define-fun m.MPORT.en@0 () Bool true)
(define-fun m.MPORT.addr@0 () (_ BitVec 5) writeAddr@0)
(define-fun m.MPORT.mask@0 () Bool true)
(define-fun m.MPORT.data@0 () (_ BitVec 8) in@0)
(assert assume@0)
(assert _resetActive@0)
(define-fun m@1 () (Array (_ BitVec 5) (_ BitVec 8)) (ite (and m.MPORT.en@0 m.MPORT.mask@0) (store m@0 m.MPORT.addr@0 m.MPORT.data@0) m@0))
(define-fun m_readValue_data_pipe_0@1 () (_ BitVec 8) (ite true m.readValue.data@0 m_readValue_data_pipe_0@0))
(define-fun _cycles@1 () Bool (ite reset@0 false (ite _cycles_active@0 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _cycles@0 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _cycles@0)))
(define-fun m_readValue_do_rand_r1@1 () Bool (not _GEN_1@0))
(define-fun out_1@1 () (_ BitVec 8) in@0)
(define-fun _resetCount@1 () Bool (ite _resetPhase@0 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _resetCount@0 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _resetCount@0))
(declare-fun reset@1 () Bool)
(declare-fun writeAddr@1 () (_ BitVec 5))
(declare-fun readAddr@1 () (_ BitVec 5))
(declare-fun in@1 () (_ BitVec 8))
(declare-fun m_readValue_rand_data@1 () (_ BitVec 8))
(define-fun m.readValue.addr@1 () (_ BitVec 5) readAddr@1)
(define-fun m.readValue.data@1 () (_ BitVec 8) (select m@1 m.readValue.addr@1))
(define-fun _cycles_active@1 () Bool (not (bvuge (ite _cycles@1 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun _after_1@1 () Bool (not _cycles_active@1))
(define-fun _GEN_1@1 () Bool true)
(define-fun m_readValue_rand_data.en@1 () Bool m_readValue_do_rand_r1@1)
(define-fun _T@1 () Bool (= readAddr@1 writeAddr@1))
(define-fun _T_2@1 () Bool (not reset@1))
(define-fun _T_3@1 () Bool (not _T@1))
(define-fun out@1 () (_ BitVec 8) (ite m_readValue_do_rand_r1@1 m_readValue_rand_data@1 m_readValue_data_pipe_0@1))
(define-fun _T_4@1 () Bool (= out@1 out_1@1))
(define-fun _T_7@1 () Bool (not _T_4@1))
(define-fun _resetPhase@1 () Bool (not (bvuge (ite _resetCount@1 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun assume@1 () Bool (=> _T_2@1 _T@1))
(define-fun assert@1 () Bool (not (=> (and _T_2@1 _after_1@1) _T_4@1)))
(define-fun _resetActive@1 () Bool (=> _resetPhase@1 reset@1))
(define-fun m.readValue.en@1 () Bool true)
(define-fun m.MPORT.en@1 () Bool true)
(define-fun m.MPORT.addr@1 () (_ BitVec 5) writeAddr@1)
(define-fun m.MPORT.mask@1 () Bool true)
(define-fun m.MPORT.data@1 () (_ BitVec 8) in@1)
(assert assume@1)
(assert _resetActive@1)
(define-fun m@2 () (Array (_ BitVec 5) (_ BitVec 8)) (ite (and m.MPORT.en@1 m.MPORT.mask@1) (store m@1 m.MPORT.addr@1 m.MPORT.data@1) m@1))
(define-fun m_readValue_data_pipe_0@2 () (_ BitVec 8) (ite true m.readValue.data@1 m_readValue_data_pipe_0@1))
(define-fun _cycles@2 () Bool (ite reset@1 false (ite _cycles_active@1 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _cycles@1 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _cycles@1)))
(define-fun m_readValue_do_rand_r1@2 () Bool (not _GEN_1@1))
(define-fun out_1@2 () (_ BitVec 8) in@1)
(define-fun _resetCount@2 () Bool (ite _resetPhase@1 (= ((_ extract 0 0) (bvadd ((_ zero_extend 1) (ite _resetCount@1 (_ bv1 1) (_ bv0 1))) (_ bv1 2))) (_ bv1 1)) _resetCount@1))
(declare-fun reset@2 () Bool)
(declare-fun writeAddr@2 () (_ BitVec 5))
(declare-fun readAddr@2 () (_ BitVec 5))
(declare-fun in@2 () (_ BitVec 8))
(declare-fun m_readValue_rand_data@2 () (_ BitVec 8))
(define-fun m.readValue.addr@2 () (_ BitVec 5) readAddr@2)
(define-fun m.readValue.data@2 () (_ BitVec 8) (select m@2 m.readValue.addr@2))
(define-fun _cycles_active@2 () Bool (not (bvuge (ite _cycles@2 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun _after_1@2 () Bool (not _cycles_active@2))
(define-fun _GEN_1@2 () Bool true)
(define-fun m_readValue_rand_data.en@2 () Bool m_readValue_do_rand_r1@2)
(define-fun _T@2 () Bool (= readAddr@2 writeAddr@2))
(define-fun _T_2@2 () Bool (not reset@2))
(define-fun _T_3@2 () Bool (not _T@2))
(define-fun out@2 () (_ BitVec 8) (ite m_readValue_do_rand_r1@2 m_readValue_rand_data@2 m_readValue_data_pipe_0@2))
(define-fun _T_4@2 () Bool (= out@2 out_1@2))
(define-fun _T_7@2 () Bool (not _T_4@2))
(define-fun _resetPhase@2 () Bool (not (bvuge (ite _resetCount@2 (_ bv1 1) (_ bv0 1)) (ite true (_ bv1 1) (_ bv0 1)))))
(define-fun assume@2 () Bool (=> _T_2@2 _T@2))
(define-fun assert@2 () Bool (not (=> (and _T_2@2 _after_1@2) _T_4@2)))
(define-fun _resetActive@2 () Bool (=> _resetPhase@2 reset@2))
(define-fun m.readValue.en@2 () Bool true)
(define-fun m.MPORT.en@2 () Bool true)
(define-fun m.MPORT.addr@2 () (_ BitVec 5) writeAddr@2)
(define-fun m.MPORT.mask@2 () Bool true)
(define-fun m.MPORT.data@2 () (_ BitVec 8) in@2)
(assert assume@2)
(assert _resetActive@2)
(assert assert@2)
(check-sat)
(get-value (m@0))
BrunoDutertre commented 2 years ago

Can you try this?

yices-smt2 --smt2-model-format <file>
ekiwi commented 2 years ago

Can you try this?

Thanks! This seems to work.

Would it be possible to make this the default when calling yices as yices-smt2? I know about this option now and will make sure to use it, but I could see others asking similar questions in the future.