[SMT-LIB] QF_BV and division by zero

[Christoph Wintersteiger]

This topic comes up every year ��

There are equal amounts of good and bad things to be said about either approach. Personally, I don't by the "least surprise" argument in this particular case, because QF_BV is used in many applications where the interpretation of bvudiv is completely fixed, always, and every single time. The only thing that's not always completely clear is the actual number that it's fixed to. However, this is easy to fix by simply asking the user for what value he prefers and the vast majority of all QF_BV users is able to make that choice. 

In the past, I suggested to introduce a mandatory option, which, when not explicitly set, will trigger a warning that reminds the user to choose the semantics by adding a command line option. Not all solvers would have to implement all options of course. 

In general however, it's fairly easy to translate between the two anyways... e.g., replace all (bvudiv x y) by 
(if (y=0) then my_chosen_value else new_uninterpreted_function)
That way, all users can add UFs wherever they want them, with minimal overhead on either side. Obviously, if they want to use a solver that doesn't support UFs this won't work. If they have to write those ITEs themselves however, they will also understand why they can't do what they want to do...

Cheers,
Christoph


Christoph M. Wintersteiger | Researcher | Tel: +44 1223 479724 | Fax: +44 1223 479999 | https://www.microsoft.com/en-us/research/people/cwinter/


Microsoft Research Limited (company number 03369488) is a company registered in England and Wales whose registered office is at 21 Station Road, Cambridge, CB1 2FB 

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of François Bobot
Sent: 30 March 2017 10:03
To: smt-lib at cs.nyu.edu
Subject: Re: [SMT-LIB] QF_BV and division by zero

Le 30/03/2017 à 05:52, Trevor Hansen a écrit :
> It'd be great to have QF_BV division and remainder by zero resolved in time for this year's SMTCOMP.
> The relevant discussion from 2015 is in the thread 
> here:http://www.cs.nyu.edu/pipermail/smt-lib/2015/000966.html

The original choice of the SMTLIB is to totalize partial function by accepting all interpretations instead of fixing one. I understand it as a choice of least surprise for the user. I acknowledge that in some cases it complicates the work or the efficiency of the solvers.


But for my part I prefer to be sure of what I'm proving, so I prefer the current choice and I'm worried that adding exceptions to the rule lead to removing the rule.

Why QF_BV division and remainder should be different from any other partial function? Does your argument should not apply to any SMTLIB partial function?


Best,

-- 
François Bobot
_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/smt-lib