mirror of
https://github.com/Z3Prover/z3
synced 2025-11-03 21:09:11 +00:00
theory_str params module, WIP
This commit is contained in:
Murphy Berzish
parent
09053b831d
commit
f5bc17b864
7 changed files with 96 additions and 35 deletions
|
|
@ -25,6 +25,7 @@ Revision History:
|
|||
#include"theory_arith_params.h"
|
||||
#include"theory_array_params.h"
|
||||
#include"theory_bv_params.h"
|
||||
#include"theory_str_params.h"
|
||||
#include"theory_pb_params.h"
|
||||
#include"theory_datatype_params.h"
|
||||
#include"preprocessor_params.h"
|
||||
|
|
@ -75,6 +76,7 @@ struct smt_params : public preprocessor_params,
|
|||
public theory_arith_params,
|
||||
public theory_array_params,
|
||||
public theory_bv_params,
|
||||
public theory_str_params,
|
||||
public theory_pb_params,
|
||||
public theory_datatype_params {
|
||||
bool m_display_proof;
|
||||
|
|
|
|||
|
|
@ -61,5 +61,6 @@ def_module_params(module_name='smt',
|
|||
('dack.gc', UINT, 2000, 'Dynamic ackermannization garbage collection frequency (per conflict)'),
|
||||
('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'),
|
||||
('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'),
|
||||
('core.validate', BOOL, False, 'validate unsat core produced by SMT context')
|
||||
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
|
||||
('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms')
|
||||
))
|
||||
|
|
|
|||
24
src/smt/params/theory_str_params.cpp
Normal file
24
src/smt/params/theory_str_params.cpp
Normal file
|
|
@ -0,0 +1,24 @@
|
|||
/*++
|
||||
Module Name:
|
||||
|
||||
theory_str_params.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Parameters for string theory plugin
|
||||
|
||||
Author:
|
||||
|
||||
Murphy Berzish (mtrberzi) 2016-12-13
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#include"theory_str_params.h"
|
||||
#include"smt_params_helper.hpp"
|
||||
|
||||
void theory_str_params::updt_params(params_ref const & _p) {
|
||||
smt_params_helper p(_p);
|
||||
m_AssertStrongerArrangements = p.str_strong_arrangements();
|
||||
}
|
||||
42
src/smt/params/theory_str_params.h
Normal file
42
src/smt/params/theory_str_params.h
Normal file
|
|
@ -0,0 +1,42 @@
|
|||
/*++
|
||||
Module Name:
|
||||
|
||||
theory_str_params.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Parameters for string theory plugin
|
||||
|
||||
Author:
|
||||
|
||||
Murphy Berzish (mtrberzi) 2016-12-13
|
||||
|
||||
Revision History:
|
||||
|
||||
--*/
|
||||
|
||||
#ifndef THEORY_STR_PARAMS_H
|
||||
#define THEORY_STR_PARAMS_H
|
||||
|
||||
#include"params.h"
|
||||
|
||||
struct theory_str_params {
|
||||
/*
|
||||
* If AssertStrongerArrangements is set to true,
|
||||
* the implications that would normally be asserted during arrangement generation
|
||||
* will instead be asserted as equivalences.
|
||||
* This is a stronger version of the standard axiom.
|
||||
* The Z3str2 axioms can be simulated by setting this to false.
|
||||
*/
|
||||
bool m_AssertStrongerArrangements;
|
||||
|
||||
theory_str_params(params_ref const & p = params_ref()):
|
||||
m_AssertStrongerArrangements(true)
|
||||
{
|
||||
updt_params(p);
|
||||
}
|
||||
|
||||
void updt_params(params_ref const & p);
|
||||
};
|
||||
|
||||
#endif /* THEORY_STR_PARAMS_H */
|
||||
|
|
@ -707,7 +707,7 @@ namespace smt {
|
|||
|
||||
void setup::setup_QF_S() {
|
||||
m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
|
||||
m_context.register_plugin(alloc(smt::theory_str, m_manager));
|
||||
m_context.register_plugin(alloc(smt::theory_str, m_manager, m_params));
|
||||
}
|
||||
|
||||
bool is_arith(static_features const & st) {
|
||||
|
|
@ -839,7 +839,7 @@ namespace smt {
|
|||
|
||||
void setup::setup_str() {
|
||||
setup_arith();
|
||||
m_context.register_plugin(alloc(theory_str, m_manager));
|
||||
m_context.register_plugin(alloc(theory_str, m_manager, m_params));
|
||||
}
|
||||
|
||||
void setup::setup_unknown() {
|
||||
|
|
|
|||
|
|
@ -29,8 +29,9 @@ Revision History:
|
|||
|
||||
namespace smt {
|
||||
|
||||
theory_str::theory_str(ast_manager & m):
|
||||
theory_str::theory_str(ast_manager & m, theory_str_params const & params):
|
||||
theory(m.mk_family_id("str")),
|
||||
m_params(params),
|
||||
/* Options */
|
||||
opt_AggressiveLengthTesting(false),
|
||||
opt_AggressiveValueTesting(false),
|
||||
|
|
@ -44,7 +45,6 @@ theory_str::theory_str(ast_manager & m):
|
|||
opt_CheckVariableScope(true),
|
||||
opt_UseFastLengthTesterCache(true),
|
||||
opt_UseFastValueTesterCache(true),
|
||||
opt_AssertStrongerArrangements(false),
|
||||
/* Internal setup */
|
||||
search_started(false),
|
||||
m_autil(m),
|
||||
|
|
@ -2911,7 +2911,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
|
|||
add_cut_info_merge(t1, sLevel, m);
|
||||
add_cut_info_merge(t1, sLevel, y);
|
||||
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -2963,7 +2963,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
|
|||
add_cut_info_merge(t2, sLevel, x);
|
||||
add_cut_info_merge(t2, sLevel, n);
|
||||
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3071,7 +3071,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
|
|||
if (!arrangement_disjunction.empty()) {
|
||||
expr_ref premise(ctx.mk_eq_atom(concatAst1, concatAst2), mgr);
|
||||
expr_ref conclusion(mk_or(arrangement_disjunction), mgr);
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom(premise, conclusion), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3272,7 +3272,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
|
|||
add_cut_info_merge(temp1, sLevel, y);
|
||||
add_cut_info_merge(temp1, sLevel, m);
|
||||
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3340,7 +3340,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
|
|||
expr_ref ax_l(mk_and(l_items), mgr);
|
||||
expr_ref ax_r(mk_and(r_items), mgr);
|
||||
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3404,7 +3404,7 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) {
|
|||
if (!arrangement_disjunction.empty()) {
|
||||
expr_ref implyR(mk_or(arrangement_disjunction), mgr);
|
||||
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref implyLHS(ctx.mk_eq_atom(concatAst1, concatAst2), mgr);
|
||||
expr_ref ax_strong(ctx.mk_eq_atom(implyLHS, implyR), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
|
|
@ -3592,7 +3592,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
|
|||
r_items.push_back(ctx.mk_eq_atom(x, prefixAst));
|
||||
r_items.push_back(ctx.mk_eq_atom(y, suf_n_concat));
|
||||
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, mk_and(r_items)), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3612,7 +3612,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
|
|||
expr_ref ax_l(mgr.mk_and(ax_l1, ax_l2), mgr);
|
||||
expr_ref ax_r(mgr.mk_and(ctx.mk_eq_atom(x, strAst), ctx.mk_eq_atom(y, n)), mgr);
|
||||
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3650,7 +3650,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
|
|||
add_cut_info_merge(temp1, sLevel, x);
|
||||
add_cut_info_merge(temp1, sLevel, n);
|
||||
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom(ax_l, ax_r), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3731,7 +3731,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) {
|
|||
if (!arrangement_disjunction.empty()) {
|
||||
expr_ref implyR(mk_or(arrangement_disjunction), mgr);
|
||||
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_lhs(ctx.mk_eq_atom(concatAst1, concatAst2), mgr);
|
||||
expr_ref ax_strong(ctx.mk_eq_atom(ax_lhs, implyR), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
|
|
@ -3813,7 +3813,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) {
|
|||
if (!in_same_eqc(tmpAst, n)) {
|
||||
// break down option 4-1
|
||||
expr_ref implyR(ctx.mk_eq_atom(n, tmpAst), mgr);
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3825,7 +3825,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) {
|
|||
//break down option 4-2
|
||||
expr_ref implyR(ctx.mk_eq_atom(n, y), mgr);
|
||||
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3838,7 +3838,7 @@ void theory_str::process_concat_eq_type4(expr * concatAst1, expr * concatAst2) {
|
|||
if (!in_same_eqc(y, tmpAst)) {
|
||||
//break down option 4-3
|
||||
expr_ref implyR(ctx.mk_eq_atom(y, tmpAst), mgr);
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3915,7 +3915,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) {
|
|||
expr_ref x_deltaStr(mk_concat(x, m_strutil.mk_string(deltaStr)), mgr);
|
||||
if (!in_same_eqc(m, x_deltaStr)) {
|
||||
expr_ref implyR(ctx.mk_eq_atom(m, x_deltaStr), mgr);
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3926,7 +3926,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) {
|
|||
// test
|
||||
if (!in_same_eqc(x, m)) {
|
||||
expr_ref implyR(ctx.mk_eq_atom(x, m), mgr);
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -3938,7 +3938,7 @@ void theory_str::process_concat_eq_type5(expr * concatAst1, expr * concatAst2) {
|
|||
expr_ref m_deltaStr(mk_concat(m, m_strutil.mk_string(deltaStr)), mgr);
|
||||
if (!in_same_eqc(x, m_deltaStr)) {
|
||||
expr_ref implyR(ctx.mk_eq_atom(x, m_deltaStr), mgr);
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -4156,7 +4156,7 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) {
|
|||
|
||||
expr_ref implyR(mk_or(arrangement_disjunction), mgr);
|
||||
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom( ctx.mk_eq_atom(concatAst1, concatAst2), implyR ), mgr);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
@ -6266,7 +6266,7 @@ void theory_str::solve_concat_eq_str(expr * concat, expr * str) {
|
|||
assert_axiom(negate_ast);
|
||||
} else {
|
||||
implyR1 = mk_or(arrangement_disjunction);
|
||||
if (opt_AssertStrongerArrangements) {
|
||||
if (m_params.m_AssertStrongerArrangements) {
|
||||
expr_ref ax_strong(ctx.mk_eq_atom(implyL, implyR1), m);
|
||||
assert_axiom(ax_strong);
|
||||
} else {
|
||||
|
|
|
|||
|
|
@ -18,6 +18,7 @@ Revision History:
|
|||
#define _THEORY_STR_H_
|
||||
|
||||
#include"smt_theory.h"
|
||||
#include"theory_str_params.h"
|
||||
#include"trail.h"
|
||||
#include"th_rewriter.h"
|
||||
#include"value_factory.h"
|
||||
|
|
@ -97,7 +98,7 @@ namespace smt {
|
|||
typedef map<std::string, expr*, str_hash_proc, default_eq<std::string> > string_map;
|
||||
|
||||
protected:
|
||||
// Some options that control how the solver operates.
|
||||
theory_str_params const & m_params;
|
||||
|
||||
/*
|
||||
* If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities
|
||||
|
|
@ -189,15 +190,6 @@ namespace smt {
|
|||
*/
|
||||
bool opt_UseFastValueTesterCache;
|
||||
|
||||
/*
|
||||
* If AssertStrongerArrangements is set to true,
|
||||
* the implications that would normally be asserted during arrangement generation
|
||||
* will instead be asserted as equivalences.
|
||||
* This is a stronger version of the regular axiom.
|
||||
* The default (Z3str2) behaviour is to set this to false.
|
||||
*/
|
||||
bool opt_AssertStrongerArrangements;
|
||||
|
||||
bool search_started;
|
||||
arith_util m_autil;
|
||||
str_util m_strutil;
|
||||
|
|
@ -548,7 +540,7 @@ namespace smt {
|
|||
void refresh_theory_var(expr * e);
|
||||
|
||||
public:
|
||||
theory_str(ast_manager & m);
|
||||
theory_str(ast_manager & m, theory_str_params const & params);
|
||||
virtual ~theory_str();
|
||||
|
||||
virtual char const * get_name() const { return "strings"; }
|
||||
|
|
@ -569,7 +561,7 @@ namespace smt {
|
|||
virtual void new_eq_eh(theory_var, theory_var);
|
||||
virtual void new_diseq_eh(theory_var, theory_var);
|
||||
|
||||
virtual theory* mk_fresh(context*) { return alloc(theory_str, get_manager()); }
|
||||
virtual theory* mk_fresh(context*) { return alloc(theory_str, get_manager(), m_params); }
|
||||
virtual void init_search_eh();
|
||||
virtual void relevant_eh(app * n);
|
||||
virtual void assign_eh(bool_var v, bool is_true);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue