mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
Formatting, mostly tabs.
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
parent
cad841cff4
commit
0381e4317a
|
@ -173,7 +173,7 @@ extern "C" {
|
|||
if (mk_c(c)->datalog_util().is_numeral(e, v)) {
|
||||
r = rational(v, rational::ui64());
|
||||
return Z3_TRUE;
|
||||
}
|
||||
}
|
||||
return Z3_FALSE;
|
||||
Z3_CATCH_RETURN(Z3_FALSE);
|
||||
}
|
||||
|
|
|
@ -413,16 +413,16 @@ sort * get_sort(expr const * n) {
|
|||
//
|
||||
// -----------------------------------
|
||||
|
||||
unsigned get_node_size(ast const * n) {
|
||||
switch(n->get_kind()) {
|
||||
case AST_SORT: return to_sort(n)->get_size();
|
||||
case AST_FUNC_DECL: return to_func_decl(n)->get_size();
|
||||
case AST_APP: return to_app(n)->get_size();
|
||||
case AST_VAR: return to_var(n)->get_size();
|
||||
case AST_QUANTIFIER: return to_quantifier(n)->get_size();
|
||||
default: UNREACHABLE();
|
||||
}
|
||||
return 0;
|
||||
unsigned get_node_size(ast const * n) {
|
||||
switch(n->get_kind()) {
|
||||
case AST_SORT: return to_sort(n)->get_size();
|
||||
case AST_FUNC_DECL: return to_func_decl(n)->get_size();
|
||||
case AST_APP: return to_app(n)->get_size();
|
||||
case AST_VAR: return to_var(n)->get_size();
|
||||
case AST_QUANTIFIER: return to_quantifier(n)->get_size();
|
||||
default: UNREACHABLE();
|
||||
}
|
||||
return 0;
|
||||
}
|
||||
|
||||
bool compare_nodes(ast const * n1, ast const * n2) {
|
||||
|
@ -737,7 +737,7 @@ func_decl * basic_decl_plugin::mk_proof_decl(
|
|||
for (unsigned i = 0; i < num_parents; i++)
|
||||
domain.push_back(m_proof_sort);
|
||||
domain.push_back(m_bool_sort);
|
||||
func_decl_info info(m_family_id, k, num_parameters, params);
|
||||
func_decl_info info(m_family_id, k, num_parameters, params);
|
||||
return m_manager->mk_func_decl(symbol(name), num_parents+1, domain.c_ptr(), m_proof_sort, info);
|
||||
}
|
||||
|
||||
|
@ -1643,12 +1643,12 @@ ast * ast_manager::register_node_core(ast * n) {
|
|||
to_func_decl(n)->m_info = alloc(func_decl_info, *(to_func_decl(n)->get_info()));
|
||||
to_func_decl(n)->m_info->init_eh(*this);
|
||||
}
|
||||
inc_array_ref(to_func_decl(n)->get_arity(), to_func_decl(n)->get_domain());
|
||||
inc_ref(to_func_decl(n)->get_range());
|
||||
break;
|
||||
inc_array_ref(to_func_decl(n)->get_arity(), to_func_decl(n)->get_domain());
|
||||
inc_ref(to_func_decl(n)->get_range());
|
||||
break;
|
||||
case AST_APP: {
|
||||
app * t = to_app(n);
|
||||
inc_ref(t->get_decl());
|
||||
inc_ref(t->get_decl());
|
||||
unsigned num_args = t->get_num_args();
|
||||
if (num_args > 0) {
|
||||
app_flags * f = t->flags();
|
||||
|
@ -1696,19 +1696,19 @@ ast * ast_manager::register_node_core(ast * n) {
|
|||
f->m_depth = depth;
|
||||
SASSERT(t->get_depth() == depth);
|
||||
}
|
||||
break;
|
||||
break;
|
||||
}
|
||||
case AST_VAR:
|
||||
inc_ref(to_var(n)->get_sort());
|
||||
break;
|
||||
case AST_QUANTIFIER:
|
||||
inc_array_ref(to_quantifier(n)->get_num_decls(), to_quantifier(n)->get_decl_sorts());
|
||||
inc_ref(to_quantifier(n)->get_expr());
|
||||
inc_array_ref(to_quantifier(n)->get_num_decls(), to_quantifier(n)->get_decl_sorts());
|
||||
inc_ref(to_quantifier(n)->get_expr());
|
||||
inc_array_ref(to_quantifier(n)->get_num_patterns(), to_quantifier(n)->get_patterns());
|
||||
inc_array_ref(to_quantifier(n)->get_num_no_patterns(), to_quantifier(n)->get_no_patterns());
|
||||
break;
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
break;
|
||||
}
|
||||
return n;
|
||||
}
|
||||
|
@ -1721,7 +1721,7 @@ void ast_manager::delete_node(ast * n) {
|
|||
while (!worklist.empty()) {
|
||||
n = worklist.back();
|
||||
worklist.pop_back();
|
||||
|
||||
|
||||
TRACE("ast", tout << "Deleting object " << n->m_id << " " << n << "\n";);
|
||||
CTRACE("del_quantifier", is_quantifier(n), tout << "deleting quantifier " << n->m_id << " " << n << "\n";);
|
||||
TRACE("mk_var_bug", tout << "del_ast: " << n->m_id << "\n";);
|
||||
|
@ -1770,8 +1770,8 @@ void ast_manager::delete_node(ast * n) {
|
|||
dec_array_ref(worklist, to_quantifier(n)->get_num_patterns(), to_quantifier(n)->get_patterns());
|
||||
dec_array_ref(worklist, to_quantifier(n)->get_num_no_patterns(), to_quantifier(n)->get_no_patterns());
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
if (m_debug_ref_count) {
|
||||
m_debug_free_indices.insert(n->m_id,0);
|
||||
|
@ -2567,9 +2567,9 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) {
|
|||
(is_eq(get_fact(p2)) || is_oeq(get_fact(p2)))));
|
||||
CTRACE("mk_transitivity", to_app(get_fact(p1))->get_arg(1) != to_app(get_fact(p2))->get_arg(0),
|
||||
tout << mk_pp(get_fact(p1), *this) << "\n\n" << mk_pp(get_fact(p2), *this) << "\n";
|
||||
tout << mk_bounded_pp(p1, *this, 5) << "\n\n";
|
||||
tout << mk_bounded_pp(p2, *this, 5) << "\n\n";
|
||||
);
|
||||
tout << mk_bounded_pp(p1, *this, 5) << "\n\n";
|
||||
tout << mk_bounded_pp(p2, *this, 5) << "\n\n";
|
||||
);
|
||||
SASSERT(to_app(get_fact(p1))->get_arg(1) == to_app(get_fact(p2))->get_arg(0));
|
||||
if (is_reflexivity(p1))
|
||||
return p2;
|
||||
|
|
|
@ -3197,7 +3197,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
|
|||
|
||||
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
|
||||
#ifdef Z3DEBUG
|
||||
// return;
|
||||
return;
|
||||
// CMW: This works only for quantifier-free formulas.
|
||||
expr_ref new_e(m);
|
||||
new_e = m.mk_fresh_const(prefix, m.get_sort(e));
|
||||
|
|
|
@ -24,31 +24,31 @@ Revision History:
|
|||
ast_manager& m = result.get_manager();
|
||||
uint64 v1, v2;
|
||||
switch(f->get_decl_kind()) {
|
||||
case datalog::OP_DL_LT:
|
||||
if (m_util.is_numeral_ext(args[0], v1) &&
|
||||
m_util.is_numeral_ext(args[1], v2)) {
|
||||
result = (v1 < v2)?m.mk_true():m.mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
// x < x <=> false
|
||||
if (args[0] == args[1]) {
|
||||
result = m.mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
// x < 0 <=> false
|
||||
if (m_util.is_numeral_ext(args[1], v2) && v2 == 0) {
|
||||
result = m.mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
// 0 < x <=> 0 != x
|
||||
if (m_util.is_numeral_ext(args[1], v1) && v1 == 0) {
|
||||
result = m.mk_not(m.mk_eq(args[0], args[1]));
|
||||
return BR_DONE;
|
||||
}
|
||||
break;
|
||||
case datalog::OP_DL_LT:
|
||||
if (m_util.is_numeral_ext(args[0], v1) &&
|
||||
m_util.is_numeral_ext(args[1], v2)) {
|
||||
result = (v1 < v2)?m.mk_true():m.mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
// x < x <=> false
|
||||
if (args[0] == args[1]) {
|
||||
result = m.mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
// x < 0 <=> false
|
||||
if (m_util.is_numeral_ext(args[1], v2) && v2 == 0) {
|
||||
result = m.mk_false();
|
||||
return BR_DONE;
|
||||
}
|
||||
// 0 < x <=> 0 != x
|
||||
if (m_util.is_numeral_ext(args[1], v1) && v1 == 0) {
|
||||
result = m.mk_not(m.mk_eq(args[0], args[1]));
|
||||
return BR_DONE;
|
||||
}
|
||||
break;
|
||||
|
||||
default:
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
return BR_FAILED;
|
||||
}
|
||||
|
|
|
@ -124,20 +124,20 @@ namespace Duality {
|
|||
}
|
||||
|
||||
void timer_stop(const char *name){
|
||||
if(current->name != name || !current->parent){
|
||||
if (current->name != name || !current->parent) {
|
||||
#if 0
|
||||
std::cerr << "imbalanced timer_start and timer_stop";
|
||||
exit(1);
|
||||
std::cerr << "imbalanced timer_start and timer_stop";
|
||||
exit(1);
|
||||
#endif
|
||||
// in case we lost a timer stop due to an exception
|
||||
while(current->name != name && current->parent)
|
||||
current = current->parent;
|
||||
if(current->parent){
|
||||
current->time += (current_time() - current->start_time);
|
||||
current = current->parent;
|
||||
// in case we lost a timer stop due to an exception
|
||||
while (current->name != name && current->parent)
|
||||
current = current->parent;
|
||||
if (current->parent) {
|
||||
current->time += (current_time() - current->start_time);
|
||||
current = current->parent;
|
||||
}
|
||||
return;
|
||||
}
|
||||
return;
|
||||
}
|
||||
current->time += (current_time() - current->start_time);
|
||||
current = current->parent;
|
||||
}
|
||||
|
|
File diff suppressed because it is too large
Load diff
|
@ -187,10 +187,10 @@ namespace datalog {
|
|||
if (m_trail.get_num_scopes() == 0) {
|
||||
throw default_exception("there are no backtracking points to pop to");
|
||||
}
|
||||
if(m_engine.get()){
|
||||
if(get_engine() != DUALITY_ENGINE)
|
||||
throw default_exception("operation is not supported by engine");
|
||||
}
|
||||
if(m_engine.get()){
|
||||
if(get_engine() != DUALITY_ENGINE)
|
||||
throw default_exception("operation is not supported by engine");
|
||||
}
|
||||
m_trail.pop_scope(1);
|
||||
}
|
||||
|
||||
|
@ -478,7 +478,7 @@ namespace datalog {
|
|||
void context::add_rule(expr* rl, symbol const& name, unsigned bound) {
|
||||
m_rule_fmls.push_back(rl);
|
||||
m_rule_names.push_back(name);
|
||||
m_rule_bounds.push_back(bound);
|
||||
m_rule_bounds.push_back(bound);
|
||||
}
|
||||
|
||||
void context::flush_add_rules() {
|
||||
|
@ -706,7 +706,7 @@ namespace datalog {
|
|||
check_existential_tail(r);
|
||||
check_positive_predicates(r);
|
||||
break;
|
||||
case DUALITY_ENGINE:
|
||||
case DUALITY_ENGINE:
|
||||
check_existential_tail(r);
|
||||
check_positive_predicates(r);
|
||||
break;
|
||||
|
|
|
@ -77,12 +77,12 @@ namespace Duality {
|
|||
old_rs = 0;
|
||||
}
|
||||
~duality_data(){
|
||||
if(old_rs)
|
||||
dealloc(old_rs);
|
||||
if(rpfp)
|
||||
dealloc(rpfp);
|
||||
if(ls)
|
||||
dealloc(ls);
|
||||
if(old_rs)
|
||||
dealloc(old_rs);
|
||||
if(rpfp)
|
||||
dealloc(rpfp);
|
||||
if(ls)
|
||||
(ls);
|
||||
}
|
||||
};
|
||||
|
||||
|
@ -171,16 +171,16 @@ lbool dl_interface::query(::expr * query) {
|
|||
query_ref = m_ctx.get_manager().mk_false();
|
||||
else {
|
||||
func_decl_ref query_pred(m_ctx.get_manager());
|
||||
query_pred = m_ctx.get_rules().get_output_predicate();
|
||||
ptr_vector<sort> sorts;
|
||||
unsigned nargs = query_pred.get()->get_arity();
|
||||
expr_ref_vector vars(m_ctx.get_manager());
|
||||
for(unsigned i = 0; i < nargs; i++){
|
||||
::sort *s = query_pred.get()->get_domain(i);
|
||||
vars.push_back(m_ctx.get_manager().mk_var(nargs-1-i,s));
|
||||
}
|
||||
query_ref = m_ctx.get_manager().mk_app(query_pred.get(),nargs,vars.c_ptr());
|
||||
query = query_ref.get();
|
||||
query_pred = m_ctx.get_rules().get_output_predicate();
|
||||
ptr_vector<sort> sorts;
|
||||
unsigned nargs = query_pred.get()->get_arity();
|
||||
expr_ref_vector vars(m_ctx.get_manager());
|
||||
for(unsigned i = 0; i < nargs; i++){
|
||||
::sort *s = query_pred.get()->get_domain(i);
|
||||
vars.push_back(m_ctx.get_manager().mk_var(nargs-1-i,s));
|
||||
}
|
||||
query_ref = m_ctx.get_manager().mk_app(query_pred.get(),nargs,vars.c_ptr());
|
||||
query = query_ref.get();
|
||||
}
|
||||
unsigned nrules = rs.get_num_rules();
|
||||
for(unsigned i = 0; i < nrules; i++){
|
||||
|
@ -250,16 +250,16 @@ lbool dl_interface::query(::expr * query) {
|
|||
|
||||
while(true){
|
||||
if(cl.is_app()){
|
||||
decl_kind k = cl.decl().get_decl_kind();
|
||||
if(k == Implies)
|
||||
cl = cl.arg(1);
|
||||
else {
|
||||
heads.insert(cl.decl());
|
||||
break;
|
||||
}
|
||||
decl_kind k = cl.decl().get_decl_kind();
|
||||
if(k == Implies)
|
||||
cl = cl.arg(1);
|
||||
else {
|
||||
heads.insert(cl.decl());
|
||||
break;
|
||||
}
|
||||
}
|
||||
else if(cl.is_quantifier())
|
||||
cl = cl.body();
|
||||
cl = cl.body();
|
||||
else break;
|
||||
}
|
||||
}
|
||||
|
@ -268,18 +268,18 @@ lbool dl_interface::query(::expr * query) {
|
|||
::ast *fa = pinned[i];
|
||||
if(is_func_decl(fa)){
|
||||
::func_decl *fd = to_func_decl(fa);
|
||||
if(m_ctx.is_predicate(fd)) {
|
||||
func_decl f(_d->ctx,fd);
|
||||
if(!heads.contains(fd)){
|
||||
int arity = f.arity();
|
||||
std::vector<expr> args;
|
||||
for(int j = 0; j < arity; j++)
|
||||
args.push_back(_d->ctx.fresh_func_decl("X",f.domain(j))());
|
||||
expr c = implies(_d->ctx.bool_val(false),f(args));
|
||||
c = _d->ctx.make_quant(Forall,args,c);
|
||||
clauses.push_back(c);
|
||||
bounds.push_back(UINT_MAX);
|
||||
}
|
||||
if (m_ctx.is_predicate(fd)) {
|
||||
func_decl f(_d->ctx, fd);
|
||||
if (!heads.contains(fd)) {
|
||||
int arity = f.arity();
|
||||
std::vector<expr> args;
|
||||
for (int j = 0; j < arity; j++)
|
||||
args.push_back(_d->ctx.fresh_func_decl("X", f.domain(j))());
|
||||
expr c = implies(_d->ctx.bool_val(false), f(args));
|
||||
c = _d->ctx.make_quant(Forall, args, c);
|
||||
clauses.push_back(c);
|
||||
bounds.push_back(UINT_MAX);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
@ -483,17 +483,17 @@ void dl_interface::display_certificate_non_const(std::ostream& out) {
|
|||
model orig_model = _d->cex.get_tree()->dualModel;
|
||||
for(unsigned i = 0; i < orig_model.num_consts(); i++){
|
||||
func_decl cnst = orig_model.get_const_decl(i);
|
||||
if(locals.find(cnst) == locals.end()){
|
||||
expr thing = orig_model.get_const_interp(cnst);
|
||||
mod.register_decl(to_func_decl(cnst.raw()),to_expr(thing.raw()));
|
||||
if (locals.find(cnst) == locals.end()) {
|
||||
expr thing = orig_model.get_const_interp(cnst);
|
||||
mod.register_decl(to_func_decl(cnst.raw()), to_expr(thing.raw()));
|
||||
}
|
||||
}
|
||||
for(unsigned i = 0; i < orig_model.num_funcs(); i++){
|
||||
func_decl cnst = orig_model.get_func_decl(i);
|
||||
if(locals.find(cnst) == locals.end()){
|
||||
func_interp thing = orig_model.get_func_interp(cnst);
|
||||
::func_interp *thing_raw = thing;
|
||||
mod.register_decl(to_func_decl(cnst.raw()),thing_raw->copy());
|
||||
if (locals.find(cnst) == locals.end()) {
|
||||
func_interp thing = orig_model.get_func_interp(cnst);
|
||||
::func_interp *thing_raw = thing;
|
||||
mod.register_decl(to_func_decl(cnst.raw()), thing_raw->copy());
|
||||
}
|
||||
}
|
||||
model_v2_pp(out,mod);
|
||||
|
|
|
@ -72,7 +72,7 @@ namespace datalog {
|
|||
|
||||
transf.register_plugin(alloc(datalog::mk_bit_blast, ctx, 35000));
|
||||
if (!ctx.get_params().quantify_arrays())
|
||||
transf.register_plugin(alloc(datalog::mk_array_blast, ctx, 36000));
|
||||
transf.register_plugin(alloc(datalog::mk_array_blast, ctx, 36000));
|
||||
transf.register_plugin(alloc(datalog::mk_karr_invariants, ctx, 36010));
|
||||
if (ctx.get_params().magic()) {
|
||||
transf.register_plugin(alloc(datalog::mk_magic_symbolic, ctx, 36020));
|
||||
|
|
|
@ -27,7 +27,7 @@ Notes:
|
|||
struct aig;
|
||||
|
||||
class aig_lit {
|
||||
friend class aig_ref;
|
||||
friend class aig_ref;
|
||||
aig * m_ref;
|
||||
public:
|
||||
aig_lit(aig * n = 0):m_ref(n) {}
|
||||
|
@ -1508,10 +1508,10 @@ public:
|
|||
template<typename S>
|
||||
aig_lit mk_aig(S const & s) {
|
||||
aig_lit r;
|
||||
r = m_true;
|
||||
inc_ref(r);
|
||||
r = m_true;
|
||||
inc_ref(r);
|
||||
try {
|
||||
expr2aig proc(*this);
|
||||
expr2aig proc(*this);
|
||||
unsigned sz = s.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
SASSERT(ref_count(r) >= 1);
|
||||
|
@ -1528,9 +1528,9 @@ public:
|
|||
}
|
||||
SASSERT(ref_count(r) >= 1);
|
||||
}
|
||||
catch (aig_exception ex) {
|
||||
dec_ref(r);
|
||||
throw ex;
|
||||
catch (aig_exception ex) {
|
||||
dec_ref(r);
|
||||
throw ex;
|
||||
}
|
||||
dec_ref_result(r);
|
||||
return r;
|
||||
|
|
Loading…
Reference in a new issue