diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt
index 59834ea13..921cace75 100644
--- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt
+++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt
@@ -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
diff --git a/contrib/cmake/src/qe/CMakeLists.txt b/contrib/cmake/src/qe/CMakeLists.txt
index b20854de1..b197183dc 100644
--- a/contrib/cmake/src/qe/CMakeLists.txt
+++ b/contrib/cmake/src/qe/CMakeLists.txt
@@ -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
)
diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 3e476b99e..e7177000f 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -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')
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 05085a3d7..fad4ca7a2 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -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;
}
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 2cd50c181..211b6777e 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -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.
diff --git a/src/ast/rewriter/label_rewriter.cpp b/src/ast/rewriter/label_rewriter.cpp
new file mode 100644
index 000000000..3017f413c
--- /dev/null
+++ b/src/ast/rewriter/label_rewriter.cpp
@@ -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>;
diff --git a/src/ast/rewriter/label_rewriter.h b/src/ast/rewriter/label_rewriter.h
new file mode 100644
index 000000000..6400aa442
--- /dev/null
+++ b/src/ast/rewriter/label_rewriter.h
@@ -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
diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 693391bef..56cc6e154 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -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>;
diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h
index 2261a7a00..f7dc18b5e 100644
--- a/src/muz/base/dl_rule.h
+++ b/src/muz/base/dl_rule.h
@@ -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;
diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp
index 92c5634a1..db18d8854 100644
--- a/src/nlsat/nlsat_evaluator.cpp
+++ b/src/nlsat/nlsat_evaluator.cpp
@@ -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() {
diff --git a/src/nlsat/nlsat_evaluator.h b/src/nlsat/nlsat_evaluator.h
index 0762c5360..a82ce79fb 100644
--- a/src/nlsat/nlsat_evaluator.h
+++ b/src/nlsat/nlsat_evaluator.h
@@ -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;
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 4b87f9e65..23480eed4 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -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
+
diff --git a/src/nlsat/nlsat_explain.h b/src/nlsat/nlsat_explain.h
index ac99b434c..4309a0090 100644
--- a/src/nlsat/nlsat_explain.h
+++ b/src/nlsat/nlsat_explain.h
@@ -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);
};
};
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index c723d9961..40177bb08 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -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;
}
diff --git a/src/nlsat/nlsat_solver.h b/src/nlsat/nlsat_solver.h
index 2875bbc8c..eec5ba19f 100644
--- a/src/nlsat/nlsat_solver.h
+++ b/src/nlsat/nlsat_solver.h
@@ -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
*/
diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp
new file mode 100644
index 000000000..7318ba06a
--- /dev/null
+++ b/src/qe/nlqsat.cpp
@@ -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);
+}
+
+
diff --git a/src/qe/nlqsat.h b/src/qe/nlqsat.h
new file mode 100644
index 000000000..9d0cb6af4
--- /dev/null
+++ b/src/qe/nlqsat.h
@@ -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
diff --git a/src/qe/qe_util.cpp b/src/qe/qe_util.cpp
deleted file mode 100644
index 2bcda608f..000000000
--- a/src/qe/qe_util.cpp
+++ /dev/null
@@ -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;
- }
-
-}
diff --git a/src/qe/qe_util.h b/src/qe/qe_util.h
deleted file mode 100644
index ea082d78c..000000000
--- a/src/qe/qe_util.h
+++ /dev/null
@@ -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
diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
new file mode 100644
index 000000000..75cf57fa3
--- /dev/null
+++ b/src/qe/qsat.cpp
@@ -0,0 +1,1176 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+ qsat.cpp
+
+Abstract:
+
+ Quantifier Satisfiability Solver.
+
+Author:
+
+ Nikolaj Bjorner (nbjorner) 2015-5-28
+
+Revision History:
+
+Notes:
+
+
+--*/
+
+#include "smt_kernel.h"
+#include "qe_mbp.h"
+#include "smt_params.h"
+#include "ast_util.h"
+#include "quant_hoist.h"
+#include "ast_pp.h"
+#include "model_v2_pp.h"
+#include "qsat.h"
+#include "expr_abstract.h"
+#include "qe.h"
+#include "label_rewriter.h"
+
+
+namespace qe {
+
+ pred_abs::pred_abs(ast_manager& m):
+ m(m),
+ m_asms(m),
+ m_trail(m),
+ m_fmc(alloc(filter_model_converter, m))
+ {
+ }
+
+ filter_model_converter* pred_abs::fmc() {
+ return m_fmc.get();
+ }
+
+ void pred_abs::reset() {
+ m_trail.reset();
+ dec_keys<expr>(m_pred2lit);
+ dec_keys<app>(m_lit2pred);
+ dec_keys<app>(m_asm2pred);
+ dec_keys<expr>(m_pred2asm);
+ m_lit2pred.reset();
+ m_pred2lit.reset();
+ m_asm2pred.reset();
+ m_pred2asm.reset();
+ m_elevel.reset();
+ m_asms.reset();
+ m_asms_lim.reset();
+ m_preds.reset();
+ }
+
+ max_level pred_abs::compute_level(app* e) {
+ unsigned sz0 = todo.size();
+ todo.push_back(e);
+ while (sz0 != todo.size()) {
+ app* a = to_app(todo.back());
+ if (m_elevel.contains(a)) {
+ todo.pop_back();
+ continue;
+ }
+ max_level lvl, lvl0;
+ bool has_new = false;
+ if (m_flevel.find(a->get_decl(), lvl)) {
+ lvl0.merge(lvl);
+ }
+ for (unsigned i = 0; i < a->get_num_args(); ++i) {
+ app* arg = to_app(a->get_arg(i));
+ if (m_elevel.find(arg, lvl)) {
+ lvl0.merge(lvl);
+ }
+ else {
+ todo.push_back(arg);
+ has_new = true;
+ }
+ }
+ if (!has_new) {
+ m_elevel.insert(a, lvl0);
+ todo.pop_back();
+ }
+ }
+ return m_elevel.find(e);
+ }
+
+ void pred_abs::add_pred(app* p, app* lit) {
+ m.inc_ref(p);
+ m_pred2lit.insert(p, lit);
+ add_lit(p, lit);
+ }
+
+ void pred_abs::add_lit(app* p, app* lit) {
+ if (!m_lit2pred.contains(lit)) {
+ m.inc_ref(lit);
+ m_lit2pred.insert(lit, p);
+ }
+ }
+
+ void pred_abs::add_asm(app* p, expr* assum) {
+ SASSERT(!m_asm2pred.contains(assum));
+ m.inc_ref(p);
+ m.inc_ref(assum);
+ m_asm2pred.insert(assum, p);
+ m_pred2asm.insert(p, assum);
+ }
+
+ void pred_abs::push() {
+ m_asms_lim.push_back(m_asms.size());
+ }
+
+ void pred_abs::pop(unsigned num_scopes) {
+ unsigned l = m_asms_lim.size() - num_scopes;
+ m_asms.resize(m_asms_lim[l]);
+ m_asms_lim.shrink(l);
+ }
+
+ void pred_abs::insert(app* a, max_level const& lvl) {
+ unsigned l = lvl.max();
+ if (l == UINT_MAX) l = 0;
+ while (m_preds.size() <= l) {
+ m_preds.push_back(app_ref_vector(m));
+ }
+ m_preds[l].push_back(a);
+ }
+
+ bool pred_abs::is_predicate(app* a, unsigned l) {
+ max_level lvl1;
+ return m_flevel.find(a->get_decl(), lvl1) && lvl1.max() < l;
+ }
+
+ void pred_abs::get_assumptions(model* mdl, expr_ref_vector& asms) {
+ unsigned level = m_asms_lim.size();
+ if (level > m_preds.size()) {
+ level = m_preds.size();
+ }
+ if (!mdl) {
+ asms.append(m_asms);
+ return;
+ }
+ if (level == 0) {
+ return;
+ }
+ expr_ref val(m);
+ for (unsigned j = 0; j < m_preds[level - 1].size(); ++j) {
+ app* p = m_preds[level - 1][j].get();
+ TRACE("qe", tout << "process level: " << level - 1 << ": " << mk_pp(p, m) << "\n";);
+
+ VERIFY(mdl->eval(p, val));
+
+ if (m.is_false(val)) {
+ m_asms.push_back(m.mk_not(p));
+ }
+ else {
+ SASSERT(m.is_true(val));
+ m_asms.push_back(p);
+ }
+ }
+ asms.append(m_asms);
+
+ for (unsigned i = level + 1; i < m_preds.size(); i += 2) {
+ for (unsigned j = 0; j < m_preds[i].size(); ++j) {
+ app* p = m_preds[i][j].get();
+ max_level lvl = m_elevel.find(p);
+ bool use =
+ (lvl.m_fa == i && (lvl.m_ex == UINT_MAX || lvl.m_ex < level)) ||
+ (lvl.m_ex == i && (lvl.m_fa == UINT_MAX || lvl.m_fa < level));
+ if (use) {
+ VERIFY(mdl->eval(p, val));
+ if (m.is_false(val)) {
+ asms.push_back(m.mk_not(p));
+ }
+ else {
+ asms.push_back(p);
+ }
+ }
+ }
+ }
+ TRACE("qe", tout << "level: " << level << "\n";
+ model_v2_pp(tout, *mdl);
+ display(tout, asms););
+ }
+
+ void pred_abs::set_expr_level(app* v, max_level const& lvl) {
+ m_elevel.insert(v, lvl);
+ }
+
+ void pred_abs::set_decl_level(func_decl* f, max_level const& lvl) {
+ m_flevel.insert(f, lvl);
+ }
+
+ void pred_abs::abstract_atoms(expr* fml, expr_ref_vector& defs) {
+ max_level level;
+ abstract_atoms(fml, level, defs);
+ }
+ /**
+ \brief create propositional abstraction of formula by replacing atomic sub-formulas by fresh
+ propositional variables, and adding definitions for each propositional formula on the side.
+ Assumption is that the formula is quantifier-free.
+ */
+ void pred_abs::abstract_atoms(expr* fml, max_level& level, expr_ref_vector& defs) {
+ expr_mark mark;
+ ptr_vector<expr> args;
+ app_ref r(m), eq(m);
+ app* p;
+ unsigned sz0 = todo.size();
+ todo.push_back(fml);
+ m_trail.push_back(fml);
+ max_level l;
+ while (sz0 != todo.size()) {
+ app* a = to_app(todo.back());
+ todo.pop_back();
+ if (mark.is_marked(a)) {
+ continue;
+ }
+
+ mark.mark(a);
+ if (m_lit2pred.find(a, p)) {
+ TRACE("qe", tout << mk_pp(a, m) << " " << mk_pp(p, m) << "\n";);
+ level.merge(m_elevel.find(p));
+ continue;
+ }
+
+ if (is_uninterp_const(a) && m.is_bool(a)) {
+ l = m_elevel.find(a);
+ level.merge(l);
+ if (!m_pred2lit.contains(a)) {
+ add_pred(a, a);
+ insert(a, l);
+ }
+ continue;
+ }
+
+ unsigned sz = a->get_num_args();
+ for (unsigned i = 0; i < sz; ++i) {
+ expr* f = a->get_arg(i);
+ if (!mark.is_marked(f)) {
+ todo.push_back(f);
+ }
+ }
+
+ bool is_boolop =
+ (a->get_family_id() == m.get_basic_family_id()) &&
+ (!m.is_eq(a) || m.is_bool(a->get_arg(0))) &&
+ (!m.is_distinct(a) || m.is_bool(a->get_arg(0)));
+
+ if (!is_boolop && m.is_bool(a)) {
+ TRACE("qe", tout << mk_pp(a, m) << "\n";);
+ r = fresh_bool("p");
+ max_level l = compute_level(a);
+ add_pred(r, a);
+ m_elevel.insert(r, l);
+ eq = m.mk_eq(r, a);
+ defs.push_back(eq);
+ if (!is_predicate(a, l.max())) {
+ insert(r, l);
+ }
+ level.merge(l);
+ }
+ }
+ }
+
+ app_ref pred_abs::fresh_bool(char const* name) {
+ app_ref r(m.mk_fresh_const(name, m.mk_bool_sort()), m);
+ m_fmc->insert(r->get_decl());
+ return r;
+ }
+
+
+ // optional pass to replace atoms by predicates
+ // so that SMT core works on propositional
+ // abstraction only.
+ expr_ref pred_abs::mk_abstract(expr* fml) {
+ expr_ref_vector trail(m), args(m);
+ obj_map<expr, expr*> cache;
+ app* b;
+ expr_ref r(m);
+ unsigned sz0 = todo.size();
+ todo.push_back(fml);
+ while (sz0 != todo.size()) {
+ app* a = to_app(todo.back());
+ if (cache.contains(a)) {
+ todo.pop_back();
+ continue;
+ }
+ if (m_lit2pred.find(a, b)) {
+ cache.insert(a, b);
+ todo.pop_back();
+ continue;
+ }
+ unsigned sz = a->get_num_args();
+ bool diff = false;
+ args.reset();
+ for (unsigned i = 0; i < sz; ++i) {
+ expr* f = a->get_arg(i), *f1;
+ if (cache.find(f, f1)) {
+ args.push_back(f1);
+ diff |= f != f1;
+ }
+ else {
+ todo.push_back(f);
+ }
+ }
+ if (sz == args.size()) {
+ if (diff) {
+ r = m.mk_app(a->get_decl(), sz, args.c_ptr());
+ trail.push_back(r);
+ }
+ else {
+ r = a;
+ }
+ cache.insert(a, r);
+ todo.pop_back();
+ }
+ }
+ return expr_ref(cache.find(fml), m);
+ }
+
+ expr_ref pred_abs::mk_assumption_literal(expr* a, model* mdl, max_level const& lvl, expr_ref_vector& defs) {
+ expr_ref A(m);
+ A = pred2asm(a);
+ a = A;
+ app_ref p(m);
+ expr_ref q(m), fml(m);
+ app *b;
+ expr *c, *d;
+ max_level lvl2;
+ TRACE("qe", tout << mk_pp(a, m) << " " << lvl << "\n";);
+ if (m_asm2pred.find(a, b)) {
+ q = b;
+ }
+ else if (m.is_not(a, c) && m_asm2pred.find(c, b)) {
+ q = m.mk_not(b);
+ }
+ else if (m_pred2asm.find(a, d)) {
+ q = a;
+ }
+ else if (m.is_not(a, c) && m_pred2asm.find(c, d)) {
+ q = a;
+ }
+ else {
+ p = fresh_bool("def");
+ if (m.is_not(a, a)) {
+ if (mdl)
+ mdl->register_decl(p->get_decl(), m.mk_false());
+ q = m.mk_not(p);
+ }
+ else {
+ if (mdl)
+ mdl->register_decl(p->get_decl(), m.mk_true());
+ q = p;
+ }
+ m_elevel.insert(p, lvl);
+ insert(p, lvl);
+ fml = a;
+ abstract_atoms(fml, lvl2, defs);
+ fml = mk_abstract(fml);
+ defs.push_back(m.mk_eq(p, fml));
+ add_asm(p, a);
+ TRACE("qe", tout << mk_pp(a, m) << " |-> " << p << "\n";);
+ }
+ return q;
+ }
+
+ void pred_abs::mk_concrete(expr_ref_vector& fmls, obj_map<expr,expr*> const& map) {
+ obj_map<expr,expr*> cache;
+ expr_ref_vector trail(m);
+ expr* p;
+ app_ref r(m);
+ ptr_vector<expr> args;
+ unsigned sz0 = todo.size();
+ todo.append(fmls.size(), (expr*const*)fmls.c_ptr());
+ while (sz0 != todo.size()) {
+ app* a = to_app(todo.back());
+ if (cache.contains(a)) {
+ todo.pop_back();
+ continue;
+ }
+ if (map.find(a, p)) {
+ cache.insert(a, p);
+ todo.pop_back();
+ continue;
+ }
+ unsigned sz = a->get_num_args();
+ args.reset();
+ bool diff = false;
+ for (unsigned i = 0; i < sz; ++i) {
+ expr* f = a->get_arg(i), *f1;
+ if (cache.find(f, f1)) {
+ args.push_back(f1);
+ diff |= f != f1;
+ }
+ else {
+ todo.push_back(f);
+ }
+ }
+ if (args.size() == sz) {
+ if (diff) {
+ r = m.mk_app(a->get_decl(), sz, args.c_ptr());
+ }
+ else {
+ r = to_app(a);
+ }
+ cache.insert(a, r);
+ trail.push_back(r);
+ todo.pop_back();
+ }
+ }
+ for (unsigned i = 0; i < fmls.size(); ++i) {
+ fmls[i] = to_app(cache.find(fmls[i].get()));
+ }
+ }
+
+ void pred_abs::pred2lit(expr_ref_vector& fmls) {
+ mk_concrete(fmls, m_pred2lit);
+ }
+
+ expr_ref pred_abs::pred2asm(expr* fml) {
+ expr_ref_vector fmls(m);
+ fmls.push_back(fml);
+ mk_concrete(fmls, m_pred2asm);
+ return mk_and(fmls);
+ }
+
+ void pred_abs::collect_statistics(statistics& st) const {
+ st.update("qsat num predicates", m_pred2lit.size());
+ }
+
+ void pred_abs::display(std::ostream& out) const {
+ out << "pred2lit:\n";
+ obj_map<expr, expr*>::iterator it = m_pred2lit.begin(), end = m_pred2lit.end();
+ for (; it != end; ++it) {
+ out << mk_pp(it->m_key, m) << " |-> " << mk_pp(it->m_value, m) << "\n";
+ }
+ for (unsigned i = 0; i < m_preds.size(); ++i) {
+ out << "level " << i << "\n";
+ for (unsigned j = 0; j < m_preds[i].size(); ++j) {
+ app* p = m_preds[i][j];
+ expr* e;
+ if (m_pred2lit.find(p, e)) {
+ out << mk_pp(p, m) << " := " << mk_pp(e, m) << "\n";
+ }
+ else {
+ out << mk_pp(p, m) << "\n";
+ }
+ }
+ }
+ }
+
+ void pred_abs::display(std::ostream& out, expr_ref_vector const& asms) const {
+ max_level lvl;
+ for (unsigned i = 0; i < asms.size(); ++i) {
+ expr* e = asms[i];
+ bool is_not = m.is_not(asms[i], e);
+ out << mk_pp(asms[i], m);
+ if (m_elevel.find(e, lvl)) {
+ lvl.display(out << " - ");
+ }
+ if (m_pred2lit.find(e, e)) {
+ out << " : " << (is_not?"!":"") << mk_pp(e, m);
+ }
+ out << "\n";
+ }
+ }
+
+ void pred_abs::get_free_vars(expr* fml, app_ref_vector& vars) {
+ ast_fast_mark1 mark;
+ unsigned sz0 = todo.size();
+ todo.push_back(fml);
+ while (sz0 != todo.size()) {
+ expr* e = todo.back();
+ todo.pop_back();
+ if (mark.is_marked(e) || is_var(e)) {
+ continue;
+ }
+ mark.mark(e);
+ if (is_quantifier(e)) {
+ todo.push_back(to_quantifier(e)->get_expr());
+ continue;
+ }
+ SASSERT(is_app(e));
+ app* a = to_app(e);
+ if (is_uninterp_const(a)) { // TBD generalize for uninterpreted functions.
+ vars.push_back(a);
+ }
+ for (unsigned i = 0; i < a->get_num_args(); ++i) {
+ todo.push_back(a->get_arg(i));
+ }
+ }
+ }
+
+ class qsat : public tactic {
+
+ struct stats {
+ unsigned m_num_rounds;
+ stats() { reset(); }
+ void reset() { memset(this, 0, sizeof(*this)); }
+ };
+
+ class kernel {
+ ast_manager& m;
+ smt_params m_smtp;
+ smt::kernel m_kernel;
+
+ public:
+ kernel(ast_manager& m):
+ m(m),
+ m_kernel(m, m_smtp)
+ {
+ m_smtp.m_model = true;
+ m_smtp.m_relevancy_lvl = 0;
+ }
+
+ smt::kernel& k() { return m_kernel; }
+ smt::kernel const& k() const { return m_kernel; }
+
+ void assert_expr(expr* e) {
+ m_kernel.assert_expr(e);
+ }
+
+ void get_core(expr_ref_vector& core) {
+ unsigned sz = m_kernel.get_unsat_core_size();
+ core.reset();
+ for (unsigned i = 0; i < sz; ++i) {
+ core.push_back(m_kernel.get_unsat_core_expr(i));
+ }
+ TRACE("qe", tout << "core: " << core << "\n";
+ m_kernel.display(tout);
+ tout << "\n";
+ );
+ }
+ };
+
+ ast_manager& m;
+ params_ref m_params;
+ stats m_stats;
+ statistics m_st;
+ qe::mbp m_mbp;
+ kernel m_fa;
+ kernel m_ex;
+ pred_abs m_pred_abs;
+ expr_ref_vector m_answer;
+ expr_ref_vector m_asms;
+ vector<app_ref_vector> m_vars; // variables from alternating prefixes.
+ unsigned m_level;
+ model_ref m_model;
+ bool m_qelim; // perform quantifier elimination
+ bool m_force_elim; // force elimination of variables during projection.
+ app_ref_vector m_avars; // variables to project
+ app_ref_vector m_free_vars;
+
+
+ /**
+ \brief check alternating satisfiability.
+ Even levels are existential, odd levels are universal.
+ */
+ lbool check_sat() {
+ while (true) {
+ ++m_stats.m_num_rounds;
+ check_cancel();
+ expr_ref_vector asms(m_asms);
+ m_pred_abs.get_assumptions(m_model.get(), asms);
+ TRACE("qe", tout << asms << "\n";);
+ smt::kernel& k = get_kernel(m_level).k();
+ lbool res = k.check(asms);
+ switch (res) {
+ case l_true:
+ k.get_model(m_model);
+ SASSERT(validate_model(asms));
+ TRACE("qe", k.display(tout); display(tout << "\n", *m_model.get()); display(tout, asms); );
+ push();
+ break;
+ case l_false:
+ switch (m_level) {
+ case 0: return l_false;
+ case 1:
+ if (!m_qelim) return l_true;
+ if (m_model.get()) {
+ project_qe(asms);
+ }
+ else {
+ pop(1);
+ }
+ break;
+ default:
+ if (m_model.get()) {
+ project(asms);
+ }
+ else {
+ pop(1);
+ }
+ break;
+ }
+ break;
+ case l_undef:
+ return res;
+ }
+ }
+ return l_undef;
+ }
+
+ kernel& get_kernel(unsigned j) {
+ if (is_exists(j)) {
+ return m_ex;
+ }
+ else {
+ return m_fa;
+ }
+ }
+
+ bool is_exists(unsigned level) const {
+ return (level % 2) == 0;
+ }
+
+ bool is_forall(unsigned level) const {
+ return is_exists(level+1);
+ }
+
+ void push() {
+ m_level++;
+ m_pred_abs.push();
+ }
+
+ void pop(unsigned num_scopes) {
+ m_model.reset();
+ SASSERT(num_scopes <= m_level);
+ m_pred_abs.pop(num_scopes);
+ m_level -= num_scopes;
+ }
+
+ void reset() {
+ m_st.reset();
+ m_fa.k().collect_statistics(m_st);
+ m_ex.k().collect_statistics(m_st);
+ m_pred_abs.collect_statistics(m_st);
+ m_level = 0;
+ m_answer.reset();
+ m_asms.reset();
+ m_pred_abs.reset();
+ m_vars.reset();
+ m_model = 0;
+ m_fa.k().reset();
+ m_ex.k().reset();
+ m_free_vars.reset();
+ }
+
+ /**
+ \brief create a quantifier prefix formula.
+ */
+ void hoist(expr_ref& fml) {
+ proof_ref pr(m);
+ label_rewriter rw(m);
+ rw.remove_labels(fml, pr);
+ quantifier_hoister hoist(m);
+ app_ref_vector vars(m);
+ bool is_forall = false;
+ m_pred_abs.get_free_vars(fml, vars);
+ m_vars.push_back(vars);
+ vars.reset();
+ if (m_qelim) {
+ is_forall = true;
+ hoist.pull_quantifier(is_forall, fml, vars);
+ m_vars.push_back(vars);
+ }
+ else {
+ hoist.pull_quantifier(is_forall, fml, vars);
+ m_vars.back().append(vars);
+ }
+ do {
+ is_forall = !is_forall;
+ vars.reset();
+ hoist.pull_quantifier(is_forall, fml, vars);
+ m_vars.push_back(vars);
+ }
+ while (!vars.empty());
+ SASSERT(m_vars.back().empty());
+ initialize_levels();
+ TRACE("qe", tout << fml << "\n";);
+ }
+
+ void initialize_levels() {
+ // initialize levels.
+ for (unsigned i = 0; i < m_vars.size(); ++i) {
+ max_level lvl;
+ if (is_exists(i)) {
+ lvl.m_ex = i;
+ }
+ else {
+ lvl.m_fa = i;
+ }
+ for (unsigned j = 0; j < m_vars[i].size(); ++j) {
+ m_pred_abs.set_expr_level(m_vars[i][j].get(), lvl);
+ }
+ }
+ }
+
+ void get_core(expr_ref_vector& core, unsigned level) {
+ get_kernel(level).get_core(core);
+ m_pred_abs.pred2lit(core);
+ }
+
+ void check_cancel() {
+ if (m.canceled()) {
+ throw tactic_exception(m.limit().get_cancel_msg());
+ }
+ }
+
+ void display(std::ostream& out) const {
+ out << "level: " << m_level << "\n";
+ for (unsigned i = 0; i < m_vars.size(); ++i) {
+ for (unsigned j = 0; j < m_vars[i].size(); ++j) {
+ expr* v = m_vars[i][j];
+ out << mk_pp(v, m) << " ";
+ }
+ out << "\n";
+ }
+ m_pred_abs.display(out);
+ }
+
+ void display(std::ostream& out, model& model) const {
+ display(out);
+ model_v2_pp(out, model);
+ }
+
+ void display(std::ostream& out, expr_ref_vector const& asms) const {
+ m_pred_abs.display(out, asms);
+ }
+
+ void add_assumption(expr* fml) {
+ expr_ref eq(m);
+ app_ref b = m_pred_abs.fresh_bool("b");
+ m_asms.push_back(b);
+ eq = m.mk_eq(b, fml);
+ m_ex.assert_expr(eq);
+ m_fa.assert_expr(eq);
+ m_pred_abs.add_pred(b, to_app(fml));
+ max_level lvl;
+ m_pred_abs.set_expr_level(b, lvl);
+ }
+
+ void project_qe(expr_ref_vector& core) {
+ SASSERT(m_level == 1);
+ expr_ref fml(m);
+ model& mdl = *m_model.get();
+ get_core(core, m_level);
+ SASSERT(validate_core(core));
+ get_vars(m_level);
+ m_mbp(m_force_elim, m_avars, mdl, core);
+ fml = negate_core(core);
+ add_assumption(fml);
+ m_answer.push_back(fml);
+ m_free_vars.append(m_avars);
+ pop(1);
+ }
+
+ void project(expr_ref_vector& core) {
+ get_core(core, m_level);
+ TRACE("qe", display(tout); display(tout << "core\n", core););
+ SASSERT(validate_core(core));
+ SASSERT(m_level >= 2);
+ expr_ref fml(m);
+ expr_ref_vector defs(m), core_save(m);
+ max_level level;
+ model& mdl = *m_model.get();
+
+ get_vars(m_level-1);
+ SASSERT(validate_project(mdl, core));
+ m_mbp(m_force_elim, m_avars, mdl, core);
+ m_free_vars.append(m_avars);
+ fml = negate_core(core);
+ unsigned num_scopes = 0;
+
+ m_pred_abs.abstract_atoms(fml, level, defs);
+ m_ex.assert_expr(mk_and(defs));
+ m_fa.assert_expr(mk_and(defs));
+ if (level.max() == UINT_MAX) {
+ num_scopes = 2*(m_level/2);
+ }
+ else if (m_qelim && !m_force_elim) {
+ num_scopes = 2;
+ }
+ else {
+ SASSERT(level.max() + 2 <= m_level);
+ num_scopes = m_level - level.max();
+ SASSERT(num_scopes >= 2);
+ if ((num_scopes % 2) != 0) {
+ --num_scopes;
+ }
+ }
+
+ pop(num_scopes);
+ TRACE("qe", tout << "backtrack: " << num_scopes << " new level: " << m_level << "\nproject:\n" << core << "\n|->\n" << fml << "\n";);
+ if (m_level == 0 && m_qelim) {
+ add_assumption(fml);
+ }
+ else {
+ fml = m_pred_abs.mk_abstract(fml);
+ get_kernel(m_level).assert_expr(fml);
+ }
+ }
+
+ void get_vars(unsigned level) {
+ m_avars.reset();
+ for (unsigned i = level; i < m_vars.size(); ++i) {
+ m_avars.append(m_vars[i]);
+ }
+ }
+
+ expr_ref negate_core(expr_ref_vector& core) {
+ return ::push_not(::mk_and(core));
+ }
+
+ expr_ref elim_rec(expr* fml) {
+ expr_ref tmp(m);
+ expr_ref_vector trail(m);
+ obj_map<expr,expr*> visited;
+ ptr_vector<expr> todo;
+ trail.push_back(fml);
+ todo.push_back(fml);
+ expr* e = 0, *r = 0;
+
+ while (!todo.empty()) {
+ check_cancel();
+
+ e = todo.back();
+ if (visited.contains(e)) {
+ todo.pop_back();
+ continue;
+ }
+
+ switch(e->get_kind()) {
+ case AST_APP: {
+ app* a = to_app(e);
+ expr_ref_vector args(m);
+ unsigned num_args = a->get_num_args();
+ bool all_visited = true;
+ for (unsigned i = 0; i < num_args; ++i) {
+ if (visited.find(a->get_arg(i), r)) {
+ args.push_back(r);
+ }
+ else {
+ todo.push_back(a->get_arg(i));
+ all_visited = false;
+ }
+ }
+ if (all_visited) {
+ r = m.mk_app(a->get_decl(), args.size(), args.c_ptr());
+ todo.pop_back();
+ trail.push_back(r);
+ visited.insert(e, r);
+ }
+ break;
+ }
+ case AST_QUANTIFIER: {
+ app_ref_vector vars(m);
+ quantifier* q = to_quantifier(e);
+ bool is_fa = q->is_forall();
+ tmp = q->get_expr();
+ extract_vars(q, tmp, vars);
+ TRACE("qe", tout << vars << " " << mk_pp(q, m) << " " << tmp << "\n";);
+ tmp = elim_rec(tmp);
+ if (is_fa) {
+ tmp = ::push_not(tmp);
+ }
+ tmp = elim(vars, tmp);
+ if (is_fa) {
+ tmp = ::push_not(tmp);
+ }
+ trail.push_back(tmp);
+ visited.insert(e, tmp);
+ todo.pop_back();
+ break;
+ }
+ default:
+ UNREACHABLE();
+ break;
+ }
+ }
+ VERIFY (visited.find(fml, e));
+ return expr_ref(e, m);
+ }
+
+ expr_ref elim(app_ref_vector const& vars, expr* _fml) {
+ expr_ref fml(_fml, m);
+ reset();
+ m_vars.push_back(app_ref_vector(m));
+ m_vars.push_back(vars);
+ initialize_levels();
+ fml = push_not(fml);
+
+ TRACE("qe", tout << vars << " " << fml << "\n";);
+ expr_ref_vector defs(m);
+ m_pred_abs.abstract_atoms(fml, defs);
+ fml = m_pred_abs.mk_abstract(fml);
+ m_ex.assert_expr(mk_and(defs));
+ m_fa.assert_expr(mk_and(defs));
+ m_ex.assert_expr(fml);
+ m_fa.assert_expr(m.mk_not(fml));
+ TRACE("qe", tout << "ex: " << fml << "\n";);
+ lbool is_sat = check_sat();
+ fml = ::mk_and(m_answer);
+ TRACE("qe", tout << "ans: " << fml << "\n";
+ tout << "Free vars: " << m_free_vars << "\n";);
+ if (is_sat == l_false) {
+ obj_hashtable<app> vars;
+ for (unsigned i = 0; i < m_free_vars.size(); ++i) {
+ app* v = m_free_vars[i].get();
+ if (vars.contains(v)) {
+ m_free_vars[i] = m_free_vars.back();
+ m_free_vars.pop_back();
+ --i;
+ }
+ else {
+ vars.insert(v);
+ }
+ }
+ fml = mk_exists(m, m_free_vars.size(), m_free_vars.c_ptr(), fml);
+ return fml;
+ }
+ else {
+ return expr_ref(_fml, m);
+ }
+ }
+
+ bool validate_core(expr_ref_vector const& core) {
+ TRACE("qe", tout << "Validate core\n";);
+ smt::kernel& k = get_kernel(m_level).k();
+ expr_ref_vector fmls(m);
+ fmls.append(core.size(), core.c_ptr());
+ fmls.append(k.size(), k.get_formulas());
+ return check_fmls(fmls);
+ }
+
+ bool check_fmls(expr_ref_vector const& fmls) {
+ smt_params p;
+ smt::kernel solver(m, p);
+ for (unsigned i = 0; i < fmls.size(); ++i) {
+ solver.assert_expr(fmls[i]);
+ }
+ lbool is_sat = solver.check();
+ CTRACE("qe", is_sat != l_false,
+ tout << fmls << "\nare not unsat\n";);
+ return (is_sat == l_false);
+ }
+
+ bool validate_model(expr_ref_vector const& asms) {
+ TRACE("qe", tout << "Validate model\n";);
+ smt::kernel& k = get_kernel(m_level).k();
+ return
+ validate_model(*m_model, asms.size(), asms.c_ptr()) &&
+ validate_model(*m_model, k.size(), k.get_formulas());
+ }
+
+ bool validate_model(model& mdl, unsigned sz, expr* const* fmls) {
+ expr_ref val(m);
+ for (unsigned i = 0; i < sz; ++i) {
+ if (!m_model->eval(fmls[i], val)) {
+ TRACE("qe", tout << "Formula does not evaluate in model: " << mk_pp(fmls[i], m) << "\n";);
+ return false;
+ }
+ if (!m.is_true(val)) {
+ TRACE("qe", tout << mk_pp(fmls[i], m) << " evaluates to " << val << " in model\n";);
+ return false;
+ }
+ }
+ return true;
+ }
+
+ // validate the following:
+ // proj is true in model.
+ // core is true in model.
+ // proj does not contain vars.
+ // proj => exists vars . core
+ // (core[model(vars)/vars] => proj)
+
+ bool validate_project(model& mdl, expr_ref_vector const& core) {
+ TRACE("qe", tout << "Validate projection\n";);
+ if (!validate_model(mdl, core.size(), core.c_ptr())) return false;
+
+ expr_ref_vector proj(core);
+ app_ref_vector vars(m_avars);
+ m_mbp(false, vars, mdl, proj);
+ if (!vars.empty()) {
+ TRACE("qe", tout << "Not validating partial projection\n";);
+ return true;
+ }
+ if (!validate_model(mdl, proj.size(), proj.c_ptr())) {
+ TRACE("qe", tout << "Projection is false in model\n";);
+ return false;
+ }
+ for (unsigned i = 0; i < m_avars.size(); ++i) {
+ contains_app cont(m, m_avars[i].get());
+ if (cont(proj)) {
+ TRACE("qe", tout << "Projection contains free variable: " << mk_pp(m_avars[i].get(), m) << "\n";);
+ return false;
+ }
+ }
+
+ //
+ // TBD: proj => exists vars . core,
+ // e.g., extract and use realizer functions from mbp.
+ //
+
+ // (core[model(vars)/vars] => proj)
+ expr_ref_vector fmls(m);
+ fmls.append(core.size(), core.c_ptr());
+ for (unsigned i = 0; i < m_avars.size(); ++i) {
+ expr_ref val(m);
+ VERIFY(mdl.eval(m_avars[i].get(), val));
+ fmls.push_back(m.mk_eq(m_avars[i].get(), val));
+ }
+ fmls.push_back(m.mk_not(mk_and(proj)));
+ if (!check_fmls(fmls)) {
+ TRACE("qe", tout << "implication check failed, could be due to turning != into >\n";);
+ }
+ return true;
+ }
+
+ public:
+
+ qsat(ast_manager& m, params_ref const& p, bool qelim, bool force_elim):
+ m(m),
+ m_mbp(m),
+ m_fa(m),
+ m_ex(m),
+ m_pred_abs(m),
+ m_answer(m),
+ m_asms(m),
+ m_level(0),
+ m_qelim(qelim),
+ m_force_elim(force_elim),
+ m_avars(m),
+ m_free_vars(m)
+ {
+ reset();
+ }
+
+ virtual ~qsat() {
+ reset();
+ }
+
+ void updt_params(params_ref const & p) {
+ }
+
+ 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("qsat-tactic", *in);
+ ptr_vector<expr> fmls;
+ expr_ref_vector defs(m);
+ expr_ref fml(m);
+ mc = 0; pc = 0; core = 0;
+ in->get_formulas(fmls);
+ fml = mk_and(m, fmls.size(), fmls.c_ptr());
+
+ // for now:
+ // fail if cores. (TBD)
+ // fail if proofs. (TBD)
+
+ if (!m_force_elim) {
+ fml = elim_rec(fml);
+ in->reset();
+ in->inc_depth();
+ in->assert_expr(fml);
+ result.push_back(in.get());
+ return;
+ }
+
+ reset();
+ TRACE("qe", tout << fml << "\n";);
+ if (m_qelim) {
+ fml = push_not(fml);
+ }
+ hoist(fml);
+ m_pred_abs.abstract_atoms(fml, defs);
+ fml = m_pred_abs.mk_abstract(fml);
+ m_ex.assert_expr(mk_and(defs));
+ m_fa.assert_expr(mk_and(defs));
+ m_ex.assert_expr(fml);
+ m_fa.assert_expr(m.mk_not(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_qelim) {
+ fml = ::mk_and(m_answer);
+ in->assert_expr(fml);
+ }
+ else {
+ in->assert_expr(m.mk_false());
+ }
+ result.push_back(in.get());
+ break;
+ case l_true:
+ in->reset();
+ in->inc_depth();
+ result.push_back(in.get());
+ if (in->models_enabled()) {
+ mc = model2model_converter(m_model.get());
+ mc = concat(m_pred_abs.fmc(), mc.get());
+ }
+ break;
+ case l_undef:
+ result.push_back(in.get());
+ std::string s = m_ex.k().last_failure_as_string();
+ if (s == "ok") {
+ s = m_fa.k().last_failure_as_string();
+ }
+ 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);
+ m_pred_abs.collect_statistics(st);
+ }
+
+ void reset_statistics() {
+ m_stats.reset();
+ m_fa.k().reset_statistics();
+ m_ex.k().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(qsat, m, m_params, m_qelim, m_force_elim);
+ }
+
+
+ };
+
+};
+
+tactic * mk_qsat_tactic(ast_manager& m, params_ref const& p) {
+ return alloc(qe::qsat, m, p, false, true);
+}
+
+tactic * mk_qe2_tactic(ast_manager& m, params_ref const& p) {
+ return alloc(qe::qsat, m, p, true, true);
+}
+
+tactic * mk_qe_rec_tactic(ast_manager& m, params_ref const& p) {
+ return alloc(qe::qsat, m, p, true, false);
+}
+
+
diff --git a/src/qe/qsat.h b/src/qe/qsat.h
new file mode 100644
index 000000000..ee9f9e6ad
--- /dev/null
+++ b/src/qe/qsat.h
@@ -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
diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp
index 7777a6c42..27a0aa1da 100644
--- a/src/test/nlsat.cpp
+++ b/src/test/nlsat.cpp
@@ -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();
}
diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index 40ecbd8c7..a1b5c2859 100644
--- a/src/test/qe_arith.cpp
+++ b/src/test/qe_arith.cpp
@@ -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);
}