mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

fix build break - by renaming tout to out

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-11-06 10:21:02 -08:00
commit 5ea2c22153
10 changed files with 70 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

6
scripts/mk_util.py
View file

@ -75,7 +75,7 @@ VER_MAJOR=None
VER_MINOR=None
VER_BUILD=None
VER_REVISION=None
PREFIX=os.path.split(os.path.split(os.path.split(PYTHON_PACKAGE_DIR)[0])[0])[0]
PREFIX=sys.prefix
GMP=False
FOCI2=False
FOCI2LIB=''
@ -531,6 +531,7 @@ if os.name == 'nt':
elif os.name == 'posix':
if os.uname()[0] == 'Darwin':
IS_OSX=True
PREFIX="/usr/local"
elif os.uname()[0] == 'Linux':
IS_LINUX=True
elif os.uname()[0] == 'FreeBSD':
@ -1984,6 +1985,7 @@ def mk_config():
print('Prefix: %s' % PREFIX)
print('64-bit: %s' % is64())
print('FP math: %s' % FPMATH)
print("Python pkg dir: %s" % PYTHON_PACKAGE_DIR)
if GPROF:
print('gprof: enabled')
print('Python version: %s' % distutils.sysconfig.get_python_version())
@ -2074,8 +2076,6 @@ def mk_makefile():
# Finalize
if VERBOSE:
print("Makefile was successfully generated.")
if not IS_WINDOWS:
print(" python packages dir: %s" % PYTHON_PACKAGE_DIR)
if DEBUG_MODE:
print(" compilation mode: Debug")
else:

4
src/api/java/Model.java
View file

