Fix extended function decomposition (#2960)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 17 Apr 2019 15:26:46 +0000 (10:26 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Wed, 17 Apr 2019 15:26:46 +0000 (08:26 -0700)
commit5b00f8d6804bf9f71d6169634341011f99d59b8b
tree001bef3833e07195ce2119978f0098d681a2a5ef
parent29a06b999c4637197282405df7040d6773bd3858
Fix extended function decomposition (#2960)

Fixes #2958.

The issue was: we had substr(x,0,2) in R, and the "derivable substitution" modifed this to substr(substr(x,0,2),0,2) in R, since substr(x,0,2) was the representative of x (which is a bad choice, but regardless is legal). Then decomposition inference asked "can i reduce substr(substr(x,0,2),0,2) in R"? It determines substr(substr(x,0,2),0,2) in R rewrites to substr(x,0,2) in R, which is already true. However, substr(x,0,2) in R was what we started with.

The fix makes things much more conservative: we never mark extended functions reduced based on decomposition, since there isnt a strong argument based on an ordering.
src/theory/strings/theory_strings.cpp
test/regress/CMakeLists.txt
test/regress/regress0/strings/issue2958.smt2 [new file with mode: 0644]