#include <sstream>
#include <sys/types.h>
#include <sys/stat.h>
#include "ast/ast_pp.h"
#include "ast/rewriter/bool_rewriter.h"
#include "ast/for_each_expr.h"
#include "ast/scoped_proof.h"
#include "muz/base/dl_context.h"
#include "muz/base/dl_rule.h"
#include "muz/base/dl_util.h"
#include "util/stopwatch.h"
#ifdef _WINDOWS
#include <windows.h>
#endif
#ifndef __STDC_FORMAT_MACROS
#define __STDC_FORMAT_MACROS
#endif
#include <inttypes.h>
namespace datalog {
verbose_action::verbose_action(char const* msg, unsigned lvl): m_lvl(lvl), m_sw(nullptr) {
IF_VERBOSE(m_lvl,
(verbose_stream() << msg << "...").flush();
m_sw = alloc(stopwatch);
m_sw->start(););
}
verbose_action::~verbose_action() {
double sec = 0.0;
if (m_sw) m_sw->stop();
sec = m_sw?m_sw->get_seconds():0.0;
if (sec < 0.001) sec = 0.0;
IF_VERBOSE(m_lvl,
(verbose_stream() << sec << "s\n").flush();
);
dealloc(m_sw);
}
bool contains_var(expr * trm, unsigned var_idx) {
expr_free_vars fv;
fv(trm);
return fv.contains(var_idx);
}
unsigned count_variable_arguments(app * pred)
{
SASSERT(is_uninterp(pred));
unsigned res = 0;
unsigned n = pred->get_num_args();
for (unsigned i = 0; i < n; ++i) {
expr * arg = pred->get_arg(i);
if (is_var(arg)) {
res++;
}
}
return res;
}
void mk_new_rule_tail(ast_manager & m, app * pred, var_idx_set const & non_local_vars, unsigned & next_idx, varidx2var_map & varidx2var,
sort_ref_buffer & new_rule_domain, expr_ref_buffer & new_rule_args, app_ref & new_pred) {
expr_ref_buffer new_args(m);
unsigned n = pred->get_num_args();
for (unsigned i = 0; i < n; ++i) {
expr * arg = pred->get_arg(i);
if (m.is_value(arg)) {
new_args.push_back(arg);
}
else {
SASSERT(is_var(arg));
int vidx = to_var(arg)->get_idx();
var * new_var = nullptr;
if (!varidx2var.find(vidx, new_var)) {
new_var = m.mk_var(next_idx, to_var(arg)->get_sort());
next_idx++;
varidx2var.insert(vidx, new_var);
if (non_local_vars.contains(vidx)) {
new_rule_domain.push_back(to_var(arg)->get_sort());
new_rule_args.push_back(new_var);
}
}
SASSERT(new_var != 0);
new_args.push_back(new_var);
}
}
new_pred = m.mk_app(pred->get_decl(), new_args.size(), new_args.data());
}
void apply_subst(expr_ref_vector& tgt, expr_ref_vector const& sub) {
ast_manager& m = tgt.get_manager();
var_subst vs(m, false);
expr_ref tmp(m);
for (unsigned i = 0; i < tgt.size(); ++i) {
if (tgt[i].get()) {
tgt[i] = vs(tgt[i].get(), sub.size(), sub.data());
}
else {
tgt[i] = sub[i];
}
}
for (unsigned i = tgt.size(); i < sub.size(); ++i) {
tgt.push_back(sub[i]);
}
}
void output_predicate(context & ctx, app * f, std::ostream & out)
{
func_decl * pred_decl = f->get_decl();
unsigned arity = f->get_num_args();
out << pred_decl->get_name() << '(';
for (unsigned i = 0; i < arity; ++i) {
expr * arg = f->get_arg(i);
if (i != 0) {
out << ',';
}
if (is_var(arg)) {
out << "#" << to_var(arg)->get_idx();
}
else {
out << mk_pp(arg, ctx.get_manager());
}
}
out << ")";
}
void display_predicate(context & ctx, app * f, std::ostream & out)
{
output_predicate(ctx, f, out);
out << "\n";
}
void display_fact(context & ctx, app * f, std::ostream & out)
{
func_decl * pred_decl = f->get_decl();
unsigned arity = f->get_num_args();
out << "\t(";
for(unsigned i = 0; i < arity; ++i) {
if (i != 0) {
out << ',';
}
expr * arg = f->get_arg(i);
uint64_t sym_num;
SASSERT(is_app(arg));
VERIFY( ctx.get_decl_util().is_numeral_ext(to_app(arg), sym_num) );
relation_sort sort = pred_decl->get_domain(i);
out << ctx.get_argument_name(pred_decl, i) << '=';
ctx.print_constant_name(sort, sym_num, out);
out << '(' << sym_num << ')';
}
out << ")\n";
}
void idx_set_union(idx_set & tgt, const idx_set & src) {
idx_set::iterator vit = src.begin();
idx_set::iterator vend = src.end();
for(;vit!=vend;++vit) {
tgt.insert(*vit);
}
}
bool variable_intersection::values_match(const expr * v1, const expr * v2)
{
return v1==v2;
}
bool variable_intersection::args_match(const app * f1, const app * f2)
{
unsigned n=size();
for (unsigned i = 0; i < n; ++i) {
unsigned f1_index, f2_index;
get(i, f1_index, f2_index);
if (!values_match(f1->get_arg(f1_index),f2->get_arg(f2_index))) {
return false;
}
}
return true;
}
bool variable_intersection::args_self_match(const app * f)
{
if(!args_match(f,f)) {
return false;
}
unsigned n = m_const_indexes.size();
for(unsigned i=0; i<n; ++i) {
unsigned f_index = m_const_indexes[i];
if(!values_match(f->get_arg(f_index), m_consts[i].get())) {
return false;
}
}
return true;
}
void variable_intersection::populate_self(const app * a)
{
SASSERT(is_uninterp(a));
unsigned arity = a->get_num_args();
for(unsigned i1=0; i1<arity; ++i1) {
expr * e1=a->get_arg(i1);
if(is_var(e1)) {
var* v1=to_var(e1);
for(unsigned i2=i1+1; i2<arity; ++i2) {
expr * e2=a->get_arg(i2);
if(!is_var(e2)) {
continue;
}
var* v2=to_var(e2);
if(v1->get_idx()==v2->get_idx()) {
add_pair(i1, i2);
}
}
}
else {
SASSERT(is_app(e1));
app * c1 = to_app(e1);
SASSERT(c1->get_num_args()==0);
m_const_indexes.push_back(i1);
m_consts.push_back(c1);
SASSERT(m_const_indexes.size()==m_consts.size());
}
}
}
void rule_counter::count_rule_vars(const rule * r, int coef) {
reset();
count_vars(r->get_head(), 1);
unsigned n = r->get_tail_size();
for (unsigned i = 0; i < n; ++i) {
count_vars(r->get_tail(i), coef);
}
}
unsigned rule_counter::get_max_rule_var(const rule & r) {
m_todo.push_back(r.get_head());
m_scopes.push_back(0);
unsigned n = r.get_tail_size();
bool has_var = false;
for (unsigned i = 0; i < n; ++i) {
m_todo.push_back(r.get_tail(i));
m_scopes.push_back(0);
}
return get_max_var(has_var);
}
void del_rule(horn_subsume_model_converter* mc, rule& r, lbool unreachable) {
if (mc) {
ast_manager& m = mc->get_manager();
expr_ref_vector body(m);
TRACE(dl, tout << "unreachable: " << unreachable << " " << r.get_decl()->get_name() << "\n");
switch (unreachable) {
case l_true:
body.push_back(m.mk_true());
break;
case l_false:
body.push_back(m.mk_false());
break;
default:
for (unsigned i = 0; i < r.get_tail_size(); ++i) {
if (r.is_neg_tail(i)) {
body.push_back(m.mk_not(r.get_tail(i)));
}
else {
body.push_back(r.get_tail(i));
}
}
break;
}
TRACE(dl,
tout << mk_pp(r.get_head(), m) << " :- \n";
for (unsigned i = 0; i < body.size(); ++i) {
tout << mk_pp(body.get(i), m) << "\n";
});
mc->insert(r.get_head(), body.size(), body.data());
}
}
void resolve_rule(rule_manager& rm,
replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx,
expr_ref_vector const& s1, expr_ref_vector const& s2, rule const& res) {
if (!pc) return;
ast_manager& m = s1.get_manager();
expr_ref fml1(m), fml2(m), fml3(m);
rm.to_formula(r1, fml1);
rm.to_formula(r2, fml2);
rm.to_formula(res, fml3);
vector<expr_ref_vector> substs;
svector<std::pair<unsigned, unsigned> > positions;
substs.push_back(s1);
substs.push_back(s2);
scoped_proof _sc(m);
proof_ref pr(m);
proof_ref_vector premises(m);
premises.push_back(m.mk_asserted(fml1));
premises.push_back(m.mk_asserted(fml2));
positions.push_back(std::make_pair(idx+1, 0));
TRACE(dl,
tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
for (unsigned i = 0; i < s1.size(); ++i) {
tout << mk_pp(s1[i], m) << " ";
}
tout << "\n";
tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";
for (unsigned i = 0; i < s2.size(); ++i) {
tout << mk_pp(s2[i], m) << " ";
}
tout << "\n";
);
pr = m.mk_hyper_resolve(2, premises.data(), fml3, positions, substs);
pc->insert(pr);
}
void resolve_rule(rule_manager& rm, rule const& r1, rule const& r2, unsigned idx,
expr_ref_vector const& s1, expr_ref_vector const& s2, rule& res) {
if (!r1.get_proof() || !r2.get_proof()) {
return;
}
SASSERT(r2.get_proof());
ast_manager& m = s1.get_manager();
expr_ref fml(m);
rm.to_formula(res, fml);
vector<expr_ref_vector> substs;
svector<std::pair<unsigned, unsigned> > positions;
substs.push_back(s1);
substs.push_back(s2);
scoped_proof _sc(m);
proof_ref pr(m);
proof_ref_vector premises(m);
premises.push_back(r1.get_proof());
premises.push_back(r2.get_proof());
positions.push_back(std::make_pair(idx+1, 0));
TRACE(dl,
tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
for (unsigned i = 0; i < s1.size(); ++i) {
tout << mk_pp(s1[i], m) << " ";
}
tout << "\n";
tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";
for (unsigned i = 0; i < s2.size(); ++i) {
tout << mk_pp(s2[i], m) << " ";
}
tout << "\n";
);
pr = m.mk_hyper_resolve(2, premises.data(), fml, positions, substs);
res.set_proof(m, pr);
}
class skip_model_converter : public model_converter {
public:
model_converter * translate(ast_translation & translator) override {
return alloc(skip_model_converter);
}
void operator()(model_ref&) override {}
void display(std::ostream & out) override { }
void get_units(obj_map<expr, bool>& units) override {}
};
model_converter* mk_skip_model_converter() { return alloc(skip_model_converter); }
class skip_proof_converter : public proof_converter {
proof_ref operator()(ast_manager & m, unsigned num_source, proof * const * source) override {
SASSERT(num_source == 1);
return proof_ref(source[0], m);
}
proof_converter * translate(ast_translation & translator) override {
return alloc(skip_proof_converter);
}
void display(std::ostream & out) override { out << "(skip-proof-converter)\n"; }
};
proof_converter* mk_skip_proof_converter() { return alloc(skip_proof_converter); }
void reverse_renaming(const var_ref_vector & src, var_ref_vector & tgt) {
ast_manager& m = src.m();
SASSERT(tgt.empty());
unsigned src_sz = src.size();
unsigned src_ofs = src_sz - 1;
unsigned max_var_idx = 0;
for(unsigned i=0; i<src_sz; ++i) {
if (!src[i]) {
continue;
}
unsigned var_idx = src[i]->get_idx();
if (var_idx > max_var_idx) {
max_var_idx = var_idx;
}
}
unsigned tgt_sz = max_var_idx+1;
unsigned tgt_ofs = tgt_sz - 1;
tgt.resize(tgt_sz, nullptr);
for(unsigned i = 0; i < src_sz; ++i) {
var* v = src[src_ofs-i];
if (!v) {
continue;
}
unsigned var_idx = v->get_idx();
tgt[tgt_ofs-var_idx] = m.mk_var(i, v->get_sort());
}
}
void print_renaming(const expr_ref_vector & cont, std::ostream & out) {
unsigned len = cont.size();
out << "(";
for(int i=len-1; i>=0; i--) {
out << (len-1-i) <<"->";
if(cont.get(i)==nullptr) {
out << "{none}";
}
else {
out << to_var(cont.get(i))->get_idx();
}
if(i!=0) { out << ","; }
}
out << ")\n";
}
void cycle_from_permutation(unsigned_vector & permutation, unsigned_vector & cycle) {
try_remove_cycle_from_permutation(permutation, cycle);
DEBUG_CODE(
unsigned_vector aux;
SASSERT(!try_remove_cycle_from_permutation(permutation, aux));
);
}
bool try_remove_cycle_from_permutation(unsigned_vector & permutation, unsigned_vector & cycle) {
SASSERT(cycle.empty());
DEBUG_CODE(
counter ctr;
ctr.count(permutation);
SASSERT(permutation.empty() || ctr.get_max_positive().value_or(0)==permutation.size()-1);
SASSERT(permutation.empty() || ctr.get_positive_count()==permutation.size());
);
unsigned sz = permutation.size();
for(unsigned i=0; i<sz; ++i) {
if(i==permutation[i]) {
continue;
}
unsigned prev_i = i;
for(;;) {
cycle.push_back(prev_i);
unsigned next_i = permutation[prev_i];
permutation[prev_i] = prev_i;
if(next_i==i) {
break;
}
prev_i = next_i;
}
return true;
}
return false;
}
void collect_sub_permutation(const unsigned_vector & permutation, const unsigned_vector & translation,
unsigned_vector & res, bool & identity) {
SASSERT(res.empty());
identity = true;
unsigned sz = permutation.size();
for(unsigned new_i=0; new_i<sz; ++new_i) {
unsigned idx = permutation[new_i];
bool is_selected = translation[idx]!=UINT_MAX;
if(is_selected) {
unsigned sel_idx = translation[idx];
if(!res.empty() && sel_idx!=res.back()+1) {
identity = false;
}
res.push_back(sel_idx);
}
}
}
void collect_and_transform(const unsigned_vector & src, const unsigned_vector & translation,
unsigned_vector & res) {
for (unsigned s : src) {
unsigned translated = translation[s];
if(translated!=UINT_MAX) {
res.push_back(translated);
}
}
}
void transform_set(const unsigned_vector & map, const idx_set & src, idx_set & result) {
for (unsigned s : src) {
result.insert(map[s]);
}
}
void add_sequence(unsigned start, unsigned count, unsigned_vector & v) {
unsigned after_last = start+count;
for(unsigned i=start; i<after_last; ++i) {
v.push_back(i);
}
}
void get_file_names(std::string directory, const std::string & extension, bool traverse_subdirs,
string_vector & res) {
if(directory[directory.size()-1]!='\\' && directory[directory.size()-1]!='/') {
#ifdef _WINDOWS
directory+='\\';
#else
directory+='/';
#endif
}
#ifdef _WINDOWS
WIN32_FIND_DATAA findFileData;
HANDLE hFind;
std::string filePattern = directory+"*."+extension;
hFind = FindFirstFileA(filePattern.c_str(), &findFileData);
if (hFind != INVALID_HANDLE_VALUE) {
do {
char const* name = findFileData.cFileName;
size_t len = strlen(name);
if (len > extension.size() && extension == std::string(name+len-extension.size())) {
res.push_back(directory+std::string(name));
}
} while(FindNextFileA(hFind, &findFileData));
FindClose(hFind);
}
if(traverse_subdirs) {
std::string subdirPattern = directory+"*.*";
hFind = FindFirstFileA(subdirPattern.c_str(), &findFileData);
if (hFind != INVALID_HANDLE_VALUE) {
do {
if(findFileData.cFileName[0]=='.') {
continue;
}
get_file_names(directory+findFileData.cFileName, extension, traverse_subdirs, res);
} while(FindNextFileA(hFind, &findFileData));
FindClose(hFind);
}
}
#else
NOT_IMPLEMENTED_YET();
#endif
}
bool file_exists(const std::string & name) {
struct stat st;
if(stat(name.c_str(),&st) == 0) {
return true;
}
return false;
}
bool is_directory(const std::string & name) {
if(!file_exists(name)) {
return false;
}
struct stat status;
stat(name.c_str(), &status);
return (status.st_mode&S_IFDIR)!=0;
}
std::string get_file_name_without_extension(const std::string & name) {
size_t slash_index = name.find_last_of("\\/");
size_t dot_index = name.rfind('.');
size_t ofs = (slash_index==std::string::npos) ? 0 : slash_index+1;
size_t count = (dot_index!=std::string::npos && dot_index>ofs) ?
(dot_index-ofs) : std::string::npos;
return name.substr(ofs, count);
}
bool string_to_uint64(const char * s, uint64_t & res) {
#if _WINDOWS
int converted = sscanf_s(s, "%" SCNu64, &res);
#else
int converted = sscanf(s, "%" SCNu64, &res);
#endif
if(converted==0) {
return false;
}
SASSERT(converted==1);
return true;
}
bool read_uint64(const char * & s, uint64_t & res) {
static const uint64_t max_but_one_digit = ULLONG_MAX/10;
static const uint64_t max_but_one_digit_safe = (ULLONG_MAX-9)/10;
if(*s<'0' || *s>'9') {
return false;
}
res=*s-'0';
s++;
while(*s>='0' && *s<='9') {
if(res>max_but_one_digit_safe) {
if(res>max_but_one_digit) {
return false; }
res*=10;
char digit = *s-'0';
if(static_cast<int>(ULLONG_MAX-res)-digit<0) {
return false; }
res+=digit;
}
else {
res*=10;
res+=*s-'0';
s++;
}
}
return true;
}
std::string to_string(uint64_t num) {
std::stringstream stm;
stm<<num;
return stm.str();
}
}