mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
missing file
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
db65cc007a
commit
48d144a6dd
|
@ -20,10 +20,10 @@ Revision History:
|
|||
#include "ast/ast_pp.h"
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
#include "ast/rewriter/var_subst.h"
|
||||
#include "util/container_util.h"
|
||||
|
||||
|
||||
|
||||
proof_post_order::proof_post_order(proof* root, ast_manager& manager) : m(manager)
|
||||
{m_todo.push_back(root);}
|
||||
|
||||
|
@ -336,7 +336,6 @@ void reduce_hypotheses(proof_ref &pr) {
|
|||
|
||||
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/rewriter/var_subst.h"
|
||||
|
||||
class reduce_hypotheses0 {
|
||||
typedef obj_hashtable<expr> expr_set;
|
||||
|
|
|
@ -20,6 +20,7 @@ Revision History:
|
|||
#ifndef PROOF_UTILS_H_
|
||||
#define PROOF_UTILS_H_
|
||||
#include "ast/ast.h"
|
||||
#include "ast/rewriter/bool_rewriter.h"
|
||||
|
||||
/*
|
||||
* iterator, which traverses the proof in depth-first post-order.
|
||||
|
@ -66,7 +67,6 @@ public:
|
|||
|
||||
};
|
||||
|
||||
#include "ast/rewriter/bool_rewriter.h"
|
||||
class elim_aux_assertions {
|
||||
|
||||
static bool matches_fact(expr_ref_vector &args, expr* &match) {
|
||||
|
|
|
@ -244,7 +244,6 @@ void virtual_solver::refresh()
|
|||
m_head = 0;
|
||||
}
|
||||
|
||||
#ifdef NOT_USED_ANYWHERE
|
||||
void virtual_solver::reset()
|
||||
{
|
||||
SASSERT(!m_pushed);
|
||||
|
@ -252,7 +251,6 @@ void virtual_solver::reset()
|
|||
m_assertions.reset();
|
||||
m_factory.refresh();
|
||||
}
|
||||
#endif
|
||||
|
||||
void virtual_solver::get_labels(svector<symbol> &r)
|
||||
{
|
||||
|
|
|
@ -91,9 +91,7 @@ public:
|
|||
virtual void set_produce_models(bool f);
|
||||
virtual bool get_produce_models();
|
||||
virtual smt_params &fparams();
|
||||
#ifdef NOT_USED_ANYWHERE
|
||||
virtual void reset();
|
||||
#endif
|
||||
virtual void set_progress_callback(progress_callback *callback)
|
||||
{UNREACHABLE();}
|
||||
|
||||
|
@ -135,6 +133,9 @@ private:
|
|||
|
||||
|
||||
void refresh();
|
||||
|
||||
smt_params &fparams() { return m_fparams; }
|
||||
|
||||
public:
|
||||
virtual_solver_factory(ast_manager &mgr, smt_params &fparams);
|
||||
virtual ~virtual_solver_factory();
|
||||
|
@ -145,7 +146,6 @@ public:
|
|||
void collect_param_descrs(param_descrs &r) { /* empty */ }
|
||||
void set_produce_models(bool f) { m_fparams.m_model = f; }
|
||||
bool get_produce_models() { return m_fparams.m_model; }
|
||||
smt_params &fparams() { return m_fparams; }
|
||||
};
|
||||
|
||||
}
|
||||
|
|
121
src/util/container_util.h
Normal file
121
src/util/container_util.h
Normal file
|
@ -0,0 +1,121 @@
|
|||
/*++
|
||||
Copyright (c) 2017 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
container_util.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Useful functions for containers
|
||||
|
||||
Author:
|
||||
|
||||
Krystof Hoder, Nikolaj Bjorner 2017-10-24
|
||||
|
||||
Revision History:
|
||||
|
||||
Extracted from dl_util.h
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef CONTAINUR_UTIL_H
|
||||
#define CONTAINER_UTIL_H_
|
||||
|
||||
// -----------------------------------
|
||||
//
|
||||
// container functions
|
||||
//
|
||||
// -----------------------------------
|
||||
|
||||
template<class Set1, class Set2>
|
||||
void set_intersection(Set1 & tgt, const Set2 & src) {
|
||||
svector<typename Set1::data> to_remove;
|
||||
for (Set1::data itm : tgt)
|
||||
if (!src.contains(itm))
|
||||
to_remove.push_back(itm);
|
||||
while (!to_remove.empty()) {
|
||||
tgt.remove(to_remove.back());
|
||||
to_remove.pop_back();
|
||||
}
|
||||
}
|
||||
|
||||
template<class Set>
|
||||
void set_difference(Set & tgt, const Set & to_remove) {
|
||||
for (auto const& itm : to_remove)
|
||||
tgt.remove(itm);
|
||||
}
|
||||
|
||||
template<class Set1, class Set2>
|
||||
void set_union(Set1 & tgt, const Set2 & to_add) {
|
||||
for (auto const& itm : to_add)
|
||||
tgt.insert(itm);
|
||||
}
|
||||
|
||||
template<class T>
|
||||
void unite_disjoint_maps(T & tgt, const T & src) {
|
||||
for (auto const& kv : src) {
|
||||
SASSERT(!tgt.contains(kv.m_key));
|
||||
tgt.insert(kv.m_key, kv.m_value);
|
||||
}
|
||||
}
|
||||
|
||||
template<class T, class U>
|
||||
void collect_map_range(T & acc, const U & map) {
|
||||
for (auto const& kv : map)
|
||||
acc.push_back(kv.m_value);
|
||||
}
|
||||
|
||||
|
||||
template<class T>
|
||||
void print_container(const T & begin, const T & end, std::ostream & out) {
|
||||
T it = begin;
|
||||
out << "(";
|
||||
bool first = true;
|
||||
for(; it!=end; ++it) {
|
||||
if(first) { first = false; } else { out << ","; }
|
||||
out << (*it);
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
|
||||
template<class T>
|
||||
void print_container(const T & cont, std::ostream & out) {
|
||||
print_container(cont.begin(), cont.end(), out);
|
||||
}
|
||||
|
||||
template<class T, class M>
|
||||
void print_container(const ref_vector<T,M> & cont, std::ostream & out) {
|
||||
print_container(cont.c_ptr(), cont.c_ptr() + cont.size(), out);
|
||||
}
|
||||
|
||||
template<class T>
|
||||
void print_map(const T & cont, std::ostream & out) {
|
||||
out << "(";
|
||||
bool first = true;
|
||||
for (auto const& kv : cont) {
|
||||
if (first) { first = false; } else { out << ","; }
|
||||
out << kv.m_key << "->" << kv.m_value;
|
||||
}
|
||||
out << ")";
|
||||
}
|
||||
|
||||
template<class It, class V>
|
||||
unsigned find_index(const It & begin, const It & end, const V & val) {
|
||||
for (unsigned idx = 0, It it = begin; it != end; it++, idx++) {
|
||||
if (*it == val) {
|
||||
return idx;
|
||||
}
|
||||
}
|
||||
return UINT_MAX;
|
||||
}
|
||||
|
||||
template<class T, class U>
|
||||
bool containers_equal(const T & begin1, const T & end1, const U & begin2, const U & end2) {
|
||||
T it1 = begin1;
|
||||
U it2 = begin2;
|
||||
for (; it1 != end1 && it2 != end2 && *it1 == *it2; ++it1, ++it2) {};
|
||||
return it1 == end1 && it2 == end2;
|
||||
}
|
||||
|
||||
#endif
|
Loading…
Reference in a new issue