Z3_get_interpolant fails (always returns "true") #47
Comments
kenmcmil
added a commit
that referenced
this issue
Apr 20, 2015
|
Fixed this in iz3interp.cpp. |
NikolajBjorner
added a commit
to NikolajBjorner/z3
that referenced
this issue
May 8, 2017
* z3py: With tactical should not try to use context as a parameter * move restore relevancy until after literals have been replayed Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * [CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. Two new options `INCLUDE_GIT_HASH` and `INCLUDE_GIT_DESCRIBE` have been added that enable/disable including the git hash and the output of `git describe` respectively. By default if the source tree is a git repository both options are on, otherwise they are false by default. To support the `Z3GITHASH` macro a different implementation is used from the old build system. In that build system the define is passed on the command line. This would not work well for CMake because CMake conservatively (and correctly) rebuilds *everything* if the flags given to the compiler change. This would result in the entire project being rebuilt everytime git's `HEAD` changed. Instead in this implementation a CMake specific version of `version.h.in` (named `version.h.cmake.in`) is added that uses the `#cmakedefine` feature of CMake's `configure_file()` command to define `Z3GITHASH` if it is available and not define it otherwise. This way only object files that depend on `version.h` get re-built rather than the whole project. It is unfortunate that the build systems now have different `version.h` file templates. However they are very simple and I don't want to modify how templates are handled in the python/Makefile build system. * add debugging to lra Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * [CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. These files allow users of CMake to use Z3 via a CMake config package. Clients can do `find_package(Z3 CONFIG)` to get use the package from their projects. When generating the files for the install tree we try to generate the files so that they are relocatable so that it shouldn't matter if the installed files aren't in the CMAKE_INSTALL_PREFIX when a user consumes them. As long as the relative locations of the files aren't changed things should still work. A new CMake cache variable `CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR` has been added so that the install location of the Z3 CMake package files can be controlled. This addresses Z3Prover#915 . * [CMake] Python examples should only be copied over if python bindings are being built. * [CMake] Build `c_example`, `cpp_example` and `z3_tptp5` as external projects. This works by giving each example it's own CMake build system and then consuming Z3 via the Z3 CMake config package from the build tree. * [CMake] Fix typo handling OpenMP flags. * [CMake] Fix examples linking against libz3 when it is built as a static library on Linux. * [CMake] On Windows when building the examples copy the Z3 library into the directory of the example executable so that it works "out of the box". * add alternate str.at semantics check in seq_rewriter this rewrites to empty string if the index is negative or beyond the length of the string, which is consistent with CVC4's semantics for this term * fixup startswith/endswith to prefixof/suffixof * added no exception support to z3++.h * add sum shorthand to C++. Issue Z3Prover#694 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add pb shorthands to C++. Issue Z3Prover#694 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * str.extract semantics fix * make seq.at operations generic Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fixing sources for double frees of clauses. Z3Prover#940 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove legacy str_decl_plugin and str_rewriter classes; these have been unified with sequence-compatible equivalents * fix crash reported in Z3Prover#946 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * disable ackerman reduction when head contains a non-constant/non-variable. Z3Prover#947 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix unterminated char* * remove code that causes infinite loop. Stackoverflow question from Dominik Wojtaszek Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix build with VS 2017 * remove unsound simplification in prefix Z3Prover#949 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * make seq.extract rewrite type-generic * fix bug in simplifier of bv2int over concatentations exposed by Z3Prover#948 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * introducing scoped detacth/attach of clauses to enforce basic sat solver invariants. Part of investigating Z3Prover#939: Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * making simplifier code exception friendlier. Towards getting a handle on Z3Prover#939 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix double ownership of enode marking causing crash during tracing. Issue Z3Prover#952 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix double ownership of enode marking causing crash during tracing. Issue Z3Prover#952 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Fixed excessive trace output * add handlers for dense difference logic Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix constant offset and handling of ite in difference logic optimizer code-path. Issue Z3Prover#946 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Disabled debug output * Build fix for systems that don't come with SSE4.1 support by default * VS2017 SSE4 intrinsics build fix * Removed unused variable * Fixed variable initialization warning * Windows build fix * Non-windows build fix * fix for --get-describe * properly handle recursive function definitions Z3Prover#898 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * properly handle recursive function definitions Z3Prover#898 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add missing axioms for str.at. Issue Z3Prover#953 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * SMT2 compliancy fix; NRA includes conversion of Int numerals * Improved decl_collector for uninterpreted sorts in :print_benchmark output * Updated declarations in decl_collector * return box model based on index. Issue Z3Prover#955 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix python interface for string extract to take symbolic indices per bug report from Kun Wei Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add index option to 'eval' command for box objectives. Issue Z3Prover#955 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add bypass to allow recursive functions from API Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove references to m_str_fid in api * remove old theory_str enums from api * remove obsolete PARAM_STRING from ast * Avoid null pointer warnings in justifications. * Added utility to compare quantifier instantiation profiles generated via smt.qi.profile=true * Fixes for qprofdiff * Build fix for qprofdiff * Result ordering fix for qprofdiff * Added rewriter.ignore_patterns_on_ground_qbody option to disable simplification of quantifiers that have their universals appear only in patterns, but otherwise have a ground body. * add facility to dispense with cancellation (not activated at this point). Address Z3Prover#961 by expanding recurisve function definitions that are not tautologies if the current model does not validate Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Added maintainers.txt for qprofdiff * Fixed valgrind warning. Fixes Z3Prover#972 * fix detection of bounds under conjunctions. Issue Z3Prover#971 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add regular expression membership for range of int.to.str functions. Issue Z3Prover#957 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * experimental new unsat core based overlap detection * add overlap assumption to other cases in theory_str * add missing string/re operations Z3Prover#977 and adding Pseudo-Boolean operations to Java API Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix for Z3Prover#975, add mask to ensure character encoding is unique within range of bits used for encoding Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * include timeout/rlimit parameters in optmize Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * replace uint by long Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * replace long by int Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * replace long by int Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * additional API per Z3Prover#977 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * issues Z3Prover#963 Z3Prover#912 * Added core.extend_nonlocal_patterns parameter to improve unsat cores. * add pre-init assumptions for smt theories * Whitespace * Added rlimit.inc() for expensive interval exponentiation in the non-linear arithmetic theory. * Fix typo noted in Z3Prover#979. `g++` is the default compiler rather than the `gcc` binary. * Be more explicit about using Clang as the compiler as noted in Z3Prover#979. Referring to the ``mk_make.py`` line might lead someone to think they need to modify the ``mk_make.py`` file rather than change the command line invocation. * unsat core validation for smt theories * pre-init assumptions and unsat core validation for smt theories * check result of unsat core validation * tidy Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Return check result in fixedpoint object This is a small change to fix a missing return statement. * [Doxygen] Fix script `--help` functionality. * [Doxygen] Fix bug where `def_Type` directives in `z3.h` would appear in generated doxygen documentation. * remove unused parameter from smt_context * unify tracing in theory_str to 'str' tag * update license for space/quotes per Z3Prover#982 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * [Doxygen] Switch to using `argparse` to parse command line arguments in `mk_api_doc.py`. Given that we need to add a bunch of new command line options it makes sense to use a less clumsy and concise API. * [Doxygen] Add `--doxygen-executable` command line option to `mk_api_doc.py`. This allows a custom path to Doxygen to be specified. * fix trace typos * string/sequence static features test * make sure consequence generation works with interpreted atoms/terms Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix str/seq parameter config * make SMT consequence finding work with compound terms and formulas Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * [Doxygen] Teach `mk_api_doc.py` a new command line option (`--temp-dir`) which allows the location of the temporary directory to be controlled. While I'm here also write `website.dox` into the temporary directory where it belongs instead of in the source tree and simplify the logic that deletes the temporary directory and its contents. * [Doxygen] Teach `mk_api_doc.py` a new command line option (`--output-dir`) to control where output files are emitted. This is implemented by making `z3api.dox` a template file (renamed `z3api.cfg.in`) and populating the template at build time with the required settings. * [Doxygen] Teach `mk_api_doc.py` to use `@` style substitutions to control whether OCaml documentation link is emitted. * [Doxygen] Fix bug in `mk_api_doc.py` where the generated doxygen configuration would not point at the correct path to the temporary directory. * [Doxygen] Fix some indentation in doxygen configuration file template. * [Doxygen] Fixed malformed code blocks in `z3_api.h`. These malformed `\code` blocks caused broken documentation to be generated. * [Doxygen] Fix typo found with Doxygen warning ``` warning: Found unknown command `\s' ``` * [Doxygen] Fix warning about non-existent functions. `Z3_push` and `Z3_pop` should be `Z3_solver_push` and `Z3_solver_pop` respectively. * [Doxygen] Add `--z3py-package-path` command line option to `mk_api_doc.py` so that the location of the z3py package can be specified. This is needed by the CMake build system because the complete Z3py package is not emitted in the source tree. Also fix a bug in the path added to the module/package search path. The directory containing the `z3` package needs to be added not the `z3` package directory itself. * [Doxygen] Put the path to the directory containing the Z3py package at the beginning of the search path so it is picked up first. This is to try to avoid picking an installed copy of Z3py. * [Doxygen] Teach `mk_api_doc.py` to prevent ".NET", "Z3py" and "Java" bindings from appearing in the generated documentation. This can be enabled with `--no-dotnet`, `--no-z3py`, and `--no-java` respectively. This fine-grained control is being added for the CMake build system which will need this control. * [Doxygen] Fix bug where temporary directory and output directory paths were not handled properly if paths contained spaces. * [Doxygen] Teach `mk_api_doc.py` to allow multiple search paths for the ".NET" and "Java" bindings. The CMake build system needs this because the generated files exist in a different directory to the source files. Multiple paths can be specified using the `--dot-search-paths` and `--java-search-paths` options. * [Doxygen] Fix `mk_api_doc.py` so it is not required that the current working directory be the `doc` directory in the source tree. * [CMake] Teach CMake to build the documentation for the API bindings and install them. The target for building the documentation is `api_docs`. This is off by default but can be enabled with the `BUILD_DOCUMENTATION` option. The C and C++ API documentation is always built but the Python, ".NET", and Java documentation are only built if they are enabled in the build system. The rationale for this is that it would be confusing to install documentation for API bindings that are not installed. By default `ALWAYS_BUILD_DOCS` is on which will slow down builds significantly but will ensure that when the `install` target is invoked the documentation is up-to-date. Unfortunately I couldn't find a better way to do this. `ALWAYS_BUILD_DOCS` can be disabled to get faster builds and still have the `api_docs` target available. * [Doxygen] Fix link to ".NET" documentation it should point to the "Microsoft.Z3" namespace, not the "Microsoft.Z3.Context" class. This mirrors the link provided for the Java API. * tuning and fixing consequence finding, adding dimacs evaluation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * adding interval designator to output of non-optimal objectives, fix python doc test Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * theory_str frontend changes * added chunk based backbone utility Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix is_string_term() * fix is_string_term() * remove redundant is_seq() check * initial integration of opt Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * revert change to String sort declaration * fixup * remove references to str_fid * theory_str static features and cmd_context * [CMake] Remove compiler flag overrides and support for C language. The setting of overrides was broken (the CXX flags were not set but the C flags were) and we aren't even using the C compiler any more. The C compiler is used by the example C project but that is built as an external project now so we don't need C support anymore. The setting of defaults was also very fragile. CMake has quite complicated support here (e.g. MSVC with a clang based tool chain) which would likely not work properly with the override approach as it existed. This means we loose some of the custom linker flags we were setting for MSVC but we were never doing a great job of replicating the exact set of flags used in the old build system anyway. Subsequent commits will gradually fix this. * [CMake] Report the various values of CMAKE_CXX_FLAGS, CMAKE_CXX_FLAGS_<CONFIG>, CMAKE_<TYPE>_LINKER_FLAGS, and CMAKE_<TYPE>_LINKER_FLAGS_<CONFIG>. This is useful for debugging where some flags come from. Now that we don't explicitly set the defaults it useful to see which default values we are getting from CMake. * [CMake] Teach build system to pass `/fp:precise` to compiler when using MSVC. This is set by the old build system but we weren't setting it. This actually MSVC's default but in an effort to try to behave more like the old build system we will set it anyway. * [CMake] CMake's default value for CMAKE_CXX_FLAGS includes `/W3` remove this so we can have fine grained control of warnings. * [CMake] Add support for link time optimization (LTO). This analogous to the `--optimize` flag in the Python/Makefile build system except that we now support doing LTO with Clang/GCC as well. However it is probably best to avoid doing LTO with Clang or GCC for now because I see a bunch of warnings about ODR violations when building with LTO. LTO can be enabled with the new `LINK_TIME_OPTIMIZATION` option which is off by default. * [CMake] Try to do a better job of matching the old build system's compiler defines and flags when using MSVC. There are lots of defines and flags that I'm unsure about so in some cases I've changed the behaviour slightly (if I'm confident the behaviour in the old build system is wrong) or not added the flag/define at all but just left comments noting what the old build system did and why I disagree with the old build system's choices. * [CMake] When building with MSVC and without `WARNINGS_AS_ERRORS` pass `/WX-` to MSVC. Although this is not necessary this duplicates the behaviour of the old build system. * [CMake] When building with MSVC try to disable incremental linking for all builds. * [CMake] When building with MSVC pass the `/STACK:` argument to the linker like the old build system does. * [CMake] When using MSVC set the `/SUBSYSTEM:` argument given to the linker. This mimics the behaviour of the old build system. * [CMake] Duplicate the remaining linker flags from the old build system. * [CMake] Override CMake's default flags for GCC/Clang as we were doing before 4cc2b29. It's useful to be able to control the defaults and CMake's internal logic for GCC/Clang is simple enough that doing this makes sense. It would be nice to do the same for MSVC but CMake's internal logic is more complicated so for now it's better that we just use CMake's default. * fix bounds update in lra optimization Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix bound bug Z3Prover#991 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix unused variables Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix unused variables Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix unused variables Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * Sat update Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * swap argument order of chunk with file Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * include 'stopwatch.h' to avoid ODR warnings, Z3Prover#994 * update get-value to also respect parameter model_index, Z3Prover#955 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * augment Z3Prover#955 to handle hyphen Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * renmae to opt_stream_buffer to avoid clash with dimacs stream buffer. Z3Prover#994 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add params for theory case split * add theory case split support to smt_context * fix warning * deal with subtraction that manages to sneak in. Issue Z3Prover#996 Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * simplify theory case split handling * revert to native chunker Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * use reference for case split sets * fix build break Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * pass qhead Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * simplify handling of objectives Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * params for theory aware branching * theory-aware branching heuristic * refactor: add asserts, use case split strategy param * cleanup * remove trace code from theory_arith * fix spacing * fix bug in tracking levels of variables: levels are not cleared, only truth assignment Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * smt_setup framework, all hooks to theory_str are redirected to theory_seq * fix quadratic behavior of extract_assumptions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add back use of all variables for tracking Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * update to retain original behavior Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * update to retain original behavior Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add common utility to set up seq Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * add iterator accessors to obj_pair_set * cleanup * fix overlap detection internalization * Fix bug in `mk_api_doc.py` where the Z3 python package path would be checked when building the Z3 python package documentation was disabled. * [CMake] Remove `BYPRODUCTS` declaration for `api_docs` target. This breaks the `clean` rule when using Ninja as the CMake generator. Unfortunately this means `clean` doesn't try to remove the generated documentation anymore when using Ninja. * Fixed bug with .NET keyfile path containing spaces. Fixes Z3Prover#1003. * Enabled C++11 in GCC and Clang * fix Z3Prover#1005, disable expansion of regular expression range to union as it degrades performance significantly Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * remove unneeded include * first-class re.range support in theory_str * add new files to cmakelist.txt files Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * formatting theory_str.cpp * formatting theory_str.h * clean up some warnings Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * use skolem function to avoid exposing temporary variables in models Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * relaxing condition for assumptions, add theory-assumption to skolem functions Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com> * fix warnings: unused variables, string constants
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This bug is caused by not collecting the assertions from the solver or proof, which had the side effect of treating all assertions in the pattern as "background".
The text was updated successfully, but these errors were encountered: