From 6bdde9047aae6b0b12ea85b19f6c6218a0e8f5e6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 5 Dec 2012 12:01:03 -0800
Subject: [PATCH] fixing unit tests
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/muz_qe/rel_context.h | 3 +--
src/smt/smt_model_checker.cpp | 1 +
src/test/dl_context.cpp | 2 +-
src/test/dl_product_relation.cpp | 9 +++++----
src/test/dl_query.cpp | 8 ++++----
src/test/dl_relation.cpp | 4 ++--
src/test/dl_table.cpp | 4 ++--
7 files changed, 16 insertions(+), 15 deletions(-)
diff --git a/src/muz_qe/rel_context.h b/src/muz_qe/rel_context.h
index 5fa2486b4..b05532d14 100644
--- a/src/muz_qe/rel_context.h
+++ b/src/muz_qe/rel_context.h
@@ -41,8 +41,6 @@ namespace datalog {
fact_vector m_table_facts;
void reset_negated_tables();
-
- lbool saturate();
relation_plugin & get_ordinary_relation_plugin(symbol relation_name);
@@ -109,6 +107,7 @@ namespace datalog {
void display_output_facts(std::ostream & out) const;
void display_facts(std::ostream & out) const;
+ lbool saturate();
};
};
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 53f3af961..cefdacef5 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -283,6 +283,7 @@ namespace smt {
if (!m_fparams) {
m_fparams = alloc(smt_params, m_context->get_fparams());
m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free
+ m_fparams->m_proof_mode = m_manager.proof_mode();
}
if (!m_aux_context) {
symbol logic;
diff --git a/src/test/dl_context.cpp b/src/test/dl_context.cpp
index ff7548abc..d5fcddb71 100644
--- a/src/test/dl_context.cpp
+++ b/src/test/dl_context.cpp
@@ -60,7 +60,7 @@ void dl_context_saturate_file(params_ref & params, const char * f) {
}
dealloc(parser);
std::cerr << "Saturating...\n";
- ctx.dl_saturate();
+ ctx.get_rel_context().saturate();
std::cerr << "Done\n";
}
diff --git a/src/test/dl_product_relation.cpp b/src/test/dl_product_relation.cpp
index e58634ec8..ef43258ad 100644
--- a/src/test/dl_product_relation.cpp
+++ b/src/test/dl_product_relation.cpp
@@ -22,11 +22,12 @@ namespace datalog {
void test_functional_columns(smt_params fparams, params_ref& params) {
ast_manager m;
context ctx(m, fparams);
+ rel_context& rctx = ctx.get_rel_context();
ctx.updt_params(params);
- relation_manager & rmgr(ctx.get_rmanager());
+ relation_manager & rmgr(rctx.get_rmanager());
sparse_table_plugin & plugin =
- static_cast<sparse_table_plugin &>(*ctx.get_rmanager().get_table_plugin(symbol("sparse")));
+ static_cast<sparse_table_plugin &>(*rctx.get_rmanager().get_table_plugin(symbol("sparse")));
SASSERT(&plugin);
table_signature sig2;
sig2.push_back(2);
@@ -126,9 +127,9 @@ namespace datalog {
context ctx(m, fparams);
ctx.updt_params(params);
dl_decl_util dl_util(m);
- relation_manager & rmgr = ctx.get_rmanager();
+ relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
- relation_plugin & rel_plugin = *ctx.get_rmanager().get_relation_plugin(params.get_sym("default_relation", symbol("sparse")));
+ relation_plugin & rel_plugin = *rmgr.get_relation_plugin(params.get_sym("default_relation", symbol("sparse")));
SASSERT(&rel_plugin);
finite_product_relation_plugin plg(rel_plugin, rmgr);
diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp
index ad21247af..4dc770056 100644
--- a/src/test/dl_query.cpp
+++ b/src/test/dl_query.cpp
@@ -57,7 +57,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
TRUSTME( p->parse_file(problem_file) );
dealloc(p);
}
- relation_manager & rel_mgr_q = ctx_b.get_rmanager();
+ relation_manager & rel_mgr_q = ctx_b.get_rel_context().get_rmanager();
decl_set out_preds = ctx_b.get_output_predicates();
decl_set::iterator it = out_preds.begin();
@@ -68,10 +68,10 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
func_decl * pred_q = ctx_q.try_get_predicate_decl(symbol(pred_b->get_name().bare_str()));
SASSERT(pred_q);
- relation_base & rel_b = ctx_b.get_relation(pred_b);
+ relation_base & rel_b = ctx_b.get_rel_context().get_relation(pred_b);
relation_signature sig_b = rel_b.get_signature();
- relation_signature sig_q = ctx_q.get_relation(pred_q).get_signature();
+ relation_signature sig_q = ctx_q.get_rel_context().get_relation(pred_q).get_signature();
SASSERT(sig_b.size()==sig_q.size());
std::cerr << "Queries on random facts...\n";
@@ -209,7 +209,7 @@ void tst_dl_query() {
TRUSTME( p->parse_file(problem_file) );
dealloc(p);
}
- ctx_base.dl_saturate();
+ ctx_base.get_rel_context().saturate();
for(unsigned use_restarts=0; use_restarts<=1; use_restarts++) {
params.set_uint("initial_restart_timeout", use_restarts ? 100 : 0);
diff --git a/src/test/dl_relation.cpp b/src/test/dl_relation.cpp
index fe8ba1730..5daf3dc9b 100644
--- a/src/test/dl_relation.cpp
+++ b/src/test/dl_relation.cpp
@@ -12,7 +12,7 @@ namespace datalog {
ast_manager ast_m;
context ctx(ast_m, params);
arith_util autil(ast_m);
- relation_manager & m = ctx.get_rmanager();
+ relation_manager & m = ctx.get_rel_context().get_rmanager();
m.register_plugin(alloc(interval_relation_plugin, m));
interval_relation_plugin& ip = dynamic_cast<interval_relation_plugin&>(*m.get_relation_plugin(symbol("interval_relation")));
SASSERT(&ip);
@@ -115,7 +115,7 @@ namespace datalog {
ast_manager ast_m;
context ctx(ast_m, params);
arith_util autil(ast_m);
- relation_manager & m = ctx.get_rmanager();
+ relation_manager & m = ctx.get_rel_context().get_rmanager();
m.register_plugin(alloc(bound_relation_plugin, m));
bound_relation_plugin& br = dynamic_cast<bound_relation_plugin&>(*m.get_relation_plugin(symbol("bound_relation")));
SASSERT(&br);
diff --git a/src/test/dl_table.cpp b/src/test/dl_table.cpp
index 6383dc1ab..0c8afcdc2 100644
--- a/src/test/dl_table.cpp
+++ b/src/test/dl_table.cpp
@@ -27,9 +27,9 @@ static void test_table(mk_table_fn mk_table) {
smt_params params;
ast_manager ast_m;
datalog::context ctx(ast_m, params);
- datalog::relation_manager & m = ctx.get_rmanager();
+ datalog::relation_manager & m = ctx.get_rel_context().get_rmanager();
- ctx.get_rmanager().register_plugin(alloc(datalog::bitvector_table_plugin, ctx.get_rmanager()));
+ m.register_plugin(alloc(datalog::bitvector_table_plugin, m));
datalog::table_base* _tbl = mk_table(m, sig);
datalog::table_base& table = *_tbl;