3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00

remove deprecated theory aware drat functionality

it is handled by the on-clause callback that is owned by the smt solver.
This commit is contained in:
Nikolaj Bjorner 2022-10-24 08:32:03 -07:00
parent cb3c86736c
commit 280887cc5a
4 changed files with 1 additions and 54 deletions

View file

@ -57,17 +57,8 @@ namespace sat {
}
std::ostream& drat::pp(std::ostream& out, status st) const {
if (st.is_redundant())
out << "l";
else if (st.is_deleted())
if (st.is_deleted())
out << "d";
else if (st.is_asserted())
out << "a";
else if (st.is_input())
out << "i";
if (!st.is_sat())
out << " " << m_theory[st.get_th()];
return out;
}
@ -102,11 +93,6 @@ namespace sat {
}
}
if (!st.is_sat()) {
for (char ch : m_theory[st.get_th()])
buffer[len++] = ch;
buffer[len++] = ' ';
}
for (unsigned i = 0; i < n; ++i) {
literal lit = c[i];
unsigned v = lit.var();

View file

@ -17,39 +17,6 @@ Notes:
For DIMACS input it produces DRAT proofs.
For SMT extensions are as follows:
Input assertion:
i <literal>* 0
Assertion (true modulo a theory):
a [<theory-id>] <literal>* 0
The if no theory id is given, the assertion is a tautology
modulo Tseitin converison. Theory ids track whether the
tautology is modulo a theory.
Assertions are irredundant.
Bridge from ast-node to boolean variable:
b <bool-var-id> <ast-node-id> 0
Definition of an expression (ast-node):
e <ast-node-id> <name> <ast-node-id>* 0
Redundant clause (theory lemma if theory id is given)
[r [<theory-id>]] <literal>* 0
Declaration of an auxiliary function:
f <smtlib2-function-declaration> 0
Garbage collection of a Boolean variable:
g <bool-var-id> 0
Available theories are:
- euf The theory lemma should be a consequence of congruence closure.
- ba TBD (need to also log cardinality and pb constraints)
Life times of theory lemmas is TBD. When they are used for conflict resolution
they are only used for the next lemma.
--*/
#pragma once
@ -89,7 +56,6 @@ namespace sat {
svector<std::pair<literal, clause*>> m_units;
vector<watch> m_watches;
svector<lbool> m_assignment;
vector<std::string> m_theory;
bool m_inconsistent = false;
bool m_check_unsat = false;
bool m_check_sat = false;
@ -135,7 +101,6 @@ namespace sat {
void updt_config();
void add_theory(int id, symbol const& s) { m_theory.setx(id, s.str(), std::string()); }
void add();
void add(literal l, bool learned);
void add(literal l1, literal l2, status st);

View file

@ -37,8 +37,6 @@ namespace euf {
!s().get_config().m_smt_proof.is_non_empty_string())
return;
get_drat().add_theory(get_id(), symbol("euf"));
get_drat().add_theory(m.get_basic_family_id(), symbol("bool"));
if (s().get_config().m_smt_proof.is_non_empty_string())
m_proof_out = alloc(std::ofstream, s().get_config().m_smt_proof.str(), std::ios_base::out);
get_drat().set_clause_eh(*this);

View file

@ -149,8 +149,6 @@ namespace euf {
void solver::add_solver(th_solver* th) {
family_id fid = th->get_id();
if (use_drat())
s().get_drat().add_theory(fid, th->name());
th->set_solver(m_solver);
th->push_scopes(s().num_scopes() + s().num_user_scopes());
m_solvers.push_back(th);