Skip to content

Commit 7b77fec

Browse files
giomascegiomasce
committed
First attempt, not working, at full proof generation with SAT refutation.
1 parent 93158dc commit 7b77fec

File tree

4 files changed

+110
-17
lines changed

4 files changed

+110
-17
lines changed

‎provers/sat.h

+1
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ Literal from_number_literal(int32_t lit);
2020
Literal invert_literal(const Literal &lit);
2121
void print_clause(std::ostream &stream, const Clause &clause);
2222

23+
// When popping many things from the stack, you actually have to do in the opposite order
2324
struct CNFCallback {
2425
// Push NOT context -> clause on the stack
2526
virtual void prove_clause(size_t idx, const Clause &context) = 0;

‎provers/wffblock.cpp

+5-5
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ static const RegisteredProver or_eliml_rp = LibraryToolbox::register_prover({"|-
7272
static const RegisteredProver or_elimr_rp = LibraryToolbox::register_prover({"|- ( ph -> -. ( ps \\/ ch ) )"}, "|- ( ph -> -. ch )");
7373
static const RegisteredProver or_elimln_rp = LibraryToolbox::register_prover({"|- ( ph -> -. ( -. ps \\/ ch ) )"}, "|- ( ph -> ps )");
7474
static const RegisteredProver or_elimrn_rp = LibraryToolbox::register_prover({"|- ( ph -> -. ( ps \\/ -. ch ) )"}, "|- ( ph -> ch )");
75-
Prover<CheckpointedProofEngine> not_or_elim_prover(const std::vector<pwff> &orands, size_t thesis_idx, bool thesis_sign, Prover<CheckpointedProofEngine> not_or_prover, pwff glob_ctx, const LibraryToolbox &tb)
75+
Prover<CheckpointedProofEngine> not_or_elim_prover(const std::vector<pwff> &orands, size_t thesis_idx, bool thesis_sign, Prover<CheckpointedProofEngine> not_or_prover, pwff loc_ctx, const LibraryToolbox &tb)
7676
{
7777
assert(thesis_idx < orands.size());
7878
pwff structure = orands[0];
@@ -87,22 +87,22 @@ Prover<CheckpointedProofEngine> not_or_elim_prover(const std::vector<pwff> &oran
8787
auto or_right = or_struct->get_b();
8888
if (eliminating == thesis_idx) {
8989
if (thesis_sign) {
90-
ret = tb.build_registered_prover(or_elimr_rp, {{"ph", glob_ctx->get_type_prover(tb)}, {"ps", or_left->get_type_prover(tb)}, {"ch", or_right->get_type_prover(tb)}}, {ret});
90+
ret = tb.build_registered_prover(or_elimr_rp, {{"ph", loc_ctx->get_type_prover(tb)}, {"ps", or_left->get_type_prover(tb)}, {"ch", or_right->get_type_prover(tb)}}, {ret});
9191
} else {
9292
auto or_right_not = dynamic_pointer_cast< const Not >(or_right);
9393
assert(or_right_not);
9494
auto or_right_not_neg = or_right_not->get_a();
95-
ret = tb.build_registered_prover(or_elimrn_rp, {{"ph", glob_ctx->get_type_prover(tb)}, {"ps", or_left->get_type_prover(tb)}, {"ch", or_right_not_neg->get_type_prover(tb)}}, {ret});
95+
ret = tb.build_registered_prover(or_elimrn_rp, {{"ph", loc_ctx->get_type_prover(tb)}, {"ps", or_left->get_type_prover(tb)}, {"ch", or_right_not_neg->get_type_prover(tb)}}, {ret});
9696
}
9797
break;
9898
} else {
9999
if (eliminating == 1 && thesis_sign) {
100100
auto or_left_not = dynamic_pointer_cast< const Not >(or_left);
101101
assert(or_left_not);
102102
auto or_left_not_neg = or_left_not->get_a();
103-
ret = tb.build_registered_prover(or_elimln_rp, {{"ph", glob_ctx->get_type_prover(tb)}, {"ps", or_left_not_neg->get_type_prover(tb)}, {"ch", or_right->get_type_prover(tb)}}, {ret});
103+
ret = tb.build_registered_prover(or_elimln_rp, {{"ph", loc_ctx->get_type_prover(tb)}, {"ps", or_left_not_neg->get_type_prover(tb)}, {"ch", or_right->get_type_prover(tb)}}, {ret});
104104
} else {
105-
ret = tb.build_registered_prover(or_eliml_rp, {{"ph", glob_ctx->get_type_prover(tb)}, {"ps", or_left->get_type_prover(tb)}, {"ch", or_right->get_type_prover(tb)}}, {ret});
105+
ret = tb.build_registered_prover(or_eliml_rp, {{"ph", loc_ctx->get_type_prover(tb)}, {"ps", or_left->get_type_prover(tb)}, {"ch", or_right->get_type_prover(tb)}}, {ret});
106106
structure = or_left;
107107
}
108108
}

‎provers/wffblock.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,6 @@
77

88
Prover<CheckpointedProofEngine> imp_mp_prover(std::shared_ptr< const Imp > imp, Prover<CheckpointedProofEngine> ant_prover, Prover<CheckpointedProofEngine> imp_prover, const LibraryToolbox &tb);
99
Prover<CheckpointedProofEngine> unit_res_prover(const std::vector< pwff > &orands, const std::vector<bool> &orand_sign, size_t thesis_idx, Prover<CheckpointedProofEngine> or_prover, const std::vector< Prover<CheckpointedProofEngine> > &orand_prover, pwff glob_ctx, pwff loc_ctx, const LibraryToolbox &tb);
10-
Prover<CheckpointedProofEngine> not_or_elim_prover(const std::vector< pwff > &orands, size_t thesis_idx, bool thesis_sign, Prover<CheckpointedProofEngine> not_or_prover, pwff glob_ctx, const LibraryToolbox &tb);
10+
Prover<CheckpointedProofEngine> not_or_elim_prover(const std::vector< pwff > &orands, size_t thesis_idx, bool thesis_sign, Prover<CheckpointedProofEngine> not_or_prover, pwff loc_ctx, const LibraryToolbox &tb);
1111
Prover<CheckpointedProofEngine> absurdum_prover(pwff concl, Prover<CheckpointedProofEngine> pos_prover, Prover<CheckpointedProofEngine> neg_prover, pwff glob_ctx, pwff loc_ctx, const LibraryToolbox &tb);
1212
Prover<CheckpointedProofEngine> imp_intr_prover(pwff concl, Prover<CheckpointedProofEngine> concl_prover, pwff glob_ctx, pwff loc_ctx, const LibraryToolbox &tb);

‎provers/wffsat.cpp

+103-11
Original file line numberDiff line numberDiff line change
@@ -6,41 +6,133 @@
66

77
using namespace std;
88

9+
static const RegisteredProver idi_rp = LibraryToolbox::register_prover({}, "|- ( ph -> ph )");
10+
static const RegisteredProver concl_rp = LibraryToolbox::register_prover({"|- ( ps -> ch )"}, "|- ( ph -> ( ps -> ch ) )");
911
struct CNFCallbackImpl : public CNFCallback {
10-
void prove_clause(size_t idx, const Clause &context) {}
11-
void prove_not_or_elim(size_t idx, const Clause &context) {}
12-
void prove_imp_intr(const Clause &clause, const Clause &context) {}
13-
void prove_unit_res(const Clause &clause, size_t unsolved_idx, const Clause &context) {}
14-
void prove_absurdum(const Literal &lit, const Clause &context) {}
12+
void prove_clause(size_t idx, const Clause &context) {
13+
pwff concl = this->clause_to_pwff(this->orig_clauses.at(idx));
14+
pwff loc_ctx = Not::create(this->clause_to_pwff(context));
15+
this->prover_stack.push_back(imp_intr_prover(concl, this->orig_provers.at(idx), this->glob_ctx, loc_ctx, this->tb));
16+
}
17+
18+
void prove_not_or_elim(size_t idx, const Clause &context) {
19+
pwff loc_ctx = Not::create(this->clause_to_pwff(context));
20+
pwff concl = this->atoms[context[idx].second];
21+
if (!context[idx].first) {
22+
concl = Not::create(concl);
23+
}
24+
vector< pwff > orands;
25+
for (const auto lit : context) {
26+
pwff new_lit = this->atoms[lit.second];
27+
if (!lit.first) {
28+
new_lit = Not::create(new_lit);
29+
}
30+
orands.push_back(new_lit);
31+
}
32+
auto p1 = this->tb.build_registered_prover(idi_rp, {{"ph", loc_ctx->get_type_prover(this->tb)}}, {});
33+
auto p2 = not_or_elim_prover(orands, idx, context[idx].first, p1, loc_ctx, this->tb);
34+
auto p3 = this->tb.build_registered_prover(concl_rp, {{"ph", this->glob_ctx->get_type_prover(this->tb)}, {"ps", loc_ctx->get_type_prover(this->tb)}, {"ch", concl->get_type_prover(this->tb)}}, {p2});
35+
this->prover_stack.push_back(p3);
36+
}
37+
38+
void prove_imp_intr(const Clause &clause, const Clause &context) {
39+
pwff loc_ctx = Not::create(this->clause_to_pwff(context));
40+
pwff concl = this->clause_to_pwff(clause);
41+
auto p1 = this->prover_stack.back();
42+
this->prover_stack.pop_back();
43+
auto p2 = imp_intr_prover(concl, p1, this->glob_ctx, loc_ctx, this->tb);
44+
this->prover_stack.push_back(p2);
45+
}
46+
47+
void prove_unit_res(const Clause &clause, size_t unsolved_idx, const Clause &context) {
48+
pwff loc_ctx = Not::create(this->clause_to_pwff(context));
49+
vector< pwff > orands;
50+
for (const auto lit : clause) {
51+
pwff new_lit = this->atoms[lit.second];
52+
if (!lit.first) {
53+
new_lit = Not::create(new_lit);
54+
}
55+
orands.push_back(new_lit);
56+
}
57+
vector< bool > orand_sign;
58+
for (size_t i = 0; i < clause.size(); i++) {
59+
if (i != unsolved_idx) {
60+
orand_sign.push_back(clause[i].first);
61+
}
62+
}
63+
auto p1 = this->prover_stack[this->prover_stack.size()-clause.size()];
64+
vector< Prover< CheckpointedProofEngine > > provers(this->prover_stack.end()-clause.size()+1, this->prover_stack.end());
65+
this->prover_stack.resize(this->prover_stack.size()-clause.size());
66+
auto p2 = unit_res_prover(orands, orand_sign, unsolved_idx, p1, provers, this->glob_ctx, loc_ctx, this->tb);
67+
this->prover_stack.push_back(p2);
68+
}
1569

70+
void prove_absurdum(const Literal &lit, const Clause &context) {
71+
pwff loc_ctx = Not::create(this->clause_to_pwff(context));
72+
pwff concl = this->atoms[lit.second];
73+
auto neg_prover = this->prover_stack.back();
74+
this->prover_stack.pop_back();
75+
auto pos_prover = this->prover_stack.back();
76+
this->prover_stack.pop_back();
77+
auto p = absurdum_prover(concl, pos_prover, neg_prover, this->glob_ctx, loc_ctx, this->tb);
78+
this->prover_stack.push_back(p);
79+
}
80+
81+
const LibraryToolbox &tb;
1682
std::vector< Clause > orig_clauses;
1783
vector< Prover< CheckpointedProofEngine > > orig_provers;
84+
vector< Prover< CheckpointedProofEngine > > prover_stack;
1885
pwff glob_ctx;
86+
vector< pwff > atoms;
87+
88+
CNFCallbackImpl(const LibraryToolbox &tb) : tb(tb) {}
89+
90+
pwff clause_to_pwff(const Clause &c) {
91+
if (c.empty()) {
92+
return False::create();
93+
}
94+
pwff ret = this->atoms[c[0].second];
95+
if (!c[0].first) {
96+
ret = Not::create(ret);
97+
}
98+
for (size_t i = 1; i < c.size(); i++) {
99+
pwff new_lit = this->atoms[c[i].second];
100+
if (!c[i].first) {
101+
new_lit = Not::create(new_lit);
102+
}
103+
ret = Or::create(ret, new_lit);
104+
}
105+
return ret;
106+
}
19107
};
20108

21109
std::pair<bool, Prover<CheckpointedProofEngine> > get_sat_prover(pwff wff, const LibraryToolbox &tb)
22110
{
23111
auto glob_ctx = Not::create(wff);
24112
auto tseitin = glob_ctx->get_tseitin_cnf_problem(tb);
25-
auto cnf = get<0>(tseitin);
26-
//auto ts_map = get<1>(tseitin);
27-
auto provers = get<2>(tseitin);
113+
auto &cnf = get<0>(tseitin);
114+
auto &ts_map = get<1>(tseitin);
115+
auto &provers = get<2>(tseitin);
28116
/*cnf.print_dimacs(cout);
29117
for (const auto &x : ts_map) {
30118
cout << (x.second + 1) << " : " << x.first->to_string() << endl;
31119
}*/
32-
CNFCallbackImpl cnf_cb;
120+
CNFCallbackImpl cnf_cb(tb);
33121
cnf_cb.orig_clauses = cnf.clauses;
34122
cnf_cb.orig_provers = provers;
35123
cnf_cb.glob_ctx = glob_ctx;
124+
for (const auto &x : ts_map) {
125+
cnf_cb.atoms[x.second] = x.first;
126+
}
36127
cnf.callback = &cnf_cb;
37128
const auto res = cnf.solve();
38129
if (res.first) {
39130
return make_pair(false, null_prover);
40131
} else {
41132
cout << "The formula is UNSATisfiable" << endl;
42133
cout << "Unwinding the proof..." << endl;
43-
//res.second();
44-
return make_pair(true, null_prover);
134+
res.second();
135+
assert(cnf_cb.prover_stack.size() == 1);
136+
return make_pair(true, cnf_cb.prover_stack[0]);
45137
}
46138
}

0 commit comments

Comments
 (0)