mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

remove internal configuration

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-05-28 12:13:18 -07:00
parent dd46224a1d
commit 8d980ea704
3 changed files with 2 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
doc/mk_api_doc.py
View file

@ -11,7 +11,6 @@ import getopt
import pydoc import pydoc
import sys import sys
import subprocess import subprocess
import shutil
ML_ENABLED=False ML_ENABLED=False
MLD_ENABLED=False MLD_ENABLED=False

21
src/ast/rewriter/bv_rewriter.cpp
View file

@ -33,7 +33,6 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
m_split_concat_eq = p.split_concat_eq(); m_split_concat_eq = p.split_concat_eq();
m_bvnot_simpl = p.bv_not_simpl(); m_bvnot_simpl = p.bv_not_simpl();
m_bv_sort_ac = p.bv_sort_ac(); m_bv_sort_ac = p.bv_sort_ac();
m_mkbv2num = _p.get_bool("mkbv2num", false);
m_extract_prop = p.bv_extract_prop(); m_extract_prop = p.bv_extract_prop();
m_ite2id = p.bv_ite2id(); m_ite2id = p.bv_ite2id();
m_le_extra = p.bv_le_extra(); m_le_extra = p.bv_le_extra();
@ -49,9 +48,6 @@ void bv_rewriter::updt_params(params_ref const & p) {
void bv_rewriter::get_param_descrs(param_descrs & r) { void bv_rewriter::get_param_descrs(param_descrs & r) {
poly_rewriter<bv_rewriter_core>::get_param_descrs(r); poly_rewriter<bv_rewriter_core>::get_param_descrs(r);
bv_rewriter_params::collect_param_descrs(r); bv_rewriter_params::collect_param_descrs(r);
#ifndef _EXTERNAL_RELEASE
r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral");
#endif
} }
br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
@ -2723,23 +2719,6 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & result) { br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & result) {
if (m_mkbv2num) {
unsigned i;
for (i = 0; i < num; i++)
if (!m().is_true(args[i]) && !m().is_false(args[i]))
return BR_FAILED;
numeral val;
numeral two(2);
i = num;
while (i > 0) {
--i;
val *= two;
if (m().is_true(args[i]))
val++;
}
result = mk_numeral(val, num);
return BR_DONE;
}
return BR_FAILED; return BR_FAILED;
} }

4
src/ast/rewriter/bv_rewriter.h
View file

@ -55,7 +55,6 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
bool m_mul2concat; bool m_mul2concat;
bool m_bit2bool; bool m_bit2bool;
bool m_blast_eq_value; bool m_blast_eq_value;
bool m_mkbv2num;
bool m_ite2id; bool m_ite2id;
bool m_split_concat_eq; bool m_split_concat_eq;
bool m_bv_sort_ac; bool m_bv_sort_ac;
@ -63,7 +62,8 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
bool m_bvnot_simpl; bool m_bvnot_simpl;
bool m_le_extra; bool m_le_extra;
bool m_le2extract; bool m_le2extract;
bool m_mkbv2num = false;
bool is_zero_bit(expr * x, unsigned idx); bool is_zero_bit(expr * x, unsigned idx);
br_status mk_ule(expr * a, expr * b, expr_ref & result); br_status mk_ule(expr * a, expr * b, expr_ref & result);