Bug #485: Non-linear SMT solver queries in BLAST - BLAST - Open-Source Projects

Actions

Copy link

Bug #485

open

Non-linear SMT solver queries in BLAST

Added by Vadim Mutilin about 14 years ago. Updated about 13 years ago.

Status:

Open

Priority:

Low

Assignee:

Mikhail Mandrykin

Category:

Target version:

Start date:

10/12/2010

Due date:

% Done:

Estimated time:

Detected in build:

7c1b9ad0ccbad6e108554fdb49202f107103b5be

Platform:

Published in build:

Description

shved3-current--X--drivers--X--bigmemtimelinux-2.6.31.6--X--32_7.pax:

linux-2.6.31.6 32_7 drivers/media/video/cx231xx/cx231xx.ko ldv_main6_seq_one ZZZ: Exception: Failure("SMT sovler answer is strange: Error: feature not supported: non linear problem.")
linux-2.6.31.6 32_7 drivers/media/video/et61x251/et61x251.ko ldv_main0_seq_one ZZZ: Exception: Failure("SMT sovler answer is strange: Error: feature not supported: non-constant division.")
linux-2.6.31.6 32_7 drivers/usb/misc/sisusbvga/sisusbvga.ko ldv_main2_seq_one ZZZ: Exception: Failure("SMT sovler answer is strange: Error: feature not supported: non linear problem.")
linux-2.6.31.6 32_7 drivers/usb/misc/usbtest.ko ldv_main0_seq_one ZZZ: Exception: Failure("SMT sovler answer is strange: Error: feature not supported: non-constant division.")
linux-2.6.31.6 32_7 drivers/media/video/gspca/gspca_main.ko ZZZ: Exception: Failure("SMT sovler answer is strange: Error: feature not supported: non linear problem.")
linux-2.6.31.6 32_7 drivers/media/video/ov511.ko ldv_main0_seq_one ZZZ: Exception: Failure("SMT sovler answer is strange: Error: feature not supported: non linear problem.")
linux-2.6.31.6 32_7 drivers/usb/misc/sisusbvga/sisusbvga.ko ldv_main2_seq_one ZZZ: Exception: Failure("SMT sovler answer is strange: Error: feature not supported: non linear problem.")
linux-2.6.31.6 32_7 drivers/media/dvb/dvb-usb/dvb-usb-vp702x.ko ldv_main1_seq_one ZZZ: Exception: Failure("SMT sovler answer is strange: Error: feature not supported: non-constant division.")
linux-2.6.31.6 32_7 drivers/media/dvb/ttpci/dvb-ttpci.ko ldv_main4_seq_one ZZZ: Exception: Failure("SMT sovler answer is strange: Error: feature not supported: non-constant division.")
linux-2.6.31.6 32_7 drivers/media/video/bt8xx/bttv.ko ldv_main0_seq_one ZZZ: Exception: Failure("SMT sovler answer is strange: Error: feature not supported: non linear problem.")

Actions

Copy link

Updated by Vadim Mutilin about 14 years ago

To run envgen with your model you should prepare .properties file
1. copy drv-env-gen/default.propeties to some folder, rename it
2. edit it by setting your envmodel identifier (e.g. include=p1)
3. set ENVGEN_PROPERTIES environment variable

BLAST_EXP_NOLATTICE=1

Actions

Copy link

Updated by Mikhail Mandrykin about 14 years ago

All BLAST queries with such strange answers collected on the whole drivers/media/video folder contained either division by a variable or by the result of an uninterpreted function application or multiplication between two variables or functions. BLAST also generates such queries even on simple examples like:

int main() {
    int a = 5, b = 10;
    if (b / a > 0) {
        goto ERROR;
    }
    return 0;
    ERROR:
    return 1;
}

int main() {
    int a = 5, b = 10;
    if (b * a > 0) {
        goto ERROR;
    }
    return 0;
    ERROR:
    return 1;   
}

Here are some example formulas, one got from the first code snippet and another from the second:

( benchmark Blast_query_9
:logic AUFLIA
:extrafuns((S2 Int ))
:extrafuns((S1 Int ))
:formula (and true true  true  true  (and true (= S1 5) (= S2 10)) (> (/ S2 S1) 0) true )
)

( benchmark Blast_query_10
:logic AUFLIA
:extrafuns((S2 Int ))
:extrafuns((S1 Int ))
:formula (and true true  true  true  true  (and true (= S1 5) (= S2 10)) (> (* S2 S1) 0) true )
)

Yices solver always give errors on such formulas, because they contain non-linear arithmetic. But CVC3 and Z3 solvers sometimes ignore the issue and try to solve these formulas. CVC3 will sometimes give an error if the formula contains the inverse of a variable (like "1000 / S3"), and Z3 will fail if the result of some division is used as integer argument to a function.
There is an idea that BLAST could use uninterpreted functions with some additional assumtions in such cases, thus generating a query in AUFLIA logic.

Actions

Copy link