mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix compilation errors after merge
This commit is contained in:
parent
d79837eed0
commit
b5fe473c3a
|
@ -1767,9 +1767,6 @@ namespace smt2 {
|
|||
case scanner::BV_TOKEN:
|
||||
parse_bv_numeral();
|
||||
break;
|
||||
case scanner::STRING_TOKEN:
|
||||
parse_string();
|
||||
break;
|
||||
case scanner::LEFT_PAREN:
|
||||
push_expr_frame(m_num_expr_frames == 0 ? 0 : static_cast<expr_frame*>(m_stack.top()));
|
||||
break;
|
||||
|
|
|
@ -4962,4 +4962,8 @@ model_value_proc * theory_str::mk_value(enode * n, model_generator & mg) {
|
|||
|
||||
void theory_str::finalize_model(model_generator & mg) {}
|
||||
|
||||
void theory_str::display(std::ostream & out) const {
|
||||
out << "TODO: theory_str display" << std::endl;
|
||||
}
|
||||
|
||||
}; /* namespace smt */
|
||||
|
|
|
@ -220,6 +220,7 @@ namespace smt {
|
|||
virtual ~theory_str();
|
||||
|
||||
virtual char const * get_name() const { return "strings"; }
|
||||
virtual void display(std::ostream & out) const;
|
||||
protected:
|
||||
virtual bool internalize_atom(app * atom, bool gate_ctx);
|
||||
virtual bool internalize_term(app * term);
|
||||
|
|
Loading…
Reference in a new issue