mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

Merge branch 'upstream-master' into develop

Browse source
This commit is contained in:
Murphy Berzish 2017-04-26 17:21:10 -04:00
parent 6fececaad9 a048d74bae
commit d16b20d62b
12 changed files with 247 additions and 49 deletions

7
LICENSE.txt
View file

@ -2,6 +2,9 @@ Z3
Copyright (c) Microsoft Corporation
All rights reserved.
MIT License
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the ""Software""), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

1
contrib/cmake/src/test/CMakeLists.txt
View file

@ -23,6 +23,7 @@ add_executable(test-z3
bv_simplifier_plugin.cpp
chashtable.cpp
check_assumptions.cpp
cnf_backbones.cpp
datalog_parser.cpp
ddnf.cpp
diff_logic.cpp

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

@ -6194,7 +6194,7 @@ class Solver(Z3PPObject):
>>> s.consequences([a],[b,c,d])
(sat, [Implies(a, b), Implies(a, c)])
>>> s.consequences([Not(c),d],[a,b,c,d])
(sat, [Implies(Not(c), Not(c)), Implies(d, d), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
(sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))])
"""
if isinstance(assumptions, list):
_asms = AstVector(None, self.ctx)

7
src/interp/iz3proof_itp.cpp
View file

@ -541,6 +541,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
placeholder_arg |= is_placeholder(args[i]);
}
try {
TRACE("duality", print_expr(tout, e); tout << "\n";);
opr f = op(e);
if(f == Equal && args[0] == args[1]) res = mk_true();
else if(f == And) res = my_and(args);
@ -853,6 +854,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast simplify_rotate_eq2leq(const ast &pl, const ast &neg_equality, const ast &pf){
if(pl == arg(pf,1)){
TRACE("duality", print_expr(tout, pl); print_expr(tout << "\n", neg_equality); print_expr(tout << "\n", pf); tout << "\n";);
ast cond = mk_true();
ast equa = sep_cond(arg(pf,0),cond);
if(is_equivrel_chain(equa)){
@ -1870,10 +1872,13 @@ class iz3proof_itp_impl : public iz3proof_itp {
ast chain_ineqs(opr comp_op, LitType t, const ast &chain, const ast &lhs, const ast &rhs){
if(is_true(chain)){
if(lhs != rhs)
if (lhs != rhs) {
TRACE("duality", print_expr(tout, lhs); tout << " "; print_expr(tout, rhs); tout << "\n";);
throw bad_ineq_inference();
}
return make(Leq,make_int(rational(0)),make_int(rational(0)));
}
TRACE("duality", print_expr(tout, chain); print_expr(tout << "\n", lhs); tout << " "; print_expr(tout, rhs); tout << "\n";);
ast last = chain_last(chain);
ast rest = chain_rest(chain);
ast mid = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last));

2
src/opt/opt_context.cpp
View file

@ -1235,7 +1235,7 @@ namespace opt {
out << " (";
display_objective(out, obj);
if (get_lower_as_num(i) != get_upper_as_num(i)) {
out << " (" << get_lower(i) << " " << get_upper(i) << ")";
out << " (interval " << get_lower(i) << " " << get_upper(i) << ")";
}
else {
out << " " << get_lower(i);

20
src/sat/sat_solver.cpp
View file

@ -3284,13 +3284,17 @@ namespace sat {
checkpoint();
literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end();
unsigned num_resolves = 0;
unsigned num_fixed = 0;
unsigned num_assigned = 0;
lbool is_sat = l_true;
for (; it != end; ++it) {
literal lit = *it;
literal lit = *it;
if (value(lit) != l_undef) {
++num_fixed;
continue;
}
push();
++num_assigned;
assign(~lit, justification());
propagate(false);
while (inconsistent()) {
@ -3307,8 +3311,18 @@ namespace sat {
break;
}
}
if (scope_lvl() == 1) {
it = unfixed_lits.begin();
for (; it != end; ++it) {
literal lit = *it;
if (value(lit) == l_true) {
VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq));
}
}
}
if (is_sat == l_true) {
if (scope_lvl() == 1 && num_resolves > 0) {
IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences backjump)\n";);
is_sat = l_undef;
}
else {
@ -3325,12 +3339,14 @@ namespace sat {
if (is_sat == l_true) {
delete_unfixed(unfixed_lits, unfixed_vars);
}
extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq);
extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq);
update_unfixed_literals(unfixed_lits, unfixed_vars);
IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences"
<< " iterations: " << num_iterations
<< " variables: " << unfixed_lits.size()
<< " fixed: " << conseq.size()
<< " status: " << is_sat
<< " pre-assigned: " << num_fixed
<< " unfixed: " << lits.size() - conseq.size() - unfixed_lits.size()
<< ")\n";);

1
src/sat/sat_solver.h
View file

@ -247,6 +247,7 @@ namespace sat {
unsigned num_clauses() const;
unsigned num_restarts() const { return m_restarts; }
bool is_external(bool_var v) const { return m_external[v] != 0; }
void set_external(bool_var v) { m_external[v] = true; }
bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; }
unsigned scope_lvl() const { return m_scope_lvl; }
lbool value(literal l) const { return static_cast<lbool>(m_assignment[l.index()]); }

137
src/smt/smt_consequences.cpp
View file

@ -30,6 +30,7 @@ namespace smt {
index_set::iterator it = vars.begin(), end = vars.end();
for (; it != end; ++it) {
expr* e = bool_var2expr(*it);
e = m_assumption2orig.find(e);
premises.push_back(get_assignment(*it) != l_false ? e : m_manager.mk_not(e));
}
return mk_and(premises);
@ -44,13 +45,14 @@ namespace smt {
// - e is an equality between a variable and value that is to be fixed.
// - e is a data-type recognizer of a variable that is to be fixed.
//
void context::extract_fixed_consequences(literal lit, obj_map<expr, expr*>& vars, index_set const& assumptions, expr_ref_vector& conseq) {
void context::extract_fixed_consequences(literal lit, index_set const& assumptions, expr_ref_vector& conseq) {
ast_manager& m = m_manager;
datatype_util dt(m);
expr* e1, *e2;
expr_ref fml(m);
if (lit == true_literal) return;
expr* e = bool_var2expr(lit.var());
TRACE("context", display(tout << mk_pp(e, m) << "\n"););
index_set s;
if (assumptions.contains(lit.var())) {
s.insert(lit.var());
@ -65,26 +67,32 @@ namespace smt {
}
tout << "\n";);
bool found = false;
if (vars.contains(e)) {
if (m_var2val.contains(e)) {
found = true;
m_var2val.erase(e);
e = m_var2orig.find(e);
fml = lit.sign() ? m.mk_not(e) : e;
vars.erase(e);
}
else if (!lit.sign() && m.is_eq(e, e1, e2)) {
if (vars.contains(e2)) {
std::swap(e1, e2);
}
if (vars.contains(e1) && m.is_value(e2)) {
if (m_var2val.contains(e2) && m.is_value(e1)) {
found = true;
fml = e;
vars.erase(e1);
m_var2val.erase(e2);
e2 = m_var2orig.find(e2);
std::swap(e1, e2);
fml = m.mk_eq(e1, e2);
}
else if (m_var2val.contains(e1) && m.is_value(e2)) {
found = true;
m_var2val.erase(e1);
e1 = m_var2orig.find(e1);
fml = m.mk_eq(e1, e2);
}
}
else if (!lit.sign() && is_app(e) && dt.is_recognizer(to_app(e)->get_decl())) {
if (vars.contains(to_app(e)->get_arg(0))) {
if (m_var2val.contains(to_app(e)->get_arg(0))) {
found = true;
fml = m.mk_eq(to_app(e)->get_arg(0), m.mk_const(dt.get_recognizer_constructor(to_app(e)->get_decl())));
vars.erase(to_app(e)->get_arg(0));
m_var2val.erase(to_app(e)->get_arg(0));
}
}
if (found) {
@ -94,6 +102,7 @@ namespace smt {
}
void context::justify(literal lit, index_set& s) {
ast_manager& m = m_manager;
b_justification js = get_justification(lit.var());
switch (js.get_kind()) {
case b_justification::CLAUSE: {
@ -119,6 +128,9 @@ namespace smt {
literal_vector literals;
m_conflict_resolution->justification2literals(js.get_justification(), literals);
for (unsigned j = 0; j < literals.size(); ++j) {
if (!m_antecedents.contains(literals[j].var())) {
TRACE("context", tout << literals[j] << " " << mk_pp(bool_var2expr(literals[j].var()), m) << "\n";);
}
s |= m_antecedents.find(literals[j].var());
}
break;
@ -126,13 +138,13 @@ namespace smt {
}
}
void context::extract_fixed_consequences(unsigned& start, obj_map<expr, expr*>& vars, index_set const& assumptions, expr_ref_vector& conseq) {
void context::extract_fixed_consequences(unsigned& start, index_set const& assumptions, expr_ref_vector& conseq) {
pop_to_search_lvl();
SASSERT(!inconsistent());
literal_vector const& lits = assigned_literals();
unsigned sz = lits.size();
for (unsigned i = start; i < sz; ++i) {
extract_fixed_consequences(lits[i], vars, assumptions, conseq);
extract_fixed_consequences(lits[i], assumptions, conseq);
}
start = sz;
SASSERT(!inconsistent());
@ -150,10 +162,10 @@ namespace smt {
// rules out as many non-fixed variables as possible.
//
unsigned context::delete_unfixed(obj_map<expr, expr*>& var2val, expr_ref_vector& unfixed) {
unsigned context::delete_unfixed(expr_ref_vector& unfixed) {
ast_manager& m = m_manager;
ptr_vector<expr> to_delete;
obj_map<expr,expr*>::iterator it = var2val.begin(), end = var2val.end();
obj_map<expr,expr*>::iterator it = m_var2val.begin(), end = m_var2val.end();
for (; it != end; ++it) {
expr* k = it->m_key;
expr* v = it->m_value;
@ -189,7 +201,7 @@ namespace smt {
}
}
for (unsigned i = 0; i < to_delete.size(); ++i) {
var2val.remove(to_delete[i]);
m_var2val.remove(to_delete[i]);
unfixed.push_back(to_delete[i]);
}
return to_delete.size();
@ -202,12 +214,12 @@ namespace smt {
// Add a clause to short-circuit the congruence justifications for
// next rounds.
//
unsigned context::extract_fixed_eqs(obj_map<expr, expr*>& var2val, expr_ref_vector& conseq) {
unsigned context::extract_fixed_eqs(expr_ref_vector& conseq) {
TRACE("context", tout << "extract fixed consequences\n";);
ast_manager& m = m_manager;
ptr_vector<expr> to_delete;
expr_ref fml(m), eq(m);
obj_map<expr,expr*>::iterator it = var2val.begin(), end = var2val.end();
obj_map<expr,expr*>::iterator it = m_var2val.begin(), end = m_var2val.end();
for (; it != end; ++it) {
expr* k = it->m_key;
expr* v = it->m_value;
@ -220,7 +232,7 @@ namespace smt {
s |= m_antecedents.find(literals[i].var());
}
fml = m.mk_eq(k, v);
fml = m.mk_eq(m_var2orig.find(k), v);
fml = m.mk_implies(antecedent2fml(s), fml);
conseq.push_back(fml);
to_delete.push_back(k);
@ -235,16 +247,20 @@ namespace smt {
}
}
for (unsigned i = 0; i < to_delete.size(); ++i) {
var2val.remove(to_delete[i]);
m_var2val.remove(to_delete[i]);
}
return to_delete.size();
}
literal context::mk_diseq(expr* e, expr* val) {
ast_manager& m = m_manager;
if (m.is_bool(e)) {
if (m.is_bool(e) && b_internalized(e)) {
return literal(get_bool_var(e), m.is_true(val));
}
else if (m.is_bool(e)) {
internalize_formula(e, false);
return literal(get_bool_var(e), !m.is_true(val));
}
else {
expr_ref eq(mk_eq_atom(e, val), m);
internalize_formula(eq, false);
@ -252,43 +268,85 @@ namespace smt {
}
}
lbool context::get_consequences(expr_ref_vector const& assumptions,
expr_ref_vector const& vars,
lbool context::get_consequences(expr_ref_vector const& assumptions0,
expr_ref_vector const& vars0,
expr_ref_vector& conseq,
expr_ref_vector& unfixed) {
m_antecedents.reset();
m_antecedents.insert(true_literal.var(), index_set());
pop_to_base_lvl();
ast_manager& m = m_manager;
expr_ref_vector vars(m), assumptions(m);
m_var2val.reset();
m_var2orig.reset();
m_assumption2orig.reset();
bool pushed = false;
for (unsigned i = 0; i < vars0.size(); ++i) {
expr* v = vars0[i];
if (is_uninterp_const(v)) {
vars.push_back(v);
m_var2orig.insert(v, v);
}
else {
if (!pushed) {
pushed = true;
push();
}
expr_ref c(m.mk_fresh_const("v", m.get_sort(v)), m);
expr_ref eq(m.mk_eq(c, v), m);
assert_expr(eq);
vars.push_back(c);
m_var2orig.insert(c, v);
}
}
for (unsigned i = 0; i < assumptions0.size(); ++i) {
expr* a = assumptions0[i];
if (is_uninterp_const(a)) {
assumptions.push_back(a);
m_assumption2orig.insert(a, a);
}
else {
if (!pushed) {
pushed = true;
push();
}
expr_ref c(m.mk_fresh_const("a", m.get_sort(a)), m);
expr_ref eq(m.mk_eq(c, a), m);
assert_expr(eq);
assumptions.push_back(c);
m_assumption2orig.insert(c, a);
}
}
lbool is_sat = check(assumptions.size(), assumptions.c_ptr());
if (is_sat != l_true) {
TRACE("context", tout << is_sat << "\n";);
if (pushed) pop(1);
return is_sat;
}
obj_map<expr, expr*> var2val;
index_set _assumptions;
for (unsigned i = 0; i < assumptions.size(); ++i) {
_assumptions.insert(get_literal(assumptions[i]).var());
_assumptions.insert(get_literal(assumptions[i].get()).var());
}
model_ref mdl;
get_model(mdl);
ast_manager& m = m_manager;
expr_ref_vector trail(m);
model_evaluator eval(*mdl.get());
expr_ref val(m);
TRACE("context", model_pp(tout, *mdl););
for (unsigned i = 0; i < vars.size(); ++i) {
eval(vars[i], val);
eval(vars[i].get(), val);
if (m.is_value(val)) {
trail.push_back(val);
var2val.insert(vars[i], val);
m_var2val.insert(vars[i].get(), val);
}
else {
unfixed.push_back(vars[i]);
unfixed.push_back(vars[i].get());
}
}
unsigned num_units = 0;
extract_fixed_consequences(num_units, var2val, _assumptions, conseq);
extract_fixed_consequences(num_units, _assumptions, conseq);
app_ref eq(m);
TRACE("context",
tout << "vars: " << vars.size() << "\n";
@ -298,11 +356,12 @@ namespace smt {
unsigned num_fixed_eqs = 0;
unsigned chunk_size = 100;
while (!var2val.empty()) {
obj_map<expr,expr*>::iterator it = var2val.begin(), end = var2val.end();
while (!m_var2val.empty()) {
obj_map<expr,expr*>::iterator it = m_var2val.begin(), end = m_var2val.end();
unsigned num_vars = 0;
for (; it != end && num_vars < chunk_size; ++it) {
if (get_cancel_flag()) {
if (pushed) pop(1);
return l_undef;
}
expr* e = it->m_key;
@ -332,6 +391,7 @@ namespace smt {
while (true) {
is_sat = bounded_search();
if (is_sat != l_true && m_last_search_failure != OK) {
if (pushed) pop(1);
return is_sat;
}
if (is_sat == l_undef) {
@ -347,18 +407,21 @@ namespace smt {
m_not_l = null_literal;
}
if (is_sat == l_true) {
delete_unfixed(var2val, unfixed);
delete_unfixed(unfixed);
}
extract_fixed_consequences(num_units, var2val, _assumptions, conseq);
num_fixed_eqs += extract_fixed_eqs(var2val, conseq);
IF_VERBOSE(1, display_consequence_progress(verbose_stream(), num_iterations, var2val.size(), conseq.size(),
extract_fixed_consequences(num_units, _assumptions, conseq);
num_fixed_eqs += extract_fixed_eqs(conseq);
IF_VERBOSE(1, display_consequence_progress(verbose_stream(), num_iterations, m_var2val.size(), conseq.size(),
unfixed.size(), num_fixed_eqs););
TRACE("context", display_consequence_progress(tout, num_iterations, var2val.size(), conseq.size(),
TRACE("context", display_consequence_progress(tout, num_iterations, m_var2val.size(), conseq.size(),
unfixed.size(), num_fixed_eqs););
}
end_search();
DEBUG_CODE(validate_consequences(assumptions, vars, conseq, unfixed););
if (pushed) {
pop(1);
}
return l_true;
}

11
src/smt/smt_context.h
View file

@ -1411,14 +1411,17 @@ namespace smt {
typedef hashtable<unsigned, u_hash, u_eq> index_set;
//typedef uint_set index_set;
u_map<index_set> m_antecedents;
void extract_fixed_consequences(literal lit, obj_map<expr, expr*>& var2val, index_set const& assumptions, expr_ref_vector& conseq);
void extract_fixed_consequences(unsigned& idx, obj_map<expr, expr*>& var2val, index_set const& assumptions, expr_ref_vector& conseq);
obj_map<expr, expr*> m_var2orig;
obj_map<expr, expr*> m_assumption2orig;
obj_map<expr, expr*> m_var2val;
void extract_fixed_consequences(literal lit, index_set const& assumptions, expr_ref_vector& conseq);
void extract_fixed_consequences(unsigned& idx, index_set const& assumptions, expr_ref_vector& conseq);
void display_consequence_progress(std::ostream& out, unsigned it, unsigned nv, unsigned fixed, unsigned unfixed, unsigned eq);
unsigned delete_unfixed(obj_map<expr, expr*>& var2val, expr_ref_vector& unfixed);
unsigned delete_unfixed(expr_ref_vector& unfixed);
unsigned extract_fixed_eqs(obj_map<expr, expr*>& var2val, expr_ref_vector& conseq);
unsigned extract_fixed_eqs(expr_ref_vector& conseq);
expr_ref antecedent2fml(index_set const& ante);

106
src/test/cnf_backbones.cpp Normal file
View file

@ -0,0 +1,106 @@
/*++
Copyright (c) 2017 Microsoft Corporation
--*/
#include<iostream>
#include<time.h>
#include<signal.h>
#include"timeout.h"
#include"rlimit.h"
#include"dimacs.h"
#include"sat_solver.h"
#include"gparams.h"
static sat::solver * g_solver = 0;
static clock_t g_start_time;
static void display_statistics() {
clock_t end_time = clock();
if (g_solver) {
std::cout.flush();
std::cerr.flush();
statistics st;
g_solver->collect_statistics(st);
st.update("total time", ((static_cast<double>(end_time) - static_cast<double>(g_start_time)) / CLOCKS_PER_SEC));
st.display_smt2(std::cout);
}
}
static void on_timeout() {
display_statistics();
exit(0);
}
static void STD_CALL on_ctrl_c(int) {
signal (SIGINT, SIG_DFL);
display_statistics();
raise(SIGINT);
}
static void display_model(sat::solver const & s) {
sat::model const & m = s.get_model();
for (unsigned i = 1; i < m.size(); i++) {
switch (m[i]) {
case l_false: std::cout << "-" << i << " "; break;
case l_undef: break;
case l_true: std::cout << i << " "; break;
}
}
std::cout << "\n";
}
static void cnf_backbones(char const* file_name) {
g_start_time = clock();
register_on_timeout_proc(on_timeout);
signal(SIGINT, on_ctrl_c);
params_ref p = gparams::get_module("sat");
p.set_bool("produce_models", true);
reslimit limit;
sat::solver solver(p, limit, 0);
g_solver = &solver;
if (file_name) {
std::ifstream in(file_name);
if (in.bad() || in.fail()) {
std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl;
exit(ERR_OPEN_FILE);
}
parse_dimacs(in, solver);
}
else {
parse_dimacs(std::cin, solver);
}
IF_VERBOSE(20, solver.display_status(verbose_stream()););
vector<sat::literal_vector> conseq;
sat::bool_var_vector vars;
sat::literal_vector assumptions;
for (unsigned i = 1; i < solver.num_vars(); ++i) {
vars.push_back(i);
solver.set_external(i);
}
lbool r = solver.get_consequences(assumptions, vars, conseq);
switch (r) {
case l_true:
std::cout << "sat\n";
std::cout << vars.size() << " " << conseq.size() << "\n";
break;
case l_undef:
std::cout << "unknown\n";
break;
case l_false:
std::cout << "unsat\n";
break;
}
display_statistics();
}
void tst_cnf_backbones(char ** argv, int argc, int& i) {
if (i + 1 < argc) {
cnf_backbones(argv[i + 1]);
++i;
}
}

1
src/test/ddnf.cpp
View file

@ -1,4 +1,3 @@
/*++
Copyright (c) 2015 Microsoft Corporation

1
src/test/main.cpp
View file

@ -229,6 +229,7 @@ int main(int argc, char ** argv) {
TST(model_evaluator);
TST(get_consequences);
TST(pb2bv);
TST_ARGV(cnf_backbones);
//TST_ARGV(hs);
}