From b6c0b8c9ff3dc85f1e2841e3a88c1569d09584f3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 7 Apr 2014 16:09:22 +0100 Subject: [PATCH 01/17] Compilation fix for FreeBSD --- scripts/mk_util.py | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 883492614..89cabe87e 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -54,6 +54,7 @@ CPP_COMPONENT='cpp' IS_WINDOWS=False IS_LINUX=False IS_OSX=False +IS_FREEBSD=False VERBOSE=True DEBUG_MODE=False SHOW_CPPS = True @@ -98,6 +99,9 @@ def is_windows(): def is_linux(): return IS_LINUX +def is_freebsd(): + return IS_FREEBSD + def is_osx(): return IS_OSX @@ -426,6 +430,8 @@ elif os.name == 'posix': IS_OSX=True elif os.uname()[0] == 'Linux': IS_LINUX=True + elif os.uname()[0] == 'FreeBSD': + IS_FREEBSD=True def display_help(exit_code): print("mk_make.py: Z3 Makefile generator\n") @@ -1181,6 +1187,8 @@ class JavaDLLComponent(Component): t = t.replace('PLATFORM', 'darwin') elif IS_LINUX: t = t.replace('PLATFORM', 'linux') + elif IS_FREEBSD: + t = t.replace('PLATFORM', 'freebsd') else: t = t.replace('PLATFORM', 'win32') out.write(t) From a3b89a8af34b987a368a118790917795f2607581 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 9 Apr 2014 11:24:42 +0100 Subject: [PATCH 02/17] .NET API documentation fixes Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Context.cs | 20 ++++++++++---------- src/api/dotnet/Global.cs | 2 +- src/api/dotnet/Solver.cs | 6 ++++-- 3 files changed, 15 insertions(+), 13 deletions(-) diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 47294244a..41ac1fa31 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -302,11 +302,11 @@ namespace Microsoft.Z3 } /// - /// Create a new finite domain sort. - /// The name used to identify the sort - /// The size of the sort - /// The result is a sort + /// Create a new finite domain sort. + /// The result is a sort /// + /// The name used to identify the sort + /// The size of the sort public FiniteDomainSort MkFiniteDomainSort(Symbol name, ulong size) { Contract.Requires(name != null); @@ -317,13 +317,13 @@ namespace Microsoft.Z3 } /// - /// Create a new finite domain sort. - /// The name used to identify the sort - /// The size of the sort - /// The result is a sort - /// Elements of the sort are created using , - /// and the elements range from 0 to size-1. + /// Create a new finite domain sort. + /// The result is a sort + /// Elements of the sort are created using , + /// and the elements range from 0 to size-1. /// + /// The name used to identify the sort + /// The size of the sort public FiniteDomainSort MkFiniteDomainSort(string name, ulong size) { Contract.Ensures(Contract.Result() != null); diff --git a/src/api/dotnet/Global.cs b/src/api/dotnet/Global.cs index 707264c82..787c9b788 100644 --- a/src/api/dotnet/Global.cs +++ b/src/api/dotnet/Global.cs @@ -43,7 +43,7 @@ namespace Microsoft.Z3 /// The parameter names are case-insensitive. The character '-' should be viewed as an "alias" for '_'. /// Thus, the following parameter names are considered equivalent: "pp.decimal-precision" and "PP.DECIMAL_PRECISION". /// This function can be used to set parameters for a specific Z3 module. - /// This can be done by using .. + /// This can be done by using [module-name].[parameter-name]. /// For example: /// Z3_global_param_set('pp.decimal', 'true') /// will set the parameter "decimal" in the module "pp" to true. diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 555a2466f..9de515e86 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -132,7 +132,8 @@ namespace Microsoft.Z3 /// /// This API is an alternative to with assumptions for extracting unsat cores. /// Both APIs can be used in the same solver. The unsat core will contain a combination - /// of the Boolean variables provided using and the Boolean literals + /// of the Boolean variables provided using + /// and the Boolean literals /// provided using with assumptions. /// public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) @@ -156,7 +157,8 @@ namespace Microsoft.Z3 /// /// This API is an alternative to with assumptions for extracting unsat cores. /// Both APIs can be used in the same solver. The unsat core will contain a combination - /// of the Boolean variables provided using and the Boolean literals + /// of the Boolean variables provided using + /// and the Boolean literals /// provided using with assumptions. /// public void AssertAndTrack(BoolExpr constraint, BoolExpr p) From aa006fa2372bf8b17e0db7d1ae78672b8767c812 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 9 Apr 2014 11:31:44 +0100 Subject: [PATCH 03/17] added dotnet generated files to .gitignore Signed-off-by: Christoph M. Wintersteiger --- .gitignore | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.gitignore b/.gitignore index 77f4d1896..647529b4f 100644 --- a/.gitignore +++ b/.gitignore @@ -55,6 +55,8 @@ src/api/api_log_macros.cpp src/api/dll/api_dll.def src/api/dotnet/Enumerations.cs src/api/dotnet/Native.cs +src/api/dotnet/Properties/AssemblyInfo.cs +src/api/dotnet/Microsoft.Z3.xml src/api/python/z3consts.py src/api/python/z3core.py src/ast/pattern/database.h From 64bfbb657c77c57390d6f5c1603693d77ed230c2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 9 Apr 2014 11:39:05 +0100 Subject: [PATCH 04/17] .NET API documentation XML build fix Signed-off-by: Christoph M. Wintersteiger --- src/api/dotnet/Microsoft.Z3.csproj | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/api/dotnet/Microsoft.Z3.csproj b/src/api/dotnet/Microsoft.Z3.csproj index 9eb9eb660..0a062054d 100644 --- a/src/api/dotnet/Microsoft.Z3.csproj +++ b/src/api/dotnet/Microsoft.Z3.csproj @@ -24,8 +24,7 @@ prompt 4 true - - + ..\Debug\Microsoft.Z3.XML False False True @@ -140,6 +139,7 @@ Full %28none%29 0 + ..\x64\Debug\Microsoft.Z3.XML ..\x64\external_64\ @@ -193,7 +193,7 @@ ..\x64\external\ true - ..\external\Microsoft.Z3.xml + ..\x64\external\Microsoft.Z3.XML true pdbonly x64 @@ -220,7 +220,7 @@ ..\Release_delaysign\ true - ..\Release_delaysign\Microsoft.Z3.xml + ..\Release_delaysign\Microsoft.Z3.XML true pdbonly AnyCPU @@ -238,7 +238,7 @@ bin\x64\Release_delaysign\ true - ..\x64\external_64\Microsoft.Z3.xml + bin\x64\Release_delaysign\Microsoft.Z3.XML true pdbonly x64 @@ -266,11 +266,12 @@ MinimumRecommendedRules.ruleset ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets ;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules + bin\x86\Debug\Microsoft.Z3.XML bin\x86\Release\ true - ..\external\Microsoft.Z3.xml + bin\x86\Release\Microsoft.Z3.xml true pdbonly x86 @@ -285,7 +286,7 @@ bin\x86\external\ true - ..\external\Microsoft.Z3.xml + bin\x86\external\Microsoft.Z3.XML true pdbonly x86 @@ -303,7 +304,7 @@ bin\x86\Release_delaysign\ DELAYSIGN true - ..\Release_delaysign\Microsoft.Z3.xml + bin\x86\Release_delaysign\Microsoft.Z3.XML true pdbonly x86 @@ -399,4 +400,4 @@ --> - + \ No newline at end of file From 52b54f395b88926703ed390b04ea7767bbadacd3 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 10 Apr 2014 19:33:34 +0100 Subject: [PATCH 05/17] FPA division bugfix Signed-off-by: Christoph M. Wintersteiger --- src/tactic/fpa/fpa2bv_converter.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/tactic/fpa/fpa2bv_converter.cpp index 2d1d6705f..533988689 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/tactic/fpa/fpa2bv_converter.cpp @@ -872,8 +872,19 @@ void fpa2bv_converter::mk_div(func_decl * f, unsigned num, expr * const * args, sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, m_bv_util.mk_extract(extra_bits-2, 0, quotient)); res_sig = m_bv_util.mk_concat(m_bv_util.mk_extract(extra_bits+sbits+1, extra_bits-1, quotient), sticky); - SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4)); + SASSERT(m_bv_util.get_bv_size(res_sig) == (sbits + 4)); + expr_ref res_sig_lz(m); + mk_leading_zeros(res_sig, sbits + 4, res_sig_lz); + dbg_decouple("fpa2bv_div_res_sig_lz", res_sig_lz); + expr_ref res_sig_shift_amount(m); + res_sig_shift_amount = m_bv_util.mk_bv_sub(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4)); + dbg_decouple("fpa2bv_div_res_sig_shift_amount", res_sig_shift_amount); + expr_ref shift_cond(m); + shift_cond = m_bv_util.mk_ule(res_sig_lz, m_bv_util.mk_numeral(1, sbits + 4)); + m_simp.mk_ite(shift_cond, res_sig, m_bv_util.mk_bv_shl(res_sig, res_sig_shift_amount), res_sig); + m_simp.mk_ite(shift_cond, res_exp, m_bv_util.mk_bv_sub(res_exp, m_bv_util.mk_extract(ebits+1, 0, res_sig_shift_amount)), res_exp); + round(f->get_range(), rm, res_sgn, res_sig, res_exp, v8); // And finally, we tie them together. From 7d16ed9fdceb73af43843404834f8daee459f85d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 23 Apr 2014 14:13:01 +0200 Subject: [PATCH 06/17] fix exception class in python API Signed-off-by: Nikolaj Bjorner --- src/api/python/z3printer.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py index d3dc43d3e..d1d85d30e 100644 --- a/src/api/python/z3printer.py +++ b/src/api/python/z3printer.py @@ -386,7 +386,7 @@ def seq3(args, lp='(', rp=')'): else: return group(indent(len(lp), compose(to_format(lp), seq(args), to_format(rp)))) -class StopPPException: +class StopPPException(Exception): def __str__(self): return 'pp-interrupted' From fb4c07a2ea336ad62fbfce3e4f49579fa088cdef Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 23 Apr 2014 18:36:38 +0100 Subject: [PATCH 07/17] FPA refactoring in preparation for FPA support in the kernel. Signed-off-by: Christoph M. Wintersteiger --- scripts/mk_project.py | 7 +- src/{tactic => ast}/fpa/fpa2bv_converter.cpp | 212 ----------------- src/{tactic => ast}/fpa/fpa2bv_converter.h | 85 ------- src/{tactic => ast}/fpa/fpa2bv_rewriter.h | 0 src/smt/theory_fpa.cpp | 46 ++++ src/smt/theory_fpa.h | 45 ++++ src/tactic/fpa/fpa2bv_model_converter.cpp | 232 +++++++++++++++++++ src/tactic/fpa/fpa2bv_model_converter.h | 106 +++++++++ src/tactic/fpa/fpa2bv_tactic.cpp | 1 + 9 files changed, 434 insertions(+), 300 deletions(-) rename src/{tactic => ast}/fpa/fpa2bv_converter.cpp (92%) rename src/{tactic => ast}/fpa/fpa2bv_converter.h (72%) rename src/{tactic => ast}/fpa/fpa2bv_rewriter.h (100%) create mode 100644 src/smt/theory_fpa.cpp create mode 100644 src/smt/theory_fpa.h create mode 100644 src/tactic/fpa/fpa2bv_model_converter.cpp create mode 100644 src/tactic/fpa/fpa2bv_model_converter.h diff --git a/scripts/mk_project.py b/scripts/mk_project.py index f2c688525..6f8fe1f7f 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -42,17 +42,18 @@ def init_project_def(): # Simplifier module will be deleted in the future. # It has been replaced with rewriter module. add_lib('simplifier', ['rewriter'], 'ast/simplifier') + add_lib('fpa', ['ast', 'util', 'simplifier'], 'ast/fpa') add_lib('macros', ['simplifier'], 'ast/macros') add_lib('pattern', ['normal_forms', 'smt2parser', 'simplifier'], 'ast/pattern') add_lib('bit_blaster', ['rewriter', 'simplifier'], 'ast/rewriter/bit_blaster') add_lib('smt_params', ['ast', 'simplifier', 'pattern', 'bit_blaster'], 'smt/params') add_lib('proto_model', ['model', 'simplifier', 'smt_params'], 'smt/proto_model') add_lib('smt', ['bit_blaster', 'macros', 'normal_forms', 'cmd_context', 'proto_model', - 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util']) + 'substitution', 'grobner', 'euclid', 'proof_checker', 'pattern', 'parser_util', 'fpa']) add_lib('user_plugin', ['smt'], 'smt/user_plugin') add_lib('bv_tactics', ['tactic', 'bit_blaster'], 'tactic/bv') add_lib('fuzzing', ['ast'], 'test/fuzzing') - add_lib('fpa', ['core_tactics', 'bv_tactics', 'sat_tactic'], 'tactic/fpa') + add_lib('fpa_tactics', ['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('qe', ['smt','sat'], 'qe') @@ -68,7 +69,7 @@ def init_project_def(): add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf'], 'muz/fp') add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics') add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv') - add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') + add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio') add_lib('smtparser', ['portfolio'], 'parsers/smt') # add_dll('foci2', ['util'], 'interp/foci2stub', # dll_name='foci2', diff --git a/src/tactic/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp similarity index 92% rename from src/tactic/fpa/fpa2bv_converter.cpp rename to src/ast/fpa/fpa2bv_converter.cpp index 533988689..20925a0f9 100644 --- a/src/tactic/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -2754,215 +2754,3 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; ); } - -void fpa2bv_model_converter::display(std::ostream & out) { - out << "(fpa2bv-model-converter"; - for (obj_map::iterator it = m_const2bv.begin(); - it != m_const2bv.end(); - it++) { - const symbol & n = it->m_key->get_name(); - out << "\n (" << n << " "; - unsigned indent = n.size() + 4; - out << mk_ismt2_pp(it->m_value, m, indent) << ")"; - } - for (obj_map::iterator it = m_rm_const2bv.begin(); - it != m_rm_const2bv.end(); - it++) { - const symbol & n = it->m_key->get_name(); - out << "\n (" << n << " "; - unsigned indent = n.size() + 4; - out << mk_ismt2_pp(it->m_value, m, indent) << ")"; - } - for (obj_map::iterator it = m_uf2bvuf.begin(); - it != m_uf2bvuf.end(); - it++) { - const symbol & n = it->m_key->get_name(); - out << "\n (" << n << " "; - unsigned indent = n.size() + 4; - out << mk_ismt2_pp(it->m_value, m, indent) << ")"; - } - for (obj_map::iterator it = m_uf23bvuf.begin(); - it != m_uf23bvuf.end(); - it++) { - const symbol & n = it->m_key->get_name(); - out << "\n (" << n << " "; - unsigned indent = n.size() + 4; - out << mk_ismt2_pp(it->m_value.f_sgn, m, indent) << " ; " << - mk_ismt2_pp(it->m_value.f_sig, m, indent) << " ; " << - mk_ismt2_pp(it->m_value.f_exp, m, indent) << " ; " << - ")"; - } - out << ")" << std::endl; -} - -model_converter * fpa2bv_model_converter::translate(ast_translation & translator) { - fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to()); - for (obj_map::iterator it = m_const2bv.begin(); - it != m_const2bv.end(); - it++) - { - func_decl * k = translator(it->m_key); - expr * v = translator(it->m_value); - res->m_const2bv.insert(k, v); - translator.to().inc_ref(k); - translator.to().inc_ref(v); - } - for (obj_map::iterator it = m_rm_const2bv.begin(); - it != m_rm_const2bv.end(); - it++) - { - func_decl * k = translator(it->m_key); - expr * v = translator(it->m_value); - res->m_rm_const2bv.insert(k, v); - translator.to().inc_ref(k); - translator.to().inc_ref(v); - } - return res; -} - -void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { - float_util fu(m); - bv_util bu(m); - mpf fp_val; - unsynch_mpz_manager & mpzm = fu.fm().mpz_manager(); - unsynch_mpq_manager & mpqm = fu.fm().mpq_manager(); - - TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl; - for (unsigned i = 0 ; i < bv_mdl->get_num_constants(); i++) - tout << bv_mdl->get_constant(i)->get_name() << " --> " << - mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl; - ); - - obj_hashtable seen; - - for (obj_map::iterator it = m_const2bv.begin(); - it != m_const2bv.end(); - it++) - { - func_decl * var = it->m_key; - app * a = to_app(it->m_value); - SASSERT(fu.is_float(var->get_range())); - SASSERT(var->get_range()->get_num_parameters() == 2); - - unsigned ebits = fu.get_ebits(var->get_range()); - unsigned sbits = fu.get_sbits(var->get_range()); - - expr_ref sgn(m), sig(m), exp(m); - sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl()); - sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl()); - exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl()); - - seen.insert(to_app(a->get_arg(0))->get_decl()); - seen.insert(to_app(a->get_arg(1))->get_decl()); - seen.insert(to_app(a->get_arg(2))->get_decl()); - - if (!sgn && !sig && !exp) - continue; - - unsigned sgn_sz = bu.get_bv_size(m.get_sort(a->get_arg(0))); - unsigned sig_sz = bu.get_bv_size(m.get_sort(a->get_arg(1))) - 1; - unsigned exp_sz = bu.get_bv_size(m.get_sort(a->get_arg(2))); - - rational sgn_q(0), sig_q(0), exp_q(0); - - if (sgn) bu.is_numeral(sgn, sgn_q, sgn_sz); - if (sig) bu.is_numeral(sig, sig_q, sig_sz); - if (exp) bu.is_numeral(exp, exp_q, exp_sz); - - // un-bias exponent - rational exp_unbiased_q; - exp_unbiased_q = exp_q - fu.fm().m_powers2.m1(ebits-1); - - mpz sig_z; mpf_exp_t exp_z; - mpzm.set(sig_z, sig_q.to_mpq().numerator()); - exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator()); - - TRACE("fpa2bv_mc", tout << var->get_name() << " == [" << sgn_q.to_string() << " " << - mpzm.to_string(sig_z) << " " << exp_z << "(" << exp_q.to_string() << ")]" << std::endl; ); - - fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z); - - float_mdl->register_decl(var, fu.mk_value(fp_val)); - - mpzm.del(sig_z); - } - - for (obj_map::iterator it = m_rm_const2bv.begin(); - it != m_rm_const2bv.end(); - it++) - { - func_decl * var = it->m_key; - app * a = to_app(it->m_value); - SASSERT(fu.is_rm(var->get_range())); - rational val(0); - unsigned sz = 0; - if (a && bu.is_numeral(a, val, sz)) { - TRACE("fpa2bv_mc", tout << var->get_name() << " == " << val.to_string() << std::endl; ); - SASSERT(val.is_uint64()); - switch (val.get_uint64()) - { - case BV_RM_TIES_TO_AWAY: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_away()); break; - case BV_RM_TIES_TO_EVEN: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_even()); break; - case BV_RM_TO_NEGATIVE: float_mdl->register_decl(var, fu.mk_round_toward_negative()); break; - case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break; - case BV_RM_TO_ZERO: - default: float_mdl->register_decl(var, fu.mk_round_toward_zero()); - } - seen.insert(var); - } - } - - for (obj_map::iterator it = m_uf2bvuf.begin(); - it != m_uf2bvuf.end(); - it++) - seen.insert(it->m_value); - - for (obj_map::iterator it = m_uf23bvuf.begin(); - it != m_uf23bvuf.end(); - it++) - { - seen.insert(it->m_value.f_sgn); - seen.insert(it->m_value.f_sig); - seen.insert(it->m_value.f_exp); - } - - fu.fm().del(fp_val); - - // Keep all the non-float constants. - unsigned sz = bv_mdl->get_num_constants(); - for (unsigned i = 0; i < sz; i++) - { - func_decl * c = bv_mdl->get_constant(i); - if (!seen.contains(c)) - float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); - } - - // And keep everything else - sz = bv_mdl->get_num_functions(); - for (unsigned i = 0; i < sz; i++) - { - func_decl * f = bv_mdl->get_function(i); - if (!seen.contains(f)) - { - TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl; ); - func_interp * val = bv_mdl->get_func_interp(f); - float_mdl->register_decl(f, val); - } - } - - sz = bv_mdl->get_num_uninterpreted_sorts(); - for (unsigned i = 0; i < sz; i++) - { - sort * s = bv_mdl->get_uninterpreted_sort(i); - ptr_vector u = bv_mdl->get_universe(s); - float_mdl->register_usort(s, u.size(), u.c_ptr()); - } -} - -model_converter * mk_fpa2bv_model_converter(ast_manager & m, - obj_map const & const2bv, - obj_map const & rm_const2bv, - obj_map const & uf2bvuf, - obj_map const & uf23bvuf) { - return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf); -} diff --git a/src/tactic/fpa/fpa2bv_converter.h b/src/ast/fpa/fpa2bv_converter.h similarity index 72% rename from src/tactic/fpa/fpa2bv_converter.h rename to src/ast/fpa/fpa2bv_converter.h index 79c8039ef..2ccdac6a9 100644 --- a/src/tactic/fpa/fpa2bv_converter.h +++ b/src/ast/fpa/fpa2bv_converter.h @@ -24,13 +24,10 @@ Notes: #include"ref_util.h" #include"float_decl_plugin.h" #include"bv_decl_plugin.h" -#include"model_converter.h" #include"basic_simplifier_plugin.h" typedef enum { BV_RM_TIES_TO_AWAY=0, BV_RM_TIES_TO_EVEN=1, BV_RM_TO_NEGATIVE=2, BV_RM_TO_POSITIVE=3, BV_RM_TO_ZERO=4 } BV_RM_VAL; -class fpa2bv_model_converter; - struct func_decl_triple { func_decl_triple () { f_sgn = 0; f_sig = 0; f_exp = 0; } func_decl_triple (func_decl * sgn, func_decl * sig, func_decl * exp) @@ -173,86 +170,4 @@ protected: expr_ref & res_sgn, expr_ref & res_sig, expr_ref & res_exp); }; - -class fpa2bv_model_converter : public model_converter { - ast_manager & m; - obj_map m_const2bv; - obj_map m_rm_const2bv; - obj_map m_uf2bvuf; - obj_map m_uf23bvuf; - -public: - fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, - obj_map const & rm_const2bv, - obj_map const & uf2bvuf, - obj_map const & uf23bvuf) : - m(m) { - // Just create a copy? - for (obj_map::iterator it = const2bv.begin(); - it != const2bv.end(); - it++) - { - m_const2bv.insert(it->m_key, it->m_value); - m.inc_ref(it->m_key); - m.inc_ref(it->m_value); - } - for (obj_map::iterator it = rm_const2bv.begin(); - it != rm_const2bv.end(); - it++) - { - m_rm_const2bv.insert(it->m_key, it->m_value); - m.inc_ref(it->m_key); - m.inc_ref(it->m_value); - } - for (obj_map::iterator it = uf2bvuf.begin(); - it != uf2bvuf.end(); - it++) - { - m_uf2bvuf.insert(it->m_key, it->m_value); - m.inc_ref(it->m_key); - m.inc_ref(it->m_value); - } - for (obj_map::iterator it = uf23bvuf.begin(); - it != uf23bvuf.end(); - it++) - { - m_uf23bvuf.insert(it->m_key, it->m_value); - m.inc_ref(it->m_key); - } - } - - virtual ~fpa2bv_model_converter() { - dec_ref_map_key_values(m, m_const2bv); - dec_ref_map_key_values(m, m_rm_const2bv); - } - - virtual void operator()(model_ref & md, unsigned goal_idx) { - SASSERT(goal_idx == 0); - model * new_model = alloc(model, m); - obj_hashtable bits; - convert(md.get(), new_model); - md = new_model; - } - - virtual void operator()(model_ref & md) { - operator()(md, 0); - } - - void display(std::ostream & out); - - virtual model_converter * translate(ast_translation & translator); - -protected: - fpa2bv_model_converter(ast_manager & m) : m(m) { } - - void convert(model * bv_mdl, model * float_mdl); -}; - - -model_converter * mk_fpa2bv_model_converter(ast_manager & m, - obj_map const & const2bv, - obj_map const & rm_const2bv, - obj_map const & uf2bvuf, - obj_map const & uf23bvuf); - #endif diff --git a/src/tactic/fpa/fpa2bv_rewriter.h b/src/ast/fpa/fpa2bv_rewriter.h similarity index 100% rename from src/tactic/fpa/fpa2bv_rewriter.h rename to src/ast/fpa/fpa2bv_rewriter.h diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp new file mode 100644 index 000000000..147d87496 --- /dev/null +++ b/src/smt/theory_fpa.cpp @@ -0,0 +1,46 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + theory_fpa.cpp + +Abstract: + + Floating-Point Theory Plugin + +Author: + + Christoph (cwinter) 2014-04-23 + +Revision History: + +--*/ +#include"ast_smt2_pp.h" +#include"theory_fpa.h" + +namespace smt { + + bool theory_fpa::internalize_atom(app * atom, bool gate_ctx) { + TRACE("bv", tout << "internalizing atom: " << mk_ismt2_pp(atom, get_manager()) << "\n";); + SASSERT(atom->get_family_id() == get_family_id()); + NOT_IMPLEMENTED_YET(); + return true; + } + + void theory_fpa::new_eq_eh(theory_var, theory_var) { + NOT_IMPLEMENTED_YET(); + } + + void theory_fpa::new_diseq_eh(theory_var, theory_var) { + NOT_IMPLEMENTED_YET(); + } + + void theory_fpa::push_scope_eh() { + NOT_IMPLEMENTED_YET(); + } + + void theory_fpa::pop_scope_eh(unsigned num_scopes) { + NOT_IMPLEMENTED_YET(); + } +}; diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h new file mode 100644 index 000000000..3716247d3 --- /dev/null +++ b/src/smt/theory_fpa.h @@ -0,0 +1,45 @@ +/*++ +Copyright (c) 2014 Microsoft Corporation + +Module Name: + + theory_fpa.h + +Abstract: + + Floating-Point Theory Plugin + +Author: + + Christoph (cwinter) 2014-04-23 + +Revision History: + +--*/ +#ifndef _THEORY_FPA_H_ +#define _THEORY_FPA_H_ + +#include"smt_theory.h" +#include"fpa2bv_converter.h" + +namespace smt { + class theory_fpa : public theory { + fpa2bv_converter m_converter; + + virtual final_check_status final_check_eh() { return FC_DONE; } + virtual bool internalize_atom(app*, bool); + virtual bool internalize_term(app*) { return internalize_atom(0, false); } + virtual void new_eq_eh(theory_var, theory_var); + virtual void new_diseq_eh(theory_var, theory_var); + virtual void push_scope_eh(); + virtual void pop_scope_eh(unsigned num_scopes); + virtual theory* mk_fresh(context*) { return alloc(theory_fpa, get_manager()); } + virtual char const * get_name() const { return "fpa"; } + public: + theory_fpa(ast_manager& m) : theory(m.mk_family_id("fpa")), m_converter(m) {} + }; + +}; + +#endif /* _THEORY_FPA_H_ */ + diff --git a/src/tactic/fpa/fpa2bv_model_converter.cpp b/src/tactic/fpa/fpa2bv_model_converter.cpp new file mode 100644 index 000000000..9b4b5a70f --- /dev/null +++ b/src/tactic/fpa/fpa2bv_model_converter.cpp @@ -0,0 +1,232 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + fpa2bv_model_converter.h + +Abstract: + + Model conversion for fpa2bv_converter + +Author: + + Christoph (cwinter) 2012-02-09 + +Notes: + +--*/ +#include"ast_smt2_pp.h" +#include"fpa2bv_model_converter.h" + +void fpa2bv_model_converter::display(std::ostream & out) { + out << "(fpa2bv-model-converter"; + for (obj_map::iterator it = m_const2bv.begin(); + it != m_const2bv.end(); + it++) { + const symbol & n = it->m_key->get_name(); + out << "\n (" << n << " "; + unsigned indent = n.size() + 4; + out << mk_ismt2_pp(it->m_value, m, indent) << ")"; + } + for (obj_map::iterator it = m_rm_const2bv.begin(); + it != m_rm_const2bv.end(); + it++) { + const symbol & n = it->m_key->get_name(); + out << "\n (" << n << " "; + unsigned indent = n.size() + 4; + out << mk_ismt2_pp(it->m_value, m, indent) << ")"; + } + for (obj_map::iterator it = m_uf2bvuf.begin(); + it != m_uf2bvuf.end(); + it++) { + const symbol & n = it->m_key->get_name(); + out << "\n (" << n << " "; + unsigned indent = n.size() + 4; + out << mk_ismt2_pp(it->m_value, m, indent) << ")"; + } + for (obj_map::iterator it = m_uf23bvuf.begin(); + it != m_uf23bvuf.end(); + it++) { + const symbol & n = it->m_key->get_name(); + out << "\n (" << n << " "; + unsigned indent = n.size() + 4; + out << mk_ismt2_pp(it->m_value.f_sgn, m, indent) << " ; " << + mk_ismt2_pp(it->m_value.f_sig, m, indent) << " ; " << + mk_ismt2_pp(it->m_value.f_exp, m, indent) << " ; " << + ")"; + } + out << ")" << std::endl; +} + +model_converter * fpa2bv_model_converter::translate(ast_translation & translator) { + fpa2bv_model_converter * res = alloc(fpa2bv_model_converter, translator.to()); + for (obj_map::iterator it = m_const2bv.begin(); + it != m_const2bv.end(); + it++) + { + func_decl * k = translator(it->m_key); + expr * v = translator(it->m_value); + res->m_const2bv.insert(k, v); + translator.to().inc_ref(k); + translator.to().inc_ref(v); + } + for (obj_map::iterator it = m_rm_const2bv.begin(); + it != m_rm_const2bv.end(); + it++) + { + func_decl * k = translator(it->m_key); + expr * v = translator(it->m_value); + res->m_rm_const2bv.insert(k, v); + translator.to().inc_ref(k); + translator.to().inc_ref(v); + } + return res; +} + +void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) { + float_util fu(m); + bv_util bu(m); + mpf fp_val; + unsynch_mpz_manager & mpzm = fu.fm().mpz_manager(); + unsynch_mpq_manager & mpqm = fu.fm().mpq_manager(); + + TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl; + for (unsigned i = 0; i < bv_mdl->get_num_constants(); i++) + tout << bv_mdl->get_constant(i)->get_name() << " --> " << + mk_ismt2_pp(bv_mdl->get_const_interp(bv_mdl->get_constant(i)), m) << std::endl; + ); + + obj_hashtable seen; + + for (obj_map::iterator it = m_const2bv.begin(); + it != m_const2bv.end(); + it++) + { + func_decl * var = it->m_key; + app * a = to_app(it->m_value); + SASSERT(fu.is_float(var->get_range())); + SASSERT(var->get_range()->get_num_parameters() == 2); + + unsigned ebits = fu.get_ebits(var->get_range()); + unsigned sbits = fu.get_sbits(var->get_range()); + + expr_ref sgn(m), sig(m), exp(m); + sgn = bv_mdl->get_const_interp(to_app(a->get_arg(0))->get_decl()); + sig = bv_mdl->get_const_interp(to_app(a->get_arg(1))->get_decl()); + exp = bv_mdl->get_const_interp(to_app(a->get_arg(2))->get_decl()); + + seen.insert(to_app(a->get_arg(0))->get_decl()); + seen.insert(to_app(a->get_arg(1))->get_decl()); + seen.insert(to_app(a->get_arg(2))->get_decl()); + + if (!sgn && !sig && !exp) + continue; + + unsigned sgn_sz = bu.get_bv_size(m.get_sort(a->get_arg(0))); + unsigned sig_sz = bu.get_bv_size(m.get_sort(a->get_arg(1))) - 1; + unsigned exp_sz = bu.get_bv_size(m.get_sort(a->get_arg(2))); + + rational sgn_q(0), sig_q(0), exp_q(0); + + if (sgn) bu.is_numeral(sgn, sgn_q, sgn_sz); + if (sig) bu.is_numeral(sig, sig_q, sig_sz); + if (exp) bu.is_numeral(exp, exp_q, exp_sz); + + // un-bias exponent + rational exp_unbiased_q; + exp_unbiased_q = exp_q - fu.fm().m_powers2.m1(ebits - 1); + + mpz sig_z; mpf_exp_t exp_z; + mpzm.set(sig_z, sig_q.to_mpq().numerator()); + exp_z = mpzm.get_int64(exp_unbiased_q.to_mpq().numerator()); + + TRACE("fpa2bv_mc", tout << var->get_name() << " == [" << sgn_q.to_string() << " " << + mpzm.to_string(sig_z) << " " << exp_z << "(" << exp_q.to_string() << ")]" << std::endl;); + + fu.fm().set(fp_val, ebits, sbits, !mpqm.is_zero(sgn_q.to_mpq()), sig_z, exp_z); + + float_mdl->register_decl(var, fu.mk_value(fp_val)); + + mpzm.del(sig_z); + } + + for (obj_map::iterator it = m_rm_const2bv.begin(); + it != m_rm_const2bv.end(); + it++) + { + func_decl * var = it->m_key; + app * a = to_app(it->m_value); + SASSERT(fu.is_rm(var->get_range())); + rational val(0); + unsigned sz = 0; + if (a && bu.is_numeral(a, val, sz)) { + TRACE("fpa2bv_mc", tout << var->get_name() << " == " << val.to_string() << std::endl;); + SASSERT(val.is_uint64()); + switch (val.get_uint64()) + { + case BV_RM_TIES_TO_AWAY: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_away()); break; + case BV_RM_TIES_TO_EVEN: float_mdl->register_decl(var, fu.mk_round_nearest_ties_to_even()); break; + case BV_RM_TO_NEGATIVE: float_mdl->register_decl(var, fu.mk_round_toward_negative()); break; + case BV_RM_TO_POSITIVE: float_mdl->register_decl(var, fu.mk_round_toward_positive()); break; + case BV_RM_TO_ZERO: + default: float_mdl->register_decl(var, fu.mk_round_toward_zero()); + } + seen.insert(var); + } + } + + for (obj_map::iterator it = m_uf2bvuf.begin(); + it != m_uf2bvuf.end(); + it++) + seen.insert(it->m_value); + + for (obj_map::iterator it = m_uf23bvuf.begin(); + it != m_uf23bvuf.end(); + it++) + { + seen.insert(it->m_value.f_sgn); + seen.insert(it->m_value.f_sig); + seen.insert(it->m_value.f_exp); + } + + fu.fm().del(fp_val); + + // Keep all the non-float constants. + unsigned sz = bv_mdl->get_num_constants(); + for (unsigned i = 0; i < sz; i++) + { + func_decl * c = bv_mdl->get_constant(i); + if (!seen.contains(c)) + float_mdl->register_decl(c, bv_mdl->get_const_interp(c)); + } + + // And keep everything else + sz = bv_mdl->get_num_functions(); + for (unsigned i = 0; i < sz; i++) + { + func_decl * f = bv_mdl->get_function(i); + if (!seen.contains(f)) + { + TRACE("fpa2bv_mc", tout << "Keeping: " << mk_ismt2_pp(f, m) << std::endl;); + func_interp * val = bv_mdl->get_func_interp(f); + float_mdl->register_decl(f, val); + } + } + + sz = bv_mdl->get_num_uninterpreted_sorts(); + for (unsigned i = 0; i < sz; i++) + { + sort * s = bv_mdl->get_uninterpreted_sort(i); + ptr_vector u = bv_mdl->get_universe(s); + float_mdl->register_usort(s, u.size(), u.c_ptr()); + } +} + +model_converter * mk_fpa2bv_model_converter(ast_manager & m, + obj_map const & const2bv, + obj_map const & rm_const2bv, + obj_map const & uf2bvuf, + obj_map const & uf23bvuf) { + return alloc(fpa2bv_model_converter, m, const2bv, rm_const2bv, uf2bvuf, uf23bvuf); +} diff --git a/src/tactic/fpa/fpa2bv_model_converter.h b/src/tactic/fpa/fpa2bv_model_converter.h new file mode 100644 index 000000000..7b9598740 --- /dev/null +++ b/src/tactic/fpa/fpa2bv_model_converter.h @@ -0,0 +1,106 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + fpa2bv_model_converter.h + +Abstract: + + Model conversion for fpa2bv_converter + +Author: + + Christoph (cwinter) 2012-02-09 + +Notes: + +--*/ +#ifndef _FPA2BV_MODEL_CONVERTER_H_ +#define _FPA2BV_MODEL_CONVERTER_H_ + +#include"fpa2bv_converter.h" +#include"model_converter.h" + +class fpa2bv_model_converter : public model_converter { + ast_manager & m; + obj_map m_const2bv; + obj_map m_rm_const2bv; + obj_map m_uf2bvuf; + obj_map m_uf23bvuf; + +public: + fpa2bv_model_converter(ast_manager & m, obj_map const & const2bv, + obj_map const & rm_const2bv, + obj_map const & uf2bvuf, + obj_map const & uf23bvuf) : + m(m) { + // Just create a copy? + for (obj_map::iterator it = const2bv.begin(); + it != const2bv.end(); + it++) + { + m_const2bv.insert(it->m_key, it->m_value); + m.inc_ref(it->m_key); + m.inc_ref(it->m_value); + } + for (obj_map::iterator it = rm_const2bv.begin(); + it != rm_const2bv.end(); + it++) + { + m_rm_const2bv.insert(it->m_key, it->m_value); + m.inc_ref(it->m_key); + m.inc_ref(it->m_value); + } + for (obj_map::iterator it = uf2bvuf.begin(); + it != uf2bvuf.end(); + it++) + { + m_uf2bvuf.insert(it->m_key, it->m_value); + m.inc_ref(it->m_key); + m.inc_ref(it->m_value); + } + for (obj_map::iterator it = uf23bvuf.begin(); + it != uf23bvuf.end(); + it++) + { + m_uf23bvuf.insert(it->m_key, it->m_value); + m.inc_ref(it->m_key); + } + } + + virtual ~fpa2bv_model_converter() { + dec_ref_map_key_values(m, m_const2bv); + dec_ref_map_key_values(m, m_rm_const2bv); + } + + virtual void operator()(model_ref & md, unsigned goal_idx) { + SASSERT(goal_idx == 0); + model * new_model = alloc(model, m); + obj_hashtable bits; + convert(md.get(), new_model); + md = new_model; + } + + virtual void operator()(model_ref & md) { + operator()(md, 0); + } + + void display(std::ostream & out); + + virtual model_converter * translate(ast_translation & translator); + +protected: + fpa2bv_model_converter(ast_manager & m) : m(m) { } + + void convert(model * bv_mdl, model * float_mdl); +}; + + +model_converter * mk_fpa2bv_model_converter(ast_manager & m, + obj_map const & const2bv, + obj_map const & rm_const2bv, + obj_map const & uf2bvuf, + obj_map const & uf23bvuf); + +#endif \ No newline at end of file diff --git a/src/tactic/fpa/fpa2bv_tactic.cpp b/src/tactic/fpa/fpa2bv_tactic.cpp index 9bb35eea6..3a6b7ea45 100644 --- a/src/tactic/fpa/fpa2bv_tactic.cpp +++ b/src/tactic/fpa/fpa2bv_tactic.cpp @@ -20,6 +20,7 @@ Notes: #include"fpa2bv_rewriter.h" #include"simplify_tactic.h" #include"fpa2bv_tactic.h" +#include"fpa2bv_model_converter.h" class fpa2bv_tactic : public tactic { struct imp { From a5ce28d82ab2e3cf71f59be61d1ef78c346c0738 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 25 Apr 2014 22:10:53 +0100 Subject: [PATCH 08/17] bugfix Signed-off-by: Christoph M. Wintersteiger --- src/math/polynomial/upolynomial_factorization.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/polynomial/upolynomial_factorization.cpp b/src/math/polynomial/upolynomial_factorization.cpp index 230d352f3..7d5a23d99 100644 --- a/src/math/polynomial/upolynomial_factorization.cpp +++ b/src/math/polynomial/upolynomial_factorization.cpp @@ -530,7 +530,7 @@ bool check_hansel_lift(z_manager & upm, numeral_vector const & C, upm.mul(A_lifted.size(), A_lifted.c_ptr(), B_lifted.size(), B_lifted.c_ptr(), test1); upm.sub(C.size(), C.c_ptr(), test1.size(), test1.c_ptr(), test1); to_zp_manager(br_upm, test1); - if (!test1.size() == 0) { + if (test1.size() != 0) { TRACE("polynomial::factorization::bughunt", tout << "sage: R. = ZZ['x']" << endl; tout << "sage: A = "; upm.display(tout, A); tout << endl; From 769b2b585bcab0d82b783acf1214f38ccf153724 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 2 May 2014 16:43:32 +0100 Subject: [PATCH 09/17] fixed typo Signed-off-by: Christoph M. Wintersteiger --- src/ast/scoped_proof.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/scoped_proof.h b/src/ast/scoped_proof.h index e37290c03..e23a6d92a 100644 --- a/src/ast/scoped_proof.h +++ b/src/ast/scoped_proof.h @@ -17,7 +17,7 @@ Revision History: --*/ #ifndef _SCOPED_PROOF__H_ -#define _SCOPED_PROOF_H_ +#define _SCOPED_PROOF__H_ #include "ast.h" From 8150bd56174177a3bfda6b554bcff9e294ce07c8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 2 May 2014 17:58:17 +0100 Subject: [PATCH 10/17] OSX timeout handling bugfix --- src/util/scoped_timer.cpp | 64 ++++++++++++++++++++++++--------------- 1 file changed, 39 insertions(+), 25 deletions(-) diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index d0a79cec6..66c321267 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -70,7 +70,9 @@ struct scoped_timer::imp { pthread_t m_thread_id; pthread_attr_t m_attributes; unsigned m_interval; + pthread_mutex_t m_mutex; pthread_cond_t m_condition_var; + struct timespec m_end_time; #elif defined(_LINUX_) || defined(_FREEBSD_) // Linux & FreeBSD timer_t m_timerid; @@ -93,35 +95,15 @@ struct scoped_timer::imp { static void * thread_func(void * arg) { scoped_timer::imp * st = static_cast(arg); - pthread_mutex_t mutex; - clock_serv_t host_clock; - struct timespec abstime; - mach_timespec_t now; - unsigned long long nano = static_cast(st->m_interval) * 1000000ull; + pthread_mutex_lock(&st->m_mutex); - host_get_clock_service(mach_host_self(), CALENDAR_CLOCK, &host_clock); - - if (pthread_mutex_init(&mutex, NULL) != 0) - throw default_exception("failed to initialize timer mutex"); - if (pthread_cond_init(&st->m_condition_var, NULL) != 0) - throw default_exception("failed to initialize timer condition variable"); - - abstime.tv_sec = nano / 1000000000ull; - abstime.tv_nsec = nano % 1000000000ull; - - pthread_mutex_lock(&mutex); - clock_get_time(host_clock, &now); - ADD_MACH_TIMESPEC(&abstime, &now); - int e = pthread_cond_timedwait(&st->m_condition_var, &mutex, &abstime); + int e = pthread_cond_timedwait(&st->m_condition_var, &st->m_mutex, &st->m_end_time); if (e != 0 && e != ETIMEDOUT) throw default_exception("failed to start timed wait"); st->m_eh->operator()(); - pthread_mutex_unlock(&mutex); - if (pthread_mutex_destroy(&mutex) != 0) - throw default_exception("failed to destroy pthread mutex"); - if (pthread_cond_destroy(&st->m_condition_var) != 0) - throw default_exception("failed to destroy pthread condition variable"); + pthread_mutex_unlock(&st->m_mutex); + return st; } #elif defined(_LINUX_) || defined(_FREEBSD_) @@ -150,6 +132,22 @@ struct scoped_timer::imp { m_interval = ms; if (pthread_attr_init(&m_attributes) != 0) throw default_exception("failed to initialize timer thread attributes"); + if (pthread_cond_init(&m_condition_var, NULL) != 0) + throw default_exception("failed to initialize timer condition variable"); + if (pthread_mutex_init(&m_mutex, NULL) != 0) + throw default_exception("failed to initialize timer mutex"); + + clock_serv_t host_clock; + mach_timespec_t now; + unsigned long long nano = static_cast(m_interval) * 1000000ull; + + host_get_clock_service(mach_host_self(), CALENDAR_CLOCK, &host_clock); + m_end_time.tv_sec = nano / 1000000000ull; + m_end_time.tv_nsec = nano % 1000000000ull; + clock_get_time(host_clock, &now); + ADD_MACH_TIMESPEC(&m_end_time, &now); + + if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0) throw default_exception("failed to start timer thread"); #elif defined(_LINUX_) || defined(_FREEBSD_) @@ -183,9 +181,25 @@ struct scoped_timer::imp { INVALID_HANDLE_VALUE); #elif defined(__APPLE__) && defined(__MACH__) // Mac OS X - pthread_cond_signal(&m_condition_var); // this is okay to fail + + // If the waiting-thread is not up and waiting yet, + // we can make sure that it finishes quickly by + // setting the end-time to zero. + m_end_time.tv_sec = 0; + m_end_time.tv_nsec = 0; + + // Otherwise it's already up and waiting, and + // we can send a signal on m_condidion_var: + pthread_mutex_lock(&m_mutex); + pthread_cond_signal(&m_condition_var); + pthread_mutex_unlock(&m_mutex); + if (pthread_join(m_thread_id, NULL) != 0) throw default_exception("failed to join thread"); + if (pthread_mutex_destroy(&m_mutex) != 0) + throw default_exception("failed to destroy pthread mutex"); + if (pthread_cond_destroy(&m_condition_var) != 0) + throw default_exception("failed to destroy pthread condition variable"); if (pthread_attr_destroy(&m_attributes) != 0) throw default_exception("failed to destroy pthread attributes object"); #elif defined(_LINUX_) || defined(_FREEBSD_) From 581bbb58fb97f0735e01e28781d5c0ef9e762f60 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 2 May 2014 18:04:32 +0100 Subject: [PATCH 11/17] typo Signed-off-by: Christoph M. Wintersteiger --- src/util/scoped_timer.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 66c321267..c4a640009 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -189,7 +189,7 @@ struct scoped_timer::imp { m_end_time.tv_nsec = 0; // Otherwise it's already up and waiting, and - // we can send a signal on m_condidion_var: + // we can send a signal on m_condition_var: pthread_mutex_lock(&m_mutex); pthread_cond_signal(&m_condition_var); pthread_mutex_unlock(&m_mutex); From 3d1ca5ecc91a498a36cfbc39ff6a0d3a03f80d89 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 May 2014 21:12:16 -0700 Subject: [PATCH 12/17] make eval cache sensitive to model completion. Bug 110 reported by cipher1024 Signed-off-by: Nikolaj Bjorner --- src/model/model.cpp | 3 ++- src/smt/proto_model/proto_model.cpp | 3 +++ src/smt/smt_model_finder.cpp | 21 +++++++++++++-------- 3 files changed, 18 insertions(+), 9 deletions(-) diff --git a/src/model/model.cpp b/src/model/model.cpp index 4a9767cb0..f87992d05 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -133,7 +133,8 @@ bool model::eval(expr * e, expr_ref & result, bool model_completion) { ev(e, result); return true; } - catch (model_evaluator_exception &) { + catch (model_evaluator_exception & ex) { + TRACE("model_evaluator", tout << ex.msg() << "\n";); return false; } } diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp index 70287728e..26b35f0ed 100644 --- a/src/smt/proto_model/proto_model.cpp +++ b/src/smt/proto_model/proto_model.cpp @@ -247,6 +247,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { new_t = mk_some_interp_for(f); } else { + TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";); is_ok = false; } } @@ -294,6 +295,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { // f is an uninterpreted function, there is no need to use m_simplifier.mk_app new_t = m_manager.mk_app(f, num_args, args.c_ptr()); trail.push_back(new_t); + TRACE("model_eval", tout << f->get_name() << " is uninterpreted\n";); is_ok = false; } } @@ -326,6 +328,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) { todo.pop_back(); break; case AST_QUANTIFIER: + TRACE("model_eval", tout << "found quantifier\n" << mk_pp(a, m_manager) << "\n";); is_ok = false; // evaluator does not handle quantifiers. SASSERT(a != 0); eval_cache.insert(a, a); diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 8303d05ac..568e9fca9 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -396,7 +396,7 @@ namespace smt { // Support for evaluating expressions in the current model. proto_model * m_model; - obj_map m_eval_cache; + obj_map m_eval_cache[2]; expr_ref_vector m_eval_cache_range; ptr_vector m_root_nodes; @@ -409,7 +409,8 @@ namespace smt { } void reset_eval_cache() { - m_eval_cache.reset(); + m_eval_cache[0].reset(); + m_eval_cache[1].reset(); m_eval_cache_range.reset(); } @@ -468,6 +469,7 @@ namespace smt { ~auf_solver() { flush_nodes(); + reset_eval_cache(); } void set_context(context * ctx) { @@ -547,7 +549,7 @@ namespace smt { for (obj_map::iterator it = elems.begin(); it != elems.end(); it++) { expr * n = it->m_key; expr * n_val = eval(n, true); - if (!m_manager.is_value(n_val)) + if (!n_val || !m_manager.is_value(n_val)) to_delete.push_back(n); } for (ptr_vector::iterator it = to_delete.begin(); it != to_delete.end(); it++) { @@ -569,16 +571,19 @@ namespace smt { virtual expr * eval(expr * n, bool model_completion) { expr * r = 0; - if (m_eval_cache.find(n, r)) { + if (m_eval_cache[model_completion].find(n, r)) { return r; } expr_ref tmp(m_manager); - if (!m_model->eval(n, tmp, model_completion)) + if (!m_model->eval(n, tmp, model_completion)) { r = 0; - else + TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n-----> null\n";); + } + else { r = tmp; - TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";); - m_eval_cache.insert(n, r); + TRACE("model_finder", tout << "eval\n" << mk_pp(n, m_manager) << "\n----->\n" << mk_pp(r, m_manager) << "\n";); + } + m_eval_cache[model_completion].insert(n, r); m_eval_cache_range.push_back(r); return r; } From 2ca14b49fe45a09aa39c36b1856e32f5ac8843ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 May 2014 09:45:32 -0700 Subject: [PATCH 13/17] fix AV in debug assertion, address warnings Signed-off-by: Nikolaj Bjorner --- src/cmd_context/pdecl.cpp | 2 +- src/duality/duality.h | 2 +- src/duality/duality_solver.cpp | 2 +- src/muz/transforms/dl_mk_coi_filter.cpp | 18 +++++++++++++++++- 4 files changed, 20 insertions(+), 4 deletions(-) diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 4a51e4943..08a29e381 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -189,7 +189,7 @@ class psort_app : public psort { m.inc_ref(d); m.inc_ref(num_args, args); SASSERT(num_args == m_decl->get_num_params() || m_decl->has_var_params()); - DEBUG_CODE(for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this);); + DEBUG_CODE(if (num_args == num_params) { for (unsigned i = 0; i < num_params; i++) args[i]->check_num_params(this); }); } virtual void finalize(pdecl_manager & m) { diff --git a/src/duality/duality.h b/src/duality/duality.h index fc70ffa70..4005adc1a 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -29,7 +29,7 @@ using namespace stl_ext; namespace Duality { - class implicant_solver; + struct implicant_solver; /* Generic operations on Z3 formulas */ diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index ff3bc190b..79055b43a 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -2201,7 +2201,7 @@ namespace Duality { #endif int expand_max = 1; if(0&&duality->BatchExpand){ - int thing = stack.size() * 0.1; + int thing = stack.size() / 10; // * 0.1; expand_max = std::max(1,thing); if(expand_max > 1) std::cout << "foo!\n"; diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index 31af7a53f..c7a8d5aa0 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -200,7 +200,23 @@ namespace datalog { func_decl_set::iterator it = pruned_preds.begin(); extension_model_converter* mc0 = alloc(extension_model_converter, m); for (; it != end; ++it) { - mc0->insert(*it, m.mk_true()); + const rule_vector& rules = source.get_predicate_rules(*it); + expr_ref_vector fmls(m); + for (unsigned i = 0; i < rules.size(); ++i) { + app* head = rules[i]->get_head(); + expr_ref_vector conj(m); + unsigned n = head->get_num_args()-1; + for (unsigned j = 0; j < head->get_num_args(); ++j) { + expr* arg = head->get_arg(j); + if (!is_var(arg)) { + conj.push_back(m.mk_eq(m.mk_var(j, m.get_sort(arg)), arg)); + } + } + fmls.push_back(m.mk_and(conj.size(), conj.c_ptr())); + } + expr_ref fml(m); + fml = m.mk_or(fmls.size(), fmls.c_ptr()); + mc0->insert(*it, fml); } m_context.add_model_converter(mc0); } From 6f0155ce94a6124caedad154f00b8389351f7f1d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 May 2014 10:14:40 -0700 Subject: [PATCH 14/17] avoid compiler warning Signed-off-by: Nikolaj Bjorner --- src/model/model.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/model/model.cpp b/src/model/model.cpp index f87992d05..a6b9695b4 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -134,6 +134,7 @@ bool model::eval(expr * e, expr_ref & result, bool model_completion) { return true; } catch (model_evaluator_exception & ex) { + (void)ex; TRACE("model_evaluator", tout << ex.msg() << "\n";); return false; } From e3098b0ec59ddf46c8f25402828d62d2fe21c122 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 May 2014 11:20:15 -0700 Subject: [PATCH 15/17] add documentation comment to bind_variables Signed-off-by: Nikolaj Bjorner --- src/muz/base/dl_context.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h index 51b54bc01..1952cc42f 100644 --- a/src/muz/base/dl_context.h +++ b/src/muz/base/dl_context.h @@ -278,6 +278,12 @@ namespace datalog { void register_variable(func_decl* var); + /* + Replace constants that have been registered as + variables by de-Bruijn indices and corresponding + universal (if is_forall is true) or existential + quantifier. + */ expr_ref bind_variables(expr* fml, bool is_forall); /** From 2ee416fc8ffb069a309bc36cd992b71be68f43cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 May 2014 10:23:31 -0700 Subject: [PATCH 16/17] deal with infinite loop in diagonalization attempt in datatype factory Signed-off-by: Nikolaj Bjorner --- src/smt/proto_model/datatype_factory.cpp | 37 +++++++++++++++++++++--- src/smt/proto_model/datatype_factory.h | 2 ++ 2 files changed, 35 insertions(+), 4 deletions(-) diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp index a45b53155..5e66ab738 100644 --- a/src/smt/proto_model/datatype_factory.cpp +++ b/src/smt/proto_model/datatype_factory.cpp @@ -20,6 +20,7 @@ Revision History: #include"proto_model.h" #include"ast_pp.h" #include"ast_ll_pp.h" +#include"expr_functors.h" datatype_factory::datatype_factory(ast_manager & m, proto_model & md): struct_factory(m, m.mk_family_id("datatype"), md), @@ -47,8 +48,10 @@ expr * datatype_factory::get_some_value(sort * s) { */ expr * datatype_factory::get_last_fresh_value(sort * s) { expr * val = 0; - if (m_last_fresh_value.find(s, val)) + if (m_last_fresh_value.find(s, val)) { + TRACE("datatype_factory", tout << "cached fresh value: " << mk_pp(val, m_manager) << "\n";); return val; + } value_set * set = get_value_set(s); if (set->empty()) val = get_some_value(s); @@ -59,6 +62,17 @@ expr * datatype_factory::get_last_fresh_value(sort * s) { return val; } +bool datatype_factory::is_subterm_of_last_value(app* e) { + expr* last; + if (!m_last_fresh_value.find(m_manager.get_sort(e), last)) { + return false; + } + contains_app contains(m_manager, e); + bool result = contains(last); + TRACE("datatype_factory", tout << mk_pp(e, m_manager) << " in " << mk_pp(last, m_manager) << " " << result << "\n";); + return result; +} + /** \brief Create an almost fresh value. If s is recursive, then the result is not 0. It also updates m_last_fresh_value @@ -105,11 +119,18 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) { } } if (recursive || found_fresh_arg) { - expr * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr()); + app * new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr()); SASSERT(!found_fresh_arg || !set->contains(new_value)); register_value(new_value); - if (m_util.is_recursive(s)) - m_last_fresh_value.insert(s, new_value); + if (m_util.is_recursive(s)) { + if (is_subterm_of_last_value(new_value)) { + new_value = static_cast(m_last_fresh_value.find(s)); + } + else { + m_last_fresh_value.insert(s, new_value); + } + } + TRACE("datatype_factory", tout << "almost fresh: " << mk_pp(new_value, m_manager) << "\n";); return new_value; } } @@ -181,12 +202,20 @@ expr * datatype_factory::get_fresh_value(sort * s) { expr_ref_vector args(m_manager); bool found_sibling = false; unsigned num = constructor->get_arity(); + TRACE("datatype_factory", tout << "checking constructor: " << constructor->get_name() << "\n";); for (unsigned i = 0; i < num; i++) { sort * s_arg = constructor->get_domain(i); + TRACE("datatype_factory", tout << mk_pp(s, m_manager) << " " + << mk_pp(s_arg, m_manager) << " are_siblings " + << m_util.are_siblings(s, s_arg) << " is_datatype " + << m_util.is_datatype(s_arg) << " found_sibling " + << found_sibling << "\n";); if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) { found_sibling = true; expr * maybe_new_arg = get_almost_fresh_value(s_arg); if (!maybe_new_arg) { + TRACE("datatype_factory", + tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";); maybe_new_arg = m_model.get_some_value(s_arg); found_sibling = false; } diff --git a/src/smt/proto_model/datatype_factory.h b/src/smt/proto_model/datatype_factory.h index e8e1f2589..f70604ca8 100644 --- a/src/smt/proto_model/datatype_factory.h +++ b/src/smt/proto_model/datatype_factory.h @@ -29,6 +29,8 @@ class datatype_factory : public struct_factory { expr * get_last_fresh_value(sort * s); expr * get_almost_fresh_value(sort * s); + bool is_subterm_of_last_value(app* e); + public: datatype_factory(ast_manager & m, proto_model & md); virtual ~datatype_factory() {} From a1ee1ec4cce4ae978c2325dd76424c55edd9c882 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 May 2014 12:28:07 -0700 Subject: [PATCH 17/17] add virtal destructor to qe_sat Signed-off-by: Nikolaj Bjorner --- src/qe/qe_sat_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp index 854e15493..b4a1a6a8b 100644 --- a/src/qe/qe_sat_tactic.cpp +++ b/src/qe/qe_sat_tactic.cpp @@ -226,7 +226,7 @@ namespace qe { return alloc(sat_tactic, m); } - ~sat_tactic() { + virtual ~sat_tactic() { for (unsigned i = 0; i < m_solvers.size(); ++i) { dealloc(m_solvers[i]); }