mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-17 19:36:17 +00:00
Code Activity

block selected configurations from HORN tactic

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-07 19:14:01 -07:00
parent 35f184a6b9
commit 6e7e53e25c
2 changed files with 36 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

27
src/muz/fp/horn_tactic.cpp
View file

@ -16,20 +16,20 @@ Author:
Revision History: Revision History:
--*/ --*/
#include "ast/ast_util.h"
#include "ast/rewriter/var_subst.h"
#include "ast/rewriter/expr_replacer.h"
#include "tactic/tactical.h" #include "tactic/tactical.h"
#include "tactic/model_converter.h" #include "tactic/model_converter.h"
#include "tactic/proof_converter.h" #include "tactic/proof_converter.h"
#include "tactic/generic_model_converter.h"
#include "muz/fp/horn_tactic.h" #include "muz/fp/horn_tactic.h"
#include "muz/base/dl_context.h" #include "muz/base/dl_context.h"
#include "muz/fp/dl_register_engine.h" #include "muz/fp/dl_register_engine.h"
#include "ast/rewriter/expr_replacer.h"
#include "muz/base/dl_rule_transformer.h" #include "muz/base/dl_rule_transformer.h"
#include "muz/transforms/dl_mk_slice.h" #include "muz/transforms/dl_mk_slice.h"
#include "tactic/generic_model_converter.h"
#include "muz/transforms/dl_transforms.h" #include "muz/transforms/dl_transforms.h"
#include "muz/base/fp_params.hpp" #include "muz/base/fp_params.hpp"
#include "ast/ast_util.h"
#include "ast/rewriter/var_subst.h"
class horn_tactic : public tactic { class horn_tactic : public tactic {
struct imp { struct imp {
@ -194,6 +194,8 @@ class horn_tactic : public tactic {
expr_ref_vector queries(m); expr_ref_vector queries(m);
std::stringstream msg; std::stringstream msg;
check_parameters();
m_ctx.reset(); m_ctx.reset();
m_ctx.ensure_opened(); m_ctx.ensure_opened();
@ -228,6 +230,7 @@ class horn_tactic : public tactic {
mc1->hide(q); mc1->hide(q);
g->add(mc1); g->add(mc1);
} }
SASSERT(queries.size() == 1); SASSERT(queries.size() == 1);
q = queries[0].get(); q = queries[0].get();
proof_converter_ref pc = g->pc(); proof_converter_ref pc = g->pc();
@ -343,8 +346,24 @@ class horn_tactic : public tactic {
g->set_prec(goal::UNDER_OVER); g->set_prec(goal::UNDER_OVER);
} }
void check_parameters() {
fp_params const& p = m_ctx.get_params();
if (p.engine() == symbol("datalog"))
not_supported();
if (p.datalog_generate_explanations())
not_supported();
if (p.datalog_magic_sets_for_queries())
not_supported();
}
void not_supported() {
throw default_exception("unsupported parameter combination passed to HORN tactic");
}
}; };
bool m_is_simplify; bool m_is_simplify;
params_ref m_params; params_ref m_params;
statistics m_stats; statistics m_stats;

25
src/muz/rel/dl_compiler.cpp
View file

@ -819,15 +819,15 @@ namespace datalog {
aci.domain=head_sig[i]; aci.domain=head_sig[i];
expr * exp = h->get_arg(i); expr * exp = h->get_arg(i);
if(is_var(exp)) { if (is_var(exp)) {
unsigned var_num=to_var(exp)->get_idx(); unsigned var_num = to_var(exp)->get_idx();
int2ints::entry * e = var_indexes.find_core(var_num); int2ints::entry* e = var_indexes.find_core(var_num);
if(e) { if (e) {
unsigned_vector & binding_indexes = e->get_data().m_value; unsigned_vector& binding_indexes = e->get_data().m_value;
aci.kind=ACK_BOUND_VAR; aci.kind = ACK_BOUND_VAR;
aci.source_column=binding_indexes.back(); aci.source_column = binding_indexes.back();
SASSERT(aci.source_column<single_res_expr.size()); //we bind only to existing columns SASSERT(aci.source_column < single_res_expr.size()); //we bind only to existing columns
if(binding_indexes.size()>1) { if (binding_indexes.size() > 1) {
//if possible, we do not want multiple head columns //if possible, we do not want multiple head columns
//point to a single column in the intermediate table, //point to a single column in the intermediate table,
//since then we would have to duplicate the column //since then we would have to duplicate the column
@ -836,13 +836,14 @@ namespace datalog {
} }
} }
else { else {
aci.kind=ACK_UNBOUND_VAR; aci.kind = ACK_UNBOUND_VAR;
aci.var_index=var_num; aci.var_index = var_num;
} }
} }
else { else {
SASSERT(is_app(exp)); SASSERT(is_app(exp));
SASSERT(m_context.get_decl_util().is_numeral_ext(exp)); if (!m_context.get_decl_util().is_numeral_ext(exp))
throw default_exception("could not process non-numeral in Datalog engine");
aci.kind=ACK_CONSTANT; aci.kind=ACK_CONSTANT;
aci.constant=to_app(exp); aci.constant=to_app(exp);
} }