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

Z3str3: refactor regex automata to subroutine, use arith_value

Browse source
This commit is contained in:
Murphy Berzish 2018-09-17 16:13:34 -04:00
parent 5bbe0508e4
commit 7e419137b1
5 changed files with 745 additions and 776 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_arith_value.cpp
View file

@ -96,4 +96,10 @@ namespace smt {
while (next != n); while (next != n);
return false; return false;
} }
final_check_status arith_value::final_check() {
family_id afid = a.get_family_id();
theory * th = m_ctx.get_theory(afid);
return th->final_check_eh();
}
}; };

1
src/smt/smt_arith_value.h
View file

@ -33,5 +33,6 @@ namespace smt {
bool get_lo(expr* e, rational& lo, bool& strict); bool get_lo(expr* e, rational& lo, bool& strict);
bool get_up(expr* e, rational& up, bool& strict); bool get_up(expr* e, rational& up, bool& strict);
bool get_value(expr* e, rational& value); bool get_value(expr* e, rational& value);
final_check_status final_check();
}; };
}; };

1
src/smt/smt_theory.h
View file

@ -36,6 +36,7 @@ namespace smt {
unsigned_vector m_var2enode_lim; unsigned_vector m_var2enode_lim;
friend class context; friend class context;
friend class arith_value;
protected: protected:
virtual void init(context * ctx); virtual void init(context * ctx);

1511
src/smt/theory_str.cpp
View file

File diff suppressed because it is too large Load diff

2
src/smt/theory_str.h
View file

@ -30,6 +30,7 @@
#include "smt/params/theory_str_params.h" #include "smt/params/theory_str_params.h"
#include "smt/proto_model/value_factory.h" #include "smt/proto_model/value_factory.h"
#include "smt/smt_model_generator.h" #include "smt/smt_model_generator.h"
#include "smt/smt_arith_value.h"
#include<set> #include<set>
#include<stack> #include<stack>
#include<vector> #include<vector>
@ -546,6 +547,7 @@ protected:
void process_concat_eq_unroll(expr * concat, expr * unroll); void process_concat_eq_unroll(expr * concat, expr * unroll);
// regex automata and length-aware regex // regex automata and length-aware regex
void solve_regex_automata();
unsigned estimate_regex_complexity(expr * re); unsigned estimate_regex_complexity(expr * re);
unsigned estimate_regex_complexity_under_complement(expr * re); unsigned estimate_regex_complexity_under_complement(expr * re);
unsigned estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2); unsigned estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2);