mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
missing new files
This commit is contained in:
parent
0ce1c34d81
commit
a66362a933
92
src/ast/rewriter/seq_eq_solver.cpp
Normal file
92
src/ast/rewriter/seq_eq_solver.cpp
Normal file
|
@ -0,0 +1,92 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
seq_eq_solver
|
||||
|
||||
Abstract:
|
||||
|
||||
Solver-agnostic equality solving routines for sequences
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-01
|
||||
|
||||
--*/
|
||||
|
||||
#include "ast/rewriter/seq_eq_solver.h"
|
||||
|
||||
namespace seq {
|
||||
|
||||
|
||||
bool eq_solver::solve(eq const& e, eq_ptr& r) {
|
||||
if (solve_itos1(e, r))
|
||||
return true;
|
||||
if (solve_itos2(e, r))
|
||||
return true;
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
void eq_solver::add_consequence(expr_ref const& a) {
|
||||
m_clause.reset();
|
||||
m_clause.push_back(a);
|
||||
m_add_consequence(true, m_clause);
|
||||
}
|
||||
|
||||
void eq_solver::add_consequence(expr_ref const& a, expr_ref const& b) {
|
||||
m_clause.reset();
|
||||
m_clause.push_back(a);
|
||||
m_clause.push_back(b);
|
||||
m_add_consequence(true, m_clause);
|
||||
}
|
||||
|
||||
/**
|
||||
* from_int(s) == from_int(t)
|
||||
* --------------------------
|
||||
* s = t or (s < 0 and t < 0)
|
||||
*/
|
||||
|
||||
bool eq_solver::match_itos1(eq const& e, expr*& a, expr*& b) {
|
||||
return
|
||||
e.ls.size() == 1 && e.rs.size() == 1 &&
|
||||
seq.str.is_itos(e.ls[0], a) && seq.str.is_itos(e.rs[0], b);
|
||||
}
|
||||
|
||||
bool eq_solver::solve_itos1(eq const& e, eq_ptr& r) {
|
||||
expr* s = nullptr, *t = nullptr;
|
||||
if (!match_itos1(e, s, t))
|
||||
return false;
|
||||
r = nullptr;
|
||||
expr_ref eq = mk_eq(s, t);
|
||||
add_consequence(eq, mk_le(s, -1));
|
||||
add_consequence(eq, mk_le(t, -1));
|
||||
return true;
|
||||
}
|
||||
|
||||
/**
|
||||
* from_int(s) == ""
|
||||
* -----------------
|
||||
* s < 0
|
||||
*/
|
||||
|
||||
bool eq_solver::match_itos2(eq const& e, expr*& s) {
|
||||
if (e.ls.size() == 1 && e.rs.empty() && seq.str.is_itos(e.ls[0], s))
|
||||
return true;
|
||||
if (e.rs.size() == 1 && e.ls.empty() && seq.str.is_itos(e.rs[0], s))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
bool eq_solver::solve_itos2(eq const& e, eq_ptr& r) {
|
||||
expr* s = nullptr;
|
||||
if (!match_itos2(e, s))
|
||||
return false;
|
||||
r = nullptr;
|
||||
add_consequence(mk_le(s, -1));
|
||||
return true;
|
||||
}
|
||||
|
||||
};
|
||||
|
75
src/ast/rewriter/seq_eq_solver.h
Normal file
75
src/ast/rewriter/seq_eq_solver.h
Normal file
|
@ -0,0 +1,75 @@
|
|||
/*++
|
||||
Copyright (c) 2011 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
seq_eq_solver
|
||||
|
||||
Abstract:
|
||||
|
||||
Solver-agnostic equality solving routines for sequences
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2021-03-01
|
||||
|
||||
--*/
|
||||
#pragma once
|
||||
|
||||
#include "ast/rewriter/seq_axioms.h"
|
||||
|
||||
namespace seq {
|
||||
|
||||
struct eq {
|
||||
expr_ref_vector ls;
|
||||
expr_ref_vector rs;
|
||||
eq(expr_ref_vector& l, expr_ref_vector& r):
|
||||
ls(l), rs(r) {}
|
||||
};
|
||||
|
||||
typedef scoped_ptr<eq> eq_ptr;
|
||||
|
||||
class eq_solver {
|
||||
ast_manager& m;
|
||||
axioms& m_ax;
|
||||
seq_util seq;
|
||||
expr_ref_vector m_clause;
|
||||
std::function<expr*(expr*)> m_value;
|
||||
std::function<bool(expr*, rational&)> m_int_value;
|
||||
std::function<void(bool, expr_ref_vector const&)> m_add_consequence;
|
||||
|
||||
bool match_itos1(eq const& e, expr*& s, expr*& t);
|
||||
bool solve_itos1(eq const& e, eq_ptr& r);
|
||||
|
||||
bool match_itos2(eq const& e, expr*& s);
|
||||
bool solve_itos2(eq const& e, eq_ptr& r);
|
||||
|
||||
void add_consequence(expr_ref const& a);
|
||||
void add_consequence(expr_ref const& a, expr_ref const& b);
|
||||
|
||||
expr_ref mk_eq(expr* a, expr* b) { return expr_ref(m.mk_eq(a, b), m); }
|
||||
expr_ref mk_ge(expr* x, int n) { return m_ax.mk_ge(x, n); }
|
||||
expr_ref mk_le(expr* x, int n) { return m_ax.mk_le(x, n); }
|
||||
expr_ref mk_ge(expr* x, rational const& n) { return m_ax.mk_ge(x, n); }
|
||||
expr_ref mk_le(expr* x, rational const& n) { return m_ax.mk_le(x, n); }
|
||||
|
||||
public:
|
||||
|
||||
eq_solver(ast_manager& m, axioms& ax):
|
||||
m(m),
|
||||
m_ax(ax),
|
||||
seq(m),
|
||||
m_clause(m)
|
||||
{}
|
||||
|
||||
void set_value(std::function<expr*(expr*)>& v) { m_value = v; }
|
||||
void set_int_value(std::function<bool(expr*,rational&)>& iv) { m_int_value = iv; }
|
||||
void set_add_consequence(std::function<void(bool, expr_ref_vector const&)>& ac) { m_add_consequence = ac; }
|
||||
|
||||
bool solve(eq const& e, eq_ptr& r);
|
||||
|
||||
|
||||
};
|
||||
|
||||
};
|
||||
|
Loading…
Reference in a new issue