Script 'mail_helper' called by obssrc
Hello community,
here is the log from the commit of package z3 for openSUSE:Factory checked in
at 2023-01-23 18:31:50
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Factory/z3 (Old)
and /work/SRC/openSUSE:Factory/.z3.new.32243 (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3"
Mon Jan 23 18:31:50 2023 rev:37 rq:1060326 version:4.12.1
Changes:
--------
--- /work/SRC/openSUSE:Factory/z3/z3.changes 2023-01-18 13:13:26.633517903
+0100
+++ /work/SRC/openSUSE:Factory/.z3.new.32243/z3.changes 2023-01-23
18:32:10.500147969 +0100
@@ -1,0 +2,7 @@
+Sat Jan 21 17:32:31 UTC 2023 - Dirk Müller <dmuel...@suse.com>
+
+- update to 4.12.1:
+ * change macos build to use explicit reference to Macos version 11. Hosted
+ builds are migrating to macos-12 and it broke a user Issue #6539.
+
+-------------------------------------------------------------------
Old:
----
z3-4.12.0.tar.gz
New:
----
z3-4.12.1.tar.gz
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Other differences:
------------------
++++++ z3.spec ++++++
--- /var/tmp/diff_new_pack.CTjD4C/_old 2023-01-23 18:32:11.040151706 +0100
+++ /var/tmp/diff_new_pack.CTjD4C/_new 2023-01-23 18:32:11.044151734 +0100
@@ -18,7 +18,7 @@
%define sover 4_12
Name: z3
-Version: 4.12.0
+Version: 4.12.1
Release: 0
Summary: Theorem prover from Microsoft Research
License: MIT
++++++ z3-4.12.0.tar.gz -> z3-4.12.1.tar.gz ++++++
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/CMakeLists.txt
new/z3-z3-4.12.1/CMakeLists.txt
--- old/z3-z3-4.12.0/CMakeLists.txt 2023-01-14 15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/CMakeLists.txt 2023-01-18 04:10:26.000000000 +0100
@@ -2,7 +2,7 @@
cmake_minimum_required(VERSION 3.4)
set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX
"${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
-project(Z3 VERSION 4.12.0.0 LANGUAGES CXX)
+project(Z3 VERSION 4.12.1.0 LANGUAGES CXX)
################################################################################
# Project version
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/RELEASE_NOTES.md
new/z3-z3-4.12.1/RELEASE_NOTES.md
--- old/z3-z3-4.12.0/RELEASE_NOTES.md 2023-01-14 15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/RELEASE_NOTES.md 2023-01-18 04:10:26.000000000 +0100
@@ -11,6 +11,10 @@
- introduction of simple induction lemmas to handle a limited repertoire of
induction proofs.
+Version 4.12.1
+==============
+- change macos build to use explicit reference to Macos version 11. Hosted
builds are migrating to macos-12 and it broke a user Issue #6539.
+
Version 4.12.0
==============
- add clause logging API.
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/scripts/mk_project.py
new/z3-z3-4.12.1/scripts/mk_project.py
--- old/z3-z3-4.12.0/scripts/mk_project.py 2023-01-14 15:24:26.000000000
+0100
+++ new/z3-z3-4.12.1/scripts/mk_project.py 2023-01-18 04:10:26.000000000
+0100
@@ -8,7 +8,7 @@
from mk_util import *
def init_version():
- set_version(4, 12, 0, 0) # express a default build version or pick up ci
build version
+ set_version(4, 12, 1, 0) # express a default build version or pick up ci
build version
# Z3 Project definition
def init_project_def():
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/scripts/nightly.yaml
new/z3-z3-4.12.1/scripts/nightly.yaml
--- old/z3-z3-4.12.0/scripts/nightly.yaml 2023-01-14 15:24:26.000000000
+0100
+++ new/z3-z3-4.12.1/scripts/nightly.yaml 2023-01-18 04:10:26.000000000
+0100
@@ -1,7 +1,7 @@
variables:
Major: '4'
Minor: '12'
- Patch: '0'
+ Patch: '1'
AssemblyVersion: $(Major).$(Minor).$(Patch).$(Build.BuildId)
NightlyVersion: $(AssemblyVersion)-$(Build.DefinitionName)
@@ -11,7 +11,7 @@
- job: Mac
displayName: "Mac Build"
pool:
- vmImage: "macOS-latest"
+ vmImage: "macOS-11"
steps:
- script: python scripts/mk_unix_dist.py
--dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk
- script: git clone https://github.com/z3prover/z3test z3test
@@ -25,7 +25,7 @@
- job: MacArm64
displayName: "Mac ARM64 Build"
pool:
- vmImage: "macOS-latest"
+ vmImage: "macOS-11"
steps:
- script: python scripts/mk_unix_dist.py
--dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64
--os=osx-11.0
- script: git clone https://github.com/z3prover/z3test z3test
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/scripts/release.yml
new/z3-z3-4.12.1/scripts/release.yml
--- old/z3-z3-4.12.0/scripts/release.yml 2023-01-14 15:24:26.000000000
+0100
+++ new/z3-z3-4.12.1/scripts/release.yml 2023-01-18 04:10:26.000000000
+0100
@@ -6,7 +6,7 @@
trigger: none
variables:
- ReleaseVersion: '4.12.0'
+ ReleaseVersion: '4.12.1'
stages:
@@ -17,7 +17,7 @@
- job: MacBuild
displayName: "macOS Build"
pool:
- vmImage: "macOS-latest"
+ vmImage: "macOS-11"
steps:
- task: PythonScript@0
displayName: Build
@@ -46,7 +46,7 @@
- job: MacBuildArm64
displayName: "macOS ARM64 Build"
pool:
- vmImage: "macOS-latest"
+ vmImage: "macOS-11"
steps:
- script: python scripts/mk_unix_dist.py
--dotnet-key=$(Build.SourcesDirectory)/resources/z3.snk --arch=arm64
--os=osx-11.0
- script: git clone https://github.com/z3prover/z3test z3test
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/ast/ast.cpp
new/z3-z3-4.12.1/src/ast/ast.cpp
--- old/z3-z3-4.12.0/src/ast/ast.cpp 2023-01-14 15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/ast/ast.cpp 2023-01-18 04:10:26.000000000 +0100
@@ -1673,6 +1673,7 @@
}
void ast_manager::add_lambda_def(func_decl* f, quantifier* q) {
+ TRACE("model", tout << "add lambda def " << mk_pp(q, *this) << "\n");
m_lambda_defs.insert(f, q);
f->get_info()->set_lambda(true);
inc_ref(q);
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/ast/ast.h
new/z3-z3-4.12.1/src/ast/ast.h
--- old/z3-z3-4.12.0/src/ast/ast.h 2023-01-14 15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/ast/ast.h 2023-01-18 04:10:26.000000000 +0100
@@ -1631,6 +1631,7 @@
void add_lambda_def(func_decl* f, quantifier* q);
quantifier* is_lambda_def(func_decl* f);
quantifier* is_lambda_def(app* e) { return is_lambda_def(e->get_decl()); }
+ obj_map<func_decl, quantifier*> const& lambda_defs() const { return
m_lambda_defs; }
symbol const& lambda_def_qid() const { return m_lambda_def; }
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/ast/euf/euf_egraph.cpp
new/z3-z3-4.12.1/src/ast/euf/euf_egraph.cpp
--- old/z3-z3-4.12.0/src/ast/euf/euf_egraph.cpp 2023-01-14 15:24:26.000000000
+0100
+++ new/z3-z3-4.12.1/src/ast/euf/euf_egraph.cpp 2023-01-18 04:10:26.000000000
+0100
@@ -91,9 +91,7 @@
m_scopes.push_back(m_updates.size());
m_region.push_scope();
m_updates.push_back(update_record(m_new_th_eqs_qhead,
update_record::new_th_eq_qhead()));
- m_updates.push_back(update_record(m_new_lits_qhead,
update_record::new_lits_qhead()));
}
- SASSERT(m_new_lits_qhead <= m_new_lits.size());
SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size());
}
@@ -156,12 +154,29 @@
}
void egraph::add_literal(enode* n, enode* ante) {
+ /*
if (n->bool_var() == sat::null_bool_var)
return;
- TRACE("euf_verbose", tout << "lit: " << n->get_expr_id() << "\n";);
- m_new_lits.push_back(enode_pair(n, ante));
- m_updates.push_back(update_record(update_record::new_lit()));
+ */
if (!ante) ++m_stats.m_num_eqs; else ++m_stats.m_num_lits;
+ if (!ante)
+ m_on_propagate_literal(n, ante);
+ else if (m.is_true(ante->get_expr()) || m.is_false(ante->get_expr())) {
+ for (enode* k : enode_class(n)) {
+ if (k != ante) {
+ //verbose_stream() << "eq: " << k->value() << " "
<<ante->value() << "\n";
+ m_on_propagate_literal(k, ante);
+ }
+ }
+ }
+ else {
+ for (enode* k : enode_class(n)) {
+ if (k->value() != ante->value()) {
+ //verbose_stream() << "eq: " << k->value() << " "
<<ante->value() << "\n";
+ m_on_propagate_literal(k, ante);
+ }
+ }
+ }
}
void egraph::new_diseq(enode* n) {
@@ -339,7 +354,6 @@
num_scopes -= m_num_scopes;
m_num_scopes = 0;
- SASSERT(m_new_lits_qhead <= m_new_lits.size());
unsigned old_lim = m_scopes.size() - num_scopes;
unsigned num_updates = m_scopes[old_lim];
auto undo_node = [&]() {
@@ -378,18 +392,12 @@
SASSERT(p.r1->get_th_var(p.m_th_id) != null_theory_var);
p.r1->replace_th_var(p.m_old_th_var, p.m_th_id);
break;
- case update_record::tag_t::is_new_lit:
- m_new_lits.pop_back();
- break;
case update_record::tag_t::is_new_th_eq:
m_new_th_eqs.pop_back();
break;
case update_record::tag_t::is_new_th_eq_qhead:
m_new_th_eqs_qhead = p.qhead;
break;
- case update_record::tag_t::is_new_lits_qhead:
- m_new_lits_qhead = p.qhead;
- break;
case update_record::tag_t::is_inconsistent:
m_inconsistent = p.m_inconsistent;
break;
@@ -424,7 +432,6 @@
m_region.pop_scope(num_scopes);
m_to_merge.reset();
- SASSERT(m_new_lits_qhead <= m_new_lits.size());
SASSERT(m_new_th_eqs_qhead <= m_new_th_eqs.size());
// DEBUG_CODE(invariant(););
@@ -461,12 +468,6 @@
std::swap(n1, n2);
}
- if (j.is_congruence() && (m.is_false(r2->get_expr()) ||
m.is_true(r2->get_expr())))
- add_literal(n1, r2);
- if (r2->value() != l_undef && n1->value() == l_undef)
- add_literal(n1, r2);
- else if (r1->value() != l_undef && n2->value() == l_undef)
- add_literal(n2, r1);
remove_parents(r1);
push_eq(r1, n1, r2->num_parents());
merge_justification(n1, n2, j);
@@ -476,6 +477,13 @@
r2->inc_class_size(r1->class_size());
merge_th_eq(r1, r2);
reinsert_parents(r1, r2);
+ if (j.is_congruence() && (m.is_false(r2->get_expr()) ||
m.is_true(r2->get_expr())))
+ add_literal(n1, r2);
+ else if (n2->value() != l_undef && n1->value() != n2->value())
+ add_literal(n1, n2);
+ else if (n1->value() != l_undef && n2->value() != n1->value())
+ add_literal(n2, n1);
+
for (auto& cb : m_on_merge)
cb(r2, r1);
}
@@ -565,7 +573,6 @@
bool egraph::propagate() {
- SASSERT(m_new_lits_qhead <= m_new_lits.size());
SASSERT(m_num_scopes == 0 || m_to_merge.empty());
force_push();
for (unsigned i = 0; i < m_to_merge.size() && m.limit().inc() &&
!inconsistent(); ++i) {
@@ -574,7 +581,6 @@
}
m_to_merge.reset();
return
- (m_new_lits_qhead < m_new_lits.size()) ||
(m_new_th_eqs_qhead < m_new_th_eqs.size()) ||
inconsistent();
}
@@ -851,7 +857,6 @@
std::ostream& egraph::display(std::ostream& out) const {
out << "updates " << m_updates.size() << "\n";
- out << "newlits " << m_new_lits.size() << " qhead: " <<
m_new_lits_qhead << "\n";
out << "neweqs " << m_new_th_eqs.size() << " qhead: " <<
m_new_th_eqs_qhead << "\n";
m_table.display(out);
unsigned max_args = 0;
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/ast/euf/euf_egraph.h
new/z3-z3-4.12.1/src/ast/euf/euf_egraph.h
--- old/z3-z3-4.12.0/src/ast/euf/euf_egraph.h 2023-01-14 15:24:26.000000000
+0100
+++ new/z3-z3-4.12.1/src/ast/euf/euf_egraph.h 2023-01-18 04:10:26.000000000
+0100
@@ -105,10 +105,8 @@
struct toggle_merge_tf {};
struct add_th_var {};
struct replace_th_var {};
- struct new_lit {};
struct new_th_eq {};
struct new_th_eq_qhead {};
- struct new_lits_qhead {};
struct inconsistent {};
struct value_assignment {};
struct lbl_hash {};
@@ -116,8 +114,8 @@
struct update_children {};
struct set_relevant {};
enum class tag_t { is_set_parent, is_add_node, is_toggle_cgc,
is_toggle_merge_tf, is_update_children,
- is_add_th_var, is_replace_th_var, is_new_lit, is_new_th_eq,
- is_lbl_hash, is_new_th_eq_qhead, is_new_lits_qhead,
+ is_add_th_var, is_replace_th_var, is_new_th_eq,
+ is_lbl_hash, is_new_th_eq_qhead,
is_inconsistent, is_value_assignment, is_lbl_set,
is_set_relevant };
tag_t tag;
enode* r1;
@@ -145,14 +143,10 @@
tag(tag_t::is_add_th_var), r1(n), n1(nullptr),
r2_num_parents(id) {}
update_record(enode* n, theory_id id, theory_var v,
replace_th_var) :
tag(tag_t::is_replace_th_var), r1(n), n1(nullptr),
m_th_id(id), m_old_th_var(v) {}
- update_record(new_lit) :
- tag(tag_t::is_new_lit), r1(nullptr), n1(nullptr),
r2_num_parents(0) {}
update_record(new_th_eq) :
tag(tag_t::is_new_th_eq), r1(nullptr), n1(nullptr),
r2_num_parents(0) {}
update_record(unsigned qh, new_th_eq_qhead):
tag(tag_t::is_new_th_eq_qhead), r1(nullptr), n1(nullptr),
qhead(qh) {}
- update_record(unsigned qh, new_lits_qhead):
- tag(tag_t::is_new_lits_qhead), r1(nullptr), n1(nullptr),
qhead(qh) {}
update_record(bool inc, inconsistent) :
tag(tag_t::is_inconsistent), r1(nullptr), n1(nullptr),
m_inconsistent(inc) {}
update_record(enode* n, value_assignment) :
@@ -187,9 +181,7 @@
enode *m_n1 = nullptr;
enode *m_n2 = nullptr;
justification m_justification;
- unsigned m_new_lits_qhead = 0;
unsigned m_new_th_eqs_qhead = 0;
- svector<enode_pair> m_new_lits;
svector<th_eq> m_new_th_eqs;
bool_vector m_th_propagates_diseqs;
enode_vector m_todo;
@@ -198,7 +190,8 @@
bool m_default_relevant = true;
uint64_t m_congruence_timestamp = 0;
- std::vector<std::function<void(enode*,enode*)>> m_on_merge;
+ std::vector<std::function<void(enode*,enode*)>> m_on_merge;
+ std::function<void(enode*, enode*)> m_on_propagate_literal;
std::function<void(enode*)> m_on_make;
std::function<void(expr*,expr*,expr*)> m_used_eq;
std::function<void(app*,app*)> m_used_cc;
@@ -290,11 +283,8 @@
is an equality consequence.
*/
void add_th_diseq(theory_id id, theory_var v1, theory_var v2,
expr* eq);
- bool has_literal() const { return m_new_lits_qhead <
m_new_lits.size(); }
bool has_th_eq() const { return m_new_th_eqs_qhead <
m_new_th_eqs.size(); }
- enode_pair get_literal() const { return m_new_lits[m_new_lits_qhead]; }
th_eq get_th_eq() const { return
m_new_th_eqs[m_new_th_eqs_qhead]; }
- void next_literal() { force_push(); SASSERT(m_new_lits_qhead <
m_new_lits.size()); m_new_lits_qhead++; }
void next_th_eq() { force_push(); SASSERT(m_new_th_eqs_qhead <
m_new_th_eqs.size()); m_new_th_eqs_qhead++; }
void set_lbl_hash(enode* n);
@@ -311,6 +301,7 @@
void set_default_relevant(bool b) { m_default_relevant = b; }
void set_on_merge(std::function<void(enode* root,enode* other)>&
on_merge) { m_on_merge.push_back(on_merge); }
+ void set_on_propagate(std::function<void(enode* lit,enode* ante)>&
on_propagate) { m_on_propagate_literal = on_propagate; }
void set_on_make(std::function<void(enode* n)>& on_make) { m_on_make =
on_make; }
void set_used_eq(std::function<void(expr*,expr*,expr*)>& used_eq) {
m_used_eq = used_eq; }
void set_used_cc(std::function<void(app*,app*)>& used_cc) { m_used_cc
= used_cc; }
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/z3-z3-4.12.0/src/ast/simplifiers/dependent_expr_state.cpp
new/z3-z3-4.12.1/src/ast/simplifiers/dependent_expr_state.cpp
--- old/z3-z3-4.12.0/src/ast/simplifiers/dependent_expr_state.cpp
2023-01-14 15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/ast/simplifiers/dependent_expr_state.cpp
2023-01-18 04:10:26.000000000 +0100
@@ -84,6 +84,23 @@
}
/**
+* Freeze all functions used in lambda defined declarations
+*/
+void dependent_expr_state::freeze_lambda() {
+ auto& m = m_frozen_trail.get_manager();
+ unsigned sz = m.lambda_defs().size();
+ if (m_num_lambdas >= sz)
+ return;
+
+ ast_mark visited;
+ for (auto const& [f, body] : m.lambda_defs())
+ freeze_terms(body, false, visited);
+ m_trail.push(value_trail(m_num_lambdas));
+ m_num_lambdas = sz;
+}
+
+
+/**
* The current qhead is to be updated to qtail.
* Before this update, freeze all functions appearing in formulas.
*/
@@ -100,8 +117,9 @@
if (m_suffix_frozen)
return;
m_suffix_frozen = true;
- auto& m = m_frozen_trail.get_manager();
freeze_recfun();
+ freeze_lambda();
+ auto& m = m_frozen_trail.get_manager();
ast_mark visited;
ptr_vector<expr> es;
for (unsigned i = qhead(); i < qtail(); ++i) {
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/z3-z3-4.12.0/src/ast/simplifiers/dependent_expr_state.h
new/z3-z3-4.12.1/src/ast/simplifiers/dependent_expr_state.h
--- old/z3-z3-4.12.0/src/ast/simplifiers/dependent_expr_state.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/ast/simplifiers/dependent_expr_state.h 2023-01-18
04:10:26.000000000 +0100
@@ -43,14 +43,14 @@
class dependent_expr_state {
unsigned m_qhead = 0;
bool m_suffix_frozen = false;
- unsigned m_num_recfun = 0;
+ unsigned m_num_recfun = 0, m_num_lambdas = 0;
lbool m_has_quantifiers = l_undef;
ast_mark m_frozen;
func_decl_ref_vector m_frozen_trail;
void freeze_prefix();
void freeze_recfun();
+ void freeze_lambda();
void freeze_terms(expr* term, bool only_as_array, ast_mark& visited);
- void freeze(expr* term);
void freeze(func_decl* f);
struct thaw : public trail {
unsigned sz;
@@ -88,6 +88,7 @@
/**
* Freeze internal functions
*/
+ void freeze(expr* term);
bool frozen(func_decl* f) const { return m_frozen.is_marked(f); }
bool frozen(expr* f) const { return is_app(f) &&
m_frozen.is_marked(to_app(f)->get_decl()); }
void freeze_suffix();
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/ast/simplifiers/max_bv_sharing.cpp
new/z3-z3-4.12.1/src/ast/simplifiers/max_bv_sharing.cpp
--- old/z3-z3-4.12.0/src/ast/simplifiers/max_bv_sharing.cpp 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/ast/simplifiers/max_bv_sharing.cpp 2023-01-18
04:10:26.000000000 +0100
@@ -22,6 +22,7 @@
#include "ast/rewriter/maximize_ac_sharing.h"
#include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/rewriter_def.h"
class max_bv_sharing : public dependent_expr_simplifier {
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/z3-z3-4.12.0/src/ast/simplifiers/model_reconstruction_trail.cpp
new/z3-z3-4.12.1/src/ast/simplifiers/model_reconstruction_trail.cpp
--- old/z3-z3-4.12.0/src/ast/simplifiers/model_reconstruction_trail.cpp
2023-01-14 15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/ast/simplifiers/model_reconstruction_trail.cpp
2023-01-18 04:10:26.000000000 +0100
@@ -23,11 +23,13 @@
// substitutions that use variables from the dependent expressions.
// TODO: add filters to skip sections of the trail that do not touch the
current free variables.
-void model_reconstruction_trail::replay(unsigned qhead, dependent_expr_state&
st) {
+void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector&
assumptions, dependent_expr_state& st) {
ast_mark free_vars;
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);
- for (unsigned i = qhead; i < st.qtail(); ++i)
+ for (unsigned i = qhead; i < st.qtail(); ++i)
add_vars(st[i], free_vars);
+ for (expr* a : assumptions)
+ add_vars(a, free_vars);
for (auto& t : m_trail) {
if (!t->m_active)
@@ -63,7 +65,7 @@
mrp.insert(head, t->m_def, t->m_dep);
dependent_expr de(m, t->m_def, nullptr, t->m_dep);
add_vars(de, free_vars);
-
+
for (unsigned i = qhead; i < st.qtail(); ++i) {
auto [f, p, dep1] = st[i]();
expr_ref g(m);
@@ -73,6 +75,15 @@
if (f != g)
st.update(i, dependent_expr(m, g, nullptr, dep2));
}
+ for (unsigned i = 0; i < assumptions.size(); ++i) {
+ expr* a = assumptions.get(i);
+ expr_ref g(m);
+ expr_dependency_ref dep(m);
+ mrp(a, nullptr, g, dep);
+ if (a != g)
+ assumptions[i] = g;
+ // ignore dep.
+ }
continue;
}
@@ -103,7 +114,15 @@
CTRACE("simplifier", f != g, tout << "updated " << mk_pp(g, m) <<
"\n");
add_vars(d, free_vars);
st.update(i, d);
- }
+ }
+
+ for (unsigned i = 0; i < assumptions.size(); ++i) {
+ expr* a = assumptions.get(i);
+ auto [g, dep2] = rp->replace_with_dep(a);
+ if (a != g)
+ assumptions[i] = g;
+ // ignore dep.
+ }
}
}
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/z3-z3-4.12.0/src/ast/simplifiers/model_reconstruction_trail.h
new/z3-z3-4.12.1/src/ast/simplifiers/model_reconstruction_trail.h
--- old/z3-z3-4.12.0/src/ast/simplifiers/model_reconstruction_trail.h
2023-01-14 15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/ast/simplifiers/model_reconstruction_trail.h
2023-01-18 04:10:26.000000000 +0100
@@ -74,13 +74,17 @@
scoped_ptr_vector<entry> m_trail;
unsigned m_trail_index = 0;
- void add_vars(dependent_expr const& d, ast_mark& free_vars) {
- for (expr* t : subterms::all(expr_ref(d.fml(), d.get_manager())))
+ void add_vars(expr* e, ast_mark& free_vars) {
+ for (expr* t : subterms::all(expr_ref(e, m)))
free_vars.mark(t, true);
}
+
+ void add_vars(dependent_expr const& d, ast_mark& free_vars) {
+ add_vars(d.fml(), free_vars);
+ }
bool intersects(ast_mark const& free_vars, dependent_expr const& d) {
- expr_ref term(d.fml(), d.get_manager());
+ expr_ref term(d.fml(), m);
auto iter = subterms::all(term);
return any_of(iter, [&](expr* t) { return free_vars.is_marked(t); });
}
@@ -126,7 +130,7 @@
* register a new depedent expression, update the trail
* by removing substitutions that are not equivalence preserving.
*/
- void replay(unsigned qhead, dependent_expr_state& fmls);
+ void replay(unsigned qhead, expr_ref_vector& assumptions,
dependent_expr_state& fmls);
/**
* retrieve the current model converter corresponding to chaining
substitutions from the trail.
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/ast/simplifiers/solve_eqs.cpp
new/z3-z3-4.12.1/src/ast/simplifiers/solve_eqs.cpp
--- old/z3-z3-4.12.0/src/ast/simplifiers/solve_eqs.cpp 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/ast/simplifiers/solve_eqs.cpp 2023-01-18
04:10:26.000000000 +0100
@@ -116,10 +116,10 @@
for (auto const& eq : m_next[j]) {
auto const& [orig, v, t, d] = eq;
SASSERT(j == var2id(v));
- bool is_safe = true;
if (m_fmls.frozen(v))
continue;
+ bool is_safe = true;
unsigned todo_sz = todo.size();
// determine if substitution is safe.
@@ -223,6 +223,8 @@
void solve_eqs::reduce() {
+ m_fmls.freeze_suffix();
+
for (extract_eq* ex : m_extract_plugins)
ex->pre_process(m_fmls);
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/nlsat/tactic/nlsat_tactic.h
new/z3-z3-4.12.1/src/nlsat/tactic/nlsat_tactic.h
--- old/z3-z3-4.12.0/src/nlsat/tactic/nlsat_tactic.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/nlsat/tactic/nlsat_tactic.h 2023-01-18
04:10:26.000000000 +0100
@@ -13,7 +13,24 @@
Leonardo (leonardo) 2012-01-02
-Notes:
+Tactic Documentation:
+
+## Tactic nlsat
+
+### Short Description
+
+(try to) solve goal using a nonlinear arithmetic solver
+
+### Example
+
+```z3
+(declare-const x Real)
+(declare-const y Real)
+(assert (> (* x x) (* y x)))
+(assert (> x 0))
+(assert (< y 1))
+(apply (then simplify purify-arith nlsat))
+```
--*/
#pragma once
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/nlsat/tactic/qfnra_nlsat_tactic.h
new/z3-z3-4.12.1/src/nlsat/tactic/qfnra_nlsat_tactic.h
--- old/z3-z3-4.12.0/src/nlsat/tactic/qfnra_nlsat_tactic.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/nlsat/tactic/qfnra_nlsat_tactic.h 2023-01-18
04:10:26.000000000 +0100
@@ -13,7 +13,26 @@
Leonardo (leonardo) 2012-01-23
-Notes:
+Tactic Documentation:
+
+## Tactic qfnra-nlsat
+
+### Short Description
+
+Self-contained tactic that attempts to solve goal using a nonlinear arithmetic
solver.
+It first applies tactics, such as `purify-arith` to convert the goal into a
format
+where the `nlsat` tactic applies.
+
+### Example
+
+```z3
+(declare-const x Real)
+(declare-const y Real)
+(assert (> (* x x) (* y x)))
+(assert (> x 0))
+(assert (< y 1))
+(apply qfnra-nlsat)
+```
--*/
#pragma once
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/qe/qe_tactic.h
new/z3-z3-4.12.1/src/qe/qe_tactic.h
--- old/z3-z3-4.12.0/src/qe/qe_tactic.h 2023-01-14 15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/qe/qe_tactic.h 2023-01-18 04:10:26.000000000 +0100
@@ -13,9 +13,33 @@
Leonardo de Moura (leonardo) 2011-12-28.
-Revision History:
+Tactic Documentation
+
+## Tactic qe
+
+### Short Description
+
+Apply quantifier elimination on quantified sub-formulas.
+
+### Long Description
+
+The tactic applies quantifier elimination procedures on quantified
sub-formulas.
+It relies on theory plugins that can perform quanifier elimination for
selected theories.
+These plugins include Booleans, bit-vectors, arithmetic (linear), arrays, and
data-types (term algebra).
+It performs feasibility checks on cases to throttle the set of sub-formulas
where quantifier elimination
+is applied.
+
+### Example
+
+```z3
+(declare-const x Int)
+(declare-const y Int)
+(assert (exists ((z Int)) (and (<= x (* 2 z)) (<= (* 3 z) y))))
+(apply qe)
+```
--*/
+
#pragma once
#include "util/params.h"
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/z3-z3-4.12.0/src/sat/sat_solver/sat_smt_preprocess.cpp
new/z3-z3-4.12.1/src/sat/sat_solver/sat_smt_preprocess.cpp
--- old/z3-z3-4.12.0/src/sat/sat_solver/sat_smt_preprocess.cpp 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/sat/sat_solver/sat_smt_preprocess.cpp 2023-01-18
04:10:26.000000000 +0100
@@ -16,6 +16,7 @@
--*/
+#include "ast/rewriter/rewriter_def.h"
#include "ast/simplifiers/bit_blaster.h"
#include "ast/simplifiers/max_bv_sharing.h"
#include "ast/simplifiers/card2bv.h"
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/sat/sat_solver/sat_smt_solver.cpp
new/z3-z3-4.12.1/src/sat/sat_solver/sat_smt_solver.cpp
--- old/z3-z3-4.12.0/src/sat/sat_solver/sat_smt_solver.cpp 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/sat/sat_solver/sat_smt_solver.cpp 2023-01-18
04:10:26.000000000 +0100
@@ -70,7 +70,7 @@
return out;
}
void append(generic_model_converter& mc) { model_trail().append(mc); }
- void replay(unsigned qhead) { m_reconstruction_trail.replay(qhead,
*this); }
+ void replay(unsigned qhead, expr_ref_vector& assumptions) {
m_reconstruction_trail.replay(qhead, assumptions, *this); }
void flatten_suffix() override {
expr_mark seen;
unsigned j = qhead();
@@ -237,8 +237,10 @@
expr_ref_vector assumptions(m);
for (unsigned i = 0; i < sz; ++i)
assumptions.push_back(ensure_literal(_assumptions[i]));
+ for (expr* a : assumptions)
+ m_preprocess_state.freeze(a);
TRACE("sat", tout << assumptions << "\n";);
- lbool r = internalize_formulas();
+ lbool r = internalize_formulas(assumptions);
if (r != l_true)
return r;
@@ -271,7 +273,8 @@
void push() override {
try {
- internalize_formulas();
+ expr_ref_vector none(m);
+ internalize_formulas(none);
}
catch (...) {
push_internal();
@@ -430,7 +433,7 @@
}
expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level)
override {
- lbool r = internalize_formulas();
+ lbool r = internalize_formulas(vs);
if (r != l_true) {
IF_VERBOSE(0, verbose_stream() << "internalize produced " << r <<
"\n");
return expr_ref_vector(m);
@@ -561,7 +564,8 @@
void convert_internalized() {
m_solver.pop_to_base_level();
- internalize_formulas();
+ expr_ref_vector none(m);
+ internalize_formulas(none);
if (!is_internalized() || m_internalized_converted)
return;
sat2goal s2g;
@@ -641,9 +645,9 @@
add_assumption(a);
}
- lbool internalize_formulas() {
+ lbool internalize_formulas(expr_ref_vector& assumptions) {
- if (is_internalized())
+ if (is_internalized() && assumptions.empty())
return l_true;
unsigned qhead = m_preprocess_state.qhead();
@@ -651,7 +655,7 @@
m_internalized_converted = false;
- m_preprocess_state.replay(qhead);
+ m_preprocess_state.replay(qhead, assumptions);
m_preprocess.reduce();
if (!m.inc())
return l_undef;
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/sat/smt/arith_diagnostics.cpp
new/z3-z3-4.12.1/src/sat/smt/arith_diagnostics.cpp
--- old/z3-z3-4.12.0/src/sat/smt/arith_diagnostics.cpp 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/sat/smt/arith_diagnostics.cpp 2023-01-18
04:10:26.000000000 +0100
@@ -124,6 +124,19 @@
return m_arith_hint.mk(ctx);
}
+ arith_proof_hint const* solver::explain_conflict(sat::literal_vector
const& core, euf::enode_pair_vector const& eqs) {
+ arith_proof_hint* hint = nullptr;
+ if (ctx.use_drat()) {
+ m_arith_hint.set_type(ctx, hint_type::farkas_h);
+ for (auto lit : core)
+ m_arith_hint.add_lit(rational::one(), lit);
+ for (auto const& [a,b] : eqs)
+ m_arith_hint.add_eq(a, b);
+ hint = m_arith_hint.mk(ctx);
+ }
+ return hint;
+ }
+
arith_proof_hint const* solver::explain_implied_eq(lp::explanation const&
e, euf::enode* a, euf::enode* b) {
if (!ctx.use_drat())
return nullptr;
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/sat/smt/arith_solver.cpp
new/z3-z3-4.12.1/src/sat/smt/arith_solver.cpp
--- old/z3-z3-4.12.0/src/sat/smt/arith_solver.cpp 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/sat/smt/arith_solver.cpp 2023-01-18
04:10:26.000000000 +0100
@@ -1196,26 +1196,31 @@
void solver::set_conflict_or_lemma(literal_vector const& core, bool
is_conflict) {
reset_evidence();
m_core.append(core);
-
- ++m_num_conflicts;
- ++m_stats.m_conflicts;
for (auto ev : m_explanation)
set_evidence(ev.ci());
+
TRACE("arith",
tout << "Lemma - " << (is_conflict ? "conflict" : "propagation")
<< "\n";
for (literal c : m_core) tout << literal2expr(c) << "\n";
for (auto p : m_eqs) tout << ctx.bpp(p.first) << " == " <<
ctx.bpp(p.second) << "\n";);
- DEBUG_CODE(
- if (is_conflict) {
- for (literal c : m_core) VERIFY(s().value(c) == l_true);
- for (auto p : m_eqs) VERIFY(p.first->get_root() ==
p.second->get_root());
- });
- for (auto const& eq : m_eqs)
- m_core.push_back(ctx.mk_literal(m.mk_eq(eq.first->get_expr(),
eq.second->get_expr())));
- for (literal& c : m_core)
- c.neg();
- add_redundant(m_core, explain(hint_type::farkas_h));
+ if (is_conflict) {
+ DEBUG_CODE(
+ for (literal c : m_core) VERIFY(s().value(c) == l_true);
+ for (auto p : m_eqs) VERIFY(p.first->get_root() ==
p.second->get_root()));
+ ++m_num_conflicts;
+ ++m_stats.m_conflicts;
+ auto* hint = explain_conflict(m_core, m_eqs);
+ ctx.set_conflict(euf::th_explain::conflict(*this, m_core, m_eqs,
hint));
+ }
+ else {
+ for (auto const& eq : m_eqs)
+ m_core.push_back(ctx.mk_literal(m.mk_eq(eq.first->get_expr(),
eq.second->get_expr())));
+ for (literal& c : m_core)
+ c.neg();
+
+ add_redundant(m_core, explain(hint_type::farkas_h));
+ }
}
bool solver::is_infeasible() const {
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/sat/smt/arith_solver.h
new/z3-z3-4.12.1/src/sat/smt/arith_solver.h
--- old/z3-z3-4.12.0/src/sat/smt/arith_solver.h 2023-01-14 15:24:26.000000000
+0100
+++ new/z3-z3-4.12.1/src/sat/smt/arith_solver.h 2023-01-18 04:10:26.000000000
+0100
@@ -478,6 +478,7 @@
arith_proof_hint const* explain(hint_type ty, sat::literal lit =
sat::null_literal);
arith_proof_hint const* explain_implied_eq(lp::explanation const& e,
euf::enode* a, euf::enode* b);
arith_proof_hint const* explain_trichotomy(sat::literal le,
sat::literal ge, sat::literal eq);
+ arith_proof_hint const* explain_conflict(sat::literal_vector const&
core, euf::enode_pair_vector const& eqs);
void explain_assumptions(lp::explanation const& e);
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/sat/smt/euf_solver.cpp
new/z3-z3-4.12.1/src/sat/smt/euf_solver.cpp
--- old/z3-z3-4.12.0/src/sat/smt/euf_solver.cpp 2023-01-14 15:24:26.000000000
+0100
+++ new/z3-z3-4.12.1/src/sat/smt/euf_solver.cpp 2023-01-18 04:10:26.000000000
+0100
@@ -63,6 +63,11 @@
};
m_egraph.set_display_justification(disp);
+ std::function<void(euf::enode* n, euf::enode* ante)> on_literal =
[&](enode* n, enode* ante) {
+ propagate_literal(n, ante);
+ };
+ m_egraph.set_on_propagate(on_literal);
+
if (m_relevancy.enabled()) {
std::function<void(euf::enode* root, euf::enode* other)> on_merge =
[&](enode* root, enode* other) {
@@ -414,7 +419,6 @@
}
bool propagated1 = false;
if (m_egraph.propagate()) {
- propagate_literals();
propagate_th_eqs();
propagated1 = true;
}
@@ -435,52 +439,52 @@
return propagated;
}
- void solver::propagate_literals() {
- for (; m_egraph.has_literal() && !s().inconsistent() &&
!m_egraph.inconsistent(); m_egraph.next_literal()) {
- auto [n, ante] = m_egraph.get_literal();
- expr* e = n->get_expr();
- expr* a = nullptr, *b = nullptr;
- bool_var v = n->bool_var();
- SASSERT(m.is_bool(e));
- size_t cnstr;
- literal lit;
- if (!ante) {
- VERIFY(m.is_eq(e, a, b));
- cnstr = eq_constraint().to_index();
- lit = literal(v, false);
- }
- else {
- //
- // There are the following three cases for propagation of
literals
- //
- // 1. n == ante is true from equallity, ante = true/false
- // 2. n == ante is true from equality, value(ante) != l_undef
- // 3. value(n) != l_undef, ante = true/false, merge_tf is set
on n
- //
- lbool val = ante->value();
- if (val == l_undef) {
- SASSERT(m.is_value(ante->get_expr()));
- val = m.is_true(ante->get_expr()) ? l_true : l_false;
- }
- auto& c = lit_constraint(ante);
- cnstr = c.to_index();
- lit = literal(v, val == l_false);
- }
- unsigned lvl = s().scope_lvl();
-
- CTRACE("euf", s().value(lit) != l_true, tout << lit << " " <<
s().value(lit) << "@" << lvl << " " << mk_bounded_pp(a, m) << " = " <<
mk_bounded_pp(b, m) << "\n";);
- if (s().value(lit) == l_false && m_ackerman && a && b)
- m_ackerman->cg_conflict_eh(a, b);
- switch (s().value(lit)) {
- case l_true:
- if (n->merge_tf() && !m.is_value(n->get_root()->get_expr()))
- m_egraph.merge(n, ante, to_ptr(lit));
- break;
- case l_undef:
- case l_false:
- s().assign(lit, sat::justification::mk_ext_justification(lvl,
cnstr));
- break;
+
+ void solver::propagate_literal(enode* n, enode* ante) {
+ expr* e = n->get_expr();
+ expr* a = nullptr, *b = nullptr;
+ bool_var v = n->bool_var();
+ if (v == sat::null_bool_var)
+ return;
+ SASSERT(m.is_bool(e));
+ size_t cnstr;
+ literal lit;
+ if (!ante) {
+ VERIFY(m.is_eq(e, a, b));
+ cnstr = eq_constraint().to_index();
+ lit = literal(v, false);
+ }
+ else {
+ //
+ // There are the following three cases for propagation of literals
+ //
+ // 1. n == ante is true from equallity, ante = true/false
+ // 2. n == ante is true from equality, value(ante) != l_undef
+ // 3. value(n) != l_undef, ante = true/false, merge_tf is set on n
+ //
+ lbool val = ante->value();
+ if (val == l_undef) {
+ SASSERT(m.is_value(ante->get_expr()));
+ val = m.is_true(ante->get_expr()) ? l_true : l_false;
}
+ auto& c = lit_constraint(ante);
+ cnstr = c.to_index();
+ lit = literal(v, val == l_false);
+ }
+ unsigned lvl = s().scope_lvl();
+
+ CTRACE("euf", s().value(lit) != l_true, tout << lit << " " <<
s().value(lit) << "@" << lvl << " " << mk_bounded_pp(a, m) << " = " <<
mk_bounded_pp(b, m) << "\n";);
+ if (s().value(lit) == l_false && m_ackerman && a && b)
+ m_ackerman->cg_conflict_eh(a, b);
+ switch (s().value(lit)) {
+ case l_true:
+ if (n->merge_tf() && !m.is_value(n->get_root()->get_expr()))
+ m_egraph.merge(n, ante, to_ptr(lit));
+ break;
+ case l_undef:
+ case l_false:
+ s().assign(lit, sat::justification::mk_ext_justification(lvl,
cnstr));
+ break;
}
}
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/sat/smt/euf_solver.h
new/z3-z3-4.12.1/src/sat/smt/euf_solver.h
--- old/z3-z3-4.12.0/src/sat/smt/euf_solver.h 2023-01-14 15:24:26.000000000
+0100
+++ new/z3-z3-4.12.1/src/sat/smt/euf_solver.h 2023-01-18 04:10:26.000000000
+0100
@@ -206,7 +206,7 @@
void validate_model(model& mdl);
// solving
- void propagate_literals();
+ void propagate_literal(enode* n, enode* ante);
void propagate_th_eqs();
bool is_self_propagated(th_eq const& e);
void get_antecedents(literal l, constraint& j, literal_vector& r, bool
probing);
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/sat/tactic/sat_tactic.h
new/z3-z3-4.12.1/src/sat/tactic/sat_tactic.h
--- old/z3-z3-4.12.0/src/sat/tactic/sat_tactic.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/sat/tactic/sat_tactic.h 2023-01-18
04:10:26.000000000 +0100
@@ -13,7 +13,36 @@
Leonardo (leonardo) 2011-10-26
-Notes:
+Tactic Documentation:
+
+## Tactic sat
+
+### Short Description
+
+Try to solve goal using a SAT solver
+
+## Tactic sat-preprocess
+
+### Short Description
+
+Apply SAT solver preprocessing procedures (bounded resolution, Boolean
constant propagation, 2-SAT, subsumption, subsumption resolution).
+
+### Example
+
+```z3
+(declare-const a Bool)
+(declare-const b Bool)
+(declare-const c Bool)
+(declare-const d Bool)
+(declare-const e Bool)
+(declare-const f Bool)
+(declare-fun p (Bool) Bool)
+(assert (=> a b))
+(assert (=> b c))
+(assert a)
+(assert (not c))
+(apply sat-preprocess)
+```
--*/
#pragma once
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/smt/smt_context.cpp
new/z3-z3-4.12.1/src/smt/smt_context.cpp
--- old/z3-z3-4.12.0/src/smt/smt_context.cpp 2023-01-14 15:24:26.000000000
+0100
+++ new/z3-z3-4.12.1/src/smt/smt_context.cpp 2023-01-18 04:10:26.000000000
+0100
@@ -866,6 +866,7 @@
SASSERT(curr != m_false_enode);
bool_var v = enode2bool_var(curr);
literal l(v, sign);
+ CTRACE("propagate", (get_assignment(l) != l_true), tout <<
enode_pp(curr, *this) << " " << l << "\n");
if (get_assignment(l) != l_true)
assign(l,
mk_justification(eq_root_propagation_justification(curr)));
curr = curr->m_next;
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/smt/smt_model_checker.cpp
new/z3-z3-4.12.1/src/smt/smt_model_checker.cpp
--- old/z3-z3-4.12.0/src/smt/smt_model_checker.cpp 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/smt/smt_model_checker.cpp 2023-01-18
04:10:26.000000000 +0100
@@ -82,22 +82,18 @@
app* fresh_term;
if (is_app(val) && to_app(val)->get_num_args() > 0) {
ptr_buffer<expr> args;
- for (expr* arg : *to_app(val)) {
+ for (expr* arg : *to_app(val))
args.push_back(get_type_compatible_term(arg));
- }
fresh_term = m.mk_app(to_app(val)->get_decl(), args.size(),
args.data());
}
else {
expr * sk_term = get_term_from_ctx(val);
- if (sk_term != nullptr) {
+ if (sk_term != nullptr)
return sk_term;
- }
- for (expr* f : m_fresh_exprs) {
- if (f->get_sort() == val->get_sort()) {
+ for (expr* f : m_fresh_exprs)
+ if (f->get_sort() == val->get_sort())
return f;
- }
- }
fresh_term = m.mk_fresh_const("sk", val->get_sort());
}
m_fresh_exprs.push_back(fresh_term);
@@ -106,13 +102,16 @@
}
void model_checker::init_value2expr() {
+
if (m_value2expr.empty()) {
// populate m_value2expr
for (auto const& kv : *m_root2value) {
enode * n = kv.m_key;
expr * val = kv.m_value;
n = n->get_eq_enode_with_min_gen();
- m_value2expr.insert(val, n->get_expr());
+ expr* e = n->get_expr();
+ if (!m.is_value(e))
+ m_value2expr.insert(val, e);
}
}
}
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/smt/smt_model_generator.cpp
new/z3-z3-4.12.1/src/smt/smt_model_generator.cpp
--- old/z3-z3-4.12.0/src/smt/smt_model_generator.cpp 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/smt/smt_model_generator.cpp 2023-01-18
04:10:26.000000000 +0100
@@ -330,27 +330,32 @@
enode * n = curr.get_enode();
SASSERT(n->get_root() == n);
TRACE("mg_top_sort", tout << curr << "\n";);
- dependencies.reset();
- dependency_values.reset();
- model_value_proc * proc = root2proc[n];
- SASSERT(proc);
- proc->get_dependencies(dependencies);
- for (model_value_dependency const& d : dependencies) {
- if (d.is_fresh_value()) {
- CTRACE("mg_top_sort", !d.get_value()->get_value(),
- tout << "#" << n->get_owner_id() << " " <<
mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
- SASSERT(d.get_value()->get_value());
-
dependency_values.push_back(d.get_value()->get_value());
- }
- else {
- enode * child = d.get_enode();
- TRACE("mg_top_sort", tout << "#" << n->get_owner_id()
<< " (" << mk_pp(n->get_expr(), m) << "): "
- << mk_pp(child->get_expr(), m) << " " <<
mk_pp(child->get_root()->get_expr(), m) << "\n";);
- child = child->get_root();
- dependency_values.push_back(m_root2value[child]);
+ app* val = nullptr;
+ if (m.is_value(n->get_expr()))
+ val = to_app(n->get_expr());
+ else {
+ dependencies.reset();
+ dependency_values.reset();
+ model_value_proc * proc = root2proc[n];
+ SASSERT(proc);
+ proc->get_dependencies(dependencies);
+ for (model_value_dependency const& d : dependencies) {
+ if (d.is_fresh_value()) {
+ CTRACE("mg_top_sort", !d.get_value()->get_value(),
+ tout << "#" << n->get_owner_id() << " " <<
mk_pp(n->get_expr(), m) << " -> " << d << "\n";);
+ SASSERT(d.get_value()->get_value());
+
dependency_values.push_back(d.get_value()->get_value());
+ }
+ else {
+ enode * child = d.get_enode();
+ TRACE("mg_top_sort", tout << "#" <<
n->get_owner_id() << " (" << mk_pp(n->get_expr(), m) << "): "
+ << mk_pp(child->get_expr(), m) << " " <<
mk_pp(child->get_root()->get_expr(), m) << "\n";);
+ child = child->get_root();
+ dependency_values.push_back(m_root2value[child]);
+ }
}
+ val = proc->mk_value(*this, dependency_values);
}
- app * val = proc->mk_value(*this, dependency_values);
register_value(val);
m_asts.push_back(val);
m_root2value.insert(n, val);
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/z3-z3-4.12.0/src/smt/tactic/ctx_solver_simplify_tactic.h
new/z3-z3-4.12.1/src/smt/tactic/ctx_solver_simplify_tactic.h
--- old/z3-z3-4.12.0/src/smt/tactic/ctx_solver_simplify_tactic.h
2023-01-14 15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/smt/tactic/ctx_solver_simplify_tactic.h
2023-01-18 04:10:26.000000000 +0100
@@ -13,7 +13,17 @@
Nikolaj (nbjorner) 2012-3-6
-Notes:
+Tactic Documentation:
+
+## Tactic ctx-solver-simplify
+
+### Short Description
+
+A heavy handed version of `ctx-simplify`. It applies SMT checks on
sub-formulas to check
+if they can be simplified to `true` or `false` within their context.
+Note that a sub-formula may occur within multiple contexts due to shared
sub-terms.
+In this case the tactic is partial and simplifies a limited number of context
occurrences.
+
--*/
#pragma once
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/z3-z3-4.12.0/src/smt/tactic/unit_subsumption_tactic.h
new/z3-z3-4.12.1/src/smt/tactic/unit_subsumption_tactic.h
--- old/z3-z3-4.12.0/src/smt/tactic/unit_subsumption_tactic.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/smt/tactic/unit_subsumption_tactic.h 2023-01-18
04:10:26.000000000 +0100
@@ -13,12 +13,20 @@
Nikolaj Bjorner (nbjorner) 2012-9-6
-Notes:
+Tactic Documentation:
- Background: PDR generates several clauses that subsume each-other.
- Simplify a goal assuming it is a conjunction of clauses.
- Subsumed clauses are simplified by using unit-propagation
- It uses the smt_context for the solver.
+## Tactic unit-subsume-simplify
+
+### Short Description
+
+implify goal using subsumption based on unit propagation
+
+### Long Description
+
+Background: PDR generates several clauses that subsume each-other.
+Simplify a goal assuming it is a conjunction of clauses.
+Subsumed clauses are simplified by using unit-propagation
+It uses the default SMT solver.
--*/
#pragma once
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/tactic/arith/arith_bounds_tactic.h
new/z3-z3-4.12.1/src/tactic/arith/arith_bounds_tactic.h
--- old/z3-z3-4.12.0/src/tactic/arith/arith_bounds_tactic.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/tactic/arith/arith_bounds_tactic.h 2023-01-18
04:10:26.000000000 +0100
@@ -27,6 +27,8 @@
for assembling bounds, but it does not have a way to check for
subsumption of atoms.
+## Tactic arith-bounds
+
--*/
#pragma once
#include "tactic/tactic.h"
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/z3-z3-4.12.0/src/tactic/core/cofactor_elim_term_ite.cpp
new/z3-z3-4.12.1/src/tactic/core/cofactor_elim_term_ite.cpp
--- old/z3-z3-4.12.0/src/tactic/core/cofactor_elim_term_ite.cpp 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/tactic/core/cofactor_elim_term_ite.cpp 2023-01-18
04:10:26.000000000 +0100
@@ -128,9 +128,8 @@
fr.m_first = false;
bool visited = true;
if (is_app(t)) {
- unsigned num_args = to_app(t)->get_num_args();
- for (unsigned i = 0; i < num_args; i++)
- visit(to_app(t)->get_arg(i), form_ctx, visited);
+ for (expr* arg : *to_app(t))
+ visit(arg, form_ctx, visited);
}
// ignoring quantifiers
if (!visited)
@@ -138,16 +137,13 @@
}
if (is_app(t)) {
- unsigned num_args = to_app(t)->get_num_args();
- unsigned i;
- for (i = 0; i < num_args; i++) {
- if (m_has_term_ite.is_marked(to_app(t)->get_arg(i)))
+ for (expr* arg : *to_app(t)) {
+ if (m_has_term_ite.is_marked(arg)) {
+ m_has_term_ite.mark(t);
+ TRACE("cofactor", tout << "saving candidate: " <<
form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
+ save_candidate(t, form_ctx);
break;
- }
- if (i < num_args) {
- m_has_term_ite.mark(t);
- TRACE("cofactor", tout << "saving candidate: " <<
form_ctx << "\n" << mk_bounded_pp(t, m) << "\n";);
- save_candidate(t, form_ctx);
+ }
}
}
else {
@@ -284,16 +280,14 @@
}
expr * best = nullptr;
unsigned best_occs = 0;
- obj_map<expr, unsigned>::iterator it = occs.begin();
- obj_map<expr, unsigned>::iterator end = occs.end();
- for (; it != end; ++it) {
+ for (auto const& [k, v] : occs) {
if ((!best) ||
- (get_depth(it->m_key) < get_depth(best)) ||
- (get_depth(it->m_key) == get_depth(best) && it->m_value >
best_occs) ||
+ (get_depth(k) < get_depth(best)) ||
+ (get_depth(k) == get_depth(best) && v > best_occs) ||
// break ties by giving preference to equalities
- (get_depth(it->m_key) == get_depth(best) && it->m_value ==
best_occs && m.is_eq(it->m_key) && !m.is_eq(best))) {
- best = it->m_key;
- best_occs = it->m_value;
+ (get_depth(k) == get_depth(best) && v == best_occs &&
m.is_eq(k) && !m.is_eq(best))) {
+ best = k;
+ best_occs = v;
}
}
visited.reset();
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore'
old/z3-z3-4.12.0/src/tactic/core/cofactor_term_ite_tactic.h
new/z3-z3-4.12.1/src/tactic/core/cofactor_term_ite_tactic.h
--- old/z3-z3-4.12.0/src/tactic/core/cofactor_term_ite_tactic.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/tactic/core/cofactor_term_ite_tactic.h 2023-01-18
04:10:26.000000000 +0100
@@ -8,13 +8,22 @@
Abstract:
Wrap cofactor_elim_term_ite as a tactic.
- Eliminate (ground) term if-then-else's using cofactors.
Author:
Leonardo de Moura (leonardo) 2012-02-20.
-Revision History:
+Tactic Documentation:
+
+## Tactic cofactor-term-ite
+
+### Short Description
+Eliminate (ground) term if-then-else's using cofactors.
+It hoists nested if-then-else expressions inside terms into the top level of
the formula.
+
+### Notes
+
+* does not support proofs, does not support cores
--*/
#pragma once
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/tactic/core/euf_completion_tactic.h
new/z3-z3-4.12.1/src/tactic/core/euf_completion_tactic.h
--- old/z3-z3-4.12.0/src/tactic/core/euf_completion_tactic.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/tactic/core/euf_completion_tactic.h 2023-01-18
04:10:26.000000000 +0100
@@ -13,6 +13,22 @@
Nikolaj Bjorner (nbjorner) 2022-10-30
+Tactic Documentation:
+
+## Tactic euf-completion
+
+### Short Description
+
+Uses the ground equalities as a rewrite system. The formulas are simplified
+using the rewrite system.
+
+### Long Description
+
+The tactic uses congruence closure to represent and orient the rewrite system.
Equalities from the formula
+are inserted in the an E-graph (congruence closure structure) and then a
representative that is most shallow
+is extracted.
+
+
--*/
#pragma once
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/tactic/core/reduce_args_tactic.h
new/z3-z3-4.12.1/src/tactic/core/reduce_args_tactic.h
--- old/z3-z3-4.12.0/src/tactic/core/reduce_args_tactic.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/tactic/core/reduce_args_tactic.h 2023-01-18
04:10:26.000000000 +0100
@@ -34,31 +34,10 @@
Since $f_a$, $f_b$, $f_c$ are new symbols, satisfiability is preserved.
This transformation is very similar in spirit to the Ackermman's reduction.
+For each function `f` and argument position of `f` it checks if all
occurrences of `f` uses a value at position `i`.
+The values may be different, but all occurrences have to be values for the
reduction to be applicable.
+It creates a fresh function for each of the different values at position `i`.
-This transformation should work in the following way:
-
-```
- 1- Create a mapping decl2arg_map from declarations to tuples of booleans,
an entry [f -> (true, false, true)]
- means that f is a declaration with 3 arguments where the first and
third arguments are always values.
- 2- Traverse the formula and populate the mapping.
- For each function application f(t1, ..., tn) do
- a) Create a boolean tuple (is_value(t1), ..., is_value(tn)) and do
- the logical-and with the tuple that is already in the mapping. If
there is no such tuple
- in the mapping, we just add a new entry.
-
- If all entries are false-tuples, then there is nothing to be done. The
transformation is not applicable.
-
- Now, we create a mapping decl2new_decl from (decl, val_1, ..., val_n) to
decls. Note that, n may be different for each entry,
- but it is the same for the same declaration.
- For example, suppose we have [f -> (true, false, true)] in decl2arg_map,
- and applications f(1, a, 2), f(1, b, 2), f(1, b, 3), f(2, b, 3), f(2, c, 3)
in the formula.
- Then, decl2arg_map would contain
- (f, 1, 2) -> f_1_2
- (f, 1, 3) -> f_1_3
- (f, 2, 3) -> f_2_3
- where f_1_2, f_1_3 and f_2_3 are new function symbols.
- Using the new map, we can replace the occurrences of f.
-```
### Example
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/tactic/core/tseitin_cnf_tactic.cpp
new/z3-z3-4.12.1/src/tactic/core/tseitin_cnf_tactic.cpp
--- old/z3-z3-4.12.0/src/tactic/core/tseitin_cnf_tactic.cpp 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/tactic/core/tseitin_cnf_tactic.cpp 2023-01-18
04:10:26.000000000 +0100
@@ -865,11 +865,11 @@
void collect_param_descrs(param_descrs & r) override {
insert_max_memory(r);
- r.insert("common_patterns", CPK_BOOL, "(default: true) minimize the
number of auxiliary variables during CNF encoding by identifing commonly used
patterns");
- r.insert("distributivity", CPK_BOOL, "(default: true) minimize the
number of auxiliary variables during CNF encoding by applying distributivity
over unshared subformulas");
- r.insert("distributivity_blowup", CPK_UINT, "(default: 32) maximum
overhead for applying distributivity during CNF encoding");
- r.insert("ite_chaing", CPK_BOOL, "(default: true) minimize the number
of auxiliary variables during CNF encoding by identifing if-then-else chains");
- r.insert("ite_extra", CPK_BOOL, "(default: true) add redundant clauses
(that improve unit propagation) when encoding if-then-else formulas");
+ r.insert("common_patterns", CPK_BOOL, "minimize the number of
auxiliary variables during CNF encoding by identifing commonly used patterns",
"true");
+ r.insert("distributivity", CPK_BOOL, "minimize the number of auxiliary
variables during CNF encoding by applying distributivity over unshared
subformulas", "true");
+ r.insert("distributivity_blowup", CPK_UINT, "maximum overhead for
applying distributivity during CNF encoding", "32");
+ r.insert("ite_chaing", CPK_BOOL, "minimize the number of auxiliary
variables during CNF encoding by identifing if-then-else chains", "true");
+ r.insert("ite_extra", CPK_BOOL, "add redundant clauses (that improve
unit propagation) when encoding if-then-else formulas", "true");
}
void operator()(goal_ref const & in, goal_ref_buffer & result) override {
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/tactic/fpa/fpa2bv_tactic.h
new/z3-z3-4.12.1/src/tactic/fpa/fpa2bv_tactic.h
--- old/z3-z3-4.12.0/src/tactic/fpa/fpa2bv_tactic.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/tactic/fpa/fpa2bv_tactic.h 2023-01-18
04:10:26.000000000 +0100
@@ -5,15 +5,16 @@
fpa2bv_tactic.h
-Abstract:
-
- Tactic that converts floating points to bit-vectors
-
Author:
Christoph (cwinter) 2012-02-09
-Notes:
+Tactic Documentation:
+
+## Tactic fpa2bv
+
+### Short Description
+Converts floating points to bit-vector representation.
--*/
#pragma once
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/tactic/fpa/qffp_tactic.h
new/z3-z3-4.12.1/src/tactic/fpa/qffp_tactic.h
--- old/z3-z3-4.12.0/src/tactic/fpa/qffp_tactic.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/tactic/fpa/qffp_tactic.h 2023-01-18
04:10:26.000000000 +0100
@@ -13,8 +13,17 @@
Christoph (cwinter) 2012-01-16
-Notes:
+Tactic Documentation:
+## Tactic qffp
+
+### Short Description
+Tactic for QF_FP formulas
+
+## Tactic qffpbv
+
+### Short Description
+Tactic for QF_FPBV formulas
--*/
#pragma once
diff -urN '--exclude=CVS' '--exclude=.cvsignore' '--exclude=.svn'
'--exclude=.svnignore' old/z3-z3-4.12.0/src/tactic/fpa/qffplra_tactic.h
new/z3-z3-4.12.1/src/tactic/fpa/qffplra_tactic.h
--- old/z3-z3-4.12.0/src/tactic/fpa/qffplra_tactic.h 2023-01-14
15:24:26.000000000 +0100
+++ new/z3-z3-4.12.1/src/tactic/fpa/qffplra_tactic.h 2023-01-18
04:10:26.000000000 +0100
@@ -14,7 +14,8 @@
Christoph (cwinter) 2018-04-24
-Notes:
+
+## Tactic qffplra
--*/
