diff --git a/scripts/mk_project.py b/scripts/mk_project.py index b29bcbf15..1ff500359 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -55,8 +55,8 @@ def init_project_def(): add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa') add_lib('smt_tactic', ['smt'], 'smt/tactic') add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls') - add_lib('duality', ['smt', 'interp']) add_lib('qe', ['smt','sat'], 'qe') + add_lib('duality', ['smt', 'interp', 'qe']) add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base') add_lib('transforms', ['muz', 'hilbert'], 'muz/transforms') add_lib('rel', ['muz', 'transforms'], 'muz/rel') diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 9295c949f..d425f6576 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -638,7 +638,13 @@ def is_compiler(given, expected): def is_CXX_gpp(): return is_compiler(CXX, 'g++') +def is_clang_in_gpp_form(cc): + version_string = subprocess.check_output([cc, '--version']) + return str(version_string).find('clang') != -1 + def is_CXX_clangpp(): + if is_compiler(CXX, 'g++'): + return is_clang_in_gpp_form(CXX) return is_compiler(CXX, 'clang++') def get_cpp_files(path): @@ -1192,9 +1198,9 @@ class JavaDLLComponent(Component): deps += '%s ' % os.path.join(self.to_src_dir, 'enumerations', jfile) out.write(deps) out.write('\n') - if IS_WINDOWS: - JAVAC = '"%s"' % JAVAC - JAR = '"%s"' % JAR + #if IS_WINDOWS: + JAVAC = '"%s"' % JAVAC + JAR = '"%s"' % JAR t = ('\t%s %s.java -d %s\n' % (JAVAC, os.path.join(self.to_src_dir, 'enumerations', '*'), os.path.join('api', 'java', 'classes'))) out.write(t) t = ('\t%s -cp %s %s.java -d %s\n' % (JAVAC, @@ -1431,7 +1437,7 @@ def mk_config(): 'SO_EXT=.dll\n' 'SLINK=cl\n' 'SLINK_OUT_FLAG=/Fe\n' - 'OS_DEFINES=/D _WINDOWS\n') + 'OS_DEFINES=/D _WINDOWS\n') extra_opt = '' if GIT_HASH: extra_opt = '%s /D Z3GITHASH=%s' % (extra_opt, GIT_HASH) @@ -1479,7 +1485,7 @@ def mk_config(): print('Java Compiler: %s' % JAVAC) else: global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG - OS_DEFINES = "" + OS_DEFINES = "" ARITH = "internal" check_ar() CXX = find_cxx_compiler() @@ -1502,7 +1508,7 @@ def mk_config(): SLIBEXTRAFLAGS = '%s %s' % (SLIBEXTRAFLAGS,FOCI2LIB) CPPFLAGS = '%s -D_FOCI2' % CPPFLAGS else: - print "FAILED\n" + print("FAILED\n") FOCI2 = False if GIT_HASH: CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH) @@ -1530,21 +1536,21 @@ def mk_config(): SLIBFLAGS = '-dynamiclib' elif sysname == 'Linux': CXXFLAGS = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS - OS_DEFINES = '-D_LINUX' + OS_DEFINES = '-D_LINUX' SO_EXT = '.so' LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS elif sysname == 'FreeBSD': CXXFLAGS = '%s -fno-strict-aliasing -D_FREEBSD_' % CXXFLAGS - OS_DEFINES = '-D_FREEBSD_' + OS_DEFINES = '-D_FREEBSD_' SO_EXT = '.so' LDFLAGS = '%s -lrt' % LDFLAGS SLIBFLAGS = '-shared' SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS elif sysname[:6] == 'CYGWIN': CXXFLAGS = '%s -D_CYGWIN -fno-strict-aliasing' % CXXFLAGS - OS_DEFINES = '-D_CYGWIN' + OS_DEFINES = '-D_CYGWIN' SO_EXT = '.dll' SLIBFLAGS = '-shared' else: @@ -1580,7 +1586,7 @@ def mk_config(): config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS) config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS) config.write('SLINK_OUT_FLAG=-o \n') - config.write('OS_DEFINES=%s\n' % OS_DEFINES) + config.write('OS_DEFINES=%s\n' % OS_DEFINES) if is_verbose(): print('Host platform: %s' % sysname) print('C++ Compiler: %s' % CXX) diff --git a/scripts/update_api.py b/scripts/update_api.py index fa6111482..f88e0393f 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -523,7 +523,7 @@ def mk_java(): java_native.write(' public static class LongPtr { public long value; }\n') java_native.write(' public static class StringPtr { public String value; }\n') java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n') - if IS_WINDOWS: + if IS_WINDOWS or os.uname()[0]=="CYGWIN": java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name) else: java_native.write(' static { System.loadLibrary("%s"); }\n' % get_component('java').dll_name[3:]) # We need 3: to extract the prexi 'lib' form the dll_name @@ -588,6 +588,9 @@ def mk_java(): java_wrapper = open(java_wrapperf, 'w') pkg_str = get_component('java').package_name.replace('.', '_') java_wrapper.write('// Automatically generated file\n') + java_wrapper.write('#ifdef _CYGWIN\n') + java_wrapper.write('typedef long long __int64;\n') + java_wrapper.write('#endif\n') java_wrapper.write('#include\n') java_wrapper.write('#include\n') java_wrapper.write('#include"z3.h"\n') diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 00503566e..98722022c 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -17,6 +17,7 @@ Revision History: --*/ #include #include +#include #include"z3.h" #include"api_log_macros.h" #include"api_context.h" @@ -42,6 +43,20 @@ Revision History: using namespace stl_ext; #endif +#ifndef WIN32 +// WARNING: don't make a hash_map with this if the range type +// has a destructor: you'll get an address dependency!!! +namespace stl_ext { + template <> + class hash { + public: + size_t operator()(const Z3_ast p) const { + return (size_t) p; + } + }; +} +#endif + typedef interpolation_options_struct *Z3_interpolation_options; extern "C" { @@ -305,8 +320,8 @@ static void get_file_params(const char *filename, hash_map= 0 && eqpos < (int)tok.size()){ + size_t eqpos = tok.find('='); + if(eqpos >= 0 && eqpos < tok.size()){ std::string left = tok.substr(0,eqpos); std::string right = tok.substr(eqpos+1,tok.size()-eqpos-1); params[left] = right; @@ -363,8 +378,8 @@ extern "C" { #else - static Z3_ast and_vec(Z3_context ctx,std::vector &c){ - return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0]; + static Z3_ast and_vec(Z3_context ctx,svector &c){ + return (c.size() > 1) ? Z3_mk_and(ctx,c.size(),&c[0]) : c[0]; } static Z3_ast parents_vector_to_tree(Z3_context ctx, int num, Z3_ast *cnsts, int *parents){ @@ -381,15 +396,15 @@ extern "C" { } } else { - std::vector > chs(num); + std::vector > chs(num); for(int i = 0; i < num-1; i++){ - std::vector &c = chs[i]; + svector &c = chs[i]; c.push_back(cnsts[i]); Z3_ast foo = Z3_mk_interp(ctx,and_vec(ctx,c)); chs[parents[i]].push_back(foo); } { - std::vector &c = chs[num-1]; + svector &c = chs[num-1]; c.push_back(cnsts[num-1]); res = and_vec(ctx,c); } @@ -454,7 +469,7 @@ extern "C" { static std::string read_msg; static std::vector read_theory; - static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, std::vector &assertions){ + static bool iZ3_parse(Z3_context ctx, const char *filename, const char **error, svector &assertions){ read_error.clear(); try { std::string foo(filename); @@ -496,26 +511,26 @@ extern "C" { hash_map file_params; get_file_params(filename,file_params); - - int num_theory = 0; + + unsigned num_theory = 0; if(file_params.find("THEORY") != file_params.end()) num_theory = atoi(file_params["THEORY"].c_str()); - std::vector assertions; + svector assertions; if(!iZ3_parse(ctx,filename,error,assertions)) return false; - if(num_theory > (int)assertions.size()) - num_theory = assertions.size(); - int num = assertions.size() - num_theory; + if(num_theory > assertions.size()) + num_theory = assertions.size(); + unsigned num = assertions.size() - num_theory; read_cnsts.resize(num); read_parents.resize(num); read_theory.resize(num_theory); - for(int j = 0; j < num_theory; j++) + for(unsigned j = 0; j < num_theory; j++) read_theory[j] = assertions[j]; - for(int j = 0; j < num; j++) + for(unsigned j = 0; j < num; j++) read_cnsts[j] = assertions[j+num_theory]; if(ret_num_theory) @@ -529,12 +544,12 @@ extern "C" { return true; } - for(int j = 0; j < num; j++) + for(unsigned j = 0; j < num; j++) read_parents[j] = SHRT_MAX; hash_map pred_map; - for(int j = 0; j < num; j++){ + for(unsigned j = 0; j < num; j++){ Z3_ast lhs = 0, rhs = read_cnsts[j]; if(Z3_get_decl_kind(ctx,Z3_get_app_decl(ctx,Z3_to_app(ctx,rhs))) == Z3_OP_IMPLIES){ @@ -588,7 +603,7 @@ extern "C" { } } - for(int j = 0; j < num-1; j++) + for(unsigned j = 0; j < num-1; j++) if(read_parents[j] == SHRT_MIN){ read_error << "formula " << j+1 << ": unreferenced"; goto fail; diff --git a/src/api/java/BitVecNum.java b/src/api/java/BitVecNum.java index 7615308b7..2dd0dd75a 100644 --- a/src/api/java/BitVecNum.java +++ b/src/api/java/BitVecNum.java @@ -35,7 +35,7 @@ public class BitVecNum extends BitVecExpr { Native.LongPtr res = new Native.LongPtr(); if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true) - throw new Z3Exception("Numeral is not an int64"); + throw new Z3Exception("Numeral is not a long"); return res.value; } diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 959566619..9233a41dc 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -586,7 +586,7 @@ class FuncDeclRef(AstRef): return Z3_func_decl_to_ast(self.ctx_ref(), self.ast) def as_func_decl(self): - return self.ast + return self.ast def name(self): """Return the name of the function declaration `self`. diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index bdf1c18db..68f7596ee 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1850,6 +1850,7 @@ func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const { ast_manager& m = const_cast(*this); + if (decl->is_associative()) { sort * expected = decl->get_domain(0); for (unsigned i = 0; i < num_args; i++) { @@ -1894,7 +1895,18 @@ void ast_manager::check_sorts_core(ast const * n) const { if (n->get_kind() != AST_APP) return; // nothing else to check... app const * a = to_app(n); - check_sort(a->get_decl(), a->get_num_args(), a->get_args()); + func_decl* d = a->get_decl(); + check_sort(d, a->get_num_args(), a->get_args()); + if (a->get_num_args() == 2 && + !d->is_flat_associative() && + d->is_right_associative()) { + check_sorts_core(a->get_arg(1)); + } + if (a->get_num_args() == 2 && + !d->is_flat_associative() && + d->is_left_associative()) { + check_sorts_core(a->get_arg(0)); + } } bool ast_manager::check_sorts(ast const * n) const { @@ -3161,3 +3173,6 @@ void prexpr(expr_ref &e){ std::cout << mk_pp(e.get(), e.get_manager()) << std::endl; } +void ast_manager::show_id_gen(){ + std::cout << "id_gen: " << m_expr_id_gen.show_hash() << " " << m_decl_id_gen.show_hash() << "\n"; +} diff --git a/src/ast/ast.h b/src/ast/ast.h index 2c3843587..68f08e1ac 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -1418,6 +1418,8 @@ protected: public: typedef expr_dependency_array_manager::ref expr_dependency_array; + void show_id_gen(); + protected: small_object_allocator m_alloc; family_manager m_family_manager; diff --git a/src/ast/float_decl_plugin.cpp b/src/ast/float_decl_plugin.cpp index eb8aba9ae..1adedb2d7 100644 --- a/src/ast/float_decl_plugin.cpp +++ b/src/ast/float_decl_plugin.cpp @@ -213,6 +213,9 @@ func_decl * float_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_par if (num_parameters == 1 && parameters[0].is_ast() && is_sort(parameters[0].get_ast()) && is_float_sort(to_sort(parameters[0].get_ast()))) { s = to_sort(parameters[0].get_ast()); } + else if (num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()) { + s = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + } else if (range != 0 && is_float_sort(range)) { s = range; } @@ -376,7 +379,19 @@ func_decl * float_decl_plugin::mk_to_float(decl_kind k, unsigned num_parameters, sort * fp = mk_float_sort(domain[2]->get_parameter(0).get_int(), domain[1]->get_parameter(0).get_int()+1); symbol name("asFloat"); return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); - } + } + else if (m_bv_plugin && arity == 1 && is_sort_of(domain[0], m_bv_fid, BV_SORT)) { + if (num_parameters != 2) + m_manager->raise_exception("invalid number of parameters to to_fp"); + if (!parameters[0].is_int() || !parameters[1].is_int()) + m_manager->raise_exception("invalid parameter type to to_fp"); + int ebits = parameters[0].get_int(); + int sbits = parameters[1].get_int(); + + sort * fp = mk_float_sort(ebits, sbits); + symbol name("asFloat"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k, num_parameters, parameters)); + } else { // .. Otherwise we only know how to convert rationals/reals. if (!(num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int())) @@ -412,6 +427,53 @@ func_decl * float_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameter return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); } +func_decl * float_decl_plugin::mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (!m_bv_plugin) + m_manager->raise_exception("fp unsupported; use a logic with BV support"); + if (arity != 3) + m_manager->raise_exception("invalid number of arguments to fp"); + if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) || + !is_sort_of(domain[1], m_bv_fid, BV_SORT) || + !is_sort_of(domain[2], m_bv_fid, BV_SORT)) + m_manager->raise_exception("sort mismtach"); + + sort * fp = mk_float_sort(domain[1]->get_parameter(0).get_int(), domain[2]->get_parameter(0).get_int() + 1); + symbol name("fp"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k)); +} + +func_decl * float_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + if (!m_bv_plugin) + m_manager->raise_exception("to_fp_unsigned unsupported; use a logic with BV support"); + if (arity != 2) + m_manager->raise_exception("invalid number of arguments to to_fp_unsigned"); + if (is_rm_sort(domain[0])) + m_manager->raise_exception("sort mismtach"); + if (!is_sort_of(domain[1], m_bv_fid, BV_SORT)) + m_manager->raise_exception("sort mismtach"); + + sort * fp = mk_float_sort(parameters[0].get_int(), parameters[1].get_int()); + symbol name("to_fp_unsigned"); + return m_manager->mk_func_decl(name, arity, domain, fp, func_decl_info(m_family_id, k)); +} + +func_decl * float_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + +func_decl * float_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + +func_decl * float_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + NOT_IMPLEMENTED_YET(); +} + func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { switch (k) { @@ -465,6 +527,16 @@ func_decl * float_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters return mk_fused_ma(k, num_parameters, parameters, arity, domain, range); case OP_TO_IEEE_BV: return mk_to_ieee_bv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_FP: + return mk_from3bv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_FP_UNSIGNED: + return mk_to_fp_unsigned(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_UBV: + return mk_to_ubv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_SBV: + return mk_to_sbv(k, num_parameters, parameters, arity, domain, range); + case OP_FLOAT_TO_REAL: + return mk_to_real(k, num_parameters, parameters, arity, domain, range); default: m_manager->raise_exception("unsupported floating point operator"); return 0; @@ -517,8 +589,9 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co if (m_bv_plugin) op_names.push_back(builtin_name("asIEEEBV", OP_TO_IEEE_BV)); - // We also support draft version 3 - op_names.push_back(builtin_name("fp", OP_TO_FLOAT)); + // These are the operators from the final draft of the SMT FloatingPoints standard + op_names.push_back(builtin_name("+oo", OP_FLOAT_PLUS_INF)); + op_names.push_back(builtin_name("-oo", OP_FLOAT_MINUS_INF)); op_names.push_back(builtin_name("RNE", OP_RM_NEAREST_TIES_TO_EVEN)); op_names.push_back(builtin_name("RNA", OP_RM_NEAREST_TIES_TO_AWAY)); @@ -547,23 +620,24 @@ void float_decl_plugin::get_op_names(svector & op_names, symbol co op_names.push_back(builtin_name("fp.isNaN", OP_FLOAT_IS_NAN)); op_names.push_back(builtin_name("fp.min", OP_FLOAT_MIN)); op_names.push_back(builtin_name("fp.max", OP_FLOAT_MAX)); - op_names.push_back(builtin_name("fp.convert", OP_TO_FLOAT)); + op_names.push_back(builtin_name("to_fp", OP_TO_FLOAT)); if (m_bv_plugin) { - // op_names.push_back(builtin_name("fp.fromBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.fromUBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.fromSBv", OP_TO_FLOAT)); - // op_names.push_back(builtin_name("fp.toUBv", OP_TO_IEEE_BV)); - // op_names.push_back(builtin_name("fp.toSBv", OP_TO_IEEE_BV)); + op_names.push_back(builtin_name("fp", OP_FLOAT_FP)); + op_names.push_back(builtin_name("to_fp_unsigned", OP_FLOAT_TO_FP_UNSIGNED)); + op_names.push_back(builtin_name("fp.to_ubv", OP_FLOAT_TO_UBV)); + op_names.push_back(builtin_name("fp.to_sbv", OP_FLOAT_TO_SBV)); } - - op_names.push_back(builtin_name("fp.fromReal", OP_TO_FLOAT)); + // op_names.push_back(builtin_name("fp.toReal", ?)); } void float_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { sort_names.push_back(builtin_name("FP", FLOAT_SORT)); sort_names.push_back(builtin_name("RoundingMode", ROUNDING_MODE_SORT)); + + // In the SMT FPA final draft, FP is called FloatingPoint + sort_names.push_back(builtin_name("FloatingPoint", FLOAT_SORT)); } expr * float_decl_plugin::get_some_value(sort * s) { diff --git a/src/ast/float_decl_plugin.h b/src/ast/float_decl_plugin.h index 0b8349793..3bd7ee424 100644 --- a/src/ast/float_decl_plugin.h +++ b/src/ast/float_decl_plugin.h @@ -72,6 +72,12 @@ enum float_op_kind { OP_TO_FLOAT, OP_TO_IEEE_BV, + + OP_FLOAT_FP, + OP_FLOAT_TO_FP_UNSIGNED, + OP_FLOAT_TO_UBV, + OP_FLOAT_TO_SBV, + OP_FLOAT_TO_REAL, LAST_FLOAT_OP }; @@ -125,7 +131,17 @@ class float_decl_plugin : public decl_plugin { unsigned arity, sort * const * domain, sort * range); func_decl * mk_to_ieee_bv(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - + func_decl * mk_from3bv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + func_decl * mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + virtual void set_manager(ast_manager * m, family_id id); unsigned mk_id(mpf const & v); void recycled_id(unsigned id); diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp index 85e0cc791..41c43b26c 100644 --- a/src/ast/proof_checker/proof_checker.cpp +++ b/src/ast/proof_checker/proof_checker.cpp @@ -479,7 +479,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { // otherwise t2 is also a quantifier. return true; } - UNREACHABLE(); + IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";); return false; } case PR_DER: { @@ -488,13 +488,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { match_fact(p, fact) && match_iff(fact.get(), t1, t2) && match_quantifier(t1, is_forall, decls1, body1) && - is_forall && - match_or(body1.get(), terms1)) { + is_forall) { // TBD: check that terms are set of equalities. // t2 is an instance of a predicate in terms1 return true; - } - UNREACHABLE(); + } + IF_VERBOSE(0, verbose_stream() << "does not match last rule: " << mk_pp(p, m) << "\n";); return false; } case PR_HYPOTHESIS: { @@ -832,7 +831,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { } else { IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" << - mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n";); + mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n" << mk_pp(p, m) << "\n";); } fmls[i] = premise1; } diff --git a/src/ast/rewriter/float_rewriter.cpp b/src/ast/rewriter/float_rewriter.cpp index 6ef147f1c..ecd06ff38 100644 --- a/src/ast/rewriter/float_rewriter.cpp +++ b/src/ast/rewriter/float_rewriter.cpp @@ -64,6 +64,11 @@ br_status float_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c case OP_FLOAT_IS_SUBNORMAL: SASSERT(num_args == 1); st = mk_is_subnormal(args[0], result); break; case OP_FLOAT_IS_SIGN_MINUS: SASSERT(num_args == 1); st = mk_is_sign_minus(args[0], result); break; case OP_TO_IEEE_BV: SASSERT(num_args == 1); st = mk_to_ieee_bv(args[0], result); break; + case OP_FLOAT_FP: SASSERT(num_args == 3); st = mk_fp(args[0], args[1], args[2], result); break; + case OP_FLOAT_TO_FP_UNSIGNED: SASSERT(num_args == 2); st = mk_to_fp_unsigned(args[0], args[1], result); break; + case OP_FLOAT_TO_UBV: SASSERT(num_args == 2); st = mk_to_ubv(args[0], args[1], result); break; + case OP_FLOAT_TO_SBV: SASSERT(num_args == 2); st = mk_to_sbv(args[0], args[1], result); break; + case OP_FLOAT_TO_REAL: SASSERT(num_args == 1); st = mk_to_real(args[0], result); break; } return st; } @@ -504,3 +509,42 @@ br_status float_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result br_status float_rewriter::mk_to_ieee_bv(expr * arg1, expr_ref & result) { return BR_FAILED; } + +br_status float_rewriter::mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result) { + bv_util bu(m()); + rational r1, r2, r3; + unsigned bvs1, bvs2, bvs3; + + if (bu.is_numeral(arg1, r1, bvs1) && bu.is_numeral(arg2, r2, bvs2) && bu.is_numeral(arg3, r3, bvs3)) { + SASSERT(m_util.fm().mpz_manager().is_one(r2.to_mpq().denominator())); + SASSERT(m_util.fm().mpz_manager().is_one(r3.to_mpq().denominator())); + SASSERT(m_util.fm().mpz_manager().is_int64(r3.to_mpq().numerator())); + scoped_mpf v(m_util.fm()); + mpf_exp_t biased_exp = m_util.fm().mpz_manager().get_int64(r2.to_mpq().numerator()); + m_util.fm().set(v, bvs2, bvs3 + 1, + r1.is_one(), + r3.to_mpq().numerator(), + m_util.fm().unbias_exp(bvs2, biased_exp)); + TRACE("fp_rewriter", tout << "v = " << m_util.fm().to_string(v) << std::endl;); + result = m_util.mk_value(v); + return BR_DONE; + } + + return BR_FAILED; +} + +br_status float_rewriter::mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result) { + return BR_FAILED; +} + +br_status float_rewriter::mk_to_real(expr * arg1, expr_ref & result) { + return BR_FAILED; +} \ No newline at end of file diff --git a/src/ast/rewriter/float_rewriter.h b/src/ast/rewriter/float_rewriter.h index 4a0879d4b..0f44d227c 100644 --- a/src/ast/rewriter/float_rewriter.h +++ b/src/ast/rewriter/float_rewriter.h @@ -73,6 +73,12 @@ public: br_status mk_is_sign_minus(expr * arg1, expr_ref & result); br_status mk_to_ieee_bv(expr * arg1, expr_ref & result); + + br_status mk_fp(expr * arg1, expr * arg2, expr * arg3, expr_ref & result); + br_status mk_to_fp_unsigned(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_to_ubv(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_to_sbv(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_to_real(expr * arg1, expr_ref & result); }; #endif diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp index 2a7de3176..7fd44c088 100644 --- a/src/cmd_context/interpolant_cmds.cpp +++ b/src/cmd_context/interpolant_cmds.cpp @@ -114,7 +114,7 @@ static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ ptr_vector::const_iterator it = ctx.begin_assertions(); ptr_vector::const_iterator end = ctx.end_assertions(); - ptr_vector cnsts(end - it); + ptr_vector cnsts((unsigned)(end - it)); for (int i = 0; it != end; ++it, ++i) cnsts[i] = *it; @@ -139,10 +139,11 @@ static void get_interpolant(cmd_context & ctx, expr * t, params_ref &m_params) { get_interpolant_and_maybe_check(ctx,t,m_params,false); } +#if 0 static void get_and_check_interpolant(cmd_context & ctx, params_ref &m_params, expr * t) { get_interpolant_and_maybe_check(ctx,t,m_params,true); } - +#endif static void compute_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_ref &m_params, bool check){ diff --git a/src/duality/duality.h b/src/duality/duality.h old mode 100644 new mode 100755 index 166e8ef0d..7db9a4479 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -25,7 +25,7 @@ Revision History: #include // make hash_map and hash_set available -#ifndef WIN32 +#ifndef _WINDOWS using namespace stl_ext; #endif @@ -36,12 +36,11 @@ namespace Duality { struct Z3User { context &ctx; - solver &slvr; typedef func_decl FuncDecl; typedef expr Term; - Z3User(context &_ctx, solver &_slvr) : ctx(_ctx), slvr(_slvr){} + Z3User(context &_ctx) : ctx(_ctx){} const char *string_of_int(int n); @@ -53,6 +52,8 @@ namespace Duality { Term SubstRec(hash_map &memo, const Term &t); + Term SubstRec(hash_map &memo, hash_map &map, const Term &t); + void Strengthen(Term &x, const Term &y); // return the func_del of an app if it is uninterpreted @@ -77,11 +78,42 @@ namespace Duality { void Summarize(const Term &t); - int CumulativeDecisions(); + int CountOperators(const Term &t); - private: + Term SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val); + + Term RemoveRedundancy(const Term &t); + + Term IneqToEq(const Term &t); + + bool IsLiteral(const expr &lit, expr &atom, expr &val); + + expr Negate(const expr &f); + + expr SimplifyAndOr(const std::vector &args, bool is_and); + + expr ReallySimplifyAndOr(const std::vector &args, bool is_and); + + int MaxIndex(hash_map &memo, const Term &t); + + bool IsClosedFormula(const Term &t); + + Term AdjustQuantifiers(const Term &t); + + FuncDecl RenumberPred(const FuncDecl &f, int n); + +protected: void SummarizeRec(hash_set &memo, std::vector &lits, int &ops, const Term &t); + int CountOperatorsRec(hash_set &memo, const Term &t); + void RemoveRedundancyOp(bool pol, std::vector &args, hash_map &smemo); + Term RemoveRedundancyRec(hash_map &memo, hash_map &smemo, const Term &t); + Term SubstAtomTriv(const expr &foo, const expr &atom, const expr &val); + expr ReduceAndOr(const std::vector &args, bool is_and, std::vector &res); + expr FinishAndOr(const std::vector &args, bool is_and); + expr PullCommonFactors(std::vector &args, bool is_and); + Term IneqToEqRec(hash_map &memo, const Term &t); + }; @@ -142,6 +174,7 @@ namespace Duality { context *ctx; /** Z3 context for formulas */ solver *slvr; /** Z3 solver */ bool need_goals; /** Can the solver use the goal tree to optimize interpolants? */ + solver aux_solver; /** For temporary use -- don't leave assertions here. */ /** Tree interpolation. This method assumes the formulas in TermTree "assumptions" are currently asserted in the solver. The return @@ -167,6 +200,9 @@ namespace Duality { /** Assert a background axiom. */ virtual void assert_axiom(const expr &axiom) = 0; + /** Get the background axioms. */ + virtual const std::vector &get_axioms() = 0; + /** Return a string describing performance. */ virtual std::string profile() = 0; @@ -178,6 +214,12 @@ namespace Duality { /** Cancel, throw Canceled object if possible. */ virtual void cancel(){ } + /* Note: aux solver uses extensional array theory, since it + needs to be able to produce counter-models for + interpolants the have array equalities in them. + */ + LogicSolver(context &c) : aux_solver(c,true){} + virtual ~LogicSolver(){} }; @@ -202,6 +244,10 @@ namespace Duality { islvr->AssertInterpolationAxiom(axiom); } + const std::vector &get_axioms() { + return islvr->GetInterpolationAxioms(); + } + std::string profile(){ return islvr->profile(); } @@ -215,9 +261,9 @@ namespace Duality { } #endif - iZ3LogicSolver(context &c){ + iZ3LogicSolver(context &c, bool models = true) : LogicSolver(c) { ctx = ictx = &c; - slvr = islvr = new interpolating_solver(*ictx); + slvr = islvr = new interpolating_solver(*ictx, models); need_goals = false; islvr->SetWeakInterpolants(true); } @@ -267,8 +313,8 @@ namespace Duality { } LogicSolver *ls; - - private: + + protected: int nodeCount; int edgeCount; @@ -277,16 +323,19 @@ namespace Duality { public: std::list edges; std::list nodes; + std::list > constraints; }; public: model dualModel; - private: + protected: literals dualLabels; std::list stack; std::vector axioms; // only saved here for printing purposes - + solver &aux_solver; + hash_set *proof_core; + public: /** Construct an RPFP graph with a given interpolating prover context. It is allowed to @@ -296,16 +345,17 @@ namespace Duality { inherit the axioms. */ - RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx), *(_ls->slvr)), dualModel(*(_ls->ctx)) + RPFP(LogicSolver *_ls) : Z3User(*(_ls->ctx)), dualModel(*(_ls->ctx)), aux_solver(_ls->aux_solver) { ls = _ls; nodeCount = 0; edgeCount = 0; stack.push_back(stack_entry()); HornClauses = false; + proof_core = 0; } - ~RPFP(); + virtual ~RPFP(); /** Symbolic representation of a relational transformer */ class Transformer @@ -351,10 +401,10 @@ namespace Duality { bool SubsetEq(const Transformer &other){ Term t = owner->SubstParams(other.IndParams,IndParams,other.Formula); expr test = Formula && !t; - owner->slvr.push(); - owner->slvr.add(test); - check_result res = owner->slvr.check(); - owner->slvr.pop(1); + owner->aux_solver.push(); + owner->aux_solver.add(test); + check_result res = owner->aux_solver.check(); + owner->aux_solver.pop(1); return res == unsat; } @@ -444,6 +494,19 @@ namespace Duality { return n; } + /** Delete a node. You can only do this if not connected to any edges.*/ + void DeleteNode(Node *node){ + if(node->Outgoing || !node->Incoming.empty()) + throw "cannot delete RPFP node"; + for(std::vector::iterator it = nodes.end(), en = nodes.begin(); it != en;){ + if(*(--it) == node){ + nodes.erase(it); + break; + } + } + delete node; + } + /** This class represents a hyper-edge in the RPFP graph */ class Edge @@ -460,6 +523,7 @@ namespace Duality { hash_map varMap; Edge *map; Term labeled; + std::vector constraints; Edge(Node *_Parent, const Transformer &_F, const std::vector &_Children, RPFP *_owner, int _number) : F(_F), Parent(_Parent), Children(_Children), dual(expr(_owner->ctx)) { @@ -480,6 +544,29 @@ namespace Duality { return e; } + + /** Delete a hyper-edge and unlink it from any nodes. */ + void DeleteEdge(Edge *edge){ + if(edge->Parent) + edge->Parent->Outgoing = 0; + for(unsigned int i = 0; i < edge->Children.size(); i++){ + std::vector &ic = edge->Children[i]->Incoming; + for(std::vector::iterator it = ic.begin(), en = ic.end(); it != en; ++it){ + if(*it == edge){ + ic.erase(it); + break; + } + } + } + for(std::vector::iterator it = edges.end(), en = edges.begin(); it != en;){ + if(*(--it) == edge){ + edges.erase(it); + break; + } + } + delete edge; + } + /** Create an edge that lower-bounds its parent. */ Edge *CreateLowerBoundEdge(Node *_Parent) { @@ -492,15 +579,28 @@ namespace Duality { * you must pop the context accordingly. The second argument is * the number of pushes we are inside. */ - void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); + virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); + + /* Constrain an edge by the annotation of one of its children. */ + + void ConstrainParent(Edge *parent, Node *child); - /** For incremental solving, asserts the negation of the upper bound associated * with a node. * */ void AssertNode(Node *n); + /** Assert a constraint on an edge in the SMT context. + */ + void ConstrainEdge(Edge *e, const Term &t); + + /** Fix the truth values of atomic propositions in the given + edge to their values in the current assignment. */ + void FixCurrentState(Edge *root); + + void FixCurrentStateFull(Edge *edge, const expr &extra); + /** Declare a constant in the background theory. */ void DeclareConstant(const FuncDecl &f); @@ -554,9 +654,13 @@ namespace Duality { lbool Solve(Node *root, int persist); + /** Same as Solve, but annotates only a single node. */ + + lbool SolveSingleNode(Node *root, Node *node); + /** Get the constraint tree (but don't solve it) */ - TermTree *GetConstraintTree(Node *root); + TermTree *GetConstraintTree(Node *root, Node *skip_descendant = 0); /** Dispose of the dual model (counterexample) if there is one. */ @@ -592,6 +696,13 @@ namespace Duality { Term ComputeUnderapprox(Node *root, int persist); + /** Try to strengthen the annotation of a node by removing disjuncts. */ + void Generalize(Node *root, Node *node); + + + /** Compute disjunctive interpolant for node by case splitting */ + void InterpolateByCases(Node *root, Node *node); + /** Push a scope. Assertions made after Push can be undone by Pop. */ void Push(); @@ -623,6 +734,16 @@ namespace Duality { /** Pop a scope (see Push). Note, you cannot pop axioms. */ void Pop(int num_scopes); + + /** Erase the proof by performing a Pop, Push and re-assertion of + all the popped constraints */ + void PopPush(); + + /** Return true if the given edge is used in the proof of unsat. + Can be called only after Solve or Check returns an unsat result. */ + + bool EdgeUsedInProof(Edge *edge); + /** Convert a collection of clauses to Nodes and Edges in the RPFP. @@ -661,7 +782,7 @@ namespace Duality { }; -#ifdef WIN32 +#ifdef _WINDOWS __declspec(dllexport) #endif void FromClauses(const std::vector &clauses); @@ -692,9 +813,31 @@ namespace Duality { /** Edges of the graph. */ std::vector edges; + /** Fuse a vector of transformers. If the total number of inputs of the transformers + is N, then the result is an N-ary transfomer whose output is the union of + the outputs of the given transformers. The is, suppose we have a vetor of transfoermers + {T_i(r_i1,...,r_iN(i) : i=1..M}. The the result is a transformer + + F(r_11,...,r_iN(1),...,r_M1,...,r_MN(M)) = + T_1(r_11,...,r_iN(1)) U ... U T_M(r_M1,...,r_MN(M)) + */ + + Transformer Fuse(const std::vector &trs); + + /** Fuse edges so that each node is the output of at most one edge. This + transformation is solution-preserving, but changes the numbering of edges in + counterexamples. + */ + void FuseEdges(); + + void RemoveDeadNodes(); + Term SubstParams(const std::vector &from, const std::vector &to, const Term &t); + Term SubstParamsNoCapture(const std::vector &from, + const std::vector &to, const Term &t); + Term Localize(Edge *e, const Term &t); void EvalNodeAsConstraint(Node *p, Transformer &res); @@ -707,8 +850,25 @@ namespace Duality { // int GetLabelsRec(hash_map *memo, const Term &f, std::vector &labels, bool labpos); - private: + /** Compute and save the proof core for future calls to + EdgeUsedInProof. You only need to call this if you will pop + the solver before calling EdgeUsedInProof. + */ + void ComputeProofCore(); + + int CumulativeDecisions(); + + solver &slvr(){ + return *ls->slvr; + } + + protected: + void ClearProofCore(){ + if(proof_core) + delete proof_core; + proof_core = 0; + } Term SuffixVariable(const Term &t, int n); @@ -724,10 +884,14 @@ namespace Duality { Term ReducedDualEdge(Edge *e); - TermTree *ToTermTree(Node *root); + TermTree *ToTermTree(Node *root, Node *skip_descendant = 0); TermTree *ToGoalTree(Node *root); + void CollapseTermTreeRec(TermTree *root, TermTree *node); + + TermTree *CollapseTermTree(TermTree *node); + void DecodeTree(Node *root, TermTree *interp, int persist); Term GetUpperBound(Node *n); @@ -777,6 +941,11 @@ namespace Duality { Term UnderapproxFormula(const Term &f, hash_set &dont_cares); + void ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, + hash_set &done, hash_set &dont_cares); + + Term UnderapproxFullFormula(const Term &f, hash_set &dont_cares); + Term ToRuleRec(Edge *e, hash_map &memo, const Term &t, std::vector &quants); hash_map resolve_ite_memo; @@ -803,10 +972,80 @@ namespace Duality { Term SubstBound(hash_map &subst, const Term &t); + void ConstrainEdgeLocalized(Edge *e, const Term &t); + + void GreedyReduce(solver &s, std::vector &conjuncts); + + void NegateLits(std::vector &lits); + + expr SimplifyOr(std::vector &lits); + + expr SimplifyAnd(std::vector &lits); + + void SetAnnotation(Node *root, const expr &t); + + void AddEdgeToSolver(Edge *edge); + + void AddToProofCore(hash_set &core); + + void GetGroundLitsUnderQuants(hash_set *memo, const Term &f, std::vector &res, int under); + + Term StrengthenFormulaByCaseSplitting(const Term &f, std::vector &case_lits); + + expr NegateLit(const expr &f); + + expr GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox); + + bool IsVar(const expr &t); + + void GetVarsRec(hash_set &memo, const expr &cnst, std::vector &vars); + + expr UnhoistPullRec(hash_map & memo, const expr &w, hash_map & init_defs, hash_map & const_params, hash_map &const_params_inv, std::vector &new_params); + + void AddParamsToTransformer(Transformer &trans, const std::vector ¶ms); + + expr AddParamsToApp(const expr &app, const func_decl &new_decl, const std::vector ¶ms); + + expr GetRelRec(hash_set &memo, const expr &t, const func_decl &rel); + + expr GetRel(Edge *edge, int child_idx); + + void GetDefs(const expr &cnst, hash_map &defs); + + void GetDefsRec(const expr &cnst, hash_map &defs); + + void AddParamsToNode(Node *node, const std::vector ¶ms); + + void UnhoistLoop(Edge *loop_edge, Edge *init_edge); + + void Unhoist(); + + Term ElimIteRec(hash_map &memo, const Term &t, std::vector &cnsts); + + Term ElimIte(const Term &t); + + void MarkLiveNodes(hash_map > &outgoing, hash_set &live_nodes, Node *node); + + virtual void slvr_add(const expr &e); + + virtual void slvr_pop(int i); + + virtual void slvr_push(); + + virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0); + + virtual lbool ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false); + + virtual bool proof_core_contains(const expr &e); }; - /** RPFP solver base class. */ + + /** RPFP solver base class. */ class Solver { @@ -850,5 +1089,179 @@ namespace Duality { /** Object thrown on cancellation */ struct Canceled {}; + /** Object thrown on incompleteness */ + struct Incompleteness {}; }; } + + +// Allow to hash on nodes and edges in deterministic way + +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const Duality::RPFP::Node *p) const { + return p->number; + } + }; +} + +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const Duality::RPFP::Edge *p) const { + return p->number; + } + }; +} + +// allow to walk sets of nodes without address dependency + +namespace std { + template <> + class less { + public: + bool operator()(Duality::RPFP::Node * const &s, Duality::RPFP::Node * const &t) const { + return s->number < t->number; // s.raw()->get_id() < t.raw()->get_id(); + } + }; +} + +// #define LIMIT_STACK_WEIGHT 5 + + +namespace Duality { + /** Caching version of RPFP. Instead of asserting constraints, returns assumption literals */ + + class RPFP_caching : public RPFP { + public: + + /** appends assumption literals for edge to lits. if with_children is true, + includes that annotation of the edge's children. + */ + void AssertEdgeCache(Edge *e, std::vector &lits, bool with_children = false); + + /** appends assumption literals for node to lits */ + void AssertNodeCache(Node *, std::vector lits); + + /** check assumption lits, and return core */ + check_result CheckCore(const std::vector &assumps, std::vector &core); + + /** Clone another RPFP into this one, keeping a map */ + void Clone(RPFP *other); + + /** Get the clone of a node */ + Node *GetNodeClone(Node *other_node); + + /** Get the clone of an edge */ + Edge *GetEdgeClone(Edge *other_edge); + + /** Try to strengthen the parent of an edge */ + void GeneralizeCache(Edge *edge); + + /** Try to propagate some facts from children to parents of edge. + Return true if success. */ + bool PropagateCache(Edge *edge); + + /** Construct a caching RPFP using a LogicSolver */ + RPFP_caching(LogicSolver *_ls) : RPFP(_ls) {} + + /** Constraint an edge by its child's annotation. Return + assumption lits. */ + void ConstrainParentCache(Edge *parent, Node *child, std::vector &lits); + +#ifdef LIMIT_STACK_WEIGHT + virtual void AssertEdge(Edge *e, int persist = 0, bool with_children = false, bool underapprox = false); +#endif + + virtual ~RPFP_caching(){} + + protected: + hash_map AssumptionLits; + hash_map NodeCloneMap; + hash_map EdgeCloneMap; + std::vector alit_stack; + std::vector alit_stack_sizes; + + // to let us use one solver per edge + struct edge_solver { + hash_map AssumptionLits; + uptr slvr; + }; + hash_map edge_solvers; + +#ifdef LIMIT_STACK_WEIGHT + struct weight_counter { + int val; + weight_counter(){val = 0;} + void swap(weight_counter &other){ + std::swap(val,other.val); + } + }; + + struct big_stack_entry { + weight_counter weight_added; + std::vector new_alits; + std::vector alit_stack; + std::vector alit_stack_sizes; + }; + + std::vector new_alits; + weight_counter weight_added; + std::vector big_stack; +#endif + + + + void GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map = 0); + + void GreedyReduceCache(std::vector &assumps, std::vector &core); + + void FilterCore(std::vector &core, std::vector &full_core); + void ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector &lits); + + virtual void slvr_add(const expr &e); + + virtual void slvr_pop(int i); + + virtual void slvr_push(); + + virtual check_result slvr_check(unsigned n = 0, expr * const assumptions = 0, unsigned *core_size = 0, expr *core = 0); + + virtual lbool ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals = 0, + bool weak = false); + + virtual bool proof_core_contains(const expr &e); + + void GetTermTreeAssertionLiterals(TermTree *assumptions); + + void GetTermTreeAssertionLiteralsRec(TermTree *assumptions); + + edge_solver &SolverForEdge(Edge *edge, bool models, bool axioms); + + public: + struct scoped_solver_for_edge { + solver *orig_slvr; + RPFP_caching *rpfp; + edge_solver *es; + scoped_solver_for_edge(RPFP_caching *_rpfp, Edge *edge, bool models = false, bool axioms = false){ + rpfp = _rpfp; + orig_slvr = rpfp->ls->slvr; + es = &(rpfp->SolverForEdge(edge,models,axioms)); + rpfp->ls->slvr = es->slvr.get(); + rpfp->AssumptionLits.swap(es->AssumptionLits); + } + ~scoped_solver_for_edge(){ + rpfp->ls->slvr = orig_slvr; + rpfp->AssumptionLits.swap(es->AssumptionLits); + } + }; + + }; + +} diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp index bec32c51a..a4e9e0240 100755 --- a/src/duality/duality_profiling.cpp +++ b/src/duality/duality_profiling.cpp @@ -25,7 +25,14 @@ Revision History: #include #include +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#endif + #include "duality_wrapper.h" +#include "iz3profiling.h" namespace Duality { @@ -103,6 +110,7 @@ namespace Duality { output_time(*pfs, it->second.t); (*pfs) << std::endl; } + profiling::print(os); // print the interpolation stats } void timer_start(const char *name){ diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp old mode 100644 new mode 100755 index 1c2927da8..5751fa890 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -21,10 +21,20 @@ Revision History: -#include "duality.h" -#include "duality_profiling.h" +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#endif + #include #include +#include +#include + + +#include "duality.h" +#include "duality_profiling.h" #ifndef WIN32 // #define Z3OPS @@ -89,18 +99,20 @@ namespace Duality { if(memo.find(t) != memo.end()) return; memo.insert(t); - decl_kind k = t.decl().get_decl_kind(); - if(k == And || k == Or || k == Not || k == Implies || k == Iff){ - ops++; - int nargs = t.num_args(); - for(int i = 0; i < nargs; i++) - SummarizeRec(memo,lits,ops,t.arg(i)); + if(t.is_app()){ + decl_kind k = t.decl().get_decl_kind(); + if(k == And || k == Or || k == Not || k == Implies || k == Iff){ + ops++; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + SummarizeRec(memo,lits,ops,t.arg(i)); + return; + } } - else - lits.push_back(t); + lits.push_back(t); } - int Z3User::CumulativeDecisions(){ + int RPFP::CumulativeDecisions(){ #if 0 std::string stats = Z3_statistics_to_string(ctx); int pos = stats.find("decisions:"); @@ -109,7 +121,7 @@ namespace Duality { std::string val = stats.substr(pos,end-pos); return atoi(val.c_str()); #endif - return slvr.get_num_decisions(); + return slvr().get_num_decisions(); } @@ -123,6 +135,32 @@ namespace Duality { } } + int Z3User::CountOperatorsRec(hash_set &memo, const Term &t){ + if(memo.find(t) != memo.end()) + return 0; + memo.insert(t); + if(t.is_app()){ + decl_kind k = t.decl().get_decl_kind(); + if(k == And || k == Or){ + int count = 1; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + count += CountOperatorsRec(memo,t.arg(i)); + return count; + } + return 0; + } + if(t.is_quantifier()) + return CountOperatorsRec(memo,t.body())+2; // count 2 for a quantifier + return 0; + } + + int Z3User::CountOperators(const Term &t){ + hash_set memo; + return CountOperatorsRec(memo,t); + } + + Z3User::Term Z3User::conjoin(const std::vector &args){ return ctx.make(And,args); } @@ -183,6 +221,7 @@ namespace Duality { return clone_quantifier(t,new_body); } + RPFP::Term RPFP::LocalizeRec(Edge *e, hash_map &memo, const Term &t) { std::pair foo(t,expr(ctx)); @@ -272,16 +311,21 @@ namespace Duality { return implies(b, Localize(e, e->F.Formula)); } - TermTree *RPFP::ToTermTree(Node *root) + TermTree *RPFP::ToTermTree(Node *root, Node *skip_descendant) { + if(skip_descendant && root == skip_descendant) + return new TermTree(ctx.bool_val(true)); Edge *e = root->Outgoing; if(!e) return new TermTree(ctx.bool_val(true), std::vector()); std::vector children(e->Children.size()); for(unsigned i = 0; i < children.size(); i++) - children[i] = ToTermTree(e->Children[i]); + children[i] = ToTermTree(e->Children[i],skip_descendant); // Term top = ReducedDualEdge(e); Term top = e->dual.null() ? ctx.bool_val(true) : e->dual; - return new TermTree(top, children); + TermTree *res = new TermTree(top, children); + for(unsigned i = 0; i < e->constraints.size(); i++) + res->addTerm(e->constraints[i]); + return res; } TermTree *RPFP::GetGoalTree(Node *root){ @@ -321,11 +365,319 @@ namespace Duality { res = f(args.size(),&args[0]); } else if (t.is_quantifier()) - res = CloneQuantifier(t,SubstRec(memo, t.body())); + { + std::vector pats; + t.get_patterns(pats); + for(unsigned i = 0; i < pats.size(); i++) + pats[i] = SubstRec(memo,pats[i]); + Term body = SubstRec(memo,t.body()); + res = clone_quantifier(t, body, pats); + } + // res = CloneQuantifier(t,SubstRec(memo, t.body())); else res = t; return res; } + Z3User::Term Z3User::SubstRec(hash_map &memo, hash_map &map, const Term &t) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()) + { + func_decl f = t.decl(); + std::vector args; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + args.push_back(SubstRec(memo, map, t.arg(i))); + hash_map::iterator it = map.find(f); + if(it != map.end()) + f = it->second; + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()) + { + std::vector pats; + t.get_patterns(pats); + for(unsigned i = 0; i < pats.size(); i++) + pats[i] = SubstRec(memo, map, pats[i]); + Term body = SubstRec(memo, map, t.body()); + res = clone_quantifier(t, body, pats); + } + // res = CloneQuantifier(t,SubstRec(memo, t.body())); + else res = t; + return res; + } + + bool Z3User::IsLiteral(const expr &lit, expr &atom, expr &val){ + if(!(lit.is_quantifier() && IsClosedFormula(lit))){ + if(!lit.is_app()) + return false; + decl_kind k = lit.decl().get_decl_kind(); + if(k == Not){ + if(IsLiteral(lit.arg(0),atom,val)){ + val = eq(val,ctx.bool_val(true)) ? ctx.bool_val(false) : ctx.bool_val(true); + return true; + } + return false; + } + if(k == And || k == Or || k == Iff || k == Implies) + return false; + } + atom = lit; + val = ctx.bool_val(true); + return true; + } + + expr Z3User::Negate(const expr &f){ + if(f.is_app() && f.decl().get_decl_kind() == Not) + return f.arg(0); + else if(eq(f,ctx.bool_val(true))) + return ctx.bool_val(false); + else if(eq(f,ctx.bool_val(false))) + return ctx.bool_val(true); + return !f; + } + + expr Z3User::ReduceAndOr(const std::vector &args, bool is_and, std::vector &res){ + for(unsigned i = 0; i < args.size(); i++) + if(!eq(args[i],ctx.bool_val(is_and))){ + if(eq(args[i],ctx.bool_val(!is_and))) + return ctx.bool_val(!is_and); + res.push_back(args[i]); + } + return expr(); + } + + expr Z3User::FinishAndOr(const std::vector &args, bool is_and){ + if(args.size() == 0) + return ctx.bool_val(is_and); + if(args.size() == 1) + return args[0]; + return ctx.make(is_and ? And : Or,args); + } + + expr Z3User::SimplifyAndOr(const std::vector &args, bool is_and){ + std::vector sargs; + expr res = ReduceAndOr(args,is_and,sargs); + if(!res.null()) return res; + return FinishAndOr(sargs,is_and); + } + + expr Z3User::PullCommonFactors(std::vector &args, bool is_and){ + + // first check if there's anything to do... + if(args.size() < 2) + return FinishAndOr(args,is_and); + for(unsigned i = 0; i < args.size(); i++){ + const expr &a = args[i]; + if(!(a.is_app() && a.decl().get_decl_kind() == (is_and ? Or : And))) + return FinishAndOr(args,is_and); + } + std::vector common; + for(unsigned i = 0; i < args.size(); i++){ + unsigned n = args[i].num_args(); + std::vector v(n),w; + for(unsigned j = 0; j < n; j++) + v[j] = args[i].arg(j); + std::less comp; + std::sort(v.begin(),v.end(),comp); + if(i == 0) + common.swap(v); + else { + std::set_intersection(common.begin(),common.end(),v.begin(),v.end(),std::inserter(w,w.begin()),comp); + common.swap(w); + } + } + if(common.empty()) + return FinishAndOr(args,is_and); + std::set common_set(common.begin(),common.end()); + for(unsigned i = 0; i < args.size(); i++){ + unsigned n = args[i].num_args(); + std::vector lits; + for(unsigned j = 0; j < n; j++){ + const expr b = args[i].arg(j); + if(common_set.find(b) == common_set.end()) + lits.push_back(b); + } + args[i] = SimplifyAndOr(lits,!is_and); + } + common.push_back(SimplifyAndOr(args,is_and)); + return SimplifyAndOr(common,!is_and); + } + + expr Z3User::ReallySimplifyAndOr(const std::vector &args, bool is_and){ + std::vector sargs; + expr res = ReduceAndOr(args,is_and,sargs); + if(!res.null()) return res; + return PullCommonFactors(sargs,is_and); + } + + Z3User::Term Z3User::SubstAtomTriv(const expr &foo, const expr &atom, const expr &val){ + if(eq(foo,atom)) + return val; + else if(foo.is_app() && foo.decl().get_decl_kind() == Not && eq(foo.arg(0),atom)) + return Negate(val); + else + return foo; + } + + Z3User::Term Z3User::SubstAtom(hash_map &memo, const expr &t, const expr &atom, const expr &val){ + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()){ + func_decl f = t.decl(); + decl_kind k = f.get_decl_kind(); + + // TODO: recur here, but how much? We don't want to be quadractic in formula size + + if(k == And || k == Or){ + int nargs = t.num_args(); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = SubstAtom(memo,t.arg(i),atom,val); + res = ReallySimplifyAndOr(args, k==And); + return res; + } + } + else if(t.is_quantifier() && atom.is_quantifier()){ + if(eq(t,atom)) + res = val; + else + res = clone_quantifier(t,SubstAtom(memo,t.body(),atom,val)); + return res; + } + res = SubstAtomTriv(t,atom,val); + return res; + } + + void Z3User::RemoveRedundancyOp(bool pol, std::vector &args, hash_map &smemo){ + for(unsigned i = 0; i < args.size(); i++){ + const expr &lit = args[i]; + expr atom, val; + if(IsLiteral(lit,atom,val)){ + if(atom.is_app() && atom.decl().get_decl_kind() == Equal) + if(pol ? eq(val,ctx.bool_val(true)) : eq(val,ctx.bool_val(false))){ + expr lhs = atom.arg(0), rhs = atom.arg(1); + if(lhs.is_numeral()) + std::swap(lhs,rhs); + if(rhs.is_numeral() && lhs.is_app()){ + for(unsigned j = 0; j < args.size(); j++) + if(j != i){ + smemo.clear(); + smemo[lhs] = rhs; + args[j] = SubstRec(smemo,args[j]); + } + } + } + for(unsigned j = 0; j < args.size(); j++) + if(j != i){ + smemo.clear(); + args[j] = SubstAtom(smemo,args[j],atom,pol ? val : !val); + } + } + } + } + + + Z3User::Term Z3User::RemoveRedundancyRec(hash_map &memo, hash_map &smemo, const Term &t) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()) + { + func_decl f = t.decl(); + std::vector args; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + args.push_back(RemoveRedundancyRec(memo, smemo, t.arg(i))); + + decl_kind k = f.get_decl_kind(); + if(k == And){ + RemoveRedundancyOp(true,args,smemo); + res = ReallySimplifyAndOr(args, true); + } + else if(k == Or){ + RemoveRedundancyOp(false,args,smemo); + res = ReallySimplifyAndOr(args, false); + } + else { + if(k == Equal && args[0].get_id() > args[1].get_id()) + std::swap(args[0],args[1]); + res = f(args.size(),&args[0]); + } + } + else if (t.is_quantifier()) + { + Term body = RemoveRedundancyRec(memo,smemo,t.body()); + res = clone_quantifier(t, body); + } + else res = t; + return res; + } + + Z3User::Term Z3User::RemoveRedundancy(const Term &t){ + hash_map memo; + hash_map smemo; + return RemoveRedundancyRec(memo,smemo,t); + } + + Z3User::Term Z3User::AdjustQuantifiers(const Term &t) + { + if(t.is_quantifier() || (t.is_app() && t.has_quantifiers())) + return t.qe_lite(); + return t; + } + + Z3User::Term Z3User::IneqToEqRec(hash_map &memo, const Term &t) + { + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()) + { + func_decl f = t.decl(); + std::vector args; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++) + args.push_back(IneqToEqRec(memo, t.arg(i))); + + decl_kind k = f.get_decl_kind(); + if(k == And){ + for(int i = 0; i < nargs-1; i++){ + if((args[i].is_app() && args[i].decl().get_decl_kind() == Geq && + args[i+1].is_app() && args[i+1].decl().get_decl_kind() == Leq) + || + (args[i].is_app() && args[i].decl().get_decl_kind() == Leq && + args[i+1].is_app() && args[i+1].decl().get_decl_kind() == Geq)) + if(eq(args[i].arg(0),args[i+1].arg(0)) && eq(args[i].arg(1),args[i+1].arg(1))){ + args[i] = ctx.make(Equal,args[i].arg(0),args[i].arg(1)); + args[i+1] = ctx.bool_val(true); + } + } + } + res = f(args.size(),&args[0]); + } + else if (t.is_quantifier()) + { + Term body = IneqToEqRec(memo,t.body()); + res = clone_quantifier(t, body); + } + else res = t; + return res; + } + + Z3User::Term Z3User::IneqToEq(const Term &t){ + hash_map memo; + return IneqToEqRec(memo,t); + } + Z3User::Term Z3User::SubstRecHide(hash_map &memo, const Term &t, int number) { std::pair foo(t,expr(ctx)); @@ -364,6 +716,51 @@ namespace Duality { return some_diff ? SubstRec(memo,t) : t; } + RPFP::Term RPFP::SubstParamsNoCapture(const std::vector &from, + const std::vector &to, const Term &t){ + hash_map memo; + bool some_diff = false; + for(unsigned i = 0; i < from.size(); i++) + if(i < to.size() && !eq(from[i],to[i])){ + memo[from[i]] = to[i]; + // if the new param is not being mapped to anything else, we need to rename it to prevent capture + // note, if the new param *is* mapped later in the list, it will override this substitution + const expr &w = to[i]; + if(memo.find(w) == memo.end()){ + std::string old_name = w.decl().name().str(); + func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), w.get_sort()); + expr y = fresh(); + memo[w] = y; + } + some_diff = true; + } + return some_diff ? SubstRec(memo,t) : t; + } + + + + RPFP::Transformer RPFP::Fuse(const std::vector &trs){ + assert(!trs.empty()); + const std::vector ¶ms = trs[0]->IndParams; + std::vector fmlas(trs.size()); + fmlas[0] = trs[0]->Formula; + for(unsigned i = 1; i < trs.size(); i++) + fmlas[i] = SubstParamsNoCapture(trs[i]->IndParams,params,trs[i]->Formula); + std::vector rel_params = trs[0]->RelParams; + for(unsigned i = 1; i < trs.size(); i++){ + const std::vector ¶ms2 = trs[i]->RelParams; + hash_map map; + for(unsigned j = 0; j < params2.size(); j++){ + func_decl rel = RenumberPred(params2[j],rel_params.size()); + rel_params.push_back(rel); + map[params2[j]] = rel; + } + hash_map memo; + fmlas[i] = SubstRec(memo,map,fmlas[i]); + } + return Transformer(rel_params,params,ctx.make(Or,fmlas),trs[0]->owner); + } + void Z3User::Strengthen(Term &x, const Term &y) { @@ -373,6 +770,19 @@ namespace Duality { x = x && y; } + void RPFP::SetAnnotation(Node *root, const expr &t){ + hash_map memo; + Term b; + std::vector v; + RedVars(root, b, v); + memo[b] = ctx.bool_val(true); + for (unsigned i = 0; i < v.size(); i++) + memo[v[i]] = root->Annotation.IndParams[i]; + Term annot = SubstRec(memo, t); + // Strengthen(ref root.Annotation.Formula, annot); + root->Annotation.Formula = annot; + } + void RPFP::DecodeTree(Node *root, TermTree *interp, int persist) { std::vector &ic = interp->getChildren(); @@ -382,16 +792,7 @@ namespace Duality { for (unsigned i = 0; i < nc.size(); i++) DecodeTree(nc[i], ic[i], persist); } - hash_map memo; - Term b; - std::vector v; - RedVars(root, b, v); - memo[b] = ctx.bool_val(true); - for (unsigned i = 0; i < v.size(); i++) - memo[v[i]] = root->Annotation.IndParams[i]; - Term annot = SubstRec(memo, interp->getTerm()); - // Strengthen(ref root.Annotation.Formula, annot); - root->Annotation.Formula = annot; + SetAnnotation(root,interp->getTerm()); #if 0 if(persist != 0) Z3_persist_ast(ctx,root->Annotation.Formula,persist); @@ -453,6 +854,33 @@ namespace Duality { #endif + expr RPFP::GetEdgeFormula(Edge *e, int persist, bool with_children, bool underapprox) + { + if (e->dual.null()) { + timer_start("ReducedDualEdge"); + e->dual = ReducedDualEdge(e); + timer_stop("ReducedDualEdge"); + timer_start("getting children"); + if(underapprox){ + std::vector cus(e->Children.size()); + for(unsigned i = 0; i < e->Children.size(); i++) + cus[i] = !UnderapproxFlag(e->Children[i]) || GetUnderapprox(e->Children[i]); + expr cnst = conjoin(cus); + e->dual = e->dual && cnst; + } + timer_stop("getting children"); + timer_start("Persisting"); + std::list::reverse_iterator it = stack.rbegin(); + for(int i = 0; i < persist && it != stack.rend(); i++) + it++; + if(it != stack.rend()) + it->edges.push_back(e); + timer_stop("Persisting"); + //Console.WriteLine("{0}", cnst); + } + return e->dual; + } + /** For incremental solving, asserts the constraint associated * with this edge in the SMT context. If this edge is removed, * you must pop the context accordingly. The second argument is @@ -474,41 +902,240 @@ namespace Duality { { if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty())) return; - if (e->dual.null()) - { - timer_start("ReducedDualEdge"); - e->dual = ReducedDualEdge(e); - timer_stop("ReducedDualEdge"); - timer_start("getting children"); - if(with_children) - for(unsigned i = 0; i < e->Children.size(); i++) - e->dual = e->dual && GetAnnotation(e->Children[i]); - if(underapprox){ - std::vector cus(e->Children.size()); - for(unsigned i = 0; i < e->Children.size(); i++) - cus[i] = !UnderapproxFlag(e->Children[i]) || GetUnderapprox(e->Children[i]); - expr cnst = conjoin(cus); - e->dual = e->dual && cnst; - } - timer_stop("getting children"); - timer_start("Persisting"); - std::list::reverse_iterator it = stack.rbegin(); - for(int i = 0; i < persist && it != stack.rend(); i++) - it++; - if(it != stack.rend()) - it->edges.push_back(e); -#if 0 - if(persist != 0) - Z3_persist_ast(ctx,e->dual,persist); -#endif - timer_stop("Persisting"); - //Console.WriteLine("{0}", cnst); - } + expr fmla = GetEdgeFormula(e, persist, with_children, underapprox); timer_start("solver add"); - slvr.add(e->dual); + slvr_add(e->dual); timer_stop("solver add"); + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + ConstrainParent(e,e->Children[i]); } + +#ifdef LIMIT_STACK_WEIGHT + void RPFP_caching::AssertEdge(Edge *e, int persist, bool with_children, bool underapprox) + { + unsigned old_new_alits = new_alits.size(); + if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty())) + return; + expr fmla = GetEdgeFormula(e, persist, with_children, underapprox); + timer_start("solver add"); + slvr_add(e->dual); + timer_stop("solver add"); + if(old_new_alits < new_alits.size()) + weight_added.val++; + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + ConstrainParent(e,e->Children[i]); + } +#endif + + // caching verion of above + void RPFP_caching::AssertEdgeCache(Edge *e, std::vector &lits, bool with_children){ + if(eq(e->F.Formula,ctx.bool_val(true)) && (!with_children || e->Children.empty())) + return; + expr fmla = GetEdgeFormula(e, 0, with_children, false); + GetAssumptionLits(fmla,lits); + if(with_children) + for(unsigned i = 0; i < e->Children.size(); i++) + ConstrainParentCache(e,e->Children[i],lits); + } + + void RPFP::slvr_add(const expr &e){ + slvr().add(e); + } + + void RPFP_caching::slvr_add(const expr &e){ + GetAssumptionLits(e,alit_stack); + } + + void RPFP::slvr_pop(int i){ + slvr().pop(i); + } + + void RPFP::slvr_push(){ + slvr().push(); + } + + void RPFP_caching::slvr_pop(int i){ + for(int j = 0; j < i; j++){ +#ifdef LIMIT_STACK_WEIGHT + if(alit_stack_sizes.empty()){ + if(big_stack.empty()) + throw "stack underflow"; + for(unsigned k = 0; k < new_alits.size(); k++){ + if(AssumptionLits.find(new_alits[k]) == AssumptionLits.end()) + throw "foo!"; + AssumptionLits.erase(new_alits[k]); + } + big_stack_entry &bsb = big_stack.back(); + bsb.alit_stack_sizes.swap(alit_stack_sizes); + bsb.alit_stack.swap(alit_stack); + bsb.new_alits.swap(new_alits); + bsb.weight_added.swap(weight_added); + big_stack.pop_back(); + slvr().pop(1); + continue; + } +#endif + alit_stack.resize(alit_stack_sizes.back()); + alit_stack_sizes.pop_back(); + } + } + + void RPFP_caching::slvr_push(){ +#ifdef LIMIT_STACK_WEIGHT + if(weight_added.val > LIMIT_STACK_WEIGHT){ + big_stack.resize(big_stack.size()+1); + big_stack_entry &bsb = big_stack.back(); + bsb.alit_stack_sizes.swap(alit_stack_sizes); + bsb.alit_stack.swap(alit_stack); + bsb.new_alits.swap(new_alits); + bsb.weight_added.swap(weight_added); + slvr().push(); + for(unsigned i = 0; i < bsb.alit_stack.size(); i++) + slvr().add(bsb.alit_stack[i]); + return; + } +#endif + alit_stack_sizes.push_back(alit_stack.size()); + } + + check_result RPFP::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){ + return slvr().check(n, assumptions, core_size, core); + } + + check_result RPFP_caching::slvr_check(unsigned n, expr * const assumptions, unsigned *core_size, expr *core){ + unsigned oldsiz = alit_stack.size(); + if(n && assumptions) + std::copy(assumptions,assumptions+n,std::inserter(alit_stack,alit_stack.end())); + check_result res; + if(core_size && core){ + std::vector full_core(alit_stack.size()), core1(n); + std::copy(assumptions,assumptions+n,core1.begin()); + res = slvr().check(alit_stack.size(), &alit_stack[0], core_size, &full_core[0]); + full_core.resize(*core_size); + if(res == unsat){ + FilterCore(core1,full_core); + *core_size = core1.size(); + std::copy(core1.begin(),core1.end(),core); + } + } + else + res = slvr().check(alit_stack.size(), &alit_stack[0]); + alit_stack.resize(oldsiz); + return res; + } + + lbool RPFP::ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals, + bool weak){ + return ls->interpolate_tree(assumptions, interpolants, _model, goals, weak); + } + + lbool RPFP_caching::ls_interpolate_tree(TermTree *assumptions, + TermTree *&interpolants, + model &_model, + TermTree *goals, + bool weak){ + GetTermTreeAssertionLiterals(assumptions); + return ls->interpolate_tree(assumptions, interpolants, _model, goals, weak); + } + + void RPFP_caching::GetTermTreeAssertionLiteralsRec(TermTree *assumptions){ + std::vector alits; + hash_map map; + GetAssumptionLits(assumptions->getTerm(),alits,&map); + std::vector &ts = assumptions->getTerms(); + for(unsigned i = 0; i < ts.size(); i++) + GetAssumptionLits(ts[i],alits,&map); + assumptions->setTerm(ctx.bool_val(true)); + ts = alits; + for(unsigned i = 0; i < alits.size(); i++) + ts.push_back(ctx.make(Implies,alits[i],map[alits[i]])); + for(unsigned i = 0; i < assumptions->getChildren().size(); i++) + GetTermTreeAssertionLiterals(assumptions->getChildren()[i]); + return; + } + + void RPFP_caching::GetTermTreeAssertionLiterals(TermTree *assumptions){ + // optimize binary case + if(assumptions->getChildren().size() == 1 + && assumptions->getChildren()[0]->getChildren().size() == 0){ + hash_map map; + TermTree *child = assumptions->getChildren()[0]; + std::vector dummy; + GetAssumptionLits(child->getTerm(),dummy,&map); + std::vector &ts = child->getTerms(); + for(unsigned i = 0; i < ts.size(); i++) + GetAssumptionLits(ts[i],dummy,&map); + std::vector assumps; + slvr().get_proof().get_assumptions(assumps); + if(!proof_core){ // save the proof core for later use + proof_core = new hash_set; + for(unsigned i = 0; i < assumps.size(); i++) + proof_core->insert(assumps[i]); + } + std::vector *cnsts[2] = {&child->getTerms(),&assumptions->getTerms()}; + for(unsigned i = 0; i < assumps.size(); i++){ + expr &ass = assumps[i]; + expr alit = (ass.is_app() && ass.decl().get_decl_kind() == Implies) ? ass.arg(0) : ass; + bool isA = map.find(alit) != map.end(); + cnsts[isA ? 0 : 1]->push_back(ass); + } + } + else + GetTermTreeAssertionLiteralsRec(assumptions); + } + + void RPFP::AddToProofCore(hash_set &core){ + std::vector assumps; + slvr().get_proof().get_assumptions(assumps); + for(unsigned i = 0; i < assumps.size(); i++) + core.insert(assumps[i]); + } + + void RPFP::ComputeProofCore(){ + if(!proof_core){ + proof_core = new hash_set; + AddToProofCore(*proof_core); + } + } + + + void RPFP_caching::GetAssumptionLits(const expr &fmla, std::vector &lits, hash_map *opt_map){ + std::vector conjs; + CollectConjuncts(fmla,conjs); + for(unsigned i = 0; i < conjs.size(); i++){ + const expr &conj = conjs[i]; + std::pair foo(conj,expr(ctx)); + std::pair::iterator, bool> bar = AssumptionLits.insert(foo); + Term &res = bar.first->second; + if(bar.second){ + func_decl pred = ctx.fresh_func_decl("@alit", ctx.bool_sort()); + res = pred(); +#ifdef LIMIT_STACK_WEIGHT + new_alits.push_back(conj); +#endif + slvr().add(ctx.make(Implies,res,conj)); + // std::cout << res << ": " << conj << "\n"; + } + if(opt_map) + (*opt_map)[res] = conj; + lits.push_back(res); + } + } + + void RPFP::ConstrainParent(Edge *parent, Node *child){ + ConstrainEdgeLocalized(parent,GetAnnotation(child)); + } + + void RPFP_caching::ConstrainParentCache(Edge *parent, Node *child, std::vector &lits){ + ConstrainEdgeLocalizedCache(parent,GetAnnotation(child),lits); + } + /** For incremental solving, asserts the negation of the upper bound associated * with a node. @@ -520,10 +1147,84 @@ namespace Duality { { n->dual = GetUpperBound(n); stack.back().nodes.push_back(n); - slvr.add(n->dual); + slvr_add(n->dual); } } + // caching version of above + void RPFP_caching::AssertNodeCache(Node *n, std::vector lits){ + if (n->dual.null()) + { + n->dual = GetUpperBound(n); + stack.back().nodes.push_back(n); + GetAssumptionLits(n->dual,lits); + } + } + + /** Clone another RPFP into this one, keeping a map */ + void RPFP_caching::Clone(RPFP *other){ +#if 0 + for(unsigned i = 0; i < other->nodes.size(); i++) + NodeCloneMap[other->nodes[i]] = CloneNode(other->nodes[i]); +#endif + for(unsigned i = 0; i < other->edges.size(); i++){ + Edge *edge = other->edges[i]; + Node *parent = CloneNode(edge->Parent); + std::vector cs; + for(unsigned j = 0; j < edge->Children.size(); j++) + // cs.push_back(NodeCloneMap[edge->Children[j]]); + cs.push_back(CloneNode(edge->Children[j])); + EdgeCloneMap[edge] = CreateEdge(parent,edge->F,cs); + } + } + + /** Get the clone of a node */ + RPFP::Node *RPFP_caching::GetNodeClone(Node *other_node){ + return NodeCloneMap[other_node]; + } + + /** Get the clone of an edge */ + RPFP::Edge *RPFP_caching::GetEdgeClone(Edge *other_edge){ + return EdgeCloneMap[other_edge]; + } + + /** check assumption lits, and return core */ + check_result RPFP_caching::CheckCore(const std::vector &assumps, std::vector &core){ + core.resize(assumps.size()); + unsigned core_size; + check_result res = slvr().check(assumps.size(),(expr *)&assumps[0],&core_size,&core[0]); + if(res == unsat) + core.resize(core_size); + else + core.clear(); + return res; + } + + + /** Assert a constraint on an edge in the SMT context. + */ + + void RPFP::ConstrainEdge(Edge *e, const Term &t) + { + Term tl = Localize(e, t); + ConstrainEdgeLocalized(e,tl); + } + + void RPFP::ConstrainEdgeLocalized(Edge *e, const Term &tl) + { + e->constraints.push_back(tl); + stack.back().constraints.push_back(std::pair(e,tl)); + slvr_add(tl); + } + + void RPFP_caching::ConstrainEdgeLocalizedCache(Edge *e, const Term &tl, std::vector &lits) + { + e->constraints.push_back(tl); + stack.back().constraints.push_back(std::pair(e,tl)); + GetAssumptionLits(tl,lits); + } + + /** Declare a constant in the background theory. */ void RPFP::DeclareConstant(const FuncDecl &f){ @@ -549,7 +1250,7 @@ namespace Duality { void RPFP::RemoveAxiom(const Term &t) { - slvr.RemoveInterpolationAxiom(t); + slvr().RemoveInterpolationAxiom(t); } #endif @@ -592,12 +1293,13 @@ namespace Duality { TermTree *goals = NULL; if(ls->need_goals) goals = GetGoalTree(root); + ClearProofCore(); // if (dualModel != null) dualModel.Dispose(); // if (dualLabels != null) dualLabels.Dispose(); timer_start("interpolate_tree"); - lbool res = ls->interpolate_tree(tree, interpolant, dualModel,goals,true); + lbool res = ls_interpolate_tree(tree, interpolant, dualModel,goals,true); timer_stop("interpolate_tree"); if (res == l_false) { @@ -613,11 +1315,54 @@ namespace Duality { return res; } + void RPFP::CollapseTermTreeRec(TermTree *root, TermTree *node){ + root->addTerm(node->getTerm()); + std::vector &cnsts = node->getTerms(); + for(unsigned i = 0; i < cnsts.size(); i++) + root->addTerm(cnsts[i]); + std::vector &chs = node->getChildren(); + for(unsigned i = 0; i < chs.size(); i++){ + CollapseTermTreeRec(root,chs[i]); + } + } + + TermTree *RPFP::CollapseTermTree(TermTree *node){ + std::vector &chs = node->getChildren(); + for(unsigned i = 0; i < chs.size(); i++) + CollapseTermTreeRec(node,chs[i]); + for(unsigned i = 0; i < chs.size(); i++) + delete chs[i]; + chs.clear(); + return node; + } + + lbool RPFP::SolveSingleNode(Node *root, Node *node) + { + timer_start("Solve"); + TermTree *tree = CollapseTermTree(GetConstraintTree(root,node)); + tree->getChildren().push_back(CollapseTermTree(ToTermTree(node))); + TermTree *interpolant = NULL; + ClearProofCore(); + + timer_start("interpolate_tree"); + lbool res = ls_interpolate_tree(tree, interpolant, dualModel,0,true); + timer_stop("interpolate_tree"); + if (res == l_false) + { + DecodeTree(node, interpolant->getChildren()[0], 0); + delete interpolant; + } + + delete tree; + timer_stop("Solve"); + return res; + } + /** Get the constraint tree (but don't solve it) */ - TermTree *RPFP::GetConstraintTree(Node *root) + TermTree *RPFP::GetConstraintTree(Node *root, Node *skip_descendant) { - return AddUpperBound(root, ToTermTree(root)); + return AddUpperBound(root, ToTermTree(root,skip_descendant)); } /** Dispose of the dual model (counterexample) if there is one. */ @@ -646,25 +1391,27 @@ namespace Duality { check_result RPFP::Check(Node *root, std::vector underapproxes, std::vector *underapprox_core ) { + timer_start("Check"); + ClearProofCore(); // if (dualModel != null) dualModel.Dispose(); check_result res; if(!underapproxes.size()) - res = slvr.check(); + res = slvr_check(); else { std::vector us(underapproxes.size()); for(unsigned i = 0; i < underapproxes.size(); i++) us[i] = UnderapproxFlag(underapproxes[i]); - slvr.check(); // TODO: no idea why I need to do this + slvr_check(); // TODO: no idea why I need to do this if(underapprox_core){ std::vector unsat_core(us.size()); unsigned core_size = 0; - res = slvr.check(us.size(),&us[0],&core_size,&unsat_core[0]); + res = slvr_check(us.size(),&us[0],&core_size,&unsat_core[0]); underapprox_core->resize(core_size); for(unsigned i = 0; i < core_size; i++) (*underapprox_core)[i] = UnderapproxFlagRev(unsat_core[i]); } else { - res = slvr.check(us.size(),&us[0]); + res = slvr_check(us.size(),&us[0]); bool dump = false; if(dump){ std::vector cnsts; @@ -674,16 +1421,20 @@ namespace Duality { ls->write_interpolation_problem("temp.smt",cnsts,std::vector()); } } - // check_result temp = slvr.check(); + // check_result temp = slvr_check(); } - dualModel = slvr.get_model(); + dualModel = slvr().get_model(); + timer_stop("Check"); return res; } check_result RPFP::CheckUpdateModel(Node *root, std::vector assumps){ - // check_result temp1 = slvr.check(); // no idea why I need to do this - check_result res = slvr.check_keep_model(assumps.size(),&assumps[0]); - dualModel = slvr.get_model(); + // check_result temp1 = slvr_check(); // no idea why I need to do this + ClearProofCore(); + check_result res = slvr_check(assumps.size(),&assumps[0]); + model mod = slvr().get_model(); + if(!mod.null()) + dualModel = mod;; return res; } @@ -696,8 +1447,6 @@ namespace Duality { return dualModel.eval(tl); } - - /** Returns true if the given node is empty in the primal solution. For proecudure summaries, this means that the procedure is not called in the current counter-model. */ @@ -975,7 +1724,7 @@ namespace Duality { } } /* Unreachable! */ - throw "error in RPFP::GetLabelsRec"; + // throw "error in RPFP::GetLabelsRec"; goto done; } else if(k == Not) { @@ -1062,7 +1811,8 @@ namespace Duality { } } /* Unreachable! */ - throw "error in RPFP::ImplicantRed"; + // TODO: need to indicate this failure to caller + // std::cerr << "error in RPFP::ImplicantRed"; goto done; } else if(k == Not) { @@ -1081,6 +1831,31 @@ namespace Duality { done[truth].insert(f); } + void RPFP::ImplicantFullRed(hash_map &memo, const Term &f, std::vector &lits, + hash_set &done, hash_set &dont_cares){ + if(done.find(f) != done.end()) + return; /* already processed */ + if(f.is_app()){ + int nargs = f.num_args(); + decl_kind k = f.decl().get_decl_kind(); + if(k == Implies || k == Iff || k == And || k == Or || k == Not){ + for(int i = 0; i < nargs; i++) + ImplicantFullRed(memo,f.arg(i),lits,done,dont_cares); + goto done; + } + } + { + if(dont_cares.find(f) == dont_cares.end()){ + int b = SubtermTruth(memo,f); + if(b != 0 && b != 1) goto done; + expr bv = (b==1) ? f : !f; + lits.push_back(bv); + } + } + done: + done.insert(f); + } + RPFP::Term RPFP::ResolveIte(hash_map &memo, const Term &t, std::vector &lits, hash_set *done, hash_set &dont_cares){ if(resolve_ite_memo.find(t) != resolve_ite_memo.end()) @@ -1118,6 +1893,57 @@ namespace Duality { return res; } + RPFP::Term RPFP::ElimIteRec(hash_map &memo, const Term &t, std::vector &cnsts){ + std::pair foo(t,expr(ctx)); + std::pair::iterator, bool> bar = memo.insert(foo); + Term &res = bar.first->second; + if(bar.second){ + if(t.is_app()){ + int nargs = t.num_args(); + std::vector args; + if(t.decl().get_decl_kind() == Equal){ + expr lhs = t.arg(0); + expr rhs = t.arg(1); + if(rhs.decl().get_decl_kind() == Ite){ + expr rhs_args[3]; + lhs = ElimIteRec(memo,lhs,cnsts); + for(int i = 0; i < 3; i++) + rhs_args[i] = ElimIteRec(memo,rhs.arg(i),cnsts); + res = (rhs_args[0] && (lhs == rhs_args[1])) || ((!rhs_args[0]) && (lhs == rhs_args[2])); + goto done; + } + } + if(t.decl().get_decl_kind() == Ite){ + func_decl sym = ctx.fresh_func_decl("@ite", t.get_sort()); + res = sym(); + cnsts.push_back(ElimIteRec(memo,ctx.make(Equal,res,t),cnsts)); + } + else { + for(int i = 0; i < nargs; i++) + args.push_back(ElimIteRec(memo,t.arg(i),cnsts)); + res = t.decl()(args.size(),&args[0]); + } + } + else if(t.is_quantifier()) + res = clone_quantifier(t,ElimIteRec(memo,t.body(),cnsts)); + else + res = t; + } + done: + return res; + } + + RPFP::Term RPFP::ElimIte(const Term &t){ + hash_map memo; + std::vector cnsts; + expr res = ElimIteRec(memo,t,cnsts); + if(!cnsts.empty()){ + cnsts.push_back(res); + res = ctx.make(And,cnsts); + } + return res; + } + void RPFP::Implicant(hash_map &memo, const Term &f, std::vector &lits, hash_set &dont_cares){ hash_set done[2]; ImplicantRed(memo,f,lits,done,true, dont_cares); @@ -1143,6 +1969,16 @@ namespace Duality { return conjoin(lits); } + RPFP::Term RPFP::UnderapproxFullFormula(const Term &f, hash_set &dont_cares){ + /* first compute truth values of subterms */ + hash_map memo; + hash_set done; + std::vector lits; + ImplicantFullRed(memo,f,lits,done,dont_cares); + /* return conjunction of literals */ + return conjoin(lits); + } + struct VariableProjector : Z3User { struct elim_cand { @@ -1565,10 +2401,14 @@ namespace Duality { for(int i = 0; i < num_args; i++) CollectConjuncts(f.arg(i),lits,false); } - else if(pos) - lits.push_back(f); - else - lits.push_back(!f); + else if(pos){ + if(!eq(f,ctx.bool_val(true))) + lits.push_back(f); + } + else { + if(!eq(f,ctx.bool_val(false))) + lits.push_back(!f); + } } struct TermLt { @@ -1669,6 +2509,121 @@ namespace Duality { return eu; } + void RPFP::FixCurrentState(Edge *edge){ + hash_set dont_cares; + resolve_ite_memo.clear(); + timer_start("UnderapproxFormula"); + Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual; + Term eu = UnderapproxFormula(dual,dont_cares); + timer_stop("UnderapproxFormula"); + ConstrainEdgeLocalized(edge,eu); + } + + void RPFP::FixCurrentStateFull(Edge *edge, const expr &extra){ + hash_set dont_cares; + resolve_ite_memo.clear(); + timer_start("UnderapproxFormula"); + Term dual = edge->dual.null() ? ctx.bool_val(true) : edge->dual; + for(unsigned i = 0; i < edge->constraints.size(); i++) + dual = dual && edge->constraints[i]; + // dual = dual && extra; + Term eu = UnderapproxFullFormula(dual,dont_cares); + timer_stop("UnderapproxFormula"); + ConstrainEdgeLocalized(edge,eu); + } + + + + + void RPFP::GetGroundLitsUnderQuants(hash_set *memo, const Term &f, std::vector &res, int under){ + if(memo[under].find(f) != memo[under].end()) + return; + memo[under].insert(f); + if(f.is_app()){ + if(!under && !f.has_quantifiers()) + return; + decl_kind k = f.decl().get_decl_kind(); + if(k == And || k == Or || k == Implies || k == Iff){ + int num_args = f.num_args(); + for(int i = 0; i < num_args; i++) + GetGroundLitsUnderQuants(memo,f.arg(i),res,under); + return; + } + } + else if (f.is_quantifier()){ +#if 0 + // treat closed quantified formula as a literal 'cause we hate nested quantifiers + if(under && IsClosedFormula(f)) + res.push_back(f); + else +#endif + GetGroundLitsUnderQuants(memo,f.body(),res,1); + return; + } + if(under && f.is_ground()) + res.push_back(f); + } + + RPFP::Term RPFP::StrengthenFormulaByCaseSplitting(const Term &f, std::vector &case_lits){ + hash_set memo[2]; + std::vector lits; + GetGroundLitsUnderQuants(memo, f, lits, 0); + hash_set lits_hash; + for(unsigned i = 0; i < lits.size(); i++) + lits_hash.insert(lits[i]); + hash_map subst; + hash_map stt_memo; + std::vector conjuncts; + for(unsigned i = 0; i < lits.size(); i++){ + const expr &lit = lits[i]; + if(lits_hash.find(NegateLit(lit)) == lits_hash.end()){ + case_lits.push_back(lit); + bool tval = false; + expr atom = lit; + if(lit.is_app() && lit.decl().get_decl_kind() == Not){ + tval = true; + atom = lit.arg(0); + } + expr etval = ctx.bool_val(tval); + if(atom.is_quantifier()) + subst[atom] = etval; // this is a bit desperate, since we can't eval quants + else { + int b = SubtermTruth(stt_memo,atom); + if(b == (tval ? 1 : 0)) + subst[atom] = etval; + else { + if(b == 0 || b == 1){ + etval = ctx.bool_val(b ? true : false); + subst[atom] = etval; + conjuncts.push_back(b ? atom : !atom); + } + } + } + } + } + expr g = f; + if(!subst.empty()){ + g = SubstRec(subst,f); + if(conjuncts.size()) + g = g && ctx.make(And,conjuncts); + g = g.simplify(); + } +#if 1 + expr g_old = g; + g = RemoveRedundancy(g); + bool changed = !eq(g,g_old); + g = g.simplify(); + if(changed) { // a second pass can get some more simplification + g = RemoveRedundancy(g); + g = g.simplify(); + } +#else + g = RemoveRedundancy(g); + g = g.simplify(); +#endif + g = AdjustQuantifiers(g); + return g; + } RPFP::Term RPFP::ModelValueAsConstraint(const Term &t){ if(t.is_array()){ @@ -1712,20 +2667,375 @@ namespace Duality { res = CreateRelation(p->Annotation.IndParams,funder); } +#if 0 + void RPFP::GreedyReduce(solver &s, std::vector &conjuncts){ + // verify + s.push(); + expr conj = ctx.make(And,conjuncts); + s.add(conj); + check_result res = s.check(); + if(res != unsat) + throw "should be unsat"; + s.pop(1); + + for(unsigned i = 0; i < conjuncts.size(); ){ + std::swap(conjuncts[i],conjuncts.back()); + expr save = conjuncts.back(); + conjuncts.pop_back(); + s.push(); + expr conj = ctx.make(And,conjuncts); + s.add(conj); + check_result res = s.check(); + s.pop(1); + if(res != unsat){ + conjuncts.push_back(save); + std::swap(conjuncts[i],conjuncts.back()); + i++; + } + } + } +#endif + + void RPFP::GreedyReduce(solver &s, std::vector &conjuncts){ + std::vector lits(conjuncts.size()); + for(unsigned i = 0; i < lits.size(); i++){ + func_decl pred = ctx.fresh_func_decl("@alit", ctx.bool_sort()); + lits[i] = pred(); + s.add(ctx.make(Implies,lits[i],conjuncts[i])); + } + + // verify + check_result res = s.check(lits.size(),&lits[0]); + if(res != unsat){ + // add the axioms in the off chance they are useful + const std::vector &theory = ls->get_axioms(); + for(unsigned i = 0; i < theory.size(); i++) + s.add(theory[i]); + for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something! + if(s.check(lits.size(),&lits[0]) == unsat) + goto is_unsat; + throw "should be unsat"; + } + is_unsat: + for(unsigned i = 0; i < conjuncts.size(); ){ + std::swap(conjuncts[i],conjuncts.back()); + std::swap(lits[i],lits.back()); + check_result res = s.check(lits.size()-1,&lits[0]); + if(res != unsat){ + std::swap(conjuncts[i],conjuncts.back()); + std::swap(lits[i],lits.back()); + i++; + } + else { + conjuncts.pop_back(); + lits.pop_back(); + } + } + } + + void RPFP_caching::FilterCore(std::vector &core, std::vector &full_core){ + hash_set core_set; + std::copy(full_core.begin(),full_core.end(),std::inserter(core_set,core_set.begin())); + std::vector new_core; + for(unsigned i = 0; i < core.size(); i++) + if(core_set.find(core[i]) != core_set.end()) + new_core.push_back(core[i]); + core.swap(new_core); + } + + void RPFP_caching::GreedyReduceCache(std::vector &assumps, std::vector &core){ + std::vector lits = assumps, full_core; + std::copy(core.begin(),core.end(),std::inserter(lits,lits.end())); + + // verify + check_result res = CheckCore(lits,full_core); + if(res != unsat){ + // add the axioms in the off chance they are useful + const std::vector &theory = ls->get_axioms(); + for(unsigned i = 0; i < theory.size(); i++) + GetAssumptionLits(theory[i],assumps); + lits = assumps; + std::copy(core.begin(),core.end(),std::inserter(lits,lits.end())); + + for(int k = 0; k < 100; k++) // keep trying, maybe MBQI will do something! + if((res = CheckCore(lits,full_core)) == unsat) + goto is_unsat; + throw "should be unsat"; + } + is_unsat: + FilterCore(core,full_core); + + std::vector dummy; + if(CheckCore(full_core,dummy) != unsat) + throw "should be unsat"; + + for(unsigned i = 0; i < core.size(); ){ + expr temp = core[i]; + std::swap(core[i],core.back()); + core.pop_back(); + lits.resize(assumps.size()); + std::copy(core.begin(),core.end(),std::inserter(lits,lits.end())); + res = CheckCore(lits,full_core); + if(res != unsat){ + core.push_back(temp); + std::swap(core[i],core.back()); + i++; + } + } + } + + expr RPFP::NegateLit(const expr &f){ + if(f.is_app() && f.decl().get_decl_kind() == Not) + return f.arg(0); + else + return !f; + } + + void RPFP::NegateLits(std::vector &lits){ + for(unsigned i = 0; i < lits.size(); i++){ + expr &f = lits[i]; + if(f.is_app() && f.decl().get_decl_kind() == Not) + f = f.arg(0); + else + f = !f; + } + } + + expr RPFP::SimplifyOr(std::vector &lits){ + if(lits.size() == 0) + return ctx.bool_val(false); + if(lits.size() == 1) + return lits[0]; + return ctx.make(Or,lits); + } + + expr RPFP::SimplifyAnd(std::vector &lits){ + if(lits.size() == 0) + return ctx.bool_val(true); + if(lits.size() == 1) + return lits[0]; + return ctx.make(And,lits); + } + + // set up edge constraint in aux solver + void RPFP::AddEdgeToSolver(Edge *edge){ + if(!edge->dual.null()) + aux_solver.add(edge->dual); + for(unsigned i = 0; i < edge->constraints.size(); i++){ + expr tl = edge->constraints[i]; + aux_solver.add(tl); + } + } + + void RPFP::InterpolateByCases(Node *root, Node *node){ + bool axioms_added = false; + aux_solver.push(); + AddEdgeToSolver(node->Outgoing); + node->Annotation.SetEmpty(); + hash_set *core = new hash_set; + core->insert(node->Outgoing->dual); + while(1){ + aux_solver.push(); + expr annot = !GetAnnotation(node); + aux_solver.add(annot); + if(aux_solver.check() == unsat){ + aux_solver.pop(1); + break; + } + dualModel = aux_solver.get_model(); + aux_solver.pop(1); + Push(); + FixCurrentStateFull(node->Outgoing,annot); + ConstrainEdgeLocalized(node->Outgoing,!GetAnnotation(node)); + check_result foo = Check(root); + if(foo != unsat) + throw "should be unsat"; + AddToProofCore(*core); + Transformer old_annot = node->Annotation; + SolveSingleNode(root,node); + + { + expr itp = GetAnnotation(node); + dualModel = aux_solver.get_model(); + std::vector case_lits; + itp = StrengthenFormulaByCaseSplitting(itp, case_lits); + SetAnnotation(node,itp); + node->Annotation.Formula = node->Annotation.Formula.simplify(); + } + + if(node->Annotation.IsEmpty()){ + if(!axioms_added){ + // add the axioms in the off chance they are useful + const std::vector &theory = ls->get_axioms(); + for(unsigned i = 0; i < theory.size(); i++) + aux_solver.add(theory[i]); + axioms_added = true; + } + else { + std::cout << "bad in InterpolateByCase -- core:\n"; + std::vector assumps; + slvr().get_proof().get_assumptions(assumps); + for(unsigned i = 0; i < assumps.size(); i++) + assumps[i].show(); + throw "ack!"; + } + } + Pop(1); + node->Annotation.UnionWith(old_annot); + } + if(proof_core) + delete proof_core; // shouldn't happen + proof_core = core; + aux_solver.pop(1); + } + + void RPFP::Generalize(Node *root, Node *node){ + timer_start("Generalize"); + aux_solver.push(); + AddEdgeToSolver(node->Outgoing); + expr fmla = GetAnnotation(node); + std::vector conjuncts; + CollectConjuncts(fmla,conjuncts,false); + GreedyReduce(aux_solver,conjuncts); // try to remove conjuncts one at a tme + aux_solver.pop(1); + NegateLits(conjuncts); + SetAnnotation(node,SimplifyOr(conjuncts)); + timer_stop("Generalize"); + } + + RPFP_caching::edge_solver &RPFP_caching::SolverForEdge(Edge *edge, bool models, bool axioms){ + edge_solver &es = edge_solvers[edge]; + uptr &p = es.slvr; + if(!p.get()){ + scoped_no_proof no_proofs_please(ctx.m()); // no proofs + p.set(new solver(ctx,true,models)); // no models + if(axioms){ + RPFP::LogicSolver *ls = edge->owner->ls; + const std::vector &axs = ls->get_axioms(); + for(unsigned i = 0; i < axs.size(); i++) + p.get()->add(axs[i]); + } + } + return es; + } + + + // caching version of above + void RPFP_caching::GeneralizeCache(Edge *edge){ + timer_start("Generalize"); + scoped_solver_for_edge ssfe(this,edge); + Node *node = edge->Parent; + std::vector assumps, core, conjuncts; + AssertEdgeCache(edge,assumps); + for(unsigned i = 0; i < edge->Children.size(); i++){ + expr ass = GetAnnotation(edge->Children[i]); + std::vector clauses; + if(!ass.is_true()){ + CollectConjuncts(ass.arg(1),clauses); + for(unsigned j = 0; j < clauses.size(); j++) + GetAssumptionLits(ass.arg(0) || clauses[j],assumps); + } + } + expr fmla = GetAnnotation(node); + std::vector lits; + if(fmla.is_true()){ + timer_stop("Generalize"); + return; + } + assumps.push_back(fmla.arg(0).arg(0)); + CollectConjuncts(!fmla.arg(1),lits); +#if 0 + for(unsigned i = 0; i < lits.size(); i++){ + const expr &lit = lits[i]; + if(lit.is_app() && lit.decl().get_decl_kind() == Equal){ + lits[i] = ctx.make(Leq,lit.arg(0),lit.arg(1)); + lits.push_back(ctx.make(Leq,lit.arg(1),lit.arg(0))); + } + } +#endif + hash_map lit_map; + for(unsigned i = 0; i < lits.size(); i++) + GetAssumptionLits(lits[i],core,&lit_map); + GreedyReduceCache(assumps,core); + for(unsigned i = 0; i < core.size(); i++) + conjuncts.push_back(lit_map[core[i]]); + NegateLits(conjuncts); + SetAnnotation(node,SimplifyOr(conjuncts)); + timer_stop("Generalize"); + } + + // caching version of above + bool RPFP_caching::PropagateCache(Edge *edge){ + timer_start("PropagateCache"); + scoped_solver_for_edge ssfe(this,edge); + bool some = false; + { + std::vector candidates, skip; + Node *node = edge->Parent; + CollectConjuncts(node->Annotation.Formula,skip); + for(unsigned i = 0; i < edge->Children.size(); i++){ + Node *child = edge->Children[i]; + if(child->map == node->map){ + CollectConjuncts(child->Annotation.Formula,candidates); + break; + } + } + if(candidates.empty()) goto done; + hash_set skip_set; + std::copy(skip.begin(),skip.end(),std::inserter(skip_set,skip_set.begin())); + std::vector new_candidates; + for(unsigned i = 0; i < candidates.size(); i++) + if(skip_set.find(candidates[i]) == skip_set.end()) + new_candidates.push_back(candidates[i]); + candidates.swap(new_candidates); + if(candidates.empty()) goto done; + std::vector assumps, core, conjuncts; + AssertEdgeCache(edge,assumps); + for(unsigned i = 0; i < edge->Children.size(); i++){ + expr ass = GetAnnotation(edge->Children[i]); + if(eq(ass,ctx.bool_val(true))) + continue; + std::vector clauses; + CollectConjuncts(ass.arg(1),clauses); + for(unsigned j = 0; j < clauses.size(); j++) + GetAssumptionLits(ass.arg(0) || clauses[j],assumps); + } + for(unsigned i = 0; i < candidates.size(); i++){ + unsigned old_size = assumps.size(); + node->Annotation.Formula = candidates[i]; + expr fmla = GetAnnotation(node); + assumps.push_back(fmla.arg(0).arg(0)); + GetAssumptionLits(!fmla.arg(1),assumps); + std::vector full_core; + check_result res = CheckCore(assumps,full_core); + if(res == unsat) + conjuncts.push_back(candidates[i]); + assumps.resize(old_size); + } + if(conjuncts.empty()) + goto done; + SetAnnotation(node,SimplifyAnd(conjuncts)); + some = true; + } + done: + timer_stop("PropagateCache"); + return some; + } + /** Push a scope. Assertions made after Push can be undone by Pop. */ void RPFP::Push() { stack.push_back(stack_entry()); - slvr.push(); + slvr_push(); } /** Pop a scope (see Push). Note, you cannot pop axioms. */ void RPFP::Pop(int num_scopes) { - slvr.pop(num_scopes); + slvr_pop(num_scopes); for (int i = 0; i < num_scopes; i++) { stack_entry &back = stack.back(); @@ -1733,10 +3043,26 @@ namespace Duality { (*it)->dual = expr(ctx,NULL); for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) (*it)->dual = expr(ctx,NULL); + for(std::list >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) + (*it).first->constraints.pop_back(); stack.pop_back(); } } + /** Erase the proof by performing a Pop, Push and re-assertion of + all the popped constraints */ + + void RPFP::PopPush(){ + slvr_pop(1); + slvr_push(); + stack_entry &back = stack.back(); + for(std::list::iterator it = back.edges.begin(), en = back.edges.end(); it != en; ++it) + slvr_add((*it)->dual); + for(std::list::iterator it = back.nodes.begin(), en = back.nodes.end(); it != en; ++it) + slvr_add((*it)->dual); + for(std::list >::iterator it = back.constraints.begin(), en = back.constraints.end(); it != en; ++it) + slvr_add((*it).second); + } @@ -1753,6 +3079,17 @@ namespace Duality { return ctx.function(name.c_str(), nargs, &sorts[0], t.get_sort()); } + Z3User::FuncDecl Z3User::RenumberPred(const FuncDecl &f, int n) + { + std::string name = f.name().str(); + name = name.substr(0,name.rfind('_')) + "_" + string_of_int(n); + int arity = f.arity(); + std::vector domain; + for(int i = 0; i < arity; i++) + domain.push_back(f.domain(i)); + return ctx.function(name.c_str(), arity, &domain[0], f.range()); + } + // Scan the clause body for occurrences of the predicate unknowns RPFP::Term RPFP::ScanBody(hash_map &memo, @@ -1799,7 +3136,7 @@ namespace Duality { bool Z3User::is_variable(const Term &t){ if(!t.is_app()) - return false; + return t.is_var(); return t.decl().get_decl_kind() == Uninterpreted && t.num_args() == 0; } @@ -1880,6 +3217,37 @@ namespace Duality { return SubstBoundRec(memo, subst, 0, t); } + int Z3User::MaxIndex(hash_map &memo, const Term &t) + { + std::pair foo(t,-1); + std::pair::iterator, bool> bar = memo.insert(foo); + int &res = bar.first->second; + if(!bar.second) return res; + if (t.is_app()){ + func_decl f = t.decl(); + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++){ + int m = MaxIndex(memo, t.arg(i)); + if(m > res) + res = m; + } + } + else if (t.is_quantifier()){ + int bound = t.get_quantifier_num_bound(); + res = MaxIndex(memo,t.body()) - bound; + } + else if (t.is_var()) { + res = t.get_index_value(); + } + return res; + } + + bool Z3User::IsClosedFormula(const Term &t){ + hash_map memo; + return MaxIndex(memo,t) < 0; + } + + /** Convert a collection of clauses to Nodes and Edges in the RPFP. Predicate unknowns are uninterpreted predicates not @@ -1917,6 +3285,8 @@ namespace Duality { arg.decl().get_decl_kind() == Uninterpreted); } +#define USE_QE_LITE + void RPFP::FromClauses(const std::vector &unskolemized_clauses){ hash_map pmap; func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort()); @@ -1924,6 +3294,7 @@ namespace Duality { std::vector clauses(unskolemized_clauses); // first, skolemize the clauses +#ifndef USE_QE_LITE for(unsigned i = 0; i < clauses.size(); i++){ expr &t = clauses[i]; if (t.is_quantifier() && t.is_quantifier_forall()) { @@ -1940,11 +3311,32 @@ namespace Duality { t = SubstBound(subst,t.body()); } } +#else + std::vector > substs(clauses.size()); +#endif // create the nodes from the heads of the clauses for(unsigned i = 0; i < clauses.size(); i++){ Term &clause = clauses[i]; + +#ifdef USE_QE_LITE + Term &t = clause; + if (t.is_quantifier() && t.is_quantifier_forall()) { + int bound = t.get_quantifier_num_bound(); + std::vector sorts; + std::vector names; + for(int j = 0; j < bound; j++){ + sort the_sort = t.get_quantifier_bound_sort(j); + symbol name = t.get_quantifier_bound_name(j); + expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort)); + substs[i][bound-1-j] = skolem; + } + clause = t.body(); + } + +#endif + if(clause.is_app() && clause.decl().get_decl_kind() == Uninterpreted) clause = implies(ctx.bool_val(true),clause); if(!canonical_clause(clause)) @@ -1976,6 +3368,13 @@ namespace Duality { seen.insert(arg); Indparams.push_back(arg); } +#ifdef USE_QE_LITE + { + hash_map > sb_memo; + for(unsigned j = 0; j < Indparams.size(); j++) + Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]); + } +#endif Node *node = CreateNode(R(Indparams.size(),&Indparams[0])); //nodes.push_back(node); pmap[R] = node; @@ -1984,6 +3383,8 @@ namespace Duality { } } + bool some_labels = false; + // create the edges for(unsigned i = 0; i < clauses.size(); i++){ @@ -2019,17 +3420,352 @@ namespace Duality { Term labeled = body; std::vector lbls; // TODO: throw this away for now body = RemoveLabels(body,lbls); + if(!eq(labeled,body)) + some_labels = true; // remember if there are labels, as we then can't do qe_lite + // body = IneqToEq(body); // UFO converts x=y to (x<=y & x >= y). Undo this. body = body.simplify(); +#ifdef USE_QE_LITE + std::set idxs; + if(!some_labels){ // can't do qe_lite if we have to reconstruct labels + for(unsigned j = 0; j < Indparams.size(); j++) + if(Indparams[j].is_var()) + idxs.insert(Indparams[j].get_index_value()); + body = body.qe_lite(idxs,false); + } + hash_map > sb_memo; + body = SubstBoundRec(sb_memo,substs[i],0,body); + if(some_labels) + labeled = SubstBoundRec(sb_memo,substs[i],0,labeled); + for(unsigned j = 0; j < Indparams.size(); j++) + Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]); +#endif + // Create the edge Transformer T = CreateTransformer(Relparams,Indparams,body); Edge *edge = CreateEdge(Parent,T,Children); edge->labeled = labeled;; // remember for label extraction // edges.push_back(edge); } + + // undo hoisting of expressions out of loops + RemoveDeadNodes(); + Unhoist(); + // FuseEdges(); } + // The following mess is used to undo hoisting of expressions outside loops by compilers + + expr RPFP::UnhoistPullRec(hash_map & memo, const expr &w, hash_map & init_defs, hash_map & const_params, hash_map &const_params_inv, std::vector &new_params){ + if(memo.find(w) != memo.end()) + return memo[w]; + expr res; + if(init_defs.find(w) != init_defs.end()){ + expr d = init_defs[w]; + std::vector vars; + hash_set get_vars_memo; + GetVarsRec(get_vars_memo,d,vars); + hash_map map; + for(unsigned j = 0; j < vars.size(); j++){ + expr x = vars[j]; + map[x] = UnhoistPullRec(memo,x,init_defs,const_params,const_params_inv,new_params); + } + expr defn = SubstRec(map,d); + res = defn; + } + else if(const_params_inv.find(w) == const_params_inv.end()){ + std::string old_name = w.decl().name().str(); + func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), w.get_sort()); + expr y = fresh(); + const_params[y] = w; + const_params_inv[w] = y; + new_params.push_back(y); + res = y; + } + else + res = const_params_inv[w]; + memo[w] = res; + return res; + } + + void RPFP::AddParamsToTransformer(Transformer &trans, const std::vector ¶ms){ + std::copy(params.begin(),params.end(),std::inserter(trans.IndParams,trans.IndParams.end())); + } + + expr RPFP::AddParamsToApp(const expr &app, const func_decl &new_decl, const std::vector ¶ms){ + int n = app.num_args(); + std::vector args(n); + for (int i = 0; i < n; i++) + args[i] = app.arg(i); + std::copy(params.begin(),params.end(),std::inserter(args,args.end())); + return new_decl(args); + } + + expr RPFP::GetRelRec(hash_set &memo, const expr &t, const func_decl &rel){ + if(memo.find(t) != memo.end()) + return expr(); + memo.insert(t); + if (t.is_app()) + { + func_decl f = t.decl(); + if(f == rel) + return t; + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++){ + expr res = GetRelRec(memo,t.arg(i),rel); + if(!res.null()) + return res; + } + } + else if (t.is_quantifier()) + return GetRelRec(memo,t.body(),rel); + return expr(); + } + + expr RPFP::GetRel(Edge *edge, int child_idx){ + func_decl &rel = edge->F.RelParams[child_idx]; + hash_set memo; + return GetRelRec(memo,edge->F.Formula,rel); + } + + void RPFP::GetDefsRec(const expr &cnst, hash_map &defs){ + if(cnst.is_app()){ + switch(cnst.decl().get_decl_kind()){ + case And: { + int n = cnst.num_args(); + for(int i = 0; i < n; i++) + GetDefsRec(cnst.arg(i),defs); + break; + } + case Equal: { + expr lhs = cnst.arg(0); + expr rhs = cnst.arg(1); + if(IsVar(lhs)) + defs[lhs] = rhs; + break; + } + default: + break; + } + } + } + + void RPFP::GetDefs(const expr &cnst, hash_map &defs){ + // GetDefsRec(IneqToEq(cnst),defs); + GetDefsRec(cnst,defs); + } + + bool RPFP::IsVar(const expr &t){ + return t.is_app() && t.num_args() == 0 && t.decl().get_decl_kind() == Uninterpreted; + } + + void RPFP::GetVarsRec(hash_set &memo, const expr &t, std::vector &vars){ + if(memo.find(t) != memo.end()) + return; + memo.insert(t); + if (t.is_app()) + { + if(IsVar(t)){ + vars.push_back(t); + return; + } + int nargs = t.num_args(); + for(int i = 0; i < nargs; i++){ + GetVarsRec(memo,t.arg(i),vars); + } + } + else if (t.is_quantifier()) + GetVarsRec(memo,t.body(),vars); + } + + void RPFP::AddParamsToNode(Node *node, const std::vector ¶ms){ + int arity = node->Annotation.IndParams.size(); + std::vector domain; + for(int i = 0; i < arity; i++) + domain.push_back(node->Annotation.IndParams[i].get_sort()); + for(unsigned i = 0; i < params.size(); i++) + domain.push_back(params[i].get_sort()); + std::string old_name = node->Name.name().str(); + func_decl fresh = ctx.fresh_func_decl(old_name.c_str(), domain, ctx.bool_sort()); + node->Name = fresh; + AddParamsToTransformer(node->Annotation,params); + AddParamsToTransformer(node->Bound,params); + AddParamsToTransformer(node->Underapprox,params); + } + + void RPFP::UnhoistLoop(Edge *loop_edge, Edge *init_edge){ + loop_edge->F.Formula = IneqToEq(loop_edge->F.Formula); + init_edge->F.Formula = IneqToEq(init_edge->F.Formula); + expr pre = GetRel(loop_edge,0); + if(pre.null()) + return; // this means the loop got simplified away + int nparams = loop_edge->F.IndParams.size(); + hash_map const_params, const_params_inv; + std::vector work_list; + // find the parameters that are constant in the loop + for(int i = 0; i < nparams; i++){ + if(eq(pre.arg(i),loop_edge->F.IndParams[i])){ + const_params[pre.arg(i)] = init_edge->F.IndParams[i]; + const_params_inv[init_edge->F.IndParams[i]] = pre.arg(i); + work_list.push_back(pre.arg(i)); + } + } + // get the definitions in the initialization + hash_map defs,memo,subst; + GetDefs(init_edge->F.Formula,defs); + // try to pull them inside the loop + std::vector new_params; + for(unsigned i = 0; i < work_list.size(); i++){ + expr v = work_list[i]; + expr w = const_params[v]; + expr def = UnhoistPullRec(memo,w,defs,const_params,const_params_inv,new_params); + if(!eq(def,v)) + subst[v] = def; + } + // do the substitutions + if(subst.empty()) + return; + subst[pre] = pre; // don't substitute inside the precondition itself + loop_edge->F.Formula = SubstRec(subst,loop_edge->F.Formula); + loop_edge->F.Formula = ElimIte(loop_edge->F.Formula); + init_edge->F.Formula = ElimIte(init_edge->F.Formula); + // add the new parameters + if(new_params.empty()) + return; + Node *parent = loop_edge->Parent; + AddParamsToNode(parent,new_params); + AddParamsToTransformer(loop_edge->F,new_params); + AddParamsToTransformer(init_edge->F,new_params); + std::vector &incoming = parent->Incoming; + for(unsigned i = 0; i < incoming.size(); i++){ + Edge *in_edge = incoming[i]; + std::vector &chs = in_edge->Children; + for(unsigned j = 0; j < chs.size(); j++) + if(chs[j] == parent){ + expr lit = GetRel(in_edge,j); + expr new_lit = AddParamsToApp(lit,parent->Name,new_params); + func_decl fd = SuffixFuncDecl(new_lit,j); + int nargs = new_lit.num_args(); + std::vector args; + for(int k = 0; k < nargs; k++) + args.push_back(new_lit.arg(k)); + new_lit = fd(nargs,&args[0]); + in_edge->F.RelParams[j] = fd; + hash_map map; + map[lit] = new_lit; + in_edge->F.Formula = SubstRec(map,in_edge->F.Formula); + } + } + } + + void RPFP::Unhoist(){ + hash_map > outgoing; + for(unsigned i = 0; i < edges.size(); i++) + outgoing[edges[i]->Parent].push_back(edges[i]); + for(unsigned i = 0; i < nodes.size(); i++){ + Node *node = nodes[i]; + std::vector &outs = outgoing[node]; + // if we're not a simple loop with one entry, give up + if(outs.size() == 2){ + for(int j = 0; j < 2; j++){ + Edge *loop_edge = outs[j]; + Edge *init_edge = outs[1-j]; + if(loop_edge->Children.size() == 1 && loop_edge->Children[0] == loop_edge->Parent){ + UnhoistLoop(loop_edge,init_edge); + break; + } + } + } + } + } + + void RPFP::FuseEdges(){ + hash_map > outgoing; + for(unsigned i = 0; i < edges.size(); i++){ + outgoing[edges[i]->Parent].push_back(edges[i]); + } + hash_set edges_to_delete; + for(unsigned i = 0; i < nodes.size(); i++){ + Node *node = nodes[i]; + std::vector &outs = outgoing[node]; + if(outs.size() > 1 && outs.size() <= 16){ + std::vector trs(outs.size()); + for(unsigned j = 0; j < outs.size(); j++) + trs[j] = &outs[j]->F; + Transformer tr = Fuse(trs); + std::vector chs; + for(unsigned j = 0; j < outs.size(); j++) + for(unsigned k = 0; k < outs[j]->Children.size(); k++) + chs.push_back(outs[j]->Children[k]); + CreateEdge(node,tr,chs); + for(unsigned j = 0; j < outs.size(); j++) + edges_to_delete.insert(outs[j]); + } + } + std::vector new_edges; + hash_set all_nodes; + for(unsigned j = 0; j < edges.size(); j++){ + if(edges_to_delete.find(edges[j]) == edges_to_delete.end()){ +#if 0 + if(all_nodes.find(edges[j]->Parent) != all_nodes.end()) + throw "help!"; + all_nodes.insert(edges[j]->Parent); +#endif + new_edges.push_back(edges[j]); + } + else + delete edges[j]; + } + edges.swap(new_edges); + } + + void RPFP::MarkLiveNodes(hash_map > &outgoing, hash_set &live_nodes, Node *node){ + if(live_nodes.find(node) != live_nodes.end()) + return; + live_nodes.insert(node); + std::vector &outs = outgoing[node]; + for(unsigned i = 0; i < outs.size(); i++) + for(unsigned j = 0; j < outs[i]->Children.size(); j++) + MarkLiveNodes(outgoing, live_nodes,outs[i]->Children[j]); + } + + void RPFP::RemoveDeadNodes(){ + hash_map > outgoing; + for(unsigned i = 0; i < edges.size(); i++) + outgoing[edges[i]->Parent].push_back(edges[i]); + hash_set live_nodes; + for(unsigned i = 0; i < nodes.size(); i++) + if(!nodes[i]->Bound.IsFull()) + MarkLiveNodes(outgoing,live_nodes,nodes[i]); + std::vector new_edges; + for(unsigned j = 0; j < edges.size(); j++){ + if(live_nodes.find(edges[j]->Parent) != live_nodes.end()) + new_edges.push_back(edges[j]); + else { + Edge *edge = edges[j]; + for(unsigned int i = 0; i < edge->Children.size(); i++){ + std::vector &ic = edge->Children[i]->Incoming; + for(std::vector::iterator it = ic.begin(), en = ic.end(); it != en; ++it){ + if(*it == edge){ + ic.erase(it); + break; + } + } + } + delete edge; + } + } + edges.swap(new_edges); + std::vector new_nodes; + for(unsigned j = 0; j < nodes.size(); j++){ + if(live_nodes.find(nodes[j]) != live_nodes.end()) + new_nodes.push_back(nodes[j]); + else + delete nodes[j]; + } + nodes.swap(new_nodes); + } void RPFP::WriteSolution(std::ostream &s){ for(unsigned i = 0; i < nodes.size(); i++){ @@ -2170,7 +3906,31 @@ namespace Duality { } + bool RPFP::proof_core_contains(const expr &e){ + return proof_core->find(e) != proof_core->end(); + } + + bool RPFP_caching::proof_core_contains(const expr &e){ + std::vector foo; + GetAssumptionLits(e,foo); + for(unsigned i = 0; i < foo.size(); i++) + if(proof_core->find(foo[i]) != proof_core->end()) + return true; + return false; + } + + bool RPFP::EdgeUsedInProof(Edge *edge){ + ComputeProofCore(); + if(!edge->dual.null() && proof_core_contains(edge->dual)) + return true; + for(unsigned i = 0; i < edge->constraints.size(); i++) + if(proof_core_contains(edge->constraints[i])) + return true; + return false; + } + RPFP::~RPFP(){ + ClearProofCore(); for(unsigned i = 0; i < nodes.size(); i++) delete nodes[i]; for(unsigned i = 0; i < edges.size(); i++) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp old mode 100644 new mode 100755 index 0043998d2..1c2f2c927 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -19,6 +19,12 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#endif + #include "duality.h" #include "duality_profiling.h" @@ -26,6 +32,7 @@ Revision History: #include #include #include +#include // TODO: make these official options or get rid of them @@ -37,14 +44,23 @@ Revision History: #define MINIMIZE_CANDIDATES // #define MINIMIZE_CANDIDATES_HARDER #define BOUNDED -#define CHECK_CANDS_FROM_IND_SET +// #define CHECK_CANDS_FROM_IND_SET #define UNDERAPPROX_NODES #define NEW_EXPAND #define EARLY_EXPAND // #define TOP_DOWN // #define EFFORT_BOUNDED_STRAT #define SKIP_UNDERAPPROX_NODES +// #define KEEP_EXPANSIONS +// #define USE_CACHING_RPFP +// #define PROPAGATE_BEFORE_CHECK +#define USE_RPFP_CLONE +#define USE_NEW_GEN_CANDS + +//#define NO_PROPAGATE +//#define NO_GENERALIZE +//#define NO_DECISIONS namespace Duality { @@ -101,7 +117,7 @@ namespace Duality { public: Duality(RPFP *_rpfp) : ctx(_rpfp->ctx), - slvr(_rpfp->slvr), + slvr(_rpfp->slvr()), nodes(_rpfp->nodes), edges(_rpfp->edges) { @@ -115,8 +131,36 @@ namespace Duality { Report = false; StratifiedInlining = false; RecursionBound = -1; + { + scoped_no_proof no_proofs_please(ctx.m()); +#ifdef USE_RPFP_CLONE + clone_rpfp = new RPFP_caching(rpfp->ls); + clone_rpfp->Clone(rpfp); +#endif +#ifdef USE_NEW_GEN_CANDS + gen_cands_rpfp = new RPFP_caching(rpfp->ls); + gen_cands_rpfp->Clone(rpfp); +#endif + } } + ~Duality(){ +#ifdef USE_RPFP_CLONE + delete clone_rpfp; +#endif +#ifdef USE_NEW_GEN_CANDS + delete gen_cands_rpfp; +#endif + } + +#ifdef USE_RPFP_CLONE + RPFP_caching *clone_rpfp; +#endif +#ifdef USE_NEW_GEN_CANDS + RPFP_caching *gen_cands_rpfp; +#endif + + typedef RPFP::Node Node; typedef RPFP::Edge Edge; @@ -184,7 +228,7 @@ namespace Duality { best.insert(*it); } #else - virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority=false){ + virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority=false, bool best_only=false){ if(high_priority) return; int best_score = INT_MAX; int worst_score = 0; @@ -194,13 +238,13 @@ namespace Duality { best_score = std::min(best_score,score); worst_score = std::max(worst_score,score); } - int cutoff = best_score + (worst_score-best_score)/2; + int cutoff = best_only ? best_score : (best_score + (worst_score-best_score)/2); for(std::set::iterator it = choices.begin(), en = choices.end(); it != en; ++it) if(scores[(*it)->map].updates <= cutoff) best.insert(*it); } #endif - + /** Called when done expanding a tree */ virtual void Done() {} }; @@ -804,8 +848,10 @@ namespace Duality { Node *child = chs[i]; if(TopoSort[child] < TopoSort[node->map]){ Node *leaf = LeafMap[child]; - if(!indset->Contains(leaf)) + if(!indset->Contains(leaf)){ + node->Outgoing->F.Formula = ctx.bool_val(false); // make this a proper leaf, else bogus cex return node->Outgoing; + } } } @@ -1085,7 +1131,8 @@ namespace Duality { void ExtractCandidateFromCex(Edge *edge, RPFP *checker, Node *root, Candidate &candidate){ candidate.edge = edge; for(unsigned j = 0; j < edge->Children.size(); j++){ - Edge *lb = root->Outgoing->Children[j]->Outgoing; + Node *node = root->Outgoing->Children[j]; + Edge *lb = node->Outgoing; std::vector &insts = insts_of_node[edge->Children[j]]; #ifndef MINIMIZE_CANDIDATES for(int k = insts.size()-1; k >= 0; k--) @@ -1095,8 +1142,8 @@ namespace Duality { { Node *inst = insts[k]; if(indset->Contains(inst)){ - if(checker->Empty(lb->Parent) || - eq(checker->Eval(lb,NodeMarker(inst)),ctx.bool_val(true))){ + if(checker->Empty(node) || + eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst)),ctx.bool_val(true))){ candidate.Children.push_back(inst); goto next_child; } @@ -1166,6 +1213,25 @@ namespace Duality { #endif + Node *CheckerForEdgeClone(Edge *edge, RPFP_caching *checker){ + Edge *gen_cands_edge = checker->GetEdgeClone(edge); + Node *root = gen_cands_edge->Parent; + root->Outgoing = gen_cands_edge; + GenNodeSolutionFromIndSet(edge->Parent, root->Bound); +#if 0 + if(root->Bound.IsFull()) + return = 0; +#endif + checker->AssertNode(root); + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *oc = edge->Children[j]; + Node *nc = gen_cands_edge->Children[j]; + GenNodeSolutionWithMarkers(oc,nc->Annotation,true); + } + checker->AssertEdge(gen_cands_edge,1,true); + return root; + } + /** If the current proposed solution is not inductive, use the induction failure to generate candidates for extension. */ void GenCandidatesFromInductionFailure(bool full_scan = false){ @@ -1175,6 +1241,7 @@ namespace Duality { Edge *edge = edges[i]; if(!full_scan && updated_nodes.find(edge->Parent) == updated_nodes.end()) continue; +#ifndef USE_NEW_GEN_CANDS slvr.push(); RPFP *checker = new RPFP(rpfp->ls); Node *root = CheckerForEdge(edge,checker); @@ -1186,6 +1253,18 @@ namespace Duality { } slvr.pop(1); delete checker; +#else + RPFP_caching::scoped_solver_for_edge ssfe(gen_cands_rpfp,edge,true /* models */, true /*axioms*/); + gen_cands_rpfp->Push(); + Node *root = CheckerForEdgeClone(edge,gen_cands_rpfp); + if(gen_cands_rpfp->Check(root) != unsat){ + Candidate candidate; + ExtractCandidateFromCex(edge,gen_cands_rpfp,root,candidate); + reporter->InductionFailure(edge,candidate.Children); + candidates.push_back(candidate); + } + gen_cands_rpfp->Pop(1); +#endif } updated_nodes.clear(); timer_stop("GenCandIndFail"); @@ -1270,18 +1349,24 @@ namespace Duality { } } + bool UpdateNodeToNode(Node *node, Node *top){ + if(!node->Annotation.SubsetEq(top->Annotation)){ + reporter->Update(node,top->Annotation); + indset->Update(node,top->Annotation); + updated_nodes.insert(node->map); + node->Annotation.IntersectWith(top->Annotation); + return true; + } + return false; + } + /** Update the unwinding solution, using an interpolant for the derivation tree. */ void UpdateWithInterpolant(Node *node, RPFP *tree, Node *top){ if(top->Outgoing) for(unsigned i = 0; i < top->Outgoing->Children.size(); i++) UpdateWithInterpolant(node->Outgoing->Children[i],tree,top->Outgoing->Children[i]); - if(!node->Annotation.SubsetEq(top->Annotation)){ - reporter->Update(node,top->Annotation); - indset->Update(node,top->Annotation); - updated_nodes.insert(node->map); - node->Annotation.IntersectWith(top->Annotation); - } + UpdateNodeToNode(node, top); heuristic->Update(node); } @@ -1303,9 +1388,13 @@ namespace Duality { node. */ bool SatisfyUpperBound(Node *node){ if(node->Bound.IsFull()) return true; +#ifdef PROPAGATE_BEFORE_CHECK + Propagate(); +#endif reporter->Bound(node); int start_decs = rpfp->CumulativeDecisions(); - DerivationTree dt(this,unwinding,reporter,heuristic,FullExpand); + DerivationTree *dtp = new DerivationTreeSlow(this,unwinding,reporter,heuristic,FullExpand); + DerivationTree &dt = *dtp; bool res = dt.Derive(unwinding,node,UseUnderapprox); int end_decs = rpfp->CumulativeDecisions(); // std::cout << "decisions: " << (end_decs - start_decs) << std::endl; @@ -1321,6 +1410,7 @@ namespace Duality { UpdateWithInterpolant(node,dt.tree,dt.top); delete dt.tree; } + delete dtp; return !res; } @@ -1404,13 +1494,77 @@ namespace Duality { } } + // Propagate conjuncts up the unwinding + void Propagate(){ + reporter->Message("beginning propagation"); + timer_start("Propagate"); + std::vector sorted_nodes = unwinding->nodes; + std::sort(sorted_nodes.begin(),sorted_nodes.end(),std::less()); // sorts by sequence number + hash_map > facts; + for(unsigned i = 0; i < sorted_nodes.size(); i++){ + Node *node = sorted_nodes[i]; + std::set &node_facts = facts[node->map]; + if(!(node->Outgoing && indset->Contains(node))) + continue; + std::vector conj_vec; + unwinding->CollectConjuncts(node->Annotation.Formula,conj_vec); + std::set conjs; + std::copy(conj_vec.begin(),conj_vec.end(),std::inserter(conjs,conjs.begin())); + if(!node_facts.empty()){ + RPFP *checker = new RPFP(rpfp->ls); + slvr.push(); + Node *root = checker->CloneNode(node); + Edge *edge = node->Outgoing; + // checker->AssertNode(root); + std::vector cs; + for(unsigned j = 0; j < edge->Children.size(); j++){ + Node *oc = edge->Children[j]; + Node *nc = checker->CloneNode(oc); + nc->Annotation = oc->Annotation; // is this needed? + cs.push_back(nc); + } + Edge *checker_edge = checker->CreateEdge(root,edge->F,cs); + checker->AssertEdge(checker_edge, 0, true, false); + std::vector propagated; + for(std::set ::iterator it = node_facts.begin(), en = node_facts.end(); it != en;){ + const expr &fact = *it; + if(conjs.find(fact) == conjs.end()){ + root->Bound.Formula = fact; + slvr.push(); + checker->AssertNode(root); + check_result res = checker->Check(root); + slvr.pop(); + if(res != unsat){ + std::set ::iterator victim = it; + ++it; + node_facts.erase(victim); // if it ain't true, nix it + continue; + } + propagated.push_back(fact); + } + ++it; + } + slvr.pop(); + for(unsigned i = 0; i < propagated.size(); i++){ + root->Annotation.Formula = propagated[i]; + UpdateNodeToNode(node,root); + } + delete checker; + } + for(std::set ::iterator it = conjs.begin(), en = conjs.end(); it != en; ++it){ + expr foo = *it; + node_facts.insert(foo); + } + } + timer_stop("Propagate"); + } /** This class represents a derivation tree. */ class DerivationTree { public: DerivationTree(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) - : slvr(rpfp->slvr), + : slvr(rpfp->slvr()), ctx(rpfp->ctx) { duality = _duality; @@ -1454,7 +1608,13 @@ namespace Duality { constrained = _constrained; false_approx = true; timer_start("Derive"); +#ifndef USE_CACHING_RPFP tree = _tree ? _tree : new RPFP(rpfp->ls); +#else + RPFP::LogicSolver *cache_ls = new RPFP::iZ3LogicSolver(ctx); + cache_ls->slvr->push(); + tree = _tree ? _tree : new RPFP_caching(cache_ls); +#endif tree->HornClauses = rpfp->HornClauses; tree->Push(); // so we can clear out the solver later when finished top = CreateApproximatedInstance(root); @@ -1466,19 +1626,28 @@ namespace Duality { timer_start("Pop"); tree->Pop(1); timer_stop("Pop"); +#ifdef USE_CACHING_RPFP + cache_ls->slvr->pop(1); + delete cache_ls; + tree->ls = rpfp->ls; +#endif timer_stop("Derive"); return res; } #define WITH_CHILDREN - Node *CreateApproximatedInstance(RPFP::Node *from){ - Node *to = tree->CloneNode(from); - to->Annotation = from->Annotation; + void InitializeApproximatedInstance(RPFP::Node *to){ + to->Annotation = to->map->Annotation; #ifndef WITH_CHILDREN tree->CreateLowerBoundEdge(to); #endif leaves.push_back(to); + } + + Node *CreateApproximatedInstance(RPFP::Node *from){ + Node *to = tree->CloneNode(from); + InitializeApproximatedInstance(to); return to; } @@ -1491,7 +1660,7 @@ namespace Duality { return res != unsat; } - bool Build(){ + virtual bool Build(){ #ifdef EFFORT_BOUNDED_STRAT start_decs = tree->CumulativeDecisions(); #endif @@ -1545,15 +1714,25 @@ namespace Duality { } } - void ExpandNode(RPFP::Node *p){ + virtual void ExpandNode(RPFP::Node *p){ // tree->RemoveEdge(p->Outgoing); - Edge *edge = duality->GetNodeOutgoing(p->map,last_decs); - std::vector &cs = edge->Children; - std::vector children(cs.size()); - for(unsigned i = 0; i < cs.size(); i++) - children[i] = CreateApproximatedInstance(cs[i]); - Edge *ne = tree->CreateEdge(p, p->map->Outgoing->F, children); - ne->map = p->map->Outgoing->map; + Edge *ne = p->Outgoing; + if(ne) { + // reporter->Message("Recycling edge..."); + std::vector &cs = ne->Children; + for(unsigned i = 0; i < cs.size(); i++) + InitializeApproximatedInstance(cs[i]); + // ne->dual = expr(); + } + else { + Edge *edge = duality->GetNodeOutgoing(p->map,last_decs); + std::vector &cs = edge->Children; + std::vector children(cs.size()); + for(unsigned i = 0; i < cs.size(); i++) + children[i] = CreateApproximatedInstance(cs[i]); + ne = tree->CreateEdge(p, p->map->Outgoing->F, children); + ne->map = p->map->Outgoing->map; + } #ifndef WITH_CHILDREN tree->AssertEdge(ne); // assert the edge in the solver #else @@ -1573,6 +1752,7 @@ namespace Duality { } #else #if 0 + void ExpansionChoices(std::set &best){ std::vector unused_set, used_set; std::set choices; @@ -1598,12 +1778,12 @@ namespace Duality { heuristic->ChooseExpand(choices, best); } #else - void ExpansionChoicesFull(std::set &best, bool high_priority){ + void ExpansionChoicesFull(std::set &best, bool high_priority, bool best_only = false){ std::set choices; for(std::list::iterator it = leaves.begin(), en = leaves.end(); it != en; ++it) if (high_priority || !tree->Empty(*it)) // if used in the counter-model choices.insert(*it); - heuristic->ChooseExpand(choices, best, high_priority); + heuristic->ChooseExpand(choices, best, high_priority, best_only); } void ExpansionChoicesRec(std::vector &unused_set, std::vector &used_set, @@ -1641,9 +1821,9 @@ namespace Duality { std::set old_choices; - void ExpansionChoices(std::set &best, bool high_priority){ + void ExpansionChoices(std::set &best, bool high_priority, bool best_only = false){ if(!underapprox || constrained || high_priority){ - ExpansionChoicesFull(best, high_priority); + ExpansionChoicesFull(best, high_priority,best_only); return; } std::vector unused_set, used_set; @@ -1668,28 +1848,341 @@ namespace Duality { #endif #endif - bool ExpandSomeNodes(bool high_priority = false){ + bool ExpandSomeNodes(bool high_priority = false, int max = INT_MAX){ #ifdef EFFORT_BOUNDED_STRAT last_decs = tree->CumulativeDecisions() - start_decs; #endif timer_start("ExpandSomeNodes"); timer_start("ExpansionChoices"); std::set choices; - ExpansionChoices(choices,high_priority); + ExpansionChoices(choices,high_priority,max != INT_MAX); timer_stop("ExpansionChoices"); std::list leaves_copy = leaves; // copy so can modify orig leaves.clear(); + int count = 0; for(std::list::iterator it = leaves_copy.begin(), en = leaves_copy.end(); it != en; ++it){ - if(choices.find(*it) != choices.end()) + if(choices.find(*it) != choices.end() && count < max){ + count++; ExpandNode(*it); + } else leaves.push_back(*it); } timer_stop("ExpandSomeNodes"); return !choices.empty(); } + void RemoveExpansion(RPFP::Node *p){ + Edge *edge = p->Outgoing; + Node *parent = edge->Parent; +#ifndef KEEP_EXPANSIONS + std::vector cs = edge->Children; + tree->DeleteEdge(edge); + for(unsigned i = 0; i < cs.size(); i++) + tree->DeleteNode(cs[i]); +#endif + leaves.push_back(parent); + } + + // remove all the descendants of tree root (but not root itself) + void RemoveTree(RPFP *tree, RPFP::Node *root){ + Edge *edge = root->Outgoing; + std::vector cs = edge->Children; + tree->DeleteEdge(edge); + for(unsigned i = 0; i < cs.size(); i++){ + RemoveTree(tree,cs[i]); + tree->DeleteNode(cs[i]); + } + } }; + class DerivationTreeSlow : public DerivationTree { + public: + + struct stack_entry { + unsigned level; // SMT solver stack level + std::vector expansions; + }; + + std::vector stack; + + hash_map updates; + + DerivationTreeSlow(Duality *_duality, RPFP *rpfp, Reporter *_reporter, Heuristic *_heuristic, bool _full_expand) + : DerivationTree(_duality, rpfp, _reporter, _heuristic, _full_expand) { + stack.push_back(stack_entry()); + } + + virtual bool Build(){ + + stack.back().level = tree->slvr().get_scope_level(); + bool was_sat = true; + + while (true) + { + lbool res; + + unsigned slvr_level = tree->slvr().get_scope_level(); + if(slvr_level != stack.back().level) + throw "stacks out of sync!"; + + // res = tree->Solve(top, 1); // incremental solve, keep interpolants for one pop + check_result foo = tree->Check(top); + res = foo == unsat ? l_false : l_true; + + if (res == l_false) { + if (stack.empty()) // should never happen + return false; + + { + std::vector &expansions = stack.back().expansions; + int update_count = 0; + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + tree->SolveSingleNode(top,node); +#ifdef NO_GENERALIZE + node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); +#else + if(expansions.size() == 1 && NodeTooComplicated(node)) + SimplifyNode(node); + else + node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); + Generalize(node); +#endif + if(RecordUpdate(node)) + update_count++; + else + heuristic->Update(node->map); // make it less likely to expand this node in future + } + if(update_count == 0){ + if(was_sat) + throw Incompleteness(); + reporter->Message("backtracked without learning"); + } + } + tree->ComputeProofCore(); // need to compute the proof core before popping solver + bool propagated = false; + while(1) { + std::vector &expansions = stack.back().expansions; + bool prev_level_used = LevelUsedInProof(stack.size()-2); // need to compute this before pop + tree->Pop(1); + hash_set leaves_to_remove; + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + // if(node != top) + // tree->ConstrainParent(node->Incoming[0],node); + std::vector &cs = node->Outgoing->Children; + for(unsigned i = 0; i < cs.size(); i++){ + leaves_to_remove.insert(cs[i]); + UnmapNode(cs[i]); + if(std::find(updated_nodes.begin(),updated_nodes.end(),cs[i]) != updated_nodes.end()) + throw "help!"; + } + } + RemoveLeaves(leaves_to_remove); // have to do this before actually deleting the children + for(unsigned i = 0; i < expansions.size(); i++){ + Node *node = expansions[i]; + RemoveExpansion(node); + } + stack.pop_back(); + if(stack.size() == 1)break; + if(prev_level_used){ + Node *node = stack.back().expansions[0]; +#ifndef NO_PROPAGATE + if(!Propagate(node)) break; +#endif + if(!RecordUpdate(node)) break; // shouldn't happen! + RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list + propagated = true; + continue; + } + if(propagated) break; // propagation invalidates the proof core, so disable non-chron backtrack + RemoveUpdateNodesAtCurrentLevel(); // this level is about to be deleted -- remove its children from update list + std::vector &unused_ex = stack.back().expansions; + for(unsigned i = 0; i < unused_ex.size(); i++) + heuristic->Update(unused_ex[i]->map); // make it less likely to expand this node in future + } + HandleUpdatedNodes(); + if(stack.size() == 1){ + if(top->Outgoing) + tree->DeleteEdge(top->Outgoing); // in case we kept the tree + return false; + } + was_sat = false; + } + else { + was_sat = true; + tree->Push(); + std::vector &expansions = stack.back().expansions; +#ifndef NO_DECISIONS + for(unsigned i = 0; i < expansions.size(); i++){ + tree->FixCurrentState(expansions[i]->Outgoing); + } +#endif +#if 0 + if(tree->slvr().check() == unsat) + throw "help!"; +#endif + stack.push_back(stack_entry()); + stack.back().level = tree->slvr().get_scope_level(); + if(ExpandSomeNodes(false,1)){ + continue; + } + while(stack.size() > 1){ + tree->Pop(1); + stack.pop_back(); + } + return true; + } + } + } + + bool NodeTooComplicated(Node *node){ + int ops = tree->CountOperators(node->Annotation.Formula); + if(ops > 10) return true; + node->Annotation.Formula = tree->RemoveRedundancy(node->Annotation.Formula).simplify(); + return tree->CountOperators(node->Annotation.Formula) > 3; + } + + void SimplifyNode(Node *node){ + // have to destroy the old proof to get a new interpolant + timer_start("SimplifyNode"); + tree->PopPush(); + tree->InterpolateByCases(top,node); + timer_stop("SimplifyNode"); + } + + bool LevelUsedInProof(unsigned level){ + std::vector &expansions = stack[level].expansions; + for(unsigned i = 0; i < expansions.size(); i++) + if(tree->EdgeUsedInProof(expansions[i]->Outgoing)) + return true; + return false; + } + + void RemoveUpdateNodesAtCurrentLevel() { + for(std::list::iterator it = updated_nodes.begin(), en = updated_nodes.end(); it != en;){ + Node *node = *it; + if(AtCurrentStackLevel(node->Incoming[0]->Parent)){ + std::list::iterator victim = it; + ++it; + updated_nodes.erase(victim); + } + else + ++it; + } + } + + void RemoveLeaves(hash_set &leaves_to_remove){ + std::list leaves_copy; + leaves_copy.swap(leaves); + for(std::list::iterator it = leaves_copy.begin(), en = leaves_copy.end(); it != en; ++it){ + if(leaves_to_remove.find(*it) == leaves_to_remove.end()) + leaves.push_back(*it); + } + } + + hash_map > node_map; + std::list updated_nodes; + + virtual void ExpandNode(RPFP::Node *p){ + stack.back().expansions.push_back(p); + DerivationTree::ExpandNode(p); + std::vector &new_nodes = p->Outgoing->Children; + for(unsigned i = 0; i < new_nodes.size(); i++){ + Node *n = new_nodes[i]; + node_map[n->map].push_back(n); + } + } + + bool RecordUpdate(Node *node){ + bool res = duality->UpdateNodeToNode(node->map,node); + if(res){ + std::vector to_update = node_map[node->map]; + for(unsigned i = 0; i < to_update.size(); i++){ + Node *node2 = to_update[i]; + // maintain invariant that no nodes on updated list are created at current stack level + if(node2 == node || !(node->Incoming.size() > 0 && AtCurrentStackLevel(node2->Incoming[0]->Parent))){ + updated_nodes.push_back(node2); + if(node2 != node) + node2->Annotation = node->Annotation; + } + } + } + return res; + } + + void HandleUpdatedNodes(){ + for(std::list::iterator it = updated_nodes.begin(), en = updated_nodes.end(); it != en;){ + Node *node = *it; + node->Annotation = node->map->Annotation; + if(node->Incoming.size() > 0) + tree->ConstrainParent(node->Incoming[0],node); + if(AtCurrentStackLevel(node->Incoming[0]->Parent)){ + std::list::iterator victim = it; + ++it; + updated_nodes.erase(victim); + } + else + ++it; + } + } + + bool AtCurrentStackLevel(Node *node){ + std::vector vec = stack.back().expansions; + for(unsigned i = 0; i < vec.size(); i++) + if(vec[i] == node) + return true; + return false; + } + + void UnmapNode(Node *node){ + std::vector &vec = node_map[node->map]; + for(unsigned i = 0; i < vec.size(); i++){ + if(vec[i] == node){ + std::swap(vec[i],vec.back()); + vec.pop_back(); + return; + } + } + throw "can't unmap node"; + } + + void Generalize(Node *node){ +#ifndef USE_RPFP_CLONE + tree->Generalize(top,node); +#else + RPFP_caching *clone_rpfp = duality->clone_rpfp; + if(!node->Outgoing->map) return; + Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map); + Node *clone_node = clone_edge->Parent; + clone_node->Annotation = node->Annotation; + for(unsigned i = 0; i < clone_edge->Children.size(); i++) + clone_edge->Children[i]->Annotation = node->map->Outgoing->Children[i]->Annotation; + clone_rpfp->GeneralizeCache(clone_edge); + node->Annotation = clone_node->Annotation; +#endif + } + + bool Propagate(Node *node){ +#ifdef USE_RPFP_CLONE + RPFP_caching *clone_rpfp = duality->clone_rpfp; + Edge *clone_edge = clone_rpfp->GetEdgeClone(node->Outgoing->map); + Node *clone_node = clone_edge->Parent; + clone_node->Annotation = node->map->Annotation; + for(unsigned i = 0; i < clone_edge->Children.size(); i++) + clone_edge->Children[i]->Annotation = node->map->Outgoing->Children[i]->Annotation; + bool res = clone_rpfp->PropagateCache(clone_edge); + if(res) + node->Annotation = clone_node->Annotation; + return res; +#else + return false; +#endif + } + + }; + + class Covering { struct cover_info { @@ -1708,6 +2201,11 @@ namespace Duality { Duality *parent; bool some_updates; +#define NO_CONJ_ON_SIMPLE_LOOPS +#ifdef NO_CONJ_ON_SIMPLE_LOOPS + hash_set simple_loops; +#endif + Node *&covered_by(Node *node){ return cm[node].covered_by; } @@ -1742,6 +2240,24 @@ namespace Duality { Covering(Duality *_parent){ parent = _parent; some_updates = false; + +#ifdef NO_CONJ_ON_SIMPLE_LOOPS + hash_map > outgoing; + for(unsigned i = 0; i < parent->rpfp->edges.size(); i++) + outgoing[parent->rpfp->edges[i]->Parent].push_back(parent->rpfp->edges[i]); + for(unsigned i = 0; i < parent->rpfp->nodes.size(); i++){ + Node * node = parent->rpfp->nodes[i]; + std::vector &outs = outgoing[node]; + if(outs.size() == 2){ + for(int j = 0; j < 2; j++){ + Edge *loop_edge = outs[j]; + if(loop_edge->Children.size() == 1 && loop_edge->Children[0] == loop_edge->Parent) + simple_loops.insert(node); + } + } + } +#endif + } bool IsCoveredRec(hash_set &memo, Node *node){ @@ -1904,6 +2420,11 @@ namespace Duality { } bool CouldCover(Node *covered, Node *covering){ +#ifdef NO_CONJ_ON_SIMPLE_LOOPS + // Forsimple loops, we rely on propagation, not covering + if(simple_loops.find(covered->map) != simple_loops.end()) + return false; +#endif #ifdef UNDERAPPROX_NODES // if(parent->underapprox_map.find(covering) != parent->underapprox_map.end()) // return parent->underapprox_map[covering] == covered; @@ -2084,7 +2605,7 @@ namespace Duality { return name; } - virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority){ + virtual void ChooseExpand(const std::set &choices, std::set &best, bool high_priority, bool best_only){ if(!high_priority || !old_cex.tree){ Heuristic::ChooseExpand(choices,best,false); return; diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp old mode 100644 new mode 100755 index fef70e031..cf2c803cb --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -18,6 +18,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "duality_wrapper.h" #include #include "smt_solver.h" @@ -26,17 +33,26 @@ Revision History: #include "expr_abstract.h" #include "stopwatch.h" #include "model_smt2_pp.h" +#include "qe_lite.h" namespace Duality { - solver::solver(Duality::context& c) : object(c), the_model(c) { + solver::solver(Duality::context& c, bool extensional, bool models) : object(c), the_model(c) { params_ref p; p.set_bool("proof", true); // this is currently useless - p.set_bool("model", true); + if(models) + p.set_bool("model", true); p.set_bool("unsat_core", true); + p.set_bool("mbqi",true); + p.set_str("mbqi.id","itp"); // use mbqi for quantifiers in interpolants + p.set_uint("mbqi.max_iterations",1); // use mbqi for quantifiers in interpolants + if(true || extensional) + p.set_bool("array.extensional",true); scoped_ptr sf = mk_smt_solver_factory(); m_solver = (*sf)(m(), p, true, true, true, ::symbol::null); + m_solver->updt_params(p); // why do we have to do this? canceled = false; + m_mode = m().proof_mode(); } expr context::constant(const std::string &name, const sort &ty){ @@ -323,6 +339,25 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st return simplify(p); } + expr expr::qe_lite() const { + ::qe_lite qe(m()); + expr_ref result(to_expr(raw()),m()); + proof_ref pf(m()); + qe(result,pf); + return ctx().cook(result); + } + + expr expr::qe_lite(const std::set &idxs, bool index_of_bound) const { + ::qe_lite qe(m()); + expr_ref result(to_expr(raw()),m()); + proof_ref pf(m()); + uint_set uis; + for(std::set::const_iterator it=idxs.begin(), en = idxs.end(); it != en; ++it) + uis.insert(*it); + qe(uis,index_of_bound,result); + return ctx().cook(result); + } + expr clone_quantifier(const expr &q, const expr &b){ return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw()))); } @@ -347,6 +382,18 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st } + unsigned func_decl::arity() const { + return (to_func_decl(raw())->get_arity()); + } + + sort func_decl::domain(unsigned i) const { + return sort(ctx(),(to_func_decl(raw())->get_domain(i))); + } + + sort func_decl::range() const { + return sort(ctx(),(to_func_decl(raw())->get_range())); + } + func_decl context::fresh_func_decl(char const * prefix, const std::vector &domain, sort const & range){ std::vector < ::sort * > _domain(domain.size()); for(unsigned i = 0; i < domain.size(); i++) @@ -425,15 +472,18 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st static int linearize_assumptions(int num, TermTree *assumptions, - std::vector &linear_assumptions, + std::vector > &linear_assumptions, std::vector &parents){ for(unsigned i = 0; i < assumptions->getChildren().size(); i++) num = linearize_assumptions(num, assumptions->getChildren()[i], linear_assumptions, parents); - linear_assumptions[num] = assumptions->getTerm(); + // linear_assumptions[num].push_back(assumptions->getTerm()); for(unsigned i = 0; i < assumptions->getChildren().size(); i++) parents[assumptions->getChildren()[i]->getNumber()] = num; parents[num] = SHRT_MAX; // in case we have no parent - linear_assumptions[num] = assumptions->getTerm(); + linear_assumptions[num].push_back(assumptions->getTerm()); + std::vector &ts = assumptions->getTerms(); + for(unsigned i = 0; i < ts.size(); i++) + linear_assumptions[num].push_back(ts[i]); return num + 1; } @@ -462,14 +512,15 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st { int size = assumptions->number(0); - std::vector linear_assumptions(size); + std::vector > linear_assumptions(size); std::vector parents(size); linearize_assumptions(0,assumptions,linear_assumptions,parents); ptr_vector< ::ast> _interpolants(size-1); - ptr_vector< ::ast>_assumptions(size); + vector >_assumptions(size); for(int i = 0; i < size; i++) - _assumptions[i] = linear_assumptions[i]; + for(unsigned j = 0; j < linear_assumptions[i].size(); j++) + _assumptions[i].push_back(linear_assumptions[i][j]); ::vector _parents; _parents.resize(parents.size()); for(unsigned i = 0; i < parents.size(); i++) _parents[i] = parents[i]; @@ -477,14 +528,18 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st for(unsigned i = 0; i < theory.size(); i++) _theory[i] = theory[i]; - push(); if(!incremental){ + push(); for(unsigned i = 0; i < linear_assumptions.size(); i++) - add(linear_assumptions[i]); + for(unsigned j = 0; j < linear_assumptions[i].size(); j++) + add(linear_assumptions[i][j]); } - check_result res = check(); + check_result res = unsat; + + if(!m_solver->get_proof()) + res = check(); if(res == unsat){ @@ -517,7 +572,8 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st } #endif - pop(); + if(!incremental) + pop(); return (res == unsat) ? l_false : ((res == sat) ? l_true : l_undef); @@ -549,6 +605,29 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st return ""; } + + static void get_assumptions_rec(stl_ext::hash_set &memo, const proof &pf, std::vector &assumps){ + if(memo.find(pf) != memo.end())return; + memo.insert(pf); + pfrule dk = pf.rule(); + if(dk == PR_ASSERTED){ + expr con = pf.conc(); + assumps.push_back(con); + } + else { + unsigned nprems = pf.num_prems(); + for(unsigned i = 0; i < nprems; i++){ + proof arg = pf.prem(i); + get_assumptions_rec(memo,arg,assumps); + } + } + } + + void proof::get_assumptions(std::vector &assumps){ + stl_ext::hash_set memo; + get_assumptions_rec(memo,*this,assumps); + } + void ast::show() const{ std::cout << mk_pp(raw(), m()) << std::endl; @@ -559,6 +638,40 @@ expr context::make_quant(decl_kind op, const std::vector &_sorts, const st std::cout << std::endl; } + void model::show_hash() const { + std::ostringstream ss; + model_smt2_pp(ss, m(), *m_model, 0); + hash_space::hash hasher; + unsigned h = hasher(ss.str()); + std::cout << "model hash: " << h << "\n"; + } + + void solver::show() { + unsigned n = m_solver->get_num_assertions(); + if(!n) + return; + ast_smt_pp pp(m()); + for (unsigned i = 0; i < n-1; ++i) + pp.add_assumption(m_solver->get_assertion(i)); + pp.display_smt2(std::cout, m_solver->get_assertion(n-1)); + } + + void solver::show_assertion_ids() { +#if 0 + unsigned n = m_solver->get_num_assertions(); + std::cerr << "assertion ids: "; + for (unsigned i = 0; i < n-1; ++i) + std::cerr << " " << m_solver->get_assertion(i)->get_id(); + std::cerr << "\n"; +#else + unsigned n = m_solver->get_num_assertions(); + std::cerr << "assertion ids hash: "; + unsigned h = 0; + for (unsigned i = 0; i < n-1; ++i) + h += m_solver->get_assertion(i)->get_id(); + std::cerr << h << "\n"; +#endif + } void include_ast_show(ast &a){ a.show(); diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 21ed45479..8a77a69da 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -26,6 +26,7 @@ Revision History: #include #include #include +#include #include"version.h" #include @@ -50,6 +51,7 @@ Revision History: #include"scoped_ctrl_c.h" #include"cancel_eh.h" #include"scoped_timer.h" +#include"scoped_proof.h" namespace Duality { @@ -393,6 +395,7 @@ namespace Duality { sort array_range() const; }; + class func_decl : public ast { public: func_decl() : ast() {} @@ -412,6 +415,7 @@ namespace Duality { expr operator()(unsigned n, expr const * args) const; expr operator()(const std::vector &args) const; + expr operator()() const; expr operator()(expr const & a) const; expr operator()(int a) const; expr operator()(expr const & a1, expr const & a2) const; @@ -447,6 +451,7 @@ namespace Duality { bool is_datatype() const { return get_sort().is_datatype(); } bool is_relation() const { return get_sort().is_relation(); } bool is_finite_domain() const { return get_sort().is_finite_domain(); } + bool is_true() const {return is_app() && decl().get_decl_kind() == True; } bool is_numeral() const { return is_app() && decl().get_decl_kind() == OtherArith && m().is_unique_value(to_expr(raw())); @@ -455,6 +460,8 @@ namespace Duality { bool is_quantifier() const {return raw()->get_kind() == AST_QUANTIFIER;} bool is_var() const {return raw()->get_kind() == AST_VAR;} bool is_label (bool &pos,std::vector &names) const ; + bool is_ground() const {return to_app(raw())->is_ground();} + bool has_quantifiers() const {return to_app(raw())->has_quantifiers();} // operator Z3_app() const { assert(is_app()); return reinterpret_cast(m_ast); } func_decl decl() const {return func_decl(ctx(),to_app(raw())->get_decl());} @@ -554,6 +561,10 @@ namespace Duality { expr simplify(params const & p) const; + expr qe_lite() const; + + expr qe_lite(const std::set &idxs, bool index_of_bound) const; + friend expr clone_quantifier(const expr &, const expr &); friend expr clone_quantifier(const expr &q, const expr &b, const std::vector &patterns); @@ -593,6 +604,36 @@ namespace Duality { }; + typedef ::decl_kind pfrule; + + class proof : public ast { + public: + proof(context & c):ast(c) {} + proof(context & c, ::proof *s):ast(c, s) {} + proof(proof const & s):ast(s) {} + operator ::proof*() const { return to_app(raw()); } + proof & operator=(proof const & s) { return static_cast(ast::operator=(s)); } + + pfrule rule() const { + ::func_decl *d = to_app(raw())->get_decl(); + return d->get_decl_kind(); + } + + unsigned num_prems() const { + return to_app(raw())->get_num_args() - 1; + } + + expr conc() const { + return ctx().cook(to_app(raw())->get_arg(num_prems())); + } + + proof prem(unsigned i) const { + return proof(ctx(),to_app(to_app(raw())->get_arg(i))); + } + + void get_assumptions(std::vector &assumps); + }; + #if 0 #if Z3_MAJOR_VERSION > 4 || Z3_MAJOR_VERSION == 4 && Z3_MINOR_VERSION >= 3 @@ -682,6 +723,7 @@ namespace Duality { m_model = s; return *this; } + bool null() const {return !m_model;} expr eval(expr const & n, bool model_completion=true) const { ::model * _m = m_model.get(); @@ -691,6 +733,7 @@ namespace Duality { } void show() const; + void show_hash() const; unsigned num_consts() const {return m_model.get()->get_num_constants();} unsigned num_funcs() const {return m_model.get()->get_num_functions();} @@ -774,8 +817,9 @@ namespace Duality { ::solver *m_solver; model the_model; bool canceled; + proof_gen_mode m_mode; public: - solver(context & c); + solver(context & c, bool extensional = false, bool models = true); solver(context & c, ::solver *s):object(c),the_model(c) { m_solver = s; canceled = false;} solver(solver const & s):object(s), the_model(s.the_model) { m_solver = s.m_solver; canceled = false;} ~solver() { @@ -787,6 +831,7 @@ namespace Duality { m_ctx = s.m_ctx; m_solver = s.m_solver; the_model = s.the_model; + m_mode = s.m_mode; return *this; } struct cancel_exception {}; @@ -795,11 +840,12 @@ namespace Duality { throw(cancel_exception()); } // void set(params const & p) { Z3_solver_set_params(ctx(), m_solver, p); check_error(); } - void push() { m_solver->push(); } - void pop(unsigned n = 1) { m_solver->pop(n); } + void push() { scoped_proof_mode spm(m(),m_mode); m_solver->push(); } + void pop(unsigned n = 1) { scoped_proof_mode spm(m(),m_mode); m_solver->pop(n); } // void reset() { Z3_solver_reset(ctx(), m_solver); check_error(); } - void add(expr const & e) { m_solver->assert_expr(e); } + void add(expr const & e) { scoped_proof_mode spm(m(),m_mode); m_solver->assert_expr(e); } check_result check() { + scoped_proof_mode spm(m(),m_mode); checkpoint(); lbool r = m_solver->check_sat(0,0); model_ref m; @@ -808,6 +854,7 @@ namespace Duality { return to_check_result(r); } check_result check_keep_model(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { + scoped_proof_mode spm(m(),m_mode); model old_model(the_model); check_result res = check(n,assumptions,core_size,core); if(the_model == 0) @@ -815,6 +862,7 @@ namespace Duality { return res; } check_result check(unsigned n, expr * const assumptions, unsigned *core_size = 0, expr *core = 0) { + scoped_proof_mode spm(m(),m_mode); checkpoint(); std::vector< ::expr *> _assumptions(n); for (unsigned i = 0; i < n; i++) { @@ -839,6 +887,7 @@ namespace Duality { } #if 0 check_result check(expr_vector assumptions) { + scoped_proof_mode spm(m(),m_mode); unsigned n = assumptions.size(); z3array _assumptions(n); for (unsigned i = 0; i < n; i++) { @@ -863,10 +912,22 @@ namespace Duality { int get_num_decisions(); void cancel(){ + scoped_proof_mode spm(m(),m_mode); canceled = true; if(m_solver) m_solver->cancel(); } + + unsigned get_scope_level(){ scoped_proof_mode spm(m(),m_mode); return m_solver->get_scope_level();} + + void show(); + void show_assertion_ids(); + + proof get_proof(){ + scoped_proof_mode spm(m(),m_mode); + return proof(ctx(),m_solver->get_proof()); + } + }; #if 0 @@ -1144,6 +1205,9 @@ namespace Duality { inline expr func_decl::operator()(const std::vector &args) const { return operator()(args.size(),&args[0]); } + inline expr func_decl::operator()() const { + return operator()(0,0); + } inline expr func_decl::operator()(expr const & a) const { return operator()(1,&a); } @@ -1199,6 +1263,8 @@ namespace Duality { inline expr getTerm(){return term;} + inline std::vector &getTerms(){return terms;} + inline std::vector &getChildren(){ return children; } @@ -1215,6 +1281,8 @@ namespace Duality { } inline void setTerm(expr t){term = t;} + + inline void addTerm(expr t){terms.push_back(t);} inline void setChildren(const std::vector & _children){ children = _children; @@ -1231,6 +1299,7 @@ namespace Duality { private: expr term; + std::vector terms; std::vector children; int num; }; @@ -1239,8 +1308,8 @@ namespace Duality { class interpolating_solver : public solver { public: - interpolating_solver(context &ctx) - : solver(ctx) + interpolating_solver(context &ctx, bool models = true) + : solver(ctx, true, models) { weak_mode = false; } @@ -1277,6 +1346,7 @@ namespace Duality { void SetWeakInterpolants(bool weak); void SetPrintToFile(const std::string &file_name); + const std::vector &GetInterpolationAxioms() {return theory;} const char *profile(); private: @@ -1303,6 +1373,21 @@ namespace Duality { typedef double clock_t; clock_t current_time(); inline void output_time(std::ostream &os, clock_t time){os << time;} + + template class uptr { + public: + X *ptr; + uptr(){ptr = 0;} + void set(X *_ptr){ + if(ptr) delete ptr; + ptr = _ptr; + } + X *get(){ return ptr;} + ~uptr(){ + if(ptr) delete ptr; + } + }; + }; // to make Duality::ast hashable @@ -1317,7 +1402,7 @@ namespace hash_space { } // to make Duality::ast hashable in windows -#ifdef WIN32 +#ifdef _WINDOWS template <> inline size_t stdext::hash_value(const Duality::ast& s) { @@ -1331,7 +1416,20 @@ namespace std { class less { public: bool operator()(const Duality::ast &s, const Duality::ast &t) const { - return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id(); + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); + } + }; +} + +// to make Duality::ast usable in ordered collections +namespace std { + template <> + class less { + public: + bool operator()(const Duality::expr &s, const Duality::expr &t) const { + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); } }; } @@ -1348,7 +1446,7 @@ namespace hash_space { } // to make Duality::func_decl hashable in windows -#ifdef WIN32 +#ifdef _WINDOWS template <> inline size_t stdext::hash_value(const Duality::func_decl& s) { @@ -1362,11 +1460,11 @@ namespace std { class less { public: bool operator()(const Duality::func_decl &s, const Duality::func_decl &t) const { - return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id(); + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); } }; } - #endif diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index f316c22cf..26146bfa3 100755 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -18,6 +18,12 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif #include "iz3base.h" #include diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index 30ac57bae..6bf09bb85 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -24,6 +24,16 @@ Revision History: #include "iz3mgr.h" #include "iz3scopes.h" +namespace hash_space { + template <> + class hash { + public: + size_t operator()(func_decl * const &s) const { + return (size_t) s; + } + }; +} + /* Base class for interpolators. Includes an AST manager and a scoping object as bases. */ @@ -182,6 +192,4 @@ class iz3base : public iz3mgr, public scopes { - - #endif diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp index b4e55af20..d423ba48f 100755 --- a/src/interp/iz3checker.cpp +++ b/src/interp/iz3checker.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3base.h" #include "iz3checker.h" diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp index 85e090c5b..1d81a1b15 100755 --- a/src/interp/iz3foci.cpp +++ b/src/interp/iz3foci.cpp @@ -51,6 +51,13 @@ public: typedef hash_map NodeToAst; NodeToAst node_to_ast; // maps Z3 ast's to foci expressions + // We only use this for FuncDeclToSymbol, which has no range destructor + struct symb_hash { + size_t operator()(const symb &s) const { + return (size_t) s; + } + }; + typedef hash_map FuncDeclToSymbol; FuncDeclToSymbol func_decl_to_symbol; // maps Z3 func decls to symbols diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index f6767c037..a564026bd 100755 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -42,7 +42,7 @@ Revision History: #include #include #else -#ifdef WIN32 +#ifdef _WINDOWS #define stl_ext stdext #define hash_space std #include @@ -61,12 +61,12 @@ Revision History: // stupid STL doesn't include hash function for class string -#ifndef WIN32 +#ifndef _WINDOWS namespace stl_ext { template <> class hash { - stl_ext::hash H; + stl_ext::hash H; public: size_t operator()(const std::string &s) const { return H(s.c_str()); @@ -86,7 +86,7 @@ namespace hash_space { }; } -#ifdef WIN32 +#ifdef _WINDOWS template <> inline size_t stdext::hash_value >(const std::pair& p) { // hash _Keyval to size_t value one-to-one @@ -112,7 +112,7 @@ size_t stdext::hash_value >(const std::pair& p) } #endif -#ifdef WIN32 +#ifdef _WINDOWS namespace std { template <> @@ -139,8 +139,9 @@ namespace std { #endif -#ifndef WIN32 +#ifndef _WINDOWS +#if 0 namespace stl_ext { template class hash { @@ -150,10 +151,11 @@ namespace stl_ext { } }; } +#endif #endif -#ifdef WIN32 +#ifdef _WINDOWS diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 92afc5723..c204cc35d 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -18,6 +18,14 @@ Revision History: --*/ /* Copyright 2011 Microsoft Research. */ + +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include #include #include @@ -75,15 +83,16 @@ struct frame_reducer : public iz3mgr { } } - void get_frames(const std::vector &z3_preds, + void get_frames(const std::vector >&z3_preds, const std::vector &orig_parents, - std::vector &assertions, + std::vector >&assertions, std::vector &parents, z3pf proof){ frames = z3_preds.size(); orig_parents_copy = orig_parents; for(unsigned i = 0; i < z3_preds.size(); i++) - frame_map[z3_preds[i]] = i; + for(unsigned j = 0; j < z3_preds[i].size(); j++) + frame_map[z3_preds[i][j]] = i; used_frames.resize(frames); hash_set memo; get_proof_assumptions_rec(proof,memo,used_frames); @@ -202,7 +211,7 @@ public: } void proof_to_interpolant(z3pf proof, - const std::vector &cnsts, + const std::vector > &cnsts, const std::vector &parents, std::vector &interps, const std::vector &theory, @@ -212,11 +221,12 @@ public: test_secondary(cnsts,parents,interps); return; #endif + profiling::timer_start("Interpolation prep"); // get rid of frames not used in proof - std::vector cnsts_vec; + std::vector > cnsts_vec; std::vector parents_vec; frame_reducer fr(*this); fr.get_frames(cnsts,parents,cnsts_vec,parents_vec,proof); @@ -235,10 +245,7 @@ public: #define BINARY_INTERPOLATION #ifndef BINARY_INTERPOLATION // create a translator - std::vector > cnsts_vec_vec(cnsts_vec.size()); - for(unsigned i = 0; i < cnsts_vec.size(); i++) - cnsts_vec_vec[i].push_back(cnsts_vec[i]); - iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec_vec,parents_vec,theory); + iz3translation *tr = iz3translation::create(*this,sp,cnsts_vec,parents_vec,theory); tr_killer.set(tr); // set the translation options, if needed @@ -273,7 +280,8 @@ public: std::vector > cnsts_vec_vec(2); for(unsigned j = 0; j < cnsts_vec.size(); j++){ bool is_A = the_base.in_range(j,rng); - cnsts_vec_vec[is_A ? 0 : 1].push_back(cnsts_vec[j]); + for(unsigned k = 0; k < cnsts_vec[j].size(); k++) + cnsts_vec_vec[is_A ? 0 : 1].push_back(cnsts_vec[j][k]); } killme tr_killer_i; @@ -308,6 +316,19 @@ public: } + void proof_to_interpolant(z3pf proof, + std::vector &cnsts, + const std::vector &parents, + std::vector &interps, + const std::vector &theory, + interpolation_options_struct *options = 0 + ){ + std::vector > cnsts_vec(cnsts.size()); + for(unsigned i = 0; i < cnsts.size(); i++) + cnsts_vec[i].push_back(cnsts[i]); + proof_to_interpolant(proof,cnsts_vec,parents,interps,theory,options); + } + // same as above, but represents the tree using an ast void proof_to_interpolant(const z3pf &proof, @@ -322,7 +343,6 @@ public: to_parents_vec_representation(_cnsts, tree, cnsts, parents, theory, pos_map); - //use the parents vector representation to compute interpolant proof_to_interpolant(proof,cnsts,parents,interps,theory,options); @@ -397,6 +417,35 @@ void iz3interpolate(ast_manager &_m_manager, interps[i] = itp.uncook(_interps[i]); } +void iz3interpolate(ast_manager &_m_manager, + ast *proof, + const ::vector > &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector &theory, + interpolation_options_struct * options) +{ + iz3interp itp(_m_manager); + if(options) + options->apply(itp); + std::vector > _cnsts(cnsts.size()); + std::vector _parents(parents.size()); + std::vector _interps; + std::vector _theory(theory.size()); + for(unsigned i = 0; i < cnsts.size(); i++) + for(unsigned j = 0; j < cnsts[i].size(); j++) + _cnsts[i].push_back(itp.cook(cnsts[i][j])); + for(unsigned i = 0; i < parents.size(); i++) + _parents[i] = parents[i]; + for(unsigned i = 0; i < theory.size(); i++) + _theory[i] = itp.cook(theory[i]); + iz3mgr::ast _proof = itp.cook(proof); + itp.proof_to_interpolant(_proof,_cnsts,_parents,_interps,_theory,options); + interps.resize(_interps.size()); + for(unsigned i = 0; i < interps.size(); i++) + interps[i] = itp.uncook(_interps[i]); +} + void iz3interpolate(ast_manager &_m_manager, ast *proof, const ptr_vector &cnsts, @@ -461,5 +510,3 @@ void interpolation_options_struct::apply(iz3base &b){ b.set_option((*it).first,(*it).second); } - - diff --git a/src/interp/iz3interp.h b/src/interp/iz3interp.h index 62f967c02..52aa716c3 100644 --- a/src/interp/iz3interp.h +++ b/src/interp/iz3interp.h @@ -56,6 +56,16 @@ void iz3interpolate(ast_manager &_m_manager, const ptr_vector &theory, interpolation_options_struct * options = 0); +/* Same as above, but each constraint is a vector of formulas. */ + +void iz3interpolate(ast_manager &_m_manager, + ast *proof, + const vector > &cnsts, + const ::vector &parents, + ptr_vector &interps, + const ptr_vector &theory, + interpolation_options_struct * options = 0); + /* Compute an interpolant from a proof. This version uses the ast representation, for compatibility with the new API. */ diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp old mode 100644 new mode 100755 index faa4a636d..35dc67bcd --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -18,6 +18,15 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#pragma warning(disable:4805) +#pragma warning(disable:4800) +#endif + #include "iz3mgr.h" #include @@ -172,7 +181,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector &bvs, ast &body){ std::vector names; - std::vector types; + std::vector types; std::vector bound_asts; unsigned num_bound = bvs.size(); @@ -190,7 +199,7 @@ iz3mgr::ast iz3mgr::make_quant(opr op, const std::vector &bvs, ast &body){ op == Forall, names.size(), &types[0], &names[0], abs_body.get(), 0, - symbol(), + symbol("itp"), symbol(), 0, 0, 0, 0 @@ -240,6 +249,9 @@ iz3mgr::ast iz3mgr::clone(const ast &t, const std::vector &_args){ void iz3mgr::show(ast t){ + if(t.null()){ + std::cout << "(null)" << std::endl; + } params_ref p; p.set_bool("flat_assoc",false); std::cout << mk_pp(t.raw(), m(), p) << std::endl; @@ -485,7 +497,7 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector& coeffs){ get_farkas_coeffs(proof,rats); coeffs.resize(rats.size()); for(unsigned i = 0; i < rats.size(); i++){ - sort *is = m().mk_sort(m_arith_fid, INT_SORT); + class sort *is = m().mk_sort(m_arith_fid, INT_SORT); ast coeff = cook(m_arith_util.mk_numeral(rats[i],is)); coeffs[i] = coeff; } @@ -640,9 +652,9 @@ void iz3mgr::get_assign_bounds_rule_coeffs(const ast &proof, std::vector &coeffs, const std::vector &ineqs){ +iz3mgr::ast iz3mgr::sum_inequalities(const std::vector &coeffs, const std::vector &ineqs, bool round_off){ ast zero = make_int("0"); ast thing = make(Leq,zero,zero); for(unsigned i = 0; i < ineqs.size(); i++){ - linear_comb(thing,coeffs[i],ineqs[i]); + linear_comb(thing,coeffs[i],ineqs[i], round_off); } thing = simplify_ineq(thing); return thing; @@ -761,6 +779,19 @@ int iz3mgr::occurs_in(ast var, ast e){ } +bool iz3mgr::solve_arith(const ast &v, const ast &x, const ast &y, ast &res){ + if(op(x) == Plus){ + int n = num_args(x); + for(int i = 0; i < n; i++){ + if(arg(x,i) == v){ + res = z3_simplify(make(Sub, y, make(Sub, x, v))); + return true; + } + } + } + return false; +} + // find a controlling equality for a given variable v in a term // a controlling equality is of the form v = t, which, being // false would force the formula to have the specifid truth value @@ -774,6 +805,9 @@ iz3mgr::ast iz3mgr::cont_eq(stl_ext::hash_set &cont_eq_memo, bool truth, as if(!truth && op(e) == Equal){ if(arg(e,0) == v) return(arg(e,1)); if(arg(e,1) == v) return(arg(e,0)); + ast res; + if(solve_arith(v,arg(e,0),arg(e,1),res)) return res; + if(solve_arith(v,arg(e,1),arg(e,0),res)) return res; } if((!truth && op(e) == And) || (truth && op(e) == Or)){ int nargs = num_args(e); @@ -815,11 +849,35 @@ iz3mgr::ast iz3mgr::subst(ast var, ast t, ast e){ return subst(memo,var,t,e); } +iz3mgr::ast iz3mgr::subst(stl_ext::hash_map &subst_memo,ast e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = subst_memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + int nargs = num_args(e); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = subst(subst_memo,arg(e,i)); + opr f = op(e); + if(f == Equal && args[0] == args[1]) res = mk_true(); + else res = clone(e,args); + } + return res; +} + // apply a quantifier to a formula, with some optimizations // 1) bound variable does not occur -> no quantifier // 2) bound variable must be equal to some term -> substitute iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){ + if((quantifier == Forall && op(e) == And) + || (quantifier == Exists && op(e) == Or)){ + int n = num_args(e); + std::vector args(n); + for(int i = 0; i < n; i++) + args[i] = apply_quant(quantifier,var,arg(e,i)); + return make(op(e),args); + } if(!occurs_in(var,e))return e; hash_set cont_eq_memo; ast cterm = cont_eq(cont_eq_memo, quantifier == Forall, var, e); @@ -829,3 +887,14 @@ iz3mgr::ast iz3mgr::apply_quant(opr quantifier, ast var, ast e){ std::vector bvs; bvs.push_back(var); return make_quant(quantifier,bvs,e); } + +#if 0 +void iz3mgr::get_bound_substitutes(stl_ext::hash_map &memo, const ast &e, const ast &var, std::vector &substs){ + std::pair foo(e,false); + std::pair::iterator,bool> bar = memo.insert(foo); + if(bar.second){ + if(op(e) == + } + +} +#endif diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h old mode 100644 new mode 100755 index f6c0bdf87..d9593ced5 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -22,6 +22,7 @@ Revision History: #include +#include #include "iz3hash.h" #include"well_sorted.h" @@ -65,7 +66,7 @@ class ast_i { return _ast == other._ast; } bool lt(const ast_i &other) const { - return _ast < other._ast; + return _ast->get_id() < other._ast->get_id(); } friend bool operator==(const ast_i &x, const ast_i&y){ return x.eq(y); @@ -76,7 +77,7 @@ class ast_i { friend bool operator<(const ast_i &x, const ast_i&y){ return x.lt(y); } - size_t hash() const {return (size_t)_ast;} + size_t hash() const {return _ast->get_id();} bool null() const {return !_ast;} }; @@ -126,7 +127,7 @@ namespace hash_space { } // to make ast_r hashable in windows -#ifdef WIN32 +#ifdef _WINDOWS template <> inline size_t stdext::hash_value(const ast_r& s) { @@ -140,7 +141,8 @@ namespace std { class less { public: bool operator()(const ast_r &s, const ast_r &t) const { - return s.raw() < t.raw(); // s.raw()->get_id() < t.raw()->get_id(); + // return s.raw() < t.raw(); + return s.raw()->get_id() < t.raw()->get_id(); } }; } @@ -261,6 +263,7 @@ class iz3mgr { default:; } assert(0); + return 0; } ast arg(const ast &t, int i){ @@ -359,6 +362,12 @@ class iz3mgr { return fid == m().get_basic_family_id() && k == BOOL_SORT; } + bool is_array_type(type t){ + family_id fid = to_sort(t)->get_family_id(); + decl_kind k = to_sort(t)->get_decl_kind(); + return fid == m_array_fid && k == ARRAY_SORT; + } + type get_range_type(symb s){ return to_func_decl(s)->get_range(); } @@ -599,9 +608,9 @@ class iz3mgr { return d; } - void linear_comb(ast &P, const ast &c, const ast &Q); + void linear_comb(ast &P, const ast &c, const ast &Q, bool round_off = false); - ast sum_inequalities(const std::vector &coeffs, const std::vector &ineqs); + ast sum_inequalities(const std::vector &coeffs, const std::vector &ineqs, bool round_off = false); ast simplify_ineq(const ast &ineq){ ast res = make(op(ineq),arg(ineq,0),z3_simplify(arg(ineq,1))); @@ -631,6 +640,9 @@ class iz3mgr { ast subst(ast var, ast t, ast e); + // apply a substitution defined by a map + ast subst(stl_ext::hash_map &map, ast e); + // apply a quantifier to a formula, with some optimizations // 1) bound variable does not occur -> no quantifier // 2) bound variable must be equal to some term -> substitute @@ -683,13 +695,14 @@ class iz3mgr { protected: ast_manager &m_manager; + int occurs_in(ast var, ast e); private: ast mki(family_id fid, decl_kind sk, int n, raw_ast **args); ast make(opr op, int n, raw_ast **args); ast make(symb sym, int n, raw_ast **args); int occurs_in1(stl_ext::hash_map &occurs_in_memo, ast var, ast e); - int occurs_in(ast var, ast e); + bool solve_arith(const ast &v, const ast &x, const ast &y, ast &res); ast cont_eq(stl_ext::hash_set &cont_eq_memo, bool truth, ast v, ast e); ast subst(stl_ext::hash_map &subst_memo, ast var, ast t, ast e); diff --git a/src/interp/iz3pp.cpp b/src/interp/iz3pp.cpp index 1f9351453..31b375c0f 100644 --- a/src/interp/iz3pp.cpp +++ b/src/interp/iz3pp.cpp @@ -40,24 +40,38 @@ Revision History: using namespace stl_ext; #endif +#ifndef WIN32 +// We promise not to use this for hash_map with range destructor +namespace stl_ext { + template <> + class hash { + public: + size_t operator()(const expr *p) const { + return (size_t) p; + } + }; +} +#endif + + // TBD: algebraic data-types declarations will not be printed. class free_func_visitor { ast_manager& m; func_decl_set m_funcs; - obj_hashtable m_sorts; + obj_hashtable m_sorts; public: free_func_visitor(ast_manager& m): m(m) {} void operator()(var * n) { } void operator()(app * n) { m_funcs.insert(n->get_decl()); - sort* s = m.get_sort(n); + class sort* s = m.get_sort(n); if (s->get_family_id() == null_family_id) { m_sorts.insert(s); } } void operator()(quantifier * n) { } func_decl_set& funcs() { return m_funcs; } - obj_hashtable& sorts() { return m_sorts; } + obj_hashtable& sorts() { return m_sorts; } }; class iz3pp_helper : public iz3mgr { @@ -132,8 +146,8 @@ void iz3pp(ast_manager &m, func_decl_set &funcs = visitor.funcs(); func_decl_set::iterator it = funcs.begin(), end = funcs.end(); - obj_hashtable& sorts = visitor.sorts(); - obj_hashtable::iterator sit = sorts.begin(), send = sorts.end(); + obj_hashtable& sorts = visitor.sorts(); + obj_hashtable::iterator sit = sorts.begin(), send = sorts.end(); diff --git a/src/interp/iz3profiling.cpp b/src/interp/iz3profiling.cpp index 262254271..2c4a31d58 100755 --- a/src/interp/iz3profiling.cpp +++ b/src/interp/iz3profiling.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3profiling.h" #include diff --git a/src/interp/iz3proof.cpp b/src/interp/iz3proof.cpp index 968a4b25a..3fefea73f 100755 --- a/src/interp/iz3proof.cpp +++ b/src/interp/iz3proof.cpp @@ -18,6 +18,12 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif #include "iz3proof.h" #include "iz3profiling.h" diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp old mode 100644 new mode 100755 index a2d05f7f9..303d90b1b --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3proof_itp.h" #ifndef WIN32 @@ -118,6 +125,30 @@ class iz3proof_itp_impl : public iz3proof_itp { where t is an arbitrary term */ symb rewrite_B; + /* a normalization step is of the form (lhs=rhs) : proof, where "proof" + is a proof of lhs=rhs and lhs is a mixed term. If rhs is a mixed term + then it must have a greater index than lhs. */ + symb normal_step; + + /* A chain of normalization steps is either "true" (the null chain) + or normal_chain( ), where step is a normalization step + and tail is a normalization chain. The lhs of must have + a less term index than any lhs in the chain. Moreover, the rhs of + may not occur as the lhs of step in . If we wish to + add lhs=rhs to the beginning of and rhs=rhs' occurs in + we must apply transitivity, transforming to lhs=rhs'. */ + + symb normal_chain; + + /* If p is a proof of Q and c is a normalization chain, then normal(p,c) + is a proof of Q(c) (that is, Q with all substitutions in c performed). */ + + symb normal; + + /** Stand-ins for quantifiers */ + + symb sforall, sexists; + ast get_placeholder(ast t){ hash_map::iterator it = placeholders.find(t); @@ -209,6 +240,10 @@ class iz3proof_itp_impl : public iz3proof_itp { ast neg_pivot_lit = mk_not(atom); if(op(pivot) != Not) std::swap(premise1,premise2); + if(op(pivot) == Equal && op(arg(pivot,0)) == Select && op(arg(pivot,1)) == Select){ + neg_pivot_lit = mk_not(neg_pivot_lit); + std::swap(premise1,premise2); + } return resolve_arith_rec1(memo, neg_pivot_lit, premise1, premise2); } @@ -333,7 +368,13 @@ class iz3proof_itp_impl : public iz3proof_itp { break; } default: - res = itp2; + { + symb s = sym(itp2); + if(s == sforall || s == sexists) + res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1))); + else + res = itp2; + } } } return res; @@ -363,7 +404,13 @@ class iz3proof_itp_impl : public iz3proof_itp { break; } default: - res = itp1; + { + symb s = sym(itp1); + if(s == sforall || s == sexists) + res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2)); + else + res = itp1; + } } } return res; @@ -451,7 +498,12 @@ class iz3proof_itp_impl : public iz3proof_itp { hash_map simplify_memo; ast simplify(const ast &t){ - return simplify_rec(t); + ast res = normalize(simplify_rec(t)); +#ifdef BOGUS_QUANTS + if(localization_vars.size()) + res = add_quants(z3_simplify(res)); +#endif + return res; } ast simplify_rec(const ast &e){ @@ -521,47 +573,88 @@ class iz3proof_itp_impl : public iz3proof_itp { throw cannot_simplify(); } + bool is_normal_ineq(const ast &ineq){ + if(sym(ineq) == normal) + return is_ineq(arg(ineq,0)); + return is_ineq(ineq); + } + + ast destruct_cond_ineq(const ast &ineq, ast &Aproves, ast &Bproves){ + ast res = ineq; + opr o = op(res); + if(o == And){ + Aproves = my_and(Aproves,arg(res,0)); + res = arg(res,1); + o = op(res); + } + if(o == Implies){ + Bproves = my_and(Bproves,arg(res,0)); + res = arg(res,1); + } + return res; + } + ast simplify_sum(std::vector &args){ - ast cond = mk_true(); - ast ineq = args[0]; - if(!is_ineq(ineq)) throw cannot_simplify(); - sum_cond_ineq(ineq,cond,args[1],args[2]); - return my_implies(cond,ineq); + ast Aproves = mk_true(), Bproves = mk_true(); + ast ineq = destruct_cond_ineq(args[0],Aproves,Bproves); + if(!is_normal_ineq(ineq)) throw cannot_simplify(); + sum_cond_ineq(ineq,args[1],args[2],Aproves,Bproves); + return my_and(Aproves,my_implies(Bproves,ineq)); } ast simplify_rotate_sum(const ast &pl, const ast &pf){ - ast cond = mk_true(); + ast Aproves = mk_true(), Bproves = mk_true(); ast ineq = make(Leq,make_int("0"),make_int("0")); - return rotate_sum_rec(pl,pf,cond,ineq); + ineq = rotate_sum_rec(pl,pf,Aproves,Bproves,ineq); + if(is_true(Aproves) && is_true(Bproves)) + return ineq; + return my_and(Aproves,my_implies(Bproves,ineq)); } bool is_rewrite_chain(const ast &chain){ return sym(chain) == concat; } - ast ineq_from_chain(const ast &chain, ast &cond){ - if(is_rewrite_chain(chain)){ - ast last = chain_last(chain); - ast rest = chain_rest(chain); - if(is_true(rest) && is_rewrite_side(LitA,last) - && is_true(rewrite_lhs(last))){ - cond = my_and(cond,rewrite_cond(last)); - return rewrite_rhs(last); - } - if(is_rewrite_side(LitB,last) && is_true(rewrite_cond(last))) - return ineq_from_chain(rest,cond); +#if 0 + ast ineq_from_chain_simple(const ast &chain, ast &cond){ + if(is_true(chain)) + return chain; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + if(is_true(rest) && is_rewrite_side(LitA,last) + && is_true(rewrite_lhs(last))){ + cond = my_and(cond,rewrite_cond(last)); + return rewrite_rhs(last); } + if(is_rewrite_side(LitB,last) && is_true(rewrite_cond(last))) + return ineq_from_chain_simple(rest,cond); + return chain; + } +#endif + + ast ineq_from_chain(const ast &chain, ast &Aproves, ast &Bproves){ + if(is_rewrite_chain(chain)) + return rewrite_chain_to_normal_ineq(chain,Aproves,Bproves); return chain; } - void sum_cond_ineq(ast &ineq, ast &cond, const ast &coeff2, const ast &ineq2){ + + void sum_cond_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){ opr o = op(ineq2); - if(o == Implies){ - sum_cond_ineq(ineq,cond,coeff2,arg(ineq2,1)); - cond = my_and(cond,arg(ineq2,0)); + if(o == And){ + sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves); + Aproves = my_and(Aproves,arg(ineq2,0)); + } + else if(o == Implies){ + sum_cond_ineq(ineq,coeff2,arg(ineq2,1),Aproves,Bproves); + Bproves = my_and(Bproves,arg(ineq2,0)); } else { - ast the_ineq = ineq_from_chain(ineq2,cond); + ast the_ineq = ineq_from_chain(ineq2,Aproves,Bproves); + if(sym(ineq) == normal || sym(the_ineq) == normal){ + sum_normal_ineq(ineq,coeff2,the_ineq,Aproves,Bproves); + return; + } if(is_ineq(the_ineq)) linear_comb(ineq,coeff2,the_ineq); else @@ -569,6 +662,27 @@ class iz3proof_itp_impl : public iz3proof_itp { } } + void destruct_normal(const ast &pf, ast &p, ast &n){ + if(sym(pf) == normal){ + p = arg(pf,0); + n = arg(pf,1); + } + else { + p = pf; + n = mk_true(); + } + } + + void sum_normal_ineq(ast &ineq, const ast &coeff2, const ast &ineq2, ast &Aproves, ast &Bproves){ + ast in1,in2,n1,n2; + destruct_normal(ineq,in1,n1); + destruct_normal(ineq2,in2,n2); + ast dummy1, dummy2; + sum_cond_ineq(in1,coeff2,in2,dummy1,dummy2); + n1 = merge_normal_chains(n1,n2, Aproves, Bproves); + ineq = make_normal(in1,n1); + } + bool is_ineq(const ast &ineq){ opr o = op(ineq); if(o == Not) o = op(arg(ineq,0)); @@ -577,6 +691,12 @@ class iz3proof_itp_impl : public iz3proof_itp { // divide both sides of inequality by a non-negative integer divisor ast idiv_ineq(const ast &ineq1, const ast &divisor){ + if(sym(ineq1) == normal){ + ast in1,n1; + destruct_normal(ineq1,in1,n1); + in1 = idiv_ineq(in1,divisor); + return make_normal(in1,n1); + } if(divisor == make_int(rational(1))) return ineq1; ast ineq = ineq1; @@ -585,17 +705,20 @@ class iz3proof_itp_impl : public iz3proof_itp { return make(op(ineq),mk_idiv(arg(ineq,0),divisor),mk_idiv(arg(ineq,1),divisor)); } - ast rotate_sum_rec(const ast &pl, const ast &pf, ast &cond, ast &ineq){ - if(pf == pl) - return my_implies(cond,simplify_ineq(ineq)); + ast rotate_sum_rec(const ast &pl, const ast &pf, ast &Aproves, ast &Bproves, ast &ineq){ + if(pf == pl){ + if(sym(ineq) == normal) + return ineq; + return simplify_ineq(ineq); + } if(op(pf) == Uninterpreted && sym(pf) == sum){ if(arg(pf,2) == pl){ - sum_cond_ineq(ineq,cond,make_int("1"),arg(pf,0)); + sum_cond_ineq(ineq,make_int("1"),arg(pf,0),Aproves,Bproves); ineq = idiv_ineq(ineq,arg(pf,1)); - return my_implies(cond,ineq); + return ineq; } - sum_cond_ineq(ineq,cond,arg(pf,1),arg(pf,2)); - return rotate_sum_rec(pl,arg(pf,0),cond,ineq); + sum_cond_ineq(ineq,arg(pf,1),arg(pf,2),Aproves,Bproves); + return rotate_sum_rec(pl,arg(pf,0),Aproves,Bproves,ineq); } throw cannot_simplify(); } @@ -605,28 +728,30 @@ class iz3proof_itp_impl : public iz3proof_itp { ast equality = arg(neg_equality,0); ast x = arg(equality,0); ast y = arg(equality,1); - ast cond1 = mk_true(); - ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),cond1)); - ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),cond1)); + ast Aproves1 = mk_true(), Bproves1 = mk_true(); + ast xleqy = round_ineq(ineq_from_chain(arg(pf,1),Aproves1,Bproves1)); + ast yleqx = round_ineq(ineq_from_chain(arg(pf,2),Aproves1,Bproves1)); ast ineq1 = make(Leq,make_int("0"),make_int("0")); - sum_cond_ineq(ineq1,cond1,make_int("-1"),xleqy); - sum_cond_ineq(ineq1,cond1,make_int("-1"),yleqx); - cond1 = my_and(cond1,z3_simplify(ineq1)); - ast cond2 = mk_true(); + sum_cond_ineq(ineq1,make_int("-1"),xleqy,Aproves1,Bproves1); + sum_cond_ineq(ineq1,make_int("-1"),yleqx,Aproves1,Bproves1); + Bproves1 = my_and(Bproves1,z3_simplify(ineq1)); + ast Aproves2 = mk_true(), Bproves2 = mk_true(); ast ineq2 = make(Leq,make_int("0"),make_int("0")); - sum_cond_ineq(ineq2,cond2,make_int("1"),xleqy); - sum_cond_ineq(ineq2,cond2,make_int("1"),yleqx); - cond2 = z3_simplify(ineq2); + sum_cond_ineq(ineq2,make_int("1"),xleqy,Aproves2,Bproves2); + sum_cond_ineq(ineq2,make_int("1"),yleqx,Aproves2,Bproves2); + Bproves2 = z3_simplify(ineq2); + if(!is_true(Aproves1) || !is_true(Aproves2)) + throw "help!"; if(get_term_type(x) == LitA){ ast iter = z3_simplify(make(Plus,x,get_ineq_rhs(xleqy))); - ast rewrite1 = make_rewrite(LitA,top_pos,cond1,make(Equal,x,iter)); - ast rewrite2 = make_rewrite(LitB,top_pos,cond2,make(Equal,iter,y)); + ast rewrite1 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,x,iter)); + ast rewrite2 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,iter,y)); return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2); } if(get_term_type(y) == LitA){ ast iter = z3_simplify(make(Plus,y,get_ineq_rhs(yleqx))); - ast rewrite2 = make_rewrite(LitA,top_pos,cond1,make(Equal,iter,y)); - ast rewrite1 = make_rewrite(LitB,top_pos,cond2,make(Equal,x,iter)); + ast rewrite2 = make_rewrite(LitA,top_pos,Bproves1,make(Equal,iter,y)); + ast rewrite1 = make_rewrite(LitB,top_pos,Bproves2,make(Equal,x,iter)); return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2); } throw cannot_simplify(); @@ -643,20 +768,50 @@ class iz3proof_itp_impl : public iz3proof_itp { return res; } + ast unmixed_eq2ineq(const ast &lhs, const ast &rhs, opr comp_op, const ast &equa, ast &cond){ + ast ineqs= chain_ineqs(comp_op,LitA,equa,lhs,rhs); // chain must be from lhs to rhs + cond = my_and(cond,chain_conditions(LitA,equa)); + ast Bconds = z3_simplify(chain_conditions(LitB,equa)); + if(is_true(Bconds) && op(ineqs) != And) + return my_implies(cond,ineqs); + if(op(ineqs) != And) + return my_and(Bconds,my_implies(cond,ineqs)); + throw "help!"; + } + + ast add_mixed_eq2ineq(const ast &lhs, const ast &rhs, const ast &equa, const ast &itp){ + if(is_true(equa)) + return itp; + std::vector args(3); + args[0] = itp; + args[1] = make_int("1"); + ast ineq = make(Leq,make_int(rational(0)),make_int(rational(0))); + args[2] = make_normal(ineq,cons_normal(fix_normal(lhs,rhs,equa),mk_true())); + return simplify_sum(args); + } + ast simplify_rotate_eq2leq(const ast &pl, const ast &neg_equality, const ast &pf){ if(pl == arg(pf,1)){ ast cond = mk_true(); ast equa = sep_cond(arg(pf,0),cond); if(is_equivrel_chain(equa)){ ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove - ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs - cond = my_and(cond,chain_conditions(LitA,equa)); - ast Bconds = chain_conditions(LitB,equa); - if(is_true(Bconds) && op(ineqs) != And) - return my_implies(cond,ineqs); + LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs); + if(lhst != LitMixed && rhst != LitMixed) + return unmixed_eq2ineq(lhs, rhs, op(arg(neg_equality,0)), equa, cond); + else { + ast left, left_term, middle, right_term, right; + left = get_left_movers(equa,lhs,middle,left_term); + middle = get_right_movers(middle,rhs,right,right_term); + ast itp = unmixed_eq2ineq(left_term, right_term, op(arg(neg_equality,0)), middle, cond); + // itp = my_implies(cond,itp); + itp = add_mixed_eq2ineq(lhs, left_term, left, itp); + itp = add_mixed_eq2ineq(right_term, rhs, right, itp); + return itp; + } } } - throw cannot_simplify(); + throw "help!"; } void reverse_modpon(std::vector &args){ @@ -723,6 +878,8 @@ class iz3proof_itp_impl : public iz3proof_itp { ast equa = sep_cond(args[0],cond); if(is_equivrel_chain(equa)) return my_implies(cond,reverse_chain(equa)); + if(is_negation_chain(equa)) + return commute_negation_chain(equa); throw cannot_simplify(); } @@ -757,11 +914,59 @@ class iz3proof_itp_impl : public iz3proof_itp { chain = concat_rewrite_chain(chain,split[1]); } } - else // if not an equivalence, must be of form T <-> pred + else { // if not an equivalence, must be of form T <-> pred chain = concat_rewrite_chain(P,PeqQ); + } return chain; } + void get_subterm_normals(const ast &ineq1, const ast &ineq2, const ast &chain, ast &normals, + const ast &pos, hash_set &memo, ast &Aproves, ast &Bproves){ + opr o1 = op(ineq1); + opr o2 = op(ineq2); + if(o1 == Not || o1 == Leq || o1 == Lt || o1 == Geq || o1 == Gt || o1 == Plus || o1 == Times){ + int n = num_args(ineq1); + if(o2 != o1 || num_args(ineq2) != n) + throw "bad inequality rewriting"; + for(int i = 0; i < n; i++){ + ast new_pos = add_pos_to_end(pos,i); + get_subterm_normals(arg(ineq1,i), arg(ineq2,i), chain, normals, new_pos, memo, Aproves, Bproves); + } + } + else if(get_term_type(ineq2) == LitMixed && memo.find(ineq2) == memo.end()){ + memo.insert(ineq2); + ast sub_chain = extract_rewrites(chain,pos); + if(is_true(sub_chain)) + throw "bad inequality rewriting"; + ast new_normal = make_normal_step(ineq2,ineq1,reverse_chain(sub_chain)); + normals = merge_normal_chains(normals,cons_normal(new_normal,mk_true()), Aproves, Bproves); + } + } + + ast rewrite_chain_to_normal_ineq(const ast &chain, ast &Aproves, ast &Bproves){ + ast tail, pref = get_head_chain(chain,tail,false); // pref is x=y, tail is x=y -> x'=y' + ast head = chain_last(pref); + ast ineq1 = rewrite_rhs(head); + ast ineq2 = apply_rewrite_chain(ineq1,tail); + ast nc = mk_true(); + hash_set memo; + get_subterm_normals(ineq1,ineq2,tail,nc,top_pos,memo, Aproves, Bproves); + ast itp; + if(is_rewrite_side(LitA,head)){ + itp = make(Leq,make_int("0"),make_int("0")); + linear_comb(itp,make_int("1"),ineq1); // make sure it is normal form + //itp = ineq1; + ast mc = z3_simplify(chain_side_proves(LitB,pref)); + Bproves = my_and(Bproves,mc); + } + else { + itp = make(Leq,make_int(rational(0)),make_int(rational(0))); + ast mc = z3_simplify(chain_side_proves(LitA,pref)); + Aproves = my_and(Aproves,mc); + } + return make_normal(itp,nc); + } + /* Given a chain rewrite chain deriving not P and a rewrite chain deriving P, return an interpolant. */ ast contra_chain(const ast &neg_chain, const ast &pos_chain){ // equality is a special case. we use the derivation of x=y to rewrite not(x=y) to not(y=y) @@ -790,11 +995,18 @@ class iz3proof_itp_impl : public iz3proof_itp { } ast simplify_modpon(const std::vector &args){ - ast cond = mk_true(); - ast chain = simplify_modpon_fwd(args,cond); - ast Q2 = sep_cond(args[2],cond); - ast interp = is_negation_chain(chain) ? contra_chain(chain,Q2) : contra_chain(Q2,chain); - return my_implies(cond,interp); + ast Aproves = mk_true(), Bproves = mk_true(); + ast chain = simplify_modpon_fwd(args,Bproves); + ast Q2 = destruct_cond_ineq(args[2],Aproves,Bproves); + ast interp; + if(is_normal_ineq(Q2)){ // inequalities are special + ast nQ2 = rewrite_chain_to_normal_ineq(chain,Aproves,Bproves); + sum_cond_ineq(nQ2,make_int(rational(1)),Q2,Aproves,Bproves); + interp = normalize(nQ2); + } + else + interp = is_negation_chain(chain) ? contra_chain(chain,Q2) : contra_chain(Q2,chain); + return my_and(Aproves,my_implies(Bproves,interp)); } @@ -1035,6 +1247,12 @@ class iz3proof_itp_impl : public iz3proof_itp { return make(add_pos,make_int(rational(arg)),pos); } + ast add_pos_to_end(const ast &pos, int i){ + if(pos == top_pos) + return pos_add(i,pos); + return make(add_pos,arg(pos,0),add_pos_to_end(arg(pos,1),i)); + } + /* return the argument number of position, if not top */ int pos_arg(const ast &pos){ rational r; @@ -1170,6 +1388,10 @@ class iz3proof_itp_impl : public iz3proof_itp { return make(sym(rew),pos_add(apos,arg(rew,0)),arg(rew,1),arg(rew,2)); } + ast rewrite_pos_set(const ast &pos, const ast &rew){ + return make(sym(rew),pos,arg(rew,1),arg(rew,2)); + } + ast rewrite_up(const ast &rew){ return make(sym(rew),arg(arg(rew,0),1),arg(rew,1),arg(rew,2)); } @@ -1274,6 +1496,50 @@ class iz3proof_itp_impl : public iz3proof_itp { return is_negation_chain(rest); } + ast commute_negation_chain(const ast &chain){ + if(is_true(chain)) + return chain; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + if(is_true(rest)){ + ast old = rewrite_rhs(last); + if(!(op(old) == Not)) + throw "bad negative equality chain"; + ast equ = arg(old,0); + if(!is_equivrel(equ)) + throw "bad negative equality chain"; + last = rewrite_update_rhs(last,top_pos,make(Not,make(op(equ),arg(equ,1),arg(equ,0))),make(True)); + return chain_cons(rest,last); + } + ast pos = rewrite_pos(last); + if(pos == top_pos) + throw "bad negative equality chain"; + int idx = pos_arg(pos); + if(idx != 0) + throw "bad negative equality chain"; + pos = arg(pos,1); + if(pos == top_pos){ + ast lhs = rewrite_lhs(last); + ast rhs = rewrite_rhs(last); + if(op(lhs) != Equal || op(rhs) != Equal) + throw "bad negative equality chain"; + last = make_rewrite(rewrite_side(last),rewrite_pos(last),rewrite_cond(last), + make(Iff,make(Equal,arg(lhs,1),arg(lhs,0)),make(Equal,arg(rhs,1),arg(rhs,0)))); + } + else { + idx = pos_arg(pos); + if(idx == 0) + idx = 1; + else if(idx == 1) + idx = 0; + else + throw "bad negative equality chain"; + pos = pos_add(0,pos_add(idx,arg(pos,1))); + last = make_rewrite(rewrite_side(last),pos,rewrite_cond(last),rewrite_equ(last)); + } + return chain_cons(commute_negation_chain(rest),last); + } + // split a rewrite chain into head and tail at last top-level rewrite ast get_head_chain(const ast &chain, ast &tail, bool is_not = true){ ast last = chain_last(chain); @@ -1290,6 +1556,47 @@ class iz3proof_itp_impl : public iz3proof_itp { return head; } + // split a rewrite chain into head and tail at last non-mixed term + ast get_right_movers(const ast &chain, const ast &rhs, ast &tail, ast &mid){ + if(is_true(chain) || get_term_type(rhs) != LitMixed){ + mid = rhs; + tail = mk_true(); + return chain; + } + ast last = chain_last(chain); + ast rest = chain_rest(chain); + ast mm = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last)); + ast res = get_right_movers(rest,mm,tail,mid); + tail = chain_cons(tail,last); + return res; + } + + // split a rewrite chain into head and tail at first non-mixed term + ast get_left_movers(const ast &chain, const ast &lhs, ast &tail, ast &mid){ + if(is_true(chain)){ + mid = lhs; + if(get_term_type(lhs) != LitMixed){ + tail = mk_true(); + return chain; + } + return ast(); + } + ast last = chain_last(chain); + ast rest = chain_rest(chain); + ast res = get_left_movers(rest,lhs,tail,mid); + if(res.null()){ + mid = subst_in_pos(mid,rewrite_pos(last),rewrite_rhs(last)); + if(get_term_type(mid) != LitMixed){ + tail = mk_true(); + return chain; + } + return ast(); + } + tail = chain_cons(tail,last); + return res; + } + + struct cannot_split {}; /** Split a chain of rewrites two chains, operating on positions 0 and 1. @@ -1317,6 +1624,28 @@ class iz3proof_itp_impl : public iz3proof_itp { split_chain_rec(chain,res); } + ast extract_rewrites(const ast &chain, const ast &pos){ + if(is_true(chain)) + return chain; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + ast new_rest = extract_rewrites(rest,pos); + ast p1 = rewrite_pos(last); + ast diff; + switch(pos_diff(p1,pos,diff)){ + case -1: { + ast new_last = rewrite_pos_set(diff, last); + return chain_cons(new_rest,new_last); + } + case 1: + if(rewrite_lhs(last) != rewrite_rhs(last)) + throw "bad rewrite chain"; + break; + default:; + } + return new_rest; + } + ast down_chain(const ast &chain){ ast split[2]; split_chain(chain,split); @@ -1381,7 +1710,7 @@ class iz3proof_itp_impl : public iz3proof_itp { // ast s = ineq_to_lhs(ineq); // ast srhs = arg(s,1); ast srhs = arg(ineq,0); - if(op(srhs) == Plus && num_args(srhs) == 2){ + if(op(srhs) == Plus && num_args(srhs) == 2 && arg(ineq,1) == make_int(rational(0))){ lhs = arg(srhs,0); rhs = arg(srhs,1); // if(op(lhs) == Times) @@ -1393,6 +1722,11 @@ class iz3proof_itp_impl : public iz3proof_itp { return; } } + if(op(ineq) == Leq || op(ineq) == Geq){ + lhs = srhs; + rhs = arg(ineq,1); + return; + } throw "bad ineq"; } @@ -1404,7 +1738,215 @@ class iz3proof_itp_impl : public iz3proof_itp { return chain_cons(rest,last); } + ast apply_rewrite_chain(const ast &t, const ast &chain){ + if(is_true(chain)) + return t; + ast last = chain_last(chain); + ast rest = chain_rest(chain); + ast mid = apply_rewrite_chain(t,rest); + ast res = subst_in_pos(mid,rewrite_pos(last),rewrite_rhs(last)); + return res; + } + ast drop_rewrites(LitType t, const ast &chain, ast &remainder){ + if(!is_true(chain)){ + ast last = chain_last(chain); + ast rest = chain_rest(chain); + if(is_rewrite_side(t,last)){ + ast res = drop_rewrites(t,rest,remainder); + remainder = chain_cons(remainder,last); + return res; + } + } + remainder = mk_true(); + return chain; + } + + // Normalization chains + + ast cons_normal(const ast &first, const ast &rest){ + return make(normal_chain,first,rest); + } + + ast normal_first(const ast &t){ + return arg(t,0); + } + + ast normal_rest(const ast &t){ + return arg(t,1); + } + + ast normal_lhs(const ast &t){ + return arg(arg(t,0),0); + } + + ast normal_rhs(const ast &t){ + return arg(arg(t,0),1); + } + + ast normal_proof(const ast &t){ + return arg(t,1); + } + + ast make_normal_step(const ast &lhs, const ast &rhs, const ast &proof){ + return make(normal_step,make_equiv(lhs,rhs),proof); + } + + ast make_normal(const ast &ineq, const ast &nrml){ + if(!is_ineq(ineq)) + throw "what?"; + return make(normal,ineq,nrml); + } + + ast fix_normal(const ast &lhs, const ast &rhs, const ast &proof){ + LitType lhst = get_term_type(lhs); + LitType rhst = get_term_type(rhs); + if(lhst == LitMixed && (rhst != LitMixed || ast_id(lhs) < ast_id(rhs))) + return make_normal_step(lhs,rhs,proof); + if(rhst == LitMixed && (lhst != LitMixed || ast_id(rhs) < ast_id(lhs))) + return make_normal_step(rhs,lhs,reverse_chain(proof)); + throw "help!"; + } + + ast chain_side_proves(LitType side, const ast &chain){ + LitType other_side = side == LitA ? LitB : LitA; + return my_and(chain_conditions(other_side,chain),my_implies(chain_conditions(side,chain),chain_formulas(side,chain))); + } + + // Merge two normalization chains + ast merge_normal_chains_rec(const ast &chain1, const ast &chain2, hash_map &trans, ast &Aproves, ast &Bproves){ + if(is_true(chain1)) + return chain2; + if(is_true(chain2)) + return chain1; + ast f1 = normal_first(chain1); + ast f2 = normal_first(chain2); + ast lhs1 = normal_lhs(f1); + ast lhs2 = normal_lhs(f2); + int id1 = ast_id(lhs1); + int id2 = ast_id(lhs2); + if(id1 < id2) + return cons_normal(f1,merge_normal_chains_rec(normal_rest(chain1),chain2,trans,Aproves,Bproves)); + if(id2 < id1) + return cons_normal(f2,merge_normal_chains_rec(chain1,normal_rest(chain2),trans,Aproves,Bproves)); + ast rhs1 = normal_rhs(f1); + ast rhs2 = normal_rhs(f2); + LitType t1 = get_term_type(rhs1); + LitType t2 = get_term_type(rhs2); + int tid1 = ast_id(rhs1); + int tid2 = ast_id(rhs2); + ast pf1 = normal_proof(f1); + ast pf2 = normal_proof(f2); + ast new_normal; + if(t1 == LitMixed && (t2 != LitMixed || tid2 > tid1)){ + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + new_normal = f2; + trans[rhs1] = make_normal_step(rhs1,rhs2,new_proof); + } + else if(t2 == LitMixed && (t1 != LitMixed || tid1 > tid2)) + return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves); + else if(t1 == LitA && t2 == LitB){ + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + ast Bproof, Aproof = drop_rewrites(LitB,new_proof,Bproof); + ast mcA = chain_side_proves(LitB,Aproof); + Bproves = my_and(Bproves,mcA); + ast mcB = chain_side_proves(LitA,Bproof); + Aproves = my_and(Aproves,mcB); + ast rep = apply_rewrite_chain(rhs1,Aproof); + new_proof = concat_rewrite_chain(pf1,Aproof); + new_normal = make_normal_step(lhs1,rep,new_proof); + ast A_normal = make_normal_step(rhs1,rep,Aproof); + ast res = cons_normal(new_normal,merge_normal_chains_rec(normal_rest(chain1),normal_rest(chain2),trans,Aproves,Bproves)); + res = merge_normal_chains_rec(res,cons_normal(A_normal,make(True)),trans,Aproves,Bproves); + return res; + } + else if(t1 == LitB && t2 == LitA) + return merge_normal_chains_rec(chain2,chain1,trans,Aproves,Bproves); + else if(t1 == LitA) { + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + ast mc = chain_side_proves(LitB,new_proof); + Bproves = my_and(Bproves,mc); + new_normal = f1; // choice is arbitrary + } + else { /* t1 = t2 = LitB */ + ast new_proof = concat_rewrite_chain(reverse_chain(pf1),pf2); + ast mc = chain_side_proves(LitA,new_proof); + Aproves = my_and(Aproves,mc); + new_normal = f1; // choice is arbitrary + } + return cons_normal(new_normal,merge_normal_chains_rec(normal_rest(chain1),normal_rest(chain2),trans,Aproves,Bproves)); + } + + ast trans_normal_chain(const ast &chain, hash_map &trans){ + if(is_true(chain)) + return chain; + ast f = normal_first(chain); + ast r = normal_rest(chain); + r = trans_normal_chain(r,trans); + ast rhs = normal_rhs(f); + hash_map::iterator it = trans.find(rhs); + ast new_normal; + if(it != trans.end() && get_term_type(normal_lhs(f)) == LitMixed){ + const ast &f2 = it->second; + ast pf = concat_rewrite_chain(normal_proof(f),normal_proof(f2)); + new_normal = make_normal_step(normal_lhs(f),normal_rhs(f2),pf); + } + else + new_normal = f; + if(get_term_type(normal_lhs(f)) == LitMixed) + trans[normal_lhs(f)] = new_normal; + return cons_normal(new_normal,r); + } + + ast merge_normal_chains(const ast &chain1, const ast &chain2, ast &Aproves, ast &Bproves){ + hash_map trans; + ast res = merge_normal_chains_rec(chain1,chain2,trans,Aproves,Bproves); + res = trans_normal_chain(res,trans); + return res; + } + + bool destruct_cond_ineq(ast t, ast &Aproves, ast &Bproves, ast&ineq){ + if(op(t) == And){ + Aproves = arg(t,0); + t = arg(t,1); + } + else + Aproves = mk_true(); + if(op(t) == Implies){ + Bproves = arg(t,0); + t = arg(t,1); + } + else + Bproves = mk_true(); + if(is_normal_ineq(t)){ + ineq = t; + return true; + } + return false; + } + + ast cons_cond_ineq(const ast &Aproves, const ast &Bproves, const ast &ineq){ + return my_and(Aproves,my_implies(Bproves,ineq)); + } + + ast normalize(const ast &ct){ + ast Aproves,Bproves,t; + if(!destruct_cond_ineq(ct,Aproves,Bproves,t)) + return ct; + if(sym(t) != normal) + return ct; + ast chain = arg(t,1); + hash_map map; + for(ast c = chain; !is_true(c); c = normal_rest(c)){ + ast first = normal_first(c); + ast lhs = normal_lhs(first); + ast rhs = normal_rhs(first); + map[lhs] = rhs; + } + ast res = subst(map,arg(t,0)); + return cons_cond_ineq(Aproves,Bproves,res); + } + /** Make an assumption node. The given clause is assumed in the given frame. */ virtual node make_assumption(int frame, const std::vector &assumption){ if(!weak){ @@ -1522,9 +2064,22 @@ class iz3proof_itp_impl : public iz3proof_itp { return itp; } + ast capture_localization(ast e){ + // #define CAPTURE_LOCALIZATION +#ifdef CAPTURE_LOCALIZATION + for(int i = localization_vars.size() - 1; i >= 0; i--){ + LocVar &lv = localization_vars[i]; + if(occurs_in(lv.var,e)){ + symb q = (pv->in_range(lv.frame,rng)) ? sexists : sforall; + e = make(q,make(Equal,lv.var,lv.term),e); // use Equal because it is polymorphic + } + } +#endif + return e; + } + /** Make an axiom node. The conclusion must be an instance of an axiom. */ - virtual node make_axiom(const std::vector &conclusion){ - prover::range frng = pv->range_full(); + virtual node make_axiom(const std::vector &conclusion, prover::range frng){ int nargs = conclusion.size(); std::vector largs(nargs); std::vector eqs; @@ -1546,7 +2101,11 @@ class iz3proof_itp_impl : public iz3proof_itp { for(unsigned i = 0; i < eqs.size(); i++) itp = make_mp(eqs[i],itp,pfs[i]); - return itp; + return capture_localization(itp); + } + + virtual node make_axiom(const std::vector &conclusion){ + return make_axiom(conclusion,pv->range_full()); } /** Make a Contra node. This rule takes a derivation of the form @@ -1594,8 +2153,14 @@ class iz3proof_itp_impl : public iz3proof_itp { /** Make a Reflexivity node. This rule produces |- x = x */ virtual node make_reflexivity(ast con){ - throw proof_error(); -} + if(get_term_type(con) == LitA) + return mk_false(); + if(get_term_type(con) == LitB) + return mk_true(); + ast itp = make(And,make(contra,no_proof,mk_false()), + make(contra,mk_true(),mk_not(con))); + return itp; + } /** Make a Symmetry node. This takes a derivation of |- x = y and produces | y = x. Ditto for ~(x=y) */ @@ -1760,7 +2325,8 @@ class iz3proof_itp_impl : public iz3proof_itp { for(unsigned i = 0; i < prem_cons.size(); i++){ const ast &lit = prem_cons[i]; if(get_term_type(lit) == LitA) - linear_comb(thing,coeffs[i],lit); + // Farkas rule seems to assume strict integer inequalities are rounded + linear_comb(thing,coeffs[i],lit,true /*round_off*/); } thing = simplify_ineq(thing); for(unsigned i = 0; i < prem_cons.size(); i++){ @@ -1785,9 +2351,9 @@ class iz3proof_itp_impl : public iz3proof_itp { /** Set P to P + cQ, where P and Q are linear inequalities. Assumes P is 0 <= y or 0 < y. */ - void linear_comb(ast &P, const ast &c, const ast &Q){ + void linear_comb(ast &P, const ast &c, const ast &Q, bool round_off = false){ ast Qrhs; - bool strict = op(P) == Lt; + bool qstrict = false; if(is_not(Q)){ ast nQ = arg(Q,0); switch(op(nQ)){ @@ -1799,11 +2365,11 @@ class iz3proof_itp_impl : public iz3proof_itp { break; case Geq: Qrhs = make(Sub,arg(nQ,1),arg(nQ,0)); - strict = true; + qstrict = true; break; case Leq: Qrhs = make(Sub,arg(nQ,0),arg(nQ,1)); - strict = true; + qstrict = true; break; default: throw proof_error(); @@ -1819,17 +2385,29 @@ class iz3proof_itp_impl : public iz3proof_itp { break; case Lt: Qrhs = make(Sub,arg(Q,1),arg(Q,0)); - strict = true; + qstrict = true; break; case Gt: Qrhs = make(Sub,arg(Q,0),arg(Q,1)); - strict = true; + qstrict = true; break; default: throw proof_error(); } } +#if 0 + bool pstrict = op(P) == Lt, strict = pstrict || qstrict; + if(pstrict && qstrict && round_off) + Qrhs = make(Sub,Qrhs,make_int(rational(1))); +#else + bool pstrict = op(P) == Lt; + if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){ + Qrhs = make(Sub,Qrhs,make_int(rational(1))); + qstrict = false; + } Qrhs = make(Times,c,Qrhs); + bool strict = pstrict || qstrict; +#endif if(strict) P = make(Lt,arg(P,0),make(Plus,arg(P,1),Qrhs)); else @@ -1848,8 +2426,14 @@ class iz3proof_itp_impl : public iz3proof_itp { itp = mk_true(); break; default: { // mixed equality - if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed) - std::cerr << "WARNING: mixed term in leq2eq\n"; + if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed){ + // std::cerr << "WARNING: mixed term in leq2eq\n"; + std::vector lits; + lits.push_back(con); + lits.push_back(make(Not,xleqy)); + lits.push_back(make(Not,yleqx)); + return make_axiom(lits); + } std::vector conjs; conjs.resize(3); conjs[0] = mk_not(con); conjs[1] = xleqy; @@ -1939,6 +2523,8 @@ class iz3proof_itp_impl : public iz3proof_itp { */ ast make_refl(const ast &e){ + if(get_term_type(e) == LitA) + return mk_false(); return mk_true(); // TODO: is this right? } @@ -1972,7 +2558,8 @@ class iz3proof_itp_impl : public iz3proof_itp { int nargs = num_args(e); if(nargs > 0 /* && (!is_local(e) || flo <= hi || fhi >= lo) */){ prover::range frng = rng; - if(op(e) == Uninterpreted){ + opr o = op(e); + if(o == Uninterpreted){ symb f = sym(e); prover::range srng = pv->sym_range(f); if(pv->ranges_intersect(srng,rng)) // localize to desired range if possible @@ -1980,6 +2567,17 @@ class iz3proof_itp_impl : public iz3proof_itp { else frng = srng; // this term will be localized } + else if(o == Plus || o == Times){ // don't want bound variables inside arith ops + // std::cout << "WARNING: non-local arithmetic\n"; + // frng = erng; // this term will be localized + } + else if(o == Select){ // treat the array term like a function symbol + prover::range srng = pv->ast_scope(arg(e,0)); + if(!(srng.lo > srng.hi) && pv->ranges_intersect(srng,rng)) // localize to desired range if possible + frng = pv->range_glb(srng,rng); + else + frng = srng; // this term will be localized + } std::vector largs(nargs); std::vector eqs; std::vector pfs; @@ -2006,6 +2604,9 @@ class iz3proof_itp_impl : public iz3proof_itp { if(pv->ranges_intersect(pv->ast_scope(e),rng)) return e; // this term occurs in range, so it's O.K. + if(is_array_type(get_type(e))) + std::cerr << "WARNING: array quantifier\n"; + // choose a frame for the constraint that is close to range int frame = pv->range_near(pv->ast_scope(e),rng); @@ -2018,12 +2619,89 @@ class iz3proof_itp_impl : public iz3proof_itp { return new_var; } + ast delete_quant(hash_map &memo, const ast &v, const ast &e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + opr o = op(e); + switch(o){ + case Or: + case And: + case Implies: { + unsigned nargs = num_args(e); + std::vector args; args.resize(nargs); + for(unsigned i = 0; i < nargs; i++) + args[i] = delete_quant(memo, v, arg(e,i)); + res = make(o,args); + break; + } + case Uninterpreted: { + symb s = sym(e); + ast w = arg(arg(e,0),0); + if(s == sforall || s == sexists){ + res = delete_quant(memo,v,arg(e,1)); + if(w != v) + res = make(s,w,res); + break; + } + } + default: + res = e; + } + } + return res; + } + + ast insert_quants(hash_map &memo, const ast &e){ + std::pair foo(e,ast()); + std::pair::iterator,bool> bar = memo.insert(foo); + ast &res = bar.first->second; + if(bar.second){ + opr o = op(e); + switch(o){ + case Or: + case And: + case Implies: { + unsigned nargs = num_args(e); + std::vector args; args.resize(nargs); + for(unsigned i = 0; i < nargs; i++) + args[i] = insert_quants(memo, arg(e,i)); + res = make(o,args); + break; + } + case Uninterpreted: { + symb s = sym(e); + if(s == sforall || s == sexists){ + opr q = (s == sforall) ? Forall : Exists; + ast v = arg(arg(e,0),0); + hash_map dmemo; + ast body = delete_quant(dmemo,v,arg(e,1)); + body = insert_quants(memo,body); + res = apply_quant(q,v,body); + break; + } + } + default: + res = e; + } + } + return res; + } + ast add_quants(ast e){ +#ifdef CAPTURE_LOCALIZATION + if(!localization_vars.empty()){ + hash_map memo; + e = insert_quants(memo,e); + } +#else for(int i = localization_vars.size() - 1; i >= 0; i--){ LocVar &lv = localization_vars[i]; opr quantifier = (pv->in_range(lv.frame,rng)) ? Exists : Forall; e = apply_quant(quantifier,lv.var,e); } +#endif return e; } @@ -2035,7 +2713,11 @@ class iz3proof_itp_impl : public iz3proof_itp { /* Return an interpolant from a proof of false */ ast interpolate(const node &pf){ // proof of false must be a formula, with quantified symbols +#ifndef BOGUS_QUANTS return add_quants(z3_simplify(pf)); +#else + return z3_simplify(pf); +#endif } ast resolve_with_quantifier(const ast &pivot1, const ast &conj1, @@ -2055,7 +2737,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast npP = make_mp(make(Iff,nPloc,nP),npPloc,neqpf); ast nrP = make_resolution(nP,conj2,npP); ast res = make_resolution(Ploc,rP,nrP); - return res; + return capture_localization(res); } ast get_contra_coeff(const ast &f){ @@ -2141,6 +2823,16 @@ public: m().inc_ref(rewrite_A); rewrite_B = function("@rewrite_B",3,boolboolbooldom,bool_type()); m().inc_ref(rewrite_B); + normal_step = function("@normal_step",2,boolbooldom,bool_type()); + m().inc_ref(normal_step); + normal_chain = function("@normal_chain",2,boolbooldom,bool_type()); + m().inc_ref(normal_chain); + normal = function("@normal",2,boolbooldom,bool_type()); + m().inc_ref(normal); + sforall = function("@sforall",2,boolbooldom,bool_type()); + m().inc_ref(sforall); + sexists = function("@sexists",2,boolbooldom,bool_type()); + m().inc_ref(sexists); } ~iz3proof_itp_impl(){ diff --git a/src/interp/iz3proof_itp.h b/src/interp/iz3proof_itp.h index 299f391ea..4d76e3a92 100644 --- a/src/interp/iz3proof_itp.h +++ b/src/interp/iz3proof_itp.h @@ -70,6 +70,9 @@ class iz3proof_itp : public iz3mgr { /** Make an axiom node. The conclusion must be an instance of an axiom. */ virtual node make_axiom(const std::vector &conclusion) = 0; + /** Make an axiom node. The conclusion must be an instance of an axiom. Localize axiom instance to range*/ + virtual node make_axiom(const std::vector &conclusion, prover::range) = 0; + /** Make a Contra node. This rule takes a derivation of the form Gamma |- False and produces |- \/~Gamma. */ diff --git a/src/interp/iz3scopes.cpp b/src/interp/iz3scopes.cpp index 382779be0..198ecffe3 100755 --- a/src/interp/iz3scopes.cpp +++ b/src/interp/iz3scopes.cpp @@ -19,6 +19,8 @@ Revision History: #include +#include + #include "iz3scopes.h" diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 4ea755eff..9eac5f040 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -17,6 +17,13 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif + #include "iz3translate.h" #include "iz3proof.h" #include "iz3profiling.h" @@ -109,36 +116,49 @@ public: symbols and assign each to a frame. THe assignment is heuristic. */ - void scan_skolems_rec(hash_set &memo, const ast &proof){ - std::pair::iterator,bool> bar = memo.insert(proof); - if(!bar.second) - return; + int scan_skolems_rec(hash_map &memo, const ast &proof, int frame){ + std::pair foo(proof,INT_MAX); + std::pair bar = memo.insert(foo); + int &res = bar.first->second; + if(!bar.second) return res; pfrule dk = pr(proof); - if(dk == PR_SKOLEMIZE){ + if(dk == PR_ASSERTED){ + ast ass = conc(proof); + res = frame_of_assertion(ass); + } + else if(dk == PR_SKOLEMIZE){ ast quanted = arg(conc(proof),0); if(op(quanted) == Not) quanted = arg(quanted,0); - range r = ast_range(quanted); - if(range_is_empty(r)) - r = ast_scope(quanted); + // range r = ast_range(quanted); + // if(range_is_empty(r)) + range r = ast_scope(quanted); if(range_is_empty(r)) throw "can't skolemize"; - int frame = range_max(r); + if(frame == INT_MAX || !in_range(frame,r)) + frame = range_max(r); // this is desperation -- may fail if(frame >= frames) frame = frames - 1; add_frame_range(frame,arg(conc(proof),1)); r = ast_scope(arg(conc(proof),1)); } + else if(dk==PR_MODUS_PONENS_OEQ){ + frame = scan_skolems_rec(memo,prem(proof,0),frame); + scan_skolems_rec(memo,prem(proof,1),frame); + } else { unsigned nprems = num_prems(proof); for(unsigned i = 0; i < nprems; i++){ - scan_skolems_rec(memo,prem(proof,i)); + int bar = scan_skolems_rec(memo,prem(proof,i),frame); + if(res == INT_MAX || res == bar) res = bar; + else if(bar != INT_MAX) res = -1; } } + return res; } void scan_skolems(const ast &proof){ - hash_set memo; - scan_skolems_rec(memo,proof); + hash_map memo; + scan_skolems_rec(memo,proof, INT_MAX); } // determine locality of a proof term @@ -168,6 +188,15 @@ public: get_Z3_lits(con, lits); iproof->make_axiom(lits); } +#ifdef LOCALIZATION_KLUDGE + else if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST + && get_locality_rec(prem(proof,1)) == INT_MAX){ + std::vector lits; + ast con = conc(proof); + get_Z3_lits(con, lits); + iproof->make_axiom(lits); + } +#endif else { unsigned nprems = num_prems(proof); for(unsigned i = 0; i < nprems; i++){ @@ -1066,7 +1095,7 @@ public: my_cons.push_back(mk_not(arg(con,i))); my_coeffs.push_back(farkas_coeffs[i]); } - ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons)); + ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons,true /* round_off */)); my_cons.push_back(mk_not(farkas_con)); my_coeffs.push_back(make_int("1")); std::vector my_hyps; @@ -1090,7 +1119,7 @@ public: my_cons.push_back(conc(prem(proof,i-1))); my_coeffs.push_back(farkas_coeffs[i]); } - ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons)); + ast farkas_con = normalize_inequality(sum_inequalities(my_coeffs,my_cons,true /* round_off */)); std::vector my_hyps; for(int i = 1; i < nargs; i++) my_hyps.push_back(prems[i-1]); @@ -1251,6 +1280,84 @@ public: return make(Plus,args); } + + ast replace_summands_with_fresh_vars(const ast &t, hash_map &map){ + if(op(t) == Plus){ + int nargs = num_args(t); + std::vector args(nargs); + for(int i = 0; i < nargs; i++) + args[i] = replace_summands_with_fresh_vars(arg(t,i),map); + return make(Plus,args); + } + if(op(t) == Times) + return make(Times,arg(t,0),replace_summands_with_fresh_vars(arg(t,1),map)); + if(map.find(t) == map.end()) + map[t] = mk_fresh_constant("@s",get_type(t)); + return map[t]; + } + + ast painfully_normalize_ineq(const ast &ineq, hash_map &map){ + ast res = normalize_inequality(ineq); + ast lhs = arg(res,0); + lhs = replace_summands_with_fresh_vars(lhs,map); + res = make(op(res),SortSum(lhs),arg(res,1)); + return res; + } + + Iproof::node painfully_reconstruct_farkas(const std::vector &prems, const std::vector &pfs, const ast &con){ + int nprems = prems.size(); + std::vector pcons(nprems),npcons(nprems); + hash_map pcon_to_pf, npcon_to_pcon, pain_map; + for(int i = 0; i < nprems; i++){ + pcons[i] = conc(prems[i]); + npcons[i] = painfully_normalize_ineq(pcons[i],pain_map); + pcon_to_pf[npcons[i]] = pfs[i]; + npcon_to_pcon[npcons[i]] = pcons[i]; + } + // ast leq = make(Leq,arg(con,0),arg(con,1)); + ast ncon = painfully_normalize_ineq(mk_not(con),pain_map); + pcons.push_back(mk_not(con)); + npcons.push_back(ncon); + // ast assumps = make(And,pcons); + ast new_proof; + if(is_sat(npcons,new_proof)) + throw "Proof error!"; + pfrule dk = pr(new_proof); + int nnp = num_prems(new_proof); + std::vector my_prems; + std::vector farkas_coeffs, my_pcons; + + if(dk == PR_TH_LEMMA + && get_theory_lemma_theory(new_proof) == ArithTheory + && get_theory_lemma_kind(new_proof) == FarkasKind) + get_farkas_coeffs(new_proof,farkas_coeffs); + else if(dk == PR_UNIT_RESOLUTION && nnp == 2){ + for(int i = 0; i < nprems; i++) + farkas_coeffs.push_back(make_int(rational(1))); + } + else + throw "cannot reconstruct farkas proof"; + + for(int i = 0; i < nnp; i++){ + ast p = conc(prem(new_proof,i)); + p = really_normalize_ineq(p); + if(pcon_to_pf.find(p) != pcon_to_pf.end()){ + my_prems.push_back(pcon_to_pf[p]); + my_pcons.push_back(npcon_to_pcon[p]); + } + else if(p == ncon){ + my_prems.push_back(iproof->make_hypothesis(mk_not(con))); + my_pcons.push_back(mk_not(con)); + } + else + throw "cannot reconstruct farkas proof"; + } + Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs); + return res; + } + + + ast really_normalize_ineq(const ast &ineq){ ast res = normalize_inequality(ineq); res = make(op(res),SortSum(arg(res,0)),arg(res,1)); @@ -1289,7 +1396,7 @@ public: farkas_coeffs.push_back(make_int(rational(1))); } else - throw "cannot reconstruct farkas proof"; + return painfully_reconstruct_farkas(prems,pfs,con); for(int i = 0; i < nnp; i++){ ast p = conc(prem(new_proof,i)); @@ -1364,6 +1471,18 @@ public: return eq2; } + bool get_store_array(const ast &t, ast &res){ + if(op(t) == Store){ + res = t; + return true; + } + int nargs = num_args(t); + for(int i = 0; i < nargs; i++) + if(get_store_array(arg(t,i),res)) + return true; + return false; + } + // translate a Z3 proof term into interpolating proof system Iproof::node translate_main(ast proof, bool expect_clause = true){ @@ -1420,9 +1539,11 @@ public: lits.push_back(from_ast(con)); // pattern match some idioms - if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST && pr(prem(proof,1)) == PR_REWRITE ) { - res = iproof->make_axiom(lits); - return res; + if(dk == PR_MODUS_PONENS && pr(prem(proof,0)) == PR_QUANT_INST){ + if(get_locality_rec(prem(proof,1)) == INT_MAX) { + res = iproof->make_axiom(lits); + return res; + } } if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or){ Iproof::node clause = translate_main(prem(proof,0),true); @@ -1433,12 +1554,20 @@ public: if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or) std::cout << "foo!\n"; +#if 0 if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){ Iproof::node clause = translate_main(prem(proof,0),true); res = make(commute,clause,conc(prem(proof,0))); // HACK -- we depend on Iproof::node being same as ast. return res; } + if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,0)) == PR_COMMUTATIVITY){ + Iproof::node clause = translate_main(prem(proof,1),true); + res = make(commute,clause,conc(prem(proof,1))); // HACK -- we depend on Iproof::node being same as ast. + return res; + } +#endif + if(dk == PR_TRANSITIVITY && is_eq_propagate(prem(proof,1))){ try { res = CombineEqPropagate(proof); @@ -1448,6 +1577,21 @@ public: } } + /* this is the symmetry rule for ~=, that is, takes x ~= y and yields y ~= x. + the proof idiom uses commutativity, monotonicity and mp, but we replace it here + with symmtrey and resolution, that is, we prove y = x |- x = y, then resolve + with the proof of ~(x=y) to get ~y=x. */ + if(dk == PR_MODUS_PONENS && pr(prem(proof,1)) == PR_MONOTONICITY && pr(prem(prem(proof,1),0)) == PR_COMMUTATIVITY && num_prems(prem(proof,1)) == 1){ + Iproof::node ante = translate_main(prem(proof,0),false); + ast eq0 = arg(conc(prem(prem(proof,1),0)),0); + ast eq1 = arg(conc(prem(prem(proof,1),0)),1); + Iproof::node eq1hy = iproof->make_hypothesis(eq1); + Iproof::node eq0pf = iproof->make_symmetry(eq0,eq1,eq1hy); + std::vector clause; // just a dummy + res = iproof->make_resolution(eq0,clause,ante,eq0pf); + return res; + } + // translate all the premises std::vector args(nprems); for(unsigned i = 0; i < nprems; i++) @@ -1578,9 +1722,14 @@ public: throw unsupported(); } break; - case ArrayTheory: // nothing fancy for this - res = iproof->make_axiom(lits); + case ArrayTheory: {// nothing fancy for this + ast store_array; + if(get_store_array(con,store_array)) + res = iproof->make_axiom(lits,ast_scope(store_array)); + else + res = iproof->make_axiom(lits); // for array extensionality axiom break; + } default: throw unsupported(); } @@ -1598,6 +1747,16 @@ public: res = iproof->make_axiom(lits); break; } + case PR_IFF_TRUE: { // turns p into p <-> true, noop for us + res = args[0]; + break; + } + case PR_COMMUTATIVITY: { + ast comm_equiv = make(op(con),arg(con,0),arg(con,0)); + ast pf = iproof->make_reflexivity(comm_equiv); + res = make(commute,pf,comm_equiv); + break; + } default: assert(0 && "translate_main: unsupported proof rule"); throw unsupported(); diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index 853ecbe86..a85c9a1c5 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -20,6 +20,14 @@ Revision History: --*/ +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#pragma warning(disable:4390) +#endif + #include "iz3translate.h" #include "iz3proof.h" #include "iz3profiling.h" @@ -38,9 +46,29 @@ Revision History: using namespace stl_ext; #endif +#ifndef WIN32 + +/* This can introduce an address dependency if the range type of hash_map has + a destructor. Since the code in this file is not used and only here for + historical comparisons, we allow this non-determinism. + */ +namespace stl_ext { + template + class hash { + public: + size_t operator()(const T *p) const { + return (size_t) p; + } + }; +} + +#endif + static int lemma_count = 0; +#if 0 static int nll_lemma_count = 0; +#endif #define SHOW_LEMMA_COUNT -1 // One half of a resolution. We need this to distinguish diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp old mode 100644 new mode 100755 index 25dfcebbd..248aca163 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -35,10 +35,15 @@ Revision History: #include "model_smt2_pp.h" #include "model_v2_pp.h" #include "fixedpoint_params.hpp" -#include "scoped_proof.h" // template class symbol_table; +#ifdef WIN32 +#pragma warning(disable:4996) +#pragma warning(disable:4800) +#pragma warning(disable:4267) +#pragma warning(disable:4101) +#endif #include "duality.h" #include "duality_profiling.h" @@ -213,6 +218,9 @@ lbool dl_interface::query(::expr * query) { catch (Duality::solver::cancel_exception &exn){ throw default_exception("duality canceled"); } + catch (Duality::Solver::Incompleteness &exn){ + throw default_exception("incompleteness"); + } // profile! @@ -472,7 +480,7 @@ static proof_ref extract_proof(dl_interface *d, Solver::Counterexample &cex) { expr conc = f(args); - ::vector pprems; + ::vector< ::proof *> pprems; for(unsigned i = 0; i < prems.size(); i++) pprems.push_back(prems[i].get()); diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index 3e933b099..d9dad5c56 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -527,6 +527,9 @@ namespace datalog { bool mk_rule_inliner::do_eager_inlining(rule * r, rule_set const& rules, rule_ref& res) { + if (r->has_negation()) { + return false; + } SASSERT(rules.is_closed()); const rule_stratifier& strat = rules.get_stratifier(); diff --git a/src/smt/params/qi_params.cpp b/src/smt/params/qi_params.cpp index f5506d35b..60fcd6fc4 100644 --- a/src/smt/params/qi_params.cpp +++ b/src/smt/params/qi_params.cpp @@ -27,6 +27,7 @@ void qi_params::updt_params(params_ref const & _p) { m_mbqi_max_iterations = p.mbqi_max_iterations(); m_mbqi_trace = p.mbqi_trace(); m_mbqi_force_template = p.mbqi_force_template(); + m_mbqi_id = p.mbqi_id(); m_qi_profile = p.qi_profile(); m_qi_profile_freq = p.qi_profile_freq(); m_qi_max_instances = p.qi_max_instances(); diff --git a/src/smt/params/qi_params.h b/src/smt/params/qi_params.h index 0cd817f22..bca3ad3fc 100644 --- a/src/smt/params/qi_params.h +++ b/src/smt/params/qi_params.h @@ -51,6 +51,7 @@ struct qi_params { unsigned m_mbqi_max_iterations; bool m_mbqi_trace; unsigned m_mbqi_force_template; + const char * m_mbqi_id; qi_params(params_ref const & p = params_ref()): /* @@ -97,7 +98,9 @@ struct qi_params { m_mbqi_max_cexs_incr(1), m_mbqi_max_iterations(1000), m_mbqi_trace(false), - m_mbqi_force_template(10) { + m_mbqi_force_template(10), + m_mbqi_id(0) + { updt_params(p); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 07c68f759..50bb6422b 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -21,6 +21,7 @@ def_module_params(module_name='smt', ('mbqi.max_iterations', UINT, 1000, 'maximum number of rounds of MBQI'), ('mbqi.trace', BOOL, False, 'generate tracing messages for Model Based Quantifier Instantiation (MBQI). It will display a message before every round of MBQI, and the quantifiers that were not satisfied'), ('mbqi.force_template', UINT, 10, 'some quantifiers can be used as templates for building interpretations for functions. Z3 uses heuristics to decide whether a quantifier will be used as a template or not. Quantifiers with weight >= mbqi.force_template are forced to be used as a template'), + ('mbqi.id', STRING, '', 'Only use model-based instantiation for quantifiers with id\'s beginning with string'), ('qi.profile', BOOL, False, 'profile quantifier instantiation'), ('qi.profile_freq', UINT, UINT_MAX, 'how frequent results are reported by qi.profile'), ('qi.max_instances', UINT, UINT_MAX, 'maximum number of quantifier instantiations'), diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index d34aa2ec8..ec62efa1c 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -759,7 +759,8 @@ namespace smt { app * fact = to_app(m_manager.get_fact(pr)); app * n1_owner = n1->get_owner(); app * n2_owner = n2->get_owner(); - if (fact->get_num_args() != 2 || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) { + bool is_eq = m_manager.is_eq(fact) || m_manager.is_iff(fact); + if (!is_eq || (fact->get_arg(0) != n2_owner && fact->get_arg(1) != n2_owner)) { CTRACE("norm_eq_proof_bug", !m_ctx.is_true(n2) && !m_ctx.is_false(n2), tout << "n1: #" << n1->get_owner_id() << ", n2: #" << n2->get_owner_id() << "\n"; if (fact->get_num_args() == 2) { diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 53f3af961..526447f9f 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -322,6 +322,7 @@ namespace smt { for (; it != end; ++it) { quantifier * q = *it; + if(!m_qm->mbqi_enabled(q)) continue; if (m_context->is_relevant(q) && m_context->get_assignment(q) == l_true) { if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) { verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n"; diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index d56fe0cff..8fd0e08bc 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -335,6 +335,10 @@ namespace smt { return m_imp->m_plugin->model_based(); } + bool quantifier_manager::mbqi_enabled(quantifier *q) const { + return m_imp->m_plugin->mbqi_enabled(q); + } + void quantifier_manager::adjust_model(proto_model * m) { m_imp->m_plugin->adjust_model(m); } @@ -434,10 +438,24 @@ namespace smt { virtual bool model_based() const { return m_fparams->m_mbqi; } + virtual bool mbqi_enabled(quantifier *q) const { + if(!m_fparams->m_mbqi_id) return true; + const symbol &s = q->get_qid(); + unsigned len = strlen(m_fparams->m_mbqi_id); + if(s == symbol::null || s.is_numerical()) + return len == 0; + return strncmp(s.bare_str(),m_fparams->m_mbqi_id,len) == 0; + } + + /* Quantifier id's must begin with the prefix specified by + parameter mbqi.id to be instantiated with MBQI. The default + value is the empty string, so all quantifiers are + instantiated. + */ virtual void add(quantifier * q) { - if (m_fparams->m_mbqi) { - m_model_finder->register_quantifier(q); - } + if (m_fparams->m_mbqi && mbqi_enabled(q)) { + m_model_finder->register_quantifier(q); + } } virtual void del(quantifier * q) { diff --git a/src/smt/smt_quantifier.h b/src/smt/smt_quantifier.h index 19113229c..e3d626157 100644 --- a/src/smt/smt_quantifier.h +++ b/src/smt/smt_quantifier.h @@ -75,6 +75,7 @@ namespace smt { }; bool model_based() const; + bool mbqi_enabled(quantifier *q) const; // can mbqi instantiate this quantifier? void adjust_model(proto_model * m); check_model_result check_model(proto_model * m, obj_map const & root2value); @@ -144,6 +145,11 @@ namespace smt { */ virtual bool model_based() const = 0; + /** + \brief Is "model based" instantiate allowed to instantiate this quantifier? + */ + virtual bool mbqi_enabled(quantifier *q) const {return true;} + /** \brief Give a change to the plugin to adjust the interpretation of unintepreted functions. It can basically change the "else" of each uninterpreted function. diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index 9f77934e5..21b892e57 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -475,10 +475,11 @@ namespace smt { bool theory_arith::all_coeff_int(row const & r) const { typename vector::const_iterator it = r.begin_entries(); typename vector::const_iterator end = r.end_entries(); - for (; it != end; ++it) { - if (!it->is_dead() && !it->m_coeff.is_int()) + for (; it != end; ++it) { + if (!it->is_dead() && !it->m_coeff.is_int()) TRACE("gomory_cut", display_row(tout, r, true);); return false; + } return true; } diff --git a/src/tactic/arith/lia2pb_tactic.cpp b/src/tactic/arith/lia2pb_tactic.cpp index 6fee55e4b..9ee8f6728 100644 --- a/src/tactic/arith/lia2pb_tactic.cpp +++ b/src/tactic/arith/lia2pb_tactic.cpp @@ -71,6 +71,7 @@ class lia2pb_tactic : public tactic { if (m_bm.has_lower(n, l, s) && m_bm.has_upper(n, u, s) && l.is_zero() && + !u.is_neg() && u.get_num_bits() <= m_max_bits) { return true; diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index ebccf4d52..2d1d6705f 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -1368,12 +1368,12 @@ void fpa2bv_converter::mk_fusedma(func_decl * f, unsigned num, expr * const * ar not_e_sgn = m_bv_util.mk_bv_not(e_sgn); not_f_sgn = m_bv_util.mk_bv_not(f_sgn); not_sign_bv = m_bv_util.mk_bv_not(sign_bv); - res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, e_sgn, sign_bv); + res_sgn_c1 = m.mk_app(bvfid, OP_BAND, not_e_sgn, f_sgn, sign_bv); res_sgn_c2 = m.mk_app(bvfid, OP_BAND, e_sgn, not_f_sgn, not_sign_bv); res_sgn_c3 = m.mk_app(bvfid, OP_BAND, e_sgn, f_sgn); expr * res_sgn_or_args[3] = { res_sgn_c1, res_sgn_c2, res_sgn_c3 }; res_sgn = m_bv_util.mk_bv_or(3, res_sgn_or_args); - + sticky_raw = m_bv_util.mk_extract(sbits-5, 0, sig_abs); sticky = m_bv_util.mk_zero_extend(sbits+3, m.mk_app(bvfid, OP_BREDOR, sticky_raw.get())); dbg_decouple("fpa2bv_fma_add_sum_sticky", sticky); @@ -1836,6 +1836,21 @@ void fpa2bv_converter::mk_to_float(func_decl * f, unsigned num, expr * const * a // Just keep it here, as there will be something else that uses it. mk_triple(args[0], args[1], args[2], result); } + else if (num == 1 && m_bv_util.is_bv(args[0])) { + sort * s = f->get_range(); + unsigned to_sbits = m_util.get_sbits(s); + unsigned to_ebits = m_util.get_ebits(s); + + expr * bv = args[0]; + int sz = m_bv_util.get_bv_size(bv); + SASSERT((unsigned)sz == to_sbits + to_ebits); + + m_bv_util.mk_extract(sz - 1, sz - 1, bv); + mk_triple(m_bv_util.mk_extract(sz - 1, sz - 1, bv), + m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv), + m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv), + result); + } else if (num == 2 && is_app(args[1]) && m_util.is_float(m.get_sort(args[1]))) { // We also support float to float conversion sort * s = f->get_range(); @@ -2043,6 +2058,27 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * result = m_bv_util.mk_concat(m_bv_util.mk_concat(sgn, e), s); } +void fpa2bv_converter::mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + SASSERT(num == 3); + mk_triple(args[0], args[2], args[1], result); +} + +void fpa2bv_converter::mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + +void fpa2bv_converter::mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result) { + NOT_IMPLEMENTED_YET(); +} + void fpa2bv_converter::split(expr * e, expr * & sgn, expr * & sig, expr * & exp) const { SASSERT(is_app_of(e, m_plugin->get_family_id(), OP_TO_FLOAT)); SASSERT(to_app(e)->get_num_args() == 3); diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/tactic/fpa/fpa2bv_converter.h index 821618bae..79c8039ef 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/tactic/fpa/fpa2bv_converter.h @@ -122,7 +122,13 @@ public: void mk_is_subnormal(func_decl * f, unsigned num, expr * const * args, expr_ref & result); void mk_to_float(func_decl * f, unsigned num, expr * const * args, expr_ref & result); - void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ieee_bv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + + void mk_fp(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_fp_unsigned(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_ubv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_sbv(func_decl * f, unsigned num, expr * const * args, expr_ref & result); + void mk_to_real(func_decl * f, unsigned num, expr * const * args, expr_ref & result); obj_map const & const2bv() const { return m_const2bv; } obj_map const & rm_const2bv() const { return m_rm_const2bv; } diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/tactic/fpa/fpa2bv_rewriter.h index d737683a8..b2e3da939 100644 --- a/src/tactic/fpa/fpa2bv_rewriter.h +++ b/src/tactic/fpa/fpa2bv_rewriter.h @@ -139,6 +139,11 @@ struct fpa2bv_rewriter_cfg : public default_rewriter_cfg { case OP_FLOAT_IS_SIGN_MINUS: m_conv.mk_is_sign_minus(f, num, args, result); return BR_DONE; case OP_TO_FLOAT: m_conv.mk_to_float(f, num, args, result); return BR_DONE; case OP_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; + case OP_FLOAT_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; + case OP_FLOAT_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index f3c913ccc..f9b7f88a1 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -36,3 +36,81 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p) { mk_sat_tactic(m, p), mk_fail_if_undecided_tactic()); } + +struct is_non_qffpa_predicate { + struct found {}; + ast_manager & m; + float_util u; + + is_non_qffpa_predicate(ast_manager & _m) : m(_m), u(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (!m.is_bool(s) && !u.is_float(s) && !u.is_rm(s)) + throw found(); + family_id fid = n->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == u.get_family_id()) + return; + if (is_uninterp_const(n)) + return; + + throw found(); + } +}; + +struct is_non_qffpabv_predicate { + struct found {}; + ast_manager & m; + bv_util bu; + float_util fu; + + is_non_qffpabv_predicate(ast_manager & _m) : m(_m), bu(m), fu(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s)) + throw found(); + family_id fid = n->get_family_id(); + if (fid == m.get_basic_family_id()) + return; + if (fid == fu.get_family_id() || fid == bu.get_family_id()) + return; + if (is_uninterp_const(n)) + return; + + throw found(); + } +}; + +class is_qffpa_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } +}; + +class is_qffpabv_probe : public probe { +public: + virtual result operator()(goal const & g) { + return !test(g); + } +}; + +probe * mk_is_qffpa_probe() { + return alloc(is_qffpa_probe); +} + +probe * mk_is_qffpabv_probe() { + return alloc(is_qffpabv_probe); +} + \ No newline at end of file diff --git a/src/tactic/fpa/qffpa_tactic.h b/src/tactic/fpa/qffpa_tactic.h index 8ca2183c1..cd16c5817 100644 --- a/src/tactic/fpa/qffpa_tactic.h +++ b/src/tactic/fpa/qffpa_tactic.h @@ -30,4 +30,11 @@ tactic * mk_qffpa_tactic(ast_manager & m, params_ref const & p = params_ref()); ADD_TACTIC("qffpabv", "(try to) solve goal using the tactic for QF_FPABV (floats+bit-vectors).", "mk_qffpa_tactic(m, p)") */ +probe * mk_is_qffpa_probe(); +probe * mk_is_qffpabv_probe(); +/* + ADD_PROBE("is-qffpa", "true if the goal is in QF_FPA (FloatingPoints).", "mk_is_qffpa_probe()") + ADD_PROBE("is-qffpabv", "true if the goal is in QF_FPABV (FloatingPoints+Bitvectors).", "mk_is_qffpabv_probe()") +*/ + #endif diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index d65ba8d35..9ecc16ecf 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -27,6 +27,7 @@ Notes: #include"nra_tactic.h" #include"probe_arith.h" #include"quant_tactics.h" +#include"qffpa_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), @@ -37,7 +38,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m), cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_lira_probe(), mk_lira_tactic(m, p), - mk_smt_tactic())))))))), + cond(mk_is_qffpabv_probe(), mk_qffpa_tactic(m, p), + mk_smt_tactic()))))))))), p); return st; } diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 8585e7eda..40d20b644 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -49,8 +49,11 @@ Revision History: // clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects // the x87 FPU, even when /arch:SSE2 is on. // Luckily, these are kind of standardized, at least for Windows/Linux/OSX. +#ifdef __clang__ +#undef USE_INTRINSICS +#else #include - +#endif hwf_manager::hwf_manager() : m_mpz_manager(m_mpq_manager) diff --git a/src/util/id_gen.h b/src/util/id_gen.h index b1713b524..c6d22246d 100644 --- a/src/util/id_gen.h +++ b/src/util/id_gen.h @@ -57,6 +57,11 @@ public: m_free_ids.finalize(); } + unsigned show_hash(){ + unsigned h = string_hash((char *)&m_free_ids[0],m_free_ids.size()*sizeof(unsigned),17); + return hash_u_u(h,m_next_id); + } + /** \brief Return N if the range of ids generated by this module is in the set [0..N) */ diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 5910f55c9..8cb6ed4fc 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -1400,6 +1400,10 @@ mpf_exp_t mpf_manager::mk_max_exp(unsigned ebits) { return m_mpz_manager.get_int64(m_powers2.m1(ebits-1, false)); } +mpf_exp_t mpf_manager::unbias_exp(unsigned ebits, mpf_exp_t biased_exponent) { + return biased_exponent - m_mpz_manager.get_int64(m_powers2.m1(ebits - 1, false)); +} + void mpf_manager::mk_nzero(unsigned ebits, unsigned sbits, mpf & o) { o.sbits = sbits; o.ebits = ebits; diff --git a/src/util/mpf.h b/src/util/mpf.h index 284b0ba7f..83646f9f3 100644 --- a/src/util/mpf.h +++ b/src/util/mpf.h @@ -182,6 +182,8 @@ public: mpf_exp_t mk_max_exp(unsigned ebits); mpf_exp_t mk_min_exp(unsigned ebits); + mpf_exp_t unbias_exp(unsigned ebits, mpf_exp_t biased_exponent); + /** \brief Return the biggest k s.t. 2^k <= a. diff --git a/src/util/rational.h b/src/util/rational.h index fc03228bf..c02a5a2c3 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -104,7 +104,7 @@ public: } bool is_int32() const { - if (is_small()) return true; + if (is_small() && is_int()) return true; // we don't assume that if it is small, then it is int32. if (!is_int64()) return false; int64 v = get_int64();