mirror of
https://github.com/Z3Prover/z3
synced 2026-02-21 07:54:42 +00:00
Lattice based refutation (#8211)
* add examples * add lattice refutation solver class * store partial order in vector * capture partial order relations * begin with the incremental reachability data structure * implement data structure for incremental reachability * fix bug in subset propagation * add trace * only propagate if new value was added * begin implementing bitvector variant of reachability matrix * fix path creation and cycle detection * fix bug * make conflict triggering more conservative * check if theory vars are in bounds * add cycle detection (including equality propagation) * add examples * remove example * remove traces * remove sln file
This commit is contained in:
lorenzwinkler1
GitHub
parent
ec3aafd51e
commit
31cbb4b144
10 changed files with 789 additions and 2 deletions
|
|
@ -59,6 +59,7 @@ z3_add_component(smt
|
|||
theory_dense_diff_logic.cpp
|
||||
theory_finite_set.cpp
|
||||
theory_finite_set_size.cpp
|
||||
theory_finite_set_lattice_refutation.cpp
|
||||
theory_diff_logic.cpp
|
||||
theory_dl.cpp
|
||||
theory_dummy.cpp
|
||||
|
|
|
|||
|
|
@ -28,7 +28,8 @@ namespace smt {
|
|||
theory(ctx, ctx.get_manager().mk_family_id("finite_set")),
|
||||
u(m),
|
||||
m_axioms(m), m_rw(m), m_find(*this),
|
||||
m_cardinality_solver(*this)
|
||||
m_cardinality_solver(*this),
|
||||
m_lattice_refutation(*this)
|
||||
{
|
||||
// Setup the add_clause callback for axioms
|
||||
std::function<void(theory_axiom *)> add_clause_fn =
|
||||
|
|
@ -227,8 +228,11 @@ namespace smt {
|
|||
e = ctx.mk_enode(term, false, m.is_bool(term), true);
|
||||
|
||||
// Attach theory variable if this is a set
|
||||
if (!is_attached_to_var(e))
|
||||
if (!is_attached_to_var(e)){
|
||||
ctx.attach_th_var(e, this, mk_var(e));
|
||||
TRACE(finite_set, tout << "create_theory_var: " << e->get_th_var(get_id()) << " enode:" << e->get_expr() << "\n";);
|
||||
}
|
||||
|
||||
|
||||
// Assert immediate axioms
|
||||
if (!ctx.relevancy())
|
||||
|
|
@ -256,6 +260,10 @@ namespace smt {
|
|||
ctx.push_trail(push_back_vector(m_eqs));
|
||||
m_find.merge(v1, v2); // triggers merge_eh, which triggers incremental generation of theory axioms
|
||||
}
|
||||
m_lattice_refutation.add_equality(v1, v2);
|
||||
|
||||
// Check if Z3 has a boolean variable for it
|
||||
TRACE(finite_set, tout << "new_eq_eh_r1: " << n1->get_root() << "r2: "<< n2->get_root() <<"\n";);
|
||||
}
|
||||
|
||||
/**
|
||||
|
|
@ -279,6 +287,7 @@ namespace smt {
|
|||
ctx.push_trail(push_back_vector(m_diseqs));
|
||||
m_axioms.extensionality_axiom(e1, e2);
|
||||
}
|
||||
m_lattice_refutation.add_disequality(v1,v2);
|
||||
}
|
||||
|
||||
//
|
||||
|
|
@ -405,6 +414,8 @@ namespace smt {
|
|||
void theory_finite_set::assign_eh(bool_var v, bool is_true) {
|
||||
TRACE(finite_set, tout << "assign_eh: v" << v << " is_true: " << is_true << "\n";);
|
||||
expr *e = ctx.bool_var2expr(v);
|
||||
TRACE(finite_set, tout << "assign_eh_expr: " << mk_pp(e, m) << "\n";);
|
||||
|
||||
// retrieve the watch list for clauses where e appears with opposite polarity
|
||||
unsigned idx = 2 * e->get_id() + (is_true ? 1 : 0);
|
||||
if (idx >= m_clauses.watch.size())
|
||||
|
|
|
|||
|
|
@ -87,6 +87,7 @@ the theory solver uses a stand-alone satisfiability checker for Boolean algebras
|
|||
#include "util/union_find.h"
|
||||
#include "smt/smt_theory.h"
|
||||
#include "smt/theory_finite_set_size.h"
|
||||
#include "smt/theory_finite_set_lattice_refutation.h"
|
||||
#include "model/finite_set_factory.h"
|
||||
|
||||
namespace smt {
|
||||
|
|
@ -96,6 +97,7 @@ namespace smt {
|
|||
using th_union_find = union_find<theory_finite_set>;
|
||||
friend class theory_finite_set_test;
|
||||
friend class theory_finite_set_size;
|
||||
friend class theory_finite_set_lattice_refutation;
|
||||
friend struct finite_set_value_proc;
|
||||
|
||||
struct var_data {
|
||||
|
|
@ -139,6 +141,7 @@ namespace smt {
|
|||
th_union_find m_find;
|
||||
theory_clauses m_clauses;
|
||||
theory_finite_set_size m_cardinality_solver;
|
||||
theory_finite_set_lattice_refutation m_lattice_refutation;
|
||||
finite_set_factory *m_factory = nullptr;
|
||||
obj_map<enode, obj_map<enode, bool> *> m_set_members;
|
||||
ptr_vector<func_decl> m_set_in_decls;
|
||||
|
|
|
|||
307
src/smt/theory_finite_set_lattice_refutation.cpp
Normal file
307
src/smt/theory_finite_set_lattice_refutation.cpp
Normal file
|
|
@ -0,0 +1,307 @@
|
|||
#include "smt/theory_finite_set_lattice_refutation.h"
|
||||
#include "ast/rewriter/finite_set_axioms.h"
|
||||
#include "smt/smt_theory.h"
|
||||
#include "smt/theory_finite_set.h"
|
||||
#include "smt/smt_context.h"
|
||||
#include "iostream"
|
||||
|
||||
const int NUM_WORDS = 5;
|
||||
// some example have shown, the introduction of large conflict clauses can severely slow down refutation
|
||||
const int MAX_DECISION_LITERALS=10;
|
||||
|
||||
namespace smt {
|
||||
reachability_matrix::reachability_matrix(context& ctx, theory_finite_set_lattice_refutation& t_lattice):
|
||||
reachable(NUM_WORDS*NUM_WORDS*64, 0),
|
||||
links(NUM_WORDS*NUM_WORDS*64*64, {nullptr, nullptr}),
|
||||
link_dls(NUM_WORDS*NUM_WORDS*64*64, 0),
|
||||
non_links(NUM_WORDS*NUM_WORDS*64),
|
||||
non_link_justifications(NUM_WORDS*NUM_WORDS*64*64, {nullptr, nullptr}), largest_var(0), max_size(NUM_WORDS*64), ctx(ctx), t_lattice_refutation(t_lattice) {}
|
||||
|
||||
int reachability_matrix::get_max_var(){
|
||||
return largest_var;
|
||||
}
|
||||
|
||||
inline int reachability_matrix::get_word_index(int row, int col) const{
|
||||
return (row * NUM_WORDS) + (col / 64);
|
||||
};
|
||||
|
||||
inline uint64_t reachability_matrix::get_bitmask(int col) const{
|
||||
return 1ull << (col%64);
|
||||
};
|
||||
|
||||
bool reachability_matrix::is_reachability_forbidden(theory_var source, theory_var dest){
|
||||
return non_links[get_word_index(source, dest)] & get_bitmask(dest);
|
||||
}
|
||||
|
||||
bool reachability_matrix::in_bounds(theory_var source, theory_var dest){
|
||||
return source >= 0 && dest >= 0 && source < max_size && dest<max_size;
|
||||
}
|
||||
|
||||
bool reachability_matrix::is_reachable(theory_var source, theory_var dest){
|
||||
return reachable[get_word_index(source,dest)] & get_bitmask(dest);
|
||||
}
|
||||
|
||||
bool reachability_matrix::is_linked(theory_var source, theory_var dest){
|
||||
return links[source*max_size+dest].first != nullptr;
|
||||
}
|
||||
|
||||
bool reachability_matrix::bitwise_or_rows(int source_dest, int source){
|
||||
bool changes = false;
|
||||
for (int i = 0; i < NUM_WORDS; i++)
|
||||
{
|
||||
uint64_t old_value = reachable[source_dest*NUM_WORDS+i];
|
||||
uint64_t new_value = reachable[source_dest*NUM_WORDS+i] | reachable[source*NUM_WORDS+i];
|
||||
if(old_value == new_value){
|
||||
continue;
|
||||
}
|
||||
ctx.push_trail(value_trail(reachable[source_dest*NUM_WORDS+i]));
|
||||
reachable[source_dest*NUM_WORDS+i] = new_value;
|
||||
changes = true;
|
||||
check_reachability_conflict_word(source_dest, i);
|
||||
}
|
||||
return changes;
|
||||
}
|
||||
|
||||
bool reachability_matrix::set_reachability(theory_var source, theory_var dest, enode_pair reachability_witness){
|
||||
if (!in_bounds(source, dest) || is_reachable(source, dest)){
|
||||
return false;
|
||||
}
|
||||
ctx.push_trail(value_trail(largest_var));
|
||||
largest_var = std::max({largest_var, source, dest});
|
||||
|
||||
int word_idx = get_word_index(source, dest);
|
||||
ctx.push_trail(value_trail(reachable[word_idx]));
|
||||
reachable[word_idx] |= get_bitmask(dest);
|
||||
ctx.push_trail(value_trail(links[source*max_size + dest]));
|
||||
links[source*max_size+dest] = reachability_witness;
|
||||
ctx.push_trail(value_trail(link_dls[source*max_size+dest]));
|
||||
TRACE(finite_set, tout << "set_reachability(" << source << "," << dest <<"), dl: "<<ctx.get_scope_level());
|
||||
link_dls[source*max_size+dest] = ctx.get_scope_level();
|
||||
|
||||
check_reachability_conflict(source, dest);
|
||||
// update reachability of source
|
||||
bitwise_or_rows(source, dest);
|
||||
|
||||
|
||||
for (int i = 0; i <= largest_var; i++)
|
||||
{ //update reachability of i to the nodes reachable from dest
|
||||
if(!is_reachable(i, source) || i == source){
|
||||
continue;
|
||||
}
|
||||
bitwise_or_rows(i, source);
|
||||
}
|
||||
if(conflict_word>=0 && conflict_row >=0){
|
||||
for (int i = conflict_word*64; i < conflict_word*64+64; i++)
|
||||
{
|
||||
check_reachability_conflict(conflict_row, i);
|
||||
}
|
||||
conflict_word = -1;
|
||||
conflict_row = -1;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool reachability_matrix::set_non_reachability(theory_var source, theory_var dest, enode_pair non_reachability_witness){
|
||||
if(is_reachability_forbidden(source, dest)){
|
||||
return false;
|
||||
}
|
||||
ctx.push_trail(value_trail(largest_var));
|
||||
largest_var = std::max({largest_var, source, dest});
|
||||
ctx.push_trail(value_trail(non_links[get_word_index(source, dest)]));
|
||||
non_links[get_word_index(source, dest)] |= get_bitmask(dest);
|
||||
ctx.push_trail(value_trail(non_link_justifications[source*max_size+dest]));
|
||||
non_link_justifications[source*max_size+dest] = non_reachability_witness;
|
||||
check_reachability_conflict(source, dest);
|
||||
return true;
|
||||
}
|
||||
|
||||
theory_finite_set_lattice_refutation::theory_finite_set_lattice_refutation(theory_finite_set& th):
|
||||
m(th.m), ctx(th.ctx), th(th), u(m), bs(m), m_assumption(m), reachability(th.ctx, *this) {}
|
||||
|
||||
// determines if the two enodes capture a subset relation:
|
||||
// checks, whether intersect_expr = intersect(subset, return_value) for some return value
|
||||
// otherwise return null
|
||||
enode* theory_finite_set_lattice_refutation::get_superset(enode* subset, enode* intersect_expr){
|
||||
expr* arg1 = nullptr, *arg2 = nullptr;
|
||||
if(u.is_intersect(intersect_expr->get_expr(), arg1, arg2)){
|
||||
if(arg1 == subset->get_expr()){
|
||||
return ctx.get_enode(arg2);
|
||||
}
|
||||
if(arg2 == subset->get_expr()){
|
||||
return ctx.get_enode(arg1);
|
||||
}
|
||||
}
|
||||
return nullptr;
|
||||
}
|
||||
|
||||
void theory_finite_set_lattice_refutation::add_equality(theory_var v1, theory_var v2){
|
||||
auto n1 = th.get_enode(v1);
|
||||
auto n2 = th.get_enode(v2);
|
||||
|
||||
enode* subset = n1;
|
||||
enode* superset = get_superset(n1, n2);
|
||||
if(superset == nullptr){
|
||||
subset = n2;
|
||||
superset = get_superset(n2, n1);
|
||||
}
|
||||
if(superset == nullptr){
|
||||
add_set_equality(n1, n2);
|
||||
return;
|
||||
}
|
||||
TRACE(finite_set, tout << "new_eq_intersection: " << enode_pp(subset, ctx) << "("<<th.get_th_var(subset)<<")" << "\\subseteq " << enode_pp(superset, ctx)<<"("<<th.get_th_var(superset)<<")");
|
||||
add_subset(subset->get_th_var(th.get_id()), superset->get_th_var(th.get_id()), {n1, n2});
|
||||
};
|
||||
|
||||
void reachability_matrix::get_path(theory_var source, theory_var dest, vector<enode_pair>& path, int& num_decisions){
|
||||
SASSERT(is_reachable(source, dest));
|
||||
vector<bool> visited(max_size, false);
|
||||
if(source != dest){
|
||||
visited[source] = true;
|
||||
}
|
||||
num_decisions = 0;
|
||||
do{
|
||||
bool success = false;
|
||||
// TRACE(finite_set, tout << "get_path:source: "<<source);
|
||||
for (int i = 0; i <= largest_var; i++)
|
||||
{
|
||||
if(!visited[i] && is_linked(source, i) && ((is_reachable(i, dest)) || i == dest)){
|
||||
path.push_back(links[source*max_size+i]);
|
||||
if(link_dls[source*max_size+i] != 0){
|
||||
num_decisions +=1;
|
||||
}
|
||||
|
||||
source = i;
|
||||
visited[source] = true;
|
||||
success = true;
|
||||
break;
|
||||
}
|
||||
}
|
||||
SASSERT(success);
|
||||
}while(source != dest);
|
||||
TRACE(finite_set, tout << "get_path_num_decisions: "<<num_decisions);
|
||||
}
|
||||
|
||||
bool reachability_matrix::check_reachability_conflict(theory_var source, theory_var dest){
|
||||
if(is_reachable(source,dest) && is_reachability_forbidden(source, dest)){
|
||||
TRACE(finite_set, tout << "found_conflict1: "<<source<<" -> "<<dest);
|
||||
vector<enode_pair> path;
|
||||
int num_decisions;
|
||||
get_path(source, dest, path, num_decisions);
|
||||
// TRACE(finite_set, tout << "found path: "<<source<<" -> "<<dest<<" length: "<<path.size());
|
||||
if(num_decisions <= MAX_DECISION_LITERALS){
|
||||
TRACE(finite_set, tout << "num_decisions: "<<num_decisions<<" path_length: "<<path.size());
|
||||
|
||||
enode_pair diseq = non_link_justifications[source*max_size+dest];
|
||||
t_lattice_refutation.trigger_conflict(path, diseq);
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
bool reachability_matrix::check_reachability_conflict_word(int row, int word){
|
||||
if(reachable[row*NUM_WORDS+word] & non_links[row*NUM_WORDS+word]){
|
||||
|
||||
// somewhere in this word there is a conflict
|
||||
conflict_row = row;
|
||||
conflict_word = word;
|
||||
return true;
|
||||
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
void reachability_matrix::print_relations(){
|
||||
TRACE(finite_set, tout << "largest_var: "<<largest_var);
|
||||
for (size_t i = 0; i < max_size; i++)
|
||||
{
|
||||
for (size_t j = 0; j < max_size; j++)
|
||||
{
|
||||
if((reachable[get_word_index(i,j)]&get_bitmask(j)) || is_reachable(i,j)){
|
||||
TRACE(finite_set, tout << "reachable: "<<i<<"->"<<j<<" :"<<is_reachable(i,j));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void theory_finite_set_lattice_refutation::trigger_conflict(vector<enode_pair> equalities, enode_pair clashing_disequality){
|
||||
auto eq_expr = m.mk_not(m.mk_eq(clashing_disequality.first->get_expr(), clashing_disequality.second->get_expr()));
|
||||
auto disequality_literal = ctx.get_literal(eq_expr);
|
||||
auto j1 = ext_theory_conflict_justification(th.get_id(), ctx, 1, &disequality_literal, equalities.size(), equalities.data());
|
||||
auto justification = ctx.mk_justification(j1);
|
||||
TRACE(finite_set, tout << "conflict_literal: "<<disequality_literal);
|
||||
|
||||
TRACE(finite_set, tout << "setting_partial_order_conflict");
|
||||
ctx.set_conflict(justification);
|
||||
}
|
||||
|
||||
void theory_finite_set_lattice_refutation::add_disequality(theory_var v1, theory_var v2){
|
||||
auto n1 = th.get_enode(v1);
|
||||
auto n2 = th.get_enode(v2);
|
||||
|
||||
enode* subset = n1;
|
||||
enode* superset = get_superset(n1, n2);
|
||||
if(superset == nullptr){
|
||||
subset = n2;
|
||||
superset = get_superset(n2, n1);
|
||||
}
|
||||
if(superset == nullptr){
|
||||
return;
|
||||
}
|
||||
TRACE(finite_set, tout << "new_diseq_intersection: " << enode_pp(subset, ctx) << "("<<th.get_th_var(subset)<<")" << "\\not\\subseteq " << enode_pp(superset, ctx)<<"("<<th.get_th_var(superset)<<")");
|
||||
add_not_subset(subset->get_th_var(th.get_id()), superset->get_th_var(th.get_id()), {n1, n2});
|
||||
};
|
||||
|
||||
void theory_finite_set_lattice_refutation::add_subset(theory_var subset_th, theory_var superset_th, enode_pair justifying_equality){
|
||||
if(!reachability.in_bounds(subset_th, superset_th)){
|
||||
return;
|
||||
}
|
||||
if (subset_th == null_theory_var || superset_th == null_theory_var){
|
||||
return;
|
||||
}
|
||||
reachability.set_reachability(subset_th, superset_th, justifying_equality);
|
||||
SASSERT(reachability.is_reachable(subset_th, superset_th));
|
||||
if(reachability.is_reachable(superset_th, subset_th)){
|
||||
TRACE(finite_set, tout << "cycle_detected: " << subset_th << " <--> " << superset_th);
|
||||
vector<enode_pair> path;
|
||||
int num_decisions;
|
||||
reachability.get_path(subset_th, subset_th, path, num_decisions);
|
||||
// we propagate the equality
|
||||
// build justification to be used by all propagated equalities
|
||||
auto j1 = ctx.mk_justification(ext_theory_conflict_justification(th.get_id(), ctx, 0, nullptr, path.size(), path.data()));
|
||||
|
||||
for (size_t i = 0; i < path.size()-1; i++)
|
||||
{
|
||||
auto set1 = path[i].first;
|
||||
auto set2 = path[i+1].first;
|
||||
ctx.add_eq(set1, set2, eq_justification(j1));
|
||||
TRACE(finite_set, tout << "added_equality: " << set1 << " == " << set2);
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
void theory_finite_set_lattice_refutation::add_not_subset(theory_var subset_th, theory_var superset_th, enode_pair justifying_disequality){
|
||||
if(!reachability.in_bounds(subset_th, superset_th)){
|
||||
return;
|
||||
}
|
||||
if (subset_th == null_theory_var || superset_th == null_theory_var){
|
||||
return;
|
||||
}
|
||||
reachability.set_non_reachability(subset_th, superset_th, justifying_disequality);
|
||||
SASSERT(reachability.is_reachability_forbidden(subset_th, superset_th));
|
||||
}
|
||||
|
||||
void theory_finite_set_lattice_refutation::add_set_equality(enode* set1, enode* set2){
|
||||
theory_var set1_th = set1->get_th_var(th.get_id());
|
||||
theory_var set2_th = set2->get_th_var(th.get_id());
|
||||
if(!reachability.in_bounds(set1_th, set2_th)){
|
||||
return;
|
||||
}
|
||||
reachability.set_reachability(set1_th, set2_th, {set1, set2});
|
||||
SASSERT(reachability.is_reachable(set1_th, set2_th));
|
||||
|
||||
reachability.set_reachability(set2_th, set1_th, {set2, set1});
|
||||
SASSERT(reachability.is_reachable(set2_th, set1_th));
|
||||
}
|
||||
}
|
||||
71
src/smt/theory_finite_set_lattice_refutation.h
Normal file
71
src/smt/theory_finite_set_lattice_refutation.h
Normal file
|
|
@ -0,0 +1,71 @@
|
|||
#pragma once
|
||||
|
||||
#include "ast/finite_set_decl_plugin.h"
|
||||
#include "ast/rewriter/finite_set_axioms.h"
|
||||
#include "smt/smt_theory.h"
|
||||
|
||||
namespace smt {
|
||||
class context;
|
||||
class theory_finite_set;
|
||||
|
||||
class theory_finite_set_lattice_refutation;
|
||||
class reachability_matrix{
|
||||
|
||||
std::vector<uint64_t> reachable;
|
||||
std::vector<enode_pair> links;
|
||||
std::vector<uint64_t> link_dls;
|
||||
std::vector<uint64_t> non_links;
|
||||
std::vector<enode_pair> non_link_justifications;
|
||||
|
||||
int largest_var;
|
||||
|
||||
int max_size;
|
||||
|
||||
context& ctx;
|
||||
theory_finite_set_lattice_refutation& t_lattice_refutation;
|
||||
int conflict_row = -1;
|
||||
int conflict_word = -1;
|
||||
|
||||
// sets source_dest |= dest, and pushing the changed words to the trail
|
||||
bool bitwise_or_rows(int source_dest, int source);
|
||||
inline int get_word_index(int row, int col) const;
|
||||
inline uint64_t get_bitmask(int col) const;
|
||||
public:
|
||||
void get_path(theory_var source, theory_var dest, vector<enode_pair>& path, int& num_decisions);
|
||||
reachability_matrix(context& ctx, theory_finite_set_lattice_refutation& t_lattice);
|
||||
bool in_bounds(theory_var source, theory_var dest);
|
||||
bool is_reachable(theory_var source, theory_var dest);
|
||||
bool is_reachability_forbidden(theory_var source, theory_var dest);
|
||||
bool is_linked(theory_var source, theory_var dest);
|
||||
|
||||
bool check_reachability_conflict(theory_var source, theory_var dest);
|
||||
bool check_reachability_conflict_word(int row, int word);
|
||||
|
||||
bool set_reachability(theory_var source, theory_var dest, enode_pair reachability_witness);
|
||||
bool set_non_reachability(theory_var source, theory_var dest, enode_pair non_reachability_witness);
|
||||
int get_max_var();
|
||||
void print_relations();
|
||||
|
||||
};
|
||||
|
||||
class theory_finite_set_lattice_refutation {
|
||||
ast_manager &m;
|
||||
context &ctx;
|
||||
theory_finite_set &th;
|
||||
finite_set_util u;
|
||||
expr_ref_vector bs;
|
||||
expr_ref m_assumption;
|
||||
reachability_matrix reachability;
|
||||
|
||||
enode* get_superset(enode*, enode*);
|
||||
void add_subset(theory_var subset, theory_var superset, enode_pair justifying_equality);
|
||||
void add_not_subset(theory_var subset, theory_var superset, enode_pair justifying_disequality);
|
||||
void propagate_new_subset(theory_var v1, theory_var v2);
|
||||
void add_set_equality(enode* set1, enode* set2);
|
||||
public:
|
||||
void trigger_conflict(vector<enode_pair> equalities, enode_pair clashing_disequality);
|
||||
theory_finite_set_lattice_refutation(theory_finite_set &th);
|
||||
void add_equality(theory_var v1, theory_var v2);
|
||||
void add_disequality(theory_var v1, theory_var v2);
|
||||
};
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue