mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2017-08-17 20:28:56 -07:00
commit a3ccdaf318
38 changed files with 365 additions and 379 deletions
Download patch file Download diff file Expand all files Collapse all files

29
cmake/z3_add_component.cmake
View file

@ -36,15 +36,8 @@ function(z3_add_component_dependencies_to_target target_name)
# Remaing args should be component names
set(_expanded_deps ${ARGN})
foreach (dependency ${_expanded_deps})
# FIXME: Adding these include paths wouldn't be necessary if the sources
# used include paths rooted in the ``src`` directory.
get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
foreach (inc_dir ${_dep_include_dirs})
target_include_directories(${target_name} PRIVATE "${inc_dir}")
endforeach()
unset(_dep_include_dirs)
# Ensure this component's dependencies are built before this component.
# This important because we might need the generated header files in
# This is important because we might need the generated header files in
# other components.
add_dependencies(${target_name} ${dependency})
endforeach()
@ -214,18 +207,14 @@ macro(z3_add_component component_name)
target_compile_options(${component_name} PRIVATE ${flag})
endforeach()
# It's unfortunate that we have to manage the include directories and dependencies ourselves.
# It's unfortunate that we have to manage dependencies ourselves.
#
# If we weren't building "object" libraries we could use
# ```
# target_include_directories(${component_name} INTERFACE "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
# target_link_libraries(${component_name} INTERFACE ${Z3_MOD_COMPONENT_DEPENDENCIES})
# ```
# but we can't do that with "object" libraries.
# Record this component's include directories
set_property(GLOBAL PROPERTY Z3_${component_name}_INCLUDES "${CMAKE_CURRENT_SOURCE_DIR}")
set_property(GLOBAL APPEND PROPERTY Z3_${component_name}_INCLUDES "${CMAKE_CURRENT_BINARY_DIR}")
set_property(GLOBAL PROPERTY Z3_${component_name}_DEPS "")
# Record this component's dependencies
foreach (dependency ${Z3_MOD_COMPONENT_DEPENDENCIES})
@ -243,12 +232,6 @@ macro(z3_add_component component_name)
endif()
#message(STATUS "Component \"${component_name}\" has the following dependencies ${_expanded_deps}")
# For any generated header files for this component
target_include_directories(${component_name} PRIVATE "${CMAKE_CURRENT_BINARY_DIR}")
# So that any generated header files can refer to source files in the component's
# source tree
target_include_directories(${component_name} PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}")
# Add any extra include directories
foreach (extra_include ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS})
target_include_directories(${component_name} PRIVATE "${extra_include}")
@ -283,7 +266,6 @@ macro(z3_add_install_tactic_rule)
endforeach()
unset(_component_tactic_header_files)
list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
add_custom_command(OUTPUT "install_tactic.cpp"
COMMAND "${PYTHON_EXECUTABLE}"
"${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py"
@ -311,13 +293,6 @@ macro(z3_add_memory_initializer_rule)
)
endif()
z3_expand_dependencies(_expanded_components ${ARGN})
# Get paths to search
set(_search_paths "")
foreach (dependency ${_expanded_components})
get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES)
list(APPEND _search_paths ${_dep_include_dirs})
endforeach()
list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}")
# Get header files that declare initializers and finalizers
set(_mem_init_finalize_headers "")

12
scripts/update_api.py
View file

@ -1573,7 +1573,7 @@ def def_APIs(api_files):
def write_log_h_preamble(log_h):
log_h.write('// Automatically generated file\n')
log_h.write('#include\"z3.h\"\n')
log_h.write('#include\"api/z3.h\"\n')
log_h.write('#ifdef __GNUC__\n')
log_h.write('#define _Z3_UNUSED __attribute__((unused))\n')
log_h.write('#else\n')
@ -1592,14 +1592,14 @@ def write_log_h_preamble(log_h):
def write_log_c_preamble(log_c):
log_c.write('// Automatically generated file\n')
log_c.write('#include<iostream>\n')
log_c.write('#include\"z3.h\"\n')
log_c.write('#include\"api_log_macros.h\"\n')
log_c.write('#include\"z3_logger.h\"\n')
log_c.write('#include\"api/z3.h\"\n')
log_c.write('#include\"api/api_log_macros.h\"\n')
log_c.write('#include\"api/z3_logger.h\"\n')
def write_exe_c_preamble(exe_c):
exe_c.write('// Automatically generated file\n')
exe_c.write('#include\"z3.h\"\n')
exe_c.write('#include\"z3_replayer.h\"\n')
exe_c.write('#include\"api/z3.h\"\n')
exe_c.write('#include\"api/z3_replayer.h\"\n')
#
exe_c.write('void Z3_replayer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n')

