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

resolve conflicts

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-02 10:38:37 -07:00
commit 19d4b0a97a
27 changed files with 197 additions and 134 deletions
Download patch file Download diff file Expand all files Collapse all files

2
README-CMake.md
View file

@ -1,4 +1,4 @@
# Z3's CMake build system
# Z3's CMake build system
[CMake](https://cmake.org/) is a "meta build system" that reads a description
of the project written in the ``CMakeLists.txt`` files and emits a build

14
src/api/api_ast.cpp
View file

@ -1124,6 +1124,20 @@ extern "C" {
case OP_SEQ_TO_RE: return Z3_OP_SEQ_TO_RE;
case OP_SEQ_IN_RE: return Z3_OP_SEQ_IN_RE;
case _OP_STRING_STRREPL: return Z3_OP_SEQ_REPLACE;
case _OP_STRING_CONCAT: return Z3_OP_SEQ_CONCAT;
case _OP_STRING_LENGTH: return Z3_OP_SEQ_LENGTH;
case _OP_STRING_STRCTN: return Z3_OP_SEQ_CONTAINS;
case _OP_STRING_PREFIX: return Z3_OP_SEQ_PREFIX;
case _OP_STRING_SUFFIX: return Z3_OP_SEQ_SUFFIX;
case _OP_STRING_IN_REGEXP: return Z3_OP_SEQ_IN_RE;
case _OP_STRING_TO_REGEXP: return Z3_OP_SEQ_TO_RE;
case _OP_STRING_CHARAT: return Z3_OP_SEQ_AT;
case _OP_STRING_SUBSTR: return Z3_OP_SEQ_EXTRACT;
case _OP_STRING_STRIDOF: return Z3_OP_SEQ_INDEX;
case _OP_REGEXP_EMPTY: return Z3_OP_RE_EMPTY_SET;
case _OP_REGEXP_FULL: return Z3_OP_RE_FULL_SET;
case OP_STRING_STOI: return Z3_OP_STR_TO_INT;
case OP_STRING_ITOS: return Z3_OP_INT_TO_STR;

16
src/api/dotnet/Expr.cs
View file

@ -797,6 +797,22 @@ namespace Microsoft.Z3
public bool IsLabelLit { get { return IsApp && FuncDecl.DeclKind == Z3_decl_kind.Z3_OP_LABEL_LIT; } }
#endregion
#region Sequences and Strings
/// <summary>
/// Check whether expression is a string constant.
/// </summary>
/// <returns>a Boolean</returns>
public bool IsString { get { return IsApp && 0 != Native.Z3_is_string(Context.nCtx, NativeObject); } }
/// <summary>
/// Retrieve string corresponding to string constant.
/// </summary>
/// <remarks>the expression should be a string constant, (IsString should be true).</remarks>
public string String { get { return Native.Z3_get_string(Context.nCtx, NativeObject); } }
#endregion
#region Proof Terms
/// <summary>
/// Indicates whether the term is a binary equivalence modulo namings.

19
src/api/dotnet/Model.cs
View file

@ -19,6 +19,7 @@ Notes:
using System;
using System.Diagnostics.Contracts;
using System.Collections.Generic;
namespace Microsoft.Z3
{
@ -131,6 +132,24 @@ namespace Microsoft.Z3
}
}
/// <summary>
/// Enumerate constants in model.
/// </summary>
public IEnumerable<KeyValuePair<FuncDecl, Expr>> Consts
{
get
{
uint nc = NumConsts;
for (uint i = 0; i < nc; ++i)
{
var f = new FuncDecl(Context, Native.Z3_model_get_const_decl(Context.nCtx, NativeObject, i));
IntPtr n = Native.Z3_model_get_const_interp(Context.nCtx, NativeObject, f.NativeObject);
if (n == IntPtr.Zero) continue;
yield return new KeyValuePair<FuncDecl, Expr>(f, Expr.Create(Context, n));
}
}
}
/// <summary>
/// The number of function interpretations in the model.
/// </summary>

22
src/api/java/Expr.java
View file

@ -126,7 +126,7 @@ public class Expr extends AST
if (isApp() && args.length != getNumArgs()) {
throw new Z3Exception("Number of arguments does not match");
}
return new Expr(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
return Expr.create(getContext(), Native.updateTerm(getContext().nCtx(), getNativeObject(),
args.length, Expr.arrayToNative(args)));
}
@ -1277,6 +1277,26 @@ public class Expr extends AST
return isApp() && getFuncDecl().getDeclKind() == Z3_decl_kind.Z3_OP_LABEL_LIT;
}
/**
* Check whether expression is a string constant.
* @return a boolean
*/
public boolean isString()
{
return isApp() && Native.isString(getContext().nCtx(), getNativeObject());
}
/**
* Retrieve string corresponding to string constant.
* Remark: the expression should be a string constant, (isString() should return true).
* @throws Z3Exception on error
* @return a string
*/
public String getString()
{
return Native.getString(getContext().nCtx(), getNativeObject());
}
/**
* Indicates whether the term is a binary equivalence modulo namings.
* Remarks: This binary predicate is used in proof terms. It captures

6
src/ast/datatype_decl_plugin.cpp
View file

@ -935,9 +935,9 @@ bool datatype_util::is_recursive(sort * ty) {
bool datatype_util::is_enum_sort(sort* s) {
if (!is_datatype(s)) {
return false;
}
if (!is_datatype(s)) {
return false;
}
bool r = false;
if (m_is_enum.find(s, r))
return r;

6
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -143,11 +143,11 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co
case OP_FPA_TO_FP_UNSIGNED: m_conv.mk_to_fp_unsigned(f, num, args, result); return BR_DONE;
case OP_FPA_FP: m_conv.mk_fp(f, num, args, result); return BR_DONE;
case OP_FPA_TO_UBV: m_conv.mk_to_ubv(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: m_conv.mk_to_ubv_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: m_conv.mk_to_sbv_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: m_conv.mk_to_real_unspecified(f, num, args, result); return BR_DONE;
case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE;
case OP_FPA_INTERNAL_TO_IEEE_BV_UNSPECIFIED: m_conv.mk_to_ieee_bv_unspecified(f, num, args, result); return BR_DONE;

2
src/ast/pb_decl_plugin.cpp
View file

@ -91,7 +91,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
}
void pb_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
if (logic == symbol::null || logic == "QF_FD") {
if (logic == symbol::null || logic == "QF_FD" || logic == "ALL") {
op_names.push_back(builtin_name(m_at_most_sym.bare_str(), OP_AT_MOST_K));
op_names.push_back(builtin_name(m_at_least_sym.bare_str(), OP_AT_LEAST_K));
op_names.push_back(builtin_name(m_pble_sym.bare_str(), OP_PB_LE));

44
src/ast/rewriter/seq_rewriter.cpp
View file

@ -92,25 +92,25 @@ public:
expr_ref fml(m.mk_true(), m);
return sym_expr::mk_pred(fml, m.mk_bool_sort());
}
virtual T mk_and(T x, T y) {
if (x->is_char() && y->is_char()) {
if (x->get_char() == y->get_char()) {
return x;
}
if (m.are_distinct(x->get_char(), y->get_char())) {
expr_ref fml(m.mk_false(), m);
return sym_expr::mk_pred(fml, x->get_sort());
}
}
virtual T mk_and(T x, T y) {
if (x->is_char() && y->is_char()) {
if (x->get_char() == y->get_char()) {
return x;
}
if (m.are_distinct(x->get_char(), y->get_char())) {
expr_ref fml(m.mk_false(), m);
return sym_expr::mk_pred(fml, x->get_sort());
}
}
sort* s = x->get_sort();
if (m.is_bool(s)) s = y->get_sort();
var_ref v(m.mk_var(0, s), m);
expr_ref fml1 = x->accept(v);
expr_ref fml2 = y->accept(v);
if (m.is_true(fml1)) {
return y;
}
sort* s = x->get_sort();
if (m.is_bool(s)) s = y->get_sort();
var_ref v(m.mk_var(0, s), m);
expr_ref fml1 = x->accept(v);
expr_ref fml2 = y->accept(v);
if (m.is_true(fml1)) {
return y;
}
if (m.is_true(fml2)) return x;
expr_ref fml(m.mk_and(fml1, fml2), m);
return sym_expr::mk_pred(fml, x->get_sort());
@ -178,10 +178,10 @@ public:
return sym_expr::mk_pred(fml, x->get_sort());
}
/*virtual vector<std::pair<vector<bool>, T>> generate_min_terms(vector<T> constraints){
return 0;
}*/
/*virtual vector<std::pair<vector<bool>, T>> generate_min_terms(vector<T> constraints){
return 0;
}*/
};
re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {}

