diff --git a/examples/tptp/tptp5.cpp b/examples/tptp/tptp5.cpp
index 8f28111ac..b2736df4c 100644
--- a/examples/tptp/tptp5.cpp
+++ b/examples/tptp/tptp5.cpp
@@ -1227,11 +1227,11 @@ public:
void display_axiom(std::ostream& out, z3::expr e) {
out << "tff(formula" << (++m_formula_id) << ", axiom,\n ";
- display(out, e);
+ display(out, e, true);
out << ").\n";
}
- void display(std::ostream& out, z3::expr e) {
+ void display(std::ostream& out, z3::expr e, bool in_paren) {
std::string s;
if (e.is_numeral(s)) {
out << s;
@@ -1249,32 +1249,33 @@ public:
out << "$false";
break;
case Z3_OP_AND:
- display_infix(out, "&", e);
+ display_infix(out, "&", e, in_paren);
break;
case Z3_OP_OR:
- display_infix(out, "|", e);
+ display_infix(out, "|", e, in_paren);
break;
case Z3_OP_IMPLIES:
- display_infix(out, "=>", e);
+ display_infix(out, "=>", e, in_paren);
break;
case Z3_OP_NOT:
- out << "(~";
- display(out, e.arg(0));
- out << ")";
+ if (!in_paren) out << "(";
+ out << "~";
+ display(out, e.arg(0), false);
+ if (!in_paren) out << ")";
break;
case Z3_OP_EQ:
if (e.arg(0).is_bool()) {
- display_infix(out, "<=>", e);
+ display_infix(out, "<=>", e, in_paren);
}
else {
- display_infix(out, "=", e);
+ display_infix(out, "=", e, in_paren);
}
break;
case Z3_OP_IFF:
- display_infix(out, "<=>", e);
+ display_infix(out, "<=>", e, in_paren);
break;
case Z3_OP_XOR:
- display_infix(out, "<~>", e);
+ display_infix(out, "<~>", e, in_paren);
break;
case Z3_OP_MUL:
display_binary(out, "$product", e);
@@ -1351,7 +1352,7 @@ public:
}
}
out << "] : ";
- display(out, e.body());
+ display(out, e.body(), false);
for (unsigned i = 0; i < nb; ++i) {
names.pop_back();
}
@@ -1366,7 +1367,7 @@ public:
out << lower_case_fun(e.decl().name()) << "(";
unsigned n = e.num_args();
for(unsigned i = 0; i < n; ++i) {
- display(out, e.arg(i));
+ display(out, e.arg(i), n == 1);
if (i + 1 < n) {
out << ", ";
}
@@ -1389,23 +1390,23 @@ public:
}
}
- void display_infix(std::ostream& out, char const* conn, z3::expr& e) {
- out << "(";
+ void display_infix(std::ostream& out, char const* conn, z3::expr& e, bool in_paren) {
+ if (!in_paren) out << "(";
unsigned sz = e.num_args();
for (unsigned i = 0; i < sz; ++i) {
- display(out, e.arg(i));
+ display(out, e.arg(i), false);
if (i + 1 < sz) {
out << " " << conn << " ";
}
}
- out << ")";
+ if (!in_paren) out << ")";
}
void display_prefix(std::ostream& out, char const* conn, z3::expr& e) {
out << conn << "(";
unsigned sz = e.num_args();
for (unsigned i = 0; i < sz; ++i) {
- display(out, e.arg(i));
+ display(out, e.arg(i), sz == 1);
if (i + 1 < sz) {
out << ", ";
}
@@ -1418,7 +1419,7 @@ public:
unsigned sz = e.num_args();
unsigned np = 1;
for (unsigned i = 0; i < sz; ++i) {
- display(out, e.arg(i));
+ display(out, e.arg(i), false);
if (i + 1 < sz) {
out << ", ";
}
@@ -1562,7 +1563,7 @@ public:
formula_file = "unknown";
}
out << "tff(" << m_node_number << ",axiom,(";
- display(out, get_proof_formula(p));
+ display(out, get_proof_formula(p), true);
out << "), file('" << formula_file << "','";
out << formula_name << "')).\n";
break;
@@ -1625,12 +1626,12 @@ public:
break;
case Z3_OP_PR_HYPOTHESIS:
out << "tff(" << m_node_number << ",assumption,(";
- display(out, get_proof_formula(p));
+ display(out, get_proof_formula(p), true);
out << "), introduced(assumption)).\n";
break;
case Z3_OP_PR_LEMMA: {
out << "tff(" << m_node_number << ",plain,(";
- display(out, get_proof_formula(p));
+ display(out, get_proof_formula(p), true);
out << "), inference(lemma,lemma(discharge,";
unsigned parent_id = Z3_get_ast_id(ctx, p.arg(0));
std::set<unsigned> const& hyps = m_proof_hypotheses.find(parent_id)->second;
@@ -1747,7 +1748,7 @@ public:
unsigned id = Z3_get_ast_id(ctx, p);
std::set<unsigned> const& hyps = m_proof_hypotheses.find(id)->second;
out << "tff(" << m_node_number << ",plain,\n (";
- display(out, get_proof_formula(p));
+ display(out, get_proof_formula(p), true);
out << "),\n inference(" << name << ",[status(" << status << ")";
if (!hyps.empty()) {
out << ", assumptions(";
@@ -1776,7 +1777,7 @@ public:
unsigned display_hyp_inference(std::ostream& out, char const* name, char const* status, z3::expr conclusion, unsigned hyp1, unsigned hyp2 = 0) {
++m_node_number;
out << "tff(" << m_node_number << ",plain,(\n ";
- display(out, conclusion);
+ display(out, conclusion, true);
out << "),\n inference(" << name << ",[status(" << status << ")],";
out << "[" << hyp1;
if (hyp2) {
@@ -2467,7 +2468,6 @@ static void prove_tptp() {
int main(int argc, char** argv) {
- //std::ostream* out = &std::cout;
g_start_time = static_cast<double>(clock());
signal(SIGINT, on_ctrl_c);
@@ -2484,10 +2484,8 @@ int main(int argc, char** argv) {
prove_tptp();
}
catch (z3::exception& ex) {
- std::cerr << "Proof display could not be completed: " << ex.msg() << "\n";
+ std::cerr << "Exception during proof: " << ex.msg() << "\n";
}
-
-
}
return 0;
}
diff --git a/src/math/automata/symbolic_automata.h b/src/math/automata/symbolic_automata.h
index cc3a0f5a8..c358bcac8 100644
--- a/src/math/automata/symbolic_automata.h
+++ b/src/math/automata/symbolic_automata.h
@@ -96,8 +96,8 @@ class symbolic_automata {
public:
symbolic_automata(M& m, ba_t& ba): m(m), m_ba(ba) {}
- automaton_t* mk_determinstic(automaton_t& a);
- automaton_t* mk_complement(automaton_t& a);
+ //automaton_t* mk_determinstic(automaton_t& a);
+ //automaton_t* mk_complement(automaton_t& a);
automaton_t* remove_epsilons(automaton_t& a);
automaton_t* mk_total(automaton_t& a);
automaton_t* mk_minimize(automaton_t& a);
diff --git a/src/muz/pdr/pdr_context.cpp b/src/muz/pdr/pdr_context.cpp
index 6dc93048a..b6a889756 100644
--- a/src/muz/pdr/pdr_context.cpp
+++ b/src/muz/pdr/pdr_context.cpp
@@ -895,7 +895,7 @@ namespace pdr {
SASSERT(m_prev);
SASSERT(children().empty());
if (this == m_next) {
- SASSERT(root == this);
+ // SASSERT(root == this);
root = 0;
}
else {
@@ -1818,6 +1818,10 @@ namespace pdr {
m_fparams.m_arith_mode = AS_UTVPI;
m_fparams.m_arith_expand_eqs = true;
}
+ else {
+ m_fparams.m_arith_mode = AS_ARITH;
+ m_fparams.m_arith_expand_eqs = false;
+ }
}
}
if (m_params.pdr_use_convex_closure_generalizer()) {