2
src/api/api_algebraic.cpp
View file

@ -18,7 +18,7 @@ Notes:
--*/
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_ast_vector.h"
#include "math/polynomial/algebraic_numbers.h"

2
src/api/api_arith.cpp
View file

@ -16,7 +16,7 @@ Revision History:
--*/
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "ast/arith_decl_plugin.h"

2
src/api/api_array.cpp
View file

@ -16,7 +16,7 @@ Revision History:
--*/
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "ast/array_decl_plugin.h"

2
src/api/api_ast.cpp
View file

@ -16,7 +16,7 @@ Revision History:
--*/
#include<iostream>
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "ast/well_sorted.h"

2
src/api/api_ast_map.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_ast_map.h"
#include "api/api_ast_vector.h"

2
src/api/api_ast_vector.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_ast_vector.h"
#include "ast/ast_translation.h"

2
src/api/api_bv.cpp
View file

@ -16,7 +16,7 @@ Revision History:
--*/
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "ast/bv_decl_plugin.h"

2
src/api/api_config_params.cpp
View file

@ -18,7 +18,7 @@ Revision History:
#include "api/z3.h"
#include "api/api_context.h"
#include "ast/pp.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_util.h"
#include "cmd_context/cmd_context.h"
#include "util/symbol.h"

4
src/api/api_context.cpp
View file

@ -20,10 +20,10 @@ Revision History:
#include<typeinfo>
#include "api/api_context.h"
#include "parsers/smt/smtparser.h"
#include"version.h"
#include "util/version.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_util.h"
#include "ast/reg_decl_plugins.h"
#include "math/realclosure/realclosure.h"

2
src/api/api_datalog.cpp
View file

@ -20,7 +20,7 @@ Revision History:
#include "api/api_util.h"
#include "ast/ast_pp.h"
#include "api/api_ast_vector.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_stats.h"
#include "muz/fp/datalog_parser.h"
#include "util/cancel_eh.h"

2
src/api/api_datatype.cpp
View file

@ -16,7 +16,7 @@ Revision History:
--*/
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "ast/datatype_decl_plugin.h"

2
src/api/api_fpa.cpp
View file

@ -18,7 +18,7 @@ Notes:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "ast/fpa_decl_plugin.h"

2
src/api/api_goal.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_goal.h"
#include "ast/ast_translation.h"

2
src/api/api_interp.cpp
View file

@ -18,7 +18,7 @@
#include<sstream>
#include<vector>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_tactic.h"
#include "api/api_solver.h"

4
src/api/api_log.cpp
View file

@ -17,9 +17,9 @@ Revision History:
--*/
#include<fstream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "util/util.h"
#include"version.h"
#include "util/version.h"
std::ostream * g_z3_log = 0;
bool g_z3_log_enabled = false;

2
src/api/api_model.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_model.h"
#include "api/api_ast_vector.h"

2
src/api/api_numeral.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "ast/arith_decl_plugin.h"

2
src/api/api_opt.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_stats.h"
#include "api/api_context.h"
#include "api/api_util.h"

2
src/api/api_params.cpp
View file

@ -19,7 +19,7 @@ Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "util/params.h"

2
src/api/api_parsers.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "cmd_context/cmd_context.h"

2
src/api/api_pb.cpp
View file

@ -16,7 +16,7 @@ Revision History:
--*/
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "ast/pb_decl_plugin.h"

