mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

fix #4028

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-19 23:10:00 -07:00
parent ad8eb8fdcb
commit c8b9eba069
3 changed files with 18 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/smt/seq_axioms.cpp
View file

@ -667,12 +667,19 @@ void seq_axioms::ensure_digit_axiom() {
/**
e1 < e2 => prefix(e1, e2) or e1 = xcy e1 < e2 => prefix(e1, e2) or
c < d e1 < e2 => prefix(e1, e2) or e2 = xdz e1 < e2 => e1 != e2
!(e1 < e2) => prefix(e2, e1) or e2 = xdz !(e1 < e2) => prefix(e2,
e1) or d < c !(e1 < e2) => prefix(e2, e1) or e1 = xcy !(e1 = e2) or
!(e1 < e2) optional: e1 < e2 or e1 = e2 or e2 < e1 !(e1 = e2) or
!(e2 < e1) !(e1 < e2) or !(e2 < e1)
e1 < e2 => prefix(e1, e2) or e1 = xcy
e1 < e2 => prefix(e1, e2) or c < d
e1 < e2 => prefix(e1, e2) or e2 = xdz
e1 < e2 => e1 != e2
!(e1 < e2) => prefix(e2, e1) or e2 = xdz
!(e1 < e2) => prefix(e2, e1) or d < c
!(e1 < e2) => prefix(e2, e1) or e1 = xcy
!(e1 = e2) or !(e1 < e2)
optional:
e1 < e2 or e1 = e2 or e2 < e1
!(e1 = e2) or !(e2 < e1)
!(e1 < e2) or !(e2 < e1)
*/
void seq_axioms::add_lt_axiom(expr* n) {
expr* e1 = nullptr, *e2 = nullptr;

2
src/smt/theory_dense_diff_logic_def.h
View file

@ -41,7 +41,7 @@ namespace smt {
template<typename Ext>
theory* theory_dense_diff_logic<Ext>::mk_fresh(context * new_ctx) {
return alloc(theory_dense_diff_logic<Ext>, new_ctx->get_manager(), m_params);
return alloc(theory_dense_diff_logic<Ext>, new_ctx->get_manager(), new_ctx->get_fparams());
}
template<typename Ext>

6
src/smt/theory_diff_logic_def.h
View file

@ -492,7 +492,7 @@ template<typename Ext>
void theory_diff_logic<Ext>::propagate() {
if (m_params.m_arith_adaptive) {
switch(m_params.m_arith_propagation_strategy) {
switch (m_params.m_arith_propagation_strategy) {
case ARITH_PROP_PROPORTIONAL: {
@ -528,6 +528,8 @@ void theory_diff_logic<Ext>::propagate() {
break;
}
default:
std::cout << m_params.m_arith_propagation_strategy << "\n";
SASSERT(false);
UNREACHABLE();
propagate_core();
}
@ -1416,7 +1418,7 @@ bool theory_diff_logic<Ext>::internalize_objective(expr * n, rational const& m,
template<typename Ext>
theory* theory_diff_logic<Ext>::mk_fresh(context* new_ctx) {
return alloc(theory_diff_logic<Ext>, new_ctx->get_manager(), m_params);
return alloc(theory_diff_logic<Ext>, new_ctx->get_manager(), new_ctx->get_fparams());
}
template<typename Ext>