mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-01 21:49:29 +00:00
Code Activity

fix bug in replace built-in and move length-equality propagation to branch final check

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-02-09 11:08:33 +00:00
parent 3ef6d91038
commit 133e3693de
3 changed files with 115 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_seq.h
View file

@ -337,6 +337,7 @@ namespace smt {
bool get_length(expr* s, expr_ref& len, literal_vector& lits);
bool reduce_length(expr* l, expr* r, literal_vector& lits);
bool reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps);
bool reduce_length(unsigned i, unsigned j, bool front, expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps);
expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); }
expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); }
@ -429,6 +430,10 @@ namespace smt {
void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal);
expr_ref mk_sub(expr* a, expr* b);
enode* ensure_enode(expr* a);
dependency* mk_join(dependency* deps, literal lit);
dependency* mk_join(dependency* deps, literal_vector const& lits);
// arithmetic integration
bool lower_bound(expr* s, rational& lo);