mirror of
https://github.com/Z3Prover/z3
synced 2025-04-29 03:45:51 +00:00
Post merge compile fixes
This commit is contained in:
Arie Gurfinkel
parent
649bab2f58
commit
3bc3b00fdd
12 changed files with 66 additions and 129 deletions
|
|
@ -14,6 +14,7 @@ z3_add_component(spacer
|
|||
spacer_iuc_solver.cpp
|
||||
spacer_virtual_solver.cpp
|
||||
spacer_legacy_mbp.cpp
|
||||
spacer_proof_utils.cpp
|
||||
spacer_unsat_core_learner.cpp
|
||||
spacer_unsat_core_plugin.cpp
|
||||
spacer_matrix.cpp
|
||||
|
|
|
|||
|
|
@ -40,7 +40,7 @@ Notes:
|
|||
#include "ast/ast_smt2_pp.h"
|
||||
#include "ast/ast_ll_pp.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/proof_checker/proof_checker.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
#include "smt/smt_value_sort.h"
|
||||
#include "ast/scoped_proof.h"
|
||||
#include "muz/spacer/spacer_qe_project.h"
|
||||
|
|
@ -3618,9 +3618,9 @@ expr_ref context::get_constraints (unsigned level)
|
|||
return m_pm.mk_and (constraints);
|
||||
}
|
||||
|
||||
void context::add_constraint (unsigned level, const expr_ref& c)
|
||||
void context::add_constraint (expr *c, unsigned level)
|
||||
{
|
||||
if (!c.get()) { return; }
|
||||
if (!c) { return; }
|
||||
if (m.is_true(c)) { return; }
|
||||
|
||||
expr *e1, *e2;
|
||||
|
|
|
|||
|
|
@ -914,7 +914,7 @@ public:
|
|||
pob& get_root() const { return m_pob_queue.get_root(); }
|
||||
|
||||
expr_ref get_constraints (unsigned lvl);
|
||||
void add_constraint (unsigned lvl, const expr_ref& c);
|
||||
void add_constraint (expr *c, unsigned lvl);
|
||||
|
||||
void new_lemma_eh(pred_transformer &pt, lemma *lem);
|
||||
|
||||
|
|
|
|||
|
|
@ -362,5 +362,5 @@ void dl_interface::add_callback(void *state,
|
|||
}
|
||||
|
||||
void dl_interface::add_constraint (expr *c, unsigned lvl){
|
||||
m_context->add_constraint(c,lvl);
|
||||
m_context->add_constraint(c, lvl);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -82,9 +82,9 @@ public:
|
|||
void add_callback(void *state,
|
||||
const datalog::t_new_lemma_eh new_lemma_eh,
|
||||
const datalog::t_predecessor_eh predecessor_eh,
|
||||
const datalog::t_unfold_eh unfold_eh);
|
||||
const datalog::t_unfold_eh unfold_eh) override;
|
||||
|
||||
void add_constraint (expr *c, unsigned lvl);
|
||||
void add_constraint (expr *c, unsigned lvl) override;
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
|||
|
|
@ -162,7 +162,7 @@ void unsat_core_generalizer::operator()(lemma_ref &lemma)
|
|||
|
||||
unsigned uses_level;
|
||||
expr_ref_vector core(m);
|
||||
VERIFY(pt.is_invariant(old_level, lemma->get_expr(), uses_level, &core));
|
||||
VERIFY(pt.is_invariant(lemma->level(), lemma.get(), uses_level, &core));
|
||||
|
||||
CTRACE("spacer", old_sz > core.size(),
|
||||
tout << "unsat core reduced lemma from: "
|
||||
|
|
|
|||
|
|
@ -1,8 +1,7 @@
|
|||
|
||||
|
||||
#include "muz/spacer/spacer_iuc_proof.h"
|
||||
#include "ast/for_each_expr.h"
|
||||
#include "ast/array_decl_plugin.h"
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
#include "muz/spacer/spacer_proof_utils.h"
|
||||
|
||||
namespace spacer {
|
||||
|
|
@ -18,7 +17,7 @@ namespace spacer {
|
|||
collect_symbols_b(b_conjuncts);
|
||||
compute_marks(b_conjuncts);
|
||||
}
|
||||
|
||||
|
||||
proof* iuc_proof::get()
|
||||
{
|
||||
return m_pr.get();
|
||||
|
|
@ -33,7 +32,7 @@ namespace spacer {
|
|||
func_decl_set& m_symbs;
|
||||
public:
|
||||
collect_pure_proc(func_decl_set& s):m_symbs(s) {}
|
||||
|
||||
|
||||
void operator()(app* a) {
|
||||
if (a->get_family_id() == null_family_id) {
|
||||
m_symbs.insert(a->get_decl());
|
||||
|
|
@ -42,7 +41,7 @@ namespace spacer {
|
|||
void operator()(var*) {}
|
||||
void operator()(quantifier*) {}
|
||||
};
|
||||
|
||||
|
||||
void iuc_proof::collect_symbols_b(expr_set& b_conjuncts)
|
||||
{
|
||||
expr_mark visited;
|
||||
|
|
@ -52,18 +51,18 @@ namespace spacer {
|
|||
for_each_expr(proc, visited, *it);
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
class is_pure_expr_proc {
|
||||
func_decl_set const& m_symbs;
|
||||
array_util m_au;
|
||||
public:
|
||||
struct non_pure {};
|
||||
|
||||
|
||||
is_pure_expr_proc(func_decl_set const& s, ast_manager& m):
|
||||
m_symbs(s),
|
||||
m_au (m)
|
||||
{}
|
||||
|
||||
|
||||
void operator()(app* a) {
|
||||
if (a->get_family_id() == null_family_id) {
|
||||
if (!m_symbs.contains(a->get_decl())) {
|
||||
|
|
@ -78,7 +77,7 @@ namespace spacer {
|
|||
void operator()(var*) {}
|
||||
void operator()(quantifier*) {}
|
||||
};
|
||||
|
||||
|
||||
// requires that m_symbols_b has already been computed, which is done during initialization.
|
||||
bool iuc_proof::only_contains_symbols_b(expr* expr) const
|
||||
{
|
||||
|
|
@ -92,26 +91,26 @@ namespace spacer {
|
|||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
/*
|
||||
* ====================================
|
||||
* methods for computing which premises
|
||||
* have been used to derive the conclusions
|
||||
* ====================================
|
||||
*/
|
||||
|
||||
|
||||
void iuc_proof::compute_marks(expr_set& b_conjuncts)
|
||||
{
|
||||
ProofIteratorPostOrder it(m_pr, m);
|
||||
proof_post_order it(m_pr, m);
|
||||
while (it.hasNext())
|
||||
{
|
||||
proof* currentNode = it.next();
|
||||
|
||||
|
||||
if (m.get_num_parents(currentNode) == 0)
|
||||
{
|
||||
switch(currentNode->get_decl_kind())
|
||||
{
|
||||
|
||||
|
||||
case PR_ASSERTED: // currentNode is an axiom
|
||||
{
|
||||
if (b_conjuncts.contains(m.get_fact(currentNode)))
|
||||
|
|
@ -142,23 +141,23 @@ namespace spacer {
|
|||
bool need_to_mark_a = false;
|
||||
bool need_to_mark_b = false;
|
||||
bool need_to_mark_h = false;
|
||||
|
||||
|
||||
for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i)
|
||||
{
|
||||
SASSERT(m.is_proof(currentNode->get_arg(i)));
|
||||
proof* premise = to_app(currentNode->get_arg(i));
|
||||
|
||||
|
||||
need_to_mark_a = need_to_mark_a || m_a_mark.is_marked(premise);
|
||||
need_to_mark_b = need_to_mark_b || m_b_mark.is_marked(premise);
|
||||
need_to_mark_h = need_to_mark_h || m_h_mark.is_marked(premise);
|
||||
}
|
||||
|
||||
|
||||
// if current node is application of lemma, we know that all hypothesis are removed
|
||||
if(currentNode->get_decl_kind() == PR_LEMMA)
|
||||
{
|
||||
need_to_mark_h = false;
|
||||
}
|
||||
|
||||
|
||||
// save results
|
||||
m_a_mark.mark(currentNode, need_to_mark_a);
|
||||
m_b_mark.mark(currentNode, need_to_mark_b);
|
||||
|
|
@ -166,7 +165,7 @@ namespace spacer {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bool iuc_proof::is_a_marked(proof* p)
|
||||
{
|
||||
return m_a_mark.is_marked(p);
|
||||
|
|
@ -179,7 +178,7 @@ namespace spacer {
|
|||
{
|
||||
return m_h_mark.is_marked(p);
|
||||
}
|
||||
|
||||
|
||||
/*
|
||||
* ====================================
|
||||
* methods for dot printing
|
||||
|
|
@ -195,22 +194,22 @@ namespace spacer {
|
|||
* statistics
|
||||
* ====================================
|
||||
*/
|
||||
|
||||
|
||||
void iuc_proof::print_farkas_stats()
|
||||
{
|
||||
unsigned farkas_counter = 0;
|
||||
unsigned farkas_counter2 = 0;
|
||||
|
||||
ProofIteratorPostOrder it3(m_pr, m);
|
||||
|
||||
proof_post_order it3(m_pr, m);
|
||||
while (it3.hasNext())
|
||||
{
|
||||
proof* currentNode = it3.next();
|
||||
|
||||
|
||||
// if node is theory lemma
|
||||
if (is_farkas_lemma(m, currentNode))
|
||||
{
|
||||
farkas_counter++;
|
||||
|
||||
|
||||
// check whether farkas lemma is to be interpolated (could potentially miss farkas lemmas, which are interpolated, because we potentially don't want to use the lowest cut)
|
||||
bool has_blue_nonred_parent = false;
|
||||
for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i)
|
||||
|
|
@ -229,7 +228,7 @@ namespace spacer {
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
verbose_stream() << "\nThis proof contains " << farkas_counter << " Farkas lemmas. " << farkas_counter2 << " Farkas lemmas participate in the lowest cut\n";
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -19,7 +19,7 @@ Notes:
|
|||
#include"muz/spacer/spacer_iuc_solver.h"
|
||||
#include"ast/ast.h"
|
||||
#include"muz/spacer/spacer_util.h"
|
||||
#include"muz/base/proof_utils.h"
|
||||
#include"ast/proofs/proof_utils.h"
|
||||
#include"muz/spacer/spacer_farkas_learner.h"
|
||||
#include"ast/rewriter/expr_replacer.h"
|
||||
#include"muz/spacer/spacer_unsat_core_learner.h"
|
||||
|
|
|
|||
|
|
@ -22,8 +22,8 @@ Notes:
|
|||
|
||||
#include<iostream>
|
||||
#include<map>
|
||||
#include "ref.h"
|
||||
#include "ref_vector.h"
|
||||
#include "util/ref.h"
|
||||
#include "util/ref_vector.h"
|
||||
|
||||
class ast;
|
||||
|
||||
|
|
|
|||
|
|
@ -16,20 +16,22 @@ Revision History:
|
|||
|
||||
--*/
|
||||
|
||||
#include "muz/spacer/spacer_proof_utils.h"
|
||||
#include "ast/ast_util.h"
|
||||
|
||||
#include "ast/ast_pp.h"
|
||||
|
||||
#include "ast/proof_checker/proof_checker.h"
|
||||
#include <unordered_map>
|
||||
#include "params.h"
|
||||
#include "muz/spacer/spacer_iuc_proof.h"
|
||||
#include "util/params.h"
|
||||
#include "ast/ast_pp.h"
|
||||
#include "ast/ast_util.h"
|
||||
#include "ast/proofs/proof_checker.h"
|
||||
#include "muz/base/dl_util.h"
|
||||
#include "muz/spacer/spacer_iuc_proof.h"
|
||||
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
#include "muz/spacer/spacer_proof_utils.h"
|
||||
|
||||
namespace spacer {
|
||||
|
||||
// arith lemmas: second parameter specifies exact type of lemma, could be "farkas", "triangle-eq", "eq-propagate", "assign-bounds", maybe also something else
|
||||
// arith lemmas: second parameter specifies exact type of lemma,
|
||||
// could be "farkas", "triangle-eq", "eq-propagate",
|
||||
// "assign-bounds", maybe also something else
|
||||
bool is_arith_lemma(ast_manager& m, proof* pr)
|
||||
{
|
||||
if (pr->get_decl_kind() == PR_TH_LEMMA)
|
||||
|
|
@ -61,57 +63,6 @@ namespace spacer {
|
|||
return false;
|
||||
}
|
||||
|
||||
/*
|
||||
* ====================================
|
||||
* methods for proof traversal
|
||||
* ====================================
|
||||
*/
|
||||
ProofIteratorPostOrder::ProofIteratorPostOrder(proof* root, ast_manager& manager) : m(manager)
|
||||
{m_todo.push_back(root);}
|
||||
|
||||
bool ProofIteratorPostOrder::hasNext()
|
||||
{return !m_todo.empty();}
|
||||
|
||||
/*
|
||||
* iterative post-order depth-first search (DFS) through the proof DAG
|
||||
*/
|
||||
proof* ProofIteratorPostOrder::next()
|
||||
{
|
||||
while (!m_todo.empty()) {
|
||||
proof* currentNode = m_todo.back();
|
||||
|
||||
// if we haven't already visited the current unit
|
||||
if (!m_visited.is_marked(currentNode)) {
|
||||
bool existsUnvisitedParent = false;
|
||||
|
||||
// add unprocessed premises to stack for DFS. If there is at least one unprocessed premise, don't compute the result
|
||||
// for currentProof now, but wait until those unprocessed premises are processed.
|
||||
for (unsigned i = 0; i < m.get_num_parents(currentNode); ++i) {
|
||||
SASSERT(m.is_proof(currentNode->get_arg(i)));
|
||||
proof* premise = to_app(currentNode->get_arg(i));
|
||||
|
||||
// if we haven't visited the current premise yet
|
||||
if (!m_visited.is_marked(premise)) {
|
||||
// add it to the stack
|
||||
m_todo.push_back(premise);
|
||||
existsUnvisitedParent = true;
|
||||
}
|
||||
}
|
||||
|
||||
// if we already visited all parent-inferences, we can visit the inference too
|
||||
if (!existsUnvisitedParent) {
|
||||
m_visited.mark(currentNode, true);
|
||||
m_todo.pop_back();
|
||||
return currentNode;
|
||||
}
|
||||
} else {
|
||||
m_todo.pop_back();
|
||||
}
|
||||
}
|
||||
// we have already iterated through all inferences
|
||||
return NULL;
|
||||
}
|
||||
|
||||
/*
|
||||
* ====================================
|
||||
* methods for dot printing
|
||||
|
|
@ -140,7 +91,7 @@ proof* ProofIteratorPostOrder::next()
|
|||
std::unordered_map<unsigned, unsigned> id_to_small_id;
|
||||
unsigned counter = 0;
|
||||
|
||||
ProofIteratorPostOrder it2(pr, m);
|
||||
proof_post_order it2(pr, m);
|
||||
while (it2.hasNext())
|
||||
{
|
||||
proof* currentNode = it2.next();
|
||||
|
|
@ -306,7 +257,7 @@ proof* ProofIteratorPostOrder::next()
|
|||
|
||||
proof_ref theory_axiom_reducer::reduce(proof* pr)
|
||||
{
|
||||
ProofIteratorPostOrder pit(pr, m);
|
||||
proof_post_order pit(pr, m);
|
||||
while (pit.hasNext())
|
||||
{
|
||||
proof* p = pit.next();
|
||||
|
|
@ -468,11 +419,11 @@ proof* ProofIteratorPostOrder::next()
|
|||
for (unsigned i = 0, sz = m.get_num_parents(p); i < sz; ++i)
|
||||
{
|
||||
proof* pp = m.get_parent(p, i);
|
||||
datalog::set_union(*parent_hyps, *m_parent_hyps.find(pp));
|
||||
set_union(*parent_hyps, *m_parent_hyps.find(pp));
|
||||
|
||||
if (!m.is_lemma(p)) // lemmas clear all hypotheses
|
||||
{
|
||||
datalog::set_union(*active_hyps, *m_active_hyps.find(pp));
|
||||
set_union(*active_hyps, *m_active_hyps.find(pp));
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -488,7 +439,7 @@ proof* ProofIteratorPostOrder::next()
|
|||
expr_set* all_hyps = m_parent_hyps.find(pr);
|
||||
SASSERT(all_hyps != nullptr);
|
||||
|
||||
ProofIteratorPostOrder pit(pr, m);
|
||||
proof_post_order pit(pr, m);
|
||||
while (pit.hasNext()) {
|
||||
proof* p = pit.next();
|
||||
if (!m.is_hypothesis(p))
|
||||
|
|
|
|||
|
|
@ -21,24 +21,9 @@ Revision History:
|
|||
#include "ast/ast.h"
|
||||
|
||||
namespace spacer {
|
||||
|
||||
|
||||
bool is_arith_lemma(ast_manager& m, proof* pr);
|
||||
bool is_farkas_lemma(ast_manager& m, proof* pr);
|
||||
/*
|
||||
* iterator, which traverses the proof in depth-first post-order.
|
||||
*/
|
||||
class ProofIteratorPostOrder {
|
||||
public:
|
||||
ProofIteratorPostOrder(proof* refutation, ast_manager& manager);
|
||||
bool hasNext();
|
||||
proof* next();
|
||||
|
||||
private:
|
||||
ptr_vector<proof> m_todo;
|
||||
ast_mark m_visited; // the proof nodes we have already visited
|
||||
|
||||
ast_manager& m;
|
||||
};
|
||||
|
||||
/*
|
||||
* prints the proof pr in dot representation to the file proof.dot
|
||||
|
|
@ -46,7 +31,7 @@ private:
|
|||
*/
|
||||
class iuc_proof;
|
||||
void pp_proof_dot(ast_manager& m, proof* pr, iuc_proof* iuc_pr = nullptr);
|
||||
|
||||
|
||||
class theory_axiom_reducer
|
||||
{
|
||||
public:
|
||||
|
|
@ -54,16 +39,16 @@ private:
|
|||
|
||||
// reduce theory axioms and return transformed proof
|
||||
proof_ref reduce(proof* pr);
|
||||
|
||||
|
||||
private:
|
||||
ast_manager &m;
|
||||
|
||||
|
||||
// tracking all created expressions
|
||||
expr_ref_vector m_pinned;
|
||||
|
||||
|
||||
// maps each proof of a clause to the transformed subproof of that clause
|
||||
obj_map<proof, proof*> m_cache;
|
||||
|
||||
|
||||
void reset();
|
||||
};
|
||||
|
||||
|
|
@ -71,7 +56,7 @@ private:
|
|||
{
|
||||
public:
|
||||
hypothesis_reducer(ast_manager &m) : m(m), m_pinned(m) {}
|
||||
|
||||
|
||||
// reduce hypothesis and return transformed proof
|
||||
proof_ref reduce(proof* pf);
|
||||
|
||||
|
|
@ -80,7 +65,7 @@ private:
|
|||
typedef obj_hashtable<proof> proof_set;
|
||||
|
||||
ast_manager &m;
|
||||
|
||||
|
||||
expr_ref_vector m_pinned; // tracking all created expressions
|
||||
ptr_vector<proof_set> m_pinned_active_hyps; // tracking all created sets of active hypothesis
|
||||
ptr_vector<expr_set> m_pinned_parent_hyps; // tracking all created sets of parent hypothesis
|
||||
|
|
@ -89,12 +74,12 @@ private:
|
|||
obj_map<expr, proof*> m_units; // maps each unit literal to the subproof of that unit
|
||||
obj_map<proof, proof_set*> m_active_hyps; // maps each proof of a clause to the set of proofs of active hypothesis' of the clause
|
||||
obj_map<proof, expr_set*> m_parent_hyps; // maps each proof of a clause to the hypothesis-fact, which are transitive parents of that clause, needed to avoid creating cycles in the proof.
|
||||
|
||||
|
||||
void reset();
|
||||
void compute_hypsets(proof* pr); // compute active_hyps and parent_hyps for pr
|
||||
void collect_units(proof* pr); // compute m_units
|
||||
proof* compute_transformed_proof(proof* pf);
|
||||
|
||||
|
||||
proof* mk_lemma_core(proof *pf, expr *fact);
|
||||
proof* mk_unit_resolution_core(ptr_buffer<proof>& args);
|
||||
proof* mk_step_core(proof* old_step, ptr_buffer<proof>& args);
|
||||
|
|
|
|||
|
|
@ -22,6 +22,7 @@ Revision History:
|
|||
#include "muz/spacer/spacer_iuc_proof.h"
|
||||
#include "ast/for_each_expr.h"
|
||||
|
||||
#include "ast/proofs/proof_utils.h"
|
||||
#include "muz/spacer/spacer_util.h"
|
||||
|
||||
|
||||
|
|
@ -54,7 +55,7 @@ void unsat_core_learner::compute_unsat_core(expr_ref_vector& unsat_core)
|
|||
{
|
||||
SASSERT(m.is_proof(currentNode->get_arg(i)));
|
||||
proof* premise = to_app(currentNode->get_arg(i));
|
||||
|
||||
|
||||
need_to_mark_closed = need_to_mark_closed && (!m_pr.is_b_marked(premise) || m_closed.is_marked(premise));
|
||||
}
|
||||
|
||||
|
|
@ -109,7 +110,7 @@ void unsat_core_learner::set_closed(proof* p, bool value)
|
|||
{
|
||||
m_closed.mark(p, value);
|
||||
}
|
||||
|
||||
|
||||
bool unsat_core_learner::is_b_open(proof *p)
|
||||
{
|
||||
return m_pr.is_b_marked(p) && !is_closed (p);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue