mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

stubs for spacer-specific API

Browse source
This commit is contained in:
Arie Gurfinkel 2017-07-31 15:42:44 -04:00
parent ffa4957362
commit 1530a39a96
2 changed files with 17 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/muz/base/dl_engine_base.h
View file

@ -20,6 +20,7 @@ Revision History:
#define DL_ENGINE_BASE_H_ #define DL_ENGINE_BASE_H_
#include "model/model.h" #include "model/model.h"
#include "muz/base/dl_util.h"
namespace datalog { namespace datalog {
enum DL_ENGINE { enum DL_ENGINE {
@ -44,6 +45,9 @@ namespace datalog {
virtual ~engine_base() {} virtual ~engine_base() {}
virtual expr_ref get_answer() = 0; virtual expr_ref get_answer() = 0;
virtual expr_ref get_ground_sat_answer () {
throw default_exception(std::string("operation is not supported for ") + m_name);
}
virtual lbool query(expr* q) = 0; virtual lbool query(expr* q) = 0;
virtual lbool query(unsigned num_rels, func_decl*const* rels) { virtual lbool query(unsigned num_rels, func_decl*const* rels) {
if (num_rels != 1) return l_undef; if (num_rels != 1) return l_undef;
@ -65,6 +69,9 @@ namespace datalog {
} }
return query(q); return query(q);
} }
virtual lbool query_from_lvl (expr* q, unsigned lvl) {
throw default_exception(std::string("operation is not supported for ") + m_name);
}
virtual void reset_statistics() {} virtual void reset_statistics() {}
virtual void display_profile(std::ostream& out) {} virtual void display_profile(std::ostream& out) {}
@ -72,18 +79,27 @@ namespace datalog {
virtual unsigned get_num_levels(func_decl* pred) { virtual unsigned get_num_levels(func_decl* pred) {
throw default_exception(std::string("get_num_levels is not supported for ") + m_name); throw default_exception(std::string("get_num_levels is not supported for ") + m_name);
} }
virtual expr_ref get_reachable(func_decl* pred) {
throw default_exception(std::string("operation is not supported for ") + m_name);
}
virtual expr_ref get_cover_delta(int level, func_decl* pred) { virtual expr_ref get_cover_delta(int level, func_decl* pred) {
throw default_exception(std::string("operation is not supported for ") + m_name); throw default_exception(std::string("operation is not supported for ") + m_name);
} }
virtual void add_cover(int level, func_decl* pred, expr* property) { virtual void add_cover(int level, func_decl* pred, expr* property) {
throw default_exception(std::string("operation is not supported for ") + m_name); throw default_exception(std::string("operation is not supported for ") + m_name);
} }
virtual void add_invariant (func_decl *pred, expr *property) {
throw default_exception(std::string("operation is not supported for ") + m_name);
}
virtual void display_certificate(std::ostream& out) const { virtual void display_certificate(std::ostream& out) const {
throw default_exception(std::string("certificates are not supported for ") + m_name); throw default_exception(std::string("certificates are not supported for ") + m_name);
} }
virtual model_ref get_model() { virtual model_ref get_model() {
return model_ref(alloc(model, m)); return model_ref(alloc(model, m));
} }
virtual void get_rules_along_trace (rule_ref_vector& rules) {
throw default_exception(std::string("get_rules_along_trace is not supported for ") + m_name);
}
virtual proof_ref get_proof() { virtual proof_ref get_proof() {
return proof_ref(m.mk_asserted(m.mk_true()), m); return proof_ref(m.mk_asserted(m.mk_true()), m);
} }

1
src/muz/base/dl_util.h
View file

@ -52,6 +52,7 @@ namespace datalog {
~verbose_action(); ~verbose_action();
}; };
typedef ref_vector<rule, rule_manager> rule_ref_vector;
enum PDR_CACHE_MODE { enum PDR_CACHE_MODE {
NO_CACHE, NO_CACHE,
HASH_CACHE, HASH_CACHE,