2
src/api/api_polynomial.cpp
View file

@ -17,7 +17,7 @@ Notes:
--*/
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_polynomial.h"
#include "api/api_ast_vector.h"

2
src/api/api_qe.cpp
View file

@ -19,7 +19,7 @@ Notes:
#include <iostream>
#include "api/z3.h"
#include "api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "api/api_model.h"

2
src/api/api_quant.cpp
View file

@ -16,7 +16,7 @@ Revision History:
--*/
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "parsers/util/pattern_validation.h"

2
src/api/api_rcf.cpp
View file

@ -21,7 +21,7 @@ Notes:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "math/realclosure/realclosure.h"

2
src/api/api_seq.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_util.h"
#include "ast/ast_pp.h"

2
src/api/api_solver.cpp
View file

@ -18,7 +18,7 @@ Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_tactic.h"
#include "api/api_solver.h"

2
src/api/api_stats.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_stats.h"

2
src/api/api_tactic.cpp
View file

@ -17,7 +17,7 @@ Revision History:
--*/
#include<iostream>
#include "api/z3.h"
#include"api_log_macros.h"
#include "api/api_log_macros.h"
#include "api/api_context.h"
#include "api/api_tactic.h"
#include "api/api_model.h"

77
src/ast/pattern/pattern_inference.cpp
View file

