mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-18 09:12:16 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
nilsbecker 2018-11-25 16:58:09 +01:00
commit 1e4f524a22
392 changed files with 9183 additions and 4268 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/CMakeLists.txt
View file

@ -56,9 +56,11 @@ z3_add_component(smt
theory_dl.cpp
theory_dummy.cpp
theory_fpa.cpp
theory_jobscheduler.cpp
theory_lra.cpp
theory_opt.cpp
theory_pb.cpp
theory_recfun.cpp
theory_seq.cpp
theory_str.cpp
theory_utvpi.cpp

2
src/smt/arith_eq_solver.cpp
View file

@ -492,7 +492,7 @@ bool arith_eq_solver::solve_integer_equations_omega(
return false;
}
else if (r[index].is_zero()) {
// Row is trival
// Row is trivial
rows_solved.pop_back();
continue;
}

4
src/smt/params/qi_params.h
View file

@ -64,14 +64,14 @@ struct qi_params {
Enodes in the input problem have generation 0.
Some combinations of m_qi_cost and m_qi_new_gen will prevent Z3 from breaking matching loops.
For example, the "Weight 0" peformace bug was triggered by the following combination:
For example, the "Weight 0" performance bug was triggered by the following combination:
- m_qi_cost: (+ weight generation)
- m_qi_new_gen: cost
If a quantifier has weight 0, then the cost of instantiating it with a term in the input problem has cost 0.
The new enodes created during the instantiation will be tagged with generation = const = 0. So, every enode
will have generation 0, and consequently every quantifier instantiation will have cost 0.
Although dangerous, this feature was requested by the Boogie team. In their case, the patterns are carefully constructred,
Although dangerous, this feature was requested by the Boogie team. In their case, the patterns are carefully constructed,
and there are no matching loops. Moreover, the tag some quantifiers with weight 0 to instruct Z3 to never block their instances.
An example is the select-store axiom. They need this feature to be able to analyze code that contains very long execution paths.

6
src/smt/params/smt_params_helper.pyg
View file

@ -12,7 +12,7 @@ def_module_params(module_name='smt',
('ematching', BOOL, True, 'E-Matching based quantifier instantiation'),
('phase_selection', UINT, 3, 'phase selection heuristic: 0 - always false, 1 - always true, 2 - phase caching, 3 - phase caching conservative, 4 - phase caching conservative 2, 5 - random, 6 - number of occurrences'),
('restart_strategy', UINT, 1, '0 - geometric, 1 - inner-outer-geometric, 2 - luby, 3 - fixed, 4 - arithmetic'),
('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the currect restart threshold'),
('restart_factor', DOUBLE, 1.1, 'when using geometric (or inner-outer-geometric) progression of restarts, it specifies the constant used to multiply the current restart threshold'),
('case_split', UINT, 1, '0 - case split based on variable activity, 1 - similar to 0, but delay case splits created during the search, 2 - similar to 0, but cache the relevancy, 3 - case split based on relevancy (structural splitting), 4 - case split on relevancy and activity, 5 - case split on relevancy and current goal, 6 - activity-based case split with theory-aware branching activity'),
('delay_units', BOOL, False, 'if true then z3 will not restart when a unit clause is learned'),
('delay_units_threshold', UINT, 32, 'maximum number of learned unit clauses before restarting, ignored if delay_units is false'),
@ -95,5 +95,7 @@ def_module_params(module_name='smt',
('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'),
('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'),
('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'),
('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy')
('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy'),
('recfun.native', BOOL, True, 'use native rec-fun solver'),
('recfun.depth', UINT, 2, 'initial depth for maxrec expansion')
))

2
src/smt/qi_queue.cpp
View file

@ -175,7 +175,7 @@ namespace smt {
}
}
m_new_entries.reset();
TRACE("new_entries_bug", tout << "[qi:instatiate]\n";);
TRACE("new_entries_bug", tout << "[qi:instantiate]\n";);
}
void qi_queue::display_instance_profile(fingerprint * f, quantifier * q, unsigned num_bindings, enode * const * bindings, unsigned proof_id, unsigned generation) {

2
src/smt/smt_conflict_resolution.cpp
View file

@ -51,7 +51,7 @@ namespace smt {
}
/**
\brief Mark all enodes in a 'proof' tree brach starting at n
\brief Mark all enodes in a 'proof' tree branch starting at n
n -> ... -> root
*/
template<bool Set>

117
src/smt/smt_context.cpp
View file

@ -37,6 +37,7 @@ Revision History:
#include "model/model_pp.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_translation.h"
#include "ast/recfun_decl_plugin.h"
namespace smt {
@ -494,7 +495,7 @@ namespace smt {
try {
TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";);
TRACE("add_eq_detail", tout << "assigning\n" << mk_pp(n1->get_owner(), m_manager) << "\n" << mk_pp(n2->get_owner(), m_manager) << "\n";
TRACE("add_eq_detail", tout << "assigning\n" << enode_pp(n1, *this) << "\n" << enode_pp(n2, *this) << "\n";
tout << "kind: " << js.get_kind() << "\n";);
m_stats.m_num_add_eq++;
@ -518,7 +519,7 @@ namespace smt {
// 2. r1 is interpreted but r2 is not.
//
// The second condition is used to enforce the invariant that if a class contain
// an interepreted enode then the root is also interpreted.
// an interpreted enode then the root is also interpreted.
if ((r1->get_class_size() > r2->get_class_size() && !r2->is_interpreted()) || r1->is_interpreted()) {
SASSERT(!r2->is_interpreted());
std::swap(n1, n2);
@ -529,7 +530,7 @@ namespace smt {
" n1: #" << n1->get_owner_id() << "\n";);
// It is necessary to propagate relevancy to other elements of
// the equivalence class. This is nessary to enforce the invariant
// the equivalence class. This is necessary to enforce the invariant
// in the field m_parent of the enode class.
if (is_relevant(r1)) { // && !m_manager.is_eq(r1->get_owner())) !is_eq HACK
// NOTE for !is_eq HACK... the !is_eq HACK does not propagate relevancy when two
@ -1232,7 +1233,7 @@ namespace smt {
if (depth == 0)
return false;
if (r1->get_num_parents() < SMALL_NUM_PARENTS) {
TRACE("is_ext_diseq", tout << mk_bounded_pp(n1->get_owner(), m_manager) << " " << mk_bounded_pp(n2->get_owner(), m_manager) << " " << depth << "\n";);
TRACE("is_ext_diseq", tout << enode_pp(n1, *this) << " " << enode_pp(n2, *this) << " " << depth << "\n";);
for (enode * p1 : enode::parents(r1)) {
if (!is_relevant(p1))
continue;
@ -1241,7 +1242,7 @@ namespace smt {
if (!p1->is_cgr())
continue;
func_decl * f = p1->get_decl();
TRACE("is_ext_diseq", tout << "p1: " << mk_bounded_pp(p1->get_owner(), m_manager) << "\n";);
TRACE("is_ext_diseq", tout << "p1: " << enode_pp(p1, *this) << "\n";);
unsigned num_args = p1->get_num_args();
for (enode * p2 : enode::parents(r2)) {
if (!is_relevant(p2))
@ -1250,7 +1251,7 @@ namespace smt {
continue;
if (!p2->is_cgr())
continue;
TRACE("is_ext_diseq", tout << "p2: " << mk_bounded_pp(p2->get_owner(), m_manager) << "\n";);
TRACE("is_ext_diseq", tout << "p2: " << enode_pp(p2, *this) << "\n";);
if (p1->get_root() != p2->get_root() && p2->get_decl() == f && p2->get_num_args() == num_args) {
unsigned j = 0;
for (j = 0; j < num_args; j++) {
@ -1264,7 +1265,7 @@ namespace smt {
break;
}
if (j == num_args) {
TRACE("is_ext_diseq", tout << "found parents: " << mk_bounded_pp(p1->get_owner(), m_manager) << " " << mk_bounded_pp(p2->get_owner(), m_manager) << "\n";);
TRACE("is_ext_diseq", tout << "found parents: " << enode_pp(p1, *this) << " " << enode_pp(p2, *this) << "\n";);
if (is_ext_diseq(p1, p2, depth - 1))
return true;
}
@ -1384,7 +1385,10 @@ namespace smt {
SASSERT(m_manager.is_eq(n));
expr * lhs = n->get_arg(0);
expr * rhs = n->get_arg(1);
if (val == l_true) {
if (m_manager.is_bool(lhs)) {
// no-op
}
else if (val == l_true) {
add_eq(get_enode(lhs), get_enode(rhs), eq_justification(l));
}
else {
@ -1770,7 +1774,7 @@ namespace smt {
void context::set_conflict(const b_justification & js, literal not_l) {
if (!inconsistent()) {
TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); );
TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout << " ", js); );
m_conflict = js;
m_not_l = not_l;
}
@ -3207,7 +3211,7 @@ namespace smt {
}
else {
set_conflict(b_justification(tmp_clause.first), null_literal);
}
}
VERIFY(!resolve_conflict());
return l_false;
next_clause:
@ -3266,6 +3270,18 @@ namespace smt {
m_assumptions.reset();
}
bool context::should_research(lbool r) {
if (r != l_false || m_unsat_core.empty()) {
return false;
}
for (theory* th : m_theory_set) {
if (th->should_research(m_unsat_core)) {
return true;
}
}
return false;
}
lbool context::mk_unsat_core(lbool r) {
if (r != l_false) return r;
SASSERT(inconsistent());
@ -3353,7 +3369,7 @@ namespace smt {
add_theory_assumptions(theory_assumptions);
if (!theory_assumptions.empty()) {
TRACE("search", tout << "Adding theory assumptions to context" << std::endl;);
return check(theory_assumptions.size(), theory_assumptions.c_ptr(), reset_cancel, true);
return check(0, nullptr, reset_cancel);
}
internalize_assertions();
@ -3407,19 +3423,24 @@ namespace smt {
}
}
lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel, bool already_did_theory_assumptions) {
lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) {
if (!check_preamble(reset_cancel)) return l_undef;
SASSERT(at_base_level());
setup_context(false);
expr_ref_vector asms(m_manager, num_assumptions, assumptions);
if (!already_did_theory_assumptions) add_theory_assumptions(asms);
// introducing proxies: if (!validate_assumptions(asms)) return l_undef;
TRACE("unsat_core_bug", tout << asms << "\n";);
internalize_assertions();
init_assumptions(asms);
TRACE("before_search", display(tout););
lbool r = search();
r = mk_unsat_core(r);
lbool r;
do {
pop_to_base_lvl();
expr_ref_vector asms(m_manager, num_assumptions, assumptions);
add_theory_assumptions(asms);
// introducing proxies: if (!validate_assumptions(asms)) return l_undef;
TRACE("unsat_core_bug", tout << asms << "\n";);
internalize_assertions();
init_assumptions(asms);
TRACE("before_search", display(tout););
r = search();
r = mk_unsat_core(r);
}
while (should_research(r));
r = check_finalize(r);
return r;
}
@ -3428,15 +3449,20 @@ namespace smt {
if (!check_preamble(true)) return l_undef;
TRACE("before_search", display(tout););
setup_context(false);
expr_ref_vector asms(cube);
add_theory_assumptions(asms);
// introducing proxies: if (!validate_assumptions(asms)) return l_undef;
for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
internalize_assertions();
init_assumptions(asms);
for (auto const& clause : clauses) init_clause(clause);
lbool r = search();
r = mk_unsat_core(r);
lbool r;
do {
pop_to_base_lvl();
expr_ref_vector asms(cube);
add_theory_assumptions(asms);
// introducing proxies: if (!validate_assumptions(asms)) return l_undef;
for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
internalize_assertions();
init_assumptions(asms);
for (auto const& clause : clauses) init_clause(clause);
r = search();
r = mk_unsat_core(r);
}
while (should_research(r));
r = check_finalize(r);
return r;
}
@ -3770,7 +3796,7 @@ namespace smt {
}
m_stats.m_num_final_checks++;
TRACE("final_check_stats", tout << "m_stats.m_num_final_checks = " << m_stats.m_num_final_checks << "\n";);
TRACE("final_check_stats", tout << "m_stats.m_num_final_checks = " << m_stats.m_num_final_checks << "\n";);
final_check_status ok = m_qmanager->final_check_eh(false);
if (ok != FC_DONE)
@ -4067,7 +4093,7 @@ namespace smt {
A literal may have been marked relevant within the scope that gets popped during
conflict resolution. In this case, the literal is no longer marked as relevant after
the pop. This can cause quantifier instantiation to miss relevant triggers and thereby
cause incmpleteness.
cause incompleteness.
*/
void context::record_relevancy(unsigned n, literal const* lits) {
m_relevant_conflict_literals.reset();
@ -4281,7 +4307,7 @@ namespace smt {
return true;
}
// the variabe is shared if the equivalence class of n
// the variable is shared if the equivalence class of n
// contains a parent application.
theory_var_list * l = n->get_th_var_list();
@ -4290,7 +4316,7 @@ namespace smt {
for (enode * parent : enode::parents(n)) {
family_id fid = parent->get_owner()->get_family_id();
if (fid != th_id && fid != m_manager.get_basic_family_id()) {
TRACE("is_shared", tout << mk_pp(n->get_owner(), m_manager) << "\nis shared because of:\n" << mk_pp(parent->get_owner(), m_manager) << "\n";);
TRACE("is_shared", tout << enode_pp(n, *this) << "\nis shared because of:\n" << enode_pp(parent, *this) << "\n";);
return true;
}
}
@ -4428,6 +4454,29 @@ namespace smt {
m_model->register_decl(f, fi);
}
}
recfun::util u(m);
func_decl_ref_vector recfuns = u.get_rec_funs();
for (func_decl* f : recfuns) {
auto& def = u.get_def(f);
expr* rhs = def.get_rhs();
if (!rhs) continue;
if (f->get_arity() == 0) {
m_model->register_decl(f, rhs);
continue;
}
func_interp* fi = alloc(func_interp, m, f->get_arity());
// reverse argument order so that variable 0 starts at the beginning.
expr_ref_vector subst(m);
for (unsigned i = 0; i < f->get_arity(); ++i) {
subst.push_back(m.mk_var(i, f->get_domain(i)));
}
var_subst sub(m, true);
expr_ref bodyr = sub(rhs, subst.size(), subst.c_ptr());
fi->set_else(bodyr);
m_model->register_decl(f, fi);
}
}
};

63
src/smt/smt_context.h
View file

@ -859,6 +859,10 @@ namespace smt {
void mk_th_axiom(theory_id tid, literal l1, literal l2, literal l3, unsigned num_params = 0, parameter * params = nullptr);
void mk_th_axiom(theory_id tid, literal_vector const& ls, unsigned num_params = 0, parameter * params = nullptr) {
mk_th_axiom(tid, ls.size(), ls.c_ptr(), num_params, params);
}
/*
* Provide a hint to the core solver that the specified literals form a "theory case split".
* The core solver will enforce the condition that exactly one of these literals can be
@ -1010,9 +1014,9 @@ namespace smt {
void restore_theory_vars(enode * r2, enode * r1);
void push_eq(enode * lhs, enode * rhs, eq_justification const & js) {
SASSERT(lhs != rhs);
SASSERT(lhs->get_root() != rhs->get_root());
m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js));
if (lhs->get_root() != rhs->get_root()) {
m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js));
}
}
void push_new_congruence(enode * n1, enode * n2, bool used_commutativity) {
@ -1133,6 +1137,8 @@ namespace smt {
void add_theory_assumptions(expr_ref_vector & theory_assumptions);
lbool mk_unsat_core(lbool result);
bool should_research(lbool result);
void validate_unsat_core();
@ -1243,6 +1249,11 @@ namespace smt {
public:
bool can_propagate() const;
// Retrieve arithmetic values.
bool get_arith_lo(expr* e, rational& lo, bool& strict);
bool get_arith_up(expr* e, rational& up, bool& strict);
bool get_arith_value(expr* e, rational& value);
// -----------------------------------
//
// Model checking... (must be improved)
@ -1515,7 +1526,7 @@ namespace smt {
void pop(unsigned num_scopes);
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true, bool already_did_theory_assumptions = false);
lbool check(unsigned num_assumptions = 0, expr * const * assumptions = nullptr, bool reset_cancel = true);
lbool check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses);
@ -1609,6 +1620,50 @@ namespace smt {
void insert_macro(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep) { m_asserted_formulas.insert_macro(f, m, pr, dep); }
};
struct pp_lit {
context & ctx;
literal lit;
pp_lit(context & ctx, literal lit) : ctx(ctx), lit(lit) {}
};
inline std::ostream & operator<<(std::ostream & out, pp_lit const & pp) {
return pp.ctx.display_detailed_literal(out, pp.lit);
}
struct pp_lits {
context & ctx;
literal const *lits;
unsigned len;
pp_lits(context & ctx, unsigned len, literal const *lits) : ctx(ctx), lits(lits), len(len) {}
pp_lits(context & ctx, literal_vector const& ls) : ctx(ctx), lits(ls.c_ptr()), len(ls.size()) {}
};
inline std::ostream & operator<<(std::ostream & out, pp_lits const & pp) {
out << "{";
bool first = true;
for (unsigned i = 0; i < pp.len; ++i) {
if (first) { first = false; } else { out << " or\n"; }
pp.ctx.display_detailed_literal(out, pp.lits[i]);
}
return out << "}";
}
struct enode_eq_pp {
context const& ctx;
enode_pair const& p;
enode_eq_pp(enode_pair const& p, context const& ctx): ctx(ctx), p(p) {}
};
std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p);
struct enode_pp {
context const& ctx;
enode* n;
enode_pp(enode* n, context const& ctx): ctx(ctx), n(n) {}
};
std::ostream& operator<<(std::ostream& out, enode_pp const& p);
};
#endif /* SMT_CONTEXT_H_ */

2
src/smt/smt_context_inv.cpp
View file

@ -303,7 +303,7 @@ namespace smt {
for (bool_var v = 0; v < num; v++) {
if (has_enode(v)) {
enode * n = bool_var2enode(v);
if (n->is_eq() && is_relevant(n) && get_assignment(v) == l_false) {
if (n->is_eq() && is_relevant(n) && get_assignment(v) == l_false && !m_manager.is_iff(n->get_owner())) {
TRACE("check_th_diseq_propagation", tout << "checking: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m_manager) << "\n";);
enode * lhs = n->get_arg(0)->get_root();
enode * rhs = n->get_arg(1)->get_root();

12
src/smt/smt_context_pp.cpp
View file

@ -603,5 +603,17 @@ namespace smt {
display(out, j);
}
std::ostream& operator<<(std::ostream& out, enode_pp const& p) {
ast_manager& m = p.ctx.get_manager();
enode* n = p.n;
return out << "[#" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), m) << "]";
}
std::ostream& operator<<(std::ostream& out, enode_eq_pp const& p) {
return out << enode_pp(p.p.first, p.ctx) << " = " << enode_pp(p.p.second, p.ctx) << "\n";
}
};

2
src/smt/smt_enode.h
View file

@ -64,7 +64,7 @@ namespace smt {
class tmp_enode;
/**
\brief Aditional data-structure for implementing congruence closure,
\brief Additional data-structure for implementing congruence closure,
equality propagation, and the theory central bus of equalities.
*/
class enode {

2
src/smt/smt_model_checker.cpp
View file

@ -261,7 +261,7 @@ namespace smt {
try {
for_each_expr(*this, m_visited, n);
}
catch (is_model_value) {
catch (const is_model_value &) {
return true;
}
return false;

6
src/smt/smt_model_finder.cpp
View file

@ -177,7 +177,7 @@ namespace smt {
try {
for_each_expr(*this, m_visited, n);
}
catch (is_model_value) {
catch (const is_model_value &) {
return true;
}
return false;
@ -2892,7 +2892,7 @@ namespace smt {
try {
for_each_expr(oc, m_visited, def);
}
catch (occurs) {
catch (const occurs &) {
return false;
}
return true;
@ -2981,7 +2981,7 @@ namespace smt {
try {
process(f);
}
catch (found_satisfied_subset) {
catch (const found_satisfied_subset &) {
set_interp();
copy_non_satisfied(qcandidates, new_qs);
return true;

5
src/smt/smt_model_generator.cpp
View file

@ -402,7 +402,10 @@ namespace smt {
enode * n = m_context->get_enode(t);
unsigned num_args = n->get_num_args();
func_decl * f = n->get_decl();
if (num_args > 0 && n->get_cg() == n && include_func_interp(f)) {
if (num_args == 0 && include_func_interp(f)) {
m_model->register_decl(f, get_value(n));
}
else if (num_args > 0 && n->get_cg() == n && include_func_interp(f)) {
ptr_buffer<expr> args;
expr * result = get_value(n);
SASSERT(result);

2
src/smt/smt_model_generator.h
View file

@ -96,7 +96,7 @@ namespace smt {
class model_value_dependency {
bool m_fresh; //!< True if the dependency is a new fresh value;
union {
enode * m_enode; //!< When m_fresh == false, contains an enode depedency.
enode * m_enode; //!< When m_fresh == false, contains an enode dependency.
extra_fresh_value * m_value; //!< When m_fresh == true, contains the sort of the fresh value
};
public:

24
src/smt/smt_setup.cpp
View file

@ -28,6 +28,7 @@ Revision History:
#include "smt/theory_array_full.h"
#include "smt/theory_bv.h"
#include "smt/theory_datatype.h"
#include "smt/theory_recfun.h"
#include "smt/theory_dummy.h"
#include "smt/theory_dl.h"
#include "smt/theory_seq_empty.h"
@ -35,6 +36,7 @@ Revision History:
#include "smt/theory_pb.h"
#include "smt/theory_fpa.h"
#include "smt/theory_str.h"
#include "smt/theory_jobscheduler.h"
namespace smt {
@ -119,6 +121,8 @@ namespace smt {
setup_UFLRA();
else if (m_logic == "LRA")
setup_LRA();
else if (m_logic == "CSP")
setup_CSP();
else if (m_logic == "QF_FP")
setup_QF_FP();
else if (m_logic == "QF_FPBV" || m_logic == "QF_BVFP")
@ -196,6 +200,8 @@ namespace smt {
setup_QF_DT();
else if (m_logic == "LRA")
setup_LRA();
else if (m_logic == "CSP")
setup_CSP();
else
setup_unknown(st);
}
@ -203,7 +209,7 @@ namespace smt {
static void check_no_arithmetic(static_features const & st, char const * logic) {
if (st.m_num_arith_ineqs > 0 || st.m_num_arith_terms > 0 || st.m_num_arith_eqs > 0)
throw default_exception("Benchmark constains arithmetic, but specified loging does not support it.");
throw default_exception("Benchmark constains arithmetic, but specified logic does not support it.");
}
void setup::setup_QF_UF() {
@ -217,6 +223,7 @@ namespace smt {
void setup::setup_QF_DT() {
setup_QF_UF();
setup_datatypes();
setup_recfuns();
}
void setup::setup_QF_BVRE() {
@ -519,7 +526,7 @@ namespace smt {
m_params.m_arith_eq2ineq = true;
m_params.m_eliminate_term_ite = true;
// if (st.m_num_exprs < 5000 && st.m_num_ite_terms < 50) { // safeguard to avoid high memory consumption
// TODO: implement analsysis function to decide where lift ite is too expensive.
// TODO: implement analysis function to decide where lift ite is too expensive.
// m_params.m_lift_ite = LI_FULL;
// }
}
@ -873,6 +880,12 @@ namespace smt {
m_context.register_plugin(alloc(theory_datatype, m_manager, m_params));
}
void setup::setup_recfuns() {
TRACE("recfun", tout << "registering theory recfun...\n";);
theory_recfun * th = alloc(theory_recfun, m_manager);
m_context.register_plugin(th);
}
void setup::setup_dl() {
m_context.register_plugin(mk_theory_dl(m_manager));
}
@ -916,6 +929,11 @@ namespace smt {
m_context.register_plugin(alloc(smt::theory_seq, m_manager, m_params));
}
void setup::setup_CSP() {
setup_unknown();
m_context.register_plugin(alloc(smt::theory_jobscheduler, m_manager));
}
void setup::setup_unknown() {
static_features st(m_manager);
ptr_vector<expr> fmls;
@ -926,6 +944,7 @@ namespace smt {
setup_arrays();
setup_bv();
setup_datatypes();
setup_recfuns();
setup_dl();
setup_seq_str(st);
setup_card();
@ -945,6 +964,7 @@ namespace smt {
setup_seq_str(st);
setup_card();
setup_fpa();
setup_recfuns();
return;
}

2
src/smt/smt_setup.h
View file

@ -81,6 +81,7 @@ namespace smt {
void setup_QF_FPBV();
void setup_QF_S();
void setup_LRA();
void setup_CSP();
void setup_AUFLIA(bool simple_array = true);
void setup_AUFLIA(static_features const & st);
void setup_AUFLIRA(bool simple_array = true);
@ -93,6 +94,7 @@ namespace smt {
void setup_unknown(static_features & st);
void setup_arrays();
void setup_datatypes();
void setup_recfuns();
void setup_bv();
void setup_arith();
void setup_dl();

15
src/smt/smt_theory.h
View file

@ -68,7 +68,7 @@ namespace smt {
public:
/**
\brief Return ture if the given enode is attached to a
\brief Return true if the given enode is attached to a
variable of the theory.
\remark The result is not equivalent to
@ -194,6 +194,15 @@ namespace smt {
return l_false;
}
/**
\brief This method is called from the smt_context when an unsat core is generated.
The theory may tell the solver to perform iterative deepening by invalidating
this unsat core and increasing some resource constraints.
*/
virtual bool should_research(expr_ref_vector & unsat_core) {
return false;
}
/**
\brief This method is invoked before the search starts.
*/
@ -294,6 +303,8 @@ namespace smt {
SASSERT(m_context);
return *m_context;
}
context & ctx() const { return get_context(); }
ast_manager & get_manager() const {
SASSERT(m_manager);
@ -389,7 +400,7 @@ namespace smt {
\brief When an eq atom n is created during the search, the default behavior is
to make sure that the n->get_arg(0)->get_id() < n->get_arg(1)->get_id().
This may create some redundant atoms, since some theories/families use different
convetions in their simplifiers. For example, arithmetic always force a numeral
conventions in their simplifiers. For example, arithmetic always force a numeral
to be in the right hand side. So, this method should be redefined if the default
behavior conflicts with a convention used by the theory/family.
*/

34
src/smt/tactic/smt_tactic.cpp
View file

@ -289,30 +289,24 @@ public:
}
};
tactic * mk_smt_tactic(params_ref const & p) {
static tactic * mk_seq_smt_tactic(params_ref const & p) {
return alloc(smt_tactic, p);
}
tactic * mk_smt_tactic_using(bool auto_config, params_ref const & _p) {
params_ref p = _p;
p.set_bool("auto_config", auto_config);
tactic * r = mk_smt_tactic(p);
TRACE("smt_tactic", tout << "auto_config: " << auto_config << "\nr: " << r << "\np: " << p << "\n";);
return using_params(r, p);
}
tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) {
parallel_params pp(p);
return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p);
}
tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p, symbol const& logic) {
parallel_params pp(_p);
params_ref p = _p;
p.set_bool("auto_config", auto_config);
return using_params(pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p), p);
}
tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p) {
return mk_parallel_tactic(mk_smt_solver(m, p, symbol::null), p);
}
tactic * mk_smt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) {
parallel_params pp(p);
return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_seq_smt_tactic(p);
}
tactic * mk_smt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p) {
parallel_params pp(_p);
params_ref p = _p;
p.set_bool("auto_config", auto_config);
return using_params(pp.enable() ? mk_parallel_smt_tactic(m, p) : mk_seq_smt_tactic(p), p);
}

8
src/smt/tactic/smt_tactic.h
View file

@ -27,17 +27,15 @@ Notes:
class tactic;
class filter_model_converter;
tactic * mk_smt_tactic(params_ref const & p = params_ref());
tactic * mk_smt_tactic(ast_manager& m, params_ref const & p = params_ref(), symbol const& logic = symbol::null);
// syntax sugar for using_params(mk_smt_tactic(), p) where p = (:auto_config, auto_config)
tactic * mk_smt_tactic_using(bool auto_config = true, params_ref const & p = params_ref());
tactic * mk_smt_tactic_using(ast_manager& m, bool auto_config = true, params_ref const & p = params_ref());
tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic = symbol::null);
tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& p, symbol const& logic = symbol::null);
tactic * mk_parallel_smt_tactic(ast_manager& m, params_ref const& p);
/*
ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(p)")
ADD_TACTIC("smt", "apply a SAT based SMT solver.", "mk_smt_tactic(m, p)")
ADD_TACTIC("psmt", "builtin strategy for SMT tactic in parallel.", "mk_parallel_smt_tactic(m, p)")
*/
#endif

14
src/smt/theory_arith.h
View file

@ -156,9 +156,9 @@ namespace smt {
row_entry & operator[](unsigned idx) { return m_entries[idx]; }
row_entry const & operator[](unsigned idx) const { return m_entries[idx]; }
typename vector<row_entry>::iterator begin_entries() { return m_entries.begin(); }
const typename vector<row_entry>::const_iterator begin_entries() const { return m_entries.begin(); }
typename vector<row_entry>::const_iterator begin_entries() const { return m_entries.begin(); }
typename vector<row_entry>::iterator end_entries() { return m_entries.end(); }
const typename vector<row_entry>::const_iterator end_entries() const { return m_entries.end(); }
typename vector<row_entry>::const_iterator end_entries() const { return m_entries.end(); }
row_entry & add_row_entry(int & pos_idx);
void del_row_entry(unsigned idx);
void compress(vector<column> & cols);
@ -195,9 +195,9 @@ namespace smt {
col_entry & operator[](unsigned idx) { return m_entries[idx]; }
col_entry const & operator[](unsigned idx) const { return m_entries[idx]; }
typename svector<col_entry>::iterator begin_entries() { return m_entries.begin(); }
const typename svector<col_entry>::const_iterator begin_entries() const { return m_entries.begin(); }
typename svector<col_entry>::const_iterator begin_entries() const { return m_entries.begin(); }
typename svector<col_entry>::iterator end_entries() { return m_entries.end(); }
const typename svector<col_entry>::const_iterator end_entries() const { return m_entries.end(); }
typename svector<col_entry>::const_iterator end_entries() const { return m_entries.end(); }
col_entry & add_col_entry(int & pos_idx);
void del_col_entry(unsigned idx);
};
@ -541,9 +541,9 @@ namespace smt {
bool process_atoms() const;
unsigned get_num_conflicts() const { return m_num_conflicts; }
var_kind get_var_kind(theory_var v) const { return m_data[v].kind(); }
bool is_base(theory_var v) const { return get_var_kind(v) == BASE; }
bool is_quasi_base(theory_var v) const { return get_var_kind(v) == QUASI_BASE; }
bool is_non_base(theory_var v) const { return get_var_kind(v) == NON_BASE; }
bool is_base(theory_var v) const { return v != null_theory_var && get_var_kind(v) == BASE; }
bool is_quasi_base(theory_var v) const { return v != null_theory_var && get_var_kind(v) == QUASI_BASE; }
bool is_non_base(theory_var v) const { return v != null_theory_var && get_var_kind(v) == NON_BASE; }
void set_var_kind(theory_var v, var_kind k) { m_data[v].m_kind = k; }
unsigned get_var_row(theory_var v) const { SASSERT(!is_non_base(v)); return m_data[v].m_row_id; }
void set_var_row(theory_var v, unsigned r_id) { m_data[v].m_row_id = r_id; }

16
src/smt/theory_arith_aux.h
View file

@ -491,13 +491,21 @@ namespace smt {
if (!it->is_dead()) {
unsigned rid = it->m_row_id;
row & r = m_rows[rid];
if (is_base(r.get_base_var()))
theory_var v = r.get_base_var();
if (v == null_theory_var) {
// skip
}
else if (is_base(v)) {
return it;
}
else if (quasi_base_rid == -1)
quasi_base_rid = rid;
}
}
SASSERT(quasi_base_rid != -1); // since c.size() != 0
if (quasi_base_rid == -1) {
return nullptr;
}
quasi_base_row2base_row(quasi_base_rid);
// There is no guarantee that v is still a variable of row quasi_base_rid.
@ -1073,7 +1081,7 @@ namespace smt {
/**
\brief: Create an atom that enforces the inequality v > val
The arithmetical expression encoding the inequality suffices
for the theory of aritmetic.
for the theory of arithmetic.
*/
template<typename Ext>
expr_ref theory_arith<Ext>::mk_gt(theory_var v) {
@ -1146,7 +1154,7 @@ namespace smt {
template<typename Ext>
void theory_arith<Ext>::enable_record_conflict(expr* bound) {
m_params.m_arith_bound_prop = BP_NONE;
SASSERT(propagation_mode() == BP_NONE); // bound propagtion rules are not (yet) handled.
SASSERT(propagation_mode() == BP_NONE); // bound propagation rules are not (yet) handled.
if (bound) {
context& ctx = get_context();
m_bound_watch = ctx.get_bool_var(bound);

7
src/smt/theory_arith_core.h
View file

@ -503,7 +503,7 @@ namespace smt {
tout << "lower: " << lower << "\n";
tout << "upper: " << upper << "\n";);
mk_axiom(eqz, eq, true);
mk_axiom(eqz, eq, false);
mk_axiom(eqz, lower, false);
mk_axiom(eqz, upper, !m_util.is_numeral(abs_divisor));
rational k;
@ -3128,7 +3128,7 @@ namespace smt {
//
// 1) Handling inequalities: (n1, k1) <= (n2, k2)
//
// The only intersting case is n1 < n2 and k1 > k2.
// The only interesting case is n1 < n2 and k1 > k2.
// Using the definition of infinitesimal numbers
// we have:
// n1 + k1 * epsilon <= n2 + k2 - epsilon
@ -3302,7 +3302,6 @@ namespace smt {
return b && to_expr(b->get_value(), is_int(v), r);
}
template<typename Ext>
bool theory_arith<Ext>::get_lower(enode * n, rational& r, bool& is_strict) {
theory_var v = n->get_th_var(get_id());
@ -3533,7 +3532,7 @@ namespace smt {
}
/**
\brief reset and retrieve built-in explanation hints for arithmetic lemmmas.
\brief reset and retrieve built-in explanation hints for arithmetic lemmas.
*/
template<typename Ext>

6
src/smt/theory_arith_nl.h
View file

@ -1337,7 +1337,7 @@ namespace smt {
}
/**
\brief Diplay a nested form expression
\brief Display a nested form expression
*/
template<typename Ext>
void theory_arith<Ext>::display_nested_form(std::ostream & out, expr * p) {
@ -1682,7 +1682,7 @@ namespace smt {
if (!get_manager().int_real_coercions() && is_mixed_real_integer(r))
return true; // giving up... see comment above
TRACE("cross_nested", tout << "cheking problematic row...\n";);
TRACE("cross_nested", tout << "checking problematic row...\n";);
rational c = rational::one();
if (is_integer(r))
@ -1764,7 +1764,7 @@ namespace smt {
updated with the fixed variables in m. A variable is only
added to dep if it is not already in already_found.
Return null if the monomial was simplied to 0.
Return null if the monomial was simplified to 0.
*/
template<typename Ext>
grobner::monomial * theory_arith<Ext>::mk_gb_monomial(rational const & _coeff, expr * m, grobner & gb, v_dependency * & dep, var_set & already_found) {

77
src/smt/theory_datatype.cpp
View file

@ -365,7 +365,7 @@ namespace smt {
if (!is_recognizer(n))
return;
TRACE("datatype", tout << "assigning recognizer: #" << n->get_owner_id() << " is_true: " << is_true << "\n"
<< mk_bounded_pp(n->get_owner(), get_manager()) << "\n";);
<< enode_pp(n, ctx) << "\n";);
SASSERT(n->get_num_args() == 1);
enode * arg = n->get_arg(0);
theory_var tv = arg->get_th_var(get_id());
@ -393,11 +393,10 @@ namespace smt {
}
void theory_datatype::relevant_eh(app * n) {
TRACE("datatype", tout << "relevant_eh: " << mk_bounded_pp(n, get_manager()) << "\n";);
context & ctx = get_context();
TRACE("datatype", tout << "relevant_eh: " << mk_pp(n, get_manager()) << "\n";);
SASSERT(ctx.relevancy());
if (is_recognizer(n)) {
TRACE("datatype", tout << "relevant_eh: #" << n->get_id() << "\n" << mk_bounded_pp(n, get_manager()) << "\n";);
SASSERT(ctx.e_internalized(n));
enode * e = ctx.get_enode(n);
theory_var v = e->get_arg(0)->get_th_var(get_id());
@ -483,31 +482,41 @@ namespace smt {
SASSERT(app->get_root() == root->get_root());
if (app != root)
m_used_eqs.push_back(enode_pair(app, root));
TRACE("datatype",
tout << "occurs_check\n";
for (enode_pair const& p : m_used_eqs) {
tout << enode_eq_pp(p, get_context());
});
}
// start exploring subgraph below `app`
bool theory_datatype::occurs_check_enter(enode * app) {
oc_mark_on_stack(app);
theory_var v = app->get_root()->get_th_var(get_id());
if (v != null_theory_var) {
v = m_find.find(v);
var_data * d = m_var_data[v];
if (d->m_constructor) {
for (enode * arg : enode::args(d->m_constructor)) {
if (oc_cycle_free(arg)) {
continue;
}
if (oc_on_stack(arg)) {
// arg was explored before app, and is still on the stack: cycle
occurs_check_explain(app, arg);
return true;
}
// explore `arg` (with parent `app`)
if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) {
m_parent.insert(arg->get_root(), app);
oc_push_stack(arg);
}
}
app = app->get_root();
theory_var v = app->get_th_var(get_id());
if (v == null_theory_var) {
return false;
}
v = m_find.find(v);
var_data * d = m_var_data[v];
if (!d->m_constructor) {
return false;
}
enode * parent = d->m_constructor;
oc_mark_on_stack(parent);
for (enode * arg : enode::args(parent)) {
if (oc_cycle_free(arg)) {
continue;
}
if (oc_on_stack(arg)) {
// arg was explored before app, and is still on the stack: cycle
occurs_check_explain(parent, arg);
return true;
}
// explore `arg` (with paren)
if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) {
m_parent.insert(arg->get_root(), parent);
oc_push_stack(arg);
}
}
return false;
@ -521,7 +530,7 @@ namespace smt {
a3 = cons(v3, a1)
*/
bool theory_datatype::occurs_check(enode * n) {
TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), get_manager()) << "\n";);
TRACE("datatype", tout << "occurs check: " << enode_pp(n, get_context()) << "\n";);
m_stats.m_occurs_check++;
bool res = false;
@ -535,7 +544,7 @@ namespace smt {
if (oc_cycle_free(app)) continue;
TRACE("datatype", tout << "occurs check loop: #" << app->get_owner_id() << " " << mk_bounded_pp(app->get_owner(), get_manager()) << (op==ENTER?" enter":" exit")<< "\n";);
TRACE("datatype", tout << "occurs check loop: " << enode_pp(app, get_context()) << (op==ENTER?" enter":" exit")<< "\n";);
switch (op) {
case ENTER:
@ -553,12 +562,6 @@ namespace smt {
context & ctx = get_context();
region & r = ctx.get_region();
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, m_used_eqs.size(), m_used_eqs.c_ptr())));
TRACE("datatype",
tout << "occurs_check: true\n";
for (enode_pair const& p : m_used_eqs) {
tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n";
tout << mk_bounded_pp(p.first->get_owner(), get_manager()) << " " << mk_bounded_pp(p.second->get_owner(), get_manager()) << "\n";
});
}
return res;
}
@ -613,7 +616,7 @@ namespace smt {
var_data * d = m_var_data[v];
out << "v" << v << " #" << get_enode(v)->get_owner_id() << " -> v" << m_find.find(v) << " ";
if (d->m_constructor)
out << mk_bounded_pp(d->m_constructor->get_owner(), get_manager());
out << enode_pp(d->m_constructor, get_context());
else
out << "(null)";
out << "\n";
@ -778,11 +781,11 @@ namespace smt {
SASSERT(!lits.empty());
region & reg = ctx.get_region();
TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_owner(), get_manager()) << "\n";
for (unsigned i = 0; i < lits.size(); i++) {
ctx.display_detailed_literal(tout, lits[i]); tout << "\n";
for (literal l : lits) {
ctx.display_detailed_literal(tout, l); tout << "\n";
}
for (unsigned i = 0; i < eqs.size(); i++) {
tout << mk_ismt2_pp(eqs[i].first->get_owner(), get_manager()) << " = " << mk_ismt2_pp(eqs[i].second->get_owner(), get_manager()) << "\n";
for (auto const& p : eqs) {
tout << enode_eq_pp(p, ctx);
});
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), reg, lits.size(), lits.c_ptr(), eqs.size(), eqs.c_ptr())));
}

2
src/smt/theory_dense_diff_logic_def.h
View file

@ -756,7 +756,7 @@ namespace smt {
(n_x, k_x) <= (n_y + n_c, k_y + k_c)
The only intersting case is n_x < n_y + n_c and k_x > k_y + k_c.
The only interesting case is n_x < n_y + n_c and k_x > k_y + k_c.
Using the definition of infinitesimal numbers
we have:

1071
src/smt/theory_jobscheduler.cpp Normal file
View file

File diff suppressed because it is too large Load diff

244
src/smt/theory_jobscheduler.h Normal file
View file

@ -0,0 +1,244 @@
/*++
Copyright (c) 2018 Microsoft Corporation
Module Name:
theory_jobscheduling.h
Abstract:
Propagation solver for jobscheduling problems.
It relies on an external module to tighten bounds of
job variables.
Author:
Nikolaj Bjorner (nbjorner) 2018-09-08.
Revision History:
--*/
#pragma once
#include "util/uint_set.h"
#include "ast/csp_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "smt/smt_theory.h"
namespace smt {
typedef uint64_t time_t;
class theory_jobscheduler : public theory {
public:
typedef svector<symbol> properties;
protected:
struct job_resource {
unsigned m_resource_id; // id of resource
time_t m_capacity; // amount of resource to use
unsigned m_loadpct; // assuming loadpct
time_t m_end; // must run before
properties m_properties;
job_resource(unsigned r, time_t cap, unsigned loadpct, time_t end, properties const& ps):
m_resource_id(r), m_capacity(cap), m_loadpct(loadpct), m_end(end), m_properties(ps) {}
};
struct job_time {
unsigned m_job;
time_t m_time;
job_time(unsigned j, time_t time): m_job(j), m_time(time) {}
struct compare {
bool operator()(job_time const& jt1, job_time const& jt2) const {
return jt1.m_time < jt2.m_time;
}
};
};
struct job_info {
bool m_is_preemptable; // can job be pre-empted
vector<job_resource> m_resources; // resources allowed to run job.
u_map<unsigned> m_resource2index; // resource to index into vector
enode* m_job;
enode* m_start;
enode* m_end;
enode* m_job2resource;
bool m_is_bound;
job_info(): m_is_preemptable(false), m_job(nullptr), m_start(nullptr), m_end(nullptr), m_job2resource(nullptr), m_is_bound(false) {}
};
struct res_available {
unsigned m_loadpct;
time_t m_start;
time_t m_end;
properties m_properties;
res_available(unsigned load_pct, time_t start, time_t end, properties const& ps):
m_loadpct(load_pct),
m_start(start),
m_end(end),
m_properties(ps)
{}
struct compare {
bool operator()(res_available const& ra1, res_available const& ra2) const {
return ra1.m_start < ra2.m_start;
}
};
};
struct res_info {
unsigned_vector m_jobs; // jobs allocated to run on resource
vector<res_available> m_available; // time intervals where resource is available
time_t m_end; // can't run after
enode* m_resource;
enode* m_makespan;
res_info(): m_end(std::numeric_limits<time_t>::max()), m_resource(nullptr), m_makespan(nullptr) {}
};
ast_manager& m;
csp_util u;
arith_util a;
vector<job_info> m_jobs;
vector<res_info> m_resources;
unsigned_vector m_bound_jobs;
unsigned m_bound_qhead;
struct scope {
unsigned m_bound_jobs_lim;
unsigned m_bound_qhead;
};
svector<scope> m_scopes;
protected:
theory_var mk_var(enode * n) override;
bool internalize_atom(app * atom, bool gate_ctx) override;
bool internalize_term(app * term) override;
void assign_eh(bool_var v, bool is_true) override {}
void new_eq_eh(theory_var v1, theory_var v2) override;
void new_diseq_eh(theory_var v1, theory_var v2) override;
void push_scope_eh() override;
void pop_scope_eh(unsigned num_scopes) override;
final_check_status final_check_eh() override;
bool can_propagate() override;
void propagate() override;
public:
theory_jobscheduler(ast_manager& m);
~theory_jobscheduler() override {}
void display(std::ostream & out) const override;
void collect_statistics(::statistics & st) const override;
bool include_func_interp(func_decl* f) override;
void init_model(model_generator & m) override;
model_value_proc * mk_value(enode * n, model_generator & mg) override;
bool get_value(enode * n, expr_ref & r) override;
theory * mk_fresh(context * new_ctx) override;
public:
// set up job/resource global constraints
void set_preemptable(unsigned j, bool is_preemptable);
void add_job_resource(unsigned j, unsigned r, unsigned loadpct, time_t cap, time_t end, properties const& ps);
void add_resource_available(unsigned r, unsigned max_loadpct, time_t start, time_t end, properties const& ps);
void add_done();
// assignments
time_t est(unsigned j); // earliest start time of job j
time_t lst(unsigned j); // last start time
time_t ect(unsigned j); // earliest completion time
time_t lct(unsigned j); // last completion time
time_t start(unsigned j); // start time of job j
time_t end(unsigned j); // end time of job j
time_t get_lo(expr* e);
time_t get_up(expr* e);
time_t get_value(expr* e);
unsigned resource(unsigned j); // resource of job j
// derived bounds
time_t ect(unsigned j, unsigned r, time_t start);
bool lst(unsigned j, unsigned r, time_t& t);
bool resource_available(job_resource const& jr, res_available const& ra) const;
bool first_available(job_resource const& jr, res_info const& ri, unsigned& idx) const;
bool last_available(job_resource const& jr, res_info const& ri, unsigned& idx) const;
time_t solve_for_start(unsigned load_pct, unsigned job_load_pct, time_t end, time_t cap);
time_t solve_for_end(unsigned load_pct, unsigned job_load_pct, time_t start, time_t cap);
time_t solve_for_capacity(unsigned load_pct, unsigned job_load_pct, time_t start, time_t end);
// validate assignment
void validate_assignment();
bool resource_available(unsigned r, time_t t, unsigned& idx); // load available on resource r at time t.
time_t capacity_used(unsigned j, unsigned r, time_t start, time_t end); // capacity used between start and end
job_resource const& get_job_resource(unsigned j, unsigned r) const;
// propagation
void propagate_end_time(unsigned j, unsigned r);
void propagate_job2resource(unsigned j, unsigned r);
// final check constraints
bool constrain_end_time_interval(unsigned j, unsigned r);
bool constrain_resource_energy(unsigned r);
bool split_job2resource(unsigned j);
void assert_last_end_time(unsigned j, unsigned r, job_resource const& jr, literal eq);
void assert_last_start_time(unsigned j, unsigned r, literal eq);
void assert_first_start_time(unsigned j, unsigned r, literal eq);
void assert_job_not_in_gap(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq);
void assert_job_non_preemptable(unsigned j, unsigned r, unsigned idx, unsigned idx1, literal eq);
void block_job_overlap(unsigned r, uint_set const& jobs, unsigned last_job);
class job_overlap {
time_t m_start;
vector<job_time> & m_starts, &m_ends;
unsigned s_idx, e_idx; // index into starts/ends
uint_set m_jobs;
public:
job_overlap(vector<job_time>& starts, vector<job_time>& ends);
bool next();
uint_set const& jobs() const { return m_jobs; }
};
// term builders
literal mk_ge(expr* e, time_t t);
expr* mk_ge_expr(expr* e, time_t t);
literal mk_ge(enode* e, time_t t);
literal mk_le(expr* e, time_t t);
expr* mk_le_expr(expr* e, time_t t);
literal mk_le(enode* e, time_t t);
literal mk_le(enode* l, enode* r);
literal mk_literal(expr* e);
literal mk_eq_lit(enode * l, enode * r) { return mk_eq_lit(l->get_owner(), r->get_owner()); }
literal mk_eq_lit(expr * l, expr * r);
void internalize_cmd(expr* cmd);
void unrecognized_argument(expr* arg) { invalid_argument("unrecognized argument ", arg); }
void invalid_argument(char const* msg, expr* arg);
std::ostream& display(std::ostream & out, res_info const& r) const;
std::ostream& display(std::ostream & out, res_available const& r) const;
std::ostream& display(std::ostream & out, job_info const& r) const;
std::ostream& display(std::ostream & out, job_resource const& r) const;
};
};

18
src/smt/theory_lra.cpp
View file

@ -1361,8 +1361,7 @@ public:
}
enode* n2 = get_enode(other);
if (n1->get_root() != n2->get_root()) {
TRACE("arith", tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
tout << mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";
TRACE("arith", tout << enode_eq_pp(enode_pair(n1, n2), ctx());
tout << "v" << v << " = " << "v" << other << "\n";);
m_assume_eq_candidates.push_back(std::make_pair(v, other));
result = true;
@ -2800,15 +2799,15 @@ public:
get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr));
TRACE("arith",
for (unsigned i = 0; i < m_core.size(); ++i) {
ctx().display_detailed_literal(tout, m_core[i]);
for (literal c : m_core) {
ctx().display_detailed_literal(tout, c);
tout << "\n";
}
for (unsigned i = 0; i < m_eqs.size(); ++i) {
tout << mk_pp(m_eqs[i].first->get_owner(), m) << " = " << mk_pp(m_eqs[i].second->get_owner(), m) << "\n";
for (enode_pair const& p : m_eqs) {
tout << enode_eq_pp(p, ctx());
}
tout << " ==> ";
tout << mk_pp(x->get_owner(), m) << " = " << mk_pp(y->get_owner(), m) << "\n";
tout << enode_pp(x, ctx()) << " = " << enode_pp(y, ctx()) << "\n";
);
// parameters are TBD.
@ -3225,7 +3224,7 @@ public:
theory_var w;
if (m_solver->is_term(ti.var())) {
//w = m_term_index2theory_var.get(m_solver->adjust_term_index(ti.var()), null_theory_var);
//if (w == null_theory_var) // if extracing expressions directly from nested term
//if (w == null_theory_var) // if extracting expressions directly from nested term
lp::lar_term const& term1 = m_solver->get_term(ti.var());
rational coeff2 = coeff * ti.coeff();
term2coeffs(term1, coeffs, coeff2, offset);
@ -3371,8 +3370,7 @@ public:
break;
}
case equality_source:
out << mk_pp(m_equalities[idx].first->get_owner(), m) << " = "
<< mk_pp(m_equalities[idx].second->get_owner(), m) << "\n";
out << enode_eq_pp(m_equalities[idx], ctx());
break;
case definition_source: {
theory_var v = m_definitions[idx];

4
src/smt/theory_pb.h
View file

@ -107,7 +107,7 @@ namespace smt {
struct ineq {
unsynch_mpz_manager& m_mpz; // mpz manager.
literal m_lit; // literal repesenting predicate
literal m_lit; // literal representing predicate
bool m_is_eq; // is this an = or >=.
arg_t m_args[2]; // encode args[0]*coeffs[0]+...+args[n-1]*coeffs[n-1] >= k();
// Watch the first few positions until the sum satisfies:
@ -192,7 +192,7 @@ namespace smt {
// If none are available, then perform unit propagation.
//
class card {
literal m_lit; // literal repesenting predicate
literal m_lit; // literal representing predicate
literal_vector m_args;
unsigned m_bound;
unsigned m_num_propagations;

452
src/smt/theory_recfun.cpp Normal file
View file

@ -0,0 +1,452 @@
/*++
Copyright (c) 2018 Microsoft Corporation, Simon Cuares
Module Name:
theory_recfun.cpp
Abstract:
Theory responsible for unrolling recursive functions
Author:
Simon Cuares December 2017
Revision History:
--*/
#include "util/stats.h"
#include "ast/ast_util.h"
#include "ast/for_each_expr.h"
#include "smt/theory_recfun.h"
#include "smt/params/smt_params_helper.hpp"
#define TRACEFN(x) TRACE("recfun", tout << x << '\n';)
namespace smt {
theory_recfun::theory_recfun(ast_manager & m)
: theory(m.mk_family_id("recfun")),
m(m),
m_plugin(*reinterpret_cast<recfun::decl::plugin*>(m.get_plugin(get_family_id()))),
m_util(m_plugin.u()),
m_preds(m),
m_max_depth(0),
m_q_case_expand(),
m_q_body_expand()
{
}
theory_recfun::~theory_recfun() {
reset_queues();
}
char const * theory_recfun::get_name() const { return "recfun"; }
theory* theory_recfun::mk_fresh(context* new_ctx) {
return alloc(theory_recfun, new_ctx->get_manager());
}
void theory_recfun::init(context* ctx) {
theory::init(ctx);
smt_params_helper p(ctx->get_params());
m_max_depth = p.recfun_depth();
if (m_max_depth < 2) m_max_depth = 2;
}
void theory_recfun::init_search_eh() {
}
bool theory_recfun::internalize_atom(app * atom, bool gate_ctx) {
TRACEFN(mk_pp(atom, m));
if (!u().has_defs()) {
return false;
}
for (expr * arg : *atom) {
ctx().internalize(arg, false);
}
if (!ctx().e_internalized(atom)) {
ctx().mk_enode(atom, false, true, false);
}
if (!ctx().b_internalized(atom)) {
bool_var v = ctx().mk_bool_var(atom);
ctx().set_var_theory(v, get_id());
}
return true;
}
bool theory_recfun::internalize_term(app * term) {
if (!u().has_defs()) {
return false;
}
for (expr* e : *term) {
ctx().internalize(e, false);
}
// the internalization of the arguments may have triggered the internalization of term.
if (!ctx().e_internalized(term)) {
ctx().mk_enode(term, false, false, true);
}
return true;
}
void theory_recfun::reset_queues() {
for (auto* e : m_q_case_expand) {
dealloc(e);
}
m_q_case_expand.reset();
for (auto* e : m_q_body_expand) {
dealloc(e);
}
m_q_body_expand.reset();
m_q_clauses.clear();
}
void theory_recfun::reset_eh() {
reset_queues();
m_stats.reset();
theory::reset_eh();
}
/*
* when `n` becomes relevant, if it's `f(t1...tn)` with `f` defined,
* then case-expand `n`. If it's a macro we can also immediately
* body-expand it.
*/
void theory_recfun::relevant_eh(app * n) {
SASSERT(ctx().relevancy());
if (u().is_defined(n) && u().has_defs()) {
TRACEFN("relevant_eh: (defined) " << mk_pp(n, m));
push_case_expand(alloc(case_expansion, u(), n));
}
}
void theory_recfun::push_scope_eh() {
theory::push_scope_eh();
m_preds_lim.push_back(m_preds.size());
}
void theory_recfun::pop_scope_eh(unsigned num_scopes) {
theory::pop_scope_eh(num_scopes);
reset_queues();
// restore depth book-keeping
unsigned new_lim = m_preds_lim.size()-num_scopes;
#if 0
// depth tracking of recursive unfolding is
// turned off when enabling this code:
unsigned start = m_preds_lim[new_lim];
for (unsigned i = start; i < m_preds.size(); ++i) {
m_pred_depth.remove(m_preds.get(i));
}
m_preds.resize(start);
#endif
m_preds_lim.shrink(new_lim);
}
void theory_recfun::restart_eh() {
TRACEFN("restart");
reset_queues();
theory::restart_eh();
}
bool theory_recfun::can_propagate() {
return ! (m_q_case_expand.empty() &&
m_q_body_expand.empty() &&
m_q_clauses.empty());
}
void theory_recfun::propagate() {
for (literal_vector & c : m_q_clauses) {
TRACEFN("add axiom " << pp_lits(ctx(), c));
ctx().mk_th_axiom(get_id(), c);
}
m_q_clauses.clear();
for (unsigned i = 0; i < m_q_case_expand.size(); ++i) {
case_expansion* e = m_q_case_expand[i];
if (e->m_def->is_fun_macro()) {
// body expand immediately
assert_macro_axiom(*e);
}
else {
// case expand
SASSERT(e->m_def->is_fun_defined());
assert_case_axioms(*e);
}
dealloc(e);
m_q_case_expand[i] = nullptr;
}
m_stats.m_case_expansions += m_q_case_expand.size();
m_q_case_expand.reset();
for (unsigned i = 0; i < m_q_body_expand.size(); ++i) {
assert_body_axiom(*m_q_body_expand[i]);
dealloc(m_q_body_expand[i]);
m_q_body_expand[i] = nullptr;
}
m_stats.m_body_expansions += m_q_body_expand.size();
m_q_body_expand.reset();
}
/**
* make clause `depth_limit => ~guard`
* the guard appears at a depth below the current cutoff.
*/
void theory_recfun::assert_max_depth_limit(expr* guard) {
literal_vector c;
app_ref dlimit = m_util.mk_depth_limit_pred(m_max_depth);
c.push_back(~mk_literal(dlimit));
c.push_back(~mk_literal(guard));
TRACEFN("max-depth limit: add clause " << pp_lits(ctx(), c));
m_q_clauses.push_back(std::move(c));
}
/**
* retrieve depth associated with predicate or expression.
*/
unsigned theory_recfun::get_depth(expr* e) {
SASSERT(u().is_defined(e) || u().is_case_pred(e));
unsigned d = 0;
m_pred_depth.find(e, d);
TRACEFN("depth " << d << " " << mk_pp(e, m));
return d;
}
/**
* Update depth of subterms of e with respect to d.
*/
void theory_recfun::set_depth_rec(unsigned d, expr* e) {
struct insert_c {
theory_recfun& th;
unsigned m_depth;
insert_c(theory_recfun& th, unsigned d): th(th), m_depth(d) {}
void operator()(app* e) { th.set_depth(m_depth, e); }
void operator()(quantifier*) {}
void operator()(var*) {}
};
insert_c proc(*this, d);
for_each_expr(proc, e);
}
void theory_recfun::set_depth(unsigned depth, expr* e) {
if ((u().is_defined(e) || u().is_case_pred(e)) && !m_pred_depth.contains(e)) {
m_pred_depth.insert(e, depth);
m_preds.push_back(e);
TRACEFN("depth " << depth << " : " << mk_pp(e, m));
}
}
/**
* if `is_true` and `v = C_f_i(t1...tn)`,
* then body-expand i-th case of `f(t1...tn)`
*/
void theory_recfun::assign_eh(bool_var v, bool is_true) {
expr* e = ctx().bool_var2expr(v);
if (is_true && u().is_case_pred(e)) {
TRACEFN("assign_case_pred_true " << mk_pp(e, m));
// body-expand
push_body_expand(alloc(body_expansion, u(), to_app(e)));
}
}
// replace `vars` by `args` in `e`
expr_ref theory_recfun::apply_args(
unsigned depth,
recfun::vars const & vars,
ptr_vector<expr> const & args,
expr * e) {
SASSERT(is_standard_order(vars));
var_subst subst(m, true);
expr_ref new_body(m);
new_body = subst(e, args.size(), args.c_ptr());
ctx().get_rewriter()(new_body); // simplify
set_depth_rec(depth + 1, new_body);
return new_body;
}
literal theory_recfun::mk_literal(expr* e) {
ctx().internalize(e, false);
literal lit = ctx().get_literal(e);
ctx().mark_as_relevant(lit);
return lit;
}
literal theory_recfun::mk_eq_lit(expr* l, expr* r) {
literal lit;
if (m.is_true(r) || m.is_false(r)) {
std::swap(l, r);
}
if (m.is_true(l)) {
lit = mk_literal(r);
}
else if (m.is_false(l)) {
lit = ~mk_literal(r);
}
else {
lit = mk_eq(l, r, false);
}
ctx().mark_as_relevant(lit);
return lit;
}
/**
* For functions f(args) that are given as macros f(vs) = rhs
*
* 1. substitute `e.args` for `vs` into the macro rhs
* 2. add unit clause `f(args) = rhs`
*/
void theory_recfun::assert_macro_axiom(case_expansion & e) {
m_stats.m_macro_expansions++;
TRACEFN("case expansion " << pp_case_expansion(e, m) << "\n");
SASSERT(e.m_def->is_fun_macro());
auto & vars = e.m_def->get_vars();
expr_ref lhs(e.m_lhs, m);
unsigned depth = get_depth(e.m_lhs);
expr_ref rhs(apply_args(depth, vars, e.m_args, e.m_def->get_rhs()), m);
literal lit = mk_eq_lit(lhs, rhs);
ctx().mk_th_axiom(get_id(), 1, &lit);
TRACEFN("macro expansion yields " << mk_pp(rhs, m) << "\n" <<
"literal " << pp_lit(ctx(), lit));
}
/**
* Add case axioms for every case expansion path.
*
* assert `p(args) <=> And(guards)` (with CNF on the fly)
*
* also body-expand paths that do not depend on any defined fun
*/
void theory_recfun::assert_case_axioms(case_expansion & e) {
TRACEFN("assert_case_axioms "<< pp_case_expansion(e,m)
<< " with " << e.m_def->get_cases().size() << " cases");
SASSERT(e.m_def->is_fun_defined());
// add case-axioms for all case-paths
auto & vars = e.m_def->get_vars();
literal_vector preds;
for (recfun::case_def const & c : e.m_def->get_cases()) {
// applied predicate to `args`
app_ref pred_applied = c.apply_case_predicate(e.m_args);
// cut off cases below max-depth
unsigned depth = get_depth(e.m_lhs);
set_depth(depth, pred_applied);
SASSERT(u().owns_app(pred_applied));
literal concl = mk_literal(pred_applied);
preds.push_back(concl);
if (c.is_immediate()) {
body_expansion be(pred_applied, c, e.m_args);
assert_body_axiom(be);
}
else if (depth >= m_max_depth) {
assert_max_depth_limit(pred_applied);
continue;
}
literal_vector guards;
guards.push_back(concl);
for (auto & g : c.get_guards()) {
expr_ref ga = apply_args(depth, vars, e.m_args, g);
literal guard = mk_literal(ga);
guards.push_back(~guard);
literal c[2] = {~concl, guard};
ctx().mk_th_axiom(get_id(), 2, c);
}
ctx().mk_th_axiom(get_id(), guards);
}
// the disjunction of branches is asserted
// to close the available cases.
ctx().mk_th_axiom(get_id(), preds);
}
/**
* For a guarded definition guards => f(vars) = rhs
* and occurrence f(args)
*
* substitute `args` for `vars` in guards, and rhs
* add axiom guards[args/vars] => f(args) = rhs[args/vars]
*
*/
void theory_recfun::assert_body_axiom(body_expansion & e) {
recfun::def & d = *e.m_cdef->get_def();
auto & vars = d.get_vars();
auto & args = e.m_args;
SASSERT(is_standard_order(vars));
unsigned depth = get_depth(e.m_pred);
expr_ref lhs(u().mk_fun_defined(d, args), m);
expr_ref rhs = apply_args(depth, vars, args, e.m_cdef->get_rhs());
literal_vector clause;
for (auto & g : e.m_cdef->get_guards()) {
expr_ref guard = apply_args(depth, vars, args, g);
clause.push_back(~mk_literal(guard));
if (clause.back() == true_literal) {
TRACEFN("body " << pp_body_expansion(e,m) << "\n" << clause << "\n" << guard);
return;
}
if (clause.back() == false_literal) {
clause.pop_back();
}
}
clause.push_back(mk_eq_lit(lhs, rhs));
ctx().mk_th_axiom(get_id(), clause);
TRACEFN("body " << pp_body_expansion(e,m));
TRACEFN(pp_lits(ctx(), clause));
}
final_check_status theory_recfun::final_check_eh() {
TRACEFN("final\n");
if (can_propagate()) {
propagate();
return FC_CONTINUE;
}
return FC_DONE;
}
void theory_recfun::add_theory_assumptions(expr_ref_vector & assumptions) {
if (u().has_defs()) {
app_ref dlimit = m_util.mk_depth_limit_pred(m_max_depth);
TRACEFN("add_theory_assumption " << mk_pp(dlimit.get(), m));
assumptions.push_back(dlimit);
}
}
// if `dlimit` occurs in unsat core, return 'true'
bool theory_recfun::should_research(expr_ref_vector & unsat_core) {
for (auto & e : unsat_core) {
if (u().is_depth_limit(e)) {
m_max_depth = (3 * m_max_depth) / 2;
IF_VERBOSE(1, verbose_stream() << "(smt.recfun :increase-depth " << m_max_depth << ")\n");
return true;
}
}
return false;
}
void theory_recfun::display(std::ostream & out) const {
out << "recfun{}";
}
void theory_recfun::collect_statistics(::statistics & st) const {
st.update("recfun macro expansion", m_stats.m_macro_expansions);
st.update("recfun case expansion", m_stats.m_case_expansions);
st.update("recfun body expansion", m_stats.m_body_expansions);
}
std::ostream& operator<<(std::ostream & out, theory_recfun::pp_case_expansion const & e) {
return out << "case_exp(" << mk_pp(e.e.m_lhs, e.m) << ")";
}
std::ostream& operator<<(std::ostream & out, theory_recfun::pp_body_expansion const & e) {
out << "body_exp(" << e.e.m_cdef->get_decl()->get_name();
for (auto* t : e.e.m_args) {
out << " " << mk_pp(t,e.m);
}
return out << ")";
}
}

163
src/smt/theory_recfun.h Normal file
View file

@ -0,0 +1,163 @@
/*++
Copyright (c) 2018 Microsoft Corporation
Module Name:
theory_recfun.h
Abstract:
Theory responsible for unrolling recursive functions
Author:
Simon Cuares December 2017
Revision History:
--*/
#ifndef THEORY_RECFUN_H_
#define THEORY_RECFUN_H_
#include "smt/smt_theory.h"
#include "smt/smt_context.h"
#include "ast/ast_pp.h"
#include "ast/recfun_decl_plugin.h"
namespace smt {
class theory_recfun : public theory {
struct stats {
unsigned m_case_expansions, m_body_expansions, m_macro_expansions;
void reset() { memset(this, 0, sizeof(stats)); }
stats() { reset(); }
};
// one case-expansion of `f(t1...tn)`
struct case_expansion {
app * m_lhs; // the term to expand
recfun::def * m_def;
ptr_vector<expr> m_args;
case_expansion(recfun::util& u, app * n) :
m_lhs(n), m_def(nullptr), m_args() {
SASSERT(u.is_defined(n));
func_decl * d = n->get_decl();
m_def = &u.get_def(d);
m_args.append(n->get_num_args(), n->get_args());
}
case_expansion(case_expansion const & from)
: m_lhs(from.m_lhs),
m_def(from.m_def),
m_args(from.m_args) {}
case_expansion(case_expansion && from)
: m_lhs(from.m_lhs),
m_def(from.m_def),
m_args(std::move(from.m_args)) {}
};
struct pp_case_expansion {
case_expansion & e;
ast_manager & m;
pp_case_expansion(case_expansion & e, ast_manager & m) : e(e), m(m) {}
};
friend std::ostream& operator<<(std::ostream&, pp_case_expansion const &);
// one body-expansion of `f(t1...tn)` using a `C_f_i(t1...tn)`
struct body_expansion {
app* m_pred;
recfun::case_def const * m_cdef;
ptr_vector<expr> m_args;
body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(0), m_args() {
m_cdef = &u.get_case_def(n);
m_args.append(n->get_num_args(), n->get_args());
}
body_expansion(app* pred, recfun::case_def const & d, ptr_vector<expr> & args) :
m_pred(pred), m_cdef(&d), m_args(args) {}
body_expansion(body_expansion const & from):
m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(from.m_args) {}
body_expansion(body_expansion && from) :
m_pred(from.m_pred), m_cdef(from.m_cdef), m_args(std::move(from.m_args)) {}
};
struct pp_body_expansion {
body_expansion & e;
ast_manager & m;
pp_body_expansion(body_expansion & e, ast_manager & m) : e(e), m(m) {}
};
friend std::ostream& operator<<(std::ostream&, pp_body_expansion const &);
ast_manager& m;
recfun::decl::plugin& m_plugin;
recfun::util& m_util;
stats m_stats;
// book-keeping for depth of predicates
obj_map<expr, unsigned> m_pred_depth;
expr_ref_vector m_preds;
unsigned_vector m_preds_lim;
unsigned m_max_depth; // for fairness and termination
ptr_vector<case_expansion> m_q_case_expand;
ptr_vector<body_expansion> m_q_body_expand;
vector<literal_vector> m_q_clauses;
recfun::util & u() const { return m_util; }
bool is_defined(app * f) const { return u().is_defined(f); }
bool is_case_pred(app * f) const { return u().is_case_pred(f); }
bool is_defined(enode * e) const { return is_defined(e->get_owner()); }
bool is_case_pred(enode * e) const { return is_case_pred(e->get_owner()); }
void reset_queues();
expr_ref apply_args(unsigned depth, recfun::vars const & vars, ptr_vector<expr> const & args, expr * e); //!< substitute variables by args
void assert_macro_axiom(case_expansion & e);
void assert_case_axioms(case_expansion & e);
void assert_body_axiom(body_expansion & e);
literal mk_literal(expr* e);
void assert_max_depth_limit(expr* guard);
unsigned get_depth(expr* e);
void set_depth(unsigned d, expr* e);
void set_depth_rec(unsigned d, expr* e);
literal mk_eq_lit(expr* l, expr* r);
bool is_standard_order(recfun::vars const& vars) const {
return vars.size() == 0 || vars[vars.size()-1]->get_idx() == 0;
}
protected:
void push_case_expand(case_expansion* e) { m_q_case_expand.push_back(e); }
void push_body_expand(body_expansion* e) { m_q_body_expand.push_back(e); }
bool internalize_atom(app * atom, bool gate_ctx) override;
bool internalize_term(app * term) override;
void reset_eh() override;
void relevant_eh(app * n) override;
char const * get_name() const override;
final_check_status final_check_eh() override;
void assign_eh(bool_var v, bool is_true) override;
void push_scope_eh() override;
void pop_scope_eh(unsigned num_scopes) override;
void restart_eh() override;
bool can_propagate() override;
void propagate() override;
bool should_research(expr_ref_vector &) override;
void new_eq_eh(theory_var v1, theory_var v2) override {}
void new_diseq_eh(theory_var v1, theory_var v2) override {}
void add_theory_assumptions(expr_ref_vector & assumptions) override;
void init(context* ctx) override;
public:
theory_recfun(ast_manager & m);
~theory_recfun() override;
theory * mk_fresh(context * new_ctx) override;
void init_search_eh() override;
void display(std::ostream & out) const override;
void collect_statistics(::statistics & st) const override;
};
}
#endif

1380
src/smt/theory_seq.cpp
View file

File diff suppressed because it is too large Load diff

98
src/smt/theory_seq.h
View file

@ -196,23 +196,28 @@ namespace smt {
class nc {
expr_ref m_contains;
literal m_len_gt;
dependency* m_dep;
public:
nc(expr_ref const& c, dependency* dep):
nc(expr_ref const& c, literal len_gt, dependency* dep):
m_contains(c),
m_len_gt(len_gt),
m_dep(dep) {}
nc(nc const& other):
m_contains(other.m_contains),
m_len_gt(other.m_len_gt),
m_dep(other.m_dep) {}
nc& operator=(nc const& other) {
if (this != &other) {
m_contains = other.m_contains;
m_dep = other.m_dep;
m_len_gt = other.m_len_gt;
}
return *this;
}
dependency* deps() const { return m_dep; }
expr_ref const& contains() const { return m_contains; }
literal len_gt() const { return m_len_gt; }
};
class apply {
@ -254,6 +259,18 @@ namespace smt {
}
};
class replay_is_axiom : public apply {
expr_ref m_e;
public:
replay_is_axiom(ast_manager& m, expr* e) : m_e(e, m) {}
~replay_is_axiom() override {}
void operator()(theory_seq& th) override {
th.check_int_string(m_e);
m_e.reset();
}
};
class push_replay : public trail<theory_seq> {
apply* m_apply;
public:
@ -272,6 +289,16 @@ namespace smt {
}
};
struct s_in_re {
literal m_lit;
expr* m_s;
expr* m_re;
eautomaton* m_aut;
bool m_active;
s_in_re(literal l, expr*s, expr* re, eautomaton* aut):
m_lit(l), m_s(s), m_re(re), m_aut(aut), m_active(true) {}
};
void erase_index(unsigned idx, unsigned i);
struct stats {
@ -316,8 +343,7 @@ namespace smt {
unsigned m_axioms_head; // index of first axiom to add.
bool m_incomplete; // is the solver (clearly) incomplete for the fragment.
expr_ref_vector m_int_string;
rational_set m_itos_axioms;
rational_set m_stoi_axioms;
obj_hashtable<expr> m_si_axioms;
obj_hashtable<expr> m_length; // is length applied
scoped_ptr_vector<apply> m_replay; // set of actions to replay
model_generator* m_mg;
@ -337,11 +363,10 @@ namespace smt {
scoped_ptr_vector<eautomaton> m_automata;
obj_map<expr, eautomaton*> m_re2aut;
expr_ref_vector m_res;
unsigned m_max_unfolding_depth;
literal m_max_unfolding_lit;
vector<s_in_re> m_s_in_re;
// queue of asserted atoms
ptr_vector<expr> m_atoms;
unsigned_vector m_atoms_lim;
unsigned m_atoms_qhead;
bool m_new_solution; // new solution added
bool m_new_propagation; // new propagation to core
re2automaton m_mk_aut;
@ -362,6 +387,8 @@ namespace smt {
void pop_scope_eh(unsigned num_scopes) override;
void restart_eh() override;
void relevant_eh(app* n) override;
bool should_research(expr_ref_vector &) override;
void add_theory_assumptions(expr_ref_vector & assumptions) override;
theory* mk_fresh(context* new_ctx) override { return alloc(theory_seq, new_ctx->get_manager(), m_params); }
char const * get_name() const override { return "seq"; }
theory_var mk_var(enode* n) override;
@ -427,6 +454,8 @@ namespace smt {
bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);
bool solve_unit_eq(expr* l, expr* r, dependency* dep);
bool solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep);
bool solve_nth_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
bool solve_itos(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep);
bool is_binary_eq(expr_ref_vector const& l, expr_ref_vector const& r, expr_ref& x, ptr_vector<expr>& xunits, ptr_vector<expr>& yunits, expr_ref& y);
bool is_quat_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x1, expr_ref_vector& xs, expr_ref& x2, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2);
bool is_ternary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref& x, expr_ref_vector& xs, expr_ref& y1, expr_ref_vector& ys, expr_ref& y2, bool flag1);
@ -530,13 +559,14 @@ namespace smt {
bool has_length(expr *e) const { return m_length.contains(e); }
void add_length(expr* e);
void enforce_length(enode* n);
void enforce_length(expr* n);
bool enforce_length(expr_ref_vector const& es, vector<rational>& len);
void enforce_length_coherence(enode* n1, enode* n2);
// model-check the functions that convert integers to strings and the other way.
void add_int_string(expr* e);
bool check_int_string();
bool check_int_string(expr* e);
expr_ref add_elim_string_axiom(expr* n);
void add_at_axiom(expr* n);
@ -545,6 +575,8 @@ namespace smt {
void add_stoi_axiom(expr* n);
bool add_stoi_val_axiom(expr* n);
bool add_itos_val_axiom(expr* n);
void add_si_axiom(expr* s, expr* i, unsigned sz);
void ensure_digit_axiom();
literal is_digit(expr* ch);
expr_ref digit2int(expr* ch);
void add_itos_length_axiom(expr* n);
@ -552,11 +584,13 @@ namespace smt {
literal mk_simplified_literal(expr* n);
literal mk_eq_empty(expr* n, bool phase = true);
literal mk_seq_eq(expr* a, expr* b);
literal mk_preferred_eq(expr* a, expr* b);
void tightest_prefix(expr* s, expr* x);
expr_ref mk_sub(expr* a, expr* b);
expr_ref mk_add(expr* a, expr* b);
expr_ref mk_len(expr* s) const { return expr_ref(m_util.str.mk_length(s), m); }
enode* ensure_enode(expr* a);
enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }
dependency* mk_join(dependency* deps, literal lit);
dependency* mk_join(dependency* deps, literal_vector const& lits);
@ -581,46 +615,34 @@ namespace smt {
literal mk_accept(expr* s, expr* idx, expr* re, expr* state);
literal mk_accept(expr* s, expr* idx, expr* re, unsigned i) { return mk_accept(s, idx, re, m_autil.mk_int(i)); }
bool is_accept(expr* acc) const { return is_skolem(m_accept, acc); }
bool is_accept(expr* acc, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut) {
return is_acc_rej(m_accept, acc, s, idx, re, i, aut);
}
literal mk_reject(expr* s, expr* idx, expr* re, expr* state);
literal mk_reject(expr* s, expr* idx, expr* re, unsigned i) { return mk_reject(s, idx, re, m_autil.mk_int(i)); }
bool is_reject(expr* rej) const { return is_skolem(m_reject, rej); }
bool is_reject(expr* rej, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut) {
return is_acc_rej(m_reject, rej, s, idx, re, i, aut);
}
bool is_acc_rej(symbol const& ar, expr* e, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut);
expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* acc);
bool is_accept(expr* acc, expr*& s, expr*& idx, expr*& re, unsigned& i, eautomaton*& aut);
expr_ref mk_step(expr* s, expr* tail, expr* re, unsigned i, unsigned j, expr* t);
bool is_step(expr* e, expr*& s, expr*& tail, expr*& re, expr*& i, expr*& j, expr*& t) const;
bool is_step(expr* e) const;
void propagate_step(literal lit, expr* n);
bool add_reject2reject(expr* rej, bool& change);
bool add_accept2step(expr* acc, bool& change);
bool add_step2accept(expr* step, bool& change);
bool add_prefix2prefix(expr* e, bool& change);
bool add_suffix2suffix(expr* e, bool& change);
bool add_contains2contains(expr* e, bool& change);
bool is_max_unfolding(expr* e) const { return is_skolem(symbol("seq.max_unfolding_depth"), e); }
expr_ref mk_max_unfolding_depth() {
return mk_skolem(symbol("seq.max_unfolding_depth"),
m_autil.mk_int(m_max_unfolding_depth),
nullptr, nullptr, nullptr, m.mk_bool_sort());
}
void propagate_not_prefix(expr* e);
void propagate_not_prefix2(expr* e);
void propagate_not_suffix(expr* e);
void ensure_nth(literal lit, expr* s, expr* idx);
bool canonizes(bool sign, expr* e);
void propagate_non_empty(literal lit, expr* s);
bool propagate_is_conc(expr* e, expr* conc);
void propagate_acc_rej_length(literal lit, expr* acc_rej);
bool propagate_automata();
void add_atom(expr* e);
void propagate_step(literal lit, expr* n);
void propagate_accept(literal lit, expr* e);
void new_eq_eh(dependency* dep, enode* n1, enode* n2);
// diagnostics
void display_equations(std::ostream& out) const;
void display_equation(std::ostream& out, eq const& e) const;
void display_disequations(std::ostream& out) const;
void display_disequation(std::ostream& out, ne const& e) const;
void display_deps(std::ostream& out, dependency* deps) const;
void display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const;
void display_nc(std::ostream& out, nc const& nc) const;
std::ostream& display_equations(std::ostream& out) const;
std::ostream& display_equation(std::ostream& out, eq const& e) const;
std::ostream& display_disequations(std::ostream& out) const;
std::ostream& display_disequation(std::ostream& out, ne const& e) const;
std::ostream& display_deps(std::ostream& out, dependency* deps) const;
std::ostream& display_deps(std::ostream& out, literal_vector const& lits, enode_pair_vector const& eqs) const;
std::ostream& display_nc(std::ostream& out, nc const& nc) const;
public:
theory_seq(ast_manager& m, theory_seq_params const & params);
~theory_seq() override;

3
src/smt/theory_str.cpp
View file

@ -5074,7 +5074,7 @@ namespace smt {
}
} else {
// ------------------------------------------------------------------------------------------------
// subStr doesn't have an eqc contant value
// subStr doesn't have an eqc constant value
// however, subStr equals to some concat(arg_1, arg_2, ..., arg_n)
// if arg_j is a constant and is not a part of the strConst, it's sure that the contains is false
// ** This check is needed here because the "strConst" and "strAst" may not be in a same eqc yet
@ -10608,7 +10608,6 @@ namespace smt {
std::map<expr*, std::map<expr*, int> > var_eq_concat_map;
int conflictInDep = ctx_dep_analysis(varAppearInAssign, freeVar_map, unrollGroup_map, var_eq_concat_map);
if (conflictInDep == -1) {
// return Z3_TRUE;
return FC_DONE;
}

2
src/smt/uses_theory.cpp
View file

@ -41,7 +41,7 @@ bool uses_theory(expr * n, family_id fid, expr_mark & visited) {
try {
for_each_expr(p, visited, n);
}
catch (uses_theory_ns::found) {
catch (const uses_theory_ns::found &) {
return true;
}
return false;