mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

recognize array and bv theories in HORN format

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-20 10:42:59 -08:00
parent a20c4ad199
commit 01ddb20441
2 changed files with 16 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/cmd_context/cmd_context.cpp
View file

@ -477,7 +477,8 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
s == "QF_UFBV" ||
s == "QF_ABV" ||
s == "QF_AUFBV" ||
s == "QF_BVRE";
s == "QF_BVRE" ||
s == "HORN";
}
bool cmd_context::logic_has_horn(symbol const& s) const {
@ -518,7 +519,8 @@ bool cmd_context::logic_has_array_core(symbol const & s) const {
s == "AUFBV" ||
s == "ABV" ||
s == "QF_ABV" ||
s == "QF_AUFBV";
s == "QF_AUFBV" ||
s == "HORN";
}
bool cmd_context::logic_has_array() const {

20
src/muz_qe/qe_lite.cpp
View file

@ -340,15 +340,23 @@ class der2 {
}
}
void apply_substitution(quantifier * q, expr_ref & r) {
void flatten_args(quantifier* q, unsigned& num_args, expr*const*& args) {
expr * e = q->get_expr();
unsigned num_args = 1;
expr* const* args = &e;
num_args = 1;
args = &e;
if ((q->is_forall() && m.is_or(e)) ||
(q->is_exists() && m.is_and(e))) {
num_args = to_app(e)->get_num_args();
args = to_app(e)->get_args();
}
}
void apply_substitution(quantifier * q, expr_ref & r) {
expr * e = q->get_expr();
unsigned num_args = 1;
expr* const* args = &e;
flatten_args(q, num_args, args);
bool_rewriter rw(m);
// get a new expression
@ -395,11 +403,7 @@ class der2 {
set_is_variable_proc(is_v);
unsigned num_args = 1;
expr* const* args = &e;
if ((q->is_forall() && m.is_or(e)) ||
(q->is_exists() && m.is_and(e))) {
num_args = to_app(e)->get_num_args();
args = to_app(e)->get_args();
}
flatten_args(q, num_args, args);
unsigned def_count = 0;
unsigned largest_vinx = 0;