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

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Leonardo de Moura 2012-11-22 16:20:19 -08:00
parent 026c81ba29 dcbf1f9fbb
commit 33c44d014b
6 changed files with 16 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -827,7 +827,6 @@ class ExprRef(AstRef):
else:
return []
def _to_expr_ref(a, ctx):
if isinstance(a, Pattern):
return PatternRef(a, ctx)

2
src/muz_qe/dl_context.cpp
View file

@ -954,7 +954,6 @@ namespace datalog {
p.insert(":default-relation", CPK_SYMBOL, "default relation implementation: 'external_relation', 'pentagon'");
p.insert(":generate-explanations", CPK_BOOL, "if true, signature of relations will be extended to contain explanations for facts");
p.insert(":explanations-on-relation-level", CPK_BOOL, "if true, explanations are generated as history of each relation, "
"rather than per fact (:generate-explanations must be set to true for this option to have any effect)");
@ -983,6 +982,7 @@ namespace datalog {
p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
PRIVATE_PARAMS(
p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL,
"if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "

1
src/muz_qe/dl_context.h
View file

@ -77,7 +77,6 @@ namespace datalog {
typedef obj_map<const sort, sort_domain*> sort_domain_map;
typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
ast_manager & m;
front_end_params& m_fparams;
params_ref m_params;

18
src/muz_qe/pdr_context.cpp
View file

@ -1140,6 +1140,19 @@ namespace pdr {
e->get_data().m_value->add_rule(pred_rules[i]);
}
}
datalog::rule_set::iterator rit = rules.begin(), rend = rules.end();
for (; rit != rend; ++rit) {
datalog::rule* r = *rit;
pred_transformer* pt;
unsigned utz = r->get_uninterpreted_tail_size();
for (unsigned i = 0; i < utz; ++i) {
func_decl* pred = r->get_decl(i);
if (!rels.find(pred, pt)) {
pt = alloc(pred_transformer, *this, get_pdr_manager(), pred);
rels.insert(pred, pt);
}
}
}
// Initialize use list dependencies
decl2rel::iterator it = rels.begin(), end = rels.end();
for (; it != end; ++it) {
@ -1149,10 +1162,7 @@ namespace pdr {
obj_hashtable<func_decl>::iterator itf = deps.begin(), endf = deps.end();
for (; itf != endf; ++itf) {
TRACE("pdr", tout << mk_pp(pred, m) << " " << mk_pp(*itf, m) << "\n";);
if (!rels.find(*itf, pt_user)) {
pt_user = alloc(pred_transformer, *this, get_pdr_manager(), *itf);
rels.insert(*itf, pt_user);
}
VERIFY (rels.find(*itf, pt_user));
pt_user->add_use(pt);
}
}

2
src/muz_qe/pdr_dl_interface.cpp
View file

@ -246,7 +246,7 @@ proof_ref dl_interface::get_proof() {
}
void dl_interface::collect_params(param_descrs& p) {
p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)");
p.insert(":generate-proof-trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object");
p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract "

2
src/muz_qe/qe_lite.cpp
View file

@ -342,8 +342,6 @@ class der2 {
void flatten_args(quantifier* q, unsigned& num_args, expr*const*& args) {
expr * e = q->get_expr();
num_args = 1;
args = &e;
if ((q->is_forall() && m.is_or(e)) ||
(q->is_exists() && m.is_and(e))) {
num_args = to_app(e)->get_num_args();