mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 20:31:21 +00:00
Code Activity

build/labels

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-30 22:29:00 -07:00
parent 53ab931626
commit 1e8009bbfc
2 changed files with 22 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/euf_proof.cpp
View file

@ -179,6 +179,8 @@ namespace euf {
void solver::drat_eq_def(literal lit, expr* eq) { void solver::drat_eq_def(literal lit, expr* eq) {
expr *a = nullptr, *b = nullptr; expr *a = nullptr, *b = nullptr;
VERIFY(m.is_eq(eq, a, b)); VERIFY(m.is_eq(eq, a, b));
drat_log_expr(a);
drat_log_expr(b);
get_drat().def_begin('e', eq->get_id(), std::string("=")); get_drat().def_begin('e', eq->get_id(), std::string("="));
get_drat().def_add_arg(a->get_id()); get_drat().def_add_arg(a->get_id());
get_drat().def_add_arg(b->get_id()); get_drat().def_add_arg(b->get_id());

29
src/shell/drat_frontend.cpp
View file

@ -173,12 +173,14 @@ public:
void parse_quantifier(sexpr_ref const& sexpr, cmd_context& ctx, quantifier_kind& k, sort_ref_vector& domain, svector<symbol>& names) { void parse_quantifier(sexpr_ref const& sexpr, cmd_context& ctx, quantifier_kind& k, sort_ref_vector& domain, svector<symbol>& names) {
k = quantifier_kind::forall_k; k = quantifier_kind::forall_k;
symbol q;
unsigned sz;
if (sexpr->get_kind() != sexpr::kind_t::COMPOSITE) if (sexpr->get_kind() != sexpr::kind_t::COMPOSITE)
goto bail; goto bail;
unsigned sz = sexpr->get_num_children(); sz = sexpr->get_num_children();
if (sz == 0) if (sz == 0)
goto bail; goto bail;
symbol q = sexpr->get_child(0)->get_symbol(); q = sexpr->get_child(0)->get_symbol();
if (q == "forall") if (q == "forall")
k = quantifier_kind::forall_k; k = quantifier_kind::forall_k;
else if (q == "exists") else if (q == "exists")
@ -188,7 +190,19 @@ public:
else else
goto bail; goto bail;
for (unsigned i = 1; i < sz; ++i) { for (unsigned i = 1; i < sz; ++i) {
std::cout << "parse bound\n"; auto* e = sexpr->get_child(i);
if (e->get_kind() != sexpr::kind_t::COMPOSITE)
goto bail;
if (2 != e->get_num_children())
goto bail;
symbol name = e->get_child(0)->get_symbol();
std::ostringstream ostrm;
e->get_child(1)->display(ostrm);
std::istringstream istrm(ostrm.str());
params_ref p;
auto srt = parse_smt2_sort(ctx, istrm, false, p, "quantifier");
names.push_back(name);
domain.push_back(srt);
} }
return; return;
bail: bail:
@ -374,6 +388,7 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
break; break;
} }
case dimacs::drat_record::tag_t::is_quantifier: { case dimacs::drat_record::tag_t::is_quantifier: {
VERIFY(r.m_args.size() == 1);
quantifier_ref q(m); quantifier_ref q(m);
std::istringstream strm(r.m_name); std::istringstream strm(r.m_name);
auto sexpr = parse_sexpr(ctx, strm, p, drat_file); auto sexpr = parse_sexpr(ctx, strm, p, drat_file);
@ -381,8 +396,7 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
svector<symbol> names; svector<symbol> names;
quantifier_kind k; quantifier_kind k;
checker.parse_quantifier(sexpr, ctx, k, domain, names); checker.parse_quantifier(sexpr, ctx, k, domain, names);
sexpr->display(std::cout << "QQ "); q = m.mk_quantifier(k, domain.size(), domain.data(), names.data(), exprs.get(r.m_args[0]));
std::cout << "\n";
exprs.reserve(r.m_node_id + 1); exprs.reserve(r.m_node_id + 1);
exprs.set(r.m_node_id, m.mk_true()); exprs.set(r.m_node_id, m.mk_true());
break; break;
@ -399,7 +413,6 @@ static void verify_smt(char const* drat_file, char const* smt_file) {
statistics st; statistics st;
drat_checker.collect_statistics(st); drat_checker.collect_statistics(st);
std::cout << st << "\n"; std::cout << st << "\n";
} }
@ -410,6 +423,4 @@ unsigned read_drat(char const* drat_file, char const* problem_file) {
} }
verify_smt(drat_file, problem_file); verify_smt(drat_file, problem_file);
return 0; return 0;
} }