z3 - Converting different widths of floating-point numbers -

-

i want compare 2 different widths of floating-point numbers giving assert z3. example, want compare between ieee 32-bit , ieee 64-bit floating-point number.

my try shown follows: 

(set-logic qf_fpa) (set-option :produce-models true) (declare-fun x_64 () (_ fp 11 53)) (declare-fun x_32 () (_ fp 8 24)) (assert (== ((_ asfloat 11 53) roundnearesttiestoeven x_64 ) x_64)) (check-sat)

but got error message:

(error "line 5 column 59: sort mismatch")

what correct way compare 32-bit , 64-bit number?

the z3 version using 4.3.1 (linux version).

in general, these conversions non-trivial, e.g., when converting 64-bit down 32-bit precision may lost. why conversion functions take rounding mode. smt standard floating-point numbers contain conversion functions of following type:

; floating point sort ((_ to_fp eb sb) roundingmode (_ floatingpoint m n) (_ floatingpoint eb sb))

so, correct way convert between floating-point numbers use to_fp function. [previously, asfloat function served purpose well; don't error using latest unstable version of z3 when using it.] full example this:

(set-logic qf_fpa) (set-option :produce-models true) (declare-fun x_64 () (_ fp 11 53)) (declare-fun x_32 () (_ fp 8 24)) (assert (== ((_ to_fp 11 53) roundnearesttiestoeven x_32) x_64)) (check-sat)

which z3 (latest unstable) accepts without errors , solves instantly. alternatively, think of casting x_64 down 32 bit, in case assertion this:

(assert (== ((_ to_fp 8 24) roundnearesttiestoeven x_64) x_32))

Comments

Post a Comment

Popular posts from this blog

Change the color of an oval at click in Java AWT -

-
i have draw ovals in java, , @ click change color. beginning tried change color after 20 ms, doesn't work. my code is: public class mycomponentnew extends frame { public graphics2d g2d; public mycomponentnew(string title) { super(title); setsize(400, 550); } @override public void paint(graphics g) { this.g2d = (graphics2d) g; this.g2d.setcolor(color.red); this.g2d.filloval(10, 55, 50, 100); } public void changecolor () { this.g2d.setcolor(color.blue); this.g2d.filloval(10, 55, 50, 100); } } and in class main method have: mycomponentnew m; m = new mycomponentnew("fereastra cu baloane"); m.setvisible(true); m.addwindowlistener(new windowadapter() { @override public void windowclosing(windowevent we) { system.exit(0); } }); try { thread.sleep(20); } catch(interruptedexception e) {} m.changecolor(); the color of oval remains red. ...
Read more

c# - Unity IoC Lifetime per HttpRequest for UserStore -

-
i'm trying clean default implementation of accountcontroller.cs comes out of box in new mvc5/owin security implementation. have modified constructor this: private usermanager<applicationuser> usermanager; public accountcontroller(usermanager<applicationuser> usermanager) { this.usermanager = usermanager; } also, have created lifetime manager unity looks this: public class httpcontextlifetimemanager<t> : lifetimemanager, idisposable { private httpcontextbase _context = null; public httpcontextlifetimemanager() { _context = new httpcontextwrapper(httpcontext.current); } public httpcontextlifetimemanager(httpcontextbase context) { if (context == null) throw new argumentnullexception("context"); _context = context; } public void dispose() { this.removevalue(); } public override object get...
Read more

I am trying to solve the error message 'incompatible ranks 0 and 1 in assignment' in a fortran 95 program. -

-
i writing program in fortran find velocity of parachuting person in relation time. keep getting error can't fix. new programming , appreciated. the error is v(i+1)=v(i)+[32-((c*v(i)*v(i))/m)]*(h) 1 error: incompatible ranks 0 , 1 in assignment @ (1) and program is program para integer :: real :: v(11) !velocity real :: q !initial velocity real :: h !time step real :: c !drag coefficient real :: m !mass ! gravity equal 32 ft/s^2 write (*,*)'enter time step' read(*,*)h write(*,*)'enter initial velocity' read(*,*)q write(*,*)'enter drag coefficient' read(*,*)c write(*,*)'enter mass' read(*,*)m i=1,10 ! 1 10, 1 being interval. end v(i+1)=v(i)+[32-((c*v(i)*v(i))/m)]*(h) q=v(1) end program you cannot use [] normal parenthesis in expressions. array constructor, [ items ] means array items elements. end do should after line.
Read more