diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 2fff61778..883492614 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -639,8 +639,8 @@ def is_CXX_gpp(): return is_compiler(CXX, 'g++') def is_clang_in_gpp_form(cc): - version_string = subprocess.check_output([cc, '--version']) - return version_string.find('clang') != -1 + version_string = check_output([cc, '--version']) + return str(version_string).find('clang') != -1 def is_CXX_clangpp(): if is_compiler(CXX, 'g++'): @@ -1198,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, @@ -1437,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) @@ -1485,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() @@ -1508,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) @@ -1536,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: @@ -1586,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/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_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 1ad2b8222..77c8ac58f 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -472,6 +472,25 @@ class smt2_printer { ast_manager & m() const { return m_manager; } ast_manager & fm() const { return format_ns::fm(m()); } + std::string ensure_quote(symbol const& s) { + std::string str; + if (is_smt2_quoted_symbol(s)) + str = mk_smt2_quoted_symbol(s); + else + str = s.str(); + return str; + } + + symbol ensure_quote_sym(symbol const& s) { + if (is_smt2_quoted_symbol(s)) { + std::string str; + str = mk_smt2_quoted_symbol(s); + return symbol(str.c_str()); + } + else + return s; + } + void pp_var(var * v) { format * f; if (v->get_idx() < m_var_names.size()) { @@ -501,11 +520,7 @@ class smt2_printer { } format * pp_simple_attribute(char const * attr, symbol const & s) { - std::string str; - if (is_smt2_quoted_symbol(s)) - str = mk_smt2_quoted_symbol(s); - else - str = s.str(); + std::string str = ensure_quote(s); return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str.c_str())); } @@ -773,7 +788,7 @@ class smt2_printer { void register_var_names(quantifier * q) { unsigned num_decls = q->get_num_decls(); for (unsigned i = 0; i < num_decls; i++) { - symbol name = q->get_decl_name(i); + symbol name = ensure_quote_sym(q->get_decl_name(i)); if (name.is_numerical()) { unsigned idx = 1; name = next_name("x", idx); @@ -997,6 +1012,7 @@ public: unsigned idx = 1; for (unsigned i = 0; i < num; i++) { symbol name = next_name(var_prefix, idx); + name = ensure_quote_sym(name); var_names.push_back(name); m_var_names_set.insert(name); m_var_names.push_back(name); diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 0856ab5b8..b040efc0c 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -753,12 +753,7 @@ br_status arith_rewriter::mk_rem_core(expr * arg1, expr * arg2, expr_ref & resul } else if (m_util.is_numeral(arg2, v2, is_int) && is_int && !v2.is_zero()) { if (is_add(arg1) || is_mul(arg1)) { - ptr_buffer new_args; - unsigned num_args = to_app(arg1)->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - new_args.push_back(m_util.mk_rem(to_app(arg1)->get_arg(i), arg2)); - result = m().mk_app(to_app(arg1)->get_decl(), new_args.size(), new_args.c_ptr()); - return BR_REWRITE2; + return BR_FAILED; } else { if (v2.is_neg()) { diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp index dfee148b5..99b0f2521 100644 --- a/src/cmd_context/check_logic.cpp +++ b/src/cmd_context/check_logic.cpp @@ -310,6 +310,8 @@ struct check_logic::imp { return false; non_numeral = arg; } + if (non_numeral == 0) + return true; if (is_diff_var(non_numeral)) return true; if (!m_a_util.is_add(non_numeral) && !m_a_util.is_sub(non_numeral)) diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 44ba2b4d2..4a51e4943 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -515,6 +515,25 @@ bool pdatatype_decl::has_missing_refs(symbol & missing) const { return false; } +bool pdatatype_decl::has_duplicate_accessors(symbol & duplicated) const { + hashtable names; + ptr_vector::const_iterator it = m_constructors.begin(); + ptr_vector::const_iterator end = m_constructors.end(); + for (; it != end; ++it) { + ptr_vector const& acc = (*it)->m_accessors; + for (unsigned i = 0; i < acc.size(); ++i) { + symbol const& name = acc[i]->get_name(); + if (names.contains(name)) { + duplicated = name; + return true; + } + names.insert(name); + } + } + return false; +} + + bool pdatatype_decl::fix_missing_refs(dictionary const & symbol2idx, symbol & missing) { ptr_vector::iterator it = m_constructors.begin(); ptr_vector::iterator end = m_constructors.end(); diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index 76ad2a020..83d881f57 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -169,6 +169,7 @@ public: class paccessor_decl : public pdecl { friend class pdecl_manager; friend class pconstructor_decl; + friend class pdatatype_decl; symbol m_name; ptype m_type; paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r); @@ -222,6 +223,7 @@ public: sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s); virtual void display(std::ostream & out) const; bool has_missing_refs(symbol & missing) const; + bool has_duplicate_accessors(symbol & repeated) const; }; /** diff --git a/src/duality/duality.h b/src/duality/duality.h index e7516c1db..fe86ed2ec 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -801,7 +801,7 @@ protected: }; -#ifdef WIN32 +#ifdef _WINDOWS __declspec(dllexport) #endif void FromClauses(const std::vector &clauses); diff --git a/src/duality/duality_hash.h b/src/duality/duality_hash.h deleted file mode 100755 index f6767c037..000000000 --- a/src/duality/duality_hash.h +++ /dev/null @@ -1,169 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - iz3hash.h - -Abstract: - - Wrapper for stl hash tables - -Author: - - Ken McMillan (kenmcmil) - -Revision History: - ---*/ - -// pull in the headers for has_map and hash_set -// these live in non-standard places - -#ifndef IZ3_HASH_H -#define IZ3_HASH_H - -//#define USE_UNORDERED_MAP -#ifdef USE_UNORDERED_MAP - -#define stl_ext std -#define hash_space std -#include -#include -#define hash_map unordered_map -#define hash_set unordered_set - -#else - -#if __GNUC__ >= 3 -#undef __DEPRECATED -#define stl_ext __gnu_cxx -#define hash_space stl_ext -#include -#include -#else -#ifdef WIN32 -#define stl_ext stdext -#define hash_space std -#include -#include -#else -#define stl_ext std -#define hash_space std -#include -#include -#endif -#endif - -#endif - -#include - -// stupid STL doesn't include hash function for class string - -#ifndef WIN32 - -namespace stl_ext { - template <> - class hash { - stl_ext::hash H; - public: - size_t operator()(const std::string &s) const { - return H(s.c_str()); - } - }; -} - -#endif - -namespace hash_space { - template <> - class hash > { - public: - size_t operator()(const std::pair &p) const { - return p.first + p.second; - } - }; -} - -#ifdef WIN32 -template <> inline -size_t stdext::hash_value >(const std::pair& p) -{ // hash _Keyval to size_t value one-to-one - return p.first + p.second; -} -#endif - -namespace hash_space { - template - class hash > { - public: - size_t operator()(const std::pair &p) const { - return (size_t)p.first + (size_t)p.second; - } - }; -} - -#if 0 -template inline -size_t stdext::hash_value >(const std::pair& p) -{ // hash _Keyval to size_t value one-to-one - return (size_t)p.first + (size_t)p.second; -} -#endif - -#ifdef WIN32 - -namespace std { - template <> - class less > { - public: - bool operator()(const pair &x, const pair &y) const { - return x.first < y.first || x.first == y.first && x.second < y.second; - } - }; - -} - -namespace std { - template - class less > { - public: - bool operator()(const pair &x, const pair &y) const { - return (size_t)x.first < (size_t)y.first || (size_t)x.first == (size_t)y.first && (size_t)x.second < (size_t)y.second; - } - }; - -} - -#endif - - -#ifndef WIN32 - -namespace stl_ext { - template - class hash { - public: - size_t operator()(const T *p) const { - return (size_t) p; - } - }; -} - -#endif - -#ifdef WIN32 - - - - -template -class hash_map : public stl_ext::hash_map > > {}; - -template -class hash_set : public stl_ext::hash_set > > {}; - -#endif - -#endif diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp index a4e9e0240..f409bfd53 100755 --- a/src/duality/duality_profiling.cpp +++ b/src/duality/duality_profiling.cpp @@ -25,7 +25,7 @@ Revision History: #include #include -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index 564f31891..25c5f9c7d 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -21,7 +21,7 @@ Revision History: -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) @@ -36,10 +36,6 @@ Revision History: #include "duality.h" #include "duality_profiling.h" -#ifndef WIN32 -// #define Z3OPS -#endif - // TODO: do we need these? #ifdef Z3OPS diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 7e36495b1..a47e90f95 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -19,7 +19,7 @@ Revision History: --*/ -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp index 0f6198edd..2a699a995 100755 --- a/src/duality/duality_wrapper.cpp +++ b/src/duality/duality_wrapper.cpp @@ -18,7 +18,7 @@ Revision History: --*/ -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/interp/foci2.h b/src/interp/foci2.h index 261dd05dc..0aa787c54 100755 --- a/src/interp/foci2.h +++ b/src/interp/foci2.h @@ -23,7 +23,7 @@ Revision History: #include #include -#ifdef WIN32 +#ifdef _WINDOWS #define FOCI2_EXPORT __declspec(dllexport) #else #define FOCI2_EXPORT __attribute__ ((visibility ("default"))) diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index 054c8a811..32fe33566 100755 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -18,7 +18,7 @@ Revision History: --*/ -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp index 02acaa5c1..223be0223 100755 --- a/src/interp/iz3checker.cpp +++ b/src/interp/iz3checker.cpp @@ -17,7 +17,7 @@ Revision History: --*/ -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp index 667d962d0..bed93a56f 100755 --- a/src/interp/iz3interp.cpp +++ b/src/interp/iz3interp.cpp @@ -19,7 +19,7 @@ Revision History: /* Copyright 2011 Microsoft Research. */ -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp index 0259f1b52..a39065922 100755 --- a/src/interp/iz3mgr.cpp +++ b/src/interp/iz3mgr.cpp @@ -18,7 +18,7 @@ Revision History: --*/ -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/interp/iz3profiling.cpp b/src/interp/iz3profiling.cpp index 2c4a31d58..3237b7cd8 100755 --- a/src/interp/iz3profiling.cpp +++ b/src/interp/iz3profiling.cpp @@ -17,7 +17,7 @@ Revision History: --*/ -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/interp/iz3proof.cpp b/src/interp/iz3proof.cpp index 3fefea73f..f806cd792 100755 --- a/src/interp/iz3proof.cpp +++ b/src/interp/iz3proof.cpp @@ -18,7 +18,7 @@ Revision History: --*/ -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 5fa3ee021..2a4c4bd85 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -17,7 +17,7 @@ Revision History: --*/ -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 345381047..2c4a22724 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -17,7 +17,7 @@ Revision History: --*/ -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp index a42c7034d..e5b8a5fca 100755 --- a/src/interp/iz3translate_direct.cpp +++ b/src/interp/iz3translate_direct.cpp @@ -20,7 +20,7 @@ Revision History: --*/ -#ifdef WIN32 +#ifdef _WINDOWS #pragma warning(disable:4996) #pragma warning(disable:4800) #pragma warning(disable:4267) diff --git a/src/muz/bmc/dl_bmc_engine.cpp b/src/muz/bmc/dl_bmc_engine.cpp index 7a88c1188..0dcbf4644 100644 --- a/src/muz/bmc/dl_bmc_engine.cpp +++ b/src/muz/bmc/dl_bmc_engine.cpp @@ -1465,6 +1465,10 @@ namespace datalog { if (m_rules.get_num_rules() == 0) { return l_false; } + if (m_rules.get_predicate_rules(m_query_pred).empty()) { + return l_false; + } + if (is_linear()) { if (m_ctx.get_engine() == QBMC_ENGINE) { diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index b5af6353e..785f578f3 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -850,6 +850,13 @@ namespace smt2 { for (unsigned i = 0; i < sz; i++) { pdatatype_decl * d = new_dt_decls[i]; SASSERT(d != 0); + symbol duplicated; + if (d->has_duplicate_accessors(duplicated)) { + std::string err_msg = "invalid datatype declaration, repeated accessor identifier '"; + err_msg += duplicated.str(); + err_msg += "'"; + throw parser_exception(err_msg, line, pos); + } m_ctx.insert(d); if (d->get_num_params() == 0) { // if datatype is not parametric... then force instantiation to register accessor, recognizers and constructors... @@ -2070,6 +2077,7 @@ namespace smt2 { void parse_option_value() { switch (curr()) { + case scanner::BV_TOKEN: case scanner::INT_TOKEN: case scanner::FLOAT_TOKEN: m_curr_cmd->set_next_arg(m_ctx, m_scanner.get_number()); diff --git a/src/shell/main.cpp b/src/shell/main.cpp index e0fa4a1f2..f23bc470c 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -87,7 +87,7 @@ void display_usage() { std::cout << "\nResources:\n"; // timeout and memout are now available on Linux and OSX too. std::cout << " -T:timeout set the timeout (in seconds).\n"; - std::cout << " -t:timeout set the soft timeout (in seconds). It only kills the current query.\n"; + std::cout << " -t:timeout set the soft timeout (in milli seconds). It only kills the current query.\n"; std::cout << " -memory:Megabytes set a limit for virtual memory consumption.\n"; // std::cout << "\nOutput:\n"; diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 30bc65b6d..911c75d36 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -27,8 +27,7 @@ enum arith_solver_id { AS_DIFF_LOGIC, AS_ARITH, AS_DENSE_DIFF_LOGIC, - AS_UTVPI, - AS_HORN + AS_UTVPI }; enum bound_prop_mode { diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp index 8fd0e08bc..e9b0e069a 100644 --- a/src/smt/smt_quantifier.cpp +++ b/src/smt/smt_quantifier.cpp @@ -439,12 +439,12 @@ 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; + if(!m_fparams->m_mbqi_id) return true; + const symbol &s = q->get_qid(); + size_t 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 diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index f91a58f87..51b83d61c 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -22,7 +22,6 @@ Revision History: #include"theory_arith.h" #include"theory_dense_diff_logic.h" #include"theory_diff_logic.h" -#include"theory_horn_ineq.h" #include"theory_utvpi.h" #include"theory_array.h" #include"theory_array_full.h" @@ -725,12 +724,6 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_dense_mi, m_manager, m_params)); } break; - case AS_HORN: - if (m_params.m_arith_int_only) - m_context.register_plugin(alloc(smt::theory_ihi, m_manager)); - else - m_context.register_plugin(alloc(smt::theory_rhi, m_manager)); - break; case AS_UTVPI: if (m_params.m_arith_int_only) m_context.register_plugin(alloc(smt::theory_iutvpi, m_manager)); diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 8cefee8da..98b7592c8 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -139,22 +139,32 @@ protected: SASSERT(g.is_well_sorted()); } + struct expr_pos { + unsigned m_parent; + unsigned m_self; + unsigned m_idx; + expr* m_expr; + expr_pos(unsigned p, unsigned s, unsigned i, expr* e): + m_parent(p), m_self(s), m_idx(i), m_expr(e) + {} + expr_pos(): + m_parent(0), m_self(0), m_idx(0), m_expr(0) + {} + }; + void reduce(expr_ref& result){ SASSERT(m.is_bool(result)); - ptr_vector todo; ptr_vector names; - svector is_checked; - svector parent_ids, self_ids; + svector todo; expr_ref_vector fresh_vars(m), trail(m); expr_ref res(m), tmp(m); - obj_map > cache; - unsigned id = 1; + obj_map cache; + unsigned id = 1, child_id = 0; expr_ref n2(m), fml(m); - unsigned path_id = 0, self_pos = 0; + unsigned parent_pos = 0, self_pos = 0, self_idx = 0; app * a; unsigned sz; - std::pair path_r; - ptr_vector found; + expr_pos path_r; expr_ref_vector args(m); expr_ref n = mk_fresh(id, m.mk_bool_sort()); trail.push_back(n); @@ -163,26 +173,25 @@ protected: tmp = m.mk_not(m.mk_iff(fml, n)); m_solver.assert_expr(tmp); - todo.push_back(fml); + todo.push_back(expr_pos(0,0,0,fml)); names.push_back(n); - is_checked.push_back(false); - parent_ids.push_back(0); - self_ids.push_back(0); m_solver.push(); while (!todo.empty() && !m_cancel) { expr_ref res(m); args.reset(); - expr* e = todo.back(); - unsigned pos = parent_ids.back(); + expr* e = todo.back().m_expr; + self_pos = todo.back().m_self; + parent_pos = todo.back().m_parent; + self_idx = todo.back().m_idx; n = names.back(); - bool checked = is_checked.back(); if (cache.contains(e)) { goto done; } - if (m.is_bool(e) && !checked && simplify_bool(n, res)) { - TRACE("ctx_solver_simplify_tactic", tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";); + if (m.is_bool(e) && simplify_bool(n, res)) { + TRACE("ctx_solver_simplify_tactic", + tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";); goto done; } if (!is_app(e)) { @@ -191,49 +200,31 @@ protected: } a = to_app(e); - if (!is_checked.back()) { - self_ids.back() = ++path_id; - is_checked.back() = true; - } - self_pos = self_ids.back(); - sz = a->get_num_args(); - + sz = a->get_num_args(); n2 = 0; - found.reset(); // arguments already simplified. for (unsigned i = 0; i < sz; ++i) { expr* arg = a->get_arg(i); - if (cache.find(arg, path_r) && !found.contains(arg)) { + if (cache.find(arg, path_r)) { // // This is a single traversal version of the context // simplifier. It simplifies only the first occurrence of // a sub-term with respect to the context. // - found.push_back(arg); - if (path_r.first == self_pos) { - TRACE("ctx_solver_simplify_tactic", tout << "cached " << mk_pp(arg, m) << " |-> " << mk_pp(path_r.second, m) << "\n";); - args.push_back(path_r.second); - } - else if (m.is_bool(arg)) { - res = local_simplify(a, n, id, i); - TRACE("ctx_solver_simplify_tactic", - tout << "Already cached: " << path_r.first << " " << mk_pp(arg, m) << " |-> " << mk_pp(res, m) << "\n";); - args.push_back(res); + if (path_r.m_parent == self_pos && path_r.m_idx == i) { + args.push_back(path_r.m_expr); } else { args.push_back(arg); } } - else if (!n2 && !found.contains(arg)) { + else if (!n2) { n2 = mk_fresh(id, m.get_sort(arg)); trail.push_back(n2); - todo.push_back(arg); - parent_ids.push_back(self_pos); - self_ids.push_back(0); + todo.push_back(expr_pos(self_pos, child_id++, i, arg)); names.push_back(n2); args.push_back(n2); - is_checked.push_back(false); } else { args.push_back(arg); @@ -251,22 +242,16 @@ protected: done: if (res) { - cache.insert(e, std::make_pair(pos, res)); - } - - TRACE("ctx_solver_simplify_tactic", - tout << mk_pp(e, m) << " checked: " << checked << " cached: " << mk_pp(res?res.get():e, m) << "\n";); + cache.insert(e, expr_pos(parent_pos, self_pos, self_idx, res)); + } todo.pop_back(); - parent_ids.pop_back(); - self_ids.pop_back(); names.pop_back(); - is_checked.pop_back(); m_solver.pop(1); } if (!m_cancel) { VERIFY(cache.find(fml, path_r)); - result = path_r.second; + result = path_r.m_expr; } } @@ -306,32 +291,6 @@ protected: } return expr_ref(m.mk_app(fn, m_arith.mk_numeral(rational(id++), true)), m); } - - - expr_ref local_simplify(app* a, expr* n, unsigned& id, unsigned index) { - SASSERT(index < a->get_num_args()); - SASSERT(m.is_bool(a->get_arg(index))); - expr_ref n2(m), result(m), tmp(m); - n2 = mk_fresh(id, m.get_sort(a->get_arg(index))); - ptr_buffer args; - for (unsigned i = 0; i < a->get_num_args(); ++i) { - if (i == index) { - args.push_back(n2); - } - else { - args.push_back(a->get_arg(i)); - } - } - m_mk_app(a->get_decl(), args.size(), args.c_ptr(), result); - m_solver.push(); - tmp = m.mk_eq(result, n); - m_solver.assert_expr(tmp); - if (!simplify_bool(n2, result)) { - result = a->get_arg(index); - } - m_solver.pop(1); - return result; - } }; diff --git a/src/smt/theory_horn_ineq.cpp b/src/smt/theory_horn_ineq.cpp deleted file mode 100644 index 978b5b003..000000000 --- a/src/smt/theory_horn_ineq.cpp +++ /dev/null @@ -1,236 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - theory_horn_ineq.h - -Author: - - Nikolaj Bjorner (nbjorner) 2013-04-18 - -Revision History: - - The implementaton is derived from theory_diff_logic. - ---*/ -#include "theory_horn_ineq.h" -#include "theory_horn_ineq_def.h" - -namespace smt { - - template class theory_horn_ineq; - template class theory_horn_ineq; - - // similar to test_diff_logic: - - horn_ineq_tester::horn_ineq_tester(ast_manager& m): m(m), a(m) {} - - bool horn_ineq_tester::operator()(expr* e) { - m_todo.reset(); - m_pols.reset(); - pos_mark.reset(); - neg_mark.reset(); - m_todo.push_back(e); - m_pols.push_back(l_true); - while (!m_todo.empty()) { - expr* e = m_todo.back(); - lbool p = m_pols.back(); - m_todo.pop_back(); - m_pols.pop_back(); - switch (p) { - case l_true: - if (pos_mark.is_marked(e)) { - continue; - } - pos_mark.mark(e, true); - break; - case l_false: - if (neg_mark.is_marked(e)) { - continue; - } - neg_mark.mark(e, true); - break; - case l_undef: - if (pos_mark.is_marked(e) && neg_mark.is_marked(e)) { - continue; - } - pos_mark.mark(e, true); - neg_mark.mark(e, true); - break; - } - if (!test_expr(p, e)) { - return false; - } - } - return true; - } - - vector > const& horn_ineq_tester::get_linearization() const { - return m_terms; - } - - bool horn_ineq_tester::test_expr(lbool p, expr* e) { - expr* e1, *e2, *e3; - if (is_var(e)) { - return true; - } - if (!is_app(e)) { - return false; - } - app* ap = to_app(e); - if (m.is_and(ap) || m.is_or(ap)) { - for (unsigned i = 0; i < ap->get_num_args(); ++i) { - m_todo.push_back(ap->get_arg(i)); - m_pols.push_back(p); - } - } - else if (m.is_not(e, e1)) { - m_todo.push_back(e); - m_pols.push_back(~p); - } - else if (m.is_ite(e, e1, e2, e3)) { - m_todo.push_back(e1); - m_pols.push_back(l_undef); - m_todo.push_back(e2); - m_pols.push_back(p); - m_todo.push_back(e3); - m_pols.push_back(p); - } - else if (m.is_iff(e, e1, e2)) { - m_todo.push_back(e1); - m_pols.push_back(l_undef); - m_todo.push_back(e2); - m_pols.push_back(l_undef); - m_todo.push_back(e2); - } - else if (m.is_implies(e, e1, e2)) { - m_todo.push_back(e1); - m_pols.push_back(~p); - m_todo.push_back(e2); - m_pols.push_back(p); - } - else if (m.is_eq(e, e1, e2)) { - return linearize(e1, e2) == diff; - } - else if (m.is_true(e) || m.is_false(e)) { - // no-op - } - else if (a.is_le(e, e1, e2) || a.is_ge(e, e2, e1) || - a.is_lt(e, e1, e2) || a.is_gt(e, e2, e1)) { - if (p == l_false) { - std::swap(e2, e1); - } - classify_t cl = linearize(e1, e2); - switch(p) { - case l_undef: - return cl == diff; - case l_true: - case l_false: - return cl == horn || cl == diff; - } - } - else if (!is_uninterp_const(e)) { - return false; - } - return true; - } - - bool horn_ineq_tester::operator()(unsigned num_fmls, expr* const* fmls) { - for (unsigned i = 0; i < num_fmls; ++i) { - if (!(*this)(fmls[i])) { - return false; - } - } - return true; - } - - horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e) { - m_terms.reset(); - m_terms.push_back(std::make_pair(e, rational(1))); - return linearize(); - } - - horn_ineq_tester::classify_t horn_ineq_tester::linearize(expr* e1, expr* e2) { - m_terms.reset(); - m_terms.push_back(std::make_pair(e1, rational(1))); - m_terms.push_back(std::make_pair(e2, rational(-1))); - return linearize(); - } - - horn_ineq_tester::classify_t horn_ineq_tester::linearize() { - - m_weight.reset(); - m_coeff_map.reset(); - - while (!m_terms.empty()) { - expr* e1, *e2; - rational num; - rational mul = m_terms.back().second; - expr* e = m_terms.back().first; - m_terms.pop_back(); - if (a.is_add(e)) { - for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) { - m_terms.push_back(std::make_pair(to_app(e)->get_arg(i), mul)); - } - } - else if (a.is_mul(e, e1, e2) && a.is_numeral(e1, num)) { - m_terms.push_back(std::make_pair(e2, mul*num)); - } - else if (a.is_mul(e, e2, e1) && a.is_numeral(e1, num)) { - m_terms.push_back(std::make_pair(e2, mul*num)); - } - else if (a.is_sub(e, e1, e2)) { - m_terms.push_back(std::make_pair(e1, mul)); - m_terms.push_back(std::make_pair(e2, -mul)); - } - else if (a.is_uminus(e, e1)) { - m_terms.push_back(std::make_pair(e1, -mul)); - } - else if (a.is_numeral(e, num)) { - m_weight += num*mul; - } - else if (a.is_to_real(e, e1)) { - m_terms.push_back(std::make_pair(e1, mul)); - } - else if (!is_uninterp_const(e)) { - return non_horn; - } - else { - m_coeff_map.insert_if_not_there2(e, rational(0))->get_data().m_value += mul; - } - } - unsigned num_negative = 0; - unsigned num_positive = 0; - bool is_unit_pos = true, is_unit_neg = true; - obj_map::iterator it = m_coeff_map.begin(); - obj_map::iterator end = m_coeff_map.end(); - for (; it != end; ++it) { - rational r = it->m_value; - if (r.is_zero()) { - continue; - } - m_terms.push_back(std::make_pair(it->m_key, r)); - if (r.is_pos()) { - is_unit_pos = is_unit_pos && r.is_one(); - num_positive++; - } - else { - is_unit_neg = is_unit_neg && r.is_minus_one(); - num_negative++; - } - } - if (num_negative <= 1 && is_unit_pos && is_unit_neg && num_positive <= 1) { - return diff; - } - if (num_positive <= 1 && is_unit_pos) { - return horn; - } - if (num_negative <= 1 && is_unit_neg) { - return co_horn; - } - return non_horn; - } - - -} diff --git a/src/smt/theory_horn_ineq.h b/src/smt/theory_horn_ineq.h deleted file mode 100644 index ed96f25f6..000000000 --- a/src/smt/theory_horn_ineq.h +++ /dev/null @@ -1,328 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - theory_horn_ineq.h - -Abstract: - - A*x <= weight + D*x, coefficients to A and D are non-negative, - D is a diagonal matrix. - Coefficients to weight may have both signs. - - Label variables by weight. - Select inequality that is not satisfied. - Set delta(LHS) := 0 - Set delta(RHS(x)) := weight(x) - b - Propagate weight increment through inequalities. - -Author: - - Nikolaj Bjorner (nbjorner) 2013-04-18 - -Revision History: - - The implementaton is derived from theory_diff_logic. - ---*/ - -#ifndef _THEORY_HORN_INEQ_H_ -#define _THEORY_HORN_INEQ_H_ - -#include"rational.h" -#include"inf_rational.h" -#include"inf_int_rational.h" -#include"inf_eps_rational.h" -#include"smt_theory.h" -#include"arith_decl_plugin.h" -#include"smt_justification.h" -#include"map.h" -#include"smt_params.h" -#include"arith_eq_adapter.h" -#include"smt_model_generator.h" -#include"numeral_factory.h" -#include"smt_clause.h" - -namespace smt { - - class horn_ineq_tester { - ast_manager& m; - arith_util a; - ptr_vector m_todo; - svector m_pols; - ast_mark pos_mark, neg_mark; - obj_map m_coeff_map; - rational m_weight; - vector > m_terms; - - public: - enum classify_t { - co_horn, - horn, - diff, - non_horn - }; - horn_ineq_tester(ast_manager& m); - - // test if formula is in the Horn inequality fragment: - bool operator()(expr* fml); - bool operator()(unsigned num_fmls, expr* const* fmls); - - // linearize inequality/equality - classify_t linearize(expr* e); - classify_t linearize(expr* e1, expr* e2); - - // retrieve linearization - vector > const& get_linearization() const; - rational const& get_weight() const { return m_weight; } - private: - bool test_expr(lbool p, expr* e); - classify_t linearize(); - }; - - template - class theory_horn_ineq : public theory, private Ext { - - typedef typename Ext::numeral numeral; - typedef typename Ext::inf_numeral inf_numeral; - typedef literal explanation; - typedef theory_var th_var; - typedef svector th_var_vector; - typedef unsigned clause_id; - typedef vector > coeffs; - - class clause; - class graph; - class assignment_trail; - class parent_trail; - - class atom { - protected: - bool_var m_bvar; - bool m_true; - int m_pos; - int m_neg; - public: - atom(bool_var bv, int pos, int neg) : - m_bvar(bv), m_true(false), - m_pos(pos), m_neg(neg) {} - ~atom() {} - bool_var get_bool_var() const { return m_bvar; } - bool is_true() const { return m_true; } - void assign_eh(bool is_true) { m_true = is_true; } - int get_asserted_edge() const { return this->m_true?m_pos:m_neg; } - int get_pos() const { return m_pos; } - int get_neg() const { return m_neg; } - std::ostream& display(theory_horn_ineq const& th, std::ostream& out) const; - }; - typedef svector atoms; - - struct scope { - unsigned m_atoms_lim; - unsigned m_asserted_atoms_lim; - unsigned m_asserted_qhead_old; - }; - - struct stats { - unsigned m_num_conflicts; - unsigned m_num_assertions; - unsigned m_num_core2th_eqs; - unsigned m_num_core2th_diseqs; - - void reset() { - memset(this, 0, sizeof(*this)); - } - - stats() { - reset(); - } - }; - - stats m_stats; - smt_params m_params; - arith_util a; - arith_eq_adapter m_arith_eq_adapter; - th_var m_zero_int; // cache the variable representing the zero variable. - th_var m_zero_real; // cache the variable representing the zero variable. - - graph* m_graph; - atoms m_atoms; - unsigned_vector m_asserted_atoms; // set of asserted atoms - unsigned m_asserted_qhead; - u_map m_bool_var2atom; - svector m_scopes; - - double m_agility; - bool m_lia; - bool m_lra; - bool m_non_horn_ineq_exprs; - - horn_ineq_tester m_test; - - - arith_factory * m_factory; - rational m_delta; - rational m_lambda; - - - // Set a conflict due to a negative cycle. - void set_neg_cycle_conflict(); - - // Create a new theory variable. - virtual th_var mk_var(enode* n); - - virtual th_var mk_var(expr* n); - - void compute_delta(); - - void found_non_horn_ineq_expr(expr * n); - - bool is_interpreted(app* n) const { - return n->get_family_id() == get_family_id(); - } - - public: - theory_horn_ineq(ast_manager& m); - - virtual ~theory_horn_ineq(); - - virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_horn_ineq, get_manager()); } - - virtual char const * get_name() const { return "horn-inequality-logic"; } - - /** - \brief See comment in theory::mk_eq_atom - */ - virtual app * mk_eq_atom(expr * lhs, expr * rhs) { return a.mk_eq(lhs, rhs); } - - virtual void init(context * ctx); - - virtual bool internalize_atom(app * atom, bool gate_ctx); - - virtual bool internalize_term(app * term); - - virtual void internalize_eq_eh(app * atom, bool_var v); - - virtual void assign_eh(bool_var v, bool is_true); - - virtual void new_eq_eh(th_var v1, th_var v2) { - m_arith_eq_adapter.new_eq_eh(v1, v2); - } - - virtual bool use_diseqs() const { return true; } - - virtual void new_diseq_eh(th_var v1, th_var v2) { - m_arith_eq_adapter.new_diseq_eh(v1, v2); - } - - virtual void push_scope_eh(); - - virtual void pop_scope_eh(unsigned num_scopes); - - virtual void restart_eh() { - m_arith_eq_adapter.restart_eh(); - } - - virtual void relevant_eh(app* e) {} - - virtual void init_search_eh() { - m_arith_eq_adapter.init_search_eh(); - } - - virtual final_check_status final_check_eh(); - - virtual bool is_shared(th_var v) const { - return false; - } - - virtual bool can_propagate() { - SASSERT(m_asserted_qhead <= m_asserted_atoms.size()); - return m_asserted_qhead != m_asserted_atoms.size(); - } - - virtual void propagate(); - - virtual justification * why_is_diseq(th_var v1, th_var v2) { - UNREACHABLE(); - return 0; - } - - virtual void reset_eh(); - - virtual void init_model(model_generator & m); - - virtual model_value_proc * mk_value(enode * n, model_generator & mg); - - virtual bool validate_eq_in_model(th_var v1, th_var v2, bool is_true) const { - return true; - } - - virtual void display(std::ostream & out) const; - - virtual void collect_statistics(::statistics & st) const; - - private: - - virtual void new_eq_eh(th_var v1, th_var v2, justification& j) { - m_stats.m_num_core2th_eqs++; - new_eq_or_diseq(true, v1, v2, j); - } - - virtual void new_diseq_eh(th_var v1, th_var v2, justification& j) { - m_stats.m_num_core2th_diseqs++; - new_eq_or_diseq(false, v1, v2, j); - } - - void negate(coeffs& coeffs, rational& weight); - numeral mk_weight(bool is_real, bool is_strict, rational const& w) const; - void mk_coeffs(vector >const& terms, coeffs& coeffs, rational& w); - - void del_atoms(unsigned old_size); - - void propagate_core(); - - bool propagate_atom(atom const& a); - - th_var mk_term(app* n); - - th_var mk_num(app* n, rational const& r); - - bool is_consistent() const; - - th_var expand(bool pos, th_var v, rational & k); - - void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just); - - th_var get_zero(sort* s) const { return a.is_int(s)?m_zero_int:m_zero_real; } - - th_var get_zero(expr* e) const { return get_zero(get_manager().get_sort(e)); } - - void inc_conflicts(); - - }; - - struct rhi_ext { - typedef inf_rational inf_numeral; - typedef inf_eps_rational numeral; - numeral m_epsilon; - numeral m_minus_infty; - rhi_ext() : m_epsilon(inf_rational(rational(), true)), m_minus_infty(rational(-1),inf_rational()) {} - }; - - struct ihi_ext { - typedef rational inf_numeral; - typedef inf_eps_rational numeral; - numeral m_epsilon; - numeral m_minus_infty; - ihi_ext() : m_epsilon(rational(1)), m_minus_infty(rational(-1),rational(0)) {} - }; - - typedef theory_horn_ineq theory_rhi; - typedef theory_horn_ineq theory_ihi; -}; - - - - -#endif /* _THEORY_HORN_INEQ_H_ */ diff --git a/src/smt/theory_horn_ineq_def.h b/src/smt/theory_horn_ineq_def.h deleted file mode 100644 index f4fa7e8d7..000000000 --- a/src/smt/theory_horn_ineq_def.h +++ /dev/null @@ -1,1166 +0,0 @@ -/*++ -Copyright (c) 2013 Microsoft Corporation - -Module Name: - - theory_horn_ineq_def.h - -Abstract: - - A*x <= b + D*x, coefficients to A and D are non-negative, - D is a diagonal matrix. - Coefficients to b may have both signs. - -Author: - - Nikolaj Bjorner (nbjorner) 2013-04-18 - -Revision History: - ---*/ - -#ifndef _THEORY_HORN_INEQ_DEF_H_ -#define _THEORY_HORN_INEQ_DEF_H_ -#include "theory_horn_ineq.h" -#include "ast_pp.h" -#include "smt_context.h" - -namespace smt { - - static const unsigned null_clause_id = UINT_MAX; - - /** - A clause represents an inequality of the form - - v1*c1 + v2*c2 + .. + v_n*c_n + w <= v*c - - where - - m_vars: [v1,v2,...,v_n] - - m_coeffs: [c1,c2,...,c_n] - - m_var: v - - m_coeff: c - - m_weight: w - - */ - template - class theory_horn_ineq::clause { - vector m_coeffs; // coefficients of body. - svector m_vars; // variables of body. - rational m_coeff; // coefficient of head. - th_var m_var; // head variable. - numeral m_weight; // constant to add - literal m_explanation; - bool m_enabled; - public: - clause(unsigned sz, rational const* coeffs, th_var const* vars, - rational const& coeff, th_var var, numeral const& w, - const literal& ex): - m_coeffs(sz, coeffs), - m_vars(sz, vars), - m_coeff(coeff), - m_var(var), - m_weight(w), - m_explanation(ex), - m_enabled(false) { - DEBUG_CODE( - { - for (unsigned i = 0; i < size(); ++i) { - SASSERT(coeffs[i].is_pos()); - } - SASSERT(coeff.is_pos()); - }); - } - - th_var vars(unsigned i) const { return m_vars[i]; } - rational const& coeffs(unsigned i) const { return m_coeffs[i]; } - th_var var() const { return m_var; } - rational const& coeff() const { return m_coeff; } - const numeral & get_weight() const { return m_weight; } - const literal & get_explanation() const { return m_explanation; } - bool is_enabled() const { return m_enabled; } - unsigned size() const { return m_vars.size(); } - - void enable() { m_enabled = true; } - void disable() { m_enabled = false; } - - void display(std::ostream& out) const { - out << (is_enabled()?"+ ":"- "); - for (unsigned i = 0; i < size(); ++i) { - if (i > 0 && coeffs(i).is_pos()) { - out << " + "; - } - display(out, coeffs(i), vars(i)); - } - if (!get_weight().is_zero()) { - out << " + " << get_weight(); - } - display(out << " <= ", coeff(), var()); - out << "\n"; - } - - private: - - void display(std::ostream& out, rational const& c, th_var v) const { - if (!c.is_one()) { - out << c << "*"; - } - out << "v" << v; - } - }; - - template - class theory_horn_ineq::assignment_trail { - th_var m_var; - numeral m_old_value; - public: - assignment_trail(th_var v, const numeral & val): - m_var(v), - m_old_value(val) {} - th_var get_var() const { return m_var; } - const numeral & get_old_value() const { return m_old_value; } - }; - - template - class theory_horn_ineq::parent_trail { - th_var m_var; - clause_id m_old_value; - public: - parent_trail(th_var v, clause_id val): - m_var(v), - m_old_value(val) {} - th_var get_var() const { return m_var; } - clause_id get_old_value() const { return m_old_value; } - }; - - - template - class theory_horn_ineq::graph : private Ext { - - typedef vector assignment_stack; - typedef vector parent_stack; - typedef unsigned_vector clause_id_vector; - - struct stats { - unsigned m_propagation_cost; - - void reset() { - memset(this, 0, sizeof(*this)); - } - }; - - struct scope { - unsigned m_clauses_lim; - unsigned m_enabled_clauses_lim; - unsigned m_assignment_lim; - unsigned m_parent_lim; - scope(unsigned e, unsigned enabled, unsigned alim, unsigned plim): - m_clauses_lim(e), - m_enabled_clauses_lim(enabled), - m_assignment_lim(alim), - m_parent_lim(plim) { - } - }; - - stats m_stats; - vector m_clauses; - vector m_assignment; // per var - clause_id_vector m_parent; // per var - assignment_stack m_assignment_stack; // stack for restoring the assignment - parent_stack m_parent_stack; // stack for restoring parents - clause_id_vector m_enabled_clauses; - vector m_out_clauses; // use-list for clauses. - vector m_in_clauses; // clauses that have variable in head. - // forward reachability - unsigned_vector m_onstack; - unsigned m_ts; - unsigned_vector m_todo; - literal_vector m_lits; - vector m_coeffs; - th_var m_zero; - clause_id m_unsat_clause; - svector m_trail_stack; - - - public: - - graph(): m_ts(0), m_zero(null_theory_var), m_unsat_clause(null_clause_id) {} - - void reset() { - m_clauses .reset(); - m_assignment .reset(); - m_parent .reset(); - m_assignment_stack .reset(); - m_parent_stack .reset(); - m_out_clauses .reset(); - m_in_clauses .reset(); - m_enabled_clauses .reset(); - m_onstack .reset(); - m_ts = 0; - m_lits .reset(); - m_trail_stack .reset(); - m_unsat_clause = null_clause_id; - } - - - void traverse_neg_cycle1(bool /*stronger_lemmas*/) { - TRACE("horn_ineq", display(tout);); - SASSERT(!m_enabled_clauses.empty()); - clause_id id = m_unsat_clause; - SASSERT(id != null_clause_id); - SASSERT(!is_feasible(m_clauses[id])); - clause_id_vector todo; - vector muls; - todo.push_back(id); - muls.push_back(rational(1)); - u_map lits; - while (!todo.empty()) { - id = todo.back(); - rational mul = muls.back(); - todo.pop_back(); - muls.pop_back(); - clause const& cl = m_clauses[id]; - literal lit = cl.get_explanation(); - if (lit != null_literal) { - lits.insert_if_not_there2(id, rational(0))->get_data().m_value += mul; - } - for (unsigned i = 0; i < cl.size(); ++i) { - id = m_parent[cl.vars(i)]; - if (id != null_clause_id) { - todo.push_back(id); - muls.push_back(mul*cl.coeffs(i)); - } - } - } - u_map::iterator it = lits.begin(), end = lits.end(); - m_lits.reset(); - m_coeffs.reset(); - for (; it != end; ++it) { - m_lits.push_back(m_clauses[it->m_key].get_explanation()); - m_coeffs.push_back(it->m_value); - } - - // TODO: use topological sort to tune traversal of parents to linear. - // (current traversal can be exponential). - // TODO: negative cycle traversal with inline resolution to find - // stronger conflict clauses. - // follow heuristic used in theory_diff_logic_def.h: - } - - unsigned get_num_clauses() const { - return m_clauses.size(); - } - - literal_vector const& get_lits() const { - return m_lits; - } - - vector const& get_coeffs() const { - return m_coeffs; - } - - numeral get_assignment(th_var v) const { - return m_assignment[v]; - } - - numeral eval_body(clause const& cl) const { - numeral v(0); - for (unsigned i = 0; i < cl.size(); ++i) { - v += cl.coeffs(i)*m_assignment[cl.vars(i)]; - } - v += cl.get_weight(); - return v; - } - - numeral eval_body(clause_id id) const { - return eval_body(m_clauses[id]); - } - - numeral eval_head(clause_id id) const { - return eval_head(m_clauses[id]); - } - - numeral eval_head(clause const& cl) const { - return cl.coeff()*m_assignment[cl.var()]; - } - - clause const& get_clause(clause_id id) const { - return m_clauses[id]; - } - - void display_clause(std::ostream& out, clause_id id) const { - if (id == null_clause_id) { - out << "null\n"; - } - else { - m_clauses[id].display(out); - } - } - - void display(std::ostream& out) const { - for (unsigned i = 0; i < m_clauses.size(); ++i) { - display_clause(out, i); - } - for (unsigned i = 0; i < m_assignment.size(); ++i) { - out << m_assignment[i] << "\n"; - } - } - - void collect_statistics(::statistics& st) const { - st.update("hi_propagation_cst", m_stats.m_propagation_cost); - } - - void push() { - m_trail_stack.push_back(scope(m_clauses.size(), m_enabled_clauses.size(), - m_assignment_stack.size(), m_parent_stack.size())); - } - - void pop(unsigned num_scopes) { - unsigned lvl = m_trail_stack.size(); - SASSERT(num_scopes <= lvl); - unsigned new_lvl = lvl - num_scopes; - scope & s = m_trail_stack[new_lvl]; - // restore enabled clauses - for (unsigned i = m_enabled_clauses.size(); i > s.m_enabled_clauses_lim; ) { - --i; - m_clauses[m_enabled_clauses[i]].disable(); - } - m_enabled_clauses.shrink(s.m_enabled_clauses_lim); - - // restore assignment stack - for (unsigned i = m_assignment_stack.size(); i > s.m_assignment_lim; ) { - --i; - m_assignment[m_assignment_stack[i].get_var()] = m_assignment_stack[i].get_old_value(); - } - m_assignment_stack.shrink(s.m_assignment_lim); - - // restore parent stack - for (unsigned i = m_parent_stack.size(); i > s.m_parent_lim; ) { - --i; - m_parent[m_parent_stack[i].get_var()] = m_parent_stack[i].get_old_value(); - } - m_assignment_stack.shrink(s.m_assignment_lim); - - // restore clauses - unsigned old_num_clauses = s.m_clauses_lim; - unsigned num_clauses = m_clauses.size(); - SASSERT(old_num_clauses <= num_clauses); - unsigned to_delete = num_clauses - old_num_clauses; - for (unsigned i = 0; i < to_delete; i++) { - const clause & cl = m_clauses.back(); - TRACE("horn_ineq", tout << "deleting clause:\n"; cl.display(tout);); - for (unsigned j = 0; j < cl.size(); ++j) { - m_out_clauses[cl.vars(j)].pop_back(); - } - m_in_clauses[cl.var()].pop_back(); - m_clauses.pop_back(); - } - m_trail_stack.shrink(new_lvl); - SASSERT(check_invariant()); - } - - /** - \brief Add clause z <= z and the assignment z := 0 - Then z cannot be incremented without causing a loop (and therefore a contradiction). - */ - void set_to_zero(th_var z) { - m_zero = z; - } - - bool enable_clause(clause_id id) { - if (id == null_clause_id) { - return true; - } - clause& cl = m_clauses[id]; - bool r = true; - if (!cl.is_enabled()) { - cl.enable(); - if (!is_feasible(cl)) { - r = make_feasible(id); - } - m_enabled_clauses.push_back(id); - } - return r; - } - - void init_var(th_var v) { - unsigned sz = static_cast(v); - while (m_assignment.size() <= sz) { - m_assignment.push_back(Ext::m_minus_infty); - m_out_clauses.push_back(clause_id_vector()); - m_in_clauses.push_back(clause_id_vector()); - m_parent.push_back(null_clause_id); - m_onstack.push_back(0); - } - m_assignment[v] = Ext::m_minus_infty; - SASSERT(m_out_clauses[v].empty()); - SASSERT(m_in_clauses[v].empty()); - SASSERT(check_invariant()); - } - - clause_id add_ineq(vector > const& terms, numeral const& weight, literal l) { - vector coeffs; - svector vars; - rational coeff(1); - th_var var = null_theory_var; - bool found_negative = false; - for (unsigned i = 0; i < terms.size(); ++i) { - rational const& r = terms[i].second; - if (r.is_pos()) { - coeffs.push_back(terms[i].second); - vars.push_back(terms[i].first); - } - else if (found_negative) { - return null_clause_id; - } - else { - SASSERT(r.is_neg()); - found_negative = true; - coeff = -r; - var = terms[i].first; - } - } - if (!found_negative) { - coeff = rational(1); - var = m_zero; - } - if (!coeff.is_one()) { - // so far just support unit coefficients on right. - return null_clause_id; - } - clause_id id = m_clauses.size(); - m_clauses.push_back(clause(coeffs.size(), coeffs.c_ptr(), vars.c_ptr(), coeff, var, weight, l)); - for (unsigned i = 0; i < vars.size(); ++i) { - m_out_clauses[vars[i]].push_back(id); - } - m_in_clauses[var].push_back(id); - - return id; - } - - bool is_feasible() const { - for (unsigned i = 0; i < m_clauses.size(); ++i) { - if (!is_feasible(m_clauses[i])) { - return false; - } - } - return true; - } - - private: - - bool check_invariant() { - return true; - } - - /** - assignments are fully retraced on backtracking. - This is not always necessary. - */ - - void acc_assignment(th_var v, const numeral & inc) { - m_assignment_stack.push_back(assignment_trail(v, m_assignment[v])); - m_assignment[v] += inc; - } - - void acc_parent(th_var v, clause_id parent) { - m_parent[v] = parent; - m_parent_stack.push_back(parent_trail(v, parent)); - } - - numeral get_delta(const clause & cl) const { - SASSERT(cl.coeff().is_one() && "Not yet support for non-units"); - return eval_body(cl) - eval_head(cl); - } - - void set_onstack(th_var v) { - SASSERT(m_ts != 0); - m_onstack[v] = m_ts; - } - - void reset_onstack(th_var v) { - m_onstack[v] = 0; - } - - bool is_onstack(th_var v) const { - return m_onstack[v] == m_ts; - } - - void inc_ts() { - m_ts++; - if (m_ts == 0) { - m_ts++; - m_onstack.reset(); - m_onstack.resize(m_assignment.size(), 0); - } - } - - // Make the assignment feasible. An assignment is feasible if - // Forall clause cl. eval_body(cl) <= eval_head(cl) - // - // This method assumes that if the assignment is not feasible, - // then the only infeasible clause is the last added clause. - // - // Traversal is by naive DFS search. - // - bool make_feasible(clause_id id) { - SASSERT(is_almost_feasible(id)); - SASSERT(!m_clauses.empty()); - SASSERT(!is_feasible(m_clauses[id])); - const clause & cl0 = m_clauses[id]; - inc_ts(); - for (unsigned i = 0; i < cl0.size(); ++i) { - set_onstack(cl0.vars(i)); - } - th_var source = cl0.var(); - numeral delta = get_delta(cl0); - acc_parent(source, id); - SASSERT(delta.is_pos()); - acc_assignment(source, delta); - m_todo.reset(); - m_todo.push_back(source); - - TRACE("horn_ineq", cl0.display(tout);); - - do { - ++m_stats.m_propagation_cost; - - typename clause_id_vector::iterator it = m_out_clauses[source].begin(); - typename clause_id_vector::iterator end = m_out_clauses[source].end(); - for (; it != end; ++it) { - clause & cl = m_clauses[*it]; - if (!cl.is_enabled()) { - continue; - } - delta = get_delta(cl); - - if (delta.is_pos()) { - TRACE("horn_ineq", cl.display(tout);); - th_var target = cl.var(); - if (is_onstack(target)) { - m_unsat_clause = *it; - return false; - } - else { - acc_assignment(target, delta); - acc_parent(target, *it); - m_todo.push_back(target); - } - } - } - set_onstack(source); - source = m_todo.back(); - // pop stack until there is a new variable to process. - while (is_onstack(source)) { - m_todo.pop_back(); - reset_onstack(source); - if (m_todo.empty()) { - break; - } - source = m_todo.back(); - } - } - while (!m_todo.empty()); - return true; - } - - bool is_almost_feasible(clause_id id) const { - for (unsigned i = 0; i < m_clauses.size(); ++i) { - if (id != static_cast(i) && !is_feasible(m_clauses[i])) { - return false; - } - } - return true; - } - - bool is_feasible(const clause & cl) const { - return !cl.is_enabled() || get_delta(cl).is_nonpos(); - } - - }; - - template - theory_horn_ineq::theory_horn_ineq(ast_manager& m): - theory(m.mk_family_id("arith")), - a(m), - m_arith_eq_adapter(*this, m_params, a), - m_zero_int(null_theory_var), - m_zero_real(null_theory_var), - m_graph(0), - m_asserted_qhead(0), - m_agility(0.5), - m_lia(false), - m_lra(false), - m_non_horn_ineq_exprs(false), - m_test(m), - m_factory(0) { - m_graph = alloc(graph); - } - - template - theory_horn_ineq::~theory_horn_ineq() { - reset_eh(); - dealloc(m_graph); - } - - template - std::ostream& theory_horn_ineq::atom::display(theory_horn_ineq const& th, std::ostream& out) const { - context& ctx = th.get_context(); - lbool asgn = ctx.get_assignment(m_bvar); - bool sign = (l_undef == asgn) || m_true; - return out << literal(m_bvar, sign) << " " << mk_pp(ctx.bool_var2expr(m_bvar), th.get_manager()) << " "; - if (l_undef == asgn) { - out << "unassigned\n"; - } - else { - th.m_graph->display_clause(out, get_asserted_edge()); - } - return out; - } - - template - theory_var theory_horn_ineq::mk_var(enode* n) { - th_var v = theory::mk_var(n); - m_graph->init_var(v); - get_context().attach_th_var(n, this, v); - return v; - } - - template - theory_var theory_horn_ineq::mk_var(expr* n) { - context & ctx = get_context(); - enode* e = 0; - th_var v = null_theory_var; - m_lia |= a.is_int(n); - m_lra |= a.is_real(n); - if (!is_app(n)) { - return v; - } - if (ctx.e_internalized(n)) { - e = ctx.get_enode(n); - v = e->get_th_var(get_id()); - } - else { - ctx.internalize(n, false); - e = ctx.get_enode(n); - } - if (v == null_theory_var) { - v = mk_var(e); - } - if (is_interpreted(to_app(n))) { - found_non_horn_ineq_expr(n); - } - return v; - } - - template - void theory_horn_ineq::reset_eh() { - m_graph ->reset(); - m_zero_int = null_theory_var; - m_zero_real = null_theory_var; - m_atoms .reset(); - m_asserted_atoms .reset(); - m_stats .reset(); - m_scopes .reset(); - m_asserted_qhead = 0; - m_agility = 0.5; - m_lia = false; - m_lra = false; - m_non_horn_ineq_exprs = false; - theory::reset_eh(); - } - - - - template - void theory_horn_ineq::new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just) { - rational k; - th_var s = expand(true, v1, k); - th_var t = expand(false, v2, k); - context& ctx = get_context(); - ast_manager& m = get_manager(); - - if (s == t) { - if (is_eq != k.is_zero()) { - // conflict 0 /= k; - inc_conflicts(); - ctx.set_conflict(&eq_just); - } - } - else { - // - // Create equality ast, internalize_atom - // assign the corresponding equality literal. - // - - app_ref eq(m), s2(m), t2(m); - app* s1 = get_enode(s)->get_owner(); - app* t1 = get_enode(t)->get_owner(); - s2 = a.mk_sub(t1, s1); - t2 = a.mk_numeral(k, m.get_sort(s2.get())); - // t1 - s1 = k - eq = m.mk_eq(s2.get(), t2.get()); - - TRACE("horn_ineq", - tout << v1 << " .. " << v2 << "\n"; - tout << mk_pp(eq.get(), m) <<"\n";); - - if (!internalize_atom(eq.get(), false)) { - UNREACHABLE(); - } - - literal l(ctx.get_literal(eq.get())); - if (!is_eq) { - l = ~l; - } - - ctx.assign(l, b_justification(&eq_just), false); - } - } - - template - void theory_horn_ineq::inc_conflicts() { - m_stats.m_num_conflicts++; - if (m_params.m_arith_adaptive) { - double g = m_params.m_arith_adaptive_propagation_threshold; - m_agility = m_agility*g + 1 - g; - } - } - - template - void theory_horn_ineq::set_neg_cycle_conflict() { - m_graph->traverse_neg_cycle1(m_params.m_arith_stronger_lemmas); - inc_conflicts(); - literal_vector const& lits = m_graph->get_lits(); - context & ctx = get_context(); - TRACE("horn_ineq", - tout << "conflict: "; - for (unsigned i = 0; i < lits.size(); ++i) { - ctx.display_literal_info(tout, lits[i]); - } - tout << "\n"; - ); - - if (m_params.m_arith_dump_lemmas) { - char const * logic = m_lra ? (m_lia?"QF_LIRA":"QF_LRA") : "QF_LIA"; - ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic); - } - - vector params; - if (get_manager().proofs_enabled()) { - params.push_back(parameter(symbol("farkas"))); - vector const& coeffs = m_graph->get_coeffs(); - for (unsigned i = 0; i < coeffs.size(); ++i) { - params.push_back(parameter(coeffs[i])); - } - } - - ctx.set_conflict( - ctx.mk_justification( - ext_theory_conflict_justification( - get_id(), ctx.get_region(), - lits.size(), lits.c_ptr(), 0, 0, params.size(), params.c_ptr()))); - } - - template - void theory_horn_ineq::found_non_horn_ineq_expr(expr* n) { - if (!m_non_horn_ineq_exprs) { - TRACE("horn_ineq", tout << "found non horn logic expression:\n" << mk_pp(n, get_manager()) << "\n";); - get_context().push_trail(value_trail(m_non_horn_ineq_exprs)); - m_non_horn_ineq_exprs = true; - } - } - - template - void theory_horn_ineq::init(context* ctx) { - theory::init(ctx); - m_zero_int = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), true), false, false, true)); - m_zero_real = mk_var(ctx->mk_enode(a.mk_numeral(rational(0), false), false, false, true)); - m_graph->set_to_zero(m_zero_int); - m_graph->set_to_zero(m_zero_real); - } - - /** - \brief Create negated literal. - - The negation of: E <= 0 - - -E + epsilon <= 0 - or - -E + 1 <= 0 - */ - template - void theory_horn_ineq::negate(coeffs& coeffs, rational& weight) { - for (unsigned i = 0; i < coeffs.size(); ++i) { - coeffs[i].second.neg(); - } - weight.neg(); - } - - template - typename theory_horn_ineq::numeral theory_horn_ineq::mk_weight(bool is_real, bool is_strict, rational const& w) const { - if (is_strict) { - return numeral(inf_numeral(w)) + (is_real?Ext::m_epsilon:numeral(1)); - } - else { - return numeral(inf_numeral(w)); - } - } - - template - void theory_horn_ineq::mk_coeffs(vector > const& terms, coeffs& coeffs, rational& w) { - coeffs.reset(); - w = m_test.get_weight(); - for (unsigned i = 0; i < terms.size(); ++i) { - coeffs.push_back(std::make_pair(mk_var(terms[i].first), terms[i].second)); - } - } - - template - bool theory_horn_ineq::internalize_atom(app * n, bool) { - context & ctx = get_context(); - if (!a.is_le(n) && !a.is_ge(n) && !a.is_lt(n) && !a.is_gt(n)) { - found_non_horn_ineq_expr(n); - return false; - } - SASSERT(!ctx.b_internalized(n)); - expr* e1 = n->get_arg(0), *e2 = n->get_arg(1); - if (a.is_ge(n) || a.is_gt(n)) { - std::swap(e1, e2); - } - bool is_strict = a.is_gt(n) || a.is_lt(n); - - horn_ineq_tester::classify_t cl = m_test.linearize(e1, e2); - if (cl == horn_ineq_tester::non_horn) { - found_non_horn_ineq_expr(n); - return false; - } - - rational w; - coeffs coeffs; - mk_coeffs(m_test.get_linearization(), coeffs, w); - bool_var bv = ctx.mk_bool_var(n); - ctx.set_var_theory(bv, get_id()); - literal l(bv); - numeral w1 = mk_weight(a.is_real(e1), is_strict, w); - clause_id pos = m_graph->add_ineq(coeffs, w1, l); - negate(coeffs, w); - numeral w2 = mk_weight(a.is_real(e1), !is_strict, w); - clause_id neg = m_graph->add_ineq(coeffs, w2, ~l); - m_bool_var2atom.insert(bv, m_atoms.size()); - m_atoms.push_back(atom(bv, pos, neg)); - - TRACE("horn_ineq", - tout << mk_pp(n, get_manager()) << "\n"; - m_graph->display_clause(tout << "pos: ", pos); - m_graph->display_clause(tout << "neg: ", neg); - ); - - return true; - } - - template - bool theory_horn_ineq::internalize_term(app * term) { - bool result = null_theory_var != mk_term(term); - CTRACE("horn_ineq", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";); - TRACE("horn_ineq", tout << "Terms may not be internalized " << mk_pp(term, get_manager()) << "\n";); - found_non_horn_ineq_expr(term); - return result; - } - - template - void theory_horn_ineq::internalize_eq_eh(app * atom, bool_var) { - // noop - } - - template - void theory_horn_ineq::assign_eh(bool_var v, bool is_true) { - m_stats.m_num_assertions++; - unsigned idx = m_bool_var2atom.find(v); - SASSERT(get_context().get_assignment(v) != l_undef); - SASSERT((get_context().get_assignment(v) == l_true) == is_true); - m_atoms[idx].assign_eh(is_true); - m_asserted_atoms.push_back(idx); - } - - template - void theory_horn_ineq::push_scope_eh() { - theory::push_scope_eh(); - m_graph->push(); - m_scopes.push_back(scope()); - scope & s = m_scopes.back(); - s.m_atoms_lim = m_atoms.size(); - s.m_asserted_atoms_lim = m_asserted_atoms.size(); - s.m_asserted_qhead_old = m_asserted_qhead; - } - - template - void theory_horn_ineq::pop_scope_eh(unsigned num_scopes) { - unsigned lvl = m_scopes.size(); - SASSERT(num_scopes <= lvl); - unsigned new_lvl = lvl - num_scopes; - scope & s = m_scopes[new_lvl]; - del_atoms(s.m_atoms_lim); - m_asserted_atoms.shrink(s.m_asserted_atoms_lim); - m_asserted_qhead = s.m_asserted_qhead_old; - m_scopes.shrink(new_lvl); - m_graph->pop(num_scopes); - theory::pop_scope_eh(num_scopes); - } - - template - final_check_status theory_horn_ineq::final_check_eh() { - SASSERT(is_consistent()); - TRACE("horn_ineq", display(tout);); - if (can_propagate()) { - propagate_core(); - return FC_CONTINUE; - } - else if (m_non_horn_ineq_exprs) { - return FC_GIVEUP; - } - else { - return FC_DONE; - } - } - - template - void theory_horn_ineq::propagate() { - propagate_core(); - } - - template - void theory_horn_ineq::display(std::ostream& out) const { - for (unsigned i = 0; i < m_atoms.size(); ++i) { - m_atoms[i].display(*this, out); - } - out << "\n"; - m_graph->display(out); - } - - template - void theory_horn_ineq::collect_statistics(::statistics& st) const { - st.update("horn ineq conflicts", m_stats.m_num_conflicts); - st.update("horn ineq assertions", m_stats.m_num_assertions); - m_arith_eq_adapter.collect_statistics(st); - m_graph->collect_statistics(st); - } - - template - void theory_horn_ineq::del_atoms(unsigned old_size) { - typename atoms::iterator begin = m_atoms.begin() + old_size; - typename atoms::iterator it = m_atoms.end(); - while (it != begin) { - --it; - m_bool_var2atom.erase(it->get_bool_var()); - } - m_atoms.shrink(old_size); - } - - template - void theory_horn_ineq::propagate_core() { - bool consistent = true; - while (consistent && can_propagate()) { - unsigned idx = m_asserted_atoms[m_asserted_qhead]; - m_asserted_qhead++; - consistent = propagate_atom(m_atoms[idx]); - } - } - - template - bool theory_horn_ineq::propagate_atom(atom const& a) { - context& ctx = get_context(); - TRACE("horn_ineq", a.display(*this, tout); tout << "\n";); - if (ctx.inconsistent()) { - return false; - } - int clause_id = a.get_asserted_edge(); - if (!m_graph->enable_clause(clause_id)) { - set_neg_cycle_conflict(); - return false; - } - return true; - } - - template - theory_var theory_horn_ineq::mk_term(app* n) { - context& ctx = get_context(); - - horn_ineq_tester::classify_t cl = m_test.linearize(n); - if (cl == horn_ineq_tester::non_horn) { - found_non_horn_ineq_expr(n); - return null_theory_var; - } - - coeffs coeffs; - rational w; - mk_coeffs(m_test.get_linearization(), coeffs, w); - if (coeffs.empty()) { - return mk_num(n, w); - } - if (coeffs.size() == 1 && coeffs[0].second.is_one()) { - return coeffs[0].first; - } - th_var target = mk_var(ctx.mk_enode(n, false, false, true)); - coeffs.push_back(std::make_pair(target, rational(-1))); - - VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal))); - negate(coeffs, w); - VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(w)), null_literal))); - return target; - } - - template - theory_var theory_horn_ineq::mk_num(app* n, rational const& r) { - theory_var v = null_theory_var; - context& ctx = get_context(); - if (r.is_zero()) { - v = a.is_int(n)?m_zero_int:m_zero_real; - } - else if (ctx.e_internalized(n)) { - enode* e = ctx.get_enode(n); - v = e->get_th_var(get_id()); - SASSERT(v != null_theory_var); - } - else { - v = mk_var(ctx.mk_enode(n, false, false, true)); - // v = k: v <= k k <= v - coeffs coeffs; - coeffs.push_back(std::make_pair(v, rational(1))); - VERIFY(m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(r)), null_literal))); - coeffs.back().second.neg(); - VERIFY (m_graph->enable_clause(m_graph->add_ineq(coeffs, numeral(inf_numeral(-r)), null_literal))); - } - return v; - } - - template - theory_var theory_horn_ineq::expand(bool pos, th_var v, rational & k) { - context& ctx = get_context(); - enode* e = get_enode(v); - expr* x, *y; - rational r; - for (;;) { - app* n = e->get_owner(); - if (a.is_add(n, x, y)) { - if (a.is_numeral(x, r)) { - e = ctx.get_enode(y); - } - else if (a.is_numeral(y, r)) { - e = ctx.get_enode(x); - } - v = e->get_th_var(get_id()); - SASSERT(v != null_theory_var); - if (v == null_theory_var) { - break; - } - if (pos) { - k += r; - } - else { - k -= r; - } - } - else { - break; - } - } - return v; - } - - template - bool theory_horn_ineq::is_consistent() const { - return m_graph->is_feasible(); - } - - // models: - template - void theory_horn_ineq::init_model(model_generator & m) { - m_factory = alloc(arith_factory, get_manager()); - m.register_factory(m_factory); - compute_delta(); - } - - template - model_value_proc * theory_horn_ineq::mk_value(enode * n, model_generator & mg) { - theory_var v = n->get_th_var(get_id()); - SASSERT(v != null_theory_var); - numeral val = m_graph->get_assignment(v); - rational num = val.get_infinity()*m_lambda + val.get_rational() + val.get_infinitesimal()*m_delta; - TRACE("horn_ineq", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";); - return alloc(expr_wrapper_proc, m_factory->mk_value(num, a.is_int(n->get_owner()))); - } - - /** - \brief Compute numeral values for the infinitesimals to satisfy the inequalities. - */ - - template - void theory_horn_ineq::compute_delta() { - m_delta = rational(1); - m_lambda = rational(0); - unsigned sz = m_graph->get_num_clauses(); - - for (unsigned i = 0; i < sz; ++i) { - if (!m_graph->get_clause(i).is_enabled()) { - continue; - } - numeral b = m_graph->eval_body(i); - numeral h = m_graph->eval_head(i); - - if (b.get_infinity() < h.get_infinity()) { - continue; - } - SASSERT(b.get_infinity() == h.get_infinity()); - - // b <= h - // suppose that h.eps < b.eps - // then we have h.num > b.num - // but also h.num + delta*h.eps >= b.num + delta*b.eps - // <=> - // (h.num - b.num)/(b.eps - h.eps) >= delta - rational num_r = h.get_rational() - b.get_rational(); - rational eps_r = b.get_infinitesimal() - h.get_infinitesimal(); - if (eps_r.is_pos()) { - SASSERT(num_r.is_pos()); - rational new_delta = num_r/eps_r; - if (new_delta < m_delta) { - m_delta = new_delta; - } - } - } - - for (unsigned i = 0; i < sz; ++i) { - if (!m_graph->get_clause(i).is_enabled()) { - continue; - } - numeral b = m_graph->eval_body(i); - numeral h = m_graph->eval_head(i); - - rational ir = h.get_infinity() - b.get_infinity(); - rational hr = b.get_rational() - h.get_rational(); - rational num_r = hr + m_delta*(b.get_infinitesimal() - h.get_infinitesimal()); - - SASSERT(b.get_infinity() <= h.get_infinity()); - - // b <= h - // suppose that h.finite < b.finite - // then we have h.infinite > b.infinite - // but also - // h.infinite*lambda + h.finite >= b.infinite*lambda + b.finite - // <=> - // lambda >= (b.finite - h.finite) / (h.infinite - b.infinite) - if (num_r.is_pos()) { - SASSERT(ir.is_pos()); - rational new_lambda = num_r/ir; - if (new_lambda > m_lambda) { - m_lambda = new_lambda; - } - } - } - } - - - -}; - -#endif diff --git a/src/tactic/bv/bv_size_reduction_tactic.cpp b/src/tactic/bv/bv_size_reduction_tactic.cpp index d24f506a1..d3fdb6e56 100644 --- a/src/tactic/bv/bv_size_reduction_tactic.cpp +++ b/src/tactic/bv/bv_size_reduction_tactic.cpp @@ -25,6 +25,7 @@ Notes: #include"bv_decl_plugin.h" #include"expr_replacer.h" #include"extension_model_converter.h" +#include"filter_model_converter.h" #include"ast_smt2_pp.h" class bv_size_reduction_tactic : public tactic { @@ -60,6 +61,7 @@ struct bv_size_reduction_tactic::imp { obj_map m_unsigned_lowers; obj_map m_unsigned_uppers; ref m_mc; + ref m_fmc; scoped_ptr m_replacer; bool m_produce_models; volatile bool m_cancel; @@ -121,21 +123,41 @@ struct bv_size_reduction_tactic::imp { negated = true; f = to_app(f)->get_arg(0); } - + if (m_util.is_bv_sle(f, lhs, rhs)) { + bv_sz = m_util.get_bv_size(lhs); if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) { TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; ); // v <= k - if (negated) update_signed_lower(to_app(lhs), val+numeral(1)); + val = m_util.norm(val, bv_sz, true); + if (negated) { + val += numeral(1); + if (m_util.norm(val, bv_sz, true) != val) { + // bound is infeasible. + } + else { + update_signed_lower(to_app(lhs), val); + } + } else update_signed_upper(to_app(lhs), val); } else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, val, bv_sz)) { TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; ); // k <= v - if (negated) update_signed_upper(to_app(rhs), val-numeral(1)); + val = m_util.norm(val, bv_sz, true); + if (negated) { + val -= numeral(1); + if (m_util.norm(val, bv_sz, true) != val) { + // bound is infeasible. + } + else { + update_signed_upper(to_app(lhs), val); + } + } else update_signed_lower(to_app(rhs), val); } } + #if 0 else if (m_util.is_bv_ule(f, lhs, rhs)) { if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) { @@ -196,6 +218,7 @@ struct bv_size_reduction_tactic::imp { numeral u = m_util.norm(entry->get_data().m_value, bv_sz, true); TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";); expr * new_def = 0; + app * new_const = 0; if (l > u) { g.assert_expr(m.mk_false()); return; @@ -208,15 +231,19 @@ struct bv_size_reduction_tactic::imp { if (l.is_neg()) { unsigned i_nb = (u - l).get_num_bits(); unsigned v_nb = m_util.get_bv_size(v); - if (i_nb < v_nb) - new_def = m_util.mk_sign_extend(v_nb - i_nb, m.mk_fresh_const(0, m_util.mk_sort(i_nb))); + if (i_nb < v_nb) { + new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb)); + new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const); + } } else { // 0 <= l <= v <= u unsigned u_nb = u.get_num_bits(); unsigned v_nb = m_util.get_bv_size(v); - if (u_nb < v_nb) - new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb))); + if (u_nb < v_nb) { + new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb)); + new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const); + } } } @@ -226,6 +253,10 @@ struct bv_size_reduction_tactic::imp { if (!m_mc) m_mc = alloc(bv_size_reduction_mc, m); m_mc->insert(v->get_decl(), new_def); + if (!m_fmc && new_const) + m_fmc = alloc(filter_model_converter, m); + if (new_const) + m_fmc->insert(new_const->get_decl()); } num_reduced++; } @@ -264,6 +295,7 @@ struct bv_size_reduction_tactic::imp { TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";); expr * new_def = 0; + app * new_const = 0; if (l > u) { g.assert_expr(m.mk_false()); return; @@ -275,8 +307,10 @@ struct bv_size_reduction_tactic::imp { // 0 <= l <= v <= u unsigned u_nb = u.get_num_bits(); unsigned v_nb = m_util.get_bv_size(v); - if (u_nb < v_nb) - new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb))); + if (u_nb < v_nb) { + new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const); + new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb)); + } } if (new_def) { @@ -285,6 +319,10 @@ struct bv_size_reduction_tactic::imp { if (!m_mc) m_mc = alloc(bv_size_reduction_mc, m); m_mc->insert(v->get_decl(), new_def); + if (!m_fmc && new_const) + m_fmc = alloc(filter_model_converter, m); + if (new_const) + m_fmc->insert(new_const->get_decl()); } num_reduced++; TRACE("bv_size_reduction", tout << "New definition = " << mk_ismt2_pp(new_def, m) << "\n";); @@ -309,7 +347,11 @@ struct bv_size_reduction_tactic::imp { g.update(i, new_f); } mc = m_mc.get(); + if (m_fmc) { + mc = concat(m_fmc.get(), mc.get()); + } m_mc = 0; + m_fmc = 0; } report_tactic_progress(":bv-reduced", num_reduced); TRACE("after_bv_size_reduction", g.display(tout); if (m_mc) m_mc->display(tout);); diff --git a/src/tactic/fpa/qffpa_tactic.cpp b/src/tactic/fpa/qffpa_tactic.cpp index 90cfc8c92..f9b7f88a1 100644 --- a/src/tactic/fpa/qffpa_tactic.cpp +++ b/src/tactic/fpa/qffpa_tactic.cpp @@ -42,7 +42,7 @@ struct is_non_qffpa_predicate { ast_manager & m; float_util u; - is_non_qffpa_predicate(ast_manager & _m) :m(_m), u(m) {} + is_non_qffpa_predicate(ast_manager & _m) : m(_m), u(m) {} void operator()(var *) { throw found(); } @@ -50,13 +50,15 @@ struct is_non_qffpa_predicate { void operator()(app * n) { sort * s = get_sort(n); - if (!m.is_bool(s) && !(u.is_float(s) || u.is_rm(s))) + if (!m.is_bool(s) && !u.is_float(s) && !u.is_rm(s)) throw found(); - family_id fid = s->get_family_id(); + 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(); } @@ -68,7 +70,7 @@ struct is_non_qffpabv_predicate { bv_util bu; float_util fu; - is_non_qffpabv_predicate(ast_manager & _m) :m(_m), bu(m), fu(m) {} + is_non_qffpabv_predicate(ast_manager & _m) : m(_m), bu(m), fu(m) {} void operator()(var *) { throw found(); } @@ -76,13 +78,15 @@ struct is_non_qffpabv_predicate { 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))) + if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s)) throw found(); - family_id fid = s->get_family_id(); + 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(); } diff --git a/src/util/rational.h b/src/util/rational.h index c02a5a2c3..0d8a23e81 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -331,22 +331,13 @@ public: return target; } - friend inline rational gcd(rational const & r1, rational const & r2) { - rational result; - m().gcd(r1.m_val, r2.m_val, result.m_val); - return result; - } + friend inline rational gcd(rational const & r1, rational const & r2); // // extended Euclid: // r1*a + r2*b = gcd // - friend inline rational gcd(rational const & r1, rational const & r2, rational & a, rational & b) { - rational result; - m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val); - return result; - } - + friend inline rational gcd(rational const & r1, rational const & r2, rational & a, rational & b); friend inline rational lcm(rational const & r1, rational const & r2) { rational result; @@ -378,11 +369,7 @@ public: return result; } - friend inline rational abs(rational const & r) { - rational result(r); - m().abs(result.m_val); - return result; - } + friend inline rational abs(rational const & r); rational to_rational() const { return *this; } @@ -446,5 +433,24 @@ inline rational power(rational const & r, unsigned p) { return r.expt(p); } +inline rational abs(rational const & r) { + rational result(r); + rational::m().abs(result.m_val); + return result; +} + +inline rational gcd(rational const & r1, rational const & r2) { + rational result; + rational::m().gcd(r1.m_val, r2.m_val, result.m_val); + return result; +} + +inline rational gcd(rational const & r1, rational const & r2, rational & a, rational & b) { + rational result; + rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val); + return result; +} + + #endif /* _RATIONAL_H_ */