mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-21 05:13:39 +00:00
Code Activity

ensure that variables passed to consequence finding have bound constraints, if applicable. Even if those variables do not occur in the constraints

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-10-28 07:41:27 -07:00
parent 4d078dc0a9
commit 2475f3bff5
1 changed files with 12 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/tactic/portfolio/enum2bv_solver.cpp
View file

@ -102,9 +102,20 @@ public:
datatype_util dt(m); datatype_util dt(m);
bv_util bv(m); bv_util bv(m);
expr_ref_vector bvars(m), conseq(m), bounds(m);
// ensure that enumeration variables that
// don't occur in the constraints
// are also internalized.
for (unsigned i = 0; i < vars.size(); ++i) {
expr_ref tmp(m.mk_eq(vars[i], vars[i]), m);
proof_ref proof(m);
m_rewriter(tmp, tmp, proof);
}
m_rewriter.flush_side_constraints(bounds);
m_solver->assert_expr(bounds);
// translate enumeration constants to bit-vectors. // translate enumeration constants to bit-vectors.
expr_ref_vector bvars(m), conseq(m);
for (unsigned i = 0; i < vars.size(); ++i) { for (unsigned i = 0; i < vars.size(); ++i) {
func_decl* f; func_decl* f;
if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) { if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) {