@ -56,7 +56,7 @@ public class Model extends Z3Object
Native.getRange(getContext().nCtx(), f.getNativeObject())) == Z3_sort_kind.Z3_ARRAY_SORT
.toInt())
throw new Z3Exception(
"Non-zero arity functions and arrays have FunctionInterpretations as a model. Use FuncInterp.");
"Non-zero arity functions and arrays have FunctionInterpretations as a model. Use getFuncInterp.");
long n = Native.modelGetConstInterp(getContext().nCtx(), getNativeObject(),
f.getNativeObject());
@ -101,7 +101,7 @@ public class Model extends Z3Object
} else
{
throw new Z3Exception(
"Constant functions do not have a function interpretation; use ConstInterp");
"Constant functions do not have a function interpretation; use getConstInterp");
}
} else
{

3
src/api/python/z3.py
View file

@ -284,6 +284,9 @@ class AstRef(Z3PPObject):
def __repr__(self):
return obj_to_string(self)
def __hash__(self):
return self.hash()
def sexpr(self):
"""Return an string representing the AST node in s-expression notation.

8
src/cmd_context/cmd_context.cpp
View file

@ -507,6 +507,8 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "QF_AUFLIRA" ||
s == "QF_AUFNIA" ||
s == "QF_AUFNIRA" ||
s == "QF_ANIA" ||
s == "QF_LIRA" ||
s == "QF_UFLIA" ||
s == "QF_UFLRA" ||
s == "QF_UFIDL" ||
@ -518,6 +520,7 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "QF_UFNIA" ||
s == "QF_UFNIRA" ||
s == "QF_BVRE" ||
s == "ALIA" ||
s == "AUFLIA" ||
s == "AUFLIRA" ||
s == "AUFNIA" ||
@ -526,9 +529,12 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
s == "UFLRA" ||
s == "UFNRA" ||
s == "UFNIRA" ||
s == "NIA" ||
s == "NRA" ||
s == "UFNIA" ||
s == "LIA" ||
s == "LRA" ||
s == "UFIDL" ||
s == "QF_FP" ||
s == "QF_FPBV" ||
s == "QF_BVFP" ||
@ -583,10 +589,12 @@ bool cmd_context::logic_has_array_core(symbol const & s) const {
return
s == "QF_AX" ||
s == "QF_AUFLIA" ||
s == "QF_ANIA" ||
s == "QF_ALIA" ||
s == "QF_AUFLIRA" ||
s == "QF_AUFNIA" ||
s == "QF_AUFNIRA" ||
s == "ALIA" ||
s == "AUFLIA" ||
s == "AUFLIRA" ||
s == "AUFNIA" ||

66
src/smt/smt_context_pp.cpp
View file

@ -27,19 +27,19 @@ namespace smt {
std::ostream& context::display_last_failure(std::ostream& out) const {
switch(m_last_search_failure) {
case OK:
case OK:
return out << "OK";
case UNKNOWN:
case UNKNOWN:
return out << "UNKNOWN";
case TIMEOUT:
return out << "TIMEOUT";
case MEMOUT:
case MEMOUT:
return out << "MEMOUT";
case CANCELED:
case CANCELED:
return out << "CANCELED";
case NUM_CONFLICTS:
case NUM_CONFLICTS:
return out << "NUM_CONFLICTS";
case THEORY:
case THEORY:
if (!m_incomplete_theories.empty()) {
ptr_vector<theory>::const_iterator it = m_incomplete_theories.begin();
ptr_vector<theory>::const_iterator end = m_incomplete_theories.end();
@ -52,7 +52,7 @@ namespace smt {
out << "THEORY";
}
return out;
case QUANTIFIERS:
case QUANTIFIERS:
return out << "QUANTIFIERS";
}
UNREACHABLE();
@ -78,18 +78,18 @@ namespace smt {
r += "))";
break;
}
case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
case UNKNOWN: r = "incomplete"; break;
}
return r;
}
void context::display_asserted_formulas(std::ostream & out) const {
m_asserted_formulas.display_ll(out, get_pp_visited());
}
void context::display_literal(std::ostream & out, literal l) const {
l.display_compact(out, m_bool_var2expr.c_ptr());
l.display_compact(out, m_bool_var2expr.c_ptr());
}
void context::display_literals(std::ostream & out, unsigned num_lits, literal const * lits) const {
@ -151,16 +151,16 @@ namespace smt {
for (unsigned i = 0; i < num_lits; i++) {
literal l = cls->get_literal(i);
display_literal(out, l);
out << ", val: " << get_assignment(l) << ", lvl: " << get_assign_level(l)
<< ", ilvl: " << get_intern_level(l.var()) << ", var: " << l.var() << "\n"
out << ", val: " << get_assignment(l) << ", lvl: " << get_assign_level(l)
<< ", ilvl: " << get_intern_level(l.var()) << ", var: " << l.var() << "\n"
<< mk_pp(bool_var2expr(l.var()), m_manager) << "\n\n";
}
}
void context::display_clause(std::ostream & out, clause const * cls) const {
cls->display_compact(out, m_manager, m_bool_var2expr.c_ptr());
}
void context::display_clauses(std::ostream & out, ptr_vector<clause> const & v) const {
ptr_vector<clause>::const_iterator it = v.begin();
ptr_vector<clause>::const_iterator end = v.end();
@ -201,7 +201,7 @@ namespace smt {
if (!m_assigned_literals.empty()) {
out << "current assignment:\n";
literal_vector::const_iterator it = m_assigned_literals.begin();
literal_vector::const_iterator end = m_assigned_literals.end();
literal_vector::const_iterator end = m_assigned_literals.end();
for (; it != end; ++it) {
display_literal(out, *it);
out << ": ";
@ -217,7 +217,7 @@ namespace smt {
pp.set_status("unknown");
pp.set_logic(logic);
literal_vector::const_iterator it = m_assigned_literals.begin();
literal_vector::const_iterator end = m_assigned_literals.end();
literal_vector::const_iterator end = m_assigned_literals.end();
for (; it != end; ++it) {
expr_ref n(m_manager);
literal2expr(*it, n);
@ -302,7 +302,7 @@ namespace smt {
th->display(out);
}
}
void context::display(std::ostream & out) const {
get_pp_visited().reset();
out << "Logical context:\n";
@ -337,16 +337,16 @@ namespace smt {
void context::display_eq_detail(std::ostream & out, enode * n) const {
SASSERT(n->is_eq());
out << "#" << n->get_owner_id()
<< ", root: #" << n->get_root()->get_owner_id()
out << "#" << n->get_owner_id()
<< ", root: #" << n->get_root()->get_owner_id()
<< ", cg: #" << n->m_cg->get_owner_id()
<< ", val: " << get_assignment(enode2bool_var(n))
<< ", lhs: #" << n->get_arg(0)->get_owner_id()
<< ", rhs: #" << n->get_arg(1)->get_owner_id()
<< ", lhs->root: #" << n->get_arg(0)->get_root()->get_owner_id()
<< ", rhs->root: #" << n->get_arg(1)->get_root()->get_owner_id()
<< ", val: " << get_assignment(enode2bool_var(n))
<< ", lhs: #" << n->get_arg(0)->get_owner_id()
<< ", rhs: #" << n->get_arg(1)->get_owner_id()
<< ", lhs->root: #" << n->get_arg(0)->get_root()->get_owner_id()
<< ", rhs->root: #" << n->get_arg(1)->get_root()->get_owner_id()
<< ", is_marked: " << n->is_marked()
<< ", is_relevant: " << is_relevant(n)
<< ", is_relevant: " << is_relevant(n)
<< ", iscope_lvl: " << n->get_iscope_lvl() << "\n";
}
@ -355,7 +355,7 @@ namespace smt {
enode_vector::iterator end = n->end_parents();
for (; it != end; ++it) {
enode * parent = *it;
if (parent->is_eq())
if (parent->is_eq())
display_eq_detail(out, parent);
}
}
@ -448,7 +448,7 @@ namespace smt {
g_lemma_id++;
}
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
literal consequent, const char * logic) const {
ast_smt_pp pp(m_manager);
@ -472,7 +472,7 @@ namespace smt {
pp.display_smt2(out, n);
}
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
literal consequent, const char * logic) const {
char buffer[BUFFER_SZ];
@ -534,7 +534,7 @@ namespace smt {
n->display_lbls(out);
}
}
void context::display_decl2enodes(std::ostream & out) const {
out << "decl2enodes:\n";
vector<enode_vector>::const_iterator it1 = m_decl2enodes.begin();
@ -545,7 +545,7 @@ namespace smt {
out << "id " << id << " ->";
enode_vector::const_iterator it2 = v.begin();
enode_vector::const_iterator end2 = v.end();
for (; it2 != end2; ++it2)
for (; it2 != end2; ++it2)
out << " #" << (*it2)->get_owner_id();
out << "\n";
}
@ -568,7 +568,7 @@ namespace smt {
out << std::right;
if (lit_internalized(n))
out << get_assignment(n);
else
else
out << "l_undef";
}
if (e_internalized(n)) {
@ -577,12 +577,12 @@ namespace smt {
}
out << "\n";
if (is_app(n)) {
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++)
for (unsigned i = 0; i < to_app(n)->get_num_args(); i++)
todo.push_back(to_app(n)->get_arg(i));
}
}
}
void context::display(std::ostream& out, b_justification j) const {
switch (j.get_kind()) {
case b_justification::AXIOM:

4
src/tactic/smtlogics/qfaufbv_tactic.h
View file

@ -25,4 +25,8 @@ class tactic;
tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("qfaufbv", "builtin strategy for solving QF_AUFBV problems.", "mk_qfaufbv_tactic(m, p)")
*/
#endif

4
src/tactic/smtlogics/qfauflia_tactic.h
View file

@ -25,4 +25,8 @@ class tactic;
tactic * mk_qfauflia_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("qfauflia", "builtin strategy for solving QF_AUFLIA problems.", "mk_qfauflia_tactic(m, p)")
*/
#endif

4
src/tactic/smtlogics/qfidl_tactic.h
View file

@ -25,4 +25,8 @@ class tactic;
tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("qfidl", "builtin strategy for solving QF_IDL problems.", "mk_qfidl_tactic(m, p)")
*/
#endif

4
src/tactic/smtlogics/qfuf_tactic.h
View file

@ -26,4 +26,8 @@ class tactic;
tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p);
/*
ADD_TACTIC("qfuf", "builtin strategy for solving QF_UF problems.", "mk_qfuf_tactic(m, p)")
*/
#endif

6
src/tactic/smtlogics/qfufbv_tactic.h
View file

@ -7,7 +7,7 @@ Module Name:
Abstract:
Tactic for QF_UFBV
Tactic for QF_UFBV
Author:
@ -25,4 +25,8 @@ class tactic;
tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p = params_ref());
/*
ADD_TACTIC("qfufbv", "builtin strategy for solving QF_UFBV problems.", "mk_qfufbv_tactic(m, p)")
*/
#endif