mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
Merge branch 'master' of https://github.com/Z3Prover/z3
This commit is contained in:
Christoph M. Wintersteiger
commit
932ba15261
33 changed files with 594 additions and 312 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 |
|
||||
| ----------- | ----------- | ---------- | ---------- | --- | -------- |
|
||||
[](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [](https://travis-ci.org/Z3Prover/z3)
|
||||
| Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | OSX | TravisCI |
|
||||
| ----------- | ----------- | ----------- | ---------- | ---------- | --- | -------- |
|
||||
[](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=4) | [](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [](https://travis-ci.org/Z3Prover/z3)
|
||||
|
||||
[1]: #building-z3-on-windows-using-visual-studio-command-prompt
|
||||
[2]: #building-z3-using-make-and-gccclang
|
||||
|
|
|
|||
|
|
@ -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";
|
||||
|
|
|
|||
|
|
@ -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");
|
||||
|
||||
|
|
|
|||
|
|
@ -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')
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
|
|
|||
19
scripts/vsts-mac.sh
Normal file
19
scripts/vsts-mac.sh
Normal file
|
|
@ -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
|
||||
|
||||
49
scripts/vsts-vs2013.cmd
Normal file
49
scripts/vsts-vs2013.cmd
Normal file
|
|
@ -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"
|
||||
|
||||
51
scripts/vsts-vs2017.cmd
Normal file
51
scripts/vsts-vs2017.cmd
Normal file
|
|
@ -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"
|
||||
|
||||
|
|
@ -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<ast_manager> m_manager;
|
||||
scoped_ptr<cmd_context> 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_context>& 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; }
|
||||
|
|
|
|||
|
|
@ -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<cmd_context>& 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()));
|
||||
}
|
||||
};
|
||||
|
|
|
|||
|
|
@ -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<Z3_symbol> _names(n);
|
||||
array<Z3_sort> _sorts(n);
|
||||
for (unsigned i = 0; i < n; i++) { _names[i] = Z3_mk_string_symbol(*this, names[i]); _sorts[i] = sorts[i]; }
|
||||
array<Z3_func_decl> _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));
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
||||
|
|
|
|||
|
|
@ -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:
|
||||
|
||||
|
|
|
|||
|
|
@ -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')
|
||||
|
|
|
|||
|
|
@ -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):
|
||||
|
|
|
|||
|
|
@ -22,6 +22,7 @@ Notes:
|
|||
#define Z3_H_
|
||||
|
||||
#include <stdio.h>
|
||||
#include <stdbool.h>
|
||||
#include "z3_macros.h"
|
||||
#include "z3_api.h"
|
||||
#include "z3_ast_containers.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.
|
||||
|
||||
|
|
|
|||
|
|
@ -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<unsigned>(m_args[pos].m_uint);
|
||||
return reinterpret_cast<bool*>(m_unsigned_arrays[idx].c_ptr());
|
||||
}
|
||||
|
||||
Z3_symbol * get_symbol_array(unsigned pos) const {
|
||||
check_arg(pos, SYMBOL_ARRAY);
|
||||
unsigned idx = static_cast<unsigned>(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);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
||||
|
|
|
|||
|
|
@ -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());
|
||||
|
|
|
|||
|
|
@ -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<func_decl> const * get_datatype_constructors(sort * ty);
|
||||
unsigned get_datatype_num_constructors(sort * ty);
|
||||
unsigned get_datatype_num_parameter_sorts(sort * ty);
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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; }
|
||||
|
|
|
|||
|
|
@ -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 &) {
|
||||
|
|
|
|||
|
|
@ -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: {
|
||||
|
|
|
|||
|
|
@ -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();
|
||||
}
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
|
||||
display_literals(out, lits);
|
||||
display_literals_verbose(out, lits);
|
||||
break;
|
||||
}
|
||||
default:
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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<theory_seq, rational_set, rational>(m_stoi_axioms, val));
|
||||
|
|
|
|||
|
|
@ -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<expr> 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<enode> 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<enode*,enode*> 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<enode> 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<expr*, expr*> key = std::pair<expr*, expr*>(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<std::pair<expr*, expr*>>());
|
||||
}
|
||||
if (!contain_pair_idx_map.contains(substr)) {
|
||||
contain_pair_idx_map.insert(substr, std::set<std::pair<expr*, expr*>>());
|
||||
}
|
||||
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<expr*, expr*>::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<unsigned int>::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<expr*, expr*> 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<std::pair<expr*, expr*> >::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<expr*> eqcConcats;
|
||||
get_concats_in_eqc(substrAst, eqcConcats);
|
||||
for (std::set<expr*>::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<std::pair<expr*, expr*> >::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<std::pair<expr*, expr*> >::iterator keysItor1 = contain_pair_idx_map[n1].begin();
|
||||
std::set<std::pair<expr*, expr*> >::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>, ..., <n1, ...>, ...}
|
||||
std::pair<expr*, expr*> key1 = *keysItor1;
|
||||
//std::pair<expr*, expr*> 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>, ..., <n2, ...>, ...}
|
||||
std::pair<expr*, expr*> key2 = *keysItor2;
|
||||
//std::pair<expr*, expr*> 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[<eqc(key1.second), eqc(key2.second)>]
|
||||
// ==> (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[<eqc(y), eqc(x)>] /\ 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<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
|
||||
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap) {
|
||||
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > 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<zstring>::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<expr> indicator_set = fvar_lenTester_map[v];
|
||||
for (ptr_vector<expr>::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<expr>());
|
||||
}
|
||||
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<expr>::iterator it = variable_set.begin(); it != variable_set.end(); ++it) {
|
||||
expr* var = *it;
|
||||
for (expr* var : variable_set) {
|
||||
//for(obj_hashtable<expr>::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<expr*>::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<expr*, int>::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<std::pair<int, expr*> > entries = fvar_valueTester_map[freeVar][len];
|
||||
for (svector<std::pair<int,expr*> >::iterator it = entries.begin(); it != entries.end(); ++it) {
|
||||
std::pair<int,expr*> 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<int, svector<std::pair<int, expr*> > >());
|
||||
}
|
||||
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<expr*>::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<expr> outOfScopeTesters;
|
||||
|
||||
for (ptr_vector<expr>::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<expr>::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<expr> indicator_set = fvar_lenTester_map[freeVar];
|
||||
for (ptr_vector<expr>::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<expr>());
|
||||
}
|
||||
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<expr*, int> & freeVar_map) {
|
||||
context & ctx = get_context();
|
||||
|
||||
std::set<expr*> eqcRepSet;
|
||||
std::set<expr*> leafVarSet;
|
||||
std::map<int, std::set<expr*> > aloneVars;
|
||||
obj_hashtable<expr> eqcRepSet;
|
||||
obj_hashtable<expr> leafVarSet;
|
||||
std::map<int, obj_hashtable<expr> > aloneVars;
|
||||
|
||||
for (std::map<expr*, int>::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<expr*>::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<expr*>::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<expr*>::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<int, std::set<expr*> >::iterator mItor = aloneVars.begin();
|
||||
mItor != aloneVars.end(); ++mItor) {
|
||||
std::set<expr*>::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);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -262,6 +262,7 @@ protected:
|
|||
ptr_vector<enode> m_concat_axiom_todo;
|
||||
ptr_vector<enode> m_string_constant_length_todo;
|
||||
ptr_vector<enode> 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<enode> m_library_aware_axiom_todo;
|
||||
|
|
@ -295,33 +296,30 @@ protected:
|
|||
obj_hashtable<expr> input_var_in_len;
|
||||
|
||||
obj_map<expr, unsigned int> fvar_len_count_map;
|
||||
std::map<expr*, ptr_vector<expr> > fvar_lenTester_map;
|
||||
obj_map<expr, ptr_vector<expr> > fvar_lenTester_map;
|
||||
obj_map<expr, expr*> lenTester_fvar_map;
|
||||
|
||||
// TBD: need to replace by obj_map for determinism
|
||||
std::map<expr*, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
|
||||
|
||||
obj_map<expr, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
|
||||
|
||||
obj_map<expr, expr*> valueTester_fvar_map;
|
||||
|
||||
obj_map<expr, int_vector> 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<expr*, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
|
||||
obj_map<expr, std::map<std::set<expr*>, ptr_vector<expr> > > unroll_tries_map;
|
||||
obj_map<expr, expr*> unroll_var_map;
|
||||
// TBD: need to replace by obj_pair_map for determinism
|
||||
std::map<std::pair<expr*, expr*>, expr*> concat_eq_unroll_ast_map;
|
||||
obj_pair_map<expr, expr, expr*> concat_eq_unroll_ast_map;
|
||||
|
||||
expr_ref_vector contains_map;
|
||||
|
||||
theory_str_contain_pair_bool_map_t contain_pair_bool_map;
|
||||
//obj_map<expr, obj_pair_set<expr, expr> > contain_pair_idx_map;
|
||||
std::map<expr*, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
|
||||
obj_map<expr, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
|
||||
|
||||
// TBD: do a curried map for determinism.
|
||||
std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
|
||||
// TBD: need to replace by obj_map for determinism
|
||||
std::map<expr*, std::set<zstring> > regex_in_var_reg_str_map;
|
||||
obj_map<expr, std::set<zstring> > regex_in_var_reg_str_map;
|
||||
obj_map<expr, nfa> regex_nfa_cache; // Regex term --> NFA
|
||||
|
||||
svector<char> char_set;
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue