mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

Merge remote-tracking branch 'upstream/master' into refactoring

Browse source
This commit is contained in:
Murphy Berzish 2018-03-19 01:43:18 -04:00
parent b5471e7fe0 b572639fcd
commit d569485170
22 changed files with 192 additions and 190 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
CMakeLists.txt
View file

@ -34,7 +34,7 @@ endif()
################################################################################
set(Z3_VERSION_MAJOR 4)
set(Z3_VERSION_MINOR 6)
set(Z3_VERSION_PATCH 1)
set(Z3_VERSION_PATCH 2)
set(Z3_VERSION_TWEAK 0)
set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}")
set(Z3_FULL_VERSION_STR "${Z3_VERSION}") # Note this might be modified
@ -240,6 +240,9 @@ elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD")
message(STATUS "Platform: FreeBSD")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_")
elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "NetBSD")
message(STATUS "Platform: NetBSD")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NetBSD_")
elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD")
message(STATUS "Platform: OpenBSD")
list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_")

2
scripts/mk_project.py
View file

@ -9,7 +9,7 @@ from mk_util import *
# Z3 Project definition
def init_project_def():
set_version(4, 6, 1, 0)
set_version(4, 6, 2, 0)
add_lib('util', [])
add_lib('lp', ['util'], 'util/lp')
add_lib('polynomial', ['util'], 'math/polynomial')

17
scripts/mk_util.py
View file

@ -69,6 +69,7 @@ IS_WINDOWS=False
IS_LINUX=False
IS_OSX=False
IS_FREEBSD=False
IS_NETBSD=False
IS_OPENBSD=False
IS_CYGWIN=False
IS_CYGWIN_MINGW=False
@ -141,6 +142,9 @@ def is_linux():
def is_freebsd():
return IS_FREEBSD
def is_netbsd():
return IS_NETBSD
def is_openbsd():
return IS_OPENBSD
@ -604,6 +608,8 @@ elif os.name == 'posix':
IS_LINUX=True
elif os.uname()[0] == 'FreeBSD':
IS_FREEBSD=True
elif os.uname()[0] == 'NetBSD':
IS_NETBSD=True
elif os.uname()[0] == 'OpenBSD':
IS_OPENBSD=True
elif os.uname()[0][:6] == 'CYGWIN':
@ -1245,7 +1251,7 @@ def get_so_ext():
sysname = os.uname()[0]
if sysname == 'Darwin':
return 'dylib'
elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'OpenBSD':
elif sysname == 'Linux' or sysname == 'FreeBSD' or sysname == 'NetBSD' or sysname == 'OpenBSD':
return 'so'
elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
return 'dll'
@ -1795,6 +1801,8 @@ class JavaDLLComponent(Component):
t = t.replace('PLATFORM', 'linux')
elif IS_FREEBSD:
t = t.replace('PLATFORM', 'freebsd')
elif IS_NETBSD:
t = t.replace('PLATFORM', 'netbsd')
elif IS_OPENBSD:
t = t.replace('PLATFORM', 'openbsd')
elif IS_CYGWIN:
@ -2504,6 +2512,13 @@ def mk_config():
LDFLAGS = '%s -lrt' % LDFLAGS
SLIBFLAGS = '-shared'
SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
elif sysname == 'NetBSD':
CXXFLAGS = '%s -D_NETBSD_' % CXXFLAGS
OS_DEFINES = '-D_NETBSD_'
SO_EXT = '.so'
LDFLAGS = '%s -lrt' % LDFLAGS
SLIBFLAGS = '-shared'
SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
elif sysname == 'OpenBSD':
CXXFLAGS = '%s -D_OPENBSD_' % CXXFLAGS
OS_DEFINES = '-D_OPENBSD_'

11
src/api/java/Context.java
View file

@ -2543,14 +2543,15 @@ public class Context implements AutoCloseable {
/**
* Parse the given string using the SMT-LIB2 parser.
*
* @return A conjunction of assertions in the scope (up to push/pop) at the
* end of the string.
* @return A conjunction of assertions.
*
* If the string contains push/pop commands, the
* set of assertions returned are the ones in the
* last scope level.
**/
public BoolExpr parseSMTLIB2String(String str, Symbol[] sortNames,
Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
Sort[] sorts, Symbol[] declNames, FuncDecl[] decls)
{
int csn = Symbol.arrayLength(sortNames);
int cs = Sort.arrayLength(sorts);
int cdn = Symbol.arrayLength(declNames);

3
src/api/ml/z3.ml
View file

@ -1402,7 +1402,6 @@ struct
let is_rewrite (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE)
let is_rewrite_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_REWRITE_STAR)
let is_pull_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT)
let is_pull_quant_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PULL_QUANT_STAR)
let is_push_quant (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_PUSH_QUANT)
let is_elim_unused_vars (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_ELIM_UNUSED_VARS)
let is_der (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_DER)
@ -1419,8 +1418,6 @@ struct
let is_iff_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_IFF_OEQ)
let is_nnf_pos (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_POS)
let is_nnf_neg (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_NEG)
let is_nnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_NNF_STAR)
let is_cnf_star (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_CNF_STAR)
let is_skolemize (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_SKOLEMIZE)
let is_modus_ponens_oeq (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_MODUS_PONENS_OEQ)
let is_theory_lemma (x:expr) = (AST.is_app x) && (FuncDecl.get_decl_kind (Expr.get_func_decl x) = OP_PR_TH_LEMMA)

23
src/api/ml/z3.mli
View file

@ -2458,13 +2458,6 @@ sig
A proof for (iff (f (forall (x) q(x)) r) (forall (x) (f (q x) r))). This proof object has no antecedents. *)
val is_pull_quant : Expr.expr -> bool
(** Indicates whether the term is a proof for pulling quantifiers out.
A proof for (iff P Q) where Q is in prenex normal form.
This proof object is only used if the parameter PROOF_MODE is 1.
This proof object has no antecedents *)
val is_pull_quant_star : Expr.expr -> bool
(** Indicates whether the term is a proof for pushing quantifiers in.
A proof for:
@ -2658,22 +2651,6 @@ sig
(and (or r_1 r_2) (or r_1' r_2'))) *)
val is_nnf_neg : Expr.expr -> bool
(** Indicates whether the term is a proof for (~ P Q) here Q is in negation normal form.
A proof for (~ P Q) where Q is in negation normal form.
This proof object is only used if the parameter PROOF_MODE is 1.
This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *)
val is_nnf_star : Expr.expr -> bool
(** Indicates whether the term is a proof for (~ P Q) where Q is in conjunctive normal form.
A proof for (~ P Q) where Q is in conjunctive normal form.
This proof object is only used if the parameter PROOF_MODE is 1.
This proof object may have n antecedents. Each antecedent is a PR_DEF_INTRO. *)
val is_cnf_star : Expr.expr -> bool
(** Indicates whether the term is a proof for a Skolemization step
Proof for:

30
src/api/python/z3/z3.py
View file

@ -114,15 +114,26 @@ def _symbol2py(ctx, s):
# Hack for having nary functions that can receive one argument that is the
# list of arguments.
# Use this when function takes a single list of arguments
def _get_args(args):
try:
if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
try:
if len(args) == 1 and (isinstance(args[0], tuple) or isinstance(args[0], list)):
return args[0]
elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)):
elif len(args) == 1 and (isinstance(args[0], set) or isinstance(args[0], AstVector)):
return [arg for arg in args[0]]
else:
return args
except: # len is not necessarily defined when args is not a sequence (use reflection?)
return args
# Use this when function takes multiple arguments
def _get_args_ast_list(args):
try:
if isinstance(args, set) or isinstance(args, AstVector) or isinstance(args, tuple):
return [arg for arg in args]
else:
return args
except: # len is not necessarily defined when args is not a sequence (use reflection?)
except:
return args
def _to_param_value(val):
@ -368,9 +379,6 @@ class AstRef(Z3PPObject):
def __copy__(self):
return self.translate(self.ctx)
def __deepcopy__(self):
return self.translate(self.ctx)
def hash(self):
"""Return a hashcode for the `self`.
@ -7946,8 +7954,10 @@ def AtLeast(*args):
return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx)
def _pb_args_coeffs(args):
args = _get_args(args)
def _pb_args_coeffs(args, default_ctx = None):
args = _get_args_ast_list(args)
if len(args) == 0:
return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)()
args, coeffs = zip(*args)
if __debug__:
_z3_assert(len(args) > 0, "Non empty list of arguments expected")
@ -7979,7 +7989,7 @@ def PbGe(args, k):
ctx, sz, _args, _coeffs = _pb_args_coeffs(args)
return BoolRef(Z3_mk_pbge(ctx.ref(), sz, _args, _coeffs, k), ctx)
def PbEq(args, k):
def PbEq(args, k, ctx = None):
"""Create a Pseudo-Boolean inequality k constraint.
>>> a, b, c = Bools('a b c')

4
src/api/python/z3/z3printer.py
View file

@ -36,7 +36,7 @@ _z3_op_to_str = {
Z3_OP_CONCAT : 'Concat', Z3_OP_EXTRACT : 'Extract', Z3_OP_BV2INT : 'BV2Int',
Z3_OP_ARRAY_MAP : 'Map', Z3_OP_SELECT : 'Select', Z3_OP_STORE : 'Store',
Z3_OP_CONST_ARRAY : 'K', Z3_OP_ARRAY_EXT : 'Ext',
Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe'
Z3_OP_PB_AT_MOST : 'AtMost', Z3_OP_PB_LE : 'PbLe', Z3_OP_PB_GE : 'PbGe', Z3_OP_PB_EQ : 'PbEq'
}
# List of infix operators
@ -930,6 +930,8 @@ class Formatter:
return self.pp_pbcmp(a, d, f, xs)
elif k == Z3_OP_PB_GE:
return self.pp_pbcmp(a, d, f, xs)
elif k == Z3_OP_PB_EQ:
return self.pp_pbcmp(a, d, f, xs)
elif z3.is_pattern(a):
return self.pp_pattern(a, d, xs)
elif self.is_infix(k):

1
src/api/z3.h
View file

@ -22,7 +22,6 @@ Notes:
#define Z3_H_
#include <stdio.h>
#include <stdbool.h>
#include "z3_macros.h"
#include "z3_api.h"
#include "z3_ast_containers.h"

2
src/api/z3_algebraic.h
View file

@ -31,7 +31,7 @@ extern "C" {
/** @name Algebraic Numbers */
/*@{*/
/**
\brief Return Z3_TRUE if \c can be used as value in the Z3 real algebraic
\brief Return Z3_TRUE if \c a can be used as value in the Z3 real algebraic
number package.
def_API('Z3_algebraic_is_value', BOOL, (_in(CONTEXT), _in(AST)))

2
src/api/z3_api.h
View file

@ -4350,7 +4350,7 @@ extern "C" {
Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a);
/**
\brief Return true if the give AST is a real algebraic number.
\brief Return true if the given AST is a real algebraic number.
def_API('Z3_is_algebraic_number', BOOL, (_in(CONTEXT), _in(AST)))
*/

2
src/ast/rewriter/rewriter_def.h
View file

@ -194,12 +194,14 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
result_stack().shrink(fr.m_spos);
result_stack().push_back(arg);
fr.m_state = REWRITE_BUILTIN;
TRACE("rewriter_step", tout << "step\n" << mk_ismt2_pp(t, m()) << "\n";);
if (visit<false>(arg, fr.m_max_depth)) {
m_r = result_stack().back();
result_stack().pop_back();
result_stack().pop_back();
result_stack().push_back(m_r);
cache_result<false>(t, m_r, m_pr, fr.m_cache_result);
TRACE("rewriter_step", tout << "step 1\n" << mk_ismt2_pp(m_r, m()) << "\n";);
frame_stack().pop_back();
set_new_child_flag(t);
}

18
src/math/polynomial/upolynomial.cpp
View file

@ -781,17 +781,15 @@ namespace upolynomial {
set(q.size(), q.c_ptr(), C);
m().set(bound, p);
}
else if (q.size() < C.size() || m().m().is_even(p) || m().m().is_even(bound)) {
// discard accumulated image, it was affected by unlucky primes
TRACE("mgcd", tout << "discarding image\n";);
set(q.size(), q.c_ptr(), C);
m().set(bound, p);
}
else {
if (q.size() < C.size()) {
// discard accumulated image, it was affected by unlucky primes
TRACE("mgcd", tout << "discarding image\n";);
set(q.size(), q.c_ptr(), C);
m().set(bound, p);
}
else {
CRA_combine_images(q, p, C, bound);
TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";);
}
CRA_combine_images(q, p, C, bound);
TRACE("mgcd", tout << "new combined:\n"; display_star(tout, C); tout << "\n";);
}
numeral_vector & candidate = q;
get_primitive(C, candidate);

11
src/model/model_evaluator.cpp
View file

@ -187,14 +187,14 @@ struct evaluator_cfg : public default_rewriter_cfg {
TRACE("model_evaluator", tout << "reduce_app " << f->get_name() << "\n";
for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m) << "\n";
tout << "---->\n" << mk_ismt2_pp(result, m) << "\n";);
return BR_DONE;
return BR_REWRITE1;
}
if (st == BR_FAILED && !m.is_builtin_family_id(fid))
st = evaluate_partial_theory_func(f, num, args, result, result_pr);
if (st == BR_DONE && is_app(result)) {
app* a = to_app(result);
if (evaluate(a->get_decl(), a->get_num_args(), a->get_args(), result)) {
return BR_DONE;
return BR_REWRITE1;
}
}
CTRACE("model_evaluator", st != BR_FAILED, tout << result << "\n";);
@ -399,12 +399,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
}
}
}
args_table::iterator it = table1.begin(), end = table1.end();
for (; it != end; ++it) {
switch (compare((*it)[arity], else2)) {
for (auto const& t : table1) {
switch (compare((t)[arity], else2)) {
case l_true: break;
case l_false: result = m.mk_false(); return BR_DONE;
default: conj.push_back(m.mk_eq((*it)[arity], else2)); break;
default: conj.push_back(m.mk_eq((t)[arity], else2)); break;
}
}
result = mk_and(conj);

108
src/smt/smt_context_pp.cpp
View file

@ -19,7 +19,7 @@ Revision History:
#include "smt/smt_context.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_pp.h"
#include "ast/ast_smt_pp.h"
#include "ast/ast_pp_util.h"
#include "util/stats.h"
namespace smt {
@ -43,11 +43,10 @@ namespace smt {
return out << "RESOURCE_LIMIT";
case THEORY:
if (!m_incomplete_theories.empty()) {
ptr_vector<theory>::const_iterator it = m_incomplete_theories.begin();
ptr_vector<theory>::const_iterator end = m_incomplete_theories.end();
for (bool first = true; it != end; ++it) {
bool first = true;
for (theory* th : m_incomplete_theories) {
if (first) first = false; else out << " ";
out << (*it)->get_name();
out << th->get_name();
}
}
else {
@ -173,12 +172,10 @@ namespace smt {
void context::display_binary_clauses(std::ostream & out) const {
bool first = true;
vector<watch_list>::const_iterator it = m_watches.begin();
vector<watch_list>::const_iterator end = m_watches.end();
for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
literal l1 = to_literal(l_idx);
unsigned l_idx = 0;
for (watch_list const& wl : m_watches) {
literal l1 = to_literal(l_idx++);
literal neg_l1 = ~l1;
watch_list const & wl = *it;
literal const * it2 = wl.begin_literals();
literal const * end2 = wl.end_literals();
for (; it2 != end2; ++it2) {
@ -291,10 +288,7 @@ namespace smt {
}
void context::display_theories(std::ostream & out) const {
ptr_vector<theory>::const_iterator it = m_theory_set.begin();
ptr_vector<theory>::const_iterator end = m_theory_set.end();
for (; it != end; ++it) {
theory * th = *it;
for (theory* th : m_theory_set) {
th->display(out);
}
}
@ -393,10 +387,8 @@ namespace smt {
#endif
m_qmanager->collect_statistics(st);
m_asserted_formulas.collect_statistics(st);
ptr_vector<theory>::const_iterator it = m_theory_set.begin();
ptr_vector<theory>::const_iterator end = m_theory_set.end();
for (; it != end; ++it) {
(*it)->collect_statistics(st);
for (theory* th : m_theory_set) {
th->collect_statistics(st);
}
}
@ -413,19 +405,23 @@ namespace smt {
}
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const {
ast_smt_pp pp(m_manager);
pp.set_benchmark_name("lemma");
pp.set_status("unsat");
pp.set_logic(logic);
ast_pp_util visitor(m_manager);
expr_ref_vector fmls(m_manager);
visitor.collect(fmls);
expr_ref n(m_manager);
for (unsigned i = 0; i < num_antecedents; i++) {
literal l = antecedents[i];
expr_ref n(m_manager);
literal2expr(l, n);
pp.add_assumption(n);
fmls.push_back(n);
}
expr_ref n(m_manager);
literal2expr(~consequent, n);
pp.display_smt2(out, n);
if (consequent != false_literal) {
literal2expr(~consequent, n);
fmls.push_back(n);
}
if (logic != symbol::null) out << "(set-logic " << logic << ")\n";
visitor.collect(fmls);
visitor.display_decls(out);
visitor.display_asserts(out, fmls, true);
}
static unsigned g_lemma_id = 0;
@ -448,25 +444,29 @@ namespace smt {
void context::display_lemma_as_smt_problem(std::ostream & out, unsigned num_antecedents, literal const * antecedents,
unsigned num_eq_antecedents, enode_pair const * eq_antecedents,
literal consequent, symbol const& logic) const {
ast_smt_pp pp(m_manager);
pp.set_benchmark_name("lemma");
pp.set_status("unsat");
pp.set_logic(logic);
ast_pp_util visitor(m_manager);
expr_ref_vector fmls(m_manager);
visitor.collect(fmls);
expr_ref n(m_manager);
for (unsigned i = 0; i < num_antecedents; i++) {
literal l = antecedents[i];
expr_ref n(m_manager);
literal2expr(l, n);
pp.add_assumption(n);
fmls.push_back(n);
}
for (unsigned i = 0; i < num_eq_antecedents; i++) {
enode_pair const & p = eq_antecedents[i];
expr_ref eq(m_manager);
eq = m_manager.mk_eq(p.first->get_owner(), p.second->get_owner());
pp.add_assumption(eq);
n = m_manager.mk_eq(p.first->get_owner(), p.second->get_owner());
fmls.push_back(n);
}
expr_ref n(m_manager);
literal2expr(~consequent, n);
pp.display_smt2(out, n);
if (consequent != false_literal) {
literal2expr(~consequent, n);
fmls.push_back(n);
}
if (logic != symbol::null) out << "(set-logic " << logic << ")\n";
visitor.collect(fmls);
visitor.display_decls(out);
visitor.display_asserts(out, fmls, true);
}
void context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents,
@ -490,10 +490,7 @@ namespace smt {
*/
void context::display_normalized_enodes(std::ostream & out) const {
out << "normalized enodes:\n";
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
enode * n = *it;
for (enode * n : m_enodes) {
out << "#";
out.width(5);
out << std::left << n->get_owner_id() << " #";
@ -524,28 +521,23 @@ namespace smt {
}
void context::display_enodes_lbls(std::ostream & out) const {
ptr_vector<enode>::const_iterator it = m_enodes.begin();
ptr_vector<enode>::const_iterator end = m_enodes.end();
for (; it != end; ++it) {
enode * n = *it;
for (enode* n : m_enodes) {
n->display_lbls(out);
}
}
void context::display_decl2enodes(std::ostream & out) const {
out << "decl2enodes:\n";
vector<enode_vector>::const_iterator it1 = m_decl2enodes.begin();
vector<enode_vector>::const_iterator end1 = m_decl2enodes.end();
for (unsigned id = 0; it1 != end1; ++it1, ++id) {
enode_vector const & v = *it1;
unsigned id = 0;
for (enode_vector const& v : m_decl2enodes) {
if (!v.empty()) {
out << "id " << id << " ->";
enode_vector::const_iterator it2 = v.begin();
enode_vector::const_iterator end2 = v.end();
for (; it2 != end2; ++it2)
out << " #" << (*it2)->get_owner_id();
for (enode* n : v) {
out << " #" << n->get_owner_id();
}
out << "\n";
}
++id;
}
}
@ -588,20 +580,20 @@ namespace smt {
case b_justification::BIN_CLAUSE: {
literal l2 = j.get_literal();
out << "bin-clause ";
display_literal(out, l2);
display_literal_verbose(out, l2);
break;
}
case b_justification::CLAUSE: {
clause * cls = j.get_clause();
out << "clause ";
if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals());
if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals());
break;
}
case b_justification::JUSTIFICATION: {
out << "justification " << j.get_justification()->get_from_theory() << ": ";
literal_vector lits;
const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
display_literals(out, lits);
display_literals_verbose(out, lits);
break;
}
default:

2
src/smt/smt_quantifier.cpp
View file

@ -222,7 +222,7 @@ namespace smt {
final_check_status final_check_eh(bool full) {
if (full) {
IF_VERBOSE(100, verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
IF_VERBOSE(100, if (!m_quantifiers.empty()) verbose_stream() << "(smt.final-check \"quantifiers\")\n";);
final_check_status result = m_qi_queue.final_check_eh() ? FC_DONE : FC_CONTINUE;
final_check_status presult = m_plugin->final_check_eh(full);
if (presult != FC_DONE)

8
src/smt/theory_seq.cpp
View file

@ -2404,8 +2404,7 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
lits.push_back(~is_digit(ith_char));
nums.push_back(digit2int(ith_char));
}
for (unsigned i = sz-1, c = 1; i > 0; c *= 10) {
--i;
for (unsigned i = sz, c = 1; i-- > 0; c *= 10) {
coeff = m_autil.mk_int(c);
nums[i] = m_autil.mk_mul(coeff, nums[i].get());
}
@ -2414,9 +2413,10 @@ bool theory_seq::add_stoi_val_axiom(expr* e) {
lits.push_back(mk_eq(e, num, false));
++m_stats.m_add_axiom;
m_new_propagation = true;
for (unsigned i = 0; i < lits.size(); ++i) {
ctx.mark_as_relevant(lits[i]);
for (literal lit : lits) {
ctx.mark_as_relevant(lit);
}
TRACE("seq", ctx.display_literals_verbose(tout, lits); tout << "\n";);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
m_stoi_axioms.insert(val);
m_trail_stack.push(insert_map<theory_seq, rational_set, rational>(m_stoi_axioms, val));

55
src/smt/theory_str.cpp
View file

@ -288,9 +288,9 @@ namespace smt {
}
}
static void cut_vars_map_copy(std::map<expr*, int> & dest, std::map<expr*, int> & src) {
for (auto entry : src) {
dest[entry.first] = 1;
static void cut_vars_map_copy(obj_map<expr, int> & dest, obj_map<expr, int> & src) {
for (auto const& kv : src) {
dest.insert(kv.m_key, 1);
}
}
@ -305,8 +305,8 @@ namespace smt {
return false;
}
for (auto entry : cut_var_map[n1].top()->vars) {
if (cut_var_map[n2].top()->vars.find(entry.first) != cut_var_map[n2].top()->vars.end()) {
for (auto const& kv : cut_var_map[n1].top()->vars) {
if (cut_var_map[n2].top()->vars.contains(kv.m_key)) {
return true;
}
}
@ -321,7 +321,7 @@ namespace smt {
T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel;
varInfo->vars[node] = 1;
varInfo->vars.insert(node, 1);
cut_var_map.insert(baseNode, std::stack<T_cut*>());
cut_var_map[baseNode].push(varInfo);
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
@ -330,7 +330,7 @@ namespace smt {
T_cut * varInfo = alloc(T_cut);
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel;
varInfo->vars[node] = 1;
varInfo->vars.insert(node, 1);
cut_var_map[baseNode].push(varInfo);
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
} else {
@ -339,11 +339,11 @@ namespace smt {
m_cut_allocs.push_back(varInfo);
varInfo->level = slevel;
cut_vars_map_copy(varInfo->vars, cut_var_map[baseNode].top()->vars);
varInfo->vars[node] = 1;
varInfo->vars.insert(node, 1);
cut_var_map[baseNode].push(varInfo);
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
} else if (cut_var_map[baseNode].top()->level == slevel) {
cut_var_map[baseNode].top()->vars[node] = 1;
cut_var_map[baseNode].top()->vars.insert(node, 1);
TRACE("str", tout << "add var info for baseNode=" << mk_pp(baseNode, get_manager()) << ", node=" << mk_pp(node, get_manager()) << " [" << slevel << "]" << std::endl;);
} else {
get_manager().raise_exception("entered illegal state during add_cut_info_one_node()");
@ -441,7 +441,7 @@ namespace smt {
void theory_str::track_variable_scope(expr * var) {
if (internal_variable_scope_levels.find(sLevel) == internal_variable_scope_levels.end()) {
internal_variable_scope_levels[sLevel] = std::set<expr*>();
internal_variable_scope_levels[sLevel] = obj_hashtable<expr>();
}
internal_variable_scope_levels[sLevel].insert(var);
}
@ -2566,8 +2566,8 @@ namespace smt {
if (cut_var_map.contains(node)) {
if (!cut_var_map[node].empty()) {
xout << "[" << cut_var_map[node].top()->level << "] ";
for (auto entry : cut_var_map[node].top()->vars) {
xout << mk_pp(entry.first, m) << ", ";
for (auto const& kv : cut_var_map[node].top()->vars) {
xout << mk_pp(kv.m_key, m) << ", ";
}
xout << std::endl;
}
@ -5530,7 +5530,8 @@ namespace smt {
return node;
}
void theory_str::get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
void theory_str::get_grounded_concats(unsigned depth,
expr* node, std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap) {
@ -5545,6 +5546,9 @@ namespace smt {
if (groundedMap.find(node) != groundedMap.end()) {
return;
}
IF_VERBOSE(100, verbose_stream() << "concats " << depth << "\n";
if (depth > 100) verbose_stream() << mk_pp(node, get_manager()) << "\n";
);
// haven't computed grounded concats for "node" (de-aliased)
// ---------------------------------------------------------
@ -5572,12 +5576,10 @@ namespace smt {
// merge arg0 and arg1
expr * arg0 = to_app(node)->get_arg(0);
expr * arg1 = to_app(node)->get_arg(1);
SASSERT(arg0 != node);
SASSERT(arg1 != node);
expr * arg0DeAlias = dealias_node(arg0, varAliasMap, concatAliasMap);
expr * arg1DeAlias = dealias_node(arg1, varAliasMap, concatAliasMap);
get_grounded_concats(arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(depth + 1, arg0DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(depth + 1, arg1DeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
std::map<std::vector<expr*>, std::set<expr*> >::iterator arg0_grdItor = groundedMap[arg0DeAlias].begin();
std::map<std::vector<expr*>, std::set<expr*> >::iterator arg1_grdItor;
@ -5627,7 +5629,7 @@ namespace smt {
else if (varEqConcatMap.find(node) != varEqConcatMap.end()) {
expr * eqConcat = varEqConcatMap[node].begin()->first;
expr * deAliasedEqConcat = dealias_node(eqConcat, varAliasMap, concatAliasMap);
get_grounded_concats(deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(depth + 1, deAliasedEqConcat, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
std::map<std::vector<expr*>, std::set<expr*> >::iterator grdItor = groundedMap[deAliasedEqConcat].begin();
for (; grdItor != groundedMap[deAliasedEqConcat].end(); grdItor++) {
@ -5836,8 +5838,8 @@ namespace smt {
expr* strDeAlias = dealias_node(str, varAliasMap, concatAliasMap);
expr* subStrDeAlias = dealias_node(subStr, varAliasMap, concatAliasMap);
get_grounded_concats(strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(0, strDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
get_grounded_concats(0, subStrDeAlias, varAliasMap, concatAliasMap, varConstMap, concatConstMap, varEqConcatMap, groundedMap);
// debugging
print_grounded_concat(strDeAlias, groundedMap);
@ -6448,7 +6450,7 @@ namespace smt {
// TODO figure out regex NFA stuff
if (!regex_nfa_cache.contains(regexTerm)) {
TRACE("str", tout << "regex_nfa_cache: cache miss" << std::endl;);
regex_nfa_cache[regexTerm] = nfa(u, regexTerm);
regex_nfa_cache.insert(regexTerm, nfa(u, regexTerm));
} else {
TRACE("str", tout << "regex_nfa_cache: cache hit" << std::endl;);
}
@ -9265,7 +9267,7 @@ namespace smt {
h++;
coverAll = get_next_val_encode(options[options.size() - 1], base);
}
val_range_map[val_indicator] = options[options.size() - 1];
val_range_map.insert(val_indicator, options[options.size() - 1]);
TRACE("str",
tout << "value tester encoding " << "{" << std::endl;
@ -9359,7 +9361,7 @@ namespace smt {
TRACE("str", tout << "no previous value testers, or none of them were in scope" << std::endl;);
int tries = 0;
expr * val_indicator = mk_internal_valTest_var(freeVar, len, tries);
valueTester_fvar_map[val_indicator] = freeVar;
valueTester_fvar_map.insert(val_indicator, freeVar);
fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, val_indicator));
print_value_tester_list(fvar_valueTester_map[freeVar][len]);
return gen_val_options(freeVar, len_indicator, val_indicator, len_valueStr, tries);
@ -9409,7 +9411,7 @@ namespace smt {
refresh_theory_var(valTester);
} else {
valTester = mk_internal_valTest_var(freeVar, len, i + 1);
valueTester_fvar_map[valTester] = freeVar;
valueTester_fvar_map.insert(valTester, freeVar);
fvar_valueTester_map[freeVar][len].push_back(std::make_pair(sLevel, valTester));
print_value_tester_list(fvar_valueTester_map[freeVar][len]);
}
@ -9606,8 +9608,9 @@ namespace smt {
// put together
toAssert = mgr.mk_and(ctx.mk_eq_atom(op0, and1), toAssert);
unroll_var_map[unrFunc] = toAssert;
} else {
unroll_var_map.insert(unrFunc, toAssert);
}
else {
toAssert = unroll_var_map[unrFunc];
}
}

42
src/smt/theory_str.h
View file

@ -77,25 +77,8 @@ public:
void register_value(expr * n) override { /* Ignore */ }
};
// rather than modify obj_pair_map I inherit from it and add my own helper methods
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {
public:
expr * operator[](std::pair<expr*, expr*> key) const {
expr * value;
bool found = this->find(key.first, key.second, value);
if (found) {
return value;
} else {
TRACE("t_str", tout << "WARNING: lookup miss in contain_pair_bool_map!" << std::endl;);
return nullptr;
}
}
bool contains(std::pair<expr*, expr*> key) const {
expr * unused;
return this->find(key.first, key.second, unused);
}
};
// NSB: added operator[] and contains to obj_pair_hashtable
class theory_str_contain_pair_bool_map_t : public obj_pair_map<expr, expr, expr*> {};
template<typename Ctx>
class binary_search_trail : public trail<Ctx> {
@ -169,7 +152,7 @@ class theory_str : public theory {
struct T_cut
{
int level;
std::map<expr*, int> vars;
obj_map<expr, int> vars;
T_cut() {
level = -100;
@ -292,8 +275,8 @@ protected:
int tmpXorVarCount;
int tmpLenTestVarCount;
int tmpValTestVarCount;
std::map<std::pair<expr*, expr*>, std::map<int, expr*> > varForBreakConcat;
// obj_pair_map<expr, expr, std::map<int, expr*> > varForBreakConcat;
std::map<std::pair<expr*,expr*>, std::map<int, expr*> > varForBreakConcat;
bool avoidLoopCut;
bool loopDetected;
obj_map<expr, std::stack<T_cut*> > cut_var_map;
@ -303,7 +286,7 @@ protected:
obj_hashtable<expr> variable_set;
obj_hashtable<expr> internal_variable_set;
obj_hashtable<expr> regex_variable_set;
std::map<int, std::set<expr*> > internal_variable_scope_levels;
std::map<int, obj_hashtable<expr> > internal_variable_scope_levels;
obj_hashtable<expr> internal_lenTest_vars;
obj_hashtable<expr> internal_valTest_vars;
@ -315,7 +298,9 @@ protected:
obj_map<expr, ptr_vector<expr> > fvar_lenTester_map;
obj_map<expr, expr*> lenTester_fvar_map;
obj_map<expr, std::map<int, svector<std::pair<int, expr*> > > > fvar_valueTester_map;
obj_map<expr, expr*> valueTester_fvar_map;
obj_map<expr, int_vector> val_range_map;
@ -331,9 +316,9 @@ protected:
theory_str_contain_pair_bool_map_t contain_pair_bool_map;
obj_map<expr, std::set<std::pair<expr*, expr*> > > contain_pair_idx_map;
// TBD: do a curried map for determinism.
std::map<std::pair<expr*, zstring>, expr*> regex_in_bool_map;
obj_map<expr, std::set<zstring> > regex_in_var_reg_str_map;
obj_map<expr, nfa> regex_nfa_cache; // Regex term --> NFA
svector<char> char_set;
@ -494,10 +479,11 @@ protected:
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr *> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap);
expr * dealias_node(expr * node, std::map<expr*, expr*> & varAliasMap, std::map<expr*, expr*> & concatAliasMap);
void get_grounded_concats(expr* node, std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void get_grounded_concats(unsigned depth,
expr* node, std::map<expr*, expr*> & varAliasMap,
std::map<expr*, expr*> & concatAliasMap, std::map<expr*, expr*> & varConstMap,
std::map<expr*, expr*> & concatConstMap, std::map<expr*, std::map<expr*, int> > & varEqConcatMap,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void print_grounded_concat(expr * node, std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);
void check_subsequence(expr* str, expr* strDeAlias, expr* subStr, expr* subStrDeAlias, expr* boolVar,
std::map<expr*, std::map<std::vector<expr*>, std::set<expr*> > > & groundedMap);

13
src/util/obj_pair_hashtable.h
View file

@ -160,10 +160,23 @@ public:
}
return (nullptr != e);
}
Value const & find(Key1 * k1, Key2 * k2) const {
entry * e = find_core(k1, k2);
return e->get_data().get_value();
}
Value const& operator[](std::pair<Key1 *, Key2 *> const& key) const {
return find(key.first, key.second);
}
bool contains(Key1 * k1, Key2 * k2) const {
return find_core(k1, k2) != nullptr;
}
bool contains(std::pair<Key1 *, Key2 *> const& key) const {
return contains(key.first, key.second);
}
void erase(Key1 * k1, Key2 * k2) {
m_table.remove(key_data(k1, k2));

18
src/util/scoped_timer.cpp
View file

@ -33,8 +33,8 @@ Revision History:
#include<sys/time.h>
#include<sys/errno.h>
#include<pthread.h>
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux
#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NetBSD_)
// Linux & FreeBSD & NetBSD
#include<errno.h>
#include<pthread.h>
#include<sched.h>
@ -66,8 +66,8 @@ struct scoped_timer::imp {
pthread_mutex_t m_mutex;
pthread_cond_t m_condition_var;
struct timespec m_end_time;
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
// Linux & FreeBSD & NetBSD
pthread_t m_thread_id;
pthread_mutex_t m_mutex;
pthread_cond_t m_cond;
@ -104,7 +104,7 @@ struct scoped_timer::imp {
return st;
}
#elif defined(_LINUX_) || defined(_FREEBSD_)
#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
static void* thread_func(void *arg) {
scoped_timer::imp *st = static_cast<scoped_timer::imp*>(arg);
@ -175,8 +175,8 @@ struct scoped_timer::imp {
if (pthread_create(&m_thread_id, &m_attributes, &thread_func, this) != 0)
throw default_exception("failed to start timer thread");
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
// Linux & FreeBSD & NetBSD
m_ms = ms;
m_initialized = false;
m_signal_sent = false;
@ -216,8 +216,8 @@ struct scoped_timer::imp {
throw default_exception("failed to destroy pthread condition variable");
if (pthread_attr_destroy(&m_attributes) != 0)
throw default_exception("failed to destroy pthread attributes object");
#elif defined(_LINUX_) || defined(_FREEBSD_)
// Linux & FreeBSD
#elif defined(_LINUX_) || defined(_FREEBSD_) || defined(_NETBSD_)
// Linux & FreeBSD & NetBSD
bool init = false;
// spin until timer thread has been created

5
src/util/stopwatch.h
View file

@ -134,6 +134,11 @@ public:
#include<ctime>
#ifndef CLOCK_PROCESS_CPUTIME_ID
/* BSD */
# define CLOCK_PROCESS_CPUTIME_ID CLOCK_MONOTONIC
#endif
class stopwatch {
unsigned long long m_time; // elapsed time in ns
bool m_running;