From 58ffffe4d4f3756381910e62c1fc4a5f169cb4c0 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Sun, 6 Apr 2014 13:01:20 -0700 Subject: [PATCH 01/35] hack to filter out Boogie axioms with large "distinct" predicates that cause legacy solver death --- src/duality/duality.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/duality/duality.h b/src/duality/duality.h index fc70ffa70..1445bc881 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -253,6 +253,10 @@ protected: } void assert_axiom(const expr &axiom){ + // HACK: large "distict" predicates can kill the legacy SMT solver -- ignore them + if(axiom.is_app() && axiom.decl().get_decl_kind() == Distinct) + if(axiom.num_args() > 10) + return; islvr->AssertInterpolationAxiom(axiom); } From f7d589fc49d1ed30761705732dcfaf7338777085 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 10 Apr 2014 17:53:00 -0700 Subject: [PATCH 02/35] changed fixedpoint output format for easier parsing in Boogie --- src/muz/duality/duality_dl_interface.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 587a184bc..99ac2ee1c 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -350,7 +350,9 @@ void dl_interface::display_certificate_non_const(std::ostream& out) { if(_d->status == StatusModel){ ast_manager &m = m_ctx.get_manager(); model_ref md = get_model(); + out << "(fixedpoint \n"; model_smt2_pp(out, m, *md.get(), 0); + out << ")\n"; } else if(_d->status == StatusRefutation){ out << "(derivation\n"; From de81db9a3bb451fb70826b5bee3c28a8adb88dd3 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 10 Apr 2014 17:53:17 -0700 Subject: [PATCH 03/35] fixed several interpolation problems --- src/interp/iz3base.cpp | 11 +++- src/interp/iz3base.h | 2 +- src/interp/iz3translate.cpp | 122 ++++++++++++++++++++++++++++++++++-- 3 files changed, 128 insertions(+), 7 deletions(-) diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp index 32fe33566..8f98a23f9 100755 --- a/src/interp/iz3base.cpp +++ b/src/interp/iz3base.cpp @@ -260,7 +260,7 @@ void iz3base::check_interp(const std::vector &itps, std::vector &theor #endif } -bool iz3base::is_sat(const std::vector &q, ast &_proof){ +bool iz3base::is_sat(const std::vector &q, ast &_proof, std::vector &vars){ params_ref p; p.set_bool("proof", true); // this is currently useless @@ -277,6 +277,15 @@ bool iz3base::is_sat(const std::vector &q, ast &_proof){ ::ast *proof = s.get_proof(); _proof = cook(proof); } + else if(vars.size()) { + model_ref(_m); + s.get_model(_m); + for(unsigned i = 0; i < vars.size(); i++){ + expr_ref r(m()); + _m.get()->eval(to_expr(vars[i].raw()),r,true); + vars[i] = cook(r.get()); + } + } dealloc(m_solver); return res != l_false; } diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h index d82e721ae..bca9b8518 100755 --- a/src/interp/iz3base.h +++ b/src/interp/iz3base.h @@ -113,7 +113,7 @@ class iz3base : public iz3mgr, public scopes { void check_interp(const std::vector &itps, std::vector &theory); /** For convenience -- is this formula SAT? */ - bool is_sat(const std::vector &consts, ast &_proof); + bool is_sat(const std::vector &consts, ast &_proof, std::vector &vars); /** Interpolator for clauses, to be implemented */ virtual void interpolate_clause(std::vector &lits, std::vector &itps){ diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index a7c2125e7..060bb74ad 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1071,6 +1071,8 @@ public: ast AssignBounds2Farkas(const ast &proof, const ast &con){ std::vector farkas_coeffs; get_assign_bounds_coeffs(proof,farkas_coeffs); + if(farkas_coeffs[0] != make_int(rational(1))) + farkas_coeffs[0] = make_int(rational(1)); std::vector lits; int nargs = num_args(con); if(nargs != (int)(farkas_coeffs.size())) @@ -1107,6 +1109,8 @@ public: ast AssignBoundsRule2Farkas(const ast &proof, const ast &con, std::vector prems){ std::vector farkas_coeffs; get_assign_bounds_rule_coeffs(proof,farkas_coeffs); + if(farkas_coeffs[0] != make_int(rational(1))) + farkas_coeffs[0] = make_int(rational(1)); std::vector lits; int nargs = num_prems(proof)+1; if(nargs != (int)(farkas_coeffs.size())) @@ -1278,6 +1282,17 @@ public: return make(Plus,args); } + void get_sum_as_vector(const ast &t, std::vector &coeffs, std::vector &vars){ + if(!(op(t) == Plus)){ + coeffs.push_back(get_coeff(t)); + vars.push_back(get_linear_var(t)); + } + else { + int nargs = num_args(t); + for(int i = 0; i < nargs; i++) + get_sum_as_vector(arg(t,i),coeffs,vars); + } + } ast replace_summands_with_fresh_vars(const ast &t, hash_map &map){ if(op(t) == Plus){ @@ -1294,6 +1309,94 @@ public: return map[t]; } + rational lcd(const std::vector &rats){ + rational res = rational(1); + for(unsigned i = 0; i < rats.size(); i++){ + res = lcm(res,denominator(rats[i])); + } + return res; + } + + Iproof::node reconstruct_farkas_with_dual(const std::vector &prems, const std::vector &pfs, const ast &con){ + int nprems = prems.size(); + std::vector npcons(nprems); + hash_map pain_map; // not needed + for(int i = 0; i < nprems; i++) + npcons[i] = painfully_normalize_ineq(conc(prems[i]),pain_map); + ast ncon = painfully_normalize_ineq(mk_not(con),pain_map); + npcons.push_back(ncon); + + hash_map dual_map; + std::vector cvec, vars_seen; + ast rhs = make_real(rational(0)); + for(unsigned i = 0; i < npcons.size(); i++){ + ast c= mk_fresh_constant("@c",real_type()); + cvec.push_back(c); + ast lhs = arg(npcons[i],0); + std::vector coeffs; + std::vector vars; + get_sum_as_vector(lhs,coeffs,vars); + for(unsigned j = 0; j < coeffs.size(); j++){ + rational coeff = coeffs[j]; + ast var = vars[j]; + if(dual_map.find(var) == dual_map.end()){ + dual_map[var] = make_real(rational(0)); + vars_seen.push_back(var); + } + ast foo = make(Plus,dual_map[var],make(Times,make_real(coeff),c)); + dual_map[var] = foo; + } + rhs = make(Plus,rhs,make(Times,c,arg(npcons[i],1))); + } + std::vector cnstrs; + for(unsigned i = 0; i < vars_seen.size(); i++) + cnstrs.push_back(make(Equal,dual_map[vars_seen[i]],make_real(rational(0)))); + cnstrs.push_back(make(Leq,rhs,make_real(rational(0)))); + for(unsigned i = 0; i < cvec.size() - 1; i++) + cnstrs.push_back(make(Geq,cvec[i],make_real(rational(0)))); + cnstrs.push_back(make(Equal,cvec.back(),make_real(rational(1)))); + ast new_proof; + + // greedily reduce the core + for(unsigned i = 0; i < cvec.size() - 1; i++){ + std::vector dummy; + cnstrs.push_back(make(Equal,cvec[i],make_real(rational(0)))); + if(!is_sat(cnstrs,new_proof,dummy)) + cnstrs.pop_back(); + } + + std::vector vals = cvec; + if(!is_sat(cnstrs,new_proof,vals)) + throw "Proof error!"; + std::vector rat_farkas_coeffs; + for(unsigned i = 0; i < cvec.size(); i++){ + ast bar = vals[i]; + rational r; + if(is_numeral(bar,r)) + rat_farkas_coeffs.push_back(r); + else + throw "Proof error!"; + } + rational the_lcd = lcd(rat_farkas_coeffs); + std::vector farkas_coeffs; + std::vector my_prems; + std::vector my_pcons; + for(unsigned i = 0; i < prems.size(); i++){ + ast fc = make_int(rat_farkas_coeffs[i] * the_lcd); + if(!(fc == make_int(rational(0)))){ + farkas_coeffs.push_back(fc); + my_prems.push_back(pfs[i]); + my_pcons.push_back(conc(prems[i])); + } + } + farkas_coeffs.push_back(make_int(the_lcd)); + my_prems.push_back(iproof->make_hypothesis(mk_not(con))); + my_pcons.push_back(mk_not(con)); + + Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs); + return res; + } + ast painfully_normalize_ineq(const ast &ineq, hash_map &map){ ast res = normalize_inequality(ineq); ast lhs = arg(res,0); @@ -1318,7 +1421,8 @@ public: npcons.push_back(ncon); // ast assumps = make(And,pcons); ast new_proof; - if(is_sat(npcons,new_proof)) + std::vector dummy; + if(is_sat(npcons,new_proof,dummy)) throw "Proof error!"; pfrule dk = pr(new_proof); int nnp = num_prems(new_proof); @@ -1334,7 +1438,7 @@ public: farkas_coeffs.push_back(make_int(rational(1))); } else - throw "cannot reconstruct farkas proof"; + return reconstruct_farkas_with_dual(prems,pfs,con); for(int i = 0; i < nnp; i++){ ast p = conc(prem(new_proof,i)); @@ -1348,7 +1452,7 @@ public: my_pcons.push_back(mk_not(con)); } else - throw "cannot reconstruct farkas proof"; + return reconstruct_farkas_with_dual(prems,pfs,con); } Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs); return res; @@ -1378,7 +1482,8 @@ public: npcons.push_back(ncon); // ast assumps = make(And,pcons); ast new_proof; - if(is_sat(npcons,new_proof)) + std::vector dummy; + if(is_sat(npcons,new_proof,dummy)) throw "Proof error!"; pfrule dk = pr(new_proof); int nnp = num_prems(new_proof); @@ -1408,7 +1513,7 @@ public: my_pcons.push_back(mk_not(con)); } else - throw "cannot reconstruct farkas proof"; + return painfully_reconstruct_farkas(prems,pfs,con); } Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs); return res; @@ -1552,6 +1657,13 @@ public: if(dk == PR_MODUS_PONENS && expect_clause && op(con) == Or) std::cout << "foo!\n"; + // no idea why this shows up + if(dk == PR_MODUS_PONENS_OEQ) + if(conc(prem(proof,0)) == con){ + res = translate_main(prem(proof,0),expect_clause); + return res; + } + #if 0 if(1 && dk == PR_TRANSITIVITY && pr(prem(proof,1)) == PR_COMMUTATIVITY){ Iproof::node clause = translate_main(prem(proof,0),true); From 60ef669fbc8b3fd3a1aaa10e179c2edee41eadbe Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 10 Apr 2014 17:54:49 -0700 Subject: [PATCH 04/35] removed distinct predicate hack --- src/duality/duality.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/duality/duality.h b/src/duality/duality.h index 1445bc881..572ce427b 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -253,10 +253,12 @@ protected: } void assert_axiom(const expr &axiom){ +#if 0 // HACK: large "distict" predicates can kill the legacy SMT solver -- ignore them if(axiom.is_app() && axiom.decl().get_decl_kind() == Distinct) if(axiom.num_args() > 10) return; +#endif islvr->AssertInterpolationAxiom(axiom); } From 77f8aa9f6b53114fea43d5c5f76b3724533079a7 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 22 Apr 2014 13:28:11 -0700 Subject: [PATCH 05/35] fix for quantifiers in interpolants --- src/interp/iz3proof_itp.cpp | 15 +++++++++++++-- src/interp/iz3scopes.h | 20 ++++++++++++++++++++ 2 files changed, 33 insertions(+), 2 deletions(-) diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 5fe3338dc..8913920ac 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -2655,8 +2655,13 @@ class iz3proof_itp_impl : public iz3proof_itp { }; std::vector localization_vars; // localization vars in order of creation - hash_map localization_map; // maps terms to their localization vars - hash_map localization_pf_map; // maps terms to proofs of their localizations + + struct locmaps { + hash_map localization_map; // maps terms to their localization vars + hash_map localization_pf_map; // maps terms to proofs of their localizations + }; + + hash_map localization_maps_per_range; /* "localize" a term e to a given frame range, creating new symbols to represent non-local subterms. This returns the localized version e_l, @@ -2678,6 +2683,12 @@ class iz3proof_itp_impl : public iz3proof_itp { } ast localize_term(ast e, const prover::range &rng, ast &pf){ + + // we need to memoize this function per range + locmaps &maps = localization_maps_per_range[rng]; + hash_map &localization_map = maps.localization_map; + hash_map &localization_pf_map = maps.localization_pf_map; + ast orig_e = e; pf = make_refl(e); // proof that e = e diff --git a/src/interp/iz3scopes.h b/src/interp/iz3scopes.h index cd7203eeb..23ab1c714 100755 --- a/src/interp/iz3scopes.h +++ b/src/interp/iz3scopes.h @@ -23,6 +23,7 @@ Revision History: #include #include +#include "iz3hash.h" class scopes { @@ -194,4 +195,23 @@ class scopes { }; + +// let us hash on ranges + +#ifndef FULL_TREE +namespace hash_space { + template <> + class hash { + public: + size_t operator()(const scopes::range &p) const { + return (size_t)p.lo + (size_t)p.hi; + } + }; +} + +inline bool operator==(const scopes::range &x, const scopes::range &y){ + return x.lo == y.lo && x.hi == y.hi; +} +#endif + #endif From 2755854c81e9cf6ec3da1d4b9ae0685e24252d67 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 22 Apr 2014 16:42:35 -0700 Subject: [PATCH 06/35] trying alternate encoding of distint --- src/duality/duality.h | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/src/duality/duality.h b/src/duality/duality.h index 572ce427b..77fbdfd55 100755 --- a/src/duality/duality.h +++ b/src/duality/duality.h @@ -253,11 +253,26 @@ protected: } void assert_axiom(const expr &axiom){ -#if 0 - // HACK: large "distict" predicates can kill the legacy SMT solver -- ignore them +#if 1 + // HACK: large "distict" predicates can kill the legacy SMT solver. + // encode them with a UIF if(axiom.is_app() && axiom.decl().get_decl_kind() == Distinct) - if(axiom.num_args() > 10) + if(axiom.num_args() > 10){ + sort s = axiom.arg(0).get_sort(); + std::vector sv; + sv.push_back(s); + int nargs = axiom.num_args(); + std::vector args(nargs); + func_decl f = ctx->fresh_func_decl("@distinct",sv,ctx->int_sort()); + for(int i = 0; i < nargs; i++){ + expr a = axiom.arg(i); + expr new_cnstr = f(a) == ctx->int_val(i); + args[i] = new_cnstr; + } + expr cnstr = ctx->make(And,args); + islvr->AssertInterpolationAxiom(cnstr); return; + } #endif islvr->AssertInterpolationAxiom(axiom); } From f4790a183d42bbfdd6ec8e345439cca0965ef9f9 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Thu, 24 Apr 2014 16:18:20 -0700 Subject: [PATCH 07/35] strarting on conjecture printing in duality --- src/duality/duality_solver.cpp | 41 ++++++++++++++++++++++++++++++++++ src/duality/duality_wrapper.h | 5 +++++ 2 files changed, 46 insertions(+) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index ff3bc190b..f973b16e5 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -100,6 +100,7 @@ namespace Duality { }; Reporter *CreateStdoutReporter(RPFP *rpfp); + Reporter *CreateConjectureFileReporter(RPFP *rpfp, const std::string &fname); /** Object we throw in case of catastrophe. */ @@ -125,6 +126,7 @@ namespace Duality { { rpfp = _rpfp; reporter = 0; + conj_reporter = 0; heuristic = 0; unwinding = 0; FullExpand = false; @@ -274,6 +276,7 @@ namespace Duality { RPFP *rpfp; // the input RPFP Reporter *reporter; // object for logging + Reporter *conj_reporter; // object for logging conjectures Heuristic *heuristic; // expansion heuristic context &ctx; // Z3 context solver &slvr; // Z3 solver @@ -297,6 +300,7 @@ namespace Duality { int last_decisions; hash_set overapproxes; std::vector proposers; + std::string ConjectureFile; #ifdef BOUNDED struct Counter { @@ -310,6 +314,7 @@ namespace Duality { /** Solve the problem. */ virtual bool Solve(){ reporter = Report ? CreateStdoutReporter(rpfp) : new Reporter(rpfp); + conj_reporter = ConjectureFile.empty() ? 0 : CreateConjectureFileReporter(rpfp,ConjectureFile); #ifndef LOCALIZE_CONJECTURES heuristic = !cex.get_tree() ? new Heuristic(rpfp) : new ReplayHeuristic(rpfp,cex); #else @@ -340,6 +345,8 @@ namespace Duality { delete heuristic; // delete unwinding; // keep the unwinding for future mining of predicates delete reporter; + if(conj_reporter) + delete conj_reporter; for(unsigned i = 0; i < proposers.size(); i++) delete proposers[i]; return res; @@ -449,6 +456,9 @@ namespace Duality { if(option == "recursion_bound"){ return SetIntOption(RecursionBound,value); } + if(option == "conjecture_file"){ + ConjectureFile = value; + } return false; } @@ -1462,6 +1472,8 @@ namespace Duality { bool Update(Node *node, const RPFP::Transformer &fact, bool eager=false){ if(!node->Annotation.SubsetEq(fact)){ reporter->Update(node,fact,eager); + if(conj_reporter) + conj_reporter->Update(node,fact,eager); indset->Update(node,fact); updated_nodes.insert(node->map); node->Annotation.IntersectWith(fact); @@ -3043,6 +3055,10 @@ namespace Duality { }; }; + void stop(int event){ + if(event == 1932) + std::cout << "foo!\n"; + } class StreamReporter : public Reporter { std::ostream &s; @@ -3052,6 +3068,7 @@ namespace Duality { int event; int depth; void ev(){ + stop(event); s << "[" << event++ << "]" ; } virtual void Extend(RPFP::Node *node){ @@ -3129,4 +3146,28 @@ namespace Duality { Reporter *CreateStdoutReporter(RPFP *rpfp){ return new StreamReporter(rpfp, std::cout); } + + class ConjectureFileReporter : public Reporter { + std::ofstream s; + public: + ConjectureFileReporter(RPFP *_rpfp, const std::string &fname) + : Reporter(_rpfp), s(fname.c_str()) {} + virtual void Update(RPFP::Node *node, const RPFP::Transformer &update, bool eager){ + s << "(define-fun " << node->Name.name() << " ("; + for(unsigned i = 0; i < update.IndParams.size(); i++){ + if(i != 0) + s << " "; + s << "(" << update.IndParams[i] << " " << update.IndParams[i].get_sort() << ")"; + } + s << ") Bool \n"; + s << update.Formula << ")\n"; + s << std::endl; + } + }; + + Reporter *CreateConjectureFileReporter(RPFP *rpfp, const std::string &fname){ + return new ConjectureFileReporter(rpfp, fname); + } + } + diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h index 3ee7c3882..979717580 100755 --- a/src/duality/duality_wrapper.h +++ b/src/duality/duality_wrapper.h @@ -397,6 +397,11 @@ namespace Duality { sort array_domain() const; sort array_range() const; + + friend std::ostream & operator<<(std::ostream & out, sort const & m){ + m.ctx().print_expr(out,m); + return out; + } }; From 769b2b585bcab0d82b783acf1214f38ccf153724 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 2 May 2014 16:43:32 +0100 Subject: [PATCH 08/35] 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 09/35] 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 10/35] 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 a4f3afd70db0f33c35f760d22b803168d1e51423 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Mon, 5 May 2014 14:29:54 -0700 Subject: [PATCH 11/35] added fixedpoint.conjecture_file option --- src/muz/base/fixedpoint_params.pyg | 1 + src/muz/duality/duality_dl_interface.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg index e201c2a19..5bfbba6b2 100644 --- a/src/muz/base/fixedpoint_params.pyg +++ b/src/muz/base/fixedpoint_params.pyg @@ -77,6 +77,7 @@ def_module_params('fixedpoint', ('mbqi', BOOL, True, 'DUALITY: use model-based quantifier instantion'), ('batch_expand', BOOL, False, 'DUALITY: use batch expansion'), ('dump_aig', SYMBOL, '', 'Dump clauses in AIG text format (AAG) to the given file name'), + ('conjecture_file', STRING, '', 'DUALITY: save conjectures to file'), )) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index 99ac2ee1c..e23f3f7ef 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -211,6 +211,7 @@ lbool dl_interface::query(::expr * query) { rs->SetOption("use_underapprox",m_ctx.get_params().use_underapprox() ? "1" : "0"); rs->SetOption("stratified_inlining",m_ctx.get_params().stratified_inlining() ? "1" : "0"); rs->SetOption("batch_expand",m_ctx.get_params().batch_expand() ? "1" : "0"); + rs->SetOption("conjecture_file",m_ctx.get_params().conjecture_file()); unsigned rb = m_ctx.get_params().recursion_bound(); if(rb != UINT_MAX){ std::ostringstream os; os << rb; From 2a887a7608d97fb79d7e7c6c0e7e06d1e95bd6bf Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 9 May 2014 13:08:39 -0700 Subject: [PATCH 12/35] interp localization hack --- src/interp/iz3proof_itp.cpp | 30 ++++++++++++++++++++++++++++-- src/interp/iz3scopes.h | 5 +++++ 2 files changed, 33 insertions(+), 2 deletions(-) diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 8913920ac..8df83a79f 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -2682,10 +2682,21 @@ class iz3proof_itp_impl : public iz3proof_itp { return make(Equal,x,y); } + bool range_is_global(const prover::range &r){ + if(pv->range_contained(r,rng)) + return false; + if(!pv->ranges_intersect(r,rng)) + return false; + return true; + } + ast localize_term(ast e, const prover::range &rng, ast &pf){ - // we need to memoize this function per range - locmaps &maps = localization_maps_per_range[rng]; + // we need to memoize this function separately for A, B and global + prover::range map_range = rng; + if(range_is_global(map_range)) + map_range = pv->range_full(); + locmaps &maps = localization_maps_per_range[map_range]; hash_map &localization_map = maps.localization_map; hash_map &localization_pf_map = maps.localization_pf_map; @@ -2775,6 +2786,21 @@ class iz3proof_itp_impl : public iz3proof_itp { ast bar = make_assumption(frame,foo); pf = make_transitivity(new_var,e,orig_e,bar,pf); localization_pf_map[orig_e] = pf; + + // HACK: try to bias this term in the future + if(!pv->range_is_full(rng)){ + prover::range rf = pv->range_full(); + locmaps &fmaps = localization_maps_per_range[rf]; + hash_map &flocalization_map = fmaps.localization_map; + hash_map &flocalization_pf_map = fmaps.localization_pf_map; + // if(flocalization_map.find(orig_e) == flocalization_map.end()) + { + flocalization_map[orig_e] = new_var; + flocalization_pf_map[orig_e] = pf; + } + } + + return new_var; } diff --git a/src/interp/iz3scopes.h b/src/interp/iz3scopes.h index 23ab1c714..bf93f4726 100755 --- a/src/interp/iz3scopes.h +++ b/src/interp/iz3scopes.h @@ -64,6 +64,11 @@ class scopes { return rng.hi < rng.lo; } + /** is this range full? */ + bool range_is_full(const range &rng){ + return rng.lo == SHRT_MIN && rng.hi == SHRT_MAX; + } + /** return an empty range */ range range_empty(){ range res; From 90ca1b95c0ab1acaf9323074be7908f1acfd5cc8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 9 May 2014 13:10:03 -0700 Subject: [PATCH 13/35] debugging code in duality --- src/duality/duality_solver.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index ff3bc190b..326d51dc8 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -3043,6 +3043,7 @@ namespace Duality { }; }; + static int stop_event = -1; class StreamReporter : public Reporter { std::ostream &s; @@ -3052,6 +3053,9 @@ namespace Duality { int event; int depth; void ev(){ + if(stop_event == event){ + std::cout << "stop!"; + } s << "[" << event++ << "]" ; } virtual void Extend(RPFP::Node *node){ From aa35f988fc09506780522c3d790db99411e0dd2f Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 13 May 2014 14:58:32 -0700 Subject: [PATCH 14/35] fix for bad coefficient in AssignBounds --- src/interp/iz3translate.cpp | 85 ++++++++++++++++++++++++++++--------- 1 file changed, 64 insertions(+), 21 deletions(-) diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 060bb74ad..5aafa94f7 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1058,38 +1058,66 @@ public: } + rational get_first_coefficient(const ast &t, ast &v){ + if(op(t) == Plus){ + unsigned best_id = UINT_MAX; + rational best_coeff(0); + int nargs = num_args(t); + for(int i = 0; i < nargs; i++) + if(op(arg(t,i)) != Numeral){ + ast lv = get_linear_var(arg(t,i)); + unsigned id = ast_id(lv); + if(id < best_id) { + v = lv; + best_id = id; + best_coeff = get_coeff(arg(t,i)); + } + } + return best_coeff; + } + else + if(op(t) != Numeral) + return(get_coeff(t)); + return rational(0); + } + ast divide_inequalities(const ast &x, const ast&y){ - std::vector xcoeffs,ycoeffs; - get_linear_coefficients(arg(x,1),xcoeffs); - get_linear_coefficients(arg(y,1),ycoeffs); - if(xcoeffs.size() != ycoeffs.size() || xcoeffs.size() == 0) + ast xvar, yvar; + rational xcoeff = get_first_coefficient(arg(x,0),xvar); + rational ycoeff = get_first_coefficient(arg(y,0),yvar); + if(xcoeff == rational(0) || ycoeff == rational(0) || xvar != yvar) + throw "bad assign-bounds lemma"; + rational ratio = xcoeff/ycoeff; + if(denominator(ratio) != rational(1)) throw "bad assign-bounds lemma"; - rational ratio = xcoeffs[0]/ycoeffs[0]; return make_int(ratio); // better be integer! } ast AssignBounds2Farkas(const ast &proof, const ast &con){ std::vector farkas_coeffs; get_assign_bounds_coeffs(proof,farkas_coeffs); - if(farkas_coeffs[0] != make_int(rational(1))) - farkas_coeffs[0] = make_int(rational(1)); - std::vector lits; int nargs = num_args(con); if(nargs != (int)(farkas_coeffs.size())) throw "bad assign-bounds theory lemma"; #if 0 - for(int i = 1; i < nargs; i++) - lits.push_back(mk_not(arg(con,i))); - ast sum = sum_inequalities(farkas_coeffs,lits); - ast conseq = rhs_normalize_inequality(arg(con,0)); - ast d = divide_inequalities(sum,conseq); - std::vector my_coeffs; - my_coeffs.push_back(d); - for(unsigned i = 0; i < farkas_coeffs.size(); i++) - my_coeffs.push_back(farkas_coeffs[i]); + if(farkas_coeffs[0] != make_int(rational(1))) + farkas_coeffs[0] = make_int(rational(1)); #else - std::vector my_coeffs; + std::vector lits, lit_coeffs; + for(int i = 1; i < nargs; i++){ + lits.push_back(mk_not(arg(con,i))); + lit_coeffs.push_back(farkas_coeffs[i]); + } + ast sum = normalize_inequality(sum_inequalities(lit_coeffs,lits)); + ast conseq = normalize_inequality(arg(con,0)); + ast d = divide_inequalities(sum,conseq); +#if 0 + if(d != farkas_coeffs[0]) + std::cout << "wow!\n"; #endif + farkas_coeffs[0] = d; +#endif + std::vector my_coeffs; std::vector my_cons; for(int i = 1; i < nargs; i++){ my_cons.push_back(mk_not(arg(con,i))); @@ -1109,12 +1137,27 @@ public: ast AssignBoundsRule2Farkas(const ast &proof, const ast &con, std::vector prems){ std::vector farkas_coeffs; get_assign_bounds_rule_coeffs(proof,farkas_coeffs); - if(farkas_coeffs[0] != make_int(rational(1))) - farkas_coeffs[0] = make_int(rational(1)); - std::vector lits; int nargs = num_prems(proof)+1; if(nargs != (int)(farkas_coeffs.size())) throw "bad assign-bounds theory lemma"; +#if 0 + if(farkas_coeffs[0] != make_int(rational(1))) + farkas_coeffs[0] = make_int(rational(1)); +#else + std::vector lits, lit_coeffs; + for(int i = 1; i < nargs; i++){ + lits.push_back(conc(prem(proof,i-1))); + lit_coeffs.push_back(farkas_coeffs[i]); + } + ast sum = normalize_inequality(sum_inequalities(lit_coeffs,lits)); + ast conseq = normalize_inequality(con); + ast d = divide_inequalities(sum,conseq); +#if 0 + if(d != farkas_coeffs[0]) + std::cout << "wow!\n"; +#endif + farkas_coeffs[0] = d; +#endif std::vector my_coeffs; std::vector my_cons; for(int i = 1; i < nargs; i++){ From 669fded98aabf26b5b6a4915b8081164847d3ad5 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 13 May 2014 14:59:09 -0700 Subject: [PATCH 15/35] fix for possible problem in Farkas proofs in interp --- src/interp/iz3proof_itp.cpp | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 8df83a79f..01c252381 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -607,7 +607,29 @@ class iz3proof_itp_impl : public iz3proof_itp { return res; } + ast distribute_coeff(const ast &coeff, const ast &s){ + if(sym(s) == sum){ + if(sym(arg(s,2)) == sum) + return make(sum, + distribute_coeff(coeff,arg(s,0)), + make_int(rational(1)), + distribute_coeff(make(Times,coeff,arg(s,1)), arg(s,2))); + else + return make(sum, + distribute_coeff(coeff,arg(s,0)), + make(Times,coeff,arg(s,1)), + arg(s,2)); + } + if(op(s) == Leq && arg(s,1) == make_int(rational(0)) && arg(s,2) == make_int(rational(0))) + return s; + return make(sum,make(Leq,make_int(rational(0)),make_int(rational(0))),coeff,s); + } + ast simplify_sum(std::vector &args){ + if(args[1] != make_int(rational(1))){ + if(sym(args[2]) == sum) + return make(sum,args[0],make_int(rational(1)),distribute_coeff(args[1],args[2])); + } ast Aproves = mk_true(), Bproves = mk_true(); ast ineq = destruct_cond_ineq(args[0],Aproves,Bproves); if(!is_normal_ineq(ineq)) throw cannot_simplify(); From c9e9b30af6a9ff699188a1f7e7004a4feabec398 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 13 May 2014 17:28:22 -0700 Subject: [PATCH 16/35] interp handle mystery arith lemmas --- src/interp/iz3mgr.h | 5 ++++- src/interp/iz3translate.cpp | 14 ++++++++++++++ 2 files changed, 18 insertions(+), 1 deletion(-) diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 4ef594cee..3ec2c42d1 100755 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -387,10 +387,13 @@ class iz3mgr { return UnknownTheory; } - enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,UnknownKind}; + enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,ArithMysteryKind,UnknownKind}; lemma_kind get_theory_lemma_kind(const ast &proof){ symb s = sym(proof); + if(s->get_num_parameters() < 2) { + return ArithMysteryKind; // Bad -- Z3 hasn't told us + } ::symbol p0; bool ok = s->get_parameter(1).is_symbol(p0); if(!ok) return UnknownKind; diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index 5aafa94f7..e467da1fc 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1581,6 +1581,12 @@ public: return res; } + ast ArithMysteryRule(const ast &con, const std::vector &prems, const std::vector &args){ + // Hope for the best! + Iproof::node guess = reconstruct_farkas(prems,args,con); + return guess; + } + struct CannotCombineEqPropagate {}; void CombineEqPropagateRec(const ast &proof, std::vector &prems, std::vector &args, ast &eqprem){ @@ -1892,6 +1898,14 @@ public: res = EqPropagate(con,prems,args); break; } + case ArithMysteryKind: { + // Z3 hasn't told us what kind of lemma this is -- maybe we can guess + std::vector prems(nprems); + for(unsigned i = 0; i < nprems; i++) + prems[i] = prem(proof,i); + res = ArithMysteryRule(con,prems,args); + break; + } default: throw unsupported(); } From 95146483eaace2638eb6916af490184cc2342494 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 13 May 2014 18:15:51 -0700 Subject: [PATCH 17/35] add round-off to farkas resconstruction in interp --- src/interp/iz3translate.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp index e467da1fc..26786d57a 100755 --- a/src/interp/iz3translate.cpp +++ b/src/interp/iz3translate.cpp @@ -1364,8 +1364,13 @@ public: int nprems = prems.size(); std::vector npcons(nprems); hash_map pain_map; // not needed - for(int i = 0; i < nprems; i++) + for(int i = 0; i < nprems; i++){ npcons[i] = painfully_normalize_ineq(conc(prems[i]),pain_map); + if(op(npcons[i]) == Lt){ + ast constval = z3_simplify(make(Sub,arg(npcons[i],1),make_int(rational(1)))); + npcons[i] = make(Leq,arg(npcons[i],0),constval); + } + } ast ncon = painfully_normalize_ineq(mk_not(con),pain_map); npcons.push_back(ncon); From 3d1ca5ecc91a498a36cfbc39ff6a0d3a03f80d89 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 May 2014 21:12:16 -0700 Subject: [PATCH 18/35] 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 19/35] 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 20/35] 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 21/35] 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 b91cca8db9b95a9e5ef3240181a7fea0447febe3 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 20 May 2014 15:10:16 -0700 Subject: [PATCH 22/35] fix unbound variables bug in duality_dl_interface --- src/muz/duality/duality_dl_interface.cpp | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp index e23f3f7ef..0584e6b58 100755 --- a/src/muz/duality/duality_dl_interface.cpp +++ b/src/muz/duality/duality_dl_interface.cpp @@ -35,6 +35,7 @@ Revision History: #include "model_smt2_pp.h" #include "model_v2_pp.h" #include "fixedpoint_params.hpp" +#include "used_vars.h" // template class symbol_table; @@ -164,6 +165,20 @@ lbool dl_interface::query(::expr * query) { clauses.push_back(e); } + std::vector b_sorts; + std::vector b_names; + used_vars uv; + uv.process(query); + unsigned nuv = uv.get_max_found_var_idx_plus_1(); + for(int i = nuv-1; i >= 0; i--){ // var indices are backward + ::sort * s = uv.get(i); + if(!s) + s = _d->ctx.m().mk_bool_sort(); // missing var, whatever + b_sorts.push_back(sort(_d->ctx,s)); + b_names.push_back(symbol(_d->ctx,::symbol(i))); // names? + } + +#if 0 // turn the query into a clause expr q(_d->ctx,m_ctx.bind_variables(query,false)); @@ -177,6 +192,9 @@ lbool dl_interface::query(::expr * query) { } q = q.arg(0); } +#else + expr q(_d->ctx,query); +#endif expr qc = implies(q,_d->ctx.bool_val(false)); qc = _d->ctx.make_quant(Forall,b_sorts,b_names,qc); From 01c6fe39ab73ce2dfb1d1aba4f0b7aba154a170b Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Tue, 20 May 2014 15:10:31 -0700 Subject: [PATCH 23/35] fix markers aliasing bug in Duality::CheckerForEdgeClone --- src/duality/duality_solver.cpp | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp index 73fc986b1..26acf7e7c 100755 --- a/src/duality/duality_solver.cpp +++ b/src/duality/duality_solver.cpp @@ -738,6 +738,13 @@ namespace Duality { return ctx.constant(name.c_str(),ctx.bool_sort()); } + /** Make a boolean variable to act as a "marker" for a pair of nodes. */ + expr NodeMarker(Node *node1, Node *node2){ + std::string name = std::string("@m_") + string_of_int(node1->number); + name += std::string("_") + string_of_int(node2->number); + return ctx.constant(name.c_str(),ctx.bool_sort()); + } + /** Union the annotation of dst into src. If with_markers is true, we conjoin the annotation formula of dst with its marker. This allows us to discover which disjunct is @@ -1146,19 +1153,19 @@ namespace Duality { } - void GenNodeSolutionWithMarkersAux(Node *node, RPFP::Transformer &annot, expr &marker_disjunction){ + void GenNodeSolutionWithMarkersAux(Node *node, RPFP::Transformer &annot, expr &marker_disjunction, Node *other_node){ #ifdef BOUNDED if(RecursionBound >= 0 && NodePastRecursionBound(node)) return; #endif RPFP::Transformer temp = node->Annotation; - expr marker = NodeMarker(node); + expr marker = (!other_node) ? NodeMarker(node) : NodeMarker(node, other_node); temp.Formula = (!marker || temp.Formula); annot.IntersectWith(temp); marker_disjunction = marker_disjunction || marker; } - bool GenNodeSolutionWithMarkers(Node *node, RPFP::Transformer &annot, bool expanded_only = false){ + bool GenNodeSolutionWithMarkers(Node *node, RPFP::Transformer &annot, bool expanded_only = false, Node *other_node = 0){ bool res = false; annot.SetFull(); expr marker_disjunction = ctx.bool_val(false); @@ -1166,7 +1173,7 @@ namespace Duality { for(unsigned j = 0; j < insts.size(); j++){ Node *node = insts[j]; if(indset->Contains(insts[j])){ - GenNodeSolutionWithMarkersAux(node, annot, marker_disjunction); res = true; + GenNodeSolutionWithMarkersAux(node, annot, marker_disjunction, other_node); res = true; } } annot.Formula = annot.Formula && marker_disjunction; @@ -1263,7 +1270,7 @@ namespace Duality { Node *inst = insts[k]; if(indset->Contains(inst)){ if(checker->Empty(node) || - eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst)),ctx.bool_val(true))){ + eq(lb ? checker->Eval(lb,NodeMarker(inst)) : checker->dualModel.eval(NodeMarker(inst,node)),ctx.bool_val(true))){ candidate.Children.push_back(inst); goto next_child; } @@ -1346,7 +1353,7 @@ namespace Duality { for(unsigned j = 0; j < edge->Children.size(); j++){ Node *oc = edge->Children[j]; Node *nc = gen_cands_edge->Children[j]; - GenNodeSolutionWithMarkers(oc,nc->Annotation,true); + GenNodeSolutionWithMarkers(oc,nc->Annotation,true,nc); } checker->AssertEdge(gen_cands_edge,1,true); return root; From 2ee416fc8ffb069a309bc36cd992b71be68f43cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 May 2014 10:23:31 -0700 Subject: [PATCH 24/35] 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 25/35] 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]); } From 06b79cd9ea7827936e67bb2908e99f61355b2b3a Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 21 May 2014 13:30:54 -0700 Subject: [PATCH 26/35] trying to prevent quantifier in interp (leq2eq rule) --- src/interp/iz3proof_itp.cpp | 34 ++++++++++++++++++++++++++++------ 1 file changed, 28 insertions(+), 6 deletions(-) diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 01c252381..e89aa1d6d 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -779,6 +779,22 @@ class iz3proof_itp_impl : public iz3proof_itp { ast Bcond = my_implies(Bproves1,my_and(Aproves1,z3_simplify(ineq2))); // if(!is_true(Aproves1) || !is_true(Bproves1)) // std::cout << "foo!\n";; + if(y == make_int(rational(0)) && op(x) == Plus && num_args(x) == 2){ + if(get_term_type(arg(x,0)) == LitA){ + ast iter = z3_simplify(make(Plus,arg(x,0),get_ineq_rhs(xleqy))); + ast rewrite1 = make_rewrite(LitA,pos_add(0,top_pos),Acond,make(Equal,arg(x,0),iter)); + iter = make(Plus,iter,arg(x,1)); + ast rewrite2 = make_rewrite(LitB,top_pos,Bcond,make(Equal,iter,y)); + return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2); + } + if(get_term_type(arg(x,1)) == LitA){ + ast iter = z3_simplify(make(Plus,arg(x,1),get_ineq_rhs(xleqy))); + ast rewrite1 = make_rewrite(LitA,pos_add(1,top_pos),Acond,make(Equal,arg(x,1),iter)); + iter = make(Plus,arg(x,0),iter); + ast rewrite2 = make_rewrite(LitB,top_pos,Bcond,make(Equal,iter,y)); + return chain_cons(chain_cons(mk_true(),rewrite1),rewrite2); + } + } if(get_term_type(x) == LitA){ ast iter = z3_simplify(make(Plus,x,get_ineq_rhs(xleqy))); ast rewrite1 = make_rewrite(LitA,top_pos,Acond,make(Equal,x,iter)); @@ -1036,6 +1052,7 @@ class iz3proof_itp_impl : public iz3proof_itp { coeff = argpos ? make_int(rational(-1)) : make_int(rational(1)); break; case Not: + coeff = make_int(rational(-1)); case Plus: break; case Times: @@ -2590,12 +2607,17 @@ class iz3proof_itp_impl : public iz3proof_itp { break; default: { // mixed equality if(get_term_type(x) == LitMixed || get_term_type(y) == LitMixed){ - // std::cerr << "WARNING: mixed term in leq2eq\n"; - std::vector lits; - lits.push_back(con); - lits.push_back(make(Not,xleqy)); - lits.push_back(make(Not,yleqx)); - return make_axiom(lits); + if(y == make_int(rational(0)) && op(x) == Plus && num_args(x) == 2){ + // std::cerr << "WARNING: untested case in leq2eq\n"; + } + else { + // std::cerr << "WARNING: mixed term in leq2eq\n"; + std::vector lits; + lits.push_back(con); + lits.push_back(make(Not,xleqy)); + lits.push_back(make(Not,yleqx)); + return make_axiom(lits); + } } std::vector conjs; conjs.resize(3); conjs[0] = mk_not(con); From 97c5d09de1ffb10b2847cba765c2ec165cf9efc0 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 21 May 2014 16:56:18 -0700 Subject: [PATCH 27/35] turn off a windows warning --- src/interp/iz3hash.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/interp/iz3hash.h b/src/interp/iz3hash.h index a12cfb990..cd94f0e04 100644 --- a/src/interp/iz3hash.h +++ b/src/interp/iz3hash.h @@ -29,6 +29,10 @@ Revision History: #ifndef IZ3_HASH_H #define IZ3_HASH_H +#ifdef _WINDOWS +#pragma warning(disable:4267) +#endif + #include #include #include From aba79802cfb5a4b2e1a0e64efa4e4ab52058f946 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 25 May 2014 21:01:10 -0700 Subject: [PATCH 28/35] fix warning about unused variable Signed-off-by: Nikolaj Bjorner --- src/muz/transforms/dl_mk_coi_filter.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/muz/transforms/dl_mk_coi_filter.cpp b/src/muz/transforms/dl_mk_coi_filter.cpp index c7a8d5aa0..cdb4a5b9e 100644 --- a/src/muz/transforms/dl_mk_coi_filter.cpp +++ b/src/muz/transforms/dl_mk_coi_filter.cpp @@ -205,7 +205,6 @@ namespace datalog { 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)) { From 4da56aa4dff9b7830ffcb7d393d8b367c0d3774d Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 29 May 2014 12:41:07 +0100 Subject: [PATCH 29/35] added debug assertion Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 9233a41dc..4eae61c3d 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -4128,6 +4128,7 @@ class Datatype: """ if __debug__: _z3_assert(isinstance(name, str), "String expected") + _z3_assert(name != "") return self.declare_core(name, "is_" + name, *args) def __repr__(self): From 756645326bb2c0578b340e05e03c8276cacd1dd9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 29 May 2014 17:33:03 +0100 Subject: [PATCH 30/35] Bugfix for And/Or operators in Python. Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 27 +++++++++++++++++++++++---- 1 file changed, 23 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 4eae61c3d..ff0bd6641 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -899,6 +899,7 @@ def _coerce_expr_merge(s, a): return s else: if __debug__: + _z3_assert(s1.ctx == s.ctx, "context mismatch") _z3_assert(False, "sort mismatch") else: return s @@ -1459,9 +1460,18 @@ def And(*args): >>> And(P) And(p__0, p__1, p__2, p__3, p__4) """ - args = _get_args(args) - ctx = _ctx_from_ast_arg_list(args) + last_arg = None + if len(args) > 0: + last_arg = args[len(args)-1] + if isinstance(last_arg, Context): + ctx = args[len(args)-1] + args = args[:len(args)-1] + else: + ctx = main_ctx() + args = _get_args(args) + ctx_args = _ctx_from_ast_arg_list(args, ctx) if __debug__: + _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch") _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): return _probe_and(args, ctx) @@ -1480,9 +1490,18 @@ def Or(*args): >>> Or(P) Or(p__0, p__1, p__2, p__3, p__4) """ - args = _get_args(args) - ctx = _ctx_from_ast_arg_list(args) + last_arg = None + if len(args) > 0: + last_arg = args[len(args)-1] + if isinstance(last_arg, Context): + ctx = args[len(args)-1] + args = args[:len(args)-1] + else: + ctx = main_ctx() + args = _get_args(args) + ctx_args = _ctx_from_ast_arg_list(args, ctx) if __debug__: + _z3_assert(ctx_args == None or ctx_args == ctx, "context mismatch") _z3_assert(ctx != None, "At least one of the arguments must be a Z3 expression or probe") if _has_probe(args): return _probe_or(args, ctx) From 1e774064bc9fbfde8c873c6664044b7e28645363 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 30 May 2014 12:26:55 +0100 Subject: [PATCH 31/35] assertion bug fix in z3py Signed-off-by: Christoph M. Wintersteiger --- src/api/python/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3.py b/src/api/python/z3.py index ff0bd6641..ce53a4c1f 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -4147,7 +4147,7 @@ class Datatype: """ if __debug__: _z3_assert(isinstance(name, str), "String expected") - _z3_assert(name != "") + _z3_assert(name != "", "Constructor name cannot be empty") return self.declare_core(name, "is_" + name, *args) def __repr__(self): From 49f9f4b3b53191e965e7a59dfd3b4868caa719ca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 30 May 2014 20:52:39 +0530 Subject: [PATCH 32/35] fix crash in model construction from finite domain theory Signed-off-by: Nikolaj Bjorner --- src/ast/dl_decl_plugin.cpp | 18 +++++++++++++++++- src/ast/dl_decl_plugin.h | 2 ++ src/smt/smt_model_generator.cpp | 2 ++ src/smt/theory_dl.cpp | 7 +++---- 4 files changed, 24 insertions(+), 5 deletions(-) diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 6d0823a24..badf8a59d 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -599,7 +599,23 @@ namespace datalog { return 0; } result = mk_compare(OP_DL_LT, m_lt_sym, domain); - break; + break; + + case OP_DL_REP: { + if (!check_domain(0, 0, num_parameters) || + !check_domain(1, 1, arity)) return 0; + func_decl_info info(m_family_id, k, 0, 0); + result = m_manager->mk_func_decl(symbol("rep"), 1, domain, range, info); + break; + } + + case OP_DL_ABS: { + if (!check_domain(0, 0, num_parameters) || + !check_domain(1, 1, arity)) return 0; + func_decl_info info(m_family_id, k, 0, 0); + result = m_manager->mk_func_decl(symbol("abs"), 1, domain, range, info); + break; + } default: m_manager->raise_exception("operator not recognized"); diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h index a662de578..65b00235c 100644 --- a/src/ast/dl_decl_plugin.h +++ b/src/ast/dl_decl_plugin.h @@ -48,6 +48,8 @@ namespace datalog { OP_RA_CLONE, OP_DL_CONSTANT, OP_DL_LT, + OP_DL_REP, + OP_DL_ABS, LAST_RA_OP }; diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index cf22c3e3a..6c138fd57 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -102,6 +102,7 @@ namespace smt { if (th && th->build_models()) { if (r->get_th_var(th->get_id()) != null_theory_var) { proc = th->mk_value(r, *this); + SASSERT(proc); } else { TRACE("model_bug", tout << "creating fresh value for #" << r->get_owner_id() << "\n";); @@ -110,6 +111,7 @@ namespace smt { } else { proc = mk_model_value(r); + SASSERT(proc); } } SASSERT(proc); diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 4ef1bd8e0..fc9138bf6 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -162,7 +162,7 @@ namespace smt { m.register_factory(alloc(dl_factory, m_util, m.get_model())); } - virtual smt::model_value_proc * mk_value(smt::enode * n) { + virtual smt::model_value_proc * mk_value(smt::enode * n, smt::model_generator&) { return alloc(dl_value_proc, *this, n); } @@ -201,9 +201,8 @@ namespace smt { if(!m_reps.find(s, r) || !m_vals.find(s,v)) { SASSERT(!m_reps.contains(s)); sort* bv = b().mk_sort(64); - // TBD: filter these from model. - r = m().mk_fresh_func_decl("rep",1, &s,bv); - v = m().mk_fresh_func_decl("val",1, &bv,s); + r = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_REP, 0, 0, 1, &s, bv); + v = m().mk_func_decl(m_util.get_family_id(), datalog::OP_DL_ABS, 0, 0, 1, &bv, s); m_reps.insert(s, r); m_vals.insert(s, v); add_trail(r); From bc25ea404fc251bb3343bb724abf8cef24356947 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 30 May 2014 18:14:33 +0100 Subject: [PATCH 33/35] Fixed potential bug (warning on OSX). Signed-off-by: Christoph M. Wintersteiger --- src/smt/theory_arith_eq.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h index 04e16e778..368ccb87d 100644 --- a/src/smt/theory_arith_eq.h +++ b/src/smt/theory_arith_eq.h @@ -193,7 +193,7 @@ namespace smt { return true; } - if (!r.get_base_var() == x && x > y) { + if (r.get_base_var() != x && x > y) { std::swap(x, y); k.neg(); } From f76b343bfa4d65417e2366da199189617604fa3a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 May 2014 11:25:54 +0530 Subject: [PATCH 34/35] expose parameter settings for controlling injectivity axiom. rquested by Jasmin Blanchette Signed-off-by: Nikolaj Bjorner --- src/smt/params/preprocessor_params.cpp | 1 + src/smt/params/smt_params_helper.pyg | 1 + 2 files changed, 2 insertions(+) diff --git a/src/smt/params/preprocessor_params.cpp b/src/smt/params/preprocessor_params.cpp index 4799b8b9f..9ad787c2a 100644 --- a/src/smt/params/preprocessor_params.cpp +++ b/src/smt/params/preprocessor_params.cpp @@ -23,6 +23,7 @@ void preprocessor_params::updt_local_params(params_ref const & _p) { smt_params_helper p(_p); m_macro_finder = p.macro_finder(); m_pull_nested_quantifiers = p.pull_nested_quantifiers(); + m_refine_inj_axiom = p.refine_inj_axioms(); } void preprocessor_params::updt_params(params_ref const & p) { diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 50bb6422b..869b8cdc4 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -14,6 +14,7 @@ def_module_params(module_name='smt', ('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'), ('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ingored if delay_units is false'), ('pull_nested_quantifiers', BOOL, False, 'pull nested quantifiers'), + ('refine_inj_axioms', BOOL, True, 'refine injectivity axioms'), ('soft_timeout', UINT, 0, 'soft timeout (0 means no timeout)'), ('mbqi', BOOL, True, 'model based quantifier instantiation (MBQI)'), ('mbqi.max_cexs', UINT, 1, 'initial maximal number of counterexamples used in MBQI, each counterexample generates a quantifier instantiation'), From 88bd01bc4fabb2800b3abfe6badf2bd3ae0fa68e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 3 Jun 2014 23:03:34 +0530 Subject: [PATCH 35/35] patching non-termination bug in datatype factory, reported by Tiago Signed-off-by: Nikolaj Bjorner --- src/smt/proto_model/datatype_factory.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/smt/proto_model/datatype_factory.cpp b/src/smt/proto_model/datatype_factory.cpp index 5e66ab738..3b0ec8e5f 100644 --- a/src/smt/proto_model/datatype_factory.cpp +++ b/src/smt/proto_model/datatype_factory.cpp @@ -191,8 +191,10 @@ expr * datatype_factory::get_fresh_value(sort * s) { // Approach 2) // For recursive datatypes. // search for constructor... + unsigned num_iterations = 0; if (m_util.is_recursive(s)) { while(true) { + ++num_iterations; TRACE("datatype_factory", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";); ptr_vector const * constructors = m_util.get_datatype_constructors(s); ptr_vector::const_iterator it = constructors->begin(); @@ -212,7 +214,13 @@ expr * datatype_factory::get_fresh_value(sort * s) { << 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); + expr * maybe_new_arg = 0; + if (num_iterations <= 1) { + maybe_new_arg = get_almost_fresh_value(s_arg); + } + else { + maybe_new_arg = get_fresh_value(s_arg); + } if (!maybe_new_arg) { TRACE("datatype_factory", tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";); @@ -231,6 +239,7 @@ expr * datatype_factory::get_fresh_value(sort * s) { if (found_sibling) { expr_ref new_value(m_manager); new_value = m_manager.mk_app(constructor, args.size(), args.c_ptr()); + TRACE("datatype_factory", tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";); m_last_fresh_value.insert(s, new_value); if (!set->contains(new_value)) { register_value(new_value);