From 954400cfa27cedf508b18da146e17973e5dbbc6f Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Fri, 13 Nov 2015 16:35:08 +0000
Subject: [PATCH] whitespace
---
src/api/api_solver_old.cpp | 48 +++++++++++++++++++-------------------
1 file changed, 24 insertions(+), 24 deletions(-)
diff --git a/src/api/api_solver_old.cpp b/src/api/api_solver_old.cpp
index 7e994a0e2..7fa469718 100644
--- a/src/api/api_solver_old.cpp
+++ b/src/api/api_solver_old.cpp
@@ -34,7 +34,7 @@ extern "C" {
mk_c(c)->push();
Z3_CATCH;
}
-
+
void Z3_API Z3_pop(Z3_context c, unsigned num_scopes) {
Z3_TRY;
LOG_Z3_pop(c, num_scopes);
@@ -62,7 +62,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_assert_cnstr(c, a);
RESET_ERROR_CODE();
- CHECK_FORMULA(a,);
+ CHECK_FORMULA(a,);
mk_c(c)->assert_cnstr(to_expr(a));
Z3_CATCH;
}
@@ -81,11 +81,11 @@ extern "C" {
result = mk_c(c)->check(_m);
if (m) {
if (_m) {
- Z3_model_ref * m_ref = alloc(Z3_model_ref);
+ Z3_model_ref * m_ref = alloc(Z3_model_ref);
m_ref->m_model = _m;
// Must bump reference counter for backward compatibility reasons.
// Don't need to invoke save_object, since the counter was bumped
- m_ref->inc_ref();
+ m_ref->inc_ref();
*m = of_model(m_ref);
}
else {
@@ -100,21 +100,21 @@ extern "C" {
RETURN_Z3_check_and_get_model static_cast<Z3_lbool>(result);
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
-
+
Z3_lbool Z3_API Z3_check(Z3_context c) {
Z3_TRY;
- // This is just syntax sugar...
- RESET_ERROR_CODE();
+ // This is just syntax sugar...
+ RESET_ERROR_CODE();
CHECK_SEARCHING(c);
Z3_lbool r = Z3_check_and_get_model(c, 0);
return r;
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
-
- Z3_lbool Z3_API Z3_check_assumptions(Z3_context c,
- unsigned num_assumptions, Z3_ast const assumptions[],
- Z3_model * m, Z3_ast* proof,
+
+ Z3_lbool Z3_API Z3_check_assumptions(Z3_context c,
+ unsigned num_assumptions, Z3_ast const assumptions[],
+ Z3_model * m, Z3_ast* proof,
unsigned* core_size, Z3_ast core[]) {
Z3_TRY;
LOG_Z3_check_assumptions(c, num_assumptions, assumptions, m, proof, core_size, core);
@@ -130,11 +130,11 @@ extern "C" {
model_ref _m;
mk_c(c)->get_smt_kernel().get_model(_m);
if (_m) {
- Z3_model_ref * m_ref = alloc(Z3_model_ref);
+ Z3_model_ref * m_ref = alloc(Z3_model_ref);
m_ref->m_model = _m;
// Must bump reference counter for backward compatibility reasons.
// Don't need to invoke save_object, since the counter was bumped
- m_ref->inc_ref();
+ m_ref->inc_ref();
*m = of_model(m_ref);
}
else {
@@ -159,7 +159,7 @@ extern "C" {
else if (proof) {
*proof = 0; // breaks abstraction.
}
- RETURN_Z3_check_assumptions static_cast<Z3_lbool>(result);
+ RETURN_Z3_check_assumptions static_cast<Z3_lbool>(result);
Z3_CATCH_RETURN(Z3_L_UNDEF);
}
@@ -185,7 +185,7 @@ extern "C" {
symbol const& get_label() const { return m_label; }
expr* get_literal() { return m_literal.get(); }
};
-
+
typedef vector<labeled_literal> labels;
Z3_literals Z3_API Z3_get_relevant_labels(Z3_context c) {
@@ -196,7 +196,7 @@ extern "C" {
ast_manager& m = mk_c(c)->m();
expr_ref_vector lits(m);
mk_c(c)->get_smt_kernel().get_relevant_labels(0, labl_syms);
- mk_c(c)->get_smt_kernel().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits);
+ mk_c(c)->get_smt_kernel().get_relevant_labeled_literals(mk_c(c)->fparams().m_at_labels_cex, lits);
labels* lbls = alloc(labels);
SASSERT(labl_syms.size() == lits.size());
for (unsigned i = 0; i < lits.size(); ++i) {
@@ -212,12 +212,12 @@ extern "C" {
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
expr_ref_vector lits(m);
- mk_c(c)->get_smt_kernel().get_relevant_literals(lits);
+ mk_c(c)->get_smt_kernel().get_relevant_literals(lits);
labels* lbls = alloc(labels);
for (unsigned i = 0; i < lits.size(); ++i) {
lbls->push_back(labeled_literal(m,lits[i].get()));
}
- RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));
+ RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));
Z3_CATCH_RETURN(0);
}
@@ -227,12 +227,12 @@ extern "C" {
RESET_ERROR_CODE();
ast_manager& m = mk_c(c)->m();
expr_ref_vector lits(m);
- mk_c(c)->get_smt_kernel().get_guessed_literals(lits);
+ mk_c(c)->get_smt_kernel().get_guessed_literals(lits);
labels* lbls = alloc(labels);
for (unsigned i = 0; i < lits.size(); ++i) {
lbls->push_back(labeled_literal(m,lits[i].get()));
}
- RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));
+ RETURN_Z3(reinterpret_cast<Z3_literals>(lbls));
Z3_CATCH_RETURN(0);
}
@@ -248,7 +248,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_num_literals(c, lbls);
RESET_ERROR_CODE();
- return reinterpret_cast<labels*>(lbls)->size();
+ return reinterpret_cast<labels*>(lbls)->size();
Z3_CATCH_RETURN(0);
}
@@ -256,7 +256,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_get_label_symbol(c, lbls, idx);
RESET_ERROR_CODE();
- return of_symbol((*reinterpret_cast<labels*>(lbls))[idx].get_label());
+ return of_symbol((*reinterpret_cast<labels*>(lbls))[idx].get_label());
Z3_CATCH_RETURN(0);
}
@@ -274,7 +274,7 @@ extern "C" {
Z3_TRY;
LOG_Z3_disable_literal(c, lbls, idx);
RESET_ERROR_CODE();
- (*reinterpret_cast<labels*>(lbls))[idx].disable();
+ (*reinterpret_cast<labels*>(lbls))[idx].disable();
Z3_CATCH;
}
@@ -348,4 +348,4 @@ void Z3_display_statistics(Z3_context c, std::ostream& s) {
void Z3_display_istatistics(Z3_context c, std::ostream& s) {
mk_c(c)->get_smt_kernel().display_istatistics(s);
}
-
+