mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

moving remaining qsat functionality over

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-19 15:35:26 -07:00
parent 296addf246
commit 20bbdfe31a
23 changed files with 3876 additions and 225 deletions
Download patch file Download diff file Expand all files Collapse all files

1
contrib/cmake/src/ast/rewriter/CMakeLists.txt
View file

@ -12,6 +12,7 @@ z3_add_component(rewriter
expr_safe_replace.cpp
factor_rewriter.cpp
fpa_rewriter.cpp
label_rewriter.cpp
mk_simplified_app.cpp
pb_rewriter.cpp
quant_hoist.cpp

8
contrib/cmake/src/qe/CMakeLists.txt
View file

@ -1,6 +1,7 @@
z3_add_component(qe
SOURCES
nlarith_util.cpp
nlqsat.cpp
qe_arith.cpp
qe_arith_plugin.cpp
qe_array_plugin.cpp
@ -16,9 +17,12 @@ z3_add_component(qe
qe_mbp.cpp
qe_sat_tactic.cpp
qe_tactic.cpp
qe_util.cpp
qsat.cpp
vsubst_tactic.cpp
COMPONENT_DEPENDENCIES
nlsat_tactic
nlqsat
sat
smt
smt
tactic
)

2
scripts/mk_project.py
View file

@ -57,7 +57,7 @@ def init_project_def():
add_lib('fuzzing', ['ast'], 'test/fuzzing')
add_lib('smt_tactic', ['smt'], 'smt/tactic')
add_lib('sls_tactic', ['tactic', 'normal_forms', 'core_tactics', 'bv_tactics'], 'tactic/sls')
add_lib('qe', ['smt','sat'], 'qe')
add_lib('qe', ['smt','sat','nlsat','tactic','nlsat_tactic'], 'qe')
add_lib('duality', ['smt', 'interp', 'qe'])
add_lib('muz', ['smt', 'sat', 'smt2parser', 'aig_tactic', 'qe'], 'muz/base')
add_lib('dataflow', ['muz'], 'muz/dataflow')

33
src/api/c++/z3++.h
View file

@ -608,12 +608,12 @@ namespace z3 {
small integers, 64 bit integers or rational or decimal strings.
*/
bool is_numeral() const { return kind() == Z3_NUMERAL_AST; }
bool is_numeral_i64(__int64& i) const { bool r = Z3_get_numeral_int64(ctx(), m_ast, &i); return r;}
bool is_numeral_u64(__uint64& i) const { bool r = Z3_get_numeral_uint64(ctx(), m_ast, &i); return r;}
bool is_numeral_i(int& i) const { bool r = Z3_get_numeral_int(ctx(), m_ast, &i); return r;}
bool is_numeral_u(unsigned& i) const { bool r = Z3_get_numeral_uint(ctx(), m_ast, &i); return r;}
bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); return true; }
bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); return true; }
bool is_numeral_i64(__int64& i) const { bool r = 0 != Z3_get_numeral_int64(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_u64(__uint64& i) const { bool r = 0 != Z3_get_numeral_uint64(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_i(int& i) const { bool r = 0 != Z3_get_numeral_int(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral_u(unsigned& i) const { bool r = 0 != Z3_get_numeral_uint(ctx(), m_ast, &i); check_error(); return r;}
bool is_numeral(std::string& s) const { if (!is_numeral()) return false; s = Z3_get_numeral_string(ctx(), m_ast); check_error(); return true; }
bool is_numeral(std::string& s, unsigned precision) const { if (!is_numeral()) return false; s = Z3_get_numeral_decimal_string(ctx(), m_ast, precision); check_error(); return true; }
/**
\brief Return true if this expression is an application.
*/
@ -633,7 +633,7 @@ namespace z3 {
/**
\brief Return true if expression is an algebraic number.
*/
bool is_algebraic() const { return Z3_is_algebraic_number(ctx(), m_ast); }
bool is_algebraic() const { return 0 != Z3_is_algebraic_number(ctx(), m_ast); }
/**
\brief Return true if this expression is well sorted (aka type correct).
@ -657,12 +657,11 @@ namespace z3 {
\pre is_numeral()
*/
int get_numeral_int() const {
assert(is_numeral());
int get_numeral_int() const {
int result;
Z3_bool state = Z3_get_numeral_int(ctx(), m_ast, &result);
if (state != Z3_TRUE)
if (!is_numeral_i(result)) {
throw exception("numeral does not fit in machine int");
}
return result;
}
@ -675,9 +674,9 @@ namespace z3 {
unsigned get_numeral_uint() const {
assert(is_numeral());
unsigned result;
Z3_bool state = Z3_get_numeral_uint(ctx(), m_ast, &result);
if (state != Z3_TRUE)
if (!is_numeral_u(result)) {
throw exception("numeral does not fit in machine uint");
}
return result;
}
@ -690,9 +689,9 @@ namespace z3 {
__int64 get_numeral_int64() const {
assert(is_numeral());
__int64 result;
Z3_bool state = Z3_get_numeral_int64(ctx(), m_ast, &result);
if (state != Z3_TRUE)
if (!is_numeral_i64(result)) {
throw exception("numeral does not fit in machine __int64");
}
return result;
}
@ -705,9 +704,9 @@ namespace z3 {
__uint64 get_numeral_uint64() const {
assert(is_numeral());
__uint64 result;
Z3_bool state = Z3_get_numeral_uint64(ctx(), m_ast, &result);
if (state != Z3_TRUE)
if (!is_numeral_u64(result)) {
throw exception("numeral does not fit in machine __uint64");
}
return result;
}

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

@ -4162,15 +4162,6 @@ def Select(a, i):
_z3_assert(is_array(a), "First argument must be a Z3 array expression")
return a[i]
def Default(a):
""" Return a default value for array expression.
>>> b = K(IntSort(), 1)
>>> prove(Default(b) == 1)
proved
"""
if __debug__:
_z3_assert(is_array(a), "First argument must be a Z3 array expression")
return a.mk_default()
def Map(f, *args):
"""Return a Z3 map array expression.

53
src/ast/rewriter/label_rewriter.cpp Normal file
View file

@ -0,0 +1,53 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
label_rewriter.cpp
Abstract:
Basic rewriting rules for removing labels.
Author:
Nikolaj Bjorner (nbjorner) 2015-19-10
Notes:
--*/
#include"rewriter.h"
#include"rewriter_def.h"
#include"label_rewriter.h"
label_rewriter::label_rewriter(ast_manager & m) :
m_label_fid(m.get_label_family_id()),
m_rwr(m, false, *this) {}
label_rewriter::~label_rewriter() {}
br_status label_rewriter::reduce_app(
func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr) {
if (is_decl_of(f, m_label_fid, OP_LABEL)) {
SASSERT(num == 1);
result = args[0];
return BR_DONE;
}
return BR_FAILED;
}
void label_rewriter::remove_labels(expr_ref& fml, proof_ref& pr) {
ast_manager& m = fml.get_manager();
expr_ref tmp(m);
m_rwr(fml, tmp);
if (pr && fml != tmp) {
pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp));
}
fml = tmp;
}
//template class rewriter_tpl<label_rewriter>;

41
src/ast/rewriter/label_rewriter.h Normal file
View file

@ -0,0 +1,41 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
label_rewriter.h
Abstract:
Basic rewriting rules for labels.
Author:
Nikolaj Bjorner (nbjorner) 2015-19-10
Notes:
--*/
#ifndef LABEL_REWRITER_H_
#define LABEL_REWRITER_H_
#include"ast.h"
#include"rewriter_types.h"
class label_rewriter : public default_rewriter_cfg {
family_id m_label_fid;
rewriter_tpl<label_rewriter> m_rwr;
public:
label_rewriter(ast_manager & m);
~label_rewriter();
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr);
void remove_labels(expr_ref& fml, proof_ref& pr);
};
#endif

26
src/muz/base/dl_rule.cpp
View file

@ -55,8 +55,7 @@ namespace datalog {
m_args(m),
m_hnf(m),
m_qe(m),
m_cfg(m),
m_rwr(m, false, m_cfg),
m_rwr(m),
m_ufproc(m) {}
void rule_manager::inc_ref(rule * r) {
@ -76,28 +75,8 @@ namespace datalog {
}
}
rule_manager::remove_label_cfg::~remove_label_cfg() {}
br_status rule_manager::remove_label_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr)
{
if (is_decl_of(f, m_label_fid, OP_LABEL)) {
SASSERT(num == 1);
result = args[0];
return BR_DONE;
}
return BR_FAILED;
}
void rule_manager::remove_labels(expr_ref& fml, proof_ref& pr) {
expr_ref tmp(m);
m_rwr(fml, tmp);
if (pr && fml != tmp) {
pr = m.mk_modus_ponens(pr, m.mk_rewrite(fml, tmp));
}
fml = tmp;
m_rwr.remove_labels(fml, pr);
}
var_idx_set& rule_manager::collect_vars(expr* e) {
@ -1092,5 +1071,4 @@ namespace datalog {
};
template class rewriter_tpl<datalog::rule_manager::remove_label_cfg>;

14
src/muz/base/dl_rule.h
View file

@ -32,6 +32,7 @@ Revision History:
#include"qe_lite.h"
#include"var_subst.h"
#include"datatype_decl_plugin.h"
#include"label_rewriter.h"
namespace datalog {
@ -102,16 +103,6 @@ namespace datalog {
*/
class rule_manager
{
class remove_label_cfg : public default_rewriter_cfg {
family_id m_label_fid;
public:
remove_label_cfg(ast_manager& m): m_label_fid(m.get_label_family_id()) {}
virtual ~remove_label_cfg();
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result,
proof_ref & result_pr);
};
ast_manager& m;
context& m_ctx;
rule_counter m_counter;
@ -124,8 +115,7 @@ namespace datalog {
svector<bool> m_neg;
hnf m_hnf;
qe_lite m_qe;
remove_label_cfg m_cfg;
rewriter_tpl<remove_label_cfg> m_rwr;
label_rewriter m_rwr;
mutable uninterpreted_function_finder_proc m_ufproc;
mutable quantifier_finder_proc m_qproc;
mutable expr_sparse_mark m_visited;

30
src/nlsat/nlsat_evaluator.cpp
View file

@ -18,10 +18,12 @@ Revision History:
--*/
#include"nlsat_evaluator.h"
#include"nlsat_solver.h"
namespace nlsat {
struct evaluator::imp {
solver& m_solver;
assignment const & m_assignment;
pmanager & m_pm;
small_object_allocator & m_allocator;
@ -357,7 +359,8 @@ namespace nlsat {
sign_table m_sign_table_tmp;
imp(assignment const & x2v, pmanager & pm, small_object_allocator & allocator):
imp(solver& s, assignment const & x2v, pmanager & pm, small_object_allocator & allocator):
m_solver(s),
m_assignment(x2v),
m_pm(pm),
m_allocator(allocator),
@ -420,10 +423,25 @@ namespace nlsat {
scoped_anum_vector & roots = m_tmp_values;
roots.reset();
m_am.isolate_roots(polynomial_ref(a->p(), m_pm), undef_var_assignment(m_assignment, a->x()), roots);
TRACE("nlsat",
m_solver.display(tout << (neg?"!":""), *a); tout << "\n";
if (roots.empty()) {
tout << "No roots\n";
}
else {
tout << "Roots for ";
for (unsigned i = 0; i < roots.size(); ++i) {
m_am.display_interval(tout, roots[i]); tout << " ";
}
tout << "\n";
}
m_assignment.display(tout);
);
SASSERT(a->i() > 0);
if (a->i() > roots.size())
return false; // p does have sufficient roots
int sign = m_am.compare(m_assignment.value(a->x()), roots[a->i() - 1]);
if (a->i() > roots.size()) {
return neg;
}
int sign = m_am.compare(m_assignment.value(a->x()), roots[a->i() - 1]);
return satisfied(sign, k, neg);
}
@ -649,8 +667,8 @@ namespace nlsat {
}
};
evaluator::evaluator(assignment const & x2v, pmanager & pm, small_object_allocator & allocator) {
m_imp = alloc(imp, x2v, pm, allocator);
evaluator::evaluator(solver& s, assignment const & x2v, pmanager & pm, small_object_allocator & allocator) {
m_imp = alloc(imp, s, x2v, pm, allocator);
}
evaluator::~evaluator() {

4
src/nlsat/nlsat_evaluator.h
View file

@ -26,11 +26,13 @@ Revision History:
namespace nlsat {
class solver;
class evaluator {
struct imp;
imp * m_imp;
public:
evaluator(assignment const & x2v, pmanager & pm, small_object_allocator & allocator);
evaluator(solver& s, assignment const & x2v, pmanager & pm, small_object_allocator & allocator);
~evaluator();
interval_set_manager & ism() const;

530
src/nlsat/nlsat_explain.cpp
View file

@ -36,6 +36,7 @@ namespace nlsat {
polynomial::cache & m_cache;
pmanager & m_pm;
polynomial_ref_vector m_ps;
polynomial_ref_vector m_ps2;
polynomial_ref_vector m_psc_tmp;
polynomial_ref_vector m_factors;
scoped_anum_vector m_roots_tmp;
@ -43,6 +44,7 @@ namespace nlsat {
bool m_full_dimensional;
bool m_minimize_cores;
bool m_factor;
bool m_signed_project;
struct todo_set {
polynomial::cache & m_cache;
@ -137,6 +139,7 @@ namespace nlsat {
m_cache(u),
m_pm(u.pm()),
m_ps(m_pm),
m_ps2(m_pm),
m_psc_tmp(m_pm),
m_factors(m_pm),
m_roots_tmp(m_am),
@ -148,6 +151,7 @@ namespace nlsat {
m_simplify_cores = false;
m_full_dimensional = false;
m_minimize_cores = false;
m_signed_project = false;
}
~imp() {
@ -202,7 +206,7 @@ namespace nlsat {
void reset_already_added() {
SASSERT(m_result != 0);
unsigned sz = m_result->size();
for (unsigned i = 0; i < sz; i++)
for (unsigned i = 0; i < sz; i++)
m_already_added_literal[(*m_result)[i].index()] = false;
}
@ -212,7 +216,7 @@ namespace nlsat {
max_var(p) must be assigned in the current interpretation.
*/
int sign(polynomial_ref const & p) {
TRACE("nlsat_explain", tout << "p: " << p << "\n";);
TRACE("nlsat_explain", tout << "p: " << p << " var: " << max_var(p) << "\n";);
SASSERT(max_var(p) == null_var || m_assignment.is_assigned(max_var(p)));
return m_am.eval_sign_at(p, m_assignment);
}
@ -697,39 +701,163 @@ namespace nlsat {
}
}
void test_root_literal(atom::kind k, var y, unsigned i, poly * p, scoped_literal_vector& result) {
m_result = &result;
add_root_literal(k, y, i, p);
reset_already_added();
m_result = 0;
}
void add_root_literal(atom::kind k, var y, unsigned i, poly * p) {
polynomial_ref pr(p, m_pm);
TRACE("nlsat_explain",
display(tout << "x" << y << " " << k << "[" << i << "](", pr); tout << ")\n";);
if (!mk_linear_root(k, y, i, p) &&
//!mk_plinear_root(k, y, i, p) &&
!mk_quadratic_root(k, y, i, p)&&
true) {
bool_var b = m_solver.mk_root_atom(k, y, i, p);
literal l(b, true);
TRACE("nlsat_explain", tout << "adding literal\n"; display(tout, l); tout << "\n";);
add_literal(l);
}
}
/**
* literal can be expressed using a linear ineq_atom
*/
bool mk_linear_root(atom::kind k, var y, unsigned i, poly * p) {
scoped_mpz c(m_pm.m());
bool_var b;
bool lsign = false;
if (m_pm.degree(p, y) == 1 && m_pm.const_coeff(p, y, 1, c)) {
SASSERT(!m_pm.m().is_zero(c));
// literal can be expressed using a linear ineq_atom
polynomial_ref p_prime(m_pm);
p_prime = p;
if (m_pm.m().is_neg(c))
p_prime = neg(p_prime);
p = p_prime.get();
switch (k) {
case atom::ROOT_EQ: k = atom::EQ; lsign = false; break;
case atom::ROOT_LT: k = atom::LT; lsign = false; break;
case atom::ROOT_GT: k = atom::GT; lsign = false; break;
case atom::ROOT_LE: k = atom::GT; lsign = true; break;
case atom::ROOT_GE: k = atom::LT; lsign = true; break;
default:
UNREACHABLE();
break;
}
bool is_even = false;
b = m_solver.mk_ineq_atom(k, 1, &p, &is_even);
mk_linear_root(k, y, i, p, m_pm.m().is_neg(c));
return true;
}
else {
b = m_solver.mk_root_atom(k, y, i, p);
lsign = false;
return false;
}
/**
Create pseudo-linear root depending on the sign of the coefficient to y.
*/
bool mk_plinear_root(atom::kind k, var y, unsigned i, poly * p) {
if (m_pm.degree(p, y) != 1) {
return false;
}
lsign = !lsign; // adding as an assumption
literal l(b, lsign);
TRACE("nlsat_explain", tout << "adding literal\n"; display(tout, l); tout << "\n";);
add_literal(l);
polynomial_ref c(m_pm);
c = m_pm.coeff(p, y, 1);
int s = sign(c);
if (s == 0) {
return false;
}
ensure_sign(c);
mk_linear_root(k, y, i, p, s < 0);
return true;
}
/**
Encode root conditions for quadratic polynomials.
Basically implements Thom's theorem. The roots are characterized by the sign of polynomials and their derivatives.
b^2 - 4ac = 0:
- there is only one root, which is -b/2a.
- relation to root is a function of the sign of
- 2ax + b
b^2 - 4ac > 0:
- assert i == 1 or i == 2
- relation to root is a function of the signs of:
- 2ax + b
- ax^2 + bx + c
*/
bool mk_quadratic_root(atom::kind k, var y, unsigned i, poly * p) {
if (m_pm.degree(p, y) != 2) {
return false;
}
if (i != 1 && i != 2) {
return false;
}
SASSERT(m_assignment.is_assigned(y));
polynomial_ref A(m_pm), B(m_pm), C(m_pm), q(m_pm), p_diff(m_pm), yy(m_pm);
A = m_pm.coeff(p, y, 2);
B = m_pm.coeff(p, y, 1);
C = m_pm.coeff(p, y, 0);
// TBD throttle based on degree of q?
q = (B*B) - (4*A*C);
yy = m_pm.mk_polynomial(y);
p_diff = 2*A*yy + B;
p_diff = m_pm.normalize(p_diff);
int sq = ensure_sign(q);
if (sq < 0) {
return false;
}
int sa = ensure_sign(A);
if (sa == 0) {
q = B*yy + C;
return mk_plinear_root(k, y, i, q);
}
ensure_sign(p_diff);
if (sq > 0) {
polynomial_ref pr(p, m_pm);
ensure_sign(pr);
}
return true;
}
int ensure_sign(polynomial_ref & p) {
#if 0
polynomial_ref f(m_pm);
factor(p, m_factors);
m_is_even.reset();
unsigned num_factors = m_factors.size();
int s = 1;
for (unsigned i = 0; i < num_factors; i++) {
f = m_factors.get(i);
s *= sign(f);
m_is_even.push_back(false);
}
if (num_factors > 0) {
atom::kind k = atom::EQ;
if (s == 0) k = atom::EQ;
if (s < 0) k = atom::LT;
if (s > 0) k = atom::GT;
bool_var b = m_solver.mk_ineq_atom(k, num_factors, m_factors.c_ptr(), m_is_even.c_ptr());
add_literal(literal(b, true));
}
return s;
#else
int s = sign(p);
if (!is_const(p)) {
add_simple_assumption(s == 0 ? atom::EQ : (s < 0 ? atom::LT : atom::GT), p);
}
return s;
#endif
}
/**
Auxiliary function to linear roots.
*/
void mk_linear_root(atom::kind k, var y, unsigned i, poly * p, bool mk_neg) {
polynomial_ref p_prime(m_pm);
p_prime = p;
bool lsign = false;
if (mk_neg)
p_prime = neg(p_prime);
p = p_prime.get();
switch (k) {
case atom::ROOT_EQ: k = atom::EQ; lsign = false; break;
case atom::ROOT_LT: k = atom::LT; lsign = false; break;
case atom::ROOT_GT: k = atom::GT; lsign = false; break;
case atom::ROOT_LE: k = atom::GT; lsign = true; break;
case atom::ROOT_GE: k = atom::LT; lsign = true; break;
default:
UNREACHABLE();
break;
}
add_simple_assumption(k, p, lsign);
}
/**
@ -1332,10 +1460,333 @@ namespace nlsat {
TRACE("nlsat_explain", tout << "[explain] result\n"; display(tout, result););
CASSERT("nlsat", check_already_added());
}
void project(var x, unsigned num, literal const * ls, scoped_literal_vector & result) {
m_result = &result;
svector<literal> lits;
TRACE("nlsat", tout << "project x" << x << "\n"; m_solver.display(tout););
DEBUG_CODE(
for (unsigned i = 0; i < num; ++i) {
SASSERT(m_solver.value(ls[i]) == l_true);
atom* a = m_atoms[ls[i].var()];
SASSERT(!a || m_evaluator.eval(a, ls[i].sign()));
});
split_literals(x, num, ls, lits);
collect_polys(lits.size(), lits.c_ptr(), m_ps);
var mx_var = max_var(m_ps);
if (!m_ps.empty()) {
svector<var> renaming;
if (x != mx_var) {
for (var i = 0; i < m_solver.num_vars(); ++i) {
renaming.push_back(i);
}
std::swap(renaming[x], renaming[mx_var]);
m_solver.reorder(renaming.size(), renaming.c_ptr());
TRACE("qe", tout << "x: " << x << " max: " << mx_var << " num_vars: " << m_solver.num_vars() << "\n";
m_solver.display(tout););
}
elim_vanishing(m_ps);
if (m_signed_project) {
signed_project(m_ps, mx_var);
}
else {
project(m_ps, mx_var);
}
reset_already_added();
m_result = 0;
if (x != mx_var) {
m_solver.restore_order();
}
}
else {
reset_already_added();
m_result = 0;
}
for (unsigned i = 0; i < result.size(); ++i) {
result.set(i, ~result[i]);
}
DEBUG_CODE(
for (unsigned i = 0; i < result.size(); ++i) {
SASSERT(l_true == m_solver.value(result[i]));
});
}
void split_literals(var x, unsigned n, literal const* ls, svector<literal>& lits) {
var_vector vs;
for (unsigned i = 0; i < n; ++i) {
vs.reset();
m_solver.vars(ls[i], vs);
if (vs.contains(x)) {
lits.push_back(ls[i]);
}
else {
add_literal(~ls[i]);
}
}
}
/**
Signed projection.
Assumptions:
- any variable in ps is at most x.
- root expressions are satisfied (positive literals)
Effect:
- if x not in p, then
- if sign(p) < 0: p < 0
- if sign(p) = 0: p = 0
- if sign(p) > 0: p > 0
else:
- let roots_j be the roots of p_j or roots_j[i]
- let L = { roots_j[i] | M(roots_j[i]) < M(x) }
- let U = { roots_j[i] | M(roots_j[i]) > M(x) }
- let E = { roots_j[i] | M(roots_j[i]) = M(x) }
- let glb in L, s.t. forall l in L . M(glb) >= M(l)
- let lub in U, s.t. forall u in U . M(lub) <= M(u)
- if root in E, then
- add E x . x = root & x > lb for lb in L
- add E x . x = root & x < ub for ub in U
- add E x . x = root & x = root2 for root2 in E \ { root }
- else
- assume |L| <= |U| (other case is symmetric)
- add E x . lb <= x & x <= glb for lb in L
- add E x . x = glb & x < ub for ub in U
*/
void signed_project(polynomial_ref_vector& ps, var x) {
TRACE("nlsat_explain", tout << "Signed projection\n";);
polynomial_ref p(m_pm);
unsigned eq_index = 0;
bool eq_valid = false;
unsigned eq_degree = 0;
for (unsigned i = 0; i < ps.size(); ++i) {
p = ps.get(i);
int s = sign(p);
if (max_var(p) != x) {
atom::kind k = (s == 0)?(atom::EQ):((s < 0)?(atom::LT):(atom::GT));
add_simple_assumption(k, p, false);
ps[i] = ps.back();
ps.pop_back();
--i;
}
else if (s == 0) {
if (!eq_valid || degree(p, x) < eq_degree) {
eq_index = i;
eq_valid = true;
eq_degree = degree(p, x);
}
}
}
if (ps.empty()) {
return;
}
if (ps.size() == 1) {
project_single(x, ps.get(0));
return;
}
// ax + b = 0, p(x) > 0 ->
if (eq_valid) {
p = ps.get(eq_index);
if (degree(p, x) == 1) {
// ax + b = 0
// let d be maximal degree of x in p.
// p(x) -> a^d*p(-b/a), a
// perform virtual substitution with equality.
solve_eq(x, eq_index, ps);
}
else {
project_pairs(x, eq_index, ps);
}
return;
}
unsigned num_lub = 0, num_glb = 0;
unsigned glb_index = 0, lub_index = 0;
scoped_anum lub(m_am), glb(m_am), x_val(m_am);
x_val = m_assignment.value(x);
for (unsigned i = 0; i < ps.size(); ++i) {
p = ps.get(i);
scoped_anum_vector & roots = m_roots_tmp;
roots.reset();
m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
bool glb_valid = false, lub_valid = false;
for (unsigned j = 0; j < roots.size(); ++j) {
int s = m_am.compare(x_val, roots[j]);
SASSERT(s != 0);
lub_valid |= s < 0;
glb_valid |= s > 0;
if (s < 0 && m_am.lt(roots[j], lub)) {
lub_index = i;
m_am.set(lub, roots[j]);
}
if (s > 0 && m_am.lt(glb, roots[j])) {
glb_index = i;
m_am.set(glb, roots[j]);
}
}
if (glb_valid) {
++num_glb;
}
if (lub_valid) {
++num_lub;
}
}
if (num_lub == 0) {
project_plus_infinity(x, ps);
return;
}
if (num_glb == 0) {
project_minus_infinity(x, ps);
return;
}
if (num_lub <= num_glb) {
glb_index = lub_index;
}
project_pairs(x, glb_index, ps);
}
void project_plus_infinity(var x, polynomial_ref_vector const& ps) {
polynomial_ref p(m_pm), lc(m_pm);
for (unsigned i = 0; i < ps.size(); ++i) {
p = ps.get(i);
unsigned d = degree(p, x);
lc = m_pm.coeff(p, x, d);
if (!is_const(lc)) {
unsigned s = sign(p);
SASSERT(s != 0);
atom::kind k = (s > 0)?(atom::GT):(atom::LT);
add_simple_assumption(k, lc);
}
}
}
void project_minus_infinity(var x, polynomial_ref_vector const& ps) {
polynomial_ref p(m_pm), lc(m_pm);
for (unsigned i = 0; i < ps.size(); ++i) {
p = ps.get(i);
unsigned d = degree(p, x);
lc = m_pm.coeff(p, x, d);
if (!is_const(lc)) {
unsigned s = sign(p);
SASSERT(s != 0);
atom::kind k;
if (s > 0) {
k = (d % 2 == 0)?(atom::GT):(atom::LT);
}
else {
k = (d % 2 == 0)?(atom::LT):(atom::GT);
}
add_simple_assumption(k, lc);
}
}
}
void project_pairs(var x, unsigned idx, polynomial_ref_vector const& ps) {
polynomial_ref p(m_pm);
p = ps.get(idx);
for (unsigned i = 0; i < ps.size(); ++i) {
if (i != idx) {
project_pair(x, ps.get(i), p);
}
}
}
void project_pair(var x, polynomial::polynomial* p1, polynomial::polynomial* p2) {
m_ps2.reset();
m_ps2.push_back(p1);
m_ps2.push_back(p2);
project(m_ps2, x);
}
void project_single(var x, polynomial::polynomial* p) {
m_ps2.reset();
m_ps2.push_back(p);
project(m_ps2, x);
}
void solve_eq(var x, unsigned idx, polynomial_ref_vector const& ps) {
polynomial_ref p(m_pm), A(m_pm), B(m_pm), C(m_pm), D(m_pm), E(m_pm), q(m_pm), r(m_pm);
polynomial_ref_vector qs(m_pm);
p = ps.get(idx);
SASSERT(degree(p, x) == 1);
A = m_pm.coeff(p, x, 1);
B = m_pm.coeff(p, x, 0);
B = neg(B);
TRACE("nlsat_explain", tout << "p: " << p << " A: " << A << " B: " << B << "\n";);
// x = B/A
for (unsigned i = 0; i < ps.size(); ++i) {
if (i != idx) {
q = ps.get(i);
unsigned d = degree(q, x);
D = m_pm.mk_const(rational(1));
E = D;
r = m_pm.mk_zero();
for (unsigned j = 0; j <= d; ++j) {
qs.push_back(D);
D = D*A;
}
for (unsigned j = 0; j <= d; ++j) {
// A^d*p0 + A^{d-1}*B*p1 + ... + B^j*A^{d-j}*pj + ... + B^d*p_d
C = m_pm.coeff(q, x, j);
if (!is_zero(C)) {
D = qs.get(d-j);
r = r + D*E*C;
}
E = E*B;
}
TRACE("nlsat_explain", tout << "q: " << q << " r: " << r << "\n";);
ensure_sign(r);
}
else {
ensure_sign(A);
}
}
}
void maximize(var x, unsigned num, literal const * ls, scoped_anum& val, bool& unbounded) {
svector<literal> lits;
polynomial_ref p(m_pm);
split_literals(x, num, ls, lits);
collect_polys(lits.size(), lits.c_ptr(), m_ps);
unbounded = true;
scoped_anum x_val(m_am);
x_val = m_assignment.value(x);
for (unsigned i = 0; i < m_ps.size(); ++i) {
p = m_ps.get(i);
scoped_anum_vector & roots = m_roots_tmp;
roots.reset();
m_am.isolate_roots(p, undef_var_assignment(m_assignment, x), roots);
for (unsigned j = 0; j < roots.size(); ++j) {
int s = m_am.compare(x_val, roots[j]);
if (s <= 0 && (unbounded || m_am.compare(roots[j], val) <= 0)) {
unbounded = false;
val = roots[j];
}
}
}
}
};
explain::explain(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,
evaluator & ev) {
explain::explain(solver & s, assignment const & x2v, polynomial::cache & u,
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev) {
m_imp = alloc(imp, s, x2v, u, atoms, x2eq, ev);
}
@ -1364,10 +1815,26 @@ namespace nlsat {
m_imp->m_factor = f;
}
void explain::set_signed_project(bool f) {
m_imp->m_signed_project = f;
}
void explain::operator()(unsigned n, literal const * ls, scoped_literal_vector & result) {
(*m_imp)(n, ls, result);
}
void explain::project(var x, unsigned n, literal const * ls, scoped_literal_vector & result) {
m_imp->project(x, n, ls, result);
}
void explain::maximize(var x, unsigned n, literal const * ls, scoped_anum& val, bool& unbounded) {
m_imp->maximize(x, n, ls, val, unbounded);
}
void explain::test_root_literal(atom::kind k, var y, unsigned i, poly* p, scoped_literal_vector & result) {
m_imp->test_root_literal(k, y, i, p, result);
}
};
#ifdef Z3DEBUG
@ -1398,3 +1865,4 @@ void pp_lit(nlsat::explain::imp & ex, nlsat::literal l) {
std::cout << std::endl;
}
#endif

49
src/nlsat/nlsat_explain.h
View file

@ -22,9 +22,11 @@ Revision History:
#include"nlsat_solver.h"
#include"nlsat_scoped_literal_vector.h"
#include"polynomial_cache.h"
#include"algebraic_numbers.h"
namespace nlsat {
class evaluator;
class explain {
public:
@ -32,8 +34,8 @@ namespace nlsat {
private:
imp * m_imp;
public:
explain(solver & s, assignment const & x2v, polynomial::cache & u, atom_vector const & atoms, atom_vector const & x2eq,
evaluator & ev);
explain(solver & s, assignment const & x2v, polynomial::cache & u,
atom_vector const& atoms, atom_vector const& x2eq, evaluator & ev);
~explain();
void reset();
@ -41,6 +43,7 @@ namespace nlsat {
void set_full_dimensional(bool f);
void set_minimize_cores(bool f);
void set_factor(bool f);
void set_signed_project(bool f);
/**
\brief Given a set of literals ls[0], ... ls[n-1] s.t.
@ -60,6 +63,48 @@ namespace nlsat {
- s_1, ..., s_m are false in the current interpretation
*/
void operator()(unsigned n, literal const * ls, scoped_literal_vector & result);
/**
\brief projection for a given variable.
Given: M |= l1[x] /\ ... /\ ln[x]
Find: M |= s1, ..., sm
Such that: |= ~s1 \/ ... \/ ~sm \/ E x. l1[x] /\ ... /\ ln[x]
Contrast this with with the core-based projection above:
Given: M |= A x . l1[x] \/ ... \/ ln[x]
Find: M |= ~s1, ..., ~sm.
Such that: |= s1 \/ ... \/ sm \/ A x . l1[x] \/ ... \/ ln[x]
Claim: the two compute the same solutions if the projection operators are independent of the value of x.
Claim: A complete, convergent projection operator can be obtained from M in a way that is independent of x.
*/
void project(var x, unsigned n, literal const * ls, scoped_literal_vector & result);
/**
Maximize the value of x (locally) under the current assignment to other variables and
while maintaining the assignment to the literals ls.
Set unbounded to 'true' if the value of x is unbounded.
Precondition: the set of literals are true in the current model.
By local optimization we understand that x is increased to the largest value within
the signs delineated by the roots of the polynomials in ls.
*/
void maximize(var x, unsigned n, literal const * ls, scoped_anum& val, bool& unbounded);
/**
Unit test routine.
*/
void test_root_literal(atom::kind k, var y, unsigned i, poly* p, scoped_literal_vector & result);
};
};

297
src/nlsat/nlsat_solver.cpp
View file

@ -66,7 +66,6 @@ namespace nlsat {
typedef polynomial::cache cache;
typedef ptr_vector<interval_set> interval_set_vector;
solver & m_solver;
reslimit& m_rlimit;
small_object_allocator m_allocator;
unsynch_mpq_manager m_qm;
@ -159,8 +158,7 @@ namespace nlsat {
unsigned m_stages;
unsigned m_irrational_assignments; // number of irrational witnesses
imp(solver & s, reslimit& rlim, params_ref const & p):
m_solver(s),
imp(solver& s, reslimit& rlim, params_ref const & p):
m_rlimit(rlim),
m_allocator("nlsat"),
m_pm(rlim, m_qm, &m_allocator),
@ -168,7 +166,7 @@ namespace nlsat {
m_am(rlim, m_qm, p, &m_allocator),
m_asm(*this, m_allocator),
m_assignment(m_am),
m_evaluator(m_assignment, m_pm, m_allocator),
m_evaluator(s, m_assignment, m_pm, m_allocator),
m_ism(m_evaluator.ism()),
m_num_bool_vars(0),
m_display_var(m_perm),
@ -183,12 +181,7 @@ namespace nlsat {
}
~imp() {
m_explain.reset();
m_lemma.reset();
m_lazy_clause.reset();
undo_until_size(0);
del_clauses();
del_unref_atoms();
reset();
}
void mk_true_bvar() {
@ -216,6 +209,18 @@ namespace nlsat {
m_am.updt_params(p.p);
}
void reset() {
m_explain.reset();
m_lemma.reset();
m_lazy_clause.reset();
undo_until_size(0);
del_clauses();
del_unref_atoms();
m_cache.reset();
m_assignment.reset();
}
void checkpoint() {
if (!m_rlimit.inc()) throw solver_exception(m_rlimit.get_cancel_msg());
if (memory::get_allocation_size() > m_max_memory) throw solver_exception(Z3_MAX_MEMORY_MSG);
@ -252,6 +257,7 @@ namespace nlsat {
}
void inc_ref(bool_var b) {
TRACE("ref", tout << "inc: " << b << "\n";);
if (b == null_bool_var)
return;
if (m_atoms[b] == 0)
@ -264,6 +270,7 @@ namespace nlsat {
}
void dec_ref(bool_var b) {
TRACE("ref", tout << "dec: " << b << "\n";);
if (b == null_bool_var)
return;
atom * a = m_atoms[b];
@ -412,6 +419,34 @@ namespace nlsat {
return x;
}
svector<bool> m_found_vars;
void vars(literal l, var_vector& vs) {
vs.reset();
atom * a = m_atoms[l.var()];
if (a == 0) {
}
else if (a->is_ineq_atom()) {
unsigned sz = to_ineq_atom(a)->size();
var_vector new_vs;
for (unsigned j = 0; j < sz; j++) {
m_found_vars.reset();
m_pm.vars(to_ineq_atom(a)->p(j), new_vs);
for (unsigned i = 0; i < new_vs.size(); ++i) {
if (!m_found_vars.get(new_vs[i], false)) {
m_found_vars.setx(new_vs[i], true, false);
vs.push_back(new_vs[i]);
}
}
}
}
else {
m_pm.vars(to_root_atom(a)->p(), vs);
//vs.erase(max_var(to_root_atom(a)->p()));
vs.push_back(to_root_atom(a)->x());
}
}
void deallocate(ineq_atom * a) {
unsigned obj_sz = ineq_atom::get_obj_size(a->size());
a->~ineq_atom();
@ -491,6 +526,7 @@ namespace nlsat {
TRACE("nlsat_table_bug", ineq_atom::hash_proc h;
tout << "mk_ineq_atom hash: " << h(new_atom) << "\n"; display(tout, *new_atom, m_display_var); tout << "\n";);
ineq_atom * old_atom = m_ineq_atoms.insert_if_not_there(new_atom);
CTRACE("nlsat_table_bug", old_atom->max_var() != max, display(tout, *old_atom, m_display_var); tout << "\n";);
SASSERT(old_atom->max_var() == max);
if (old_atom != new_atom) {
deallocate(new_atom);
@ -726,7 +762,7 @@ namespace nlsat {
template<typename Predicate>
void undo_until(Predicate const & pred) {
while (pred()) {
while (pred() && !m_trail.empty()) {
trail & t = m_trail.back();
switch (t.m_kind) {
case trail::BVAR_ASSIGNMENT:
@ -803,6 +839,14 @@ namespace nlsat {
SASSERT(m_bvalues[b] == l_undef);
}
struct true_pred {
bool operator()() const { return true; }
};
void undo_until_empty() {
undo_until(true_pred());
}
/**
\brief Create a new scope level
*/
@ -868,10 +912,11 @@ namespace nlsat {
var max = a->max_var();
if (!m_assignment.is_assigned(max))
return l_undef;
TRACE("value_bug", tout << "value of: "; display(tout, l); tout << "\n"; tout << "xk: " << m_xk << ", a->max_var(): " << a->max_var() << "\n";
display_assignment(tout);
display_bool_assignment(tout););
return to_lbool(m_evaluator.eval(a, l.sign()));
val = to_lbool(m_evaluator.eval(a, l.sign()));
TRACE("value_bug", tout << "value of: "; display(tout, l); tout << " := " << val << "\n";
tout << "xk: " << m_xk << ", a->max_var(): " << a->max_var() << "\n";
display_assignment(tout););
return val;
}
/**
@ -880,8 +925,10 @@ namespace nlsat {
bool is_satisfied(clause const & cls) const {
unsigned sz = cls.size();
for (unsigned i = 0; i < sz; i++) {
if (const_cast<imp*>(this)->value(cls[i]) == l_true)
if (const_cast<imp*>(this)->value(cls[i]) == l_true) {
TRACE("value_bug:", tout << cls[i] << " := true\n";);
return true;
}
}
return false;
}
@ -984,8 +1031,10 @@ namespace nlsat {
If satisfy_learned is true, then learned clauses are satisfied even if m_lazy > 0
*/
bool process_arith_clause(clause const & cls, bool satisfy_learned) {
if (!satisfy_learned && m_lazy >= 2 && cls.is_learned())
if (!satisfy_learned && m_lazy >= 2 && cls.is_learned()) {
TRACE("nlsat", tout << "skip learned\n";);
return true; // ignore lemmas in super lazy mode
}
SASSERT(m_xk == max_var(cls));
unsigned num_undef = 0; // number of undefined literals
unsigned first_undef = UINT_MAX; // position of the first undefined literal
@ -1064,7 +1113,7 @@ namespace nlsat {
If satisfy_learned is true, then (arithmetic) learned clauses are satisfied even if m_lazy > 0
*/
bool process_clause(clause const & cls, bool satisfy_learned) {
TRACE("nlsat", tout << "processing clause:\n"; display(tout, cls); tout << "\n";);
TRACE("nlsat", tout << "processing clause: "; display(tout, cls); tout << "\n";);
if (is_satisfied(cls))
return true;
if (m_xk == null_var)
@ -1151,7 +1200,7 @@ namespace nlsat {
}
TRACE("nlsat_bug", tout << "xk: x" << m_xk << " bk: b" << m_bk << "\n";);
if (m_bk == null_bool_var && m_xk >= num_vars()) {
TRACE("nlsat", tout << "found model\n"; display_assignment(tout); display_bool_assignment(tout););
TRACE("nlsat", tout << "found model\n"; display_assignment(tout););
return l_true; // all variables were assigned, and all clauses were satisfied.
}
TRACE("nlsat", tout << "processing variable ";
@ -1186,23 +1235,102 @@ namespace nlsat {
lbool check() {
TRACE("nlsat_smt2", display_smt2(tout););
TRACE("nlsat_fd", tout << "is_full_dimensional: " << is_full_dimensional() << "\n";);
m_xk = null_var;
init_search();
m_explain.set_full_dimensional(is_full_dimensional());
if (m_random_order) {
bool reordered = false;
if (!can_reorder()) {
}
else if (m_random_order) {
shuffle_vars();
reordered = true;
}
else if (m_reorder) {
heuristic_reorder();
reordered = true;
}
sort_watched_clauses();
lbool r = search();
CTRACE("nlsat_model", r == l_true, tout << "model before restore order\n"; display_assignment(tout); display_bool_assignment(tout););
if (m_reorder)
CTRACE("nlsat_model", r == l_true, tout << "model before restore order\n"; display_assignment(tout););
if (reordered)
restore_order();
CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout); display_bool_assignment(tout););
CTRACE("nlsat_model", r == l_true, tout << "model\n"; display_assignment(tout););
CTRACE("nlsat", r == l_false, display(tout););
return r;
}
void init_search() {
undo_until_empty();
while (m_scope_lvl > 0) {
undo_new_level();
}
m_xk = null_var;
for (unsigned i = 0; i < m_bvalues.size(); ++i) {
m_bvalues[i] = l_undef;
}
m_assignment.reset();
}
lbool check(literal_vector& assumptions) {
literal_vector result;
unsigned sz = assumptions.size();
literal const* ptr = assumptions.c_ptr();
for (unsigned i = 0; i < sz; ++i) {
mk_clause(1, ptr+i, (assumption)(ptr+i));
}
lbool r = check();
if (r == l_false) {
// collect used literals from m_lemma_assumptions
vector<assumption, false> deps;
m_asm.linearize(m_lemma_assumptions.get(), deps);
for (unsigned i = 0; i < deps.size(); ++i) {
literal const* lp = (literal const*)(deps[i]);
if (ptr <= lp && lp < ptr + sz) {
result.push_back(*lp);
}
}
}
collect(assumptions, m_clauses);
collect(assumptions, m_learned);
assumptions.reset();
assumptions.append(result);
return r;
}
void collect(literal_vector const& assumptions, clause_vector& clauses) {
unsigned n = clauses.size();
unsigned j = 0;
for (unsigned i = 0; i < n; i++) {
clause * c = clauses[i];
if (collect(assumptions, *c)) {
del_clause(c);
}
else {
clauses[j] = c;
j++;
}
}
clauses.shrink(j);
}
bool collect(literal_vector const& assumptions, clause const& c) {
unsigned sz = assumptions.size();
literal const* ptr = assumptions.c_ptr();
_assumption_set asms = static_cast<_assumption_set>(c.assumptions());
if (asms == 0) {
return false;
}
vector<assumption, false> deps;
m_asm.linearize(asms, deps);
bool found = false;
for (unsigned i = 0; !found && i < deps.size(); ++i) {
found = ptr <= deps[i] && deps[i] < ptr + sz;
}
return found;
}
// -----------------------
//
// Conflict Resolution
@ -1447,7 +1575,7 @@ namespace nlsat {
TRACE("nlsat", tout << "resolve, conflicting clause:\n"; display(tout, *conflict_clause); tout << "\n";
tout << "xk: "; if (m_xk != null_var) m_display_var(tout, m_xk); else tout << "<null>"; tout << "\n";
tout << "scope_lvl: " << scope_lvl() << "\n";
tout << "current assignment\n"; display_assignment(tout); display_bool_assignment(tout););
tout << "current assignment\n"; display_assignment(tout););
// static unsigned counter = 0;
// counter++;
@ -1588,7 +1716,7 @@ namespace nlsat {
conflict_clause = new_cls;
goto start;
}
TRACE("nlsat_resolve_done", display_assignment(tout); display_bool_assignment(tout););
TRACE("nlsat_resolve_done", display_assignment(tout););
return true;
}
@ -1801,6 +1929,15 @@ namespace nlsat {
reorder(p.size(), p.c_ptr());
}
bool can_reorder() const {
for (unsigned i = 0; i < m_atoms.size(); ++i) {
if (m_atoms[i]) {
if (m_atoms[i]->is_root_atom()) return false;
}
}
return true;
}
/**
\brief Reorder variables using the giving permutation.
p maps internal variables to their new positions
@ -1921,6 +2058,9 @@ namespace nlsat {
void reinit_cache() {
reinit_cache(m_clauses);
reinit_cache(m_learned);
for (unsigned i = 0; i < m_atoms.size(); ++i) {
reinit_cache(m_atoms[i]);
}
}
void reinit_cache(clause_vector const & cs) {
unsigned sz = cs.size();
@ -1934,10 +2074,13 @@ namespace nlsat {
}
void reinit_cache(literal l) {
bool_var b = l.var();
atom * a = m_atoms[b];
if (a == 0)
return;
if (a->is_ineq_atom()) {
reinit_cache(m_atoms[b]);
}
void reinit_cache(atom* a) {
if (a == 0) {
}
else if (a->is_ineq_atom()) {
var max = 0;
unsigned sz = to_ineq_atom(a)->size();
for (unsigned i = 0; i < sz; i++) {
@ -2073,7 +2216,7 @@ namespace nlsat {
//
// -----------------------
void display_assignment(std::ostream & out, display_var_proc const & proc) const {
void display_num_assignment(std::ostream & out, display_var_proc const & proc) const {
for (var x = 0; x < num_vars(); x++) {
if (m_assignment.is_assigned(x)) {
proc(out, x);
@ -2084,7 +2227,7 @@ namespace nlsat {
}
}
void display_bool_assignment(std::ostream & out, display_var_proc const & proc) const {
void display_bool_assignment(std::ostream & out) const {
unsigned sz = m_atoms.size();
for (bool_var b = 0; b < sz; b++) {
if (m_atoms[b] == 0 && m_bvalues[b] != l_undef) {
@ -2112,12 +2255,13 @@ namespace nlsat {
return !first;
}
void display_assignment(std::ostream & out) const {
display_assignment(out, m_display_var);
void display_num_assignment(std::ostream & out) const {
display_num_assignment(out, m_display_var);
}
void display_bool_assignment(std::ostream & out) const {
display_bool_assignment(out, m_display_var);
void display_assignment(std::ostream& out) const {
display_bool_assignment(out);
display_num_assignment(out);
}
void display(std::ostream & out, ineq_atom const & a, display_var_proc const & proc, bool use_star = false) const {
@ -2511,6 +2655,7 @@ namespace nlsat {
void display(std::ostream & out) const {
display(out, m_display_var);
display_assignment(out);
}
void display_vars(std::ostream & out) const {
@ -2562,6 +2707,20 @@ namespace nlsat {
return m_imp->check();
}
lbool solver::check(literal_vector& assumptions) {
return m_imp->check(assumptions);
}
void solver::reset() {
m_imp->reset();
}
void solver::updt_params(params_ref const & p) {
m_imp->updt_params(p);
}
void solver::collect_param_descrs(param_descrs & d) {
algebraic_numbers::manager::collect_param_descrs(d);
nlsat_params::collect_param_descrs(d);
@ -2583,6 +2742,10 @@ namespace nlsat {
m_imp->m_display_var.m_proc = &proc;
}
unsigned solver::num_vars() const {
return m_imp->num_vars();
}
bool solver::is_int(var x) const {
return m_imp->is_int(x);
}
@ -2590,10 +2753,61 @@ namespace nlsat {
bool_var solver::mk_bool_var() {
return m_imp->mk_bool_var();
}
literal solver::mk_true() {
return literal(0, false);
}
atom * solver::bool_var2atom(bool_var b) {
return m_imp->m_atoms[b];
}
void solver::vars(literal l, var_vector& vs) {
m_imp->vars(l, vs);
}
atom_vector const& solver::get_atoms() {
return m_imp->m_atoms;
}
atom_vector const& solver::get_var2eq() {
return m_imp->m_var2eq;
}
evaluator& solver::get_evaluator() {
return m_imp->m_evaluator;
}
explain& solver::get_explain() {
return m_imp->m_explain;
}
void solver::reorder(unsigned sz, var const* p) {
m_imp->reorder(sz, p);
}
void solver::restore_order() {
m_imp->restore_order();
}
void solver::set_rvalues(assignment const& as) {
m_imp->m_assignment.copy(as);
}
void solver::get_rvalues(assignment& as) {
as.copy(m_imp->m_assignment);
}
void solver::get_bvalues(svector<lbool>& vs) {
vs.reset();
vs.append(m_imp->m_bvalues);
}
void solver::set_bvalues(svector<lbool> const& vs) {
m_imp->m_bvalues.reset();
m_imp->m_bvalues.append(vs);
m_imp->m_bvalues.resize(m_imp->m_atoms.size(), l_undef);
}
var solver::mk_var(bool is_int) {
return m_imp->mk_var(is_int);
@ -2631,10 +2845,21 @@ namespace nlsat {
m_imp->display(out, l);
}
void solver::display(std::ostream & out, unsigned n, literal const* ls) const {
for (unsigned i = 0; i < n; ++i) {
display(out, ls[i]);
out << "; ";
}
}
void solver::display(std::ostream & out, var x) const {
m_imp->m_display_var(out, x);
}
void solver::display(std::ostream & out, atom const& a) const {
m_imp->display(out, a, m_imp->m_display_var);
}
display_var_proc const & solver::display_proc() const {
return m_imp->m_display_var;
}

56
src/nlsat/nlsat_solver.h
View file

@ -28,6 +28,9 @@ Revision History:
namespace nlsat {
class evaluator;
class explain;
class solver {
struct imp;
imp * m_imp;
@ -63,7 +66,9 @@ namespace nlsat {
nonlinear arithmetic atom.
*/
bool_var mk_bool_var();
literal mk_true();
/**
\brief Create a real/integer variable.
*/
@ -121,6 +126,48 @@ namespace nlsat {
*/
atom * bool_var2atom(bool_var b);
/**
\brief extract free variables from literal.
*/
void vars(literal l, var_vector& vs);
/**
\brief provide access to atoms. Used by explain.
*/
atom_vector const& get_atoms();
/**
\brief Access var -> asserted equality.
*/
atom_vector const& get_var2eq();
/**
\brief expose evaluator.
*/
evaluator& get_evaluator();
/**
\brief Access explanation module.
*/
explain& get_explain();
/**
\brief Access assignments to variables.
*/
void get_rvalues(assignment& as);
void set_rvalues(assignment const& as);
void get_bvalues(svector<lbool>& vs);
void set_bvalues(svector<lbool> const& vs);
/**
\brief reorder variables.
*/
void reorder(unsigned sz, var const* permutation);
void restore_order();
/**
\brief Return number of integer/real variables
*/
@ -135,6 +182,8 @@ namespace nlsat {
// -----------------------
lbool check();
lbool check(literal_vector& assumptions);
// -----------------------
//
// Model
@ -154,6 +203,7 @@ namespace nlsat {
void updt_params(params_ref const & p);
static void collect_param_descrs(param_descrs & d);
void reset();
void collect_statistics(statistics & st);
void reset_statistics();
void display_status(std::ostream & out) const;
@ -174,6 +224,10 @@ namespace nlsat {
*/
void display(std::ostream & out, literal l) const;
void display(std::ostream & out, unsigned n, literal const* ls) const;
void display(std::ostream & out, atom const& a) const;
/**
\brief Display variable
*/

921
src/qe/nlqsat.cpp Normal file
View file

@ -0,0 +1,921 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
nlqsat.cpp
Abstract:
Quantifier Satisfiability Solver for nlsat
Author:
Nikolaj Bjorner (nbjorner) 2015-10-17
Revision History:
--*/
#include "nlqsat.h"
#include "nlsat_solver.h"
#include "nlsat_explain.h"
#include "nlsat_assignment.h"
#include "qsat.h"
#include "quant_hoist.h"
#include "goal2nlsat.h"
#include "expr2var.h"
#include "uint_set.h"
#include "ast_util.h"
#include "tseitin_cnf_tactic.h"
#include "expr_safe_replace.h"
namespace qe {
enum qsat_mode_t {
qsat_t,
elim_t,
interp_t
};
class nlqsat : public tactic {
typedef unsigned_vector assumption_vector;
typedef nlsat::scoped_literal_vector clause;
struct stats {
unsigned m_num_rounds;
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
ast_manager& m;
qsat_mode_t m_mode;
params_ref m_params;
nlsat::solver m_solver;
tactic_ref m_nftactic;
nlsat::literal_vector m_asms;
nlsat::literal_vector m_cached_asms;
unsigned_vector m_cached_asms_lim;
nlsat::literal m_is_true;
nlsat::assignment m_rmodel;
svector<lbool> m_bmodel;
nlsat::assignment m_rmodel0;
svector<lbool> m_bmodel0;
bool m_valid_model;
vector<nlsat::var_vector> m_bound_rvars;
vector<svector<nlsat::bool_var> > m_bound_bvars;
vector<nlsat::scoped_literal_vector> m_preds;
svector<max_level> m_rvar2level;
u_map<max_level> m_bvar2level;
expr2var m_a2b, m_t2x;
u_map<expr*> m_b2a, m_x2t;
volatile bool m_cancel;
stats m_stats;
statistics m_st;
obj_hashtable<expr> m_free_vars;
expr_ref_vector m_answer;
expr_safe_replace m_answer_simplify;
nlsat::literal_vector m_assumptions;
u_map<expr*> m_asm2fml;
expr_ref_vector m_trail;
lbool check_sat() {
while (true) {
++m_stats.m_num_rounds;
check_cancel();
init_assumptions();
lbool res = m_solver.check(m_asms);
switch (res) {
case l_true:
TRACE("qe", display(tout); );
save_model();
push();
break;
case l_false:
if (0 == level()) return l_false;
if (1 == level() && m_mode == qsat_t) return l_true;
project();
break;
case l_undef:
return res;
}
}
return l_undef;
}
void init_assumptions() {
unsigned lvl = level();
m_asms.reset();
m_asms.push_back(is_exists()?m_is_true:~m_is_true);
m_asms.append(m_assumptions);
TRACE("qe", tout << "model valid: " << m_valid_model << " level: " << lvl << " ";
display_assumptions(tout);
m_solver.display(tout););
if (!m_valid_model) {
m_asms.append(m_cached_asms);
return;
}
unsave_model();
if (lvl == 0) {
SASSERT(m_cached_asms.empty());
return;
}
if (lvl <= m_preds.size()) {
for (unsigned j = 0; j < m_preds[lvl - 1].size(); ++j) {
add_literal(m_cached_asms, m_preds[lvl - 1][j]);
}
}
m_asms.append(m_cached_asms);
for (unsigned i = lvl + 1; i < m_preds.size(); i += 2) {
for (unsigned j = 0; j < m_preds[i].size(); ++j) {
nlsat::literal l = m_preds[i][j];
max_level lv = m_bvar2level.find(l.var());
bool use =
(lv.m_fa == i && (lv.m_ex == UINT_MAX || lv.m_ex < lvl)) ||
(lv.m_ex == i && (lv.m_fa == UINT_MAX || lv.m_fa < lvl));
if (use) {
add_literal(m_asms, l);
}
}
}
TRACE("qe", display(tout);
for (unsigned i = 0; i < m_asms.size(); ++i) {
m_solver.display(tout, m_asms[i]); tout << "\n";
});
save_model();
}
void add_literal(nlsat::literal_vector& lits, nlsat::literal l) {
lbool r = m_solver.value(l);
switch (r) {
case l_true:
lits.push_back(l);
break;
case l_false:
lits.push_back(~l);
break;
default:
UNREACHABLE();
break;
}
}
template<class S, class T>
void insert_set(S& set, T const& vec) {
for (unsigned i = 0; i < vec.size(); ++i) {
set.insert(vec[i]);
}
}
void mbp(unsigned level, nlsat::scoped_literal_vector& result) {
nlsat::var_vector vars;
uint_set fvars;
extract_vars(level, vars, fvars);
mbp(vars, fvars, result);
}
void extract_vars(unsigned level, nlsat::var_vector& vars, uint_set& fvars) {
for (unsigned i = 0; i < m_bound_rvars.size(); ++i) {
if (i < level) {
insert_set(fvars, m_bound_bvars[i]);
}
else {
vars.append(m_bound_rvars[i]);
}
}
}
void mbp(nlsat::var_vector const& vars, uint_set const& fvars, clause& result) {
//
// Also project auxiliary variables from clausification.
//
unsave_model();
nlsat::explain& ex = m_solver.get_explain();
nlsat::scoped_literal_vector new_result(m_solver);
result.reset();
// project quantified Boolean variables.
for (unsigned i = 0; i < m_asms.size(); ++i) {
nlsat::literal lit = m_asms[i];
if (!m_b2a.contains(lit.var()) || fvars.contains(lit.var())) {
result.push_back(lit);
}
}
TRACE("qe", m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";);
// project quantified real variables.
// They are sorted by size, so we project the largest variables first to avoid
// renaming variables.
for (unsigned i = vars.size(); i > 0;) {
--i;
new_result.reset();
ex.project(vars[i], result.size(), result.c_ptr(), new_result);
result.swap(new_result);
TRACE("qe", m_solver.display(tout, result.size(), result.c_ptr()); tout << "\n";);
}
negate_clause(result);
}
void negate_clause(clause& result) {
for (unsigned i = 0; i < result.size(); ++i) {
result.set(i, ~result[i]);
}
}
void save_model() {
m_solver.get_rvalues(m_rmodel);
m_solver.get_bvalues(m_bmodel);
m_valid_model = true;
if (is_exists(level())) {
m_rmodel0.copy(m_rmodel);
m_bmodel0.reset();
m_bmodel0.append(m_bmodel);
}
}
void unsave_model() {
SASSERT(m_valid_model);
m_solver.set_rvalues(m_rmodel);
m_solver.set_bvalues(m_bmodel);
}
void clear_model() {
m_valid_model = false;
m_rmodel.reset();
m_bmodel.reset();
m_solver.set_rvalues(m_rmodel);
}
unsigned level() const {
return m_cached_asms_lim.size();
}
void enforce_parity(clause& cl) {
cl.push_back(is_exists()?~m_is_true:m_is_true);
}
void add_clause(clause& cl) {
if (cl.empty()) {
cl.push_back(~m_solver.mk_true());
}
SASSERT(!cl.empty());
nlsat::literal_vector lits(cl.size(), cl.c_ptr());
m_solver.mk_clause(lits.size(), lits.c_ptr());
}
max_level get_level(clause const& cl) {
return get_level(cl.size(), cl.c_ptr());
}
max_level get_level(unsigned n, nlsat::literal const* ls) {
max_level level;
for (unsigned i = 0; i < n; ++i) {
level.merge(get_level(ls[i]));
}
return level;
}
max_level get_level(nlsat::literal l) {
max_level level;
if (m_bvar2level.find(l.var(), level)) {
return level;
}
nlsat::var_vector vs;
m_solver.vars(l, vs);
for (unsigned i = 0; i < vs.size(); ++i) {
level.merge(m_rvar2level[vs[i]]);
}
set_level(l.var(), level);
return level;
}
void set_level(nlsat::bool_var v, max_level const& level) {
unsigned k = level.max();
while (m_preds.size() <= k) {
m_preds.push_back(nlsat::scoped_literal_vector(m_solver));
}
nlsat::literal l(v, false);
m_preds[k].push_back(l);
m_bvar2level.insert(v, level);
TRACE("qe", m_solver.display(tout, l); tout << ": " << level << "\n";);
}
void project() {
TRACE("qe", display_assumptions(tout););
if (!m_valid_model) {
pop(1);
return;
}
if (m_mode == elim_t) {
project_qe();
return;
}
SASSERT(level() >= 2);
unsigned num_scopes;
clause cl(m_solver);
mbp(level()-1, cl);
max_level clevel = get_level(cl);
enforce_parity(cl);
add_clause(cl);
if (clevel.max() == UINT_MAX) {
num_scopes = 2*(level()/2);
}
else {
SASSERT(clevel.max() + 2 <= level());
num_scopes = level() - clevel.max();
if ((num_scopes % 2) != 0) {
--num_scopes;
}
SASSERT(num_scopes >= 2);
}
TRACE("qe", tout << "backtrack: " << num_scopes << "\n";);
pop(num_scopes);
}
void project_qe() {
SASSERT(level() >= 1 && m_mode == elim_t && m_valid_model);
clause cl(m_solver);
mbp(std::max(1u, level()-1), cl);
expr_ref fml = clause2fml(cl);
TRACE("qe", tout << level() << ": " << fml << "\n";);
max_level clevel = get_level(cl);
if (level() == 1 || clevel.max() == 0) {
add_assumption_literal(cl, fml);
}
else {
enforce_parity(cl);
}
add_clause(cl);
if (level() == 1) { // is_forall() && clevel.max() == 0
add_to_answer(fml);
}
if (level() == 1) {
pop(1);
}
else {
pop(2);
}
}
void add_to_answer(expr_ref& fml) {
m_answer_simplify(fml);
expr* e;
if (m.is_not(fml, e)) {
m_answer_simplify.insert(e, m.mk_false());
}
else {
m_answer_simplify.insert(fml, m.mk_true());
}
m_answer.push_back(fml);
}
expr_ref clause2fml(nlsat::scoped_literal_vector const& clause) {
expr_ref_vector fmls(m);
expr_ref fml(m);
expr* t;
nlsat2goal n2g(m);
for (unsigned i = 0; i < clause.size(); ++i) {
nlsat::literal l = clause[i];
if (m_asm2fml.find(l.var(), t)) {
fml = t;
if (l.sign()) {
fml = push_not(fml);
}
SASSERT(l.sign());
fmls.push_back(fml);
}
else {
fmls.push_back(n2g(m_solver, m_b2a, m_x2t, l));
}
}
fml = mk_or(fmls);
return fml;
}
void add_assumption_literal(clause& clause, expr* fml) {
nlsat::bool_var b = m_solver.mk_bool_var();
clause.push_back(nlsat::literal(b, true));
m_assumptions.push_back(nlsat::literal(b, false));
m_asm2fml.insert(b, fml);
m_trail.push_back(fml);
m_bvar2level.insert(b, max_level());
}
bool is_exists() const { return is_exists(level()); }
bool is_forall() const { return is_forall(level()); }
bool is_exists(unsigned level) const { return (level % 2) == 0; }
bool is_forall(unsigned level) const { return is_exists(level+1); }
void check_cancel() {
if (m_cancel) {
throw tactic_exception(TACTIC_CANCELED_MSG);
}
}
void reset() {
//m_solver.reset();
m_asms.reset();
m_cached_asms.reset();
m_cached_asms_lim.reset();
m_is_true = nlsat::null_literal;
m_rmodel.reset();
m_valid_model = false;
m_bound_rvars.reset();
m_bound_bvars.reset();
m_preds.reset();
m_rvar2level.reset();
m_bvar2level.reset();
m_t2x.reset();
m_a2b.reset();
m_b2a.reset();
m_x2t.reset();
m_cancel = false;
m_st.reset();
m_solver.collect_statistics(m_st);
m_free_vars.reset();
m_answer.reset();
m_answer_simplify.reset();
m_assumptions.reset();
m_asm2fml.reset();
m_trail.reset();
}
void push() {
m_cached_asms_lim.push_back(m_cached_asms.size());
}
void pop(unsigned num_scopes) {
clear_model();
unsigned new_level = level() - num_scopes;
m_cached_asms.shrink(m_cached_asms_lim[new_level]);
m_cached_asms_lim.shrink(new_level);
}
void display(std::ostream& out) {
display_preds(out);
display_assumptions(out);
m_solver.display(out << "solver:\n");
}
void display_assumptions(std::ostream& out) {
m_solver.display(out << "assumptions: ", m_asms.size(), m_asms.c_ptr());
out << "\n";
}
void display_preds(std::ostream& out) {
for (unsigned i = 0; i < m_preds.size(); ++i) {
m_solver.display(out << i << ": ", m_preds[i].size(), m_preds[i].c_ptr());
out << "\n";
}
}
// expr -> nlsat::solver
void hoist(expr_ref& fml) {
quantifier_hoister hoist(m);
vector<app_ref_vector> qvars;
app_ref_vector vars(m);
bool is_forall = false;
pred_abs abs(m);
abs.get_free_vars(fml, vars);
insert_set(m_free_vars, vars);
qvars.push_back(vars);
vars.reset();
if (m_mode == elim_t) {
is_forall = true;
hoist.pull_quantifier(is_forall, fml, vars);
qvars.push_back(vars);
}
else {
hoist.pull_quantifier(is_forall, fml, vars);
qvars.back().append(vars);
}
do {
is_forall = !is_forall;
vars.reset();
hoist.pull_quantifier(is_forall, fml, vars);
qvars.push_back(vars);
}
while (!vars.empty());
SASSERT(qvars.back().empty());
init_expr2var(qvars);
goal2nlsat g2s;
expr_ref is_true(m), fml1(m), fml2(m);
is_true = m.mk_fresh_const("is_true", m.mk_bool_sort());
fml = m.mk_iff(is_true, fml);
goal_ref g = alloc(goal, m);
g->assert_expr(fml);
proof_converter_ref pc;
expr_dependency_ref core(m);
model_converter_ref mc;
goal_ref_buffer result;
(*m_nftactic)(g, result, mc, pc, core);
SASSERT(result.size() == 1);
TRACE("qe", result[0]->display(tout););
g2s(*result[0], m_params, m_solver, m_a2b, m_t2x);
// insert variables and their levels.
for (unsigned i = 0; i < qvars.size(); ++i) {
m_bound_bvars.push_back(svector<nlsat::bool_var>());
m_bound_rvars.push_back(nlsat::var_vector());
max_level lvl;
if (is_exists(i)) lvl.m_ex = i; else lvl.m_fa = i;
for (unsigned j = 0; j < qvars[i].size(); ++j) {
app* v = qvars[i][j].get();
if (m_a2b.is_var(v)) {
SASSERT(m.is_bool(v));
nlsat::bool_var b = m_a2b.to_var(v);
m_bound_bvars.back().push_back(b);
set_level(b, lvl);
}
else if (m_t2x.is_var(v)) {
nlsat::var w = m_t2x.to_var(v);
m_bound_rvars.back().push_back(w);
m_rvar2level.setx(w, lvl, max_level());
}
}
}
init_var2expr();
m_is_true = nlsat::literal(m_a2b.to_var(is_true), false);
// insert literals from arithmetical sub-formulas
nlsat::atom_vector const& atoms = m_solver.get_atoms();
for (unsigned i = 0; i < atoms.size(); ++i) {
if (atoms[i]) {
get_level(nlsat::literal(i, false));
}
}
TRACE("qe", tout << fml << "\n";);
}
void init_expr2var(vector<app_ref_vector> const& qvars) {
for (unsigned i = 0; i < qvars.size(); ++i) {
init_expr2var(qvars[i]);
}
}
void init_expr2var(app_ref_vector const& qvars) {
for (unsigned i = 0; i < qvars.size(); ++i) {
app* v = qvars[i];
if (m.is_bool(v)) {
m_a2b.insert(v, m_solver.mk_bool_var());
}
else {
// TODO: assert it is of type Real.
m_t2x.insert(v, m_solver.mk_var(false));
}
}
}
void init_var2expr() {
expr2var::iterator it = m_t2x.begin(), end = m_t2x.end();
for (; it != end; ++it) {
m_x2t.insert(it->m_value, it->m_key);
}
it = m_a2b.begin(), end = m_a2b.end();
for (; it != end; ++it) {
m_b2a.insert(it->m_value, it->m_key);
}
}
// Return false if nlsat assigned noninteger value to an integer variable.
// [copied from nlsat_tactic.cpp]
bool mk_model(model_converter_ref & mc) {
bool ok = true;
model_ref md = alloc(model, m);
arith_util util(m);
expr2var::iterator it = m_t2x.begin(), end = m_t2x.end();
for (; it != end; ++it) {
nlsat::var x = it->m_value;
expr * t = it->m_key;
if (!is_uninterp_const(t) || !m_free_vars.contains(t))
continue;
expr * v;
try {
v = util.mk_numeral(m_rmodel0.value(x), util.is_int(t));
}
catch (z3_error & ex) {
throw ex;
}
catch (z3_exception &) {
v = util.mk_to_int(util.mk_numeral(m_rmodel0.value(x), false));
ok = false;
}
md->register_decl(to_app(t)->get_decl(), v);
}
it = m_a2b.begin(), end = m_a2b.end();
for (; it != end; ++it) {
expr * a = it->m_key;
nlsat::bool_var b = it->m_value;
if (a == 0 || !is_uninterp_const(a) || b == m_is_true.var() || !m_free_vars.contains(a))
continue;
lbool val = m_bmodel0.get(b, l_undef);
if (val == l_undef)
continue; // don't care
md->register_decl(to_app(a)->get_decl(), val == l_true ? m.mk_true() : m.mk_false());
}
mc = model2model_converter(md.get());
return ok;
}
public:
nlqsat(ast_manager& m, qsat_mode_t mode, params_ref const& p):
m(m),
m_mode(mode),
m_params(p),
m_solver(m.limit(), p),
m_nftactic(0),
m_rmodel(m_solver.am()),
m_rmodel0(m_solver.am()),
m_valid_model(false),
m_a2b(m),
m_t2x(m),
m_cancel(false),
m_answer(m),
m_answer_simplify(m),
m_trail(m)
{
m_solver.get_explain().set_signed_project(true);
m_nftactic = mk_tseitin_cnf_tactic(m);
}
virtual ~nlqsat() {
}
void updt_params(params_ref const & p) {
params_ref p2(p);
p2.set_bool("factor", false);
m_solver.updt_params(p2);
}
void collect_param_descrs(param_descrs & r) {
}
void operator()(/* in */ goal_ref const & in,
/* out */ goal_ref_buffer & result,
/* out */ model_converter_ref & mc,
/* out */ proof_converter_ref & pc,
/* out */ expr_dependency_ref & core) {
tactic_report report("nlqsat-tactic", *in);
ptr_vector<expr> fmls;
expr_ref fml(m);
mc = 0; pc = 0; core = 0;
in->get_formulas(fmls);
fml = mk_and(m, fmls.size(), fmls.c_ptr());
if (m_mode == elim_t) {
fml = m.mk_not(fml);
}
reset();
TRACE("qe", tout << fml << "\n";);
hoist(fml);
TRACE("qe", tout << "ex: " << fml << "\n";);
lbool is_sat = check_sat();
switch (is_sat) {
case l_false:
in->reset();
in->inc_depth();
if (m_mode == elim_t) {
fml = mk_and(m_answer);
}
else {
fml = m.mk_false();
}
in->assert_expr(fml);
result.push_back(in.get());
break;
case l_true:
SASSERT(m_mode == qsat_t);
in->reset();
in->inc_depth();
result.push_back(in.get());
if (in->models_enabled()) {
VERIFY(mk_model(mc));
}
break;
case l_undef:
result.push_back(in.get());
std::string s = "search failed";
throw tactic_exception(s.c_str());
}
}
void collect_statistics(statistics & st) const {
st.copy(m_st);
st.update("qsat num rounds", m_stats.m_num_rounds);
}
void reset_statistics() {
m_stats.reset();
m_solver.reset_statistics();
}
void cleanup() {
reset();
}
void set_logic(symbol const & l) {
}
void set_progress_callback(progress_callback * callback) {
}
tactic * translate(ast_manager & m) {
return alloc(nlqsat, m, m_mode, m_params);
}
#if 0
/**
Algorithm:
I := true
while there is M, such that M |= ~B & I:
find P, such that M => P => exists y . ~B & I
; forall y B => ~P
C := core of P with respect to A
; A => ~ C => ~ P
I := I & ~C
Alternative Algorithm:
R := false
while there is M, such that M |= A & ~R:
find I, such that M => I => forall y . B
R := R | I
*/
lbool interpolate(expr* a, expr* b, expr_ref& result) {
SASSERT(m_mode == interp_t);
reset();
app_ref enableA(m), enableB(m);
expr_ref A(m), B(m), fml(m);
expr_ref_vector fmls(m), answer(m);
// varsB are private to B.
nlsat::var_vector vars;
uint_set fvars;
private_vars(a, b, vars, fvars);
enableA = m.mk_const(symbol("#A"), m.mk_bool_sort());
enableB = m.mk_not(enableA);
A = m.mk_implies(enableA, a);
B = m.mk_implies(enableB, m.mk_not(b));
fml = m.mk_and(A, B);
hoist(fml);
nlsat::literal _enableB = nlsat::literal(m_a2b.to_var(enableB), false);
nlsat::literal _enableA = ~_enableB;
while (true) {
m_mode = qsat_t;
// enable B
m_assumptions.reset();
m_assumptions.push_back(_enableB);
lbool is_sat = check_sat();
switch (is_sat) {
case l_undef:
return l_undef;
case l_true:
break;
case l_false:
result = mk_and(answer);
return l_true;
}
// disable B, enable A
m_assumptions.reset();
m_assumptions.push_back(_enableA);
// add blocking clause to solver.
nlsat::scoped_literal_vector core(m_solver);
m_mode = elim_t;
mbp(vars, fvars, core);
// minimize core.
nlsat::literal_vector _core(core.size(), core.c_ptr());
_core.push_back(_enableA);
is_sat = m_solver.check(_core); // TBD: only for quantifier-free A. Generalize output of elim_t to be a core.
switch (is_sat) {
case l_undef:
return l_undef;
case l_true:
UNREACHABLE();
case l_false:
core.reset();
core.append(_core.size(), _core.c_ptr());
break;
}
negate_clause(core);
// keep polarity of enableA, such that clause is only
// used when checking satisfiability of B.
for (unsigned i = 0; i < core.size(); ++i) {
if (core[i].var() == _enableA.var()) core.set(i, ~core[i]);
}
add_clause(core); // Invariant is added as assumption for B.
answer.push_back(clause2fml(core)); // TBD: remove answer literal.
}
}
/**
\brief extract variables that are private to a (not used in b).
vars cover the real variables, and fvars cover the Boolean variables.
TBD: We want fvars to be the complement such that returned core contains
Shared boolean variables, but not the ones private to B.
*/
void private_vars(expr* a, expr* b, nlsat::var_vector& vars, uint_set& fvars) {
app_ref_vector varsA(m), varsB(m);
obj_hashtable<expr> varsAS;
pred_abs abs(m);
abs.get_free_vars(a, varsA);
abs.get_free_vars(b, varsB);
insert_set(varsAS, varsA);
for (unsigned i = 0; i < varsB.size(); ++i) {
if (varsAS.contains(varsB[i].get())) {
varsB[i] = varsB.back();
varsB.pop_back();
--i;
}
}
for (unsigned j = 0; j < varsB.size(); ++j) {
app* v = varsB[j].get();
if (m_a2b.is_var(v)) {
fvars.insert(m_a2b.to_var(v));
}
else if (m_t2x.is_var(v)) {
vars.push_back(m_t2x.to_var(v));
}
}
}
lbool maximize(app* _x, expr* _fml, scoped_anum& result, bool& unbounded) {
expr_ref fml(_fml, m);
reset();
hoist(fml);
nlsat::literal_vector lits;
lbool is_sat = l_true;
nlsat::var x = m_t2x.to_var(_x);
m_mode = qsat_t;
while (is_sat == l_true) {
is_sat = check_sat();
if (is_sat == l_true) {
// m_asms is minimized set of literals that satisfy formula.
nlsat::explain& ex = m_solver.get_explain();
polynomial::manager& pm = m_solver.pm();
anum_manager& am = m_solver.am();
ex.maximize(x, m_asms.size(), m_asms.c_ptr(), result, unbounded);
if (unbounded) {
break;
}
// TBD: assert the new bound on x using the result.
bool is_even = false;
polynomial::polynomial_ref pr(pm);
pr = pm.mk_polynomial(x);
rational r;
am.get_upper(result, r);
// result is algebraic numeral, but polynomials are not defined over extension field.
polynomial::polynomial* p = pr;
nlsat::bool_var b = m_solver.mk_ineq_atom(nlsat::atom::GT, 1, &p, &is_even);
nlsat::literal bound(b, false);
m_solver.mk_clause(1, &bound);
}
}
return is_sat;
}
#endif
};
};
tactic * mk_nlqsat_tactic(ast_manager & m, params_ref const& p) {
return alloc(qe::nlqsat, m, qe::qsat_t, p);
}
tactic * mk_nlqe_tactic(ast_manager & m, params_ref const& p) {
return alloc(qe::nlqsat, m, qe::elim_t, p);
}

38
src/qe/nlqsat.h Normal file
View file

@ -0,0 +1,38 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
nlqsat.h
Abstract:
Quantifier Satisfiability Solver for nlsat
Author:
Nikolaj Bjorner (nbjorner) 2015-10-17
Revision History:
--*/
#ifndef QE_NLQSAT_H__
#define QE_NLQSAT_H__
#include "tactic.h"
tactic * mk_nlqsat_tactic(ast_manager & m, params_ref const& p = params_ref());
tactic * mk_nlqe_tactic(ast_manager & m, params_ref const& p = params_ref());
/*
ADD_TACTIC("nlqsat", "apply a NL-QSAT solver.", "mk_nlqsat_tactic(m, p)")
*/
// TBD_TACTIC("nlqe", "apply a NL-QE solver.", "mk_nlqe_tactic(m, p)")
#endif

26
src/qe/qe_util.cpp
View file

@ -1,26 +0,0 @@
/*++
Copyright (c) 2015 Microsoft Corporation
--*/
#include "qe_util.h"
#include "bool_rewriter.h"
namespace qe {
expr_ref mk_and(expr_ref_vector const& fmls) {
ast_manager& m = fmls.get_manager();
expr_ref result(m);
bool_rewriter(m).mk_and(fmls.size(), fmls.c_ptr(), result);
return result;
}
expr_ref mk_or(expr_ref_vector const& fmls) {
ast_manager& m = fmls.get_manager();
expr_ref result(m);
bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), result);
return result;
}
}

31
src/qe/qe_util.h
View file

@ -1,31 +0,0 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
qe_util.h
Abstract:
Utilities for quantifiers.
Author:
Nikolaj Bjorner (nbjorner) 2013-08-28
Revision History:
--*/
#ifndef QE_UTIL_H_
#define QE_UTIL_H_
#include "ast.h"
namespace qe {
expr_ref mk_and(expr_ref_vector const& fmls);
expr_ref mk_or(expr_ref_vector const& fmls);
}
#endif

1176
src/qe/qsat.cpp Normal file
View file

File diff suppressed because it is too large Load diff

135
src/qe/qsat.h Normal file
View file

@ -0,0 +1,135 @@
/*++
Copyright (c) 2015 Microsoft Corporation
Module Name:
qsat.h
Abstract:
Quantifier Satisfiability Solver.
Author:
Nikolaj Bjorner (nbjorner) 2015-5-28
Revision History:
--*/
#ifndef QE_QSAT_H__
#define QE_QSAT_H__
#include "tactic.h"
#include "filter_model_converter.h"
namespace qe {
struct max_level {
unsigned m_ex, m_fa;
max_level(): m_ex(UINT_MAX), m_fa(UINT_MAX) {}
void merge(max_level const& other) {
merge(m_ex, other.m_ex);
merge(m_fa, other.m_fa);
}
static unsigned max(unsigned a, unsigned b) {
if (a == UINT_MAX) return b;
if (b == UINT_MAX) return a;
return std::max(a, b);
}
unsigned max() const {
return max(m_ex, m_fa);
}
void merge(unsigned& lvl, unsigned other) {
lvl = max(lvl, other);
}
std::ostream& display(std::ostream& out) const {
if (m_ex != UINT_MAX) out << "e" << m_ex << " ";
if (m_fa != UINT_MAX) out << "a" << m_fa << " ";
return out;
}
bool operator==(max_level const& other) const {
return
m_ex == other.m_ex &&
m_fa == other.m_fa;
}
};
inline std::ostream& operator<<(std::ostream& out, max_level const& lvl) {
return lvl.display(out);
}
class pred_abs {
ast_manager& m;
vector<app_ref_vector> m_preds;
expr_ref_vector m_asms;
unsigned_vector m_asms_lim;
obj_map<expr, expr*> m_pred2lit; // maintain definitions of predicates.
obj_map<expr, app*> m_lit2pred; // maintain reverse mapping to predicates
obj_map<expr, app*> m_asm2pred; // maintain map from assumptions to predicates
obj_map<expr, expr*> m_pred2asm; // predicates |-> assumptions
expr_ref_vector m_trail;
filter_model_converter_ref m_fmc;
ptr_vector<expr> todo;
obj_map<expr, max_level> m_elevel;
obj_map<func_decl, max_level> m_flevel;
template <typename T>
void dec_keys(obj_map<expr, T*>& map) {
typename obj_map<expr, T*>::iterator it = map.begin(), end = map.end();
for (; it != end; ++it) {
m.dec_ref(it->m_key);
}
}
void add_lit(app* p, app* lit);
void add_asm(app* p, expr* lit);
bool is_predicate(app* a, unsigned l);
void mk_concrete(expr_ref_vector& fmls, obj_map<expr, expr*> const& map);
public:
pred_abs(ast_manager& m);
filter_model_converter* fmc();
void reset();
max_level compute_level(app* e);
void push();
void pop(unsigned num_scopes);
void insert(app* a, max_level const& lvl);
void get_assumptions(model* mdl, expr_ref_vector& asms);
void set_expr_level(app* v, max_level const& lvl);
void set_decl_level(func_decl* v, max_level const& lvl);
void abstract_atoms(expr* fml, max_level& level, expr_ref_vector& defs);
void abstract_atoms(expr* fml, expr_ref_vector& defs);
expr_ref mk_abstract(expr* fml);
void pred2lit(expr_ref_vector& fmls);
expr_ref pred2asm(expr* fml);
void get_free_vars(expr* fml, app_ref_vector& vars);
expr_ref mk_assumption_literal(expr* a, model* mdl, max_level const& lvl, expr_ref_vector& defs);
void add_pred(app* p, app* lit);
app_ref fresh_bool(char const* name);
void display(std::ostream& out) const;
void display(std::ostream& out, expr_ref_vector const& asms) const;
void collect_statistics(statistics& st) const;
};
}
tactic * mk_qsat_tactic(ast_manager & m, params_ref const& p = params_ref());
tactic * mk_qe2_tactic(ast_manager & m, params_ref const& p = params_ref());
tactic * mk_qe_rec_tactic(ast_manager & m, params_ref const& p = params_ref());
/*
ADD_TACTIC("qsat", "apply a QSAT solver.", "mk_qsat_tactic(m, p)")
ADD_TACTIC("qe2", "apply a QSAT based quantifier elimination.", "mk_qe2_tactic(m, p)")
ADD_TACTIC("qe_rec", "apply a QSAT based quantifier elimination recursively.", "mk_qe_rec_tactic(m, p)")
*/
#endif

414
src/test/nlsat.cpp
View file

@ -21,6 +21,8 @@ Notes:
#include"nlsat_evaluator.h"
#include"nlsat_solver.h"
#include"util.h"
#include"nlsat_explain.h"
#include"polynomial_cache.h"
#include"rlimit.h"
nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1,
@ -29,7 +31,6 @@ nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1,
bool check_num_intervals = true) {
nlsat::interval_set_manager & ism = s1.m();
nlsat::interval_set_ref r(ism);
std::cout << "------------------\n";
std::cout << "s1: " << s1 << "\n";
std::cout << "s2: " << s2 << "\n";
r = ism.mk_union(s1, s2);
@ -277,10 +278,12 @@ static void tst5() {
nlsat::assignment as(am);
small_object_allocator allocator;
nlsat::interval_set_manager ism(am, allocator);
nlsat::evaluator ev(as, pm, allocator);
nlsat::evaluator ev(s, as, pm, allocator);
nlsat::var x0, x1;
x0 = pm.mk_var();
x1 = pm.mk_var();
nlsat::interval_set_ref i(ism);
polynomial_ref p(pm);
polynomial_ref _x0(pm), _x1(pm);
_x0 = pm.mk_polynomial(x0);
@ -291,7 +294,6 @@ static void tst5() {
nlsat::bool_var b = s.mk_ineq_atom(nlsat::atom::GT, 1, _p, is_even);
nlsat::atom * a = s.bool_var2atom(b);
SASSERT(a != 0);
nlsat::interval_set_ref i(ism);
scoped_anum zero(am);
am.set(zero, 0);
as.set(0, zero);
@ -302,8 +304,414 @@ static void tst5() {
std::cout << "2) " << i << "\n";
}
static void project(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, unsigned num, nlsat::literal const* lits) {
std::cout << "Project ";
s.display(std::cout, num, lits);
nlsat::scoped_literal_vector result(s);
ex.project(x, num, lits, result);
s.display(std::cout << "\n==>\n", result.size(), result.c_ptr());
std::cout << "\n";
}
static nlsat::literal mk_gt(nlsat::solver& s, nlsat::poly* p) {
nlsat::poly * _p[1] = { p };
bool is_even[1] = { false };
return s.mk_ineq_literal(nlsat::atom::GT, 1, _p, is_even);
}
static nlsat::literal mk_eq(nlsat::solver& s, nlsat::poly* p) {
nlsat::poly * _p[1] = { p };
bool is_even[1] = { false };
return s.mk_ineq_literal(nlsat::atom::EQ, 1, _p, is_even);
}
static void tst6() {
params_ref ps;
reslimit rlim;
nlsat::solver s(rlim, ps);
anum_manager & am = s.am();
nlsat::pmanager & pm = s.pm();
nlsat::assignment as(am);
nlsat::explain& ex = s.get_explain();
nlsat::var x0, x1, x2, a, b, c, d;
a = s.mk_var(false);
b = s.mk_var(false);
c = s.mk_var(false);
d = s.mk_var(false);
x0 = s.mk_var(false);
x1 = s.mk_var(false);
x2 = s.mk_var(false);
polynomial_ref p1(pm), p2(pm), p3(pm), p4(pm), p5(pm);
polynomial_ref _x0(pm), _x1(pm), _x2(pm);
polynomial_ref _a(pm), _b(pm), _c(pm), _d(pm);
_x0 = pm.mk_polynomial(x0);
_x1 = pm.mk_polynomial(x1);
_x2 = pm.mk_polynomial(x2);
_a = pm.mk_polynomial(a);
_b = pm.mk_polynomial(b);
_c = pm.mk_polynomial(c);
_d = pm.mk_polynomial(d);
p1 = (_a*(_x0^2)) + _x2 + 2;
p2 = (_b*_x1) - (2*_x2) - _x0 + 8;
nlsat::scoped_literal_vector lits(s);
lits.push_back(mk_gt(s, p1));
lits.push_back(mk_gt(s, p2));
lits.push_back(mk_gt(s, (_c*_x0) + _x2 + 1));
lits.push_back(mk_gt(s, (_d*_x0) - _x1 + 5*_x2));
scoped_anum zero(am), one(am), two(am);
am.set(zero, 0);
am.set(one, 1);
am.set(two, 2);
as.set(0, one);
as.set(1, one);
as.set(2, two);
as.set(3, two);
as.set(4, two);
as.set(5, one);
as.set(6, one);
s.set_rvalues(as);
project(s, ex, x0, 2, lits.c_ptr());
project(s, ex, x1, 3, lits.c_ptr());
project(s, ex, x2, 3, lits.c_ptr());
project(s, ex, x2, 2, lits.c_ptr());
project(s, ex, x2, 4, lits.c_ptr());
project(s, ex, x2, 3, lits.c_ptr()+1);
}
static void tst7() {
params_ref ps;
reslimit rlim;
nlsat::solver s(rlim, ps);
anum_manager & am = s.am();
nlsat::pmanager & pm = s.pm();
nlsat::var x0, x1, x2, a, b, c, d;
a = s.mk_var(false);
b = s.mk_var(false);
c = s.mk_var(false);
d = s.mk_var(false);
x0 = s.mk_var(false);
x1 = s.mk_var(false);
x2 = s.mk_var(false);
polynomial_ref p1(pm), p2(pm), p3(pm), p4(pm), p5(pm);
polynomial_ref _x0(pm), _x1(pm), _x2(pm);
polynomial_ref _a(pm), _b(pm), _c(pm), _d(pm);
_x0 = pm.mk_polynomial(x0);
_x1 = pm.mk_polynomial(x1);
_x2 = pm.mk_polynomial(x2);
_a = pm.mk_polynomial(a);
_b = pm.mk_polynomial(b);
_c = pm.mk_polynomial(c);
_d = pm.mk_polynomial(d);
p1 = _x0 + _x1;
p2 = _x2 - _x0;
p3 = (-1*_x0) - _x1;
nlsat::scoped_literal_vector lits(s);
lits.push_back(mk_gt(s, p1));
lits.push_back(mk_gt(s, p2));
lits.push_back(mk_gt(s, p3));
nlsat::literal_vector litsv(lits.size(), lits.c_ptr());
lbool res = s.check(litsv);
SASSERT(res == l_false);
for (unsigned i = 0; i < litsv.size(); ++i) {
s.display(std::cout, litsv[i]);
std::cout << " ";
}
std::cout << "\n";
litsv.reset();
litsv.append(2, lits.c_ptr());
res = s.check(litsv);
SASSERT(res == l_true);
s.display(std::cout);
s.am().display(std::cout, s.value(x0)); std::cout << "\n";
s.am().display(std::cout, s.value(x1)); std::cout << "\n";
s.am().display(std::cout, s.value(x2)); std::cout << "\n";
}
static void tst8() {
params_ref ps;
reslimit rlim;
nlsat::solver s(rlim, ps);
anum_manager & am = s.am();
nlsat::pmanager & pm = s.pm();
nlsat::assignment as(am);
nlsat::explain& ex = s.get_explain();
nlsat::var x0, x1, x2, a, b, c, d;
a = s.mk_var(false);
b = s.mk_var(false);
c = s.mk_var(false);
d = s.mk_var(false);
x0 = s.mk_var(false);
x1 = s.mk_var(false);
x2 = s.mk_var(false);
polynomial_ref p1(pm), p2(pm), p3(pm), p4(pm), p5(pm);
polynomial_ref _x0(pm), _x1(pm), _x2(pm);
polynomial_ref _a(pm), _b(pm), _c(pm), _d(pm);
_x0 = pm.mk_polynomial(x0);
_x1 = pm.mk_polynomial(x1);
_x2 = pm.mk_polynomial(x2);
_a = pm.mk_polynomial(a);
_b = pm.mk_polynomial(b);
_c = pm.mk_polynomial(c);
_d = pm.mk_polynomial(d);
scoped_anum zero(am), one(am), two(am), six(am);
am.set(zero, 0);
am.set(one, 1);
am.set(two, 2);
am.set(six, 6);
as.set(0, two); // a
as.set(1, one); // b
as.set(2, six); // c
as.set(3, zero); // d
as.set(4, zero); // x0
as.set(5, zero); // x1
as.set(6, two); // x2
s.set_rvalues(as);
nlsat::scoped_literal_vector lits(s);
lits.push_back(mk_eq(s, (_a*_x2*_x2) - (_b*_x2) - _c));
project(s, ex, x2, 1, lits.c_ptr());
}
static void tst9() {
params_ref ps;
reslimit rlim;
nlsat::solver s(rlim, ps);
anum_manager & am = s.am();
nlsat::pmanager & pm = s.pm();
nlsat::assignment as(am);
nlsat::explain& ex = s.get_explain();
int num_lo = 4;
int num_hi = 5;
svector<nlsat::var> los, his;
for (int i = 0; i < num_lo; ++i) {
los.push_back(s.mk_var(false));
scoped_anum num(am);
am.set(num, - i - 1);
as.set(i, num);
}
for (int i = 0; i < num_hi; ++i) {
his.push_back(s.mk_var(false));
scoped_anum num(am);
am.set(num, i + 1);
as.set(num_lo + i, num);
}
nlsat::var _z = s.mk_var(false);
nlsat::var _x = s.mk_var(false);
polynomial_ref x(pm), z(pm);
x = pm.mk_polynomial(_x);
scoped_anum val(am);
am.set(val, 0);
as.set(num_lo + num_hi, val);
as.set(num_lo + num_hi + 1, val);
s.set_rvalues(as);
nlsat::scoped_literal_vector lits(s);
for (int i = 0; i < num_lo; ++i) {
polynomial_ref y(pm);
y = pm.mk_polynomial(los[i]);
lits.push_back(mk_gt(s, x - y));
}
for (int i = 0; i < num_hi; ++i) {
polynomial_ref y(pm);
y = pm.mk_polynomial(his[i]);
lits.push_back(mk_gt(s, y - x));
}
z = pm.mk_polynomial(_z);
lits.push_back(mk_eq(s, x - z));
#define TEST_ON_OFF() \
std::cout << "Off "; \
ex.set_signed_project(false); \
project(s, ex, _x, lits.size()-1, lits.c_ptr()); \
std::cout << "On "; \
ex.set_signed_project(true); \
project(s, ex, _x, lits.size()-1, lits.c_ptr()); \
std::cout << "Off "; \
ex.set_signed_project(false); \
project(s, ex, _x, lits.size(), lits.c_ptr()); \
std::cout << "On "; \
ex.set_signed_project(true); \
project(s, ex, _x, lits.size(), lits.c_ptr()) \
TEST_ON_OFF();
lits.reset();
polynomial_ref u(pm);
u = pm.mk_polynomial(his[1]);
for (int i = 0; i < num_lo; ++i) {
polynomial_ref y(pm);
y = pm.mk_polynomial(los[i]);
lits.push_back(mk_gt(s, u*x - y));
}
for (int i = 0; i < num_hi; ++i) {
polynomial_ref y(pm);
y = pm.mk_polynomial(his[i]);
lits.push_back(mk_gt(s, y - u*x));
}
z = pm.mk_polynomial(_z);
lits.push_back(mk_eq(s, u*x - z));
TEST_ON_OFF();
lits.reset();
u = pm.mk_polynomial(los[1]);
for (int i = 0; i < num_lo; ++i) {
polynomial_ref y(pm);
y = pm.mk_polynomial(los[i]);
lits.push_back(mk_gt(s, u*x - y));
}
for (int i = 0; i < num_hi; ++i) {
polynomial_ref y(pm);
y = pm.mk_polynomial(his[i]);
lits.push_back(mk_gt(s, y - u*x));
}
z = pm.mk_polynomial(_z);
lits.push_back(mk_eq(s, x - z));
TEST_ON_OFF();
}
#if 0
#endif
static void test_root_literal(nlsat::solver& s, nlsat::explain& ex, nlsat::var x, nlsat::atom::kind k, unsigned i, nlsat::poly* p) {
nlsat::scoped_literal_vector result(s);
ex.test_root_literal(k, x, 1, p, result);
nlsat::bool_var b = s.mk_root_atom(k, x, i, p);
s.display(std::cout, nlsat::literal(b, false));
s.display(std::cout << " ==> ", result.size(), result.c_ptr());
std::cout << "\n";
}
static bool satisfies_root(nlsat::solver& s, nlsat::atom::kind k, nlsat::poly* p) {
nlsat::pmanager & pm = s.pm();
anum_manager & am = s.am();
nlsat::assignment as(am);
s.get_rvalues(as);
polynomial_ref pr(p, pm);
switch (k) {
case nlsat::atom::ROOT_EQ: return am.eval_sign_at(pr, as) == 0;
case nlsat::atom::ROOT_LE: return am.eval_sign_at(pr, as) <= 0;
case nlsat::atom::ROOT_LT: return am.eval_sign_at(pr, as) < 0;
case nlsat::atom::ROOT_GE: return am.eval_sign_at(pr, as) >= 0;
case nlsat::atom::ROOT_GT: return am.eval_sign_at(pr, as) > 0;
default:
UNREACHABLE();
return false;
}
}
static void tst10() {
params_ref ps;
reslimit rlim;
nlsat::solver s(rlim, ps);
anum_manager & am = s.am();
nlsat::pmanager & pm = s.pm();
nlsat::assignment as(am);
nlsat::explain& ex = s.get_explain();
nlsat::var _a = s.mk_var(false);
nlsat::var _b = s.mk_var(false);
nlsat::var _c = s.mk_var(false);
nlsat::var _x = s.mk_var(false);
polynomial_ref x(pm), a(pm), b(pm), c(pm), p(pm);
x = pm.mk_polynomial(_x);
a = pm.mk_polynomial(_a);
b = pm.mk_polynomial(_b);
c = pm.mk_polynomial(_c);
p = a*x*x + b*x + c;
scoped_anum one(am), two(am), three(am), mone(am), mtwo(am), mthree(am), zero(am), one_a_half(am);
am.set(zero, 0);
am.set(one, 1);
am.set(two, 2);
am.set(three, 3);
am.set(mone, -1);
am.set(mtwo, -2);
am.set(mthree, -3);
rational oah(1,2);
am.set(one_a_half, oah.to_mpq());
scoped_anum_vector nums(am);
nums.push_back(one);
nums.push_back(two);
nums.push_back(one_a_half);
nums.push_back(mone);
nums.push_back(three);
// a = 1, b = -3, c = 2:
// has roots x = 2, x = 1:
// 2^2 - 3*2 + 2 = 0
// 1 - 3 + 2 = 0
as.set(_a, one);
as.set(_b, mthree);
as.set(_c, two);
for (unsigned i = 0; i < nums.size(); ++i) {
as.set(_x, nums[i]);
s.set_rvalues(as);
std::cout << p << "\n";
as.display(std::cout);
for (unsigned k = nlsat::atom::ROOT_EQ; k <= nlsat::atom::ROOT_GE; ++k) {
if (satisfies_root(s, (nlsat::atom::kind) k, p)) {
test_root_literal(s, ex, _x, (nlsat::atom::kind) k, 1, p);
}
}
}
as.set(_a, mone);
as.set(_b, three);
as.set(_c, mtwo);
for (unsigned i = 0; i < nums.size(); ++i) {
as.set(_x, nums[i]);
s.set_rvalues(as);
std::cout << p << "\n";
as.display(std::cout);
for (unsigned k = nlsat::atom::ROOT_EQ; k <= nlsat::atom::ROOT_GE; ++k) {
if (satisfies_root(s, (nlsat::atom::kind) k, p)) {
test_root_literal(s, ex, _x, (nlsat::atom::kind) k, 1, p);
}
}
}
std::cout << "\n";
}
void tst_nlsat() {
tst10();
std::cout << "------------------\n";
exit(0);
tst9();
std::cout << "------------------\n";
exit(0);
tst8();
std::cout << "------------------\n";
tst7();
std::cout << "------------------\n";
tst6();
std::cout << "------------------\n";
tst5();
std::cout << "------------------\n";
tst4();
std::cout << "------------------\n";
tst3();
}

207
src/test/qe_arith.cpp
View file

@ -12,9 +12,9 @@ Copyright (c) 2015 Microsoft Corporation
#include "reg_decl_plugins.h"
#include "arith_rewriter.h"
#include "ast_pp.h"
#include "qe_util.h"
#include "smt_context.h"
#include "expr_abstract.h"
#include "expr_safe_replace.h"
static expr_ref parse_fml(ast_manager& m, char const* str) {
expr_ref result(m);
@ -29,6 +29,11 @@ static expr_ref parse_fml(ast_manager& m, char const* str) {
<< "(declare-const t Real)\n"
<< "(declare-const a Real)\n"
<< "(declare-const b Real)\n"
<< "(declare-const i Int)\n"
<< "(declare-const j Int)\n"
<< "(declare-const k Int)\n"
<< "(declare-const l Int)\n"
<< "(declare-const m Int)\n"
<< "(assert " << str << ")\n";
std::istringstream is(buffer.str());
VERIFY(parse_smt2_commands(ctx, is));
@ -42,6 +47,8 @@ static char const* example2 = "(and (<= z x) (<= x 3.0) (<= (* 3.0 x) y) (<= z y
static char const* example3 = "(and (<= z x) (<= x 3.0) (< (* 3.0 x) y) (<= z y))";
static char const* example4 = "(and (<= z x) (<= x 3.0) (not (>= (* 3.0 x) y)) (<= z y))";
static char const* example5 = "(and (<= y x) (<= z x) (<= x u) (<= x v) (<= x t))";
static char const* example7 = "(and (<= x y) (<= x z) (<= u x) (< v x))";
static char const* example8 = "(and (<= (* 2 i) k) (<= j (* 3 i)))";
static char const* example6 = "(and (<= 0 (+ x z))\
(>= y x) \
@ -51,30 +58,175 @@ static char const* example6 = "(and (<= 0 (+ x z))\
(>= x 0.0)\
(<= x 1.0))";
// phi[M] => result => E x . phi[x]
static void test(char const *ex) {
static void test(app* var, expr_ref& fml) {
ast_manager& m = fml.get_manager();
smt_params params;
params.m_model = true;
symbol x_name(var->get_decl()->get_name());
sort* x_sort = m.get_sort(var);
expr_ref pr(m);
expr_ref_vector lits(m);
flatten_and(fml, lits);
model_ref md;
{
smt::context ctx(m, params);
ctx.assert_expr(fml);
lbool result = ctx.check();
if (result != l_true) return;
ctx.get_model(md);
}
VERIFY(qe::arith_project(*md, var, lits));
pr = mk_and(lits);
std::cout << "original: " << mk_pp(fml, m) << "\n";
std::cout << "projected: " << mk_pp(pr, m) << "\n";
// projection is consistent with model.
expr_ref tmp(m);
VERIFY(md->eval(pr, tmp) && m.is_true(tmp));
// projection implies E x. fml
{
qe::expr_quant_elim qelim(m, params);
expr_ref result(m), efml(m);
expr* x = var;
expr_abstract(m, 0, 1, &x, fml, efml);
efml = m.mk_exists(1, &x_sort, &x_name, efml);
qelim(m.mk_true(), efml, result);
smt::context ctx(m, params);
ctx.assert_expr(pr);
ctx.assert_expr(m.mk_not(result));
std::cout << "exists: " << pr << " =>\n" << result << "\n";
VERIFY(l_false == ctx.check());
}
std::cout << "\n";
}
static void testR(char const *ex) {
ast_manager m;
reg_decl_plugins(m);
arith_util a(m);
expr_ref fml = parse_fml(m, ex);
app_ref_vector vars(m);
expr_ref_vector lits(m);
vars.push_back(m.mk_const(symbol("x"), a.mk_real()));
flatten_and(fml, lits);
symbol x_name("x");
sort_ref x_sort(a.mk_real(), m);
app_ref var(m.mk_const(x_name, x_sort), m);
test(var, fml);
}
smt::context ctx(m, params);
ctx.assert_expr(fml);
lbool result = ctx.check();
SASSERT(result == l_true);
ref<model> md;
ctx.get_model(md);
expr_ref pr = qe::arith_project(*md, vars, lits);
std::cout << mk_pp(fml, m) << "\n";
std::cout << mk_pp(pr, m) << "\n";
static void testI(char const *ex) {
ast_manager m;
reg_decl_plugins(m);
arith_util a(m);
expr_ref fml = parse_fml(m, ex);
symbol x_name("i");
sort_ref x_sort(a.mk_int(), m);
app_ref var(m.mk_const(x_name, x_sort), m);
test(var, fml);
}
static expr_ref_vector mk_ineqs(app* x, app* y, app_ref_vector const& nums) {
ast_manager& m = nums.get_manager();
arith_util a(m);
expr_ref_vector result(m);
for (unsigned i = 0; i < nums.size(); ++i) {
expr_ref ax(a.mk_mul(nums[i], x), m);
result.push_back(a.mk_le(ax, y));
result.push_back(m.mk_not(a.mk_ge(ax, y)));
result.push_back(m.mk_not(a.mk_gt(y, ax)));
result.push_back(a.mk_lt(y, ax));
}
return result;
}
static app_ref generate_ineqs(ast_manager& m, sort* s, vector<expr_ref_vector>& cs, bool mods_too) {
arith_util a(m);
app_ref_vector vars(m), nums(m);
vars.push_back(m.mk_const(symbol("x"), s));
vars.push_back(m.mk_const(symbol("y"), s));
vars.push_back(m.mk_const(symbol("z"), s));
vars.push_back(m.mk_const(symbol("u"), s));
vars.push_back(m.mk_const(symbol("v"), s));
vars.push_back(m.mk_const(symbol("w"), s));
nums.push_back(a.mk_numeral(rational(1), s));
nums.push_back(a.mk_numeral(rational(2), s));
nums.push_back(a.mk_numeral(rational(3), s));
app* x = vars[0].get();
app* y = vars[1].get();
app* z = vars[2].get();
//
// ax <= by, ax < by, not (ax >= by), not (ax > by)
//
cs.push_back(mk_ineqs(x, vars[1].get(), nums));
cs.push_back(mk_ineqs(x, vars[2].get(), nums));
cs.push_back(mk_ineqs(x, vars[3].get(), nums));
cs.push_back(mk_ineqs(x, vars[4].get(), nums));
cs.push_back(mk_ineqs(x, vars[5].get(), nums));
if (mods_too) {
expr_ref_vector mods(m);
expr_ref zero(a.mk_numeral(rational(0), s), m);
mods.push_back(m.mk_true());
for (unsigned j = 0; j < nums.size(); ++j) {
mods.push_back(m.mk_eq(a.mk_mod(a.mk_add(a.mk_mul(nums[j].get(),x), y), nums[1].get()), zero));
}
cs.push_back(mods);
mods.resize(1);
for (unsigned j = 0; j < nums.size(); ++j) {
mods.push_back(m.mk_eq(a.mk_mod(a.mk_add(a.mk_mul(nums[j].get(),x), y), nums[2].get()), zero));
}
cs.push_back(mods);
}
return app_ref(x, m);
}
static void test_c(app* x, expr_ref_vector const& c) {
ast_manager& m = c.get_manager();
expr_ref fml(m);
fml = m.mk_and(c.size(), c.c_ptr());
test(x, fml);
}
static void test_cs(app* x, expr_ref_vector& c, vector<expr_ref_vector> const& cs) {
if (c.size() == cs.size()) {
test_c(x, c);
return;
}
expr_ref_vector const& c1 = cs[c.size()];
for (unsigned i = 0; i < c1.size(); ++i) {
c.push_back(c1[i]);
test_cs(x, c, cs);
c.pop_back();
}
}
static void test_ineqs(ast_manager& m, sort* s, bool mods_too) {
vector<expr_ref_vector> ineqs;
app_ref x = generate_ineqs(m, s, ineqs, mods_too);
expr_ref_vector cs(m);
test_cs(x, cs, ineqs);
}
static void test_ineqs() {
ast_manager m;
reg_decl_plugins(m);
arith_util a(m);
sort* s_int = a.mk_int();
sort* s_real = a.mk_real();
test_ineqs(m, s_int, true);
test_ineqs(m, s_real, false);
}
static void test2(char const *ex) {
@ -102,7 +254,7 @@ static void test2(char const *ex) {
std::cout << mk_pp(fml, m) << "\n";
expr_ref pr2(m), fml2(m);
expr_ref pr1(m), pr2(m), fml2(m);
expr_ref_vector bound(m);
ptr_vector<sort> sorts;
svector<symbol> names;
@ -114,7 +266,10 @@ static void test2(char const *ex) {
expr_abstract(m, 0, bound.size(), bound.c_ptr(), fml, fml2);
fml2 = m.mk_exists(bound.size(), sorts.c_ptr(), names.c_ptr(), fml2);
qe::expr_quant_elim qe(m, params);
expr_ref pr1 = qe::arith_project(*md, vars, lits);
for (unsigned i = 0; i < vars.size(); ++i) {
VERIFY(qe::arith_project(*md, vars[i].get(), lits));
}
pr1 = mk_and(lits);
qe(m.mk_true(), fml2, pr2);
std::cout << mk_pp(pr1, m) << "\n";
std::cout << mk_pp(pr2, m) << "\n";
@ -131,11 +286,17 @@ static void test2(char const *ex) {
}
void tst_qe_arith() {
// enable_trace("qe");
testI(example8);
testR(example7);
test_ineqs();
return;
testR(example1);
testR(example2);
testR(example3);
testR(example4);
testR(example5);
return;
test2(example6);
return;
test(example1);
test(example2);
test(example3);
test(example4);
test(example5);
}