formula.smt2

(set-info :smt-lib-version 2.6)
(set-logic QF_BVFP)
(set-info :source |
Generated by the tool Ultimate Automizer [1,2] which implements 
an automata theoretic approach [3] to software verification.

This SMT script belongs to a set of SMT scripts that was generated by 
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2017 [5,6].

This script might _not_ contain all SMT commands that are used by 
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.

2017-05-01, Matthias Heizmann ([email protected])


[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus, 
Alexander Nutz, Betim Musa, Claus Schätzle, Christian Schilling, 
Frank Schüssele, Andreas Podelski:
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare 
Automata - (Competition Contribution). TACAS (2) 2017: 394-398
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model 
Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Software Verification with Validation of Results - 
(Report on SV-COMP 2017). TACAS (2) 2017: 331-349
[6] https://sv-comp.sosy-lab.org/2017/
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun v_SqrtR_~xn~4_2_const_1851013811 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~xnp1~4_2_const_1579108604 () (_ FloatingPoint 11 53))
(declare-fun v_~_EPS_2_const_559985957 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~lsup~4_2_const_-1813226745 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~cond~4_4_const_-1357618322 () (_ BitVec 32))
(declare-fun v_SqrtR_~Input_2_const_1153083841 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~xn~4_3_const_1851013820 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~residu~4_2_const_8319327 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~linf~4_2_const_-1234996430 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~cond~4_3_const_-1357618321 () (_ BitVec 32))
(declare-fun v_SqrtR_~i~4_2_const_-1484952015 () (_ BitVec 32))
(declare-fun v_SqrtR_~i~4_3_const_-1484952016 () (_ BitVec 32))
(assert (let ((v_SqrtR_~xn~4_2 v_SqrtR_~xn~4_2_const_1851013811) (v_SqrtR_~xnp1~4_2 v_SqrtR_~xnp1~4_2_const_1579108604) (v_~_EPS_2 v_~_EPS_2_const_559985957) (v_SqrtR_~lsup~4_2 v_SqrtR_~lsup~4_2_const_-1813226745) (v_SqrtR_~cond~4_4 v_SqrtR_~cond~4_4_const_-1357618322) (v_SqrtR_~Input_2 v_SqrtR_~Input_2_const_1153083841) (v_SqrtR_~xn~4_3 v_SqrtR_~xn~4_3_const_1851013820) (v_SqrtR_~residu~4_2 v_SqrtR_~residu~4_2_const_8319327) (v_SqrtR_~linf~4_2 v_SqrtR_~linf~4_2_const_-1234996430) (v_SqrtR_~cond~4_3 v_SqrtR_~cond~4_3_const_-1357618321) (v_SqrtR_~i~4_2 v_SqrtR_~i~4_2_const_-1484952015) (v_SqrtR_~i~4_3 v_SqrtR_~i~4_3_const_-1484952016)) (and (not (= v_SqrtR_~cond~4_4 (_ bv0 32))) (= v_SqrtR_~xnp1~4_2 (fp.div RNE (fp.mul RNE v_SqrtR_~xn~4_3 (fp.add RNE ((_ to_fp 11 53) RNE 15.0) (fp.mul RNE (fp.mul RNE (fp.mul RNE v_SqrtR_~Input_2 v_SqrtR_~xn~4_3) v_SqrtR_~xn~4_3) (fp.add RNE (fp.neg ((_ to_fp 11 53) RNE 10.0)) (fp.mul RNE (fp.mul RNE (fp.mul RNE ((_ to_fp 11 53) RNE 3.0) v_SqrtR_~Input_2) v_SqrtR_~xn~4_3) v_SqrtR_~xn~4_3))))) ((_ to_fp 11 53) RNE 8.0))) (= v_SqrtR_~residu~4_2 (fp.mul RNE ((_ to_fp 11 53) RNE 2.0) (fp.sub RNE v_SqrtR_~xnp1~4_2 v_SqrtR_~xn~4_3))) (= v_SqrtR_~xn~4_2 v_SqrtR_~xnp1~4_2) (= v_SqrtR_~lsup~4_2 (fp.mul RNE v_~_EPS_2 (fp.add RNE v_SqrtR_~xn~4_2 v_SqrtR_~xnp1~4_2))) (= v_SqrtR_~linf~4_2 (fp.neg v_SqrtR_~lsup~4_2)) (= v_SqrtR_~cond~4_3 (ite (or (fp.gt v_SqrtR_~residu~4_2 v_SqrtR_~lsup~4_2) (fp.lt v_SqrtR_~residu~4_2 v_SqrtR_~linf~4_2)) (_ bv1 32) (_ bv0 32))) (= (bvadd v_SqrtR_~i~4_2 (_ bv4294967295 32)) v_SqrtR_~i~4_3))))
(check-sat)
(exit)

main.cpp

#include <z3++.h>
#include <iostream>

void construct_model_fast(z3::context& c, z3::model& new_model, z3::expr_vector& assignments){
    for (z3::expr assignment : assignments){
        z3::func_decl lhs = assignment.arg(0).decl();
        z3::expr rhs = assignment.arg(1);
        new_model.add_const_interp(lhs, rhs);
    }
}

/*void construct_model_slow(z3::context& c, z3::model& new_model, z3::expr_vector& assignments){
    z3::solver s(c);

    for (z3::expr assignment : assignments){
        s.add(assignment);
    }
    s.check();
    new_model = s.get_model();
}*/


int main(int argc, char **argv)
{
    const char* constraintsFile = argv[1];
    const char* modelFile = argv[2];

    z3::context ctx;
    
    z3::expr_vector constraints = ctx.parse_file(constraintsFile);
    z3::expr constraint = z3::mk_and(constraints);
    
    z3::expr_vector assignments = ctx.parse_file(modelFile);
    assert(assignments.size() == 1);
    z3::expr topAnd = *assignments.begin();

    z3::expr_vector equalities(ctx);
    for (unsigned i = 0; i < topAnd.num_args(); ++i) {
        z3::expr equality = topAnd.arg(i);
        equalities.push_back(equality);
    }

    z3::model m(ctx);
    construct_model_fast(ctx, m, equalities);

    std::cout << "Evaluation: " << m.eval(constraint) << std::endl;
    return 0;
}

model.smt2

; 
(set-info :status sat)
(declare-fun v_SqrtR_~i~4_3_const_-1484952016 () (_ BitVec 32))
(declare-fun v_SqrtR_~cond~4_3_const_-1357618321 () (_ BitVec 32))
(declare-fun v_SqrtR_~residu~4_2_const_8319327 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~xnp1~4_2_const_1579108604 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~linf~4_2_const_-1234996430 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~xn~4_3_const_1851013820 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~lsup~4_2_const_-1813226745 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~xn~4_2_const_1851013811 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~Input_2_const_1153083841 () (_ FloatingPoint 11 53))
(declare-fun v_SqrtR_~i~4_2_const_-1484952015 () (_ BitVec 32))
(declare-fun v_SqrtR_~cond~4_4_const_-1357618322 () (_ BitVec 32))
(declare-fun v_~_EPS_2_const_559985957 () (_ FloatingPoint 11 53))
(assert
 (and (= v_~_EPS_2_const_559985957 (fp #b0 #b00000000000 #xc000000000009)) (= v_SqrtR_~cond~4_4_const_-1357618322 (_ bv458751 32)) (= v_SqrtR_~i~4_2_const_-1484952015 (_ bv0 32)) (= v_SqrtR_~Input_2_const_1153083841 (fp #b0 #b01010111111 #xfffffffff89ff)) (= v_SqrtR_~xn~4_2_const_1851013811 (_ NaN 11 53)) (= v_SqrtR_~lsup~4_2_const_-1813226745 (_ NaN 11 53)) (= v_SqrtR_~xn~4_3_const_1851013820 (_ NaN 11 53)) (= v_SqrtR_~linf~4_2_const_-1234996430 (_ NaN 11 53)) (= v_SqrtR_~xnp1~4_2_const_1579108604 (_ NaN 11 53)) (= v_SqrtR_~residu~4_2_const_8319327 (_ NaN 11 53)) (= v_SqrtR_~cond~4_3_const_-1357618321 (_ bv0 32)) (= v_SqrtR_~i~4_3_const_-1484952016 (_ bv4294967295 32))))
(check-sat)