mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 04:38:53 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-09-09 23:05:34 -07:00
commit ab5894412d
4 changed files with 12 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

2
examples/tptp/tptp5.tab.c
View file

@ -107,7 +107,7 @@ struct pTreeNode {
pTree children[MAX_CHILDREN+1]; pTree children[MAX_CHILDREN+1];
}; };
//----------------------------------------------------------------------------- //-----------------------------------------------------------------------------
int yyerror( char *s ) { int yyerror( char const *s ) {
fprintf( stderr, "%s in line %d at item \"%s\".\n", s, yylineno, yytext); fprintf( stderr, "%s in line %d at item \"%s\".\n", s, yylineno, yytext);
return 0; return 0;

2
src/muz/base/dl_util.cpp
View file

@ -34,8 +34,6 @@ Revision History:
namespace datalog { namespace datalog {
static unsigned verbose_action_inside = 0;
verbose_action::verbose_action(char const* msg, unsigned lvl): m_lvl(lvl), m_sw(0) { verbose_action::verbose_action(char const* msg, unsigned lvl): m_lvl(lvl), m_sw(0) {
IF_VERBOSE(m_lvl, IF_VERBOSE(m_lvl,
(verbose_stream() << msg << "...").flush(); (verbose_stream() << msg << "...").flush();

3
src/muz/rel/dl_lazy_table.cpp
View file

@ -19,7 +19,7 @@ Revision History:
#include "dl_lazy_table.h" #include "dl_lazy_table.h"
#include "dl_relation_manager.h" #include "dl_relation_manager.h"
#include <strstream> #include <sstream>
namespace datalog { namespace datalog {
@ -53,7 +53,6 @@ namespace datalog {
virtual table_base* operator()(const table_base& _t1, const table_base& _t2) { virtual table_base* operator()(const table_base& _t1, const table_base& _t2) {
lazy_table const& t1 = get(_t1); lazy_table const& t1 = get(_t1);
lazy_table const& t2 = get(_t2); lazy_table const& t2 = get(_t2);
lazy_table_plugin& p = t1.get_lplugin();
lazy_table_ref* tr = alloc(lazy_table_join, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr(), t1, t2, get_result_signature()); lazy_table_ref* tr = alloc(lazy_table_join, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr(), t1, t2, get_result_signature());
return alloc(lazy_table, tr); return alloc(lazy_table, tr);
} }

20
src/muz/rel/dl_lazy_table.h
View file

@ -156,7 +156,7 @@ namespace datalog {
virtual table_base::iterator begin() const; virtual table_base::iterator begin() const;
virtual table_base::iterator end() const; virtual table_base::iterator end() const;
lazy_table_ref* ref() const { return m_ref.get(); } lazy_table_ref* get_ref() const { return m_ref.get(); }
void set(lazy_table_ref* r) { m_ref = r; } void set(lazy_table_ref* r) { m_ref = r; }
}; };
@ -184,8 +184,8 @@ namespace datalog {
: lazy_table_ref(t1.get_lplugin(), sig), : lazy_table_ref(t1.get_lplugin(), sig),
m_cols1(col_cnt, cols1), m_cols1(col_cnt, cols1),
m_cols2(col_cnt, cols2), m_cols2(col_cnt, cols2),
m_t1(t1.ref()), m_t1(t1.get_ref()),
m_t2(t2.ref()) { } m_t2(t2.get_ref()) { }
virtual ~lazy_table_join() {} virtual ~lazy_table_join() {}
virtual lazy_table_kind kind() const { return LAZY_TABLE_JOIN; } virtual lazy_table_kind kind() const { return LAZY_TABLE_JOIN; }
unsigned_vector const& cols1() const { return m_cols1; } unsigned_vector const& cols1() const { return m_cols1; }
@ -203,7 +203,7 @@ namespace datalog {
lazy_table_project(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig) lazy_table_project(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig)
: lazy_table_ref(src.get_lplugin(), sig), : lazy_table_ref(src.get_lplugin(), sig),
m_cols(col_cnt, cols), m_cols(col_cnt, cols),
m_src(src.ref()) {} m_src(src.get_ref()) {}
virtual ~lazy_table_project() {} virtual ~lazy_table_project() {}
virtual lazy_table_kind kind() const { return LAZY_TABLE_PROJECT; } virtual lazy_table_kind kind() const { return LAZY_TABLE_PROJECT; }
@ -219,7 +219,7 @@ namespace datalog {
lazy_table_rename(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig) lazy_table_rename(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig)
: lazy_table_ref(src.get_lplugin(), sig), : lazy_table_ref(src.get_lplugin(), sig),
m_cols(col_cnt, cols), m_cols(col_cnt, cols),
m_src(src.ref()) {} m_src(src.get_ref()) {}
virtual ~lazy_table_rename() {} virtual ~lazy_table_rename() {}
virtual lazy_table_kind kind() const { return LAZY_TABLE_RENAME; } virtual lazy_table_kind kind() const { return LAZY_TABLE_RENAME; }
@ -233,7 +233,7 @@ namespace datalog {
ref<lazy_table_ref> m_src; ref<lazy_table_ref> m_src;
public: public:
lazy_table_filter_identical(unsigned col_cnt, const unsigned * cols, lazy_table const& src) lazy_table_filter_identical(unsigned col_cnt, const unsigned * cols, lazy_table const& src)
: lazy_table_ref(src.get_lplugin(), src.get_signature()), m_cols(col_cnt, cols), m_src(src.ref()) {} : lazy_table_ref(src.get_lplugin(), src.get_signature()), m_cols(col_cnt, cols), m_src(src.get_ref()) {}
virtual ~lazy_table_filter_identical() {} virtual ~lazy_table_filter_identical() {}
virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_IDENTICAL; } virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_IDENTICAL; }
@ -251,7 +251,7 @@ namespace datalog {
: lazy_table_ref(src.get_lplugin(), src.get_signature()), : lazy_table_ref(src.get_lplugin(), src.get_signature()),
m_col(col), m_col(col),
m_value(value), m_value(value),
m_src(src.ref()) {} m_src(src.get_ref()) {}
virtual ~lazy_table_filter_equal() {} virtual ~lazy_table_filter_equal() {}
virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_EQUAL; } virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_EQUAL; }
@ -267,7 +267,7 @@ namespace datalog {
public: public:
lazy_table_filter_interpreted(lazy_table const& src, app* condition) lazy_table_filter_interpreted(lazy_table const& src, app* condition)
: lazy_table_ref(src.get_lplugin(), src.get_signature()), : lazy_table_ref(src.get_lplugin(), src.get_signature()),
m_condition(condition, src.get_lplugin().get_ast_manager()), m_src(src.ref()) {} m_condition(condition, src.get_lplugin().get_ast_manager()), m_src(src.get_ref()) {}
virtual ~lazy_table_filter_interpreted() {} virtual ~lazy_table_filter_interpreted() {}
virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_INTERPRETED; } virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_INTERPRETED; }
@ -286,8 +286,8 @@ namespace datalog {
lazy_table_filter_by_negation(lazy_table const& tgt, lazy_table const& src, lazy_table_filter_by_negation(lazy_table const& tgt, lazy_table const& src,
unsigned_vector const& c1, unsigned_vector const& c2) unsigned_vector const& c1, unsigned_vector const& c2)
: lazy_table_ref(tgt.get_lplugin(), tgt.get_signature()), : lazy_table_ref(tgt.get_lplugin(), tgt.get_signature()),
m_tgt(tgt.ref()), m_tgt(tgt.get_ref()),
m_src(src.ref()), m_src(src.get_ref()),
m_cols1(c1), m_cols1(c1),
m_cols2(c2) {} m_cols2(c2) {}
virtual ~lazy_table_filter_by_negation() {} virtual ~lazy_table_filter_by_negation() {}