diff --git a/CMakeLists.txt b/CMakeLists.txt index c11c272be..bd3774ac7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -34,7 +34,7 @@ endif() ################################################################################ set(Z3_VERSION_MAJOR 4) set(Z3_VERSION_MINOR 6) -set(Z3_VERSION_PATCH 2) +set(Z3_VERSION_PATCH 3) set(Z3_VERSION_TWEAK 0) set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified diff --git a/README.md b/README.md index 70956d439..8ebf6a078 100644 --- a/README.md +++ b/README.md @@ -12,9 +12,9 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z ## Build status -| Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | OSX | TravisCI | -| ----------- | ----------- | ---------- | ---------- | --- | -------- | -[![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) +| Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | OSX | TravisCI | +| ----------- | ----------- | ----------- | ---------- | ---------- | --- | -------- | +[![win64-badge](https://z3build.visualstudio.com/_apis/public/build/definitions/2e0aa542-a22c-4b1a-8dcd-3ebae8e12db4/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=4) | [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index df977268a..ed5bf7086 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -920,6 +920,16 @@ void enum_sort_example() { std::cout << "2: " << result_goal.as_expr() << std::endl; } +void tuple_example() { + std::cout << "tuple example\n"; + context ctx; + const char * names[] = { "first", "second" }; + sort sorts[2] = { ctx.int_sort(), ctx.bool_sort() }; + func_decl_vector projs(ctx); + func_decl pair = ctx.tuple_sort("pair", 2, names, sorts, projs); + std::cout << pair << "\n"; +} + void expr_vector_example() { std::cout << "expr_vector example\n"; context c; @@ -1179,6 +1189,7 @@ int main() { incremental_example2(); std::cout << "\n"; incremental_example3(); std::cout << "\n"; enum_sort_example(); std::cout << "\n"; + tuple_example(); std::cout << "\n"; expr_vector_example(); std::cout << "\n"; exists_expr_vector_example(); std::cout << "\n"; substitute_example(); std::cout << "\n"; diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index b947928a7..c2b1f0af9 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -2452,7 +2452,6 @@ Z3_lbool ext_check(Z3_ext_context ctx) { } printf("\n"); } - return result; } @@ -2464,7 +2463,7 @@ void incremental_example1() { Z3_context ctx = ext_ctx->m_context; Z3_ast x, y, z, two, one; unsigned c1, c2, c3, c4; - Z3_bool result; + Z3_lbool result; printf("\nincremental_example1\n"); LOG_MSG("incremental_example1"); @@ -2485,7 +2484,7 @@ void incremental_example1() { c4 = assert_retractable_cnstr(ext_ctx, Z3_mk_lt(ctx, y, one)); result = ext_check(ext_ctx); - if (result != Z3_L_FALSE) + if (result != Z3_L_FALSE) exitf("bug in Z3"); printf("unsat\n"); diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 2f7402760..b77975dfa 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -9,7 +9,7 @@ from mk_util import * # Z3 Project definition def init_project_def(): - set_version(4, 6, 2, 0) + set_version(4, 6, 3, 0) add_lib('util', []) add_lib('lp', ['util'], 'util/lp') add_lib('polynomial', ['util'], 'math/polynomial') diff --git a/scripts/update_api.py b/scripts/update_api.py index 18878d6ea..0a86db18d 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -957,11 +957,16 @@ def def_API(name, result, params): log_c.write(" }\n") log_c.write(" Au(a%s);\n" % sz) exe_c.write("in.get_uint_array(%s)" % i) - elif ty == INT or ty == BOOL: + elif ty == INT: log_c.write("U(a%s[i]);" % i) log_c.write(" }\n") log_c.write(" Au(a%s);\n" % sz) exe_c.write("in.get_int_array(%s)" % i) + elif ty == BOOL: + log_c.write("U(a%s[i]);" % i) + log_c.write(" }\n") + log_c.write(" Au(a%s);\n" % sz) + exe_c.write("in.get_bool_array(%s)" % i) else: error ("unsupported parameter for %s, %s, %s" % (ty, name, p)) elif kind == OUT_ARRAY: diff --git a/scripts/vsts-mac.sh b/scripts/vsts-mac.sh new file mode 100644 index 000000000..9be53967f --- /dev/null +++ b/scripts/vsts-mac.sh @@ -0,0 +1,19 @@ +#!/bin/sh + +cd .. +mkdir build +CSC=/usr/bin/csc GACUTIL=/usr/bin/gacutil CXX=clang++ CC=clang python scripts/mk_make.py --java --python +cd build +make +make test-z3 +make cpp_example +make c_example +# make java_example +# make python_example +./cpp_example +./test_capi + +git clone https://github.com/z3prover/z3test.git z3test +ls +python z3test/scripts/test_benchmarks.py ./z3 ./z3test/regressions/smt2 + diff --git a/scripts/vsts-vs2013.cmd b/scripts/vsts-vs2013.cmd new file mode 100644 index 000000000..1676f3e2d --- /dev/null +++ b/scripts/vsts-vs2013.cmd @@ -0,0 +1,49 @@ + +set +echo "Build" +md build +cd build +call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" amd64 +cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -G "NMake Makefiles" ../ +nmake +if ERRORLEVEL 1 exit 1 + +rem echo "Test python bindings" +rem pushd python +rem python z3test.py z3 +rem if ERRORLEVEL 1 exit 1 +rem python z3test.py z3num +rem if ERRORLEVEL 1 exit 1 +rem popd + +echo "Build and run examples" +nmake cpp_example +examples\cpp_example_build_dir\cpp_example.exe +if ERRORLEVEL 1 exit 1 + +nmake c_example +examples\c_example_build_dir\c_example.exe +if ERRORLEVEL 1 exit 1 + +rem nmake java_example +rem java_example.exe +if ERRORLEVEL 1 exit 1 + +rem nmake dotnet_example +rem dotnet_example.exe +if ERRORLEVEL 1 exit 1 + +echo "Build and run unit tests" +nmake test-z3 +rem TBD: test error level +rem test-z3.exe -a + + +cd .. +echo "Run regression tests" +git clone https://github.com/z3prover/z3test z3test +echo "test-benchmarks" +python z3test\scripts\test_benchmarks.py build\z3.exe z3test\regressions\smt2 +if ERRORLEVEL 1 exit 1 +echo "benchmarks tested" + diff --git a/scripts/vsts-vs2017.cmd b/scripts/vsts-vs2017.cmd new file mode 100644 index 000000000..4ec4deca9 --- /dev/null +++ b/scripts/vsts-vs2017.cmd @@ -0,0 +1,51 @@ +rem Supply argument x64 or x86 + +echo "Build" +md build +cd build +call "C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Auxiliary\Build\vcvarsall.bat" %1 +cmake -DBUILD_DOTNET_BINDINGS=True -DBUILD_JAVA_BINDINGS=True -DBUILD_PYTHON_BINDINGS=True -G "NMake Makefiles" ../ +nmake +if ERRORLEVEL 1 exit 1 + +if %1 == "x86" goto :BUILD_EXAMPLES +echo "Test python bindings" +pushd python +python z3test.py z3 +if ERRORLEVEL 1 exit 1 +python z3test.py z3num +if ERRORLEVEL 1 exit 1 +popd + +:BUILD_EXAMPLES +echo "Build and run examples" +nmake cpp_example +examples\cpp_example_build_dir\cpp_example.exe +if ERRORLEVEL 1 exit 1 + +nmake c_example +examples\c_example_build_dir\c_example.exe +if ERRORLEVEL 1 exit 1 + +rem nmake java_example +rem java_example.exe +if ERRORLEVEL 1 exit 1 + +rem nmake dotnet_example +rem dotnet_example.exe +if ERRORLEVEL 1 exit 1 + +echo "Build and run unit tests" +nmake test-z3 +rem TBD: test error level +rem test-z3.exe -a + + +cd .. +echo "Run regression tests" +git clone https://github.com/z3prover/z3test z3test +echo "test-benchmarks" +python z3test\scripts\test_benchmarks.py build\z3.exe z3test\regressions\smt2 +if ERRORLEVEL 1 exit 1 +echo "benchmarks tested" + diff --git a/src/api/api_context.h b/src/api/api_context.h index 7009250cc..185eb9e0f 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -34,6 +34,7 @@ Revision History: #include "util/event_handler.h" #include "cmd_context/tactic_manager.h" #include "cmd_context/context_params.h" +#include "cmd_context/cmd_context.h" #include "api/api_polynomial.h" #include "util/hashtable.h" @@ -53,6 +54,7 @@ namespace api { context_params m_params; bool m_user_ref_count; //!< if true, the user is responsible for managing reference counters. scoped_ptr m_manager; + scoped_ptr m_cmd; add_plugins m_plugins; arith_util m_arith_util; @@ -114,6 +116,7 @@ namespace api { ast_manager & m() const { return *(m_manager.get()); } context_params & params() { return m_params; } + scoped_ptr& cmd() { return m_cmd; } bool produce_proofs() const { return m().proofs_enabled(); } bool produce_models() const { return m_params.m_model; } bool produce_unsat_cores() const { return m_params.m_unsat_core; } diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index 2e33c1a13..28db62cc3 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -21,8 +21,11 @@ Revision History: #include "api/api_context.h" #include "api/api_util.h" #include "cmd_context/cmd_context.h" +#include "smt/smt_solver.h" #include "parsers/smt2/smt2parser.h" #include "solver/solver_na2as.h" +#include "tactic/portfolio/smt_strategic_solver.h" + extern "C" { @@ -117,4 +120,34 @@ extern "C" { RETURN_Z3(r); Z3_CATCH_RETURN(nullptr); } + + Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context c, Z3_string str) { + std::stringstream ous; + Z3_TRY; + LOG_Z3_eval_smtlib2_string(c, str); + if (!mk_c(c)->cmd()) { + mk_c(c)->cmd() = alloc(cmd_context, false, &(mk_c(c)->m())); + mk_c(c)->cmd()->set_solver_factory(mk_smt_strategic_solver_factory()); + } + scoped_ptr& ctx = mk_c(c)->cmd(); + std::string s(str); + std::istringstream is(s); + ctx->set_regular_stream(ous); + ctx->set_diagnostic_stream(ous); + try { + if (!parse_smt2_commands(*ctx.get(), is)) { + mk_c(c)->m_parser_error_buffer = ous.str(); + SET_ERROR_CODE(Z3_PARSER_ERROR); + RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); + } + } + catch (z3_exception& e) { + if (ous.str().empty()) ous << e.msg(); + mk_c(c)->m_parser_error_buffer = ous.str(); + SET_ERROR_CODE(Z3_PARSER_ERROR); + RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); + } + RETURN_Z3(mk_c(c)->mk_external_string(ous.str())); + Z3_CATCH_RETURN(mk_c(c)->mk_external_string(ous.str())); + } }; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 42467cb22..6f46f9440 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -267,6 +267,15 @@ namespace z3 { and in \c ts the predicates for testing if terms of the enumeration sort correspond to an enumeration. */ sort enumeration_sort(char const * name, unsigned n, char const * const * enum_names, func_decl_vector & cs, func_decl_vector & ts); + + /** + \brief Return a tuple constructor. + \c name is the name of the returned constructor, + \c n are the number of arguments, \c names and \c sorts are their projected sorts. + \c projs is an output paramter. It contains the set of projection functions. + */ + func_decl tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs); + /** \brief create an uninterpreted sort with the name given by the string or symbol. */ @@ -2432,6 +2441,19 @@ namespace z3 { for (unsigned i = 0; i < n; i++) { cs.push_back(func_decl(*this, _cs[i])); ts.push_back(func_decl(*this, _ts[i])); } return s; } + inline func_decl context::tuple_sort(char const * name, unsigned n, char const * const * names, sort const* sorts, func_decl_vector & projs) { + array _names(n); + array _sorts(n); + for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; } + array _projs(n); + Z3_symbol _name = Z3_mk_string_symbol(*this, name); + Z3_func_decl tuple; + sort _ignore_s = to_sort(*this, Z3_mk_tuple_sort(*this, _name, n, _names.ptr(), _sorts.ptr(), &tuple, _projs.ptr())); + check_error(); + for (unsigned i = 0; i < n; i++) { projs.push_back(func_decl(*this, _projs[i])); } + return func_decl(*this, tuple); + } + inline sort context::uninterpreted_sort(char const* name) { Z3_symbol _name = Z3_mk_string_symbol(*this, name); return to_sort(*this, Z3_mk_uninterpreted_sort(*this, _name)); diff --git a/src/api/dotnet/AlgebraicNum.cs b/src/api/dotnet/AlgebraicNum.cs index 66552f1a0..3687e1f83 100644 --- a/src/api/dotnet/AlgebraicNum.cs +++ b/src/api/dotnet/AlgebraicNum.cs @@ -3,11 +3,11 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - IntNum.cs + AlgebraicNum.cs Abstract: - Z3 Managed API: Int Numerals + Z3 Managed API: Algebraic Numerals Author: diff --git a/src/api/dotnet/BitVecNum.cs b/src/api/dotnet/BitVecNum.cs index c6ac471f6..66054761a 100644 --- a/src/api/dotnet/BitVecNum.cs +++ b/src/api/dotnet/BitVecNum.cs @@ -3,11 +3,11 @@ Copyright (c) 2012 Microsoft Corporation Module Name: - IntNum.cs + BitVecNum.cs Abstract: - Z3 Managed API: Int Numerals + Z3 Managed API: BitVec Numerals Author: diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index d4ff556fe..36283356d 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -114,15 +114,26 @@ def _symbol2py(ctx, s): # Hack for having nary functions that can receive one argument that is the # list of arguments. +# Use this when function takes a single list of arguments def _get_args(args): - try: - if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)): + try: + if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)): return args[0] - elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)): + elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)): return [arg for arg in args[0]] + else: + return args + except: # len is not necessarily defined when args is not a sequence (use reflection?) + return args + +# Use this when function takes multiple arguments +def _get_args_ast_list(args): + try: + if isinstance(args, set) or isinstance(args, AstVector) or isinstance(args, tuple): + return [arg for arg in args] else: return args - except: # len is not necessarily defined when args is not a sequence (use reflection?) + except: return args def _to_param_value(val): @@ -7943,8 +7954,10 @@ def AtLeast(*args): return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx) -def _pb_args_coeffs(args): - args = _get_args(args) +def _pb_args_coeffs(args, default_ctx = None): + args = _get_args_ast_list(args) + if len(args) == 0: + return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)() args, coeffs = zip(*args) if __debug__: _z3_assert(len(args) > 0, "Non empty list of arguments expected") @@ -7976,7 +7989,7 @@ def PbGe(args, k): ctx, sz, _args, _coeffs = _pb_args_coeffs(args) return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx) -def PbEq(args, k): +def PbEq(args, k, ctx = None): """Create a Pseudo-Boolean inequality k constraint. >>> a, b, c = Bools('a b c') diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index 3a6b7269e..8fd0c182e 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -36,7 +36,7 @@ _z3_op_to_str = { Z3_OP_CONCAT : 'Concat', Z3_OP_EXTRACT : 'Extract', Z3_OP_BV2INT : 'BV2Int', Z3_OP_ARRAY_MAP : 'Map', Z3_OP_SELECT : 'Select', Z3_OP_STORE : 'Store', Z3_OP_CONST_ARRAY : 'K', Z3_OP_ARRAY_EXT : 'Ext', - Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe' + Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe', Z3_OP_PB_EQ : 'PbEq' } # List of infix operators @@ -930,6 +930,8 @@ class Formatter: return self.pp_pbcmp(a, d, f, xs) elif k == Z3_OP_PB_GE: return self.pp_pbcmp(a, d, f, xs) + elif k == Z3_OP_PB_EQ: + return self.pp_pbcmp(a, d, f, xs) elif z3.is_pattern(a): return self.pp_pattern(a, d, xs) elif self.is_infix(k): diff --git a/src/api/z3.h b/src/api/z3.h index e08b0c073..b29f1d6ba 100644 --- a/src/api/z3.h +++ b/src/api/z3.h @@ -22,6 +22,7 @@ Notes: #define Z3_H_ #include +#include #include "z3_macros.h" #include "z3_api.h" #include "z3_ast_containers.h" diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 87bb4d818..2b46127fa 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -80,9 +80,9 @@ DEFINE_TYPE(Z3_rcf_num); */ /** - \brief Z3 Boolean type. It is just an alias for \c int. + \brief Z3 Boolean type. It is just an alias for \c bool. */ -typedef int Z3_bool; +typedef bool Z3_bool; /** \brief Z3 string type. It is just an alias for \ccode{const char *}. @@ -5209,6 +5209,17 @@ extern "C" { Z3_func_decl const decls[]); + /** + \brief Parse and evaluate and SMT-LIB2 command sequence. The state from a previous call is saved so the next + evaluation builds on top of the previous call. + + \returns output generated from processing commands. + + def_API('Z3_eval_smtlib2_string', STRING, (_in(CONTEXT), _in(STRING),)) + */ + + Z3_string Z3_API Z3_eval_smtlib2_string(Z3_context, Z3_string str); + /** \brief Retrieve that last error message information generated from parsing. diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index 1515e6df7..fde9b1f48 100644 --- a/src/api/z3_replayer.cpp +++ b/src/api/z3_replayer.cpp @@ -630,6 +630,12 @@ struct z3_replayer::imp { return m_int_arrays[idx].c_ptr(); } + bool * get_bool_array(unsigned pos) const { + check_arg(pos, UINT_ARRAY); + unsigned idx = static_cast(m_args[pos].m_uint); + return reinterpret_cast(m_unsigned_arrays[idx].c_ptr()); + } + Z3_symbol * get_symbol_array(unsigned pos) const { check_arg(pos, SYMBOL_ARRAY); unsigned idx = static_cast(m_args[pos].m_uint); @@ -761,6 +767,10 @@ int * z3_replayer::get_int_array(unsigned pos) const { return m_imp->get_int_array(pos); } +bool * z3_replayer::get_bool_array(unsigned pos) const { + return m_imp->get_bool_array(pos); +} + Z3_symbol * z3_replayer::get_symbol_array(unsigned pos) const { return m_imp->get_symbol_array(pos); } diff --git a/src/api/z3_replayer.h b/src/api/z3_replayer.h index e1b32af75..b81659945 100644 --- a/src/api/z3_replayer.h +++ b/src/api/z3_replayer.h @@ -51,6 +51,7 @@ public: unsigned * get_uint_array(unsigned pos) const; int * get_int_array(unsigned pos) const; + bool * get_bool_array(unsigned pos) const; Z3_symbol * get_symbol_array(unsigned pos) const; void ** get_obj_array(unsigned pos) const; diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 44f824959..f685c70d5 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -821,6 +821,10 @@ namespace datatype { return d; } + app* util::mk_is(func_decl * c, expr *f) { + return m.mk_app(get_constructor_is(c), 1, &f); + } + func_decl * util::get_recognizer_constructor(func_decl * recognizer) const { SASSERT(is_recognizer(recognizer)); return to_func_decl(recognizer->get_parameter(0).get_ast()); diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index e644ccbda..f32e9990d 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -362,6 +362,7 @@ namespace datatype { bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); } bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); } bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); } + app* mk_is(func_decl * c, expr *f); ptr_vector const * get_datatype_constructors(sort * ty); unsigned get_datatype_num_constructors(sort * ty); unsigned get_datatype_num_parameter_sorts(sort * ty); diff --git a/src/ast/rewriter/datatype_rewriter.cpp b/src/ast/rewriter/datatype_rewriter.cpp index f0a95929b..194668b9c 100644 --- a/src/ast/rewriter/datatype_rewriter.cpp +++ b/src/ast/rewriter/datatype_rewriter.cpp @@ -23,6 +23,9 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr switch(f->get_decl_kind()) { case OP_DT_CONSTRUCTOR: return BR_FAILED; case OP_DT_RECOGNISER: + SASSERT(num_args == 1); + result = m_util.mk_is(m_util.get_recognizer_constructor(f), args[0]); + return BR_REWRITE1; case OP_DT_IS: // // simplify is_cons(cons(x,y)) -> true diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index d1e470c3b..90b3f6c56 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -406,6 +406,7 @@ public: void reset_user_tactics(); void set_regular_stream(char const * name) { m_regular.set(name); } void set_regular_stream(std::ostream& out) { m_regular.set(out); } + void set_diagnostic_stream(std::ostream& out) { m_diagnostic.set(out); } void set_diagnostic_stream(char const * name); std::ostream & regular_stream() override { return *m_regular; } std::ostream & diagnostic_stream() override { return *m_diagnostic; } diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 3d1d84f3c..41c968bd8 100644 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -255,12 +255,12 @@ public: catch (const char *msg) { throw interpolation_failure(msg); } - catch (const iz3translation::unsupported &) { - TRACE("iz3", tout << "unsupported\n";); + catch (const iz3translation::unsupported & ex) { + TRACE("iz3", tout << "unsupported " << "\n";); throw interpolation_error(); } - catch (const iz3proof::proof_error &) { - TRACE("iz3", tout << "proof error\n";); + catch (const iz3proof::proof_error & ex) { + TRACE("iz3", tout << "proof error " << "\n";); throw interpolation_error(); } profiling::timer_stop("Proof translation"); @@ -306,8 +306,8 @@ public: catch (const char *msg) { throw interpolation_failure(msg); } - catch (const iz3translation::unsupported &) { - TRACE("iz3", tout << "unsupported\n";); + catch (const iz3translation::unsupported & ex) { + TRACE("iz3", tout << "unsupported " << "\n";); throw interpolation_error(); } catch (const iz3proof::proof_error &) { diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 9680ec95e..44bac0643 100644 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -2029,8 +2029,8 @@ public: case PR_IFF_FALSE: { // turns ~p into p <-> false, noop for us if(is_local(con)) res = args[0]; - else - throw_unsupported(con); + else + throw_unsupported(proof); break; } case PR_COMMUTATIVITY: { diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 9265312d4..e72b9ad79 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -949,8 +949,9 @@ namespace smt2 { check_duplicate(d, line, pos); d->commit(pm()); - check_rparen_next("invalid end of datatype declaration, ')' expected"); + check_rparen("invalid end of datatype declaration, ')' expected"); m_ctx.print_success(); + next(); } diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index f072a1d13..f4f56df5d 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -580,20 +580,20 @@ namespace smt { case b_justification::BIN_CLAUSE: { literal l2 = j.get_literal(); out << "bin-clause "; - display_literal(out, l2); + display_literal_verbose(out, l2); break; } case b_justification::CLAUSE: { clause * cls = j.get_clause(); out << "clause "; - if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals()); + if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals()); break; } case b_justification::JUSTIFICATION: { out << "justification " << j.get_justification()->get_from_theory() << ": "; literal_vector lits; const_cast(*m_conflict_resolution).justification2literals(j.get_justification(), lits); - display_literals(out, lits); + display_literals_verbose(out, lits); break; } default: diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 0ca244185..1f6811a0f 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -222,7 +222,7 @@ namespace smt { final_check_status final_check_eh(bool full) { if (full) { - IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"quantifiers\")\n";); + IF_VERBOSE(100, if (!m_quantifiers.empty()) verbose_stream() << "(smt.final-check \"quantifiers\")\n";); final_check_status result = m_qi_queue.final_check_eh() ? FC_DONE : FC_CONTINUE; final_check_status presult = m_plugin->final_check_eh(full); if (presult != FC_DONE) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index b90735a07..94841603d 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2404,8 +2404,7 @@ bool theory_seq::add_stoi_val_axiom(expr* e) { lits.push_back(~is_digit(ith_char)); nums.push_back(digit2int(ith_char)); } - for (unsigned i = sz-1, c = 1; i > 0; c *= 10) { - --i; + for (unsigned i = sz, c = 1; i-- > 0; c *= 10) { coeff = m_autil.mk_int(c); nums[i] = m_autil.mk_mul(coeff, nums[i].get()); } @@ -2414,9 +2413,10 @@ bool theory_seq::add_stoi_val_axiom(expr* e) { lits.push_back(mk_eq(e, num, false)); ++m_stats.m_add_axiom; m_new_propagation = true; - for (unsigned i = 0; i < lits.size(); ++i) { - ctx.mark_as_relevant(lits[i]); + for (literal lit : lits) { + ctx.mark_as_relevant(lit); } + TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); m_stoi_axioms.insert(val); m_trail_stack.push(insert_map(m_stoi_axioms, val)); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 69cf80de6..7d2364f4b 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -50,6 +50,7 @@ namespace smt { m_factory(nullptr), m_unused_id(0), m_delayed_axiom_setup_terms(m), + m_delayed_assertions_todo(m), tmpStringVarCount(0), tmpXorVarCount(0), tmpLenTestVarCount(0), @@ -169,6 +170,8 @@ namespace smt { } void theory_str::assert_axiom(expr * _e) { + if (_e == nullptr) + return; if (opt_VerifyFinalCheckProgress) { finalCheckProgressIndicator = true; } @@ -638,6 +641,7 @@ namespace smt { return contains; } + // note, this invokes "special-case" handling for the start index being 0 app * theory_str::mk_indexof(expr * haystack, expr * needle) { app * indexof = u.str.mk_index(haystack, needle, mk_int(0)); m_trail.push_back(indexof); @@ -779,8 +783,8 @@ namespace smt { ptr_vector childrenVector; get_nodes_in_concat(concatAst, childrenVector); expr_ref_vector items(m); - for (unsigned int i = 0; i < childrenVector.size(); i++) { - items.push_back(mk_strlen(childrenVector.get(i))); + for (auto el : childrenVector) { + items.push_back(mk_strlen(el)); } expr_ref lenAssert(ctx.mk_eq_atom(concat_length, m_autil.mk_add(items.size(), items.c_ptr())), m); assert_axiom(lenAssert); @@ -792,7 +796,8 @@ namespace smt { return !m_basicstr_axiom_todo.empty() || !m_str_eq_todo.empty() || !m_concat_axiom_todo.empty() || !m_concat_eval_todo.empty() || !m_library_aware_axiom_todo.empty() - || !m_delayed_axiom_setup_terms.empty(); + || !m_delayed_axiom_setup_terms.empty() + || (search_started && !m_delayed_assertions_todo.empty()) ; } @@ -800,66 +805,101 @@ namespace smt { context & ctx = get_context(); while (can_propagate()) { TRACE("str", tout << "propagating..." << std::endl;); - for (unsigned i = 0; i < m_basicstr_axiom_todo.size(); ++i) { - instantiate_basic_string_axioms(m_basicstr_axiom_todo[i]); + while(true) { + // this can potentially recursively activate itself + unsigned start_count = m_basicstr_axiom_todo.size(); + ptr_vector axioms_tmp(m_basicstr_axiom_todo); + for (auto const& el : axioms_tmp) { + instantiate_basic_string_axioms(el); + } + unsigned end_count = m_basicstr_axiom_todo.size(); + if (end_count > start_count) { + TRACE("str", tout << "new basic string axiom terms added -- checking again" << std::endl;); + continue; + } else { + break; + } } m_basicstr_axiom_todo.reset(); TRACE("str", tout << "reset m_basicstr_axiom_todo" << std::endl;); - for (unsigned i = 0; i < m_str_eq_todo.size(); ++i) { - std::pair pair = m_str_eq_todo[i]; + for (auto const& pair : m_str_eq_todo) { enode * lhs = pair.first; enode * rhs = pair.second; handle_equality(lhs->get_owner(), rhs->get_owner()); } m_str_eq_todo.reset(); - for (unsigned i = 0; i < m_concat_axiom_todo.size(); ++i) { - instantiate_concat_axiom(m_concat_axiom_todo[i]); + for (auto const& el : m_concat_axiom_todo) { + instantiate_concat_axiom(el); } m_concat_axiom_todo.reset(); - for (unsigned i = 0; i < m_concat_eval_todo.size(); ++i) { - try_eval_concat(m_concat_eval_todo[i]); + for (auto const& el : m_concat_eval_todo) { + try_eval_concat(el); } m_concat_eval_todo.reset(); - for (unsigned i = 0; i < m_library_aware_axiom_todo.size(); ++i) { - enode * e = m_library_aware_axiom_todo[i]; - app * a = e->get_owner(); - if (u.str.is_stoi(a)) { - instantiate_axiom_str_to_int(e); - } else if (u.str.is_itos(a)) { - instantiate_axiom_int_to_str(e); - } else if (u.str.is_at(a)) { - instantiate_axiom_CharAt(e); - } else if (u.str.is_prefix(a)) { - instantiate_axiom_prefixof(e); - } else if (u.str.is_suffix(a)) { - instantiate_axiom_suffixof(e); - } else if (u.str.is_contains(a)) { - instantiate_axiom_Contains(e); - } else if (u.str.is_index(a)) { - instantiate_axiom_Indexof(e); - } else if (u.str.is_extract(a)) { - instantiate_axiom_Substr(e); - } else if (u.str.is_replace(a)) { - instantiate_axiom_Replace(e); - } else if (u.str.is_in_re(a)) { - instantiate_axiom_RegexIn(e); + while(true) { + // Special handling: terms can recursively set up other terms + // (e.g. indexof can instantiate other indexof terms). + // - Copy the list so it can potentially be modified during setup. + // - Don't clear this list if new ones are added in the process; + // instead, set up all the new terms before proceeding. + // TODO see if any other propagate() worklists need this kind of handling + // TODO we really only need to check the new ones on each pass + unsigned start_count = m_library_aware_axiom_todo.size(); + ptr_vector axioms_tmp(m_library_aware_axiom_todo); + for (auto const& e : axioms_tmp) { + app * a = e->get_owner(); + if (u.str.is_stoi(a)) { + instantiate_axiom_str_to_int(e); + } else if (u.str.is_itos(a)) { + instantiate_axiom_int_to_str(e); + } else if (u.str.is_at(a)) { + instantiate_axiom_CharAt(e); + } else if (u.str.is_prefix(a)) { + instantiate_axiom_prefixof(e); + } else if (u.str.is_suffix(a)) { + instantiate_axiom_suffixof(e); + } else if (u.str.is_contains(a)) { + instantiate_axiom_Contains(e); + } else if (u.str.is_index(a)) { + instantiate_axiom_Indexof(e); + } else if (u.str.is_extract(a)) { + instantiate_axiom_Substr(e); + } else if (u.str.is_replace(a)) { + instantiate_axiom_Replace(e); + } else if (u.str.is_in_re(a)) { + instantiate_axiom_RegexIn(e); + } else { + TRACE("str", tout << "BUG: unhandled library-aware term " << mk_pp(e->get_owner(), get_manager()) << std::endl;); + NOT_IMPLEMENTED_YET(); + } + } + unsigned end_count = m_library_aware_axiom_todo.size(); + if (end_count > start_count) { + TRACE("str", tout << "new library-aware terms added during axiom setup -- checking again" << std::endl;); + continue; } else { - TRACE("str", tout << "BUG: unhandled library-aware term " << mk_pp(e->get_owner(), get_manager()) << std::endl;); - NOT_IMPLEMENTED_YET(); + break; } } m_library_aware_axiom_todo.reset(); - for (unsigned i = 0; i < m_delayed_axiom_setup_terms.size(); ++i) { + for (auto el : m_delayed_axiom_setup_terms) { // I think this is okay - ctx.internalize(m_delayed_axiom_setup_terms[i].get(), false); - set_up_axioms(m_delayed_axiom_setup_terms[i].get()); + ctx.internalize(el, false); + set_up_axioms(el); } m_delayed_axiom_setup_terms.reset(); + + if (search_started) { + for (auto const& el : m_delayed_assertions_todo) { + assert_axiom(el); + } + m_delayed_assertions_todo.reset(); + } } } @@ -969,6 +1009,15 @@ namespace smt { TRACE("str", tout << "set up basic string axioms on " << mk_pp(str->get_owner(), m) << std::endl;); + { + sort * a_sort = m.get_sort(str->get_owner()); + sort * str_sort = u.str.mk_string_sort(); + if (a_sort != str_sort) { + TRACE("str", tout << "WARNING: not setting up string axioms on non-string term " << mk_pp(str->get_owner(), m) << std::endl;); + return; + } + } + // TESTING: attempt to avoid a crash here when a variable goes out of scope if (str->get_iscope_lvl() > ctx.get_scope_level()) { TRACE("str", tout << "WARNING: skipping axiom setup on out-of-scope string term" << std::endl;); @@ -977,6 +1026,7 @@ namespace smt { // generate a stronger axiom for constant strings app * a_str = str->get_owner(); + if (u.str.is_string(a_str)) { expr_ref len_str(m); len_str = mk_strlen(a_str); @@ -1204,6 +1254,12 @@ namespace smt { contains_map.push_back(ex); std::pair key = std::pair(str, substr); contain_pair_bool_map.insert(str, substr, ex); + if (!contain_pair_idx_map.contains(str)) { + contain_pair_idx_map.insert(str, std::set>()); + } + if (!contain_pair_idx_map.contains(substr)) { + contain_pair_idx_map.insert(substr, std::set>()); + } contain_pair_idx_map[str].insert(key); contain_pair_idx_map[substr].insert(key); } @@ -1294,91 +1350,102 @@ namespace smt { expr_ref conclusion(m_autil.mk_ge(ex, zeroAst), m); expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m); SASSERT(containsAxiom); + // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent - m_delayed_axiom_setup_terms.push_back(containsAxiom); + //m_delayed_axiom_setup_terms.push_back(containsAxiom); } } - void theory_str::instantiate_axiom_Indexof_extended(enode * e) { + void theory_str::instantiate_axiom_Indexof_extended(enode * _e) { context & ctx = get_context(); ast_manager & m = get_manager(); - app * expr = e->get_owner(); - if (axiomatized_terms.contains(expr)) { - TRACE("str", tout << "already set up extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;); + app * e = _e->get_owner(); + if (axiomatized_terms.contains(e)) { + TRACE("str", tout << "already set up extended str.indexof axiom for " << mk_pp(e, m) << std::endl;); return; } - SASSERT(expr->get_num_args() == 3); - axiomatized_terms.insert(expr); + SASSERT(e->get_num_args() == 3); + axiomatized_terms.insert(e); - TRACE("str", tout << "instantiate extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;); + TRACE("str", tout << "instantiate extended str.indexof axiom for " << mk_pp(e, m) << std::endl;); - // ------------------------------------------------------------------------------- - // if (arg[2] >= length(arg[0])) // ite2 - // resAst = -1 - // else - // args[0] = prefix . suffix - // /\ indexAst = indexof(suffix, arg[1]) - // /\ args[2] = len(prefix) - // /\ if (indexAst == -1) resAst = indexAst // ite3 - // else resAst = args[2] + indexAst - // ------------------------------------------------------------------------------- + // str.indexof(H, N, i): + // i < 0 --> -1 + // i == 0 --> str.indexof(H, N, 0) + // i >= len(H) --> -1 + // 0 < i < len(H) --> + // H = hd ++ tl + // len(hd) = i + // str.indexof(tl, N, 0) - expr_ref resAst(mk_int_var("res"), m); - expr_ref indexAst(mk_int_var("index"), m); - expr_ref prefix(mk_str_var("prefix"), m); - expr_ref suffix(mk_str_var("suffix"), m); - expr_ref prefixLen(mk_strlen(prefix), m); - expr_ref zeroAst(mk_int(0), m); - expr_ref negOneAst(mk_int(-1), m); + expr * H; // "haystack" + expr * N; // "needle" + expr * i; // start index + u.str.is_index(e, H, N, i); - expr_ref ite3(m.mk_ite( - ctx.mk_eq_atom(indexAst, negOneAst), - ctx.mk_eq_atom(resAst, negOneAst), - ctx.mk_eq_atom(resAst, m_autil.mk_add(expr->get_arg(2), indexAst)) - ),m); + expr_ref minus_one(m_autil.mk_numeral(rational::minus_one(), true), m); + expr_ref zero(m_autil.mk_numeral(rational::zero(), true), m); - expr_ref_vector ite2ElseItems(m); - ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(prefix, suffix))); - ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1)))); - ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen)); - ite2ElseItems.push_back(ite3); - expr_ref ite2Else(mk_and(ite2ElseItems), m); - SASSERT(ite2Else); + // case split - expr_ref ite2(m.mk_ite( - //m_autil.mk_ge(expr->get_arg(2), mk_strlen(expr->get_arg(0))), - m_autil.mk_ge(m_autil.mk_add(expr->get_arg(2), m_autil.mk_mul(mk_int(-1), mk_strlen(expr->get_arg(0)))), zeroAst), - ctx.mk_eq_atom(resAst, negOneAst), - ite2Else - ), m); - SASSERT(ite2); + // case 1: i < 0 + { + expr_ref premise(m_autil.mk_le(i, minus_one), m); + expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m); + assert_implication(premise, conclusion); + } - expr_ref ite1(m.mk_ite( - //m_autil.mk_lt(expr->get_arg(2), zeroAst), - mk_not(m, m_autil.mk_ge(expr->get_arg(2), zeroAst)), - ctx.mk_eq_atom(resAst, mk_indexof(expr->get_arg(0), expr->get_arg(1))), - ite2 - ), m); - SASSERT(ite1); - assert_axiom(ite1); + // case 2: i = 0 + { + expr_ref premise(ctx.mk_eq_atom(i, zero), m); + // reduction to simpler case + expr_ref conclusion(ctx.mk_eq_atom(e, mk_indexof(H, N)), m); + assert_implication(premise, conclusion); + } + // case 3: i >= len(H) + { + //expr_ref _premise(m_autil.mk_ge(i, mk_strlen(H)), m); + //expr_ref premise(_premise); + //th_rewriter rw(m); + //rw(premise); + expr_ref premise(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero), m); + expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m); + assert_implication(premise, conclusion); + } + // case 4: 0 < i < len(H) + { + expr_ref premise1(m_autil.mk_gt(i, zero), m); + //expr_ref premise2(m_autil.mk_lt(i, mk_strlen(H)), m); + expr_ref premise2(m.mk_not(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero)), m); + expr_ref _premise(m.mk_and(premise1, premise2), m); + expr_ref premise(_premise); + th_rewriter rw(m); + rw(premise); - expr_ref reduceTerm(ctx.mk_eq_atom(expr, resAst), m); - SASSERT(reduceTerm); - assert_axiom(reduceTerm); + expr_ref hd(mk_str_var("hd"), m); + expr_ref tl(mk_str_var("tl"), m); + + expr_ref_vector conclusion_terms(m); + conclusion_terms.push_back(ctx.mk_eq_atom(H, mk_concat(hd, tl))); + conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(hd), i)); + conclusion_terms.push_back(ctx.mk_eq_atom(e, mk_indexof(tl, N))); + + expr_ref conclusion(mk_and(conclusion_terms), m); + assert_implication(premise, conclusion); + } { // heuristic: integrate with str.contains information // (but don't introduce it if it isn't already in the instance) - expr_ref haystack(expr->get_arg(0), m), needle(expr->get_arg(1), m), startIdx(expr->get_arg(2), m); // (H contains N) <==> (H indexof N, i) >= 0 - expr_ref premise(u.str.mk_contains(haystack, needle), m); + expr_ref premise(u.str.mk_contains(H, N), m); ctx.internalize(premise, false); - expr_ref conclusion(m_autil.mk_ge(expr, zeroAst), m); + expr_ref conclusion(m_autil.mk_ge(e, zero), m); expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m); SASSERT(containsAxiom); // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent - m_delayed_axiom_setup_terms.push_back(containsAxiom); + m_delayed_assertions_todo.push_back(containsAxiom); } } @@ -2378,9 +2445,8 @@ namespace smt { } else { expr_ref_vector items(m); int pos = 0; - std::map::iterator itor = resolvedMap.begin(); - for (; itor != resolvedMap.end(); ++itor) { - items.push_back(ctx.mk_eq_atom(itor->first, itor->second)); + for (auto itor : resolvedMap) { + items.push_back(ctx.mk_eq_atom(itor.first, itor.second)); pos += 1; } expr_ref premise(mk_and(items), m); @@ -2556,8 +2622,7 @@ namespace smt { context & ctx = get_context(); // pull each literal out of the arrangement disjunction literal_vector ls; - for (unsigned i = 0; i < terms.size(); ++i) { - expr * e = terms.get(i); + for (expr * e : terms) { literal l = ctx.get_literal(e); ls.push_back(l); } @@ -4495,8 +4560,7 @@ namespace smt { } } - for (std::list::iterator itor = overlapLen.begin(); itor != overlapLen.end(); itor++) { - unsigned int overLen = *itor; + for (unsigned int overLen : overlapLen) { zstring prefix = str1Value.extract(0, str1Len - overLen); zstring suffix = str2Value.extract(overLen, str2Len - overLen); @@ -4577,10 +4641,10 @@ namespace smt { TRACE("str", tout << "concat = " << mk_pp(concat, mgr) << ", unroll = " << mk_pp(unroll, mgr) << std::endl;); - std::pair key = std::make_pair(concat, unroll); expr_ref toAssert(mgr); + expr * _toAssert; - if (concat_eq_unroll_ast_map.find(key) == concat_eq_unroll_ast_map.end()) { + if (!concat_eq_unroll_ast_map.find(concat, unroll, _toAssert)) { expr_ref arg1(to_app(concat)->get_arg(0), mgr); expr_ref arg2(to_app(concat)->get_arg(1), mgr); expr_ref r1(to_app(unroll)->get_arg(0), mgr); @@ -4631,9 +4695,9 @@ namespace smt { toAssert = mgr.mk_and(opAnd1, opAnd2); m_trail.push_back(toAssert); - concat_eq_unroll_ast_map[key] = toAssert; + concat_eq_unroll_ast_map.insert(concat, unroll, toAssert); } else { - toAssert = concat_eq_unroll_ast_map[key]; + toAssert = _toAssert; } assert_axiom(toAssert); @@ -4917,11 +4981,10 @@ namespace smt { expr_ref_vector litems(m); - if (contain_pair_idx_map.find(varNode) != contain_pair_idx_map.end()) { - std::set >::iterator itor1 = contain_pair_idx_map[varNode].begin(); - for (; itor1 != contain_pair_idx_map[varNode].end(); ++itor1) { - expr * strAst = itor1->first; - expr * substrAst = itor1->second; + if (contain_pair_idx_map.contains(varNode)) { + for (auto entry : contain_pair_idx_map[varNode]) { + expr * strAst = entry.first; + expr * substrAst = entry.second; expr * boolVar = nullptr; if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) { @@ -4979,23 +5042,18 @@ namespace smt { // collect eqc concat std::set eqcConcats; get_concats_in_eqc(substrAst, eqcConcats); - for (std::set::iterator concatItor = eqcConcats.begin(); - concatItor != eqcConcats.end(); concatItor++) { + for (expr * aConcat : eqcConcats) { expr_ref_vector constList(m); bool counterEgFound = false; - // get constant strings in concat - expr * aConcat = *concatItor; get_const_str_asts_in_node(aConcat, constList); - for (expr_ref_vector::iterator cstItor = constList.begin(); - cstItor != constList.end(); cstItor++) { + for (auto const& cst : constList) { zstring pieceStr; - u.str.is_string(*cstItor, pieceStr); + u.str.is_string(cst, pieceStr); if (!strConst.contains(pieceStr)) { counterEgFound = true; if (aConcat != substrAst) { litems.push_back(ctx.mk_eq_atom(substrAst, aConcat)); } - //implyR = Z3_mk_eq(ctx, boolVar, Z3_mk_false(ctx)); implyR = mk_not(m, boolVar); break; } @@ -5054,11 +5112,10 @@ namespace smt { ast_manager & m = get_manager(); expr_ref_vector litems(m); - if (contain_pair_idx_map.find(varNode) != contain_pair_idx_map.end()) { - std::set >::iterator itor1 = contain_pair_idx_map[varNode].begin(); - for (; itor1 != contain_pair_idx_map[varNode].end(); ++itor1) { - expr * strAst = itor1->first; - expr * substrAst = itor1->second; + if (contain_pair_idx_map.contains(varNode)) { + for (auto entry : contain_pair_idx_map[varNode]) { + expr * strAst = entry.first; + expr * substrAst = entry.second; expr * boolVar = nullptr; if (!contain_pair_bool_map.find(strAst, substrAst, boolVar)) { @@ -5087,17 +5144,16 @@ namespace smt { zstring strConst; u.str.is_string(strValue, strConst); // iterate eqc (also eqc-to-be) of substr - for (expr_ref_vector::iterator itAst = willEqClass.begin(); itAst != willEqClass.end(); itAst++) { + for (auto itAst : willEqClass) { bool counterEgFound = false; - if (u.str.is_concat(to_app(*itAst))) { + if (u.str.is_concat(to_app(itAst))) { expr_ref_vector constList(m); // get constant strings in concat - app * aConcat = to_app(*itAst); + app * aConcat = to_app(itAst); get_const_str_asts_in_node(aConcat, constList); - for (expr_ref_vector::iterator cstItor = constList.begin(); - cstItor != constList.end(); cstItor++) { + for (auto cst : constList) { zstring pieceStr; - u.str.is_string(*cstItor, pieceStr); + u.str.is_string(cst, pieceStr); if (!strConst.contains(pieceStr)) { TRACE("str", tout << "Inconsistency found!" << std::endl;); counterEgFound = true; @@ -5122,7 +5178,7 @@ namespace smt { } bool theory_str::in_contain_idx_map(expr * n) { - return contain_pair_idx_map.find(n) != contain_pair_idx_map.end(); + return contain_pair_idx_map.contains(n); } void theory_str::check_contain_by_eq_nodes(expr * n1, expr * n2) { @@ -5130,12 +5186,9 @@ namespace smt { ast_manager & m = get_manager(); if (in_contain_idx_map(n1) && in_contain_idx_map(n2)) { - std::set >::iterator keysItor1 = contain_pair_idx_map[n1].begin(); - std::set >::iterator keysItor2; - - for (; keysItor1 != contain_pair_idx_map[n1].end(); keysItor1++) { + for (auto const& key1 : contain_pair_idx_map[n1]) { // keysItor1 is on set {<.., n1>, ..., , ...} - std::pair key1 = *keysItor1; + //std::pair key1 = *keysItor1; if (key1.first == n1 && key1.second == n2) { expr_ref implyL(m); expr_ref implyR(contain_pair_bool_map[key1], m); @@ -5147,10 +5200,10 @@ namespace smt { } } - for (keysItor2 = contain_pair_idx_map[n2].begin(); - keysItor2 != contain_pair_idx_map[n2].end(); keysItor2++) { + //for (keysItor2 = contain_pair_idx_map[n2].begin(); keysItor2 != contain_pair_idx_map[n2].end(); keysItor2++) { + for (auto const& key2 : contain_pair_idx_map[n2]) { // keysItor2 is on set {<.., n2>, ..., , ...} - std::pair key2 = *keysItor2; + //std::pair key2 = *keysItor2; // skip if the pair is eq if (key1 == key2) { continue; @@ -5244,10 +5297,12 @@ namespace smt { // * key1.first = key2.first // check eqc(key1.second) and eqc(key2.second) // ----------------------------------------------------------- - expr_ref_vector::iterator eqItorSub1 = subAst1Eqc.begin(); - for (; eqItorSub1 != subAst1Eqc.end(); eqItorSub1++) { - expr_ref_vector::iterator eqItorSub2 = subAst2Eqc.begin(); - for (; eqItorSub2 != subAst2Eqc.end(); eqItorSub2++) { + //expr_ref_vector::iterator eqItorSub1 = subAst1Eqc.begin(); + //for (; eqItorSub1 != subAst1Eqc.end(); eqItorSub1++) { + for (auto eqSubVar1 : subAst1Eqc) { + //expr_ref_vector::iterator eqItorSub2 = subAst2Eqc.begin(); + //for (; eqItorSub2 != subAst2Eqc.end(); eqItorSub2++) { + for (auto eqSubVar2 : subAst2Eqc) { // ------------ // key1.first = key2.first /\ containPairBoolMap[] // ==> (containPairBoolMap[key1] --> containPairBoolMap[key2]) @@ -5257,11 +5312,11 @@ namespace smt { if (n1 != n2) { litems3.push_back(ctx.mk_eq_atom(n1, n2)); } - expr * eqSubVar1 = *eqItorSub1; + if (eqSubVar1 != subAst1) { litems3.push_back(ctx.mk_eq_atom(subAst1, eqSubVar1)); } - expr * eqSubVar2 = *eqItorSub2; + if (eqSubVar2 != subAst2) { litems3.push_back(ctx.mk_eq_atom(subAst2, eqSubVar2)); } @@ -5282,11 +5337,11 @@ namespace smt { if (n1 != n2) { litems4.push_back(ctx.mk_eq_atom(n1, n2)); } - expr * eqSubVar1 = *eqItorSub1; + if (eqSubVar1 != subAst1) { litems4.push_back(ctx.mk_eq_atom(subAst1, eqSubVar1)); } - expr * eqSubVar2 = *eqItorSub2; + if (eqSubVar2 != subAst2) { litems4.push_back(ctx.mk_eq_atom(subAst2, eqSubVar2)); } @@ -5394,20 +5449,18 @@ namespace smt { // * key1.second = key2.second // check eqc(key1.first) and eqc(key2.first) // ----------------------------------------------------------- - expr_ref_vector::iterator eqItorStr1 = str1Eqc.begin(); - for (; eqItorStr1 != str1Eqc.end(); eqItorStr1++) { - expr_ref_vector::iterator eqItorStr2 = str2Eqc.begin(); - for (; eqItorStr2 != str2Eqc.end(); eqItorStr2++) { + for (auto const& eqStrVar1 : str1Eqc) { + for (auto const& eqStrVar2 : str2Eqc) { { expr_ref_vector litems3(m); if (n1 != n2) { litems3.push_back(ctx.mk_eq_atom(n1, n2)); } - expr * eqStrVar1 = *eqItorStr1; + if (eqStrVar1 != str1) { litems3.push_back(ctx.mk_eq_atom(str1, eqStrVar1)); } - expr * eqStrVar2 = *eqItorStr2; + if (eqStrVar2 != str2) { litems3.push_back(ctx.mk_eq_atom(str2, eqStrVar2)); } @@ -5430,11 +5483,9 @@ namespace smt { if (n1 != n2) { litems4.push_back(ctx.mk_eq_atom(n1, n2)); } - expr * eqStrVar1 = *eqItorStr1; if (eqStrVar1 != str1) { litems4.push_back(ctx.mk_eq_atom(str1, eqStrVar1)); } - expr *eqStrVar2 = *eqItorStr2; if (eqStrVar2 != str2) { litems4.push_back(ctx.mk_eq_atom(str2, eqStrVar2)); } @@ -5480,8 +5531,7 @@ namespace smt { expr * constStrAst = (constStrAst_1 != nullptr) ? constStrAst_1 : constStrAst_2; TRACE("str", tout << "eqc of n1 is {"; - for (expr_ref_vector::iterator it = willEqClass.begin(); it != willEqClass.end(); ++it) { - expr * el = *it; + for (expr * el : willEqClass) { tout << " " << mk_pp(el, m); } tout << std::endl; @@ -5494,12 +5544,11 @@ namespace smt { // step 1: we may have constant values for Contains checks now if (constStrAst != nullptr) { - expr_ref_vector::iterator itAst = willEqClass.begin(); - for (; itAst != willEqClass.end(); itAst++) { - if (*itAst == constStrAst) { + for (auto a : willEqClass) { + if (a == constStrAst) { continue; } - check_contain_by_eqc_val(*itAst, constStrAst); + check_contain_by_eqc_val(a, constStrAst); } } else { // no concrete value to be put in eqc, solely based on context @@ -5511,9 +5560,8 @@ namespace smt { // * "EQC(M) U EQC(concat(..., "jio", ...))" as substr and // * If strAst registered has an eqc constant in the context // ------------------------------------------------------------- - expr_ref_vector::iterator itAst = willEqClass.begin(); - for (; itAst != willEqClass.end(); ++itAst) { - check_contain_by_substr(*itAst, willEqClass); + for (auto a : willEqClass) { + check_contain_by_substr(a, willEqClass); } } @@ -5530,12 +5578,8 @@ namespace smt { // (9) containPairBoolMap[] /\ m = n ==> (b1 -> b2) // ------------------------------------------ - expr_ref_vector::iterator varItor1 = willEqClass.begin(); - for (; varItor1 != willEqClass.end(); ++varItor1) { - expr * varAst1 = *varItor1; - expr_ref_vector::iterator varItor2 = varItor1; - for (; varItor2 != willEqClass.end(); ++varItor2) { - expr * varAst2 = *varItor2; + for (auto varAst1 : willEqClass) { + for (auto varAst2 : willEqClass) { check_contain_by_eq_nodes(varAst1, varAst2); } } @@ -5849,11 +5893,10 @@ namespace smt { std::map & concatAliasMap, std::map & varConstMap, std::map & concatConstMap, std::map > & varEqConcatMap) { std::map, std::set > > groundedMap; - theory_str_contain_pair_bool_map_t::iterator containItor = contain_pair_bool_map.begin(); - for (; containItor != contain_pair_bool_map.end(); containItor++) { - expr* containBoolVar = containItor->get_value(); - expr* str = containItor->get_key1(); - expr* subStr = containItor->get_key2(); + for (auto const& kv : contain_pair_bool_map) { + expr* containBoolVar = kv.get_value(); + expr* str = kv.get_key1(); + expr* subStr = kv.get_key2(); expr* strDeAlias = dealias_node(str, varAliasMap, concatAliasMap); expr* subStrDeAlias = dealias_node(subStr, varAliasMap, concatAliasMap); @@ -6455,7 +6498,7 @@ namespace smt { } else { expr_ref_vector::iterator itor = eqNodeSet.begin(); for (; itor != eqNodeSet.end(); itor++) { - if (regex_in_var_reg_str_map.find(*itor) != regex_in_var_reg_str_map.end()) { + if (regex_in_var_reg_str_map.contains(*itor)) { std::set::iterator strItor = regex_in_var_reg_str_map[*itor].begin(); for (; strItor != regex_in_var_reg_str_map[*itor].end(); strItor++) { zstring regStr = *strItor; @@ -6914,12 +6957,12 @@ namespace smt { if (!map_effectively_empty) { map_effectively_empty = true; - ptr_vector indicator_set = fvar_lenTester_map[v]; - for (ptr_vector::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) { - expr * indicator = *it; - if (internal_variable_set.find(indicator) != internal_variable_set.end()) { - map_effectively_empty = false; - break; + if (fvar_lenTester_map.contains(v)) { + for (expr * indicator : fvar_lenTester_map[v]) { + if (internal_variable_set.contains(indicator)) { + map_effectively_empty = false; + break; + } } } } @@ -6964,16 +7007,19 @@ namespace smt { } // now create a fake length tester over this finite disjunction of lengths - fvar_len_count_map[v] = 1; + fvar_len_count_map.insert(v, 1); unsigned int testNum = fvar_len_count_map[v]; expr_ref indicator(mk_internal_lenTest_var(v, testNum), m); SASSERT(indicator); m_trail.push_back(indicator); + if (!fvar_lenTester_map.contains(v)) { + fvar_lenTester_map.insert(v, ptr_vector()); + } fvar_lenTester_map[v].shrink(0); fvar_lenTester_map[v].push_back(indicator); - lenTester_fvar_map[indicator] = v; + lenTester_fvar_map.insert(indicator, v); expr_ref_vector orList(m); expr_ref_vector andList(m); @@ -7040,7 +7086,12 @@ namespace smt { } } } else { - int lenTesterCount = fvar_lenTester_map[fVar].size(); + int lenTesterCount; + if (fvar_lenTester_map.contains(fVar)) { + lenTesterCount = fvar_lenTester_map[fVar].size(); + } else { + lenTesterCount = 0; + } expr * effectiveLenInd = nullptr; zstring effectiveLenIndiStr = ""; @@ -7411,8 +7462,7 @@ namespace smt { if (is_app(ex)) { app * ap = to_app(ex); - // TODO indexof2/lastindexof - if (u.str.is_index(ap) /* || is_Indexof2(ap) || is_LastIndexof(ap) */) { + if (u.str.is_index(ap)) { m_library_aware_axiom_todo.push_back(n); } else if (u.str.is_stoi(ap)) { TRACE("str", tout << "found string-integer conversion term: " << mk_pp(ex, get_manager()) << std::endl;); @@ -7945,11 +7995,12 @@ namespace smt { // Step 1: get variables / concat AST appearing in the context // the thing we iterate over should just be variable_set - internal_variable_set // so we avoid computing the set difference (but this might be slower) - for(obj_hashtable::iterator it = variable_set.begin(); it != variable_set.end(); ++it) { - expr* var = *it; + for (expr* var : variable_set) { + //for(obj_hashtable::iterator it = variable_set.begin(); it != variable_set.end(); ++it) { + //expr* var = *it; if (internal_variable_set.find(var) == internal_variable_set.end()) { TRACE("str", tout << "new variable: " << mk_pp(var, m) << std::endl;); - strVarMap[*it] = 1; + strVarMap[var] = 1; } } classify_ast_by_type_in_positive_context(strVarMap, concatMap, unrollMap); @@ -8977,12 +9028,12 @@ namespace smt { CTRACE("str", needToAssignFreeVars, tout << "Need to assign values to the following free variables:" << std::endl; - for (std::set::iterator itx = free_variables.begin(); itx != free_variables.end(); ++itx) { - tout << mk_ismt2_pp(*itx, m) << std::endl; + for (expr* v : free_variables) { + tout << mk_ismt2_pp(v, m) << std::endl; } tout << "freeVar_map has the following entries:" << std::endl; - for (std::map::iterator fvIt = freeVar_map.begin(); fvIt != freeVar_map.end(); fvIt++) { - expr * var = fvIt->first; + for (auto const& kv : freeVar_map) { + expr * var = kv.first; tout << mk_ismt2_pp(var, m) << std::endl; } ); @@ -9360,13 +9411,12 @@ namespace smt { // check whether any value tester is actually in scope TRACE("str", tout << "checking scope of previous value testers" << std::endl;); bool map_effectively_empty = true; - if (fvar_valueTester_map[freeVar].find(len) != fvar_valueTester_map[freeVar].end()) { + if (fvar_valueTester_map.contains(freeVar) && + fvar_valueTester_map[freeVar].find(len) != fvar_valueTester_map[freeVar].end()) { // there's *something* in the map, but check its scope - svector > entries = fvar_valueTester_map[freeVar][len]; - for (svector >::iterator it = entries.begin(); it != entries.end(); ++it) { - std::pair entry = *it; + for (auto const& entry : fvar_valueTester_map[freeVar][len]) { expr * aTester = entry.second; - if (internal_variable_set.find(aTester) == internal_variable_set.end()) { + if (!internal_variable_set.contains(aTester)) { TRACE("str", tout << mk_pp(aTester, m) << " out of scope" << std::endl;); } else { TRACE("str", tout << mk_pp(aTester, m) << " in scope" << std::endl;); @@ -9381,6 +9431,9 @@ namespace smt { int tries = 0; expr * val_indicator = mk_internal_valTest_var(freeVar, len, tries); valueTester_fvar_map.insert(val_indicator, freeVar); + if (!fvar_valueTester_map.contains(freeVar)) { + fvar_valueTester_map.insert(freeVar, std::map > >()); + } fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, val_indicator)); print_value_tester_list(fvar_valueTester_map[freeVar][len]); return gen_val_options(freeVar, len_indicator, val_indicator, len_valueStr, tries); @@ -9396,7 +9449,7 @@ namespace smt { expr * aTester = fvar_valueTester_map[freeVar][len][i].second; // it's probably worth checking scope here, actually - if (internal_variable_set.find(aTester) == internal_variable_set.end()) { + if (!internal_variable_set.contains(aTester)) { TRACE("str", tout << "value tester " << mk_pp(aTester, m) << " out of scope, skipping" << std::endl;); continue; } @@ -9721,8 +9774,8 @@ namespace smt { int dist = opt_LCMUnrollStep; expr_ref_vector litems(mgr); expr_ref moreAst(mk_string("more"), mgr); - for (std::set::iterator itor = unrolls.begin(); itor != unrolls.end(); itor++) { - expr_ref item(ctx.mk_eq_atom(var, *itor), mgr); + for (expr * e : unrolls) { + expr_ref item(ctx.mk_eq_atom(var, e), mgr); TRACE("str", tout << "considering unroll " << mk_pp(item, mgr) << std::endl;); litems.push_back(item); } @@ -9731,10 +9784,8 @@ namespace smt { ptr_vector outOfScopeTesters; - for (ptr_vector::iterator it = unroll_tries_map[var][unrolls].begin(); - it != unroll_tries_map[var][unrolls].end(); ++it) { - expr * tester = *it; - bool inScope = (internal_unrollTest_vars.find(tester) != internal_unrollTest_vars.end()); + for (expr * tester : unroll_tries_map[var][unrolls]) { + bool inScope = internal_unrollTest_vars.contains(tester); TRACE("str", tout << "unroll test var " << mk_pp(tester, mgr) << (inScope ? " in scope" : " out of scope") << std::endl;); @@ -9743,12 +9794,10 @@ namespace smt { } } - for (ptr_vector::iterator it = outOfScopeTesters.begin(); - it != outOfScopeTesters.end(); ++it) { - unroll_tries_map[var][unrolls].erase(*it); + for (expr* e : outOfScopeTesters) { + unroll_tries_map[var][unrolls].erase(e); } - if (unroll_tries_map[var][unrolls].size() == 0) { unroll_tries_map[var][unrolls].push_back(mk_unroll_test_var()); } @@ -10264,14 +10313,14 @@ namespace smt { // assume empty and find a counterexample map_effectively_empty = true; - ptr_vector indicator_set = fvar_lenTester_map[freeVar]; - for (ptr_vector::iterator it = indicator_set.begin(); it != indicator_set.end(); ++it) { - expr * indicator = *it; - if (internal_variable_set.find(indicator) != internal_variable_set.end()) { - TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m) - << " in fvar_lenTester_map[freeVar]" << std::endl;); - map_effectively_empty = false; - break; + if (fvar_lenTester_map.contains(freeVar)) { + for (expr * indicator : fvar_lenTester_map[freeVar]) { + if (internal_variable_set.find(indicator) != internal_variable_set.end()) { + TRACE("str", tout <<"found active internal variable " << mk_ismt2_pp(indicator, m) + << " in fvar_lenTester_map[freeVar]" << std::endl;); + map_effectively_empty = false; + break; + } } } CTRACE("str", map_effectively_empty, tout << "all variables in fvar_lenTester_map[freeVar] out of scope" << std::endl;); @@ -10288,6 +10337,9 @@ namespace smt { SASSERT(indicator); // since the map is "effectively empty", we can remove those variables that have left scope... + if (!fvar_lenTester_map.contains(freeVar)) { + fvar_lenTester_map.insert(freeVar, ptr_vector()); + } fvar_lenTester_map[freeVar].shrink(0); fvar_lenTester_map[freeVar].push_back(indicator); lenTester_fvar_map.insert(indicator, freeVar); @@ -10300,7 +10352,12 @@ namespace smt { expr * effectiveLenInd = nullptr; zstring effectiveLenIndiStr(""); - int lenTesterCount = (int) fvar_lenTester_map[freeVar].size(); + int lenTesterCount; + if (fvar_lenTester_map.contains(freeVar)) { + lenTesterCount = fvar_lenTester_map[freeVar].size(); + } else { + lenTesterCount = 0; + } TRACE("str", tout << lenTesterCount << " length testers in fvar_lenTester_map[" << mk_pp(freeVar, m) << "]:" << std::endl; @@ -10437,14 +10494,14 @@ namespace smt { void theory_str::process_free_var(std::map & freeVar_map) { context & ctx = get_context(); - std::set eqcRepSet; - std::set leafVarSet; - std::map > aloneVars; + obj_hashtable eqcRepSet; + obj_hashtable leafVarSet; + std::map > aloneVars; - for (std::map::iterator fvIt = freeVar_map.begin(); fvIt != freeVar_map.end(); fvIt++) { - expr * freeVar = fvIt->first; + for (auto const& kv : freeVar_map) { + expr * freeVar = kv.first; // skip all regular expression vars - if (regex_variable_set.find(freeVar) != regex_variable_set.end()) { + if (regex_variable_set.contains(freeVar)) { continue; } @@ -10454,10 +10511,10 @@ namespace smt { get_var_in_eqc(freeVar, eqVarSet); bool duplicated = false; expr * dupVar = nullptr; - for (std::set::iterator itorEqv = eqVarSet.begin(); itorEqv != eqVarSet.end(); itorEqv++) { - if (eqcRepSet.find(*itorEqv) != eqcRepSet.end()) { + for (expr* eq : eqVarSet) { + if (eqcRepSet.contains(eq)) { duplicated = true; - dupVar = *itorEqv; + dupVar = eq; break; } } @@ -10470,13 +10527,9 @@ namespace smt { } } - for (std::set::iterator fvIt = eqcRepSet.begin(); fvIt != eqcRepSet.end(); fvIt++) { - bool standAlone = true; - expr * freeVar = *fvIt; + for (expr * freeVar : eqcRepSet) { // has length constraint initially - if (input_var_in_len.find(freeVar) != input_var_in_len.end()) { - standAlone = false; - } + bool standAlone = !input_var_in_len.contains(freeVar); // iterate parents if (standAlone) { // I hope this works! @@ -10507,25 +10560,19 @@ namespace smt { } } - for(std::set::iterator itor1 = leafVarSet.begin(); - itor1 != leafVarSet.end(); ++itor1) { - expr * toAssert = gen_len_val_options_for_free_var(*itor1, nullptr, ""); + for (expr* lv : leafVarSet) { + expr * toAssert = gen_len_val_options_for_free_var(lv, nullptr, ""); // gen_len_val_options_for_free_var() can legally return NULL, // as methods that it calls may assert their own axioms instead. - if (toAssert != nullptr) { - assert_axiom(toAssert); - } + if (toAssert) assert_axiom(toAssert); + } - for (std::map >::iterator mItor = aloneVars.begin(); - mItor != aloneVars.end(); ++mItor) { - std::set::iterator itor2 = mItor->second.begin(); - for(; itor2 != mItor->second.end(); ++itor2) { - expr * toAssert = gen_len_val_options_for_free_var(*itor2, nullptr, ""); + for (auto const& kv : aloneVars) { + for (expr* av : kv.second) { + expr * toAssert = gen_len_val_options_for_free_var(av, nullptr, ""); // same deal with returning a NULL axiom here - if(toAssert != nullptr) { - assert_axiom(toAssert); - } + if (toAssert) assert_axiom(toAssert); } } } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 508a1c905..5378b05f3 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -262,6 +262,7 @@ protected: ptr_vector m_concat_axiom_todo; ptr_vector m_string_constant_length_todo; ptr_vector m_concat_eval_todo; + expr_ref_vector m_delayed_assertions_todo; // enode lists for library-aware/high-level string terms (e.g. substr, contains) ptr_vector m_library_aware_axiom_todo; @@ -295,33 +296,30 @@ protected: obj_hashtable input_var_in_len; obj_map fvar_len_count_map; - std::map > fvar_lenTester_map; + obj_map > fvar_lenTester_map; obj_map lenTester_fvar_map; - // TBD: need to replace by obj_map for determinism - std::map > > > fvar_valueTester_map; + + obj_map > > > fvar_valueTester_map; + obj_map valueTester_fvar_map; obj_map val_range_map; // This can't be an expr_ref_vector because the constructor is wrong, // we would need to modify the allocator so we pass in ast_manager - // TBD: need to replace by obj_map for determinism - std::map, ptr_vector > > unroll_tries_map; + obj_map, ptr_vector > > unroll_tries_map; obj_map unroll_var_map; - // TBD: need to replace by obj_pair_map for determinism - std::map, expr*> concat_eq_unroll_ast_map; + obj_pair_map concat_eq_unroll_ast_map; expr_ref_vector contains_map; theory_str_contain_pair_bool_map_t contain_pair_bool_map; - //obj_map > contain_pair_idx_map; - std::map > > contain_pair_idx_map; + obj_map > > contain_pair_idx_map; // TBD: do a curried map for determinism. std::map, expr*> regex_in_bool_map; - // TBD: need to replace by obj_map for determinism - std::map > regex_in_var_reg_str_map; + obj_map > regex_in_var_reg_str_map; obj_map regex_nfa_cache; // Regex term --> NFA svector char_set; diff --git a/src/util/hashtable.h b/src/util/hashtable.h index 742438814..cea74f466 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -600,9 +600,8 @@ public: core_hashtable& operator|=(core_hashtable const& other) { if (this == &other) return *this; - iterator i = other.begin(), e = other.end(); - for (; i != e; ++i) { - insert(*i); + for (const data& d : other) { + insert(d); } return *this; } @@ -610,10 +609,9 @@ public: core_hashtable& operator&=(core_hashtable const& other) { if (this == &other) return *this; core_hashtable copy(*this); - iterator i = copy.begin(), e = copy.end(); - for (; i != e; ++i) { - if (!other.contains(*i)) { - remove(*i); + for (const data& d : copy) { + if (!other.contains(d)) { + remove(d); } } return *this; @@ -622,9 +620,8 @@ public: core_hashtable& operator=(core_hashtable const& other) { if (this == &other) return *this; reset(); - iterator i = other.begin(), e = other.end(); - for (; i != e; ++i) { - insert(*i); + for (const data& d : other) { + insert(d); } return *this; }