@ -54,7 +54,7 @@ bool smaller_pattern::process(expr * p1, expr * p2) {
unsigned num1 = app1->get_num_args();
if (num1 != app2->get_num_args() || app1->get_decl() != app2->get_decl())
return false;
for (unsigned i = 0; i < num1; i++)
for (unsigned i = 0; i < num1; i++)
save(app1->get_arg(i), app2->get_arg(i));
break;
}
@ -67,7 +67,7 @@ bool smaller_pattern::process(expr * p1, expr * p2) {
return false;
}
// it is a variable bound by an external quantifier
else if (p1 != p2)
else if (p1 != p2)
return false;
break;
}
@ -137,7 +137,7 @@ bool pattern_inference::collect::visit_children(expr * n, unsigned delta) {
bool visited = true;
unsigned i;
switch (n->get_kind()) {
case AST_APP:
case AST_APP:
i = to_app(n)->get_num_args();
while (i > 0) {
--i;
@ -187,14 +187,14 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
save(n, delta, 0);
return;
}
if (c->get_num_args() == 0) {
save(n, delta, alloc(info, m, n, uint_set(), 1));
return;
}
ptr_buffer<expr> buffer;
bool changed = false; // false if none of the children is mapped to a node different from itself.
bool changed = false; // false if none of the children is mapped to a node different from itself.
uint_set free_vars;
unsigned size = 1;
unsigned num = c->get_num_args();
@ -216,7 +216,7 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
if (child != child_info->m_node.get())
changed = true;
}
app * new_node = 0;
if (changed)
new_node = m.mk_app(decl, buffer.size(), buffer.c_ptr());
@ -229,11 +229,11 @@ void pattern_inference::collect::save_candidate(expr * n, unsigned delta) {
//
// Remark: The rule above has an exception. The operators (div, idiv, mod) are allowed to be
// used as patterns even when they are not nested in other terms. The motivation is that
// Z3 currently doesn't implement them (i.e., they are uninterpreted). So, some users add axioms
// Z3 currently doesn't implement them (i.e., they are uninterpreted). So, some users add axioms
// stating properties about these operators.
family_id fid = c->get_family_id();
decl_kind k = c->get_decl_kind();
if (!free_vars.empty() &&
if (!free_vars.empty() &&
(fid != m_afid || (fid == m_afid && !m_owner.m_nested_arith_only && (k == OP_DIV || k == OP_IDIV || k == OP_MOD || k == OP_REM || k == OP_MUL)))) {
TRACE("pattern_inference", tout << "potential candidate: \n" << mk_pp(new_node, m) << "\n";);
m_owner.add_candidate(new_node, free_vars, size);
@ -288,7 +288,7 @@ void pattern_inference::filter_looping_patterns(ptr_vector<app> & result) {
uint_set const & s2 = e2->get_data().m_value.m_free_vars;
// Remark: the comparison operator only makes sense if both AST nodes
// contain the same number of variables.
// Example:
// Example:
// (f X Y) <: (f (g X Z W) Y)
if (s1 == s2 && m_le(m_num_bindings, n1, n2) && !m_le(m_num_bindings, n2, n1)) {
smaller = true;
@ -421,12 +421,12 @@ void pattern_inference::candidates2unary_patterns(ptr_vector<app> const & candid
}
// TODO: this code is too inefficient when the number of candidate
// patterns is too big.
// patterns is too big.
// HACK: limit the number of case-splits:
#define MAX_SPLITS 32
void pattern_inference::candidates2multi_patterns(unsigned max_num_patterns,
ptr_vector<app> const & candidate_patterns,
void pattern_inference::candidates2multi_patterns(unsigned max_num_patterns,
ptr_vector<app> const & candidate_patterns,
app_ref_buffer & result) {
SASSERT(!candidate_patterns.empty());
m_pre_patterns.push_back(alloc(pre_pattern));
@ -464,7 +464,7 @@ void pattern_inference::candidates2multi_patterns(unsigned max_num_patterns,
m_pre_patterns.push_back(curr);
}
}
TRACE("pattern_inference", tout << "m_pre_patterns.size(): " << m_pre_patterns.size() <<
TRACE("pattern_inference", tout << "m_pre_patterns.size(): " << m_pre_patterns.size() <<
"\nnum_splits: " << num_splits << "\n";);
}
}
@ -478,7 +478,7 @@ void pattern_inference::reset_pre_patterns() {
static void dump_app_vector(std::ostream & out, ptr_vector<app> const & v, ast_manager & m) {
ptr_vector<app>::const_iterator it = v.begin();
ptr_vector<app>::const_iterator end = v.end();
for (; it != end; ++it)
for (; it != end; ++it)
out << mk_pp(*it, m) << "\n";
}
#endif
@ -487,8 +487,8 @@ bool pattern_inference::is_forbidden(app * n) const {
func_decl const * decl = n->get_decl();
if (is_ground(n))
return false;
// Remark: skolem constants should not be used in patterns, since they do not
// occur outside of the quantifier. That is, Z3 will never match this kind of
// Remark: skolem constants should not be used in patterns, since they do not
// occur outside of the quantifier. That is, Z3 will never match this kind of
// pattern.
if (m_params.m_pi_avoid_skolems && decl->is_skolem()) {
CTRACE("pattern_inference_skolem", decl->is_skolem(), tout << "ignoring: " << mk_pp(n, m) << "\n";);
@ -521,9 +521,9 @@ bool pattern_inference::has_preferred_patterns(ptr_vector<app> & candidate_patte
return found;
}
void pattern_inference::mk_patterns(unsigned num_bindings,
expr * n,
unsigned num_no_patterns,
void pattern_inference::mk_patterns(unsigned num_bindings,
expr * n,
unsigned num_no_patterns,
expr * const * no_patterns,
app_ref_buffer & result) {
m_num_bindings = num_bindings;
@ -532,7 +532,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
m_collect(n, num_bindings);
TRACE("pattern_inference",
TRACE("pattern_inference",
tout << mk_pp(n, m);
tout << "\ncandidates:\n";
unsigned num = m_candidates.size();
@ -558,7 +558,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
m_tmp1.reset();
candidates2unary_patterns(m_tmp2, m_tmp1, result);
unsigned num_extra_multi_patterns = m_params.m_pi_max_multi_patterns;
if (result.empty())
if (result.empty())
num_extra_multi_patterns++;
if (num_extra_multi_patterns > 0 && !m_tmp1.empty()) {
// m_pattern_weight_lt is not a total order
@ -604,7 +604,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
else {
quantifier_ref tmp(m);
tmp = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), q->get_expr());
new_q = m.update_quantifier_weight(tmp, new_weight);
new_q = m.update_quantifier_weight(tmp, new_weight);
TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m) << "\n";);
}
proof * pr = 0;
@ -635,15 +635,15 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
proof * new_pattern_pr;
get_cached(q->get_no_pattern(i), new_pattern, new_pattern_pr);
new_no_patterns.push_back(new_pattern);
}
}
app_ref_buffer new_patterns(m);
if (m_params.m_pi_arith == AP_CONSERVATIVE)
m_forbidden.push_back(m_afid);
mk_patterns(q->get_num_decls(), new_body, new_no_patterns.size(), new_no_patterns.c_ptr(), new_patterns);
if (new_patterns.empty() && !new_no_patterns.empty()) {
if (new_patterns.empty()) {
mk_patterns(q->get_num_decls(), new_body, 0, 0, new_patterns);
@ -652,7 +652,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
}
}
}
if (m_params.m_pi_arith == AP_CONSERVATIVE) {
m_forbidden.pop_back();
if (new_patterns.empty()) {
@ -661,13 +661,13 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
if (!new_patterns.empty()) {
weight = std::max(weight, static_cast<int>(m_params.m_pi_arith_weight));
if (m_params.m_pi_warnings) {
warning_msg("using arith. in pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_ARITH_WEIGHT=<val>).",
warning_msg("using arith. in pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_ARITH_WEIGHT=<val>).",
q->get_qid().str().c_str(), weight);
}
}
}
}
if (m_params.m_pi_arith != AP_NO && new_patterns.empty()) {
if (new_patterns.empty()) {
flet<bool> l1(m_nested_arith_only, false); // try to find a non-nested arith pattern
@ -676,8 +676,8 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
if (!new_patterns.empty()) {
weight = std::max(weight, static_cast<int>(m_params.m_pi_non_nested_arith_weight));
if (m_params.m_pi_warnings) {
warning_msg("using non nested arith. pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=<val>).",
q->get_qid().str().c_str(), weight);
warning_msg("using non nested arith. pattern (quantifier id: %s), the weight was increased to %d (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=<val>).",
q->get_qid().str().c_str(), weight);
}
// verbose_stream() << mk_pp(q, m) << "\n";
}
@ -689,12 +689,12 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
if (weight != q->get_weight())
new_q = m.update_quantifier_weight(new_q, weight);
proof_ref pr(m);
if (m.fine_grain_proofs()) {
if (m.fine_grain_proofs()) {
if (new_body_pr == 0)
new_body_pr = m.mk_reflexivity(new_body);
pr = m.mk_quant_intro(q, new_q, new_body_pr);
}
if (new_patterns.empty() && m_params.m_pi_pull_quantifiers) {
pull_quant pull(m);
expr_ref new_expr(m);
@ -728,9 +728,14 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
cache_result(q, q, 0);
return;
}
cache_result(q, new_q, pr);
IF_IVERBOSE(10,
verbose_stream() << "(smt.inferred-patterns :qid " << q->get_qid() << "\n";
for (unsigned i = 0; i < new_patterns.size(); i++)
verbose_stream() << " " << mk_ismt2_pp(new_patterns[i], m, 2) << "\n";
verbose_stream() << ")\n"; );
cache_result(q, new_q, pr);
}
@ -739,7 +744,7 @@ void pattern_inference::reduce1_quantifier(quantifier * q) {
static void dump_expr_vector(std::ostream & out, ptr_vector<expr> const & v, ast_manager & m) {
ptr_vector<expr>::const_iterator it = v.begin();
ptr_vector<expr>::const_iterator end = v.end();
for (; it != end; ++it)
for (; it != end; ++it)
out << mk_pp(*it, m) << "\n";
}
#endif

2
src/cmd_context/basic_cmds.cpp
View file

@ -16,7 +16,7 @@ Notes:
--*/
#include "cmd_context/cmd_context.h"
#include"version.h"
#include "util/version.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_pp.h"

2
src/duality/duality_wrapper.h
View file

@ -27,7 +27,7 @@
#include<vector>
#include<list>
#include <set>
#include"version.h"
#include "util/version.h"
#include<limits.h>
#include "interp/iz3hash.h"

2
src/shell/main.cpp
View file

@ -26,7 +26,7 @@ Revision History:
#include "shell/smtlib_frontend.h"
#include "shell/z3_log_frontend.h"
#include "util/warning.h"
#include"version.h"
#include "util/version.h"
#include "shell/dimacs_frontend.h"
#include "shell/datalog_frontend.h"
#include "shell/opt_frontend.h"

493
src/smt/mam.cpp
View file

File diff suppressed because it is too large Load diff

57
src/smt/smt_model_checker.cpp
View file

@ -40,7 +40,7 @@ namespace smt {
m_max_cexs(1),
m_iteration_idx(0),
m_curr_model(0),
m_new_instances_bindings(m) {
m_pinned_exprs(m) {
}
model_checker::~model_checker() {
@ -53,8 +53,8 @@ namespace smt {
}
void model_checker::set_qm(quantifier_manager & qm) {
SASSERT(m_qm == 0);
SASSERT(m_context == 0);
SASSERT(m_qm == 0);
SASSERT(m_context == 0);
m_qm = &qm;
m_context = &(m_qm->get_context());
}
@ -112,7 +112,7 @@ namespace smt {
if (!m_curr_model->eval(q->get_expr(), tmp, true)) {
return;
}
TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);
TRACE("model_checker", tout << "q after applying interpretation:\n" << mk_ismt2_pp(tmp, m) << "\n";);
ptr_buffer<expr> subst_args;
unsigned num_decls = q->get_num_decls();
subst_args.resize(num_decls, 0);
@ -139,7 +139,7 @@ namespace smt {
bool model_checker::add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv) {
if (cex == 0) {
TRACE("model_checker", tout << "no model is available\n";);
return false;
return false;
}
unsigned num_decls = q->get_num_decls();
// Remark: sks were created for the flat version of q.
@ -187,21 +187,25 @@ namespace smt {
}
bindings.set(num_decls - i - 1, sk_value);
}
TRACE("model_checker", tout << q->get_qid() << " found (use_inv: " << use_inv << ") new instance: ";
for (unsigned i = 0; i < num_decls; i++) {
tout << mk_ismt2_pp(bindings[i].get(), m) << " ";
}
tout << "\n";);
max_generation = std::max(m_qm->get_generation(q), max_generation);
add_instance(q, bindings, max_generation);
return true;
}
void model_checker::add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation) {
for (unsigned i = 0; i < bindings.size(); i++)
m_new_instances_bindings.push_back(bindings[i]);
SASSERT(q->get_num_decls() == bindings.size());
for (unsigned i = 0; i < bindings.size(); i++)
m_pinned_exprs.push_back(bindings[i]);
m_pinned_exprs.push_back(q);
void * mem = m_new_instances_region.allocate(instance::get_obj_size(q->get_num_decls()));
instance * new_inst = new (mem) instance(q, bindings.c_ptr(), max_generation);
m_new_instances.push_back(new_inst);
@ -260,39 +264,39 @@ namespace smt {
bool model_checker::check(quantifier * q) {
SASSERT(!m_aux_context->relevancy());
m_aux_context->push();
quantifier * flat_q = get_flat_quantifier(q);
TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" <<
TRACE("model_checker", tout << "model checking:\n" << mk_ismt2_pp(q->get_expr(), m) << "\n" <<
mk_ismt2_pp(flat_q->get_expr(), m) << "\n";);
expr_ref_vector sks(m);
assert_neg_q_m(flat_q, sks);
TRACE("model_checker", tout << "skolems:\n";
TRACE("model_checker", tout << "skolems:\n";
for (unsigned i = 0; i < sks.size(); i++) {
expr * sk = sks.get(i);
tout << mk_ismt2_pp(sk, m) << " " << mk_pp(m.get_sort(sk), m) << "\n";
});
lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[complete] model-checker result: " << to_sat_str(r) << "\n";);
if (r != l_true) {
m_aux_context->pop(1);
return r == l_false; // quantifier is satisfied by m_curr_model
}
model_ref complete_cex;
m_aux_context->get_model(complete_cex);
m_aux_context->get_model(complete_cex);
// try to find new instances using instantiation sets.
m_model_finder.restrict_sks_to_inst_set(m_aux_context.get(), q, sks);
unsigned num_new_instances = 0;
while (true) {
lbool r = m_aux_context->check();
TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
TRACE("model_checker", tout << "[restricted] model-checker (" << (num_new_instances+1) << ") result: " << to_sat_str(r) << "\n";);
if (r != l_true)
break;
break;
model_ref cex;
m_aux_context->get_model(cex);
if (!add_instance(q, cex.get(), sks, true)) {
@ -302,7 +306,7 @@ namespace smt {
if (num_new_instances >= m_max_cexs || !add_blocking_clause(cex.get(), sks)) {
TRACE("model_checker", tout << "Add blocking clause failed new-instances: " << num_new_instances << " max-cex: " << m_max_cexs << "\n";);
// add_blocking_clause failed... stop the search for new counter-examples...
break;
break;
}
}
@ -395,17 +399,17 @@ namespace smt {
check_quantifiers(false, found_relevant, num_failures);
if (found_relevant)
m_iteration_idx++;
TRACE("model_checker", tout << "model after check:\n"; model_pp(tout, *md););
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
TRACE("model_checker", tout << "model checker result: " << (num_failures == 0) << "\n";);
m_max_cexs += m_params.m_mbqi_max_cexs;
if (num_failures == 0 && !m_context->validate_model()) {
num_failures = 1;
// this time force expanding recursive function definitions
// this time force expanding recursive function definitions
// that are not forced true in the current model.
check_quantifiers(true, found_relevant, num_failures);
}
@ -426,7 +430,7 @@ namespace smt {
for (; it != end; ++it) {
quantifier * q = *it;
if(!m_qm->mbqi_enabled(q)) continue;
TRACE("model_checker",
TRACE("model_checker",
tout << "Check: " << mk_pp(q, m) << "\n";
tout << m_context->get_assignment(q) << "\n";);
@ -469,8 +473,9 @@ namespace smt {
}
void model_checker::reset_new_instances() {
m_new_instances_region.reset();
m_pinned_exprs.reset();
m_new_instances.reset();
m_new_instances_region.reset();
}
void model_checker::reset() {
@ -505,7 +510,7 @@ namespace smt {
expr * b = inst->m_bindings[i];
tout << mk_pp(b, m) << "\n";
});
TRACE("model_checker_instance",
TRACE("model_checker_instance",
expr_ref inst_expr(m);
instantiate(m, q, inst->m_bindings, inst_expr);
tout << "(assert " << mk_ismt2_pp(inst_expr, m) << ")\n";);

8
src/smt/smt_model_checker.h
View file

@ -39,7 +39,7 @@ namespace smt {
class model_checker {
ast_manager & m; // _manager;
qi_params const & m_params;
// copy of smt_params for auxiliary context.
// copy of smt_params for auxiliary context.
// the idea is to use a different configuration for the aux context (e.g., disable relevancy)
scoped_ptr<smt_params> m_fparams;
quantifier_manager * m_qm;
@ -73,8 +73,8 @@ namespace smt {
};
region m_new_instances_region;
expr_ref_vector m_new_instances_bindings;
ptr_vector<instance> m_new_instances;
expr_ref_vector m_pinned_exprs;
bool add_instance(quantifier * q, model * cex, expr_ref_vector & sks, bool use_inv);
void reset_new_instances();
void assert_new_instances();
@ -83,8 +83,8 @@ namespace smt {
struct is_model_value {};
expr_mark m_visited;
bool contains_model_value(expr* e);
void add_instance(quantifier* q, expr_ref_vector const& bindings, unsigned max_generation);
bool contains_model_value(expr * e);
void add_instance(quantifier * q, expr_ref_vector const & bindings, unsigned max_generation);
public:
model_checker(ast_manager & m, qi_params const & p, model_finder & mf);