2
src/ast/static_features.cpp
View file

@ -391,7 +391,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite
if (is_marked(e)) {
m_num_sharing++;
return;
}
}
if (stack_depth > m_max_stack_depth) {
return;
}

8
src/cmd_context/basic_cmds.cpp
View file

@ -622,7 +622,7 @@ public:
m_status(":status"),
m_reason_unknown(":reason-unknown"),
m_all_statistics(":all-statistics"),
m_assertion_stack_levels("assertion-stack-levels") {
m_assertion_stack_levels(":assertion-stack-levels") {
}
virtual char const * get_usage() const { return "<keyword>"; }
virtual char const * get_descr(cmd_context & ctx) const { return "get information."; }
@ -652,7 +652,7 @@ public:
ctx.regular_stream() << "(:status " << ctx.get_status() << ")" << std::endl;
}
else if (opt == m_reason_unknown) {
ctx.regular_stream() << "(:reason-unknown \"" << ctx.reason_unknown() << "\")" << std::endl;
ctx.regular_stream() << "(:reason-unknown \"" << escaped(ctx.reason_unknown().c_str()) << "\")" << std::endl;
}
else if (opt == m_all_statistics) {
ctx.display_statistics();
@ -852,9 +852,7 @@ void install_basic_cmds(cmd_context & ctx) {
ctx.insert(alloc(builtin_cmd, "declare-datatypes", "(<symbol>*) (<datatype-declaration>+)", "declare mutually recursive datatypes.\n<datatype-declaration> ::= (<symbol> <constructor-decl>+)\n<constructor-decl> ::= (<symbol> <accessor-decl>*)\n<accessor-decl> ::= (<symbol> <sort>)\nexample: (declare-datatypes (T) ((BinTree (leaf (value T)) (node (left BinTree) (right BinTree)))))"));
ctx.insert(alloc(builtin_cmd, "check-sat-asuming", "( hprop_literali* )", "check sat assuming a collection of literals"));
// ctx.insert(alloc(builtin_cmd, "define-fun-rec", "hfun-defi", "define a function satisfying recursive equations"));
// ctx.insert(alloc(builtin_cmd, "define-funs-rec", "( hfun_decin+1 ) ( htermin+1 )", "define multiple mutually recursive functions"));
// ctx.insert(alloc(get_unsat_assumptions_cmd));
ctx.insert(alloc(get_unsat_assumptions_cmd));
ctx.insert(alloc(reset_assertions_cmd));
}

6
src/cmd_context/cmd_context.cpp
View file

@ -530,10 +530,6 @@ bool cmd_context::logic_has_fpa() const {
return !has_logic() || smt_logics::logic_has_fpa(m_logic);
}
bool cmd_context::logic_has_str() const {
return !has_logic() || m_logic == "QF_S";
}
bool cmd_context::logic_has_array() const {
return !has_logic() || smt_logics::logic_has_array(m_logic);
}
@ -638,7 +634,7 @@ bool cmd_context::set_logic(symbol const & s) {
std::string cmd_context::reason_unknown() const {
if (m_check_sat_result.get() == 0)
throw cmd_exception("state of the most recent check-sat command is not known");
return "state of the most recent check-sat command is not known";
return m_check_sat_result->reason_unknown();
}

1
src/cmd_context/cmd_context.h
View file

@ -257,7 +257,6 @@ protected:
bool logic_has_array() const;
bool logic_has_datatype() const;
bool logic_has_fpa() const;
bool logic_has_str() const;
void print_unsupported_msg() { regular_stream() << "unsupported" << std::endl; }
void print_unsupported_info(symbol const& s, int line, int pos) { if (s != symbol::null) diagnostic_stream() << "; " << s << " line: " << line << " position: " << pos << std::endl;}

2
src/muz/pdr/pdr_context.cpp
View file

@ -1728,7 +1728,7 @@ namespace pdr {
void context::validate_search() {
expr_ref tr = m_search.get_trace(*this);
TRACE("pdr", tout << tr << "\n";);
TRACE("pdr", tout << tr << "\n";);
smt::kernel solver(m, get_fparams());
solver.assert_expr(tr);
lbool res = solver.check();

35
src/sat/sat_solver/inc_sat_solver.cpp
View file

@ -140,13 +140,36 @@ public:
m_solver.display_wcnf(out, m_asms.size(), m_asms.c_ptr(), nweights.c_ptr());
}
bool is_literal(expr* e) const {
return
is_uninterp_const(e) ||
(m.is_not(e, e) && is_uninterp_const(e));
}
virtual lbool check_sat(unsigned sz, expr * const * assumptions) {
m_solver.pop_to_base_level();
expr_ref_vector _assumptions(m);
obj_map<expr, expr*> asm2fml;
for (unsigned i = 0; i < sz; ++i) {
if (!is_literal(assumptions[i])) {
expr_ref a(m.mk_fresh_const("s", m.mk_bool_sort()), m);
expr_ref fml(m.mk_eq(a, assumptions[i]), m);
assert_expr(fml);
_assumptions.push_back(a);
asm2fml.insert(a, assumptions[i]);
}
else {
_assumptions.push_back(assumptions[i]);
asm2fml.insert(assumptions[i], assumptions[i]);
}
}
TRACE("sat", tout << _assumptions << "\n";);
dep2asm_t dep2asm;
m_model = 0;
lbool r = internalize_formulas();
if (r != l_true) return r;
r = internalize_assumptions(sz, assumptions, dep2asm);
r = internalize_assumptions(sz, _assumptions.c_ptr(), dep2asm);
if (r != l_true) return r;
m_internalized = true;
m_internalized_converted = false;
@ -163,7 +186,7 @@ public:
case l_false:
// TBD: expr_dependency core is not accounted for.
if (!m_asms.empty()) {
extract_core(dep2asm);
extract_core(dep2asm, asm2fml);
}
break;
default:
@ -286,6 +309,7 @@ public:
sat::bool_var_vector bvars;
vector<sat::literal_vector> lconseq;
dep2asm_t dep2asm;
obj_map<expr, expr*> asm2fml;
m_solver.pop_to_base_level();
lbool r = internalize_formulas();
if (r != l_true) return r;
@ -296,7 +320,7 @@ public:
r = m_solver.get_consequences(m_asms, bvars, lconseq);
if (r == l_false) {
if (!m_asms.empty()) {
extract_core(dep2asm);
extract_core(dep2asm, asm2fml);
}
return r;
}
@ -651,7 +675,7 @@ private:
}
}
void extract_core(dep2asm_t& dep2asm) {
void extract_core(dep2asm_t& dep2asm, obj_map<expr, expr*> const& asm2fml) {
u_map<expr*> asm2dep;
extract_asm2dep(dep2asm, asm2dep);
sat::literal_vector const& core = m_solver.get_core();
@ -672,6 +696,9 @@ private:
for (unsigned i = 0; i < core.size(); ++i) {
expr* e = 0;
VERIFY(asm2dep.find(core[i].index(), e));
if (asm2fml.contains(e)) {
e = asm2fml.find(e);
}
m_core.push_back(e);
}
}

6
src/smt/smt_case_split_queue.cpp
View file

@ -51,9 +51,9 @@ namespace smt {
if (!m_theory_var_priority.find(v2, p_v2)) {
p_v2 = 0.0;
}
// add clause activity
p_v1 += m_activity[v1];
p_v2 += m_activity[v2];
// add clause activity
p_v1 += m_activity[v1];
p_v2 += m_activity[v2];
return p_v1 > p_v2;
}
};

2
src/smt/smt_context.cpp
View file

@ -3044,7 +3044,7 @@ namespace smt {
// not counting any literals that get assigned by this method
// this relies on bcp() to give us its old m_qhead and therefore
// bcp() should always be called before this method
unsigned assigned_literal_end = m_assigned_literals.size();
for (; qhead < assigned_literal_end; ++qhead) {
literal l = m_assigned_literals[qhead];

2
src/smt/smt_for_each_relevant_expr.cpp
View file

@ -23,7 +23,7 @@ Revision History:
namespace smt {
bool check_at_labels::check(expr* n) {
bool check_at_labels::check(expr* n) {
m_first = true;
return count_at_labels_pos(n) <= 1;
}

4
src/smt/smt_model_checker.cpp
View file

@ -279,7 +279,7 @@ namespace smt {
m_aux_context->pop(1);
return r == l_false; // quantifier is satisfied by m_curr_model
}
model_ref complete_cex;
m_aux_context->get_model(complete_cex);
@ -425,7 +425,7 @@ namespace smt {
ptr_vector<quantifier>::const_iterator end = m_qm->end_quantifiers();
for (; it != end; ++it) {
quantifier * q = *it;
if(!m_qm->mbqi_enabled(q)) continue;
if(!m_qm->mbqi_enabled(q)) continue;
TRACE("model_checker",
tout << "Check: " << mk_pp(q, m) << "\n";
tout << m_context->get_assignment(q) << "\n";);

24
src/smt/theory_array_base.cpp
View file

@ -426,19 +426,19 @@ namespace smt {
ptr_buffer<enode> to_unmark;
unsigned num_vars = get_num_vars();
for (unsigned i = 0; i < num_vars; i++) {
enode * n = get_enode(i);
enode * n = get_enode(i);
if (ctx.is_relevant(n)) {
enode * r = n->get_root();
if (!r->is_marked()){
if(is_array_sort(r) && ctx.is_shared(r)) {
TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
theory_var r_th_var = r->get_th_var(get_id());
SASSERT(r_th_var != null_theory_var);
result.push_back(r_th_var);
}
r->set_mark();
to_unmark.push_back(r);
}
enode * r = n->get_root();
if (!r->is_marked()){
if(is_array_sort(r) && ctx.is_shared(r)) {
TRACE("array_shared", tout << "new shared var: #" << r->get_owner_id() << "\n";);
theory_var r_th_var = r->get_th_var(get_id());
SASSERT(r_th_var != null_theory_var);
result.push_back(r_th_var);
}
r->set_mark();
to_unmark.push_back(r);
}
}
}
unmark_enodes(to_unmark.size(), to_unmark.c_ptr());

70
src/smt/theory_str.cpp
View file

@ -25,6 +25,7 @@
#include<algorithm>
#include"theory_seq_empty.h"
#include"theory_arith.h"
#include"ast_util.h"
namespace smt {
@ -98,7 +99,7 @@ namespace smt {
if (defaultCharset) {
// valid C strings can't contain the null byte ('\0')
charSetSize = 255;
char_set = alloc_svect(char, charSetSize);
char_set.resize(256, 0);
int idx = 0;
// small letters
for (int i = 97; i < 123; i++) {
@ -157,8 +158,7 @@ namespace smt {
} else {
const char setset[] = { 'a', 'b', 'c' };
int fSize = sizeof(setset) / sizeof(char);
char_set = alloc_svect(char, fSize);
char_set.resize(fSize, 0);
charSetSize = fSize;
for (int i = 0; i < charSetSize; i++) {
char_set[i] = setset[i];
@ -494,6 +494,7 @@ namespace smt {
sort * string_sort = u.str.mk_string_sort();
app * a = mk_fresh_const(name.c_str(), string_sort);
m_trail.push_back(a);
TRACE("str", tout << "a->get_family_id() = " << a->get_family_id() << std::endl
<< "this->get_family_id() = " << this->get_family_id() << std::endl;);
@ -507,7 +508,6 @@ namespace smt {
m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;);
m_trail.push_back(a);
variable_set.insert(a);
internal_variable_set.insert(a);
track_variable_scope(a);
@ -521,6 +521,7 @@ namespace smt {
sort * string_sort = u.str.mk_string_sort();
app * a = mk_fresh_const("regex", string_sort);
m_trail.push_back(a);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
@ -529,7 +530,6 @@ namespace smt {
m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
TRACE("str", tout << "add " << mk_pp(a, m) << " to m_basicstr_axiom_todo" << std::endl;);
m_trail.push_back(a);
variable_set.insert(a);
//internal_variable_set.insert(a);
regex_variable_set.insert(a);
@ -5563,7 +5563,7 @@ namespace smt {
if (arg0VecSize > 0 && arg1VecSize > 0 && u.str.is_string(arg0_grdItor->first[arg0VecSize - 1]) && u.str.is_string(arg1_grdItor->first[0])) {
ndVec.pop_back();
ndVec.push_back(mk_concat(arg0_grdItor->first[arg0VecSize - 1], arg1_grdItor->first[0]));
for (int i = 1; i < arg1VecSize; i++) {
for (size_t i = 1; i < arg1VecSize; i++) {
ndVec.push_back(arg1_grdItor->first[i]);
}
} else {
@ -5666,7 +5666,7 @@ namespace smt {
if (subStrCnt == 1) {
zstring subStrVal;
if (u.str.is_string(subStrVec[0], subStrVal)) {
for (int i = 0; i < strCnt; i++) {
for (size_t i = 0; i < strCnt; i++) {
zstring strVal;
if (u.str.is_string(strVec[i], strVal)) {
if (strVal.contains(subStrVal)) {
@ -5675,7 +5675,7 @@ namespace smt {
}
}
} else {
for (int i = 0; i < strCnt; i++) {
for (size_t i = 0; i < strCnt; i++) {
if (strVec[i] == subStrVec[0]) {
return true;
}
@ -5683,7 +5683,7 @@ namespace smt {
}
return false;
} else {
for (int i = 0; i <= (strCnt - subStrCnt); i++) {
for (size_t i = 0; i <= (strCnt - subStrCnt); i++) {
// The first node in subStrVect should be
// * constant: a suffix of a note in strVec[i]
// * variable:
@ -5712,7 +5712,7 @@ namespace smt {
// middle nodes
bool midNodesOK = true;
for (int j = 1; j < subStrCnt - 1; j++) {
for (size_t j = 1; j < subStrCnt - 1; j++) {
if (subStrVec[j] != strVec[i + j]) {
midNodesOK = false;
break;
@ -6927,9 +6927,9 @@ namespace smt {
ast_manager & m = get_manager();
if (lenTester_fvar_map.contains(lenTester)) {
expr * fVar = lenTester_fvar_map[lenTester];
expr * toAssert = gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue);
expr_ref toAssert(gen_len_val_options_for_free_var(fVar, lenTester, lenTesterValue), m);
TRACE("str", tout << "asserting more length tests for free variable " << mk_ismt2_pp(fVar, m) << std::endl;);
if (toAssert != NULL) {
if (toAssert) {
assert_axiom(toAssert);
}
}
@ -9123,7 +9123,7 @@ namespace smt {
zstring theory_str::gen_val_string(int len, int_vector & encoding) {
SASSERT(charSetSize > 0);
SASSERT(char_set != NULL);
SASSERT(!char_set.empty());
std::string re(len, char_set[0]);
for (int i = 0; i < (int) encoding.size() - 1; i++) {
@ -9173,7 +9173,7 @@ namespace smt {
}
}
expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator,
expr* theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator,
zstring lenStr, int tries) {
ast_manager & m = get_manager();
context & ctx = get_context();
@ -9240,8 +9240,7 @@ namespace smt {
// ----------------------------------------------------------------------------------------
ptr_vector<expr> orList;
ptr_vector<expr> andList;
expr_ref_vector orList(m), andList(m);
for (long long i = l; i < h; i++) {
orList.push_back(m.mk_eq(val_indicator, mk_string(longlong_to_string(i).c_str()) ));
@ -9262,7 +9261,7 @@ namespace smt {
} else {
strAst = mk_string(aStr);
}
andList.push_back(m.mk_eq(orList[orList.size() - 1], m.mk_eq(freeVar, strAst)));
andList.push_back(m.mk_eq(orList[orList.size() - 1].get(), m.mk_eq(freeVar, strAst)));
}
if (!coverAll) {
orList.push_back(m.mk_eq(val_indicator, mk_string("more")));
@ -9273,21 +9272,8 @@ namespace smt {
}
}
expr ** or_items = alloc_svect(expr*, orList.size());
expr ** and_items = alloc_svect(expr*, andList.size() + 1);
for (int i = 0; i < (int) orList.size(); i++) {
or_items[i] = orList[i];
}
if (orList.size() > 1)
and_items[0] = m.mk_or(orList.size(), or_items);
else
and_items[0] = or_items[0];
for (int i = 0; i < (int) andList.size(); i++) {
and_items[i + 1] = andList[i];
}
expr * valTestAssert = m.mk_and(andList.size() + 1, and_items);
andList.push_back(mk_or(orList));
expr_ref valTestAssert = mk_and(andList);
// ---------------------------------------
// If the new value tester is $$_val_x_16_i
@ -9300,20 +9286,9 @@ namespace smt {
if (vTester != val_indicator)
andList.push_back(m.mk_eq(vTester, mk_string("more")));
}
expr * assertL = NULL;
if (andList.size() == 1) {
assertL = andList[0];
} else {
expr ** and_items = alloc_svect(expr*, andList.size());
for (int i = 0; i < (int) andList.size(); i++) {
and_items[i] = andList[i];
}
assertL = m.mk_and(andList.size(), and_items);
}
expr_ref assertL = mk_and(andList);
// (assertL => valTestAssert) <=> (!assertL OR valTestAssert)
valTestAssert = m.mk_or(m.mk_not(assertL), valTestAssert);
return valTestAssert;
return m.mk_or(m.mk_not(assertL), valTestAssert);
}
expr * theory_str::gen_free_var_options(expr * freeVar, expr * len_indicator,
@ -9378,7 +9353,7 @@ namespace smt {
<< " doesn't have an equivalence class value." << std::endl;);
refresh_theory_var(aTester);
expr * makeupAssert = gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i);
expr_ref makeupAssert(gen_val_options(freeVar, len_indicator, aTester, len_valueStr, i), m);
TRACE("str", tout << "var: " << mk_ismt2_pp(freeVar, m) << std::endl
<< mk_ismt2_pp(makeupAssert, m) << std::endl;);
@ -9400,8 +9375,7 @@ namespace smt {
fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester));
print_value_tester_list(fvar_valueTester_map[freeVar][len]);
}
expr * nextAssert = gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1);
return nextAssert;
return gen_val_options(freeVar, len_indicator, valTester, len_valueStr, i + 1);
}
return NULL;

8
src/smt/theory_str.h
View file

@ -330,9 +330,9 @@ protected:
std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
char * char_set;
std::map<char, int> charSetLookupTable;
int charSetSize;
svector<char> char_set;
std::map<char, int> charSetLookupTable;
int charSetSize;
obj_pair_map<expr, expr, expr*> concat_astNode_map;
@ -553,7 +553,7 @@ protected:
expr * gen_len_test_options(expr * freeVar, expr * indicator, int tries);
expr * gen_free_var_options(expr * freeVar, expr * len_indicator,
zstring len_valueStr, expr * valTesterInCbEq, zstring valTesterValueStr);
expr * gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator,
expr* gen_val_options(expr * freeVar, expr * len_indicator, expr * val_indicator,
zstring lenStr, int tries);
void print_value_tester_list(svector<std::pair<int, expr*> > & testerList);
bool get_next_val_encode(int_vector & base, int_vector & next);

2
src/solver/smt_logics.cpp
View file

@ -153,5 +153,5 @@ bool smt_logics::logic_has_pb(symbol const& s) {
}
bool smt_logics::logic_has_datatype(symbol const& s) {
return s == "QF_FD";
return s == "QF_FD" || s == "ALL";
}

2
src/tactic/smtlogics/qfbv_tactic.cpp
View file

@ -103,7 +103,7 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat
tactic * st = main_p(and_then(preamble_st,
// If the user sets HI_DIV0=false, then the formula may contain uninterpreted function
// symbols. In this case, we should not use the `sat', but instead `smt'. Alternatively,
// the UFs can be eliminated by eager ackermannization in the preamble.
// the UFs can be eliminated by eager ackermannization in the preamble.
cond(mk_is_qfbv_eq_probe(),
and_then(mk_bv1_blaster_tactic(m),
using_params(smt, solver_p)),

2
src/util/hwf.cpp
View file

@ -29,7 +29,7 @@ Revision History:
#include<fenv.h>
#endif
#if defined(__x86_64__) || defined(_M_X64) || \
#if defined(__x86_64__) || defined(_M_X64) || \
defined(__i386) || defined(_M_IX86)
#define USE_INTRINSICS
#endif

2
src/util/trace.cpp
View file

@ -52,7 +52,7 @@ void disable_trace(const char * tag) {
bool is_trace_enabled(const char * tag) {
return g_enable_all_trace_tags ||
(g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast<char *>(tag)));
(g_enabled_trace_tags && get_enabled_trace_tags().contains(const_cast<char *>(tag)));
}
void close_trace() {

22
src/util/warning.cpp
View file

@ -115,22 +115,22 @@ void format2ostream(std::ostream & out, char const* msg, va_list args) {
while (true) {
int nc = VPRF(buff.c_ptr(), buff.size(), msg, args);
#if !defined(_WINDOWS) && defined(_AMD64_)
// For some strange reason, on Linux 64-bit version, va_list args is reset by vsnprintf.
// Z3 crashes when trying to use va_list args again.
// For some strange reason, on Linux 64-bit version, va_list args is reset by vsnprintf.
// Z3 crashes when trying to use va_list args again.
// Hack: I truncate the message instead of expanding the buffer to make sure that
// va_list args is only used once.
END_ERR_HANDLER();
if (nc < 0) {
// vsnprintf didn't work, so we just print the msg
out << msg;
return;
}
if (nc >= static_cast<int>(buff.size())) {
END_ERR_HANDLER();
if (nc < 0) {
// vsnprintf didn't work, so we just print the msg
out << msg;
return;
}
if (nc >= static_cast<int>(buff.size())) {
// truncate the message
buff[buff.size() - 1] = 0;
}
}
out << buff.c_ptr();
return;
return;
#else
if (nc >= 0 && nc < static_cast<int>(buff.size()))
break; // success