mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

Replaced antiquated header with modern equivalent.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-24 13:29:17 +01:00
parent 4f3f21bff1
commit df2a569d25
1 changed files with 17 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/cmd_context/check_logic.cpp
View file

@ -24,7 +24,7 @@ Revision History:
#include"datatype_decl_plugin.h" #include"datatype_decl_plugin.h"
#include"ast_pp.h" #include"ast_pp.h"
#include"for_each_expr.h" #include"for_each_expr.h"
#include<strstream> #include<sstream>
struct check_logic::imp { struct check_logic::imp {
ast_manager & m; ast_manager & m;
@ -189,7 +189,7 @@ struct check_logic::imp {
else { else {
m_unknown_logic = true; m_unknown_logic = true;
} }
m_logic = logic; m_logic = logic;
} }
@ -237,7 +237,7 @@ struct check_logic::imp {
} }
} }
void operator()(var * n) { void operator()(var * n) {
if (!m_quantifiers) if (!m_quantifiers)
fail("logic does not support quantifiers"); fail("logic does not support quantifiers");
check_sort(m.get_sort(n)); check_sort(m.get_sort(n));
@ -279,7 +279,7 @@ struct check_logic::imp {
} }
} }
} }
// check if the divisor is a numeral // check if the divisor is a numeral
void check_div(app * n) { void check_div(app * n) {
SASSERT(n->get_num_args() == 2); SASSERT(n->get_num_args() == 2);
@ -328,8 +328,8 @@ struct check_logic::imp {
return false; return false;
non_numeral = arg; non_numeral = arg;
} }
if (non_numeral == 0) if (non_numeral == 0)
return true; return true;
if (is_diff_var(non_numeral)) if (is_diff_var(non_numeral))
return true; return true;
if (!m_a_util.is_add(non_numeral) && !m_a_util.is_sub(non_numeral)) if (!m_a_util.is_add(non_numeral) && !m_a_util.is_sub(non_numeral))
@ -338,10 +338,10 @@ struct check_logic::imp {
} }
return true; return true;
} }
bool is_diff_arg(expr * t) { bool is_diff_arg(expr * t) {
if (is_diff_var(t)) if (is_diff_var(t))
return true; return true;
if (is_numeral(t)) if (is_numeral(t))
return true; return true;
if (m_a_util.is_add(t) || m_a_util.is_sub(t)) if (m_a_util.is_add(t) || m_a_util.is_sub(t))
@ -366,7 +366,7 @@ struct check_logic::imp {
expr * t1 = to_app(lhs)->get_arg(0); expr * t1 = to_app(lhs)->get_arg(0);
expr * t2 = to_app(lhs)->get_arg(1); expr * t2 = to_app(lhs)->get_arg(1);
if (is_diff_var(t1) && is_diff_var(t2)) if (is_diff_var(t1) && is_diff_var(t2))
return; return;
if (m_a_util.is_add(t1) && m_a_util.is_add(t2)) { if (m_a_util.is_add(t1) && m_a_util.is_add(t2)) {
// QF_RDL supports (<= (- (+ x ... x) (+ y ... y)) c) // QF_RDL supports (<= (- (+ x ... x) (+ y ... y)) c)
if (to_app(t1)->get_num_args() != to_app(t2)->get_num_args()) if (to_app(t1)->get_num_args() != to_app(t2)->get_num_args())
@ -391,7 +391,7 @@ struct check_logic::imp {
check_diff_arg(n); check_diff_arg(n);
} }
} }
void operator()(app * n) { void operator()(app * n) {
sort * s = m.get_sort(n); sort * s = m.get_sort(n);
check_sort(s); check_sort(s);
@ -415,18 +415,18 @@ struct check_logic::imp {
if (!m_ints || !m_reals) { if (!m_ints || !m_reals) {
if (m_a_util.is_to_real(n) || m_a_util.is_to_int(n)) if (m_a_util.is_to_real(n) || m_a_util.is_to_int(n))
fail("logic does not support casting operators"); fail("logic does not support casting operators");
} }
} }
else if (fid == m_bv_util.get_family_id()) { else if (fid == m_bv_util.get_family_id()) {
// nothing to check... // nothing to check...
} }
else if (fid == m_ar_util.get_family_id()) { else if (fid == m_ar_util.get_family_id()) {
// nothing to check... // nothing to check...
if (m_diff) if (m_diff)
check_diff_args(n); check_diff_args(n);
} }
else if (fid == m.get_basic_family_id()) { else if (fid == m.get_basic_family_id()) {
// nothing to check... // nothing to check...
if (m_diff) { if (m_diff) {
if (m.is_eq(n)) if (m.is_eq(n))
check_diff_predicate(n); check_diff_predicate(n);
@ -449,8 +449,8 @@ struct check_logic::imp {
fail(strm.str().c_str()); fail(strm.str().c_str());
} }
} }
void operator()(quantifier * n) { void operator()(quantifier * n) {
if (!m_quantifiers) if (!m_quantifiers)
fail("logic does not support quantifiers"); fail("logic does not support quantifiers");
} }
@ -490,7 +490,7 @@ struct check_logic::imp {
check_logic::check_logic() { check_logic::check_logic() {
m_imp = 0; m_imp = 0;
} }
check_logic::~check_logic() { check_logic::~check_logic() {
if (m_imp) if (m_imp)
dealloc(m_imp); dealloc(m_imp);