From 5166b96d206dcb03e358d3aaeaae06123f8281cd Mon Sep 17 00:00:00 2001 From: bannsec Date: Mon, 23 Apr 2018 17:17:51 -0400 Subject: [PATCH 1/4] Fancy dots are not allowed here!! --- src/smt/theory_datatype.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 9ff81fa08..049555297 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -461,7 +461,7 @@ namespace smt { TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";); enode* app_parent = nullptr; - // first: explain that root=v, given that app=cstor(…,v,…) + // first: explain that root=v, given that app=cstor(...,v,...) for (enode * arg : enode::args(oc_get_cstor(app))) { // found an argument which is equal to root if (arg->get_root() == root->get_root()) { From a1d870f19f6638432eb5f15f0f1a59319a9927ab Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 24 Apr 2018 12:43:11 +0100 Subject: [PATCH 2/4] Added tactic for QF_FPLRA --- src/solver/smt_logics.cpp | 11 ++-- src/tactic/fpa/qffplra_tactic.cpp | 72 +++++++++++++++++++++++++ src/tactic/fpa/qffplra_tactic.h | 38 +++++++++++++ src/tactic/portfolio/default_tactic.cpp | 12 +++-- 4 files changed, 123 insertions(+), 10 deletions(-) create mode 100644 src/tactic/fpa/qffplra_tactic.cpp create mode 100644 src/tactic/fpa/qffplra_tactic.h diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp index 874f1cfcc..7ed2b0445 100644 --- a/src/solver/smt_logics.cpp +++ b/src/solver/smt_logics.cpp @@ -22,14 +22,14 @@ Revision History: bool smt_logics::supported_logic(symbol const & s) { - return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) || + return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) || logic_has_arith(s) || logic_has_bv(s) || logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) || logic_has_horn(s) || logic_has_fpa(s); } bool smt_logics::logic_has_reals_only(symbol const& s) { - return + return s == "QF_RDL" || s == "QF_LRA" || s == "UFLRA" || @@ -84,8 +84,9 @@ bool smt_logics::logic_has_arith(symbol const & s) { s == "QF_BVFP" || s == "QF_S" || s == "ALL" || - s == "QF_FD" || - s == "HORN"; + s == "QF_FD" || + s == "HORN" || + s == "QF_FPLRA"; } bool smt_logics::logic_has_bv(symbol const & s) { @@ -137,7 +138,7 @@ bool smt_logics::logic_has_str(symbol const & s) { } bool smt_logics::logic_has_fpa(symbol const & s) { - return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "ALL"; + return s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA" || s == "ALL"; } bool smt_logics::logic_has_uf(symbol const & s) { diff --git a/src/tactic/fpa/qffplra_tactic.cpp b/src/tactic/fpa/qffplra_tactic.cpp new file mode 100644 index 000000000..947a41111 --- /dev/null +++ b/src/tactic/fpa/qffplra_tactic.cpp @@ -0,0 +1,72 @@ +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + qffpalra_tactic.cpp + +Abstract: + + Tactic for QF_FPLRA benchmarks. + +Author: + + Christoph (cwinter) 2018-04-24 + +Notes: + +--*/ +#include "tactic/tactical.h" +#include "tactic/fpa/qffp_tactic.h" +#include "tactic/fpa/qffplra_tactic.h" + +tactic * mk_qffplra_tactic(ast_manager & m, params_ref const & p) { + tactic * st = mk_qffp_tactic(m, p); + st->updt_params(p); + return st; +} + +struct is_non_qffplra_predicate { + struct found {}; + ast_manager & m; + bv_util bu; + fpa_util fu; + arith_util au; + + is_non_qffplra_predicate(ast_manager & _m) : m(_m), bu(m), fu(m), au(m) {} + + void operator()(var *) { throw found(); } + + void operator()(quantifier *) { throw found(); } + + void operator()(app * n) { + sort * s = get_sort(n); + if (!m.is_bool(s) && !fu.is_float(s) && !fu.is_rm(s) && !bu.is_bv_sort(s) && !au.is_real(s)) + throw found(); + family_id fid = n->get_family_id(); + if (fid == m.get_basic_family_id() || + fid == fu.get_family_id() || + fid == bu.get_family_id() || + fid == au.get_family_id()) + return; + if (is_uninterp_const(n)) + return; + if (au.is_real(s)) + return; + + throw found(); + } +}; + +class is_qffplra_probe : public probe { +public: + result operator()(goal const & g) override { + return !test(g); + } + + ~is_qffplra_probe() override {} +}; + +probe * mk_is_qffplra_probe() { + return alloc(is_qffplra_probe); +} diff --git a/src/tactic/fpa/qffplra_tactic.h b/src/tactic/fpa/qffplra_tactic.h new file mode 100644 index 000000000..b5a741ac3 --- /dev/null +++ b/src/tactic/fpa/qffplra_tactic.h @@ -0,0 +1,38 @@ +#pragma once +/*++ +Copyright (c) 2012 Microsoft Corporation + +Module Name: + + qffplra_tactic.h + +Abstract: + + Tactic for QF_FPLRA benchmarks. + +Author: + + Christoph (cwinter) 2018-04-24 + +Notes: + + +--*/ +#ifndef QFFPLRA_TACTIC_H_ +#define QFFPLRA_TACTIC_H_ + +#include "util/params.h" +class ast_manager; +class tactic; + +tactic * mk_qffplra_tactic(ast_manager & m, params_ref const & p = params_ref()); +/* +ADD_TACTIC("qffplra", "(try to) solve goal using the tactic for QF_FPLRA.", "mk_qffplra_tactic(m, p)") +*/ + +probe * mk_is_qffplra_probe(); +/* +ADD_PROBE("is-qffplra", "true if the goal is in QF_FPLRA.", "mk_is_qffplra_probe()") +*/ + +#endif diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 09052869b..5cf06ca86 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -28,24 +28,26 @@ Notes: #include "tactic/arith/probe_arith.h" #include "tactic/smtlogics/quant_tactics.h" #include "tactic/fpa/qffp_tactic.h" +#include "tactic/fpa/qffplra_tactic.h" #include "tactic/smtlogics/qfaufbv_tactic.h" #include "tactic/smtlogics/qfauflia_tactic.h" #include "tactic/smtlogics/qfufnra_tactic.h" tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), - cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), - cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m), + cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), + cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m), cond(mk_is_qflia_probe(), mk_qflia_tactic(m), cond(mk_is_qfauflia_probe(), mk_qfauflia_tactic(m), cond(mk_is_qflra_probe(), mk_qflra_tactic(m), cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m), cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m), - cond(mk_is_lira_probe(), mk_lira_tactic(m, p), - cond(mk_is_nra_probe(), mk_nra_tactic(m), + cond(mk_is_lira_probe(), mk_lira_tactic(m, p), + cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p), + cond(mk_is_qffplra_probe(), mk_qffplra_tactic(m, p), //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), - mk_smt_tactic()))))))))))), + mk_smt_tactic())))))))))))), p); return st; } From e13f3d92af517c6caeceec77f7bdaf4560323a17 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 24 Apr 2018 15:01:05 +0100 Subject: [PATCH 3/4] Updated CMakelists.txt --- src/tactic/fpa/CMakeLists.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/tactic/fpa/CMakeLists.txt b/src/tactic/fpa/CMakeLists.txt index a54212235..c647df7fc 100644 --- a/src/tactic/fpa/CMakeLists.txt +++ b/src/tactic/fpa/CMakeLists.txt @@ -3,6 +3,7 @@ z3_add_component(fpa_tactics fpa2bv_model_converter.cpp fpa2bv_tactic.cpp qffp_tactic.cpp + qffplra_tactic.cpp COMPONENT_DEPENDENCIES arith_tactics bv_tactics @@ -14,4 +15,5 @@ z3_add_component(fpa_tactics TACTIC_HEADERS fpa2bv_tactic.h qffp_tactic.h + qffplra_tactic.h ) From f7bcf0fd585e3fd7c294d63307356d7357ea3383 Mon Sep 17 00:00:00 2001 From: yxliang01 <13267.okk@gmail.com> Date: Tue, 24 Apr 2018 08:17:20 -0700 Subject: [PATCH 4/4] Z3 now will also try to find libz3 in PYTHONPATH --- scripts/update_api.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 8a7b33efd..78fad45be 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1657,7 +1657,7 @@ else: if hasattr(builtins, "Z3_LIB_DIRS"): _all_dirs = builtins.Z3_LIB_DIRS -for v in ('Z3_LIBRARY_PATH', 'PATH'): +for v in ('Z3_LIBRARY_PATH', 'PATH', 'PYTHONPATH'): if v in os.environ: lp = os.environ[v]; lds = lp.split(';') if sys.platform in ('win32') else lp.split(':')