mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 01:24:08 +00:00
Code Activity

add DDNF based engine

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-21 18:04:46 -07:00
parent 8822bc1755
commit b596828d23
11 changed files with 761 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
scripts/mk_project.py
View file

@ -66,8 +66,9 @@ def init_project_def():
add_lib('clp', ['muz', 'transforms'], 'muz/clp')
add_lib('tab', ['muz', 'transforms'], 'muz/tab')
add_lib('bmc', ['muz', 'transforms'], 'muz/bmc')
add_lib('ddnf', ['muz', 'transforms'], 'muz/ddnf')
add_lib('duality_intf', ['muz', 'transforms', 'duality'], 'muz/duality')
add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf'], 'muz/fp')
add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc', 'duality_intf', 'ddnf'], 'muz/fp')
add_lib('smtlogic_tactics', ['arith_tactics', 'bv_tactics', 'nlsat_tactic', 'smt_tactic', 'aig_tactic', 'fp', 'muz','qe'], 'tactic/smtlogics')
add_lib('ufbv_tactic', ['normal_forms', 'core_tactics', 'macros', 'smt_tactic', 'rewriter'], 'tactic/ufbv')
add_lib('portfolio', ['smtlogic_tactics', 'ufbv_tactic', 'fpa_tactics', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')

6
src/muz/base/dl_context.cpp
View file

@ -712,6 +712,8 @@ namespace datalog {
check_existential_tail(r);
check_positive_predicates(r);
break;
case DDNF_ENGINE:
break;
case LAST_ENGINE:
default:
UNREACHABLE();
@ -932,6 +934,9 @@ namespace datalog {
else if (e == symbol("duality")) {
m_engine_type = DUALITY_ENGINE;
}
else if (e == symbol("ddnf")) {
m_engine_type = DDNF_ENGINE;
}
if (m_engine_type == LAST_ENGINE) {
expr_fast_mark1 mark;
@ -980,6 +985,7 @@ namespace datalog {
case QBMC_ENGINE:
case TAB_ENGINE:
case CLP_ENGINE:
case DDNF_ENGINE:
flush_add_rules();
break;
case DUALITY_ENGINE:

5
src/muz/base/dl_engine_base.h
View file

@ -30,8 +30,9 @@ namespace datalog {
QBMC_ENGINE,
TAB_ENGINE,
CLP_ENGINE,
LAST_ENGINE,
DUALITY_ENGINE
DUALITY_ENGINE,
DDNF_ENGINE,
LAST_ENGINE
};
class engine_base {

620
src/muz/ddnf/ddnf.cpp Normal file
View file

@ -0,0 +1,620 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
ddnf.cpp
Abstract:
DDNF based engine.
Author:
Nikolaj Bjorner (nbjorner) 2014-08-21
Revision History:
- inherits from Nuno Lopes Hassel utilities
and Garvit Juniwal's DDNF engine.
--*/
#include "ddnf.h"
#include "trail.h"
#include "dl_rule_set.h"
#include "dl_context.h"
#include "dl_mk_rule_inliner.h"
#include "smt_kernel.h"
#include "qe_lite.h"
#include "bool_rewriter.h"
#include "th_rewriter.h"
#include "datatype_decl_plugin.h"
#include "for_each_expr.h"
#include "matcher.h"
#include "scoped_proof.h"
#include "fixedpoint_params.hpp"
namespace datalog {
#define BIT_0 ((0<<1)|1)
#define BIT_1 ((1<<1)|0)
#define BIT_x ((1<<1)|1)
#define BIT_z 0
class tbv : private bit_vector {
public:
tbv(): bit_vector() {}
tbv(unsigned n): bit_vector(2*n) {}
tbv(tbv const& other): bit_vector(other) {}
tbv(unsigned n, unsigned val): bit_vector() {
SASSERT(val <= 3);
resize(n, val);
}
tbv(uint64 val, unsigned n) : bit_vector(2*n) {
for (unsigned bit = n; bit > 0;) {
--bit;
if (val & (1ULL << bit)) {
set(bit, BIT_1);
} else {
set(bit, BIT_0);
}
}
}
tbv(rational const& v, unsigned n) : bit_vector(2*n) {
if (v.is_uint64() && n <= 64) {
tbv tmp(v.get_uint64(), n);
*this = tmp;
return;
}
for (unsigned bit = n; bit > 0; ) {
--bit;
if (bitwise_and(v, rational::power_of_two(bit)).is_zero()) {
set(bit, BIT_0);
} else {
set(bit, BIT_1);
}
}
}
tbv& operator=(tbv const& other) {
bit_vector::operator=(other);
return *this;
}
bool operator!=(tbv const& other) const {
return bit_vector::operator!=(other);
}
bool operator==(tbv const& other) const {
return bit_vector::operator==(other);
}
void resize(unsigned n, unsigned val) {
while (size() < n) {
bit_vector::push_back((val & 2) != 0);
bit_vector::push_back((val & 1) != 0);
}
}
bool empty() const { return false; } // TBD
bool is_subset(tbv const& other) const {
SASSERT(size() == other.size());
return other.contains(*this);
}
bool is_superset(tbv const& other) const {
SASSERT(size() == other.size());
return contains(other);
}
unsigned size() const { return bit_vector::size()/2; }
void display(std::ostream& out) const {
for (unsigned i = 0; i < size(); ++i) {
switch (get(i)) {
case BIT_0:
out << '0';
break;
case BIT_1:
out << '1';
break;
case BIT_x:
out << 'x';
break;
case BIT_z:
out << 'z';
break;
default:
UNREACHABLE();
}
}
}
private:
void set(unsigned index, unsigned value) {
SASSERT(value <= 3);
bit_vector::set(2*index, (value & 2) != 0);
bit_vector::set(2*index+1, (value & 1) != 0);
}
unsigned get(unsigned index) const {
index *= 2;
return (bit_vector::get(index) << 1) | (unsigned)bit_vector::get(index+1);
}
};
class dot {
tbv m_pos;
vector<tbv> m_negs;
public:
dot(tbv const& pos, vector<tbv> const& negs):
m_pos(pos), m_negs(negs) {}
bool operator==(dot const& other) const {
if (m_pos != other.m_pos) return false;
if (m_negs.size() != other.m_negs.size()) return false;
for (unsigned i = 0; i < m_negs.size(); ++i) {
if (m_negs[i] != other.m_negs[i]) return false;
}
return true;
}
void display(std::ostream& out) {
out << "<";
m_pos.display(out);
out << "\\";
for (unsigned i = 0; i < m_negs.size(); ++i) {
m_negs[i].display(out);
if (i + 1 < m_negs.size()) out << " u ";
}
out << ">";
}
};
class ddnf_mgr;
class ddnf_node;
typedef ref_vector<ddnf_node, ddnf_mgr> ddnf_node_vector;
class ddnf_node {
tbv m_tbv;
ddnf_node_vector m_children;
vector<dot> m_pos;
vector<dot> m_neg;
unsigned m_refs;
public:
ddnf_node(ddnf_mgr& m, tbv const& tbv):
m_tbv(tbv),
m_children(m),
m_refs(0) {
}
unsigned inc_ref() {
return ++m_refs;
}
unsigned dec_ref() {
SASSERT(m_refs > 0);
return --m_refs;
}
unsigned num_children() const { return m_children.size(); }
ddnf_node* operator[](unsigned index) { return m_children[index].get(); }
tbv const& get_tbv() const { return m_tbv; }
void add_child(ddnf_node* n);
void remove_child(ddnf_node* n);
bool contains_child(ddnf_node* n) const;
};
class ddnf_mgr {
unsigned m_num_bits;
ddnf_node* m_root;
ddnf_node_vector m_nodes;
vector<dot> m_dots;
public:
ddnf_mgr(unsigned n): m_num_bits(n), m_nodes(*this) {
m_root = alloc(ddnf_node, *this, tbv(n, BIT_x));
m_nodes.push_back(m_root);
}
void inc_ref(ddnf_node* n) {
n->inc_ref();
}
void dec_ref(ddnf_node* n) {
unsigned count = n->dec_ref();
NOT_IMPLEMENTED_YET();
}
private:
void insert_new(ddnf_node& root, ddnf_node* new_n,
ptr_vector<tbv>& new_intersections) {
SASSERT(root.get_tbv().is_superset(new_n->get_tbv()));
// if (root == *new_n) return;
bool inserted = false;
for (unsigned i = 0; i < root.num_children(); ++i) {
ddnf_node& child = *(root[i]);
if (child.get_tbv().is_superset(new_n->get_tbv())) {
inserted = true;
insert_new(child, new_n, new_intersections);
}
}
if (inserted) return;
ddnf_node_vector subset_children(*this);
for (unsigned i = 0; i < root.num_children(); ++i) {
ddnf_node& child = *(root[i]);
// cannot be superset
// checking for subset
if (child.get_tbv().is_subset(new_n->get_tbv())) {
subset_children.push_back(&child);
}
// this means there is a non-full intersection
else {
tbv intr;
// TBD intersect(child.get_tbv(), new_n->get_tbv(), intr);
if (!intr.empty()) {
// TBD new_intersections.push_back(intr);
}
}
}
for (unsigned i = 0; i < subset_children.size(); ++i) {
root.remove_child(subset_children[i].get());
new_n->add_child(subset_children[i].get());
}
root.add_child(new_n);
}
#if 0
DDNFNode InsertTBV(TernaryBitVector aTbv)
{
foreach (DDNFNode node in allNodes)
{
if (node.tbv.IsEqualset(aTbv))
{
return node;
}
}
DDNFNode newNode = new DDNFNode(aTbv);
this.allNodes.Add(newNode);
List<TernaryBitVector> newIntersections = new List<TernaryBitVector>();
InsertNewNode(this.root, newNode, newIntersections);
// add the TBVs corresponding to new intersections
foreach (TernaryBitVector newIntr in newIntersections)
{
// this assert guarantees termination since you can only
// insert smaller tbvs recursively
Debug.Assert(!newIntr.IsSupset(aTbv));
InsertTBV(newIntr);
}
return newNode;
}
public void InsertDot(DOT aDot)
{
this.allDots.Add(aDot);
DDNFNode posNode = InsertTBV(aDot.pos);
List<DDNFNode> negNodes = new List<DDNFNode>();
foreach (TernaryBitVector neg in aDot.negs)
{
negNodes.Add(InsertTBV(neg));
}
posNode.posDots.Add(aDot);
foreach (DDNFNode negNode in negNodes)
{
negNode.negDots.Add(aDot);
}
}
// remove all negNodes for each dot in dot2Nodes
void RemoveNegNodesForAllDots(DDNFNode aNode, HashSet<DOT> activeDots,
ref Dictionary<DOT, HashSet<DDNFNode>> dot2Nodes)
{
foreach (DOT negDot in aNode.negDots)
{
activeDots.Add(negDot);
}
foreach (DOT activeDot in activeDots)
{
dot2Nodes[activeDot].Remove(aNode);
}
foreach (DDNFNode child in aNode.children)
{
RemoveNegNodesForAllDots(child, new HashSet<DOT>(activeDots), ref dot2Nodes);
}
}
// add all posNodes for each dot in dot2Nodes
void AddPosNodesForAllDots(DDNFNode aNode, HashSet<DOT> activeDots,
ref Dictionary<DOT, HashSet<DDNFNode>> dot2Nodes)
{
foreach (DOT posDot in aNode.posDots)
{
activeDots.Add(posDot);
}
foreach (DOT activeDot in activeDots)
{
dot2Nodes[activeDot].Add(aNode);
}
foreach (DDNFNode child in aNode.children)
{
AddPosNodesForAllDots(child, new HashSet<DOT>(activeDots), ref dot2Nodes);
}
}
public Dictionary<DOT, HashSet<DDNFNode>> NodesForAllDots()
{
Dictionary<DOT, HashSet<DDNFNode>> dot2Nodes =
new Dictionary<DOT, HashSet<DDNFNode>>();
foreach (DOT dot in allDots)
{
dot2Nodes[dot] = new HashSet<DDNFNode>();
}
AddPosNodesForAllDots(this.root, new HashSet<DOT>(), ref dot2Nodes);
RemoveNegNodesForAllDots(this.root, new HashSet<DOT>(), ref dot2Nodes);
return dot2Nodes;
}
public string PrintNodes()
{
StringBuilder retVal = new StringBuilder();
retVal.Append("<DDNF: ");
foreach (DDNFNode node in allNodes)
{
retVal.Append("\n").Append(node.ToString());
}
return retVal.Append(">").ToString();
}
}
}
#endif
};
void ddnf_node::add_child(ddnf_node* n) {
SASSERT(!m_tbv.is_subset(n->m_tbv));
m_children.push_back(n);
}
void ddnf_node::remove_child(ddnf_node* n) {
m_children.erase(n);
}
bool ddnf_node::contains_child(ddnf_node* n) const {
return m_children.contains(n);
}
class ddnf::imp {
struct stats {
stats() { reset(); }
void reset() { memset(this, 0, sizeof(*this)); }
};
context& m_ctx;
ast_manager& m;
rule_manager& rm;
volatile bool m_cancel;
ptr_vector<expr> m_todo;
ast_mark m_visited1, m_visited2;
stats m_stats;
public:
imp(context& ctx):
m_ctx(ctx),
m(ctx.get_manager()),
rm(ctx.get_rule_manager()),
m_cancel(false)
{
}
~imp() {}
lbool query(expr* query) {
m_ctx.ensure_opened();
if (!can_handle_rules()) {
return l_undef;
}
IF_VERBOSE(0, verbose_stream() << "rules are OK\n";);
return run();
}
void cancel() {
m_cancel = true;
}
void cleanup() {
m_cancel = false;
}
void reset_statistics() {
m_stats.reset();
}
void collect_statistics(statistics& st) const {
}
void display_certificate(std::ostream& out) const {
expr_ref ans = get_answer();
out << mk_pp(ans, m) << "\n";
}
expr_ref get_answer() const {
UNREACHABLE();
return expr_ref(m.mk_true(), m);
}
private:
proof_ref get_proof() const {
scoped_proof sp(m);
proof_ref pr(m);
return pr;
}
lbool run() {
return l_undef;
}
bool can_handle_rules() {
m_visited1.reset();
m_todo.reset();
rule_set const& rules = m_ctx.get_rules();
datalog::rule_set::iterator it = rules.begin();
datalog::rule_set::iterator end = rules.end();
for (; it != end; ++it) {
if (!can_handle_rule(**it)) {
return false;
}
}
return true;
}
bool can_handle_rule(rule const& r) {
// all predicates are monadic.
unsigned utsz = r.get_uninterpreted_tail_size();
unsigned sz = r.get_tail_size();
for (unsigned i = utsz; i < sz; ++i) {
m_todo.push_back(r.get_tail(i));
}
if (check_monadic()) {
return true;
}
else {
r.display(m_ctx, std::cout);
return false;
}
}
bool check_monadic() {
expr* e1, *e2;
while (!m_todo.empty()) {
expr* e = m_todo.back();
m_todo.pop_back();
if (m_visited1.is_marked(e)) {
continue;
}
m_visited1.mark(e, true);
if (is_var(e)) {
continue;
}
if (is_quantifier(e)) {
return false;
}
if (m.is_and(e) ||
m.is_or(e) ||
m.is_iff(e) ||
m.is_not(e) ||
m.is_implies(e)) {
m_todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
continue;
}
if (m.is_eq(e, e1, e2)) {
if (is_var(e1) && is_ground(e2)) {
continue;
}
if (is_var(e2) && is_ground(e1)) {
continue;
}
if (is_var(e1) && is_var(e2)) {
continue;
}
}
if (is_ground(e)) {
continue;
}
if (is_unary(e)) {
continue;
}
IF_VERBOSE(0, verbose_stream() << "Could not handle: " << mk_pp(e, m) << "\n";);
return false;
}
return true;
}
bool is_unary(expr* e) {
var* v = 0;
m_visited2.reset();
unsigned sz = m_todo.size();
m_todo.push_back(e);
while (m_todo.size() > sz) {
expr* e = m_todo.back();
m_todo.pop_back();
if (m_visited2.is_marked(e)) {
continue;
}
m_visited2.mark(e, true);
if (is_var(e)) {
if (v && v != e) {
return false;
}
v = to_var(e);
}
else if (is_app(e)) {
m_todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
}
else {
return false;
}
}
return true;
}
};
ddnf::ddnf(context& ctx):
datalog::engine_base(ctx.get_manager(),"tabulation"),
m_imp(alloc(imp, ctx)) {
}
ddnf::~ddnf() {
dealloc(m_imp);
}
lbool ddnf::query(expr* query) {
return m_imp->query(query);
}
void ddnf::cancel() {
m_imp->cancel();
}
void ddnf::cleanup() {
m_imp->cleanup();
}
void ddnf::reset_statistics() {
m_imp->reset_statistics();
}
void ddnf::collect_statistics(statistics& st) const {
m_imp->collect_statistics(st);
}
void ddnf::display_certificate(std::ostream& out) const {
m_imp->display_certificate(out);
}
expr_ref ddnf::get_answer() {
return m_imp->get_answer();
}
};

46
src/muz/ddnf/ddnf.h Normal file
View file

@ -0,0 +1,46 @@
/*++
Copyright (c) 2013 Microsoft Corporation
Module Name:
ddnf.h
Abstract:
DDNF based engine.
Author:
Nikolaj Bjorner (nbjorner) 2014-08-21
Revision History:
--*/
#ifndef _DDNF__H_
#define _DDNF__H_
#include "ast.h"
#include "lbool.h"
#include "statistics.h"
#include "dl_engine_base.h"
namespace datalog {
class context;
class ddnf : public engine_base {
class imp;
imp* m_imp;
public:
ddnf(context& ctx);
~ddnf();
virtual lbool query(expr* query);
virtual void cancel();
virtual void cleanup();
virtual void reset_statistics();
virtual void collect_statistics(statistics& st) const;
virtual void display_certificate(std::ostream& out) const;
virtual expr_ref get_answer();
};
};
#endif

3
src/muz/fp/dl_register_engine.cpp
View file

@ -22,6 +22,7 @@ Revision History:
#include "tab_context.h"
#include "rel_context.h"
#include "pdr_dl_interface.h"
#include "ddnf.h"
#include "duality_dl_interface.h"
namespace datalog {
@ -43,6 +44,8 @@ namespace datalog {
return alloc(clp, *m_ctx);
case DUALITY_ENGINE:
return alloc(Duality::dl_interface, *m_ctx);
case DDNF_ENGINE:
return alloc(ddnf, *m_ctx);
case LAST_ENGINE:
UNREACHABLE();
return 0;

52
src/opt/maxres.cpp
View file

@ -82,6 +82,7 @@ private:
expr_ref_vector m_trail;
strategy_t m_st;
rational m_max_upper;
bool m_hill_climb;
public:
maxres(context& c,
@ -92,7 +93,8 @@ public:
m_mus(m_s, m),
m_mss(m_s, m),
m_trail(m),
m_st(st)
m_st(st),
m_hill_climb(true)
{
}
@ -299,7 +301,21 @@ public:
TRACE("opt",
display_vec(tout << "core: ", core.size(), core.c_ptr());
display_vec(tout << "assumptions: ", asms.size(), asms.c_ptr()););
is_sat = s().check_sat(asms.size(), asms.c_ptr());
if (m_hill_climb) {
/**
Give preference to cores that have large minmal values.
*/
sort_assumptions(asms);
unsigned index = 0;
while (index < asms.size() && is_sat != l_false) {
index = next_index(asms, index);
is_sat = s().check_sat(index, asms.c_ptr());
}
}
else {
is_sat = s().check_sat(asms.size(), asms.c_ptr());
}
}
TRACE("opt",
tout << "num cores: " << cores.size() << "\n";
@ -315,6 +331,36 @@ public:
}
struct compare_asm {
maxres& mr;
compare_asm(maxres& mr):mr(mr) {}
bool operator()(expr* a, expr* b) const {
return mr.get_weight(a) > mr.get_weight(b);
}
};
void sort_assumptions(expr_ref_vector& _asms) {
compare_asm comp(*this);
ptr_vector<expr> asms(_asms.size(), _asms.c_ptr());
expr_ref_vector trail(_asms);
std::sort(asms.begin(), asms.end(), comp);
_asms.reset();
_asms.append(asms.size(), asms.c_ptr());
DEBUG_CODE(
for (unsigned i = 0; i + 1 < asms.size(); ++i) {
SASSERT(get_weight(asms[i]) >= get_weight(asms[i+1]));
});
}
unsigned next_index(expr_ref_vector const& asms, unsigned index) {
if (index < asms.size()) {
rational w = get_weight(asms[index]);
++index;
for (; index < asms.size() && w == get_weight(asms[index]); ++index);
}
return index;
}
lbool process_sat(ptr_vector<expr>& corr_set) {
expr_ref fml(m), tmp(m);
TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr()););
@ -379,7 +425,7 @@ public:
return l_true;
}
rational get_weight(expr* e) {
rational get_weight(expr* e) const {
return m_asm2weight.find(e);
}

3
src/sat/sat_mus.cpp
View file

@ -71,7 +71,7 @@ namespace sat {
literal lit = core.back();
core.pop_back();
unsigned sz = mus.size();
// mus.push_back(~lit); // TBD: measure
mus.push_back(~lit); // TBD: measure
mus.append(core);
lbool is_sat = s.check(mus.size(), mus.c_ptr());
TRACE("sat", tout << "mus: " << mus << "\n";);
@ -102,6 +102,7 @@ namespace sat {
core.push_back(lit);
}
}
IF_VERBOSE(2, verbose_stream() << "reduced core: " << core.size() << "\n";);
break;
}
}

15
src/sat/sat_solver.cpp
View file

@ -902,6 +902,11 @@ namespace sat {
m_assumption_set.reset();
push();
propagate(false);
if (inconsistent()) {
return;
}
TRACE("sat",
for (unsigned i = 0; i < num_lits; ++i)
tout << lits[i] << " ";
@ -916,15 +921,17 @@ namespace sat {
m_assumption_set.insert(_l_); \
m_assumptions.push_back(_l_); \
assign(_l_, justification()); \
// propagate(false); \
for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) {
literal nlit = ~m_user_scope_literals[i];
_INSERT_LIT(nlit);
}
for (unsigned i = 0; !inconsistent() && i < num_lits; ++i) {
literal lit = lits[i];
_INSERT_LIT(lit);
}
for (unsigned i = 0; !inconsistent() && i < m_user_scope_literals.size(); ++i) {
literal nlit = ~m_user_scope_literals[i];
_INSERT_LIT(nlit);
}
}
void solver::reinit_assumptions() {

16
src/util/bit_vector.cpp
View file

@ -208,6 +208,22 @@ void bit_vector::display(std::ostream & out) const {
#endif
}
bool bit_vector::contains(bit_vector const& other) const {
unsigned n = num_words();
if (n == 0)
return true;
for (unsigned i = 0; i < n - 1; ++i) {
if ((m_data[i] & other.m_data[i]) != other.m_data[i])
return false;
}
unsigned bit_rest = m_num_bits % 32;
unsigned mask = (1U << bit_rest) - 1;
if (mask == 0) mask = UINT_MAX;
unsigned other_data = other.m_data[n-1] & mask;
return (m_data[n-1] & other_data) == other_data;
}
void fr_bit_vector::reset() {
unsigned sz = size();
unsigned_vector::const_iterator it = m_one_idxs.begin();

3
src/util/bit_vector.h
View file

@ -200,6 +200,9 @@ public:
bit_vector & operator&=(bit_vector const & source);
void display(std::ostream & out) const;
bool contains(const bit_vector & other) const;
};
inline std::ostream & operator<<(std::ostream & out, bit_vector const & b) {