mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge branch 'opt' of https://git01.codeplex.com/z3 into opt
This commit is contained in:
commit
06073db413
|
@ -63,11 +63,11 @@ def init_project_def():
|
|||
add_lib('tab', ['muz', 'transforms'], 'muz/tab')
|
||||
add_lib('bmc', ['muz', 'transforms'], 'muz/bmc')
|
||||
add_lib('fp', ['muz', 'pdr', 'clp', 'tab', 'rel', 'bmc'], 'muz/fp')
|
||||
add_lib('opt', ['smt'], 'opt')
|
||||
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', 'aig_tactic', 'fp', 'qe','sls_tactic', 'subpaving_tactic'], 'tactic/portfolio')
|
||||
add_lib('smtparser', ['portfolio'], 'parsers/smt')
|
||||
add_lib('opt', ['smt', 'smtlogic_tactics'], 'opt')
|
||||
API_files = ['z3_api.h', 'z3_algebraic.h', 'z3_polynomial.h', 'z3_rcf.h']
|
||||
add_lib('api', ['portfolio', 'user_plugin', 'smtparser', 'realclosure'],
|
||||
includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files)
|
||||
|
|
|
@ -18,10 +18,11 @@ Notes:
|
|||
--*/
|
||||
|
||||
#include "fu_malik.h"
|
||||
#include "smtlogics/qfbv_tactic.h"
|
||||
#include "qfbv_tactic.h"
|
||||
#include "tactic2solver.h"
|
||||
#include "goal.h"
|
||||
#include "probe.h"
|
||||
#include "tactic.h"
|
||||
#include "smt_context.h"
|
||||
|
||||
/**
|
||||
|
@ -41,16 +42,16 @@ Notes:
|
|||
namespace opt {
|
||||
|
||||
struct fu_malik::imp {
|
||||
ast_manager& m;
|
||||
ref<solver> m_s;
|
||||
ast_manager& m;
|
||||
expr_ref_vector m_soft;
|
||||
expr_ref_vector m_orig_soft;
|
||||
expr_ref_vector m_aux;
|
||||
expr_ref_vector m_assignment;
|
||||
unsigned m_upper_size;
|
||||
|
||||
ref<solver> m_s;
|
||||
solver & m_original_solver;
|
||||
bool m_use_new_bv_solver;
|
||||
bool m_use_new_bv_solver;
|
||||
|
||||
imp(ast_manager& m, solver& s, expr_ref_vector const& soft):
|
||||
m(m),
|
||||
|
@ -82,6 +83,71 @@ namespace opt {
|
|||
* add at-most-one constraint with blocking
|
||||
*/
|
||||
|
||||
typedef obj_hashtable<expr> expr_set;
|
||||
|
||||
void set2vector(expr_set const& set, expr_ref_vector & es) const {
|
||||
es.reset();
|
||||
expr_set::iterator it = set.begin(), end = set.end();
|
||||
for (; it != end; ++it) {
|
||||
es.push_back(*it);
|
||||
}
|
||||
}
|
||||
|
||||
void set_union(expr_set const& set1, expr_set const& set2, expr_set & set) const {
|
||||
set.reset();
|
||||
expr_set::iterator it = set1.begin(), end = set1.end();
|
||||
for (; it != end; ++it) {
|
||||
set.insert(*it);
|
||||
}
|
||||
it = set2.begin();
|
||||
end = set2.end();
|
||||
for (; it != end; ++it) {
|
||||
set.insert(*it);
|
||||
}
|
||||
}
|
||||
|
||||
void quick_explain(expr_ref_vector const& assumptions, expr_ref_vector & literals, bool has_set, expr_set & core) {
|
||||
if (has_set && s().check_sat(assumptions.size(), assumptions.c_ptr()) == l_false) {
|
||||
core.reset();
|
||||
return;
|
||||
}
|
||||
|
||||
SASSERT(!literals.empty());
|
||||
if (literals.size() == 1) {
|
||||
core.reset();
|
||||
core.insert(literals[0].get());
|
||||
return;
|
||||
}
|
||||
|
||||
unsigned mid = literals.size()/2;
|
||||
expr_ref_vector ls1(m), ls2(m);
|
||||
ls1.append(mid, literals.c_ptr());
|
||||
ls2.append(literals.size()-mid, literals.c_ptr() + mid);
|
||||
#if Z3DEBUG
|
||||
expr_ref_vector ls(m);
|
||||
ls.append(ls1);
|
||||
ls.append(ls2);
|
||||
SASSERT(ls.size() == literals.size());
|
||||
for (unsigned i = 0; i < literals.size(); ++i) {
|
||||
SASSERT(ls[i].get() == literals[i].get());
|
||||
}
|
||||
#endif
|
||||
expr_ref_vector as1(m);
|
||||
as1.append(assumptions);
|
||||
as1.append(ls1);
|
||||
expr_set core2;
|
||||
quick_explain(as1, ls2, !ls1.empty(), core2);
|
||||
|
||||
expr_ref_vector as2(m), cs2(m);
|
||||
as2.append(assumptions);
|
||||
set2vector(core2, cs2);
|
||||
as2.append(cs2);
|
||||
expr_set core1;
|
||||
quick_explain(as2, ls1, !core2.empty(), core1);
|
||||
|
||||
set_union(core1, core2, core);
|
||||
}
|
||||
|
||||
lbool step() {
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat step " << m_soft.size() + 2 - m_upper_size << ")\n";);
|
||||
expr_ref_vector assumptions(m), block_vars(m);
|
||||
|
@ -95,12 +161,33 @@ namespace opt {
|
|||
|
||||
ptr_vector<expr> core;
|
||||
if (m_use_new_bv_solver) {
|
||||
unsigned i = 0;
|
||||
while (s().check_sat(core.size(), core.c_ptr()) != l_false) {
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";);
|
||||
core.push_back(assumptions[i].get());
|
||||
++i;
|
||||
// Binary search for minimal unsat core
|
||||
expr_set core_set;
|
||||
expr_ref_vector empty(m);
|
||||
quick_explain(empty, assumptions, true, core_set);
|
||||
expr_set::iterator it = core_set.begin(), end = core_set.end();
|
||||
for (; it != end; ++it) {
|
||||
core.push_back(*it);
|
||||
}
|
||||
|
||||
//// Forward linear search for unsat core
|
||||
//unsigned i = 0;
|
||||
//while (s().check_sat(core.size(), core.c_ptr()) != l_false) {
|
||||
// IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";);
|
||||
// core.push_back(assumptions[i].get());
|
||||
// ++i;
|
||||
//}
|
||||
|
||||
//// Backward linear search for unsat core
|
||||
//unsigned i = 0;
|
||||
//core.append(assumptions.size(), assumptions.c_ptr());
|
||||
//while (!core.empty() && s().check_sat(core.size()-1, core.c_ptr()) == l_false) {
|
||||
// IF_VERBOSE(0, verbose_stream() << "(opt.max_sat get-unsat-core round " << i << ")\n";);
|
||||
// core.pop_back();
|
||||
// ++i;
|
||||
//}
|
||||
|
||||
IF_VERBOSE(0, verbose_stream() << "(opt.max_sat unsat-core of size " << core.size() << ")\n";);
|
||||
}
|
||||
else {
|
||||
s().get_unsat_core(core);
|
||||
|
@ -154,7 +241,11 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
|
||||
void set_solver() {
|
||||
void set_solver() {
|
||||
opt_solver & opt_s = opt_solver::to_opt(m_original_solver);
|
||||
if (opt_s.is_dumping_benchmark())
|
||||
return;
|
||||
|
||||
solver& current_solver = s();
|
||||
goal g(m, true, false);
|
||||
unsigned num_assertions = current_solver.get_num_assertions();
|
||||
|
@ -163,12 +254,11 @@ namespace opt {
|
|||
}
|
||||
probe *p = mk_is_qfbv_probe();
|
||||
bool all_bv = (*p)(g).is_true();
|
||||
if (all_bv) {
|
||||
opt_solver & os = opt_solver::to_opt(m_original_solver);
|
||||
smt::context & ctx = os.get_context();
|
||||
tactic* t = mk_qfbv_tactic(m, ctx.get_params());
|
||||
if (all_bv) {
|
||||
smt::context & ctx = opt_s.get_context();
|
||||
tactic_ref t = mk_qfbv_tactic(m, ctx.get_params());
|
||||
// The new SAT solver hasn't supported unsat core yet
|
||||
m_s = mk_tactic2solver(m, t);
|
||||
m_s = mk_tactic2solver(m, t.get());
|
||||
SASSERT(m_s != &m_original_solver);
|
||||
for (unsigned i = 0; i < num_assertions; ++i) {
|
||||
m_s->assert_expr(current_solver.get_assertion(i));
|
||||
|
@ -211,6 +301,11 @@ namespace opt {
|
|||
}
|
||||
}
|
||||
}
|
||||
statistics st;
|
||||
s().collect_statistics(st);
|
||||
SASSERT(st.size() > 0);
|
||||
opt_solver & opt_s = opt_solver::to_opt(m_original_solver);
|
||||
opt_s.set_interim_stats(st);
|
||||
// We are done and soft_constraints has
|
||||
// been updated with the max-sat assignment.
|
||||
return is_sat;
|
||||
|
|
|
@ -55,7 +55,13 @@ namespace opt {
|
|||
}
|
||||
|
||||
void opt_solver::collect_statistics(statistics & st) const {
|
||||
m_context.collect_statistics(st);
|
||||
// Hack to display fu_malik statistics
|
||||
if (m_stats.size() > 0) {
|
||||
st.copy(m_stats);
|
||||
}
|
||||
else {
|
||||
m_context.collect_statistics(st);
|
||||
}
|
||||
}
|
||||
|
||||
void opt_solver::assert_expr(expr * t) {
|
||||
|
@ -99,6 +105,10 @@ namespace opt {
|
|||
|
||||
static unsigned g_checksat_count = 0;
|
||||
|
||||
bool opt_solver::is_dumping_benchmark() {
|
||||
return m_is_dump;
|
||||
}
|
||||
|
||||
lbool opt_solver::check_sat_core(unsigned num_assumptions, expr * const * assumptions) {
|
||||
TRACE("opt_solver_na2as", {
|
||||
tout << "opt_opt_solver::check_sat_core: " << m_context.size() << "\n";
|
||||
|
@ -213,6 +223,10 @@ namespace opt {
|
|||
}
|
||||
return dynamic_cast<opt_solver&>(s);
|
||||
}
|
||||
|
||||
void opt_solver::set_interim_stats(statistics & st) {
|
||||
m_stats.copy(st);
|
||||
}
|
||||
|
||||
void opt_solver::to_smt2_benchmark(std::ofstream & buffer, char const * name, char const * logic,
|
||||
char const * status, char const * attributes) {
|
||||
|
|
|
@ -46,7 +46,8 @@ namespace opt {
|
|||
bool m_objective_enabled;
|
||||
svector<smt::theory_var> m_objective_vars;
|
||||
vector<inf_eps> m_objective_values;
|
||||
bool m_is_dump;
|
||||
bool m_is_dump;
|
||||
statistics m_stats;
|
||||
public:
|
||||
opt_solver(ast_manager & m, params_ref const & p, symbol const & l);
|
||||
virtual ~opt_solver();
|
||||
|
@ -77,7 +78,9 @@ namespace opt {
|
|||
expr_ref block_upper_bound(unsigned obj_index, inf_eps const& val);
|
||||
|
||||
static opt_solver& to_opt(solver& s);
|
||||
|
||||
void set_interim_stats(statistics & st);
|
||||
bool is_dumping_benchmark();
|
||||
|
||||
class toggle_objective {
|
||||
opt_solver& s;
|
||||
bool m_old_value;
|
||||
|
|
|
@ -671,6 +671,7 @@ namespace sat {
|
|||
//
|
||||
// -----------------------
|
||||
lbool solver::check() {
|
||||
IF_VERBOSE(0, verbose_stream() << "(sat.sat-solver using the new SAT solver)\n";);
|
||||
SASSERT(scope_lvl() == 0);
|
||||
#ifdef CLONE_BEFORE_SOLVING
|
||||
if (m_mc.empty()) {
|
||||
|
@ -1970,7 +1971,7 @@ namespace sat {
|
|||
m_cancel = f;
|
||||
}
|
||||
|
||||
void solver::collect_statistics(statistics & st) {
|
||||
void solver::collect_statistics(statistics & st) {
|
||||
m_stats.collect_statistics(st);
|
||||
m_cleaner.collect_statistics(st);
|
||||
m_simplifier.collect_statistics(st);
|
||||
|
|
|
@ -25,6 +25,7 @@ Revision History:
|
|||
#include"trace.h"
|
||||
#include"warning.h"
|
||||
#include"uint_set.h"
|
||||
#include<deque>
|
||||
|
||||
typedef int dl_var;
|
||||
|
||||
|
@ -953,6 +954,87 @@ public:
|
|||
return m_edges;
|
||||
}
|
||||
|
||||
void get_neighbours_undirected(dl_var current, svector<dl_var> & neighbours) {
|
||||
neighbours.reset();
|
||||
edge_id_vector & edges = m_out_edges[current];
|
||||
typename edge_id_vector::iterator it = edges.begin(), end = edges.end();
|
||||
for (; it != end; ++it) {
|
||||
edge_id e_id = *it;
|
||||
edge & e = m_edges[e_id];
|
||||
if (!e.is_enabled()) continue;
|
||||
SASSERT(e.get_source() == current);
|
||||
dl_var neighbour = e.get_target();
|
||||
neighbours.push_back(neighbour);
|
||||
}
|
||||
edges = m_in_edges[current];
|
||||
it = edges.begin();
|
||||
end = edges.end();
|
||||
for (; it != end; ++it) {
|
||||
edge_id e_id = *it;
|
||||
edge & e = m_edges[e_id];
|
||||
if (!e.is_enabled()) continue;
|
||||
SASSERT(e.get_target() == current);
|
||||
dl_var neighbour = e.get_source();
|
||||
neighbours.push_back(neighbour);
|
||||
}
|
||||
}
|
||||
|
||||
void dfs_undirected(dl_var start, svector<dl_var> & threads) {
|
||||
threads.reset();
|
||||
threads.resize(get_num_nodes());
|
||||
uint_set visited;
|
||||
svector<dl_var> nodes;
|
||||
nodes.push_back(start);
|
||||
dl_var prev = -1;
|
||||
while(!nodes.empty()) {
|
||||
dl_var current = nodes.back();
|
||||
nodes.pop_back();
|
||||
visited.insert(current);
|
||||
if (prev != -1)
|
||||
threads[prev] = current;
|
||||
prev = current;
|
||||
svector<dl_var> neighbours;
|
||||
get_neighbours_undirected(current, neighbours);
|
||||
for (unsigned i = 0; i < neighbours.size(); ++i) {
|
||||
edge_id id;
|
||||
SASSERT(prev == -1 || get_edge_id(prev, current, id) || get_edge_id(current, prev, id));
|
||||
if (!visited.contains(neighbours[i])) {
|
||||
nodes.push_back(neighbours[i]);
|
||||
}
|
||||
}
|
||||
}
|
||||
threads[prev] = start;
|
||||
}
|
||||
|
||||
void bfs_undirected(dl_var start, svector<dl_var> & parents, svector<dl_var> & depths) {
|
||||
parents.reset();
|
||||
parents.resize(get_num_nodes());
|
||||
depths.reset();
|
||||
depths.resize(get_num_nodes());
|
||||
uint_set visited;
|
||||
std::deque<dl_var> nodes;
|
||||
visited.insert(start);
|
||||
nodes.push_front(start);
|
||||
while(!nodes.empty()) {
|
||||
dl_var current = nodes.back();
|
||||
nodes.pop_back();
|
||||
SASSERT(visited.contains(current));
|
||||
svector<dl_var> neighbours;
|
||||
get_neighbours_undirected(current, neighbours);
|
||||
for (unsigned i = 0; i < neighbours.size(); ++i) {
|
||||
dl_var & next = neighbours[i];
|
||||
edge_id id;
|
||||
SASSERT(get_edge_id(current, next, id) || get_edge_id(next, current, id));
|
||||
if (!visited.contains(next)) {
|
||||
parents[next] = current;
|
||||
depths[next] = depths[current] + 1;
|
||||
visited.insert(next);
|
||||
nodes.push_front(next);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
template<typename Functor>
|
||||
void enumerate_edges(dl_var source, dl_var target, Functor& f) {
|
||||
edge_id_vector & edges = m_out_edges[source];
|
||||
|
|
|
@ -244,7 +244,7 @@ namespace smt {
|
|||
};
|
||||
|
||||
graph m_graph;
|
||||
thread_spanning_tree<Ext> m_tree;
|
||||
spanning_tree_base * m_tree;
|
||||
|
||||
// Denote supply/demand b_i on node i
|
||||
vector<fin_numeral> m_balances;
|
||||
|
|
|
@ -27,8 +27,7 @@ namespace smt {
|
|||
|
||||
template<typename Ext>
|
||||
network_flow<Ext>::network_flow(graph & g, vector<fin_numeral> const & balances) :
|
||||
m_balances(balances),
|
||||
m_tree(m_graph) {
|
||||
m_balances(balances) {
|
||||
// Network flow graph has the edges in the reversed order compared to constraint graph
|
||||
// We only take enabled edges from the original graph
|
||||
for (unsigned i = 0; i < g.get_num_nodes(); ++i) {
|
||||
|
@ -42,6 +41,7 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
m_step = 0;
|
||||
m_tree = alloc(basic_spanning_tree<Ext>, m_graph);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
|
@ -82,7 +82,7 @@ namespace smt {
|
|||
tree.push_back(m_graph.add_edge(src, tgt, numeral::one(), explanation()));
|
||||
}
|
||||
|
||||
m_tree.initialize(tree);
|
||||
m_tree->initialize(tree);
|
||||
|
||||
TRACE("network_flow", {
|
||||
tout << pp_vector("Potentials", m_potentials, true) << pp_vector("Flows", m_flows);
|
||||
|
@ -96,14 +96,14 @@ namespace smt {
|
|||
node src = m_graph.get_source(m_enter_id);
|
||||
node tgt = m_graph.get_target(m_enter_id);
|
||||
numeral cost = m_potentials[src] - m_potentials[tgt] - m_graph.get_weight(m_enter_id);
|
||||
numeral change = m_tree.in_subtree_t2(tgt) ? cost : -cost;
|
||||
numeral change = m_tree->in_subtree_t2(tgt) ? cost : -cost;
|
||||
node start = m_graph.get_source(m_leave_id);
|
||||
if (!m_tree.in_subtree_t2(start)) {
|
||||
if (!m_tree->in_subtree_t2(start)) {
|
||||
start = m_graph.get_target(m_leave_id);;
|
||||
}
|
||||
TRACE("network_flow", tout << "update_potentials of T_" << start << " with change = " << change << "...\n";);
|
||||
svector<node> descendants;
|
||||
m_tree.get_descendants(start, descendants);
|
||||
m_tree->get_descendants(start, descendants);
|
||||
SASSERT(descendants.size() >= 1);
|
||||
for (unsigned i = 0; i < descendants.size(); ++i) {
|
||||
node u = descendants[i];
|
||||
|
@ -120,7 +120,7 @@ namespace smt {
|
|||
node tgt = m_graph.get_target(m_enter_id);
|
||||
svector<edge_id> path;
|
||||
svector<bool> against;
|
||||
m_tree.get_path(src, tgt, path, against);
|
||||
m_tree->get_path(src, tgt, path, against);
|
||||
SASSERT(path.size() >= 1);
|
||||
for (unsigned i = 0; i < path.size(); ++i) {
|
||||
edge_id e_id = path[i];
|
||||
|
@ -138,7 +138,7 @@ namespace smt {
|
|||
edge_id leave_id;
|
||||
svector<edge_id> path;
|
||||
svector<bool> against;
|
||||
m_tree.get_path(src, tgt, path, against);
|
||||
m_tree->get_path(src, tgt, path, against);
|
||||
SASSERT(path.size() >= 1);
|
||||
for (unsigned i = 0; i < path.size(); ++i) {
|
||||
edge_id e_id = path[i];
|
||||
|
@ -164,7 +164,7 @@ namespace smt {
|
|||
|
||||
template<typename Ext>
|
||||
void network_flow<Ext>::update_spanning_tree() {
|
||||
m_tree.update(m_enter_id, m_leave_id);
|
||||
m_tree->update(m_enter_id, m_leave_id);
|
||||
}
|
||||
|
||||
// FIXME: should declare pivot as a pivot_rule_impl and refactor
|
||||
|
@ -240,7 +240,7 @@ namespace smt {
|
|||
|
||||
template<typename Ext>
|
||||
bool network_flow<Ext>::check_well_formed() {
|
||||
SASSERT(m_tree.check_well_formed());
|
||||
SASSERT(m_tree->check_well_formed());
|
||||
SASSERT(!m_delta || !(*m_delta).is_neg());
|
||||
|
||||
// m_flows are zero on non-basic edges
|
||||
|
|
|
@ -25,8 +25,8 @@ Notes:
|
|||
namespace smt {
|
||||
|
||||
template<typename Ext>
|
||||
class thread_spanning_tree : public spanning_tree_base, private Ext {
|
||||
private:
|
||||
class thread_spanning_tree : public spanning_tree_base, protected Ext {
|
||||
protected:
|
||||
typedef dl_var node;
|
||||
typedef dl_edge<Ext> edge;
|
||||
typedef dl_graph<Ext> graph;
|
||||
|
@ -49,7 +49,7 @@ namespace smt {
|
|||
|
||||
void swap_order(node q, node v);
|
||||
node find_rev_thread(node n) const;
|
||||
void fix_depth(node start, node end);
|
||||
void fix_depth(node start, node after_end);
|
||||
node get_final(int start);
|
||||
bool is_preorder_traversal(node start, node end);
|
||||
node get_common_ancestor(node u, node v);
|
||||
|
@ -57,20 +57,29 @@ namespace smt {
|
|||
bool is_ancestor_of(node ancestor, node child);
|
||||
|
||||
public:
|
||||
thread_spanning_tree() {};
|
||||
thread_spanning_tree(graph & g);
|
||||
~thread_spanning_tree() {};
|
||||
|
||||
void initialize(svector<edge_id> const & tree);
|
||||
virtual void initialize(svector<edge_id> const & tree);
|
||||
void get_descendants(node start, svector<node> & descendants);
|
||||
|
||||
void update(edge_id enter_id, edge_id leave_id);
|
||||
virtual void update(edge_id enter_id, edge_id leave_id);
|
||||
void get_path(node start, node end, svector<edge_id> & path, svector<bool> & against);
|
||||
bool in_subtree_t2(node child);
|
||||
|
||||
bool check_well_formed();
|
||||
};
|
||||
|
||||
template<typename Ext>
|
||||
class basic_spanning_tree : public thread_spanning_tree<Ext> {
|
||||
private:
|
||||
graph * m_tree_graph;
|
||||
|
||||
public:
|
||||
basic_spanning_tree(graph & g);
|
||||
void initialize(svector<edge_id> const & tree);
|
||||
void update(edge_id enter_id, edge_id leave_id);
|
||||
};
|
||||
|
||||
}
|
||||
|
||||
#endif
|
||||
|
|
|
@ -47,14 +47,14 @@ namespace smt {
|
|||
typedef int node;
|
||||
|
||||
public:
|
||||
virtual void initialize(svector<edge_id> const & tree) {};
|
||||
virtual void get_descendants(node start, svector<node> & descendants) {};
|
||||
virtual void initialize(svector<edge_id> const & tree) = 0;
|
||||
virtual void get_descendants(node start, svector<node> & descendants) = 0;
|
||||
|
||||
virtual void update(edge_id enter_id, edge_id leave_id) {};
|
||||
virtual void get_path(node start, node end, svector<edge_id> & path, svector<bool> & against) {};
|
||||
virtual bool in_subtree_t2(node child) {UNREACHABLE(); return false;};
|
||||
virtual void update(edge_id enter_id, edge_id leave_id) = 0;
|
||||
virtual void get_path(node start, node end, svector<edge_id> & path, svector<bool> & against) = 0;
|
||||
virtual bool in_subtree_t2(node child) = 0;
|
||||
|
||||
virtual bool check_well_formed() {UNREACHABLE(); return false;};
|
||||
virtual bool check_well_formed() = 0;
|
||||
};
|
||||
}
|
||||
|
||||
|
|
|
@ -162,11 +162,26 @@ namespace smt {
|
|||
tout << u << ", " << v << ") leaves\n";
|
||||
});
|
||||
|
||||
// Old threads: alpha -> v -*-> f(v) -> beta | p -*-> f(p) -> gamma
|
||||
// New threads: alpha -> beta | p -*-> f(p) -> v -*-> f(v) -> gamma
|
||||
|
||||
node f_p = get_final(p);
|
||||
node f_v = get_final(v);
|
||||
node alpha = find_rev_thread(v);
|
||||
node beta = m_thread[f_v];
|
||||
node gamma = m_thread[f_p];
|
||||
|
||||
if (v != gamma) {
|
||||
m_thread[alpha] = beta;
|
||||
m_thread[f_p] = v;
|
||||
m_thread[f_v] = gamma;
|
||||
}
|
||||
|
||||
node old_pred = m_pred[q];
|
||||
// Update stem nodes from q to v
|
||||
if (q != v) {
|
||||
for (node n = q; n != u; ) {
|
||||
SASSERT(old_pred != u || n == v); // the last processed node is v
|
||||
for (node n = q; n != v; ) {
|
||||
SASSERT(old_pred != u); // the last processed node is v
|
||||
SASSERT(-1 != m_pred[old_pred]);
|
||||
int next_old_pred = m_pred[old_pred];
|
||||
swap_order(n, old_pred);
|
||||
|
@ -175,34 +190,18 @@ namespace smt {
|
|||
old_pred = next_old_pred;
|
||||
}
|
||||
}
|
||||
|
||||
// Old threads: alpha -> q -*-> f(q) -> beta | p -*-> f(p) -> gamma
|
||||
// New threads: alpha -> beta | p -*-> f(p) -> q -*-> f(q) -> gamma
|
||||
|
||||
node f_p = get_final(p);
|
||||
node f_q = get_final(q);
|
||||
node alpha = find_rev_thread(q);
|
||||
node beta = m_thread[f_q];
|
||||
node gamma = m_thread[f_p];
|
||||
|
||||
if (q != gamma) {
|
||||
m_thread[alpha] = beta;
|
||||
m_thread[f_p] = q;
|
||||
m_thread[f_q] = gamma;
|
||||
}
|
||||
|
||||
|
||||
m_pred[q] = p;
|
||||
m_tree[q] = enter_id;
|
||||
m_root_t2 = q;
|
||||
|
||||
node after_final_q = (v == gamma) ? beta : gamma;
|
||||
fix_depth(q, after_final_q);
|
||||
|
||||
SASSERT(!in_subtree_t2(p));
|
||||
SASSERT(in_subtree_t2(q));
|
||||
SASSERT(!in_subtree_t2(u));
|
||||
SASSERT(in_subtree_t2(v));
|
||||
|
||||
// Update the depth.
|
||||
|
||||
fix_depth(q, get_final(q));
|
||||
|
||||
TRACE("network_flow", {
|
||||
tout << pp_vector("Predecessors", m_pred, true) << pp_vector("Threads", m_thread);
|
||||
|
@ -210,6 +209,53 @@ namespace smt {
|
|||
});
|
||||
}
|
||||
|
||||
/**
|
||||
swap v and q in tree.
|
||||
- fixup m_thread
|
||||
- fixup m_pred
|
||||
|
||||
Case 1: final(q) == final(v)
|
||||
-------
|
||||
Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> next
|
||||
New thread: prev -> q -*-> final(q) -> v -*-> alpha -> next
|
||||
|
||||
Case 2: final(q) != final(v)
|
||||
-------
|
||||
Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> beta -*-> final(v) -> next
|
||||
New thread: prev -> q -*-> final(q) -> v -*-> alpha -> beta -*-> final(v) -> next
|
||||
|
||||
*/
|
||||
template<typename Ext>
|
||||
void thread_spanning_tree<Ext>::swap_order(node q, node v) {
|
||||
SASSERT(q != v);
|
||||
SASSERT(m_pred[q] == v);
|
||||
SASSERT(is_preorder_traversal(v, get_final(v)));
|
||||
node prev = find_rev_thread(v);
|
||||
node f_q = get_final(q);
|
||||
node f_v = get_final(v);
|
||||
node next = m_thread[f_v];
|
||||
node alpha = find_rev_thread(q);
|
||||
|
||||
if (f_q == f_v) {
|
||||
SASSERT(f_q != v && alpha != next);
|
||||
m_thread[f_q] = v;
|
||||
m_thread[alpha] = next;
|
||||
f_q = alpha;
|
||||
}
|
||||
else {
|
||||
node beta = m_thread[f_q];
|
||||
SASSERT(f_q != v && alpha != beta);
|
||||
m_thread[f_q] = v;
|
||||
m_thread[alpha] = beta;
|
||||
f_q = f_v;
|
||||
}
|
||||
SASSERT(prev != q);
|
||||
m_thread[prev] = q;
|
||||
m_pred[v] = q;
|
||||
// Notes: f_q has to be used since m_depth hasn't been updated yet.
|
||||
SASSERT(is_preorder_traversal(q, f_q));
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Check invariants of main data-structures.
|
||||
|
||||
|
@ -311,53 +357,6 @@ namespace smt {
|
|||
roots[y] = x;
|
||||
}
|
||||
|
||||
/**
|
||||
swap v and q in tree.
|
||||
- fixup m_thread
|
||||
- fixup m_pred
|
||||
|
||||
Case 1: final(q) == final(v)
|
||||
-------
|
||||
Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> next
|
||||
New thread: prev -> q -*-> final(q) -> v -*-> alpha -> next
|
||||
|
||||
Case 2: final(q) != final(v)
|
||||
-------
|
||||
Old thread: prev -> v -*-> alpha -> q -*-> final(q) -> beta -*-> final(v) -> next
|
||||
New thread: prev -> q -*-> final(q) -> v -*-> alpha -> beta -*-> final(v) -> next
|
||||
|
||||
*/
|
||||
template<typename Ext>
|
||||
void thread_spanning_tree<Ext>::swap_order(node q, node v) {
|
||||
SASSERT(q != v);
|
||||
SASSERT(m_pred[q] == v);
|
||||
SASSERT(is_preorder_traversal(v, get_final(v)));
|
||||
node prev = find_rev_thread(v);
|
||||
node f_q = get_final(q);
|
||||
node f_v = get_final(v);
|
||||
node next = m_thread[f_v];
|
||||
node alpha = find_rev_thread(q);
|
||||
|
||||
if (f_q == f_v) {
|
||||
SASSERT(f_q != v && alpha != next);
|
||||
m_thread[f_q] = v;
|
||||
m_thread[alpha] = next;
|
||||
f_q = alpha;
|
||||
}
|
||||
else {
|
||||
node beta = m_thread[f_q];
|
||||
SASSERT(f_q != v && alpha != beta);
|
||||
m_thread[f_q] = v;
|
||||
m_thread[alpha] = beta;
|
||||
f_q = f_v;
|
||||
}
|
||||
SASSERT(prev != q);
|
||||
m_thread[prev] = q;
|
||||
m_pred[v] = q;
|
||||
// Notes: f_q has to be used since m_depth hasn't been updated yet.
|
||||
SASSERT(is_preorder_traversal(q, f_q));
|
||||
}
|
||||
|
||||
/**
|
||||
\brief find node that points to 'n' in m_thread
|
||||
*/
|
||||
|
@ -372,12 +371,11 @@ namespace smt {
|
|||
}
|
||||
|
||||
template<typename Ext>
|
||||
void thread_spanning_tree<Ext>::fix_depth(node start, node end) {
|
||||
SASSERT(m_pred[start] != -1);
|
||||
m_depth[start] = m_depth[m_pred[start]]+1;
|
||||
while (start != end) {
|
||||
start = m_thread[start];
|
||||
void thread_spanning_tree<Ext>::fix_depth(node start, node after_end) {
|
||||
while (start != after_end) {
|
||||
SASSERT(m_pred[start] != -1);
|
||||
m_depth[start] = m_depth[m_pred[start]]+1;
|
||||
start = m_thread[start];
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -414,6 +412,63 @@ namespace smt {
|
|||
SASSERT(children.empty());
|
||||
return true;
|
||||
}
|
||||
|
||||
// Basic spanning tree
|
||||
template<typename Ext>
|
||||
basic_spanning_tree<Ext>::basic_spanning_tree(graph & g) : thread_spanning_tree<Ext>(g) {
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void basic_spanning_tree<Ext>::initialize(svector<edge_id> const & tree) {
|
||||
unsigned num_nodes = m_graph.get_num_nodes();
|
||||
m_tree_graph = alloc(graph);
|
||||
for (unsigned i = 0; i < num_nodes; ++i) {
|
||||
m_tree_graph->init_var(i);
|
||||
}
|
||||
|
||||
vector<edge> const & es = m_graph.get_all_edges();
|
||||
svector<edge_id>::const_iterator it = tree.begin(), end = tree.end();
|
||||
for(; it != end; ++it) {
|
||||
edge const & e = es[*it];
|
||||
m_tree_graph->add_edge(e.get_source(), e.get_target(), e.get_weight(), explanation());
|
||||
}
|
||||
|
||||
node root = num_nodes - 1;
|
||||
m_tree_graph->bfs_undirected(root, m_pred, m_depth);
|
||||
m_tree_graph->dfs_undirected(root, m_thread);
|
||||
}
|
||||
|
||||
template<typename Ext>
|
||||
void basic_spanning_tree<Ext>::update(edge_id enter_id, edge_id leave_id) {
|
||||
if (m_tree_graph)
|
||||
dealloc(m_tree_graph);
|
||||
m_tree_graph = alloc(graph);
|
||||
unsigned num_nodes = m_graph.get_num_nodes();
|
||||
for (unsigned i = 0; i < num_nodes; ++i) {
|
||||
m_tree_graph->init_var(i);
|
||||
}
|
||||
|
||||
vector<edge> const & es = m_graph.get_all_edges();
|
||||
svector<edge_id>::const_iterator it = m_tree.begin(), end = m_tree.end();
|
||||
for(; it != end; ++it) {
|
||||
edge const & e = es[*it];
|
||||
if (leave_id != *it) {
|
||||
m_tree_graph->add_edge(e.get_source(), e.get_target(), e.get_weight(), explanation());
|
||||
}
|
||||
}
|
||||
m_tree_graph->add_edge(m_graph.get_source(enter_id), m_graph.get_target(enter_id), m_graph.get_weight(enter_id), explanation());
|
||||
|
||||
node root = num_nodes - 1;
|
||||
m_tree_graph->bfs_undirected(root, m_pred, m_depth);
|
||||
m_tree_graph->dfs_undirected(root, m_thread);
|
||||
|
||||
for (node x = m_thread[root]; x != root; x = m_thread[x]) {
|
||||
edge_id id;
|
||||
VERIFY(m_graph.get_edge_id(x, m_pred[x], id));
|
||||
m_tree[x] = id;
|
||||
}
|
||||
}
|
||||
|
||||
}
|
||||
|
||||
#endif
|
|
@ -135,6 +135,7 @@ public:
|
|||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
try {
|
||||
IF_VERBOSE(0, verbose_stream() << "(smt.smt-tactic using the old SAT solver)\n";);
|
||||
SASSERT(in->is_well_sorted());
|
||||
ast_manager & m = in->m();
|
||||
TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " "
|
||||
|
|
733
src/smt/theory_pb.cpp
Normal file
733
src/smt/theory_pb.cpp
Normal file
|
@ -0,0 +1,733 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
theory_pb.cpp
|
||||
|
||||
Abstract:
|
||||
|
||||
Pseudo-Boolean theory plugin.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-11-05
|
||||
|
||||
Notes:
|
||||
|
||||
|
||||
--*/
|
||||
|
||||
#include "theory_pb.h"
|
||||
#include "smt_context.h"
|
||||
#include "ast_pp.h"
|
||||
#include "sorting_network.h"
|
||||
|
||||
namespace smt {
|
||||
|
||||
theory_pb::theory_pb(ast_manager& m):
|
||||
theory(m.mk_family_id("card")),
|
||||
m_util(m)
|
||||
{}
|
||||
|
||||
theory_pb::~theory_pb() {
|
||||
reset_eh();
|
||||
}
|
||||
|
||||
theory * theory_pb::mk_fresh(context * new_ctx) {
|
||||
return alloc(theory_pb, new_ctx->get_manager());
|
||||
}
|
||||
|
||||
bool theory_pb::internalize_atom(app * atom, bool gate_ctx) {
|
||||
context& ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
unsigned num_args = atom->get_num_args();
|
||||
SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom));
|
||||
|
||||
if (ctx.b_internalized(atom)) {
|
||||
return false;
|
||||
}
|
||||
|
||||
m_stats.m_num_predicates++;
|
||||
|
||||
SASSERT(!ctx.b_internalized(atom));
|
||||
bool_var abv = ctx.mk_bool_var(atom);
|
||||
|
||||
ineq* c = alloc(ineq, atom, literal(abv));
|
||||
c->m_k = m_util.get_k(atom);
|
||||
int& k = c->m_k;
|
||||
arg_t& args = c->m_args;
|
||||
|
||||
// extract literals and coefficients.
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
expr* arg = atom->get_arg(i);
|
||||
literal l = compile_arg(arg);
|
||||
int c = m_util.get_le_coeff(atom, i);
|
||||
args.push_back(std::make_pair(l, c));
|
||||
}
|
||||
// turn W <= k into -W >= -k
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
args[i].second = -args[i].second;
|
||||
}
|
||||
k = -k;
|
||||
lbool is_true = normalize_ineq(args, k);
|
||||
|
||||
literal lit(abv);
|
||||
switch(is_true) {
|
||||
case l_false:
|
||||
lit = ~lit;
|
||||
// fall-through
|
||||
case l_true:
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
TRACE("card", tout << mk_pp(atom, m) << " := " << lit << "\n";);
|
||||
dealloc(c);
|
||||
return true;
|
||||
case l_undef:
|
||||
break;
|
||||
}
|
||||
|
||||
// TBD: special cases: args.size() == 1
|
||||
|
||||
// maximal coefficient:
|
||||
int& max_coeff = c->m_max_coeff;
|
||||
max_coeff = 0;
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
max_coeff = std::max(max_coeff, args[i].second);
|
||||
}
|
||||
|
||||
// compute watch literals:
|
||||
int sum = 0;
|
||||
unsigned& wsz = c->m_watch_sz;
|
||||
wsz = 0;
|
||||
while (sum < k + max_coeff && wsz < args.size()) {
|
||||
sum += args[wsz].second;
|
||||
wsz++;
|
||||
}
|
||||
|
||||
for (unsigned i = 0; i < wsz; ++i) {
|
||||
add_watch(args[i].first, c);
|
||||
}
|
||||
|
||||
// pre-compile threshold for cardinality
|
||||
bool is_cardinality = true;
|
||||
for (unsigned i = 0; is_cardinality && i < args.size(); ++i) {
|
||||
is_cardinality = (args[i].second == 1);
|
||||
}
|
||||
if (is_cardinality) {
|
||||
unsigned log = 1, n = 1;
|
||||
while (n <= args.size()) {
|
||||
++log;
|
||||
n *= 2;
|
||||
}
|
||||
c->m_compilation_threshold = args.size()*log;
|
||||
TRACE("card", tout << "threshold:" << (args.size()*log) << "\n";);
|
||||
}
|
||||
else {
|
||||
c->m_compilation_threshold = UINT_MAX;
|
||||
}
|
||||
m_ineqs.insert(abv, c);
|
||||
m_ineqs_trail.push_back(abv);
|
||||
|
||||
TRACE("card", display(tout, *c););
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
literal theory_pb::compile_arg(expr* arg) {
|
||||
context& ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
if (!ctx.b_internalized(arg)) {
|
||||
ctx.internalize(arg, false);
|
||||
}
|
||||
bool_var bv;
|
||||
bool has_bv = false;
|
||||
bool negate = m.is_not(arg, arg);
|
||||
if (ctx.b_internalized(arg)) {
|
||||
bv = ctx.get_bool_var(arg);
|
||||
if (null_theory_var == ctx.get_var_theory(bv)) {
|
||||
ctx.set_var_theory(bv, get_id());
|
||||
}
|
||||
has_bv = (ctx.get_var_theory(bv) == get_id());
|
||||
}
|
||||
|
||||
// pre-processing should better remove negations under cardinality.
|
||||
// assumes relevancy level = 2 or 0.
|
||||
if (!has_bv) {
|
||||
expr_ref tmp(m), fml(m);
|
||||
tmp = m.mk_fresh_const("card_proxy",m.mk_bool_sort());
|
||||
fml = m.mk_iff(tmp, arg);
|
||||
ctx.internalize(fml, false);
|
||||
SASSERT(ctx.b_internalized(tmp));
|
||||
bv = ctx.get_bool_var(tmp);
|
||||
SASSERT(null_theory_var == ctx.get_var_theory(bv));
|
||||
ctx.set_var_theory(bv, get_id());
|
||||
literal lit(ctx.get_bool_var(fml));
|
||||
ctx.mk_th_axiom(get_id(), 1, &lit);
|
||||
ctx.mark_as_relevant(tmp);
|
||||
}
|
||||
return negate?~literal(bv):literal(bv);
|
||||
}
|
||||
|
||||
void theory_pb::add_watch(literal l, ineq* c) {
|
||||
unsigned idx = l.index();
|
||||
ptr_vector<ineq>* ineqs;
|
||||
if (!m_watch.find(idx, ineqs)) {
|
||||
ineqs = alloc(ptr_vector<ineq>);
|
||||
m_watch.insert(idx, ineqs);
|
||||
}
|
||||
ineqs->push_back(c);
|
||||
}
|
||||
|
||||
static unsigned gcd(unsigned a, unsigned b) {
|
||||
while (a != b) {
|
||||
if (a == 0) return b;
|
||||
if (b == 0) return a;
|
||||
SASSERT(a != 0 && b != 0);
|
||||
if (a < b) {
|
||||
b %= a;
|
||||
}
|
||||
else {
|
||||
a %= b;
|
||||
}
|
||||
}
|
||||
return a;
|
||||
}
|
||||
|
||||
lbool theory_pb::normalize_ineq(arg_t& args, int& k) {
|
||||
|
||||
// normalize first all literals to be positive:
|
||||
// then we can compare them more easily.
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
if (args[i].first.sign()) {
|
||||
args[i].first.neg();
|
||||
k -= args[i].second;
|
||||
args[i].second = -args[i].second;
|
||||
}
|
||||
}
|
||||
// sort and coalesce arguments:
|
||||
std::sort(args.begin(), args.end());
|
||||
for (unsigned i = 0; i + 1 < args.size(); ++i) {
|
||||
if (args[i].first == args[i+1].first) {
|
||||
args[i].second += args[i+1].second;
|
||||
for (unsigned j = i+1; j + 1 < args.size(); ++j) {
|
||||
args[j] = args[j+1];
|
||||
}
|
||||
args.resize(args.size()-1);
|
||||
}
|
||||
if (args[i].second == 0) {
|
||||
for (unsigned j = i; j + 1 < args.size(); ++j) {
|
||||
args[j] = args[j+1];
|
||||
}
|
||||
args.resize(args.size()-1);
|
||||
}
|
||||
}
|
||||
//
|
||||
// Ensure all coefficients are positive:
|
||||
// c*l + y >= k
|
||||
// <=>
|
||||
// c*(1-~l) + y >= k
|
||||
// <=>
|
||||
// c - c*~l + y >= k
|
||||
// <=>
|
||||
// -c*~l + y >= k - c
|
||||
//
|
||||
unsigned sum = 0;
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
int c = args[i].second;
|
||||
if (c < 0) {
|
||||
args[i].second = -c;
|
||||
args[i].first = ~args[i].first;
|
||||
k -= c;
|
||||
}
|
||||
sum += args[i].second;
|
||||
}
|
||||
// detect tautologies:
|
||||
if (k <= 0) {
|
||||
args.reset();
|
||||
return l_true;
|
||||
}
|
||||
// detect infeasible constraints:
|
||||
if (static_cast<int>(sum) < k) {
|
||||
args.reset();
|
||||
return l_false;
|
||||
}
|
||||
// Ensure the largest coefficient is not larger than k:
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
int c = args[i].second;
|
||||
if (c > k) {
|
||||
args[i].second = k;
|
||||
}
|
||||
}
|
||||
SASSERT(!args.empty());
|
||||
|
||||
// apply cutting plane reduction:
|
||||
unsigned g = 0;
|
||||
for (unsigned i = 0; g != 1 && i < args.size(); ++i) {
|
||||
int c = args[i].second;
|
||||
if (c != k) {
|
||||
g = gcd(g, c);
|
||||
}
|
||||
}
|
||||
if (g == 0) {
|
||||
// all coefficients are equal to k.
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
SASSERT(args[i].second == k);
|
||||
args[i].second = 1;
|
||||
}
|
||||
k = 1;
|
||||
}
|
||||
else if (g > 1) {
|
||||
//
|
||||
// Example 5x + 5y + 2z + 2u >= 5
|
||||
// becomes 3x + 3y + z + u >= 3
|
||||
//
|
||||
int k_new = k / g; // k_new is the ceiling of k / g.
|
||||
if (gcd(k, g) != g) {
|
||||
k_new++;
|
||||
}
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
int c = args[i].second;
|
||||
if (c == k) {
|
||||
c = k_new;
|
||||
}
|
||||
else {
|
||||
c = c / g;
|
||||
}
|
||||
args[i].second = c;
|
||||
}
|
||||
k = k_new;
|
||||
}
|
||||
|
||||
return l_undef;
|
||||
}
|
||||
|
||||
void theory_pb::collect_statistics(::statistics& st) const {
|
||||
st.update("pb axioms", m_stats.m_num_axioms);
|
||||
st.update("pb propagations", m_stats.m_num_propagations);
|
||||
st.update("pb predicates", m_stats.m_num_predicates);
|
||||
st.update("pb compilations", m_stats.m_num_compiles);
|
||||
}
|
||||
|
||||
void theory_pb::reset_eh() {
|
||||
|
||||
// m_watch;
|
||||
u_map<ptr_vector<ineq>*>::iterator it = m_watch.begin(), end = m_watch.end();
|
||||
for (; it != end; ++it) {
|
||||
dealloc(it->m_value);
|
||||
}
|
||||
u_map<ineq*>::iterator itc = m_ineqs.begin(), endc = m_ineqs.end();
|
||||
for (; itc != endc; ++itc) {
|
||||
dealloc(itc->m_value);
|
||||
}
|
||||
m_watch.reset();
|
||||
m_ineqs.reset();
|
||||
m_ineqs_trail.reset();
|
||||
m_ineqs_lim.reset();
|
||||
m_stats.reset();
|
||||
}
|
||||
|
||||
|
||||
#if 0
|
||||
void theory_pb::propagate_assignment(ineq& c) {
|
||||
if (c.m_compiled) {
|
||||
return;
|
||||
}
|
||||
if (should_compile(c)) {
|
||||
compile_ineq(c);
|
||||
return;
|
||||
}
|
||||
context& ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
arg_t const& args = c.m_args;
|
||||
bool_var abv = c.m_bv;
|
||||
int min = c.m_current_min;
|
||||
int max = c.m_current_max;
|
||||
int k = c.m_k;
|
||||
|
||||
TRACE("card",
|
||||
tout << mk_pp(c.m_app, m) << " min: "
|
||||
<< min << " max: " << max << "\n";);
|
||||
|
||||
//
|
||||
// if min > k && abv != l_false -> force abv false
|
||||
// if max <= k && abv != l_true -> force abv true
|
||||
// if min == k && abv == l_true -> force positive
|
||||
// unassigned literals false
|
||||
// if max == k + 1 && abv == l_false -> force negative
|
||||
// unassigned literals false
|
||||
//
|
||||
lbool aval = ctx.get_assignment(abv);
|
||||
if (min > k && aval != l_false) {
|
||||
literal_vector& lits = get_lits();
|
||||
int curr_min = accumulate_min(lits, c);
|
||||
SASSERT(curr_min > k);
|
||||
add_assign(c, lits, ~literal(abv));
|
||||
}
|
||||
else if (max <= k && aval != l_true) {
|
||||
literal_vector& lits = get_lits();
|
||||
int curr_max = accumulate_max(lits, c);
|
||||
SASSERT(curr_max <= k);
|
||||
add_assign(c, lits, literal(abv));
|
||||
}
|
||||
else if (min <= k && k < min + get_max_delta(c) && aval == l_true) {
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(~literal(abv));
|
||||
int curr_min = accumulate_min(lits, c);
|
||||
if (curr_min > k) {
|
||||
add_clause(c, lits);
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
bool_var bv = args[i].first;
|
||||
int inc = args[i].second;
|
||||
if (curr_min + inc > k && inc_min(inc, ctx.get_assignment(bv)) == l_undef) {
|
||||
add_assign(c, lits, literal(bv, inc > 0));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (max - get_max_delta(c) <= k && k < max && aval == l_false) {
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(literal(abv));
|
||||
int curr_max = accumulate_max(lits, c);
|
||||
if (curr_max <= k) {
|
||||
add_clause(c, lits);
|
||||
}
|
||||
else {
|
||||
for (unsigned i = 0; i < args.size(); ++i) {
|
||||
bool_var bv = args[i].first;
|
||||
int inc = args[i].second;
|
||||
if (curr_max - abs(inc) <= k && dec_max(inc, ctx.get_assignment(bv)) == l_undef) {
|
||||
add_assign(c, lits, literal(bv, inc < 0));
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
else if (aval == l_true) {
|
||||
SASSERT(min < k);
|
||||
literal_vector& lits = get_lits();
|
||||
int curr_min = accumulate_min(lits, c);
|
||||
bool all_inc = curr_min == k;
|
||||
unsigned num_incs = 0;
|
||||
for (unsigned i = 0; all_inc && i < args.size(); ++i) {
|
||||
bool_var bv = args[i].first;
|
||||
int inc = args[i].second;
|
||||
if (inc_min(inc, ctx.get_assignment(bv)) == l_undef) {
|
||||
all_inc = inc + min > k;
|
||||
num_incs++;
|
||||
}
|
||||
}
|
||||
if (num_incs > 0) {
|
||||
std::cout << "missed T propgations " << num_incs << "\n";
|
||||
}
|
||||
}
|
||||
else if (aval == l_false) {
|
||||
literal_vector& lits = get_lits();
|
||||
lits.push_back(literal(abv));
|
||||
int curr_max = accumulate_max(lits, c);
|
||||
bool all_dec = curr_max > k;
|
||||
unsigned num_decs = 0;
|
||||
for (unsigned i = 0; all_dec && i < args.size(); ++i) {
|
||||
bool_var bv = args[i].first;
|
||||
int inc = args[i].second;
|
||||
if (dec_max(inc, ctx.get_assignment(bv)) == l_undef) {
|
||||
all_dec = inc + max <= k;
|
||||
num_decs++;
|
||||
}
|
||||
}
|
||||
if (num_decs > 0) {
|
||||
std::cout << "missed F propgations " << num_decs << "\n";
|
||||
}
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
void theory_pb::assign_eh(bool_var v, bool is_true) {
|
||||
context& ctx = get_context();
|
||||
ast_manager& m = get_manager();
|
||||
ptr_vector<ineq>* ineqs = 0;
|
||||
ineq* c = 0;
|
||||
TRACE("card", tout << "assign: " << mk_pp(ctx.bool_var2expr(v), m) << " <- " << is_true << "\n";);
|
||||
|
||||
if (m_watch.find(v, ineqs)) {
|
||||
for (unsigned i = 0; i < ineqs->size(); ++i) {
|
||||
assign_watch(v, is_true, *ineqs, i);
|
||||
}
|
||||
}
|
||||
if (m_ineqs.find(v, c)) {
|
||||
// TBD: propagate_assignment(*c);
|
||||
}
|
||||
}
|
||||
|
||||
void theory_pb::assign_watch(bool_var v, bool is_true, watch_list& watch, unsigned index) {
|
||||
#if 0
|
||||
TBD
|
||||
ineq& c = *watch[i];
|
||||
c.m_sum;
|
||||
unsigned w;
|
||||
for (w = 0; w < c.m_watch_sz; ++i) {
|
||||
if (c.m_args[w].first.var() == v) {
|
||||
break;
|
||||
}
|
||||
}
|
||||
SASSERT(w < c.m_watch_sz);
|
||||
literal l = c.m_args[w].first;
|
||||
int coeff = c.m_args[w].second;
|
||||
if (is_true == !l.sign()) {
|
||||
ctx.push_trail(value_trail<context, int>(c.m_sum));
|
||||
c.m_sum += coeff;
|
||||
// optional propagate
|
||||
}
|
||||
else {
|
||||
unsigned deficit = c.m_max_sum - coeff;
|
||||
for (unsigned i = c.m_watch_sz; i < c.m_args.size(); ++i) {
|
||||
if
|
||||
}
|
||||
// find a different literal to watch.
|
||||
ctx.push_trail(value_trail<context, unsigned>(c.m_watch_sz));
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
struct theory_pb::sort_expr {
|
||||
theory_pb& th;
|
||||
context& ctx;
|
||||
ast_manager& m;
|
||||
expr_ref_vector m_trail;
|
||||
sort_expr(theory_pb& th):
|
||||
th(th),
|
||||
ctx(th.get_context()),
|
||||
m(th.get_manager()),
|
||||
m_trail(m) {}
|
||||
typedef expr* T;
|
||||
typedef expr_ref_vector vector;
|
||||
|
||||
T mk_ite(T a, T b, T c) {
|
||||
if (m.is_true(a)) {
|
||||
return b;
|
||||
}
|
||||
if (m.is_false(a)) {
|
||||
return c;
|
||||
}
|
||||
if (b == c) {
|
||||
return b;
|
||||
}
|
||||
m_trail.push_back(m.mk_ite(a, b, c));
|
||||
return m_trail.back();
|
||||
}
|
||||
|
||||
T mk_le(T a, T b) {
|
||||
return mk_ite(b, a, m.mk_true());
|
||||
}
|
||||
|
||||
T mk_default() {
|
||||
return m.mk_false();
|
||||
}
|
||||
|
||||
literal internalize(ineq& ca, expr* e) {
|
||||
obj_map<expr, literal> cache;
|
||||
for (unsigned i = 0; i < ca.m_args.size(); ++i) {
|
||||
cache.insert(ca.m_app->get_arg(i), literal(ca.m_args[i].first));
|
||||
}
|
||||
cache.insert(m.mk_false(), false_literal);
|
||||
cache.insert(m.mk_true(), true_literal);
|
||||
ptr_vector<expr> todo;
|
||||
todo.push_back(e);
|
||||
expr *a, *b, *c;
|
||||
literal la, lb, lc;
|
||||
while (!todo.empty()) {
|
||||
expr* t = todo.back();
|
||||
if (cache.contains(t)) {
|
||||
todo.pop_back();
|
||||
continue;
|
||||
}
|
||||
VERIFY(m.is_ite(t, a, b, c));
|
||||
unsigned sz = todo.size();
|
||||
if (!cache.find(a, la)) {
|
||||
todo.push_back(a);
|
||||
}
|
||||
if (!cache.find(b, lb)) {
|
||||
todo.push_back(b);
|
||||
}
|
||||
if (!cache.find(c, lc)) {
|
||||
todo.push_back(c);
|
||||
}
|
||||
if (sz != todo.size()) {
|
||||
continue;
|
||||
}
|
||||
todo.pop_back();
|
||||
cache.insert(t, mk_ite(ca, t, la, lb, lc));
|
||||
}
|
||||
return cache.find(e);
|
||||
}
|
||||
|
||||
literal mk_ite(ineq& ca, expr* t, literal a, literal b, literal c) {
|
||||
if (a == true_literal) {
|
||||
return b;
|
||||
}
|
||||
else if (a == false_literal) {
|
||||
return c;
|
||||
}
|
||||
else if (b == true_literal && c == false_literal) {
|
||||
return a;
|
||||
}
|
||||
else if (b == false_literal && c == true_literal) {
|
||||
return ~a;
|
||||
}
|
||||
else if (b == c) {
|
||||
return b;
|
||||
}
|
||||
else {
|
||||
literal l;
|
||||
if (ctx.b_internalized(t)) {
|
||||
l = literal(ctx.get_bool_var(t));
|
||||
}
|
||||
else {
|
||||
l = literal(ctx.mk_bool_var(t));
|
||||
}
|
||||
add_clause(~l, ~a, b);
|
||||
add_clause(~l, a, c);
|
||||
add_clause(l, ~a, ~b);
|
||||
add_clause(l, a, ~c);
|
||||
TRACE("card", tout << mk_pp(t, m) << " ::= (if ";
|
||||
ctx.display_detailed_literal(tout, a);
|
||||
ctx.display_detailed_literal(tout << " ", b);
|
||||
ctx.display_detailed_literal(tout << " ", c);
|
||||
tout << ")\n";);
|
||||
return l;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
// auxiliary clauses don't get garbage collected.
|
||||
void add_clause(literal a, literal b, literal c) {
|
||||
literal_vector& lits = th.get_lits();
|
||||
if (a != null_literal) lits.push_back(a);
|
||||
if (b != null_literal) lits.push_back(b);
|
||||
if (c != null_literal) lits.push_back(c);
|
||||
justification* js = 0;
|
||||
TRACE("card",
|
||||
ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
|
||||
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX, 0);
|
||||
}
|
||||
|
||||
void add_clause(literal l1, literal l2) {
|
||||
add_clause(l1, l2, null_literal);
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
||||
bool theory_pb::should_compile(ineq& c) {
|
||||
#if 1
|
||||
return false;
|
||||
#else
|
||||
return c.m_num_propagations > c.m_compilation_threshold;
|
||||
#endif
|
||||
}
|
||||
|
||||
void theory_pb::compile_ineq(ineq& c) {
|
||||
++m_stats.m_num_compiles;
|
||||
ast_manager& m = get_manager();
|
||||
context& ctx = get_context();
|
||||
app* a = c.m_app;
|
||||
SASSERT(m_util.is_at_most_k(a));
|
||||
literal atmostk;
|
||||
int k = m_util.get_k(a);
|
||||
unsigned num_args = a->get_num_args();
|
||||
|
||||
sort_expr se(*this);
|
||||
if (k >= static_cast<int>(num_args)) {
|
||||
atmostk = true_literal;
|
||||
}
|
||||
else if (k < 0) {
|
||||
atmostk = false_literal;
|
||||
}
|
||||
else {
|
||||
sorting_network<sort_expr> sn(se);
|
||||
expr_ref_vector in(m), out(m);
|
||||
for (unsigned i = 0; i < num_args; ++i) {
|
||||
in.push_back(c.m_app->get_arg(i));
|
||||
}
|
||||
sn(in, out);
|
||||
atmostk = ~se.internalize(c, out[k].get()); // k'th output is 0.
|
||||
TRACE("card", tout << "~atmost: " << mk_pp(out[k].get(), m) << "\n";);
|
||||
}
|
||||
literal thl = c.m_lit;
|
||||
se.add_clause(~thl, atmostk);
|
||||
se.add_clause(thl, ~atmostk);
|
||||
TRACE("card", tout << mk_pp(a, m) << "\n";);
|
||||
// auxiliary clauses get removed when popping scopes.
|
||||
// we have to recompile the circuit after back-tracking.
|
||||
ctx.push_trail(value_trail<context, bool>(c.m_compiled));
|
||||
c.m_compiled = true;
|
||||
}
|
||||
|
||||
|
||||
void theory_pb::init_search_eh() {
|
||||
|
||||
}
|
||||
|
||||
void theory_pb::push_scope_eh() {
|
||||
m_ineqs_lim.push_back(m_ineqs_trail.size());
|
||||
}
|
||||
|
||||
void theory_pb::pop_scope_eh(unsigned num_scopes) {
|
||||
unsigned sz = m_ineqs_lim[m_ineqs_lim.size()-num_scopes];
|
||||
while (m_ineqs_trail.size() > sz) {
|
||||
SASSERT(m_ineqs.contains(m_ineqs_trail.back()));
|
||||
m_ineqs.remove(m_ineqs_trail.back());
|
||||
m_ineqs_trail.pop_back();
|
||||
}
|
||||
m_ineqs_lim.resize(m_ineqs_lim.size()-num_scopes);
|
||||
}
|
||||
|
||||
std::ostream& theory_pb::display(std::ostream& out, ineq& c) const {
|
||||
ast_manager& m = get_manager();
|
||||
out << mk_pp(c.m_app, m) << "\n";
|
||||
for (unsigned i = 0; i < c.m_args.size(); ++i) {
|
||||
out << c.m_args[i].second << "*" << c.m_args[i].first;
|
||||
if (i + 1 < c.m_args.size()) {
|
||||
out << " + ";
|
||||
}
|
||||
}
|
||||
out << " >= " << c.m_k << "\n"
|
||||
<< "propagations: " << c.m_num_propagations
|
||||
<< " max_coeff: " << c.m_max_coeff
|
||||
<< " watch size: " << c.m_watch_sz
|
||||
<< "\n";
|
||||
return out;
|
||||
}
|
||||
|
||||
|
||||
literal_vector& theory_pb::get_lits() {
|
||||
m_literals.reset();
|
||||
return m_literals;
|
||||
}
|
||||
|
||||
void theory_pb::add_assign(ineq& c, literal_vector const& lits, literal l) {
|
||||
literal_vector ls;
|
||||
++c.m_num_propagations;
|
||||
m_stats.m_num_propagations++;
|
||||
context& ctx = get_context();
|
||||
for (unsigned i = 0; i < lits.size(); ++i) {
|
||||
ls.push_back(~lits[i]);
|
||||
}
|
||||
ctx.assign(l, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), ls.size(), ls.c_ptr(), l)));
|
||||
}
|
||||
|
||||
|
||||
|
||||
void theory_pb::add_clause(ineq& c, literal_vector const& lits) {
|
||||
++c.m_num_propagations;
|
||||
m_stats.m_num_axioms++;
|
||||
context& ctx = get_context();
|
||||
TRACE("card", tout << "#prop:" << c.m_num_propagations << " - "; ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr()); tout << "\n";);
|
||||
justification* js = 0;
|
||||
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
|
||||
IF_VERBOSE(2, ctx.display_literals_verbose(verbose_stream(),
|
||||
lits.size(), lits.c_ptr());
|
||||
verbose_stream() << "\n";);
|
||||
// ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
|
||||
}
|
||||
}
|
118
src/smt/theory_pb.h
Normal file
118
src/smt/theory_pb.h
Normal file
|
@ -0,0 +1,118 @@
|
|||
/*++
|
||||
Copyright (c) 2013 Microsoft Corporation
|
||||
|
||||
Module Name:
|
||||
|
||||
theory_pb.h
|
||||
|
||||
Abstract:
|
||||
|
||||
Cardinality theory plugin.
|
||||
|
||||
Author:
|
||||
|
||||
Nikolaj Bjorner (nbjorner) 2013-11-05
|
||||
|
||||
Notes:
|
||||
|
||||
This custom theory handles cardinality constraints
|
||||
It performs unit propagation and switches to creating
|
||||
sorting circuits if it keeps having to propagate (create new clauses).
|
||||
--*/
|
||||
|
||||
#include "smt_theory.h"
|
||||
#include "card_decl_plugin.h"
|
||||
#include "smt_clause.h"
|
||||
|
||||
namespace smt {
|
||||
class theory_pb : public theory {
|
||||
|
||||
struct sort_expr;
|
||||
typedef svector<std::pair<literal, int> > arg_t;
|
||||
|
||||
struct stats {
|
||||
unsigned m_num_axioms;
|
||||
unsigned m_num_propagations;
|
||||
unsigned m_num_predicates;
|
||||
unsigned m_num_compiles;
|
||||
void reset() { memset(this, 0, sizeof(*this)); }
|
||||
stats() { reset(); }
|
||||
};
|
||||
|
||||
|
||||
struct ineq {
|
||||
app* m_app;
|
||||
literal m_lit; // literal repesenting predicate
|
||||
arg_t m_args; // encode args[0]*coeffs[0]+...+args[n-1]*coeffs[n-1] >= m_k;
|
||||
int m_k; // invariants: m_k > 0, coeffs[i] > 0
|
||||
|
||||
// Watch the first few positions until the sum satisfies:
|
||||
// sum coeffs[i] >= m_lower + max_coeff
|
||||
|
||||
int m_max_coeff; // maximal coefficient.
|
||||
unsigned m_watch_sz; // number of literals being watched.
|
||||
unsigned m_num_propagations;
|
||||
unsigned m_compilation_threshold;
|
||||
bool m_compiled;
|
||||
|
||||
ineq(app* a, literal l):
|
||||
m_app(a),
|
||||
m_lit(l),
|
||||
m_num_propagations(0),
|
||||
m_compilation_threshold(UINT_MAX),
|
||||
m_compiled(false)
|
||||
{}
|
||||
};
|
||||
|
||||
typedef ptr_vector<ineq> watch_list;
|
||||
|
||||
u_map<watch_list*> m_watch; // per literal.
|
||||
u_map<ineq*> m_ineqs; // per inequality.
|
||||
unsigned_vector m_ineqs_trail;
|
||||
unsigned_vector m_ineqs_lim;
|
||||
literal_vector m_literals; // temporary vector
|
||||
card_util m_util;
|
||||
stats m_stats;
|
||||
|
||||
// internalize_atom:
|
||||
lbool normalize_ineq(arg_t& args, int& k);
|
||||
literal compile_arg(expr* arg);
|
||||
void add_watch(literal l, ineq* c);
|
||||
void assign_watch(bool_var v, bool is_true, watch_list& watch, unsigned index);
|
||||
|
||||
std::ostream& display(std::ostream& out, ineq& c) const;
|
||||
|
||||
void add_clause(ineq& c, literal_vector const& lits);
|
||||
void add_assign(ineq& c, literal_vector const& lits, literal l);
|
||||
literal_vector& get_lits();
|
||||
|
||||
//
|
||||
// Utilities to compile cardinality
|
||||
// constraints into a sorting network.
|
||||
//
|
||||
void compile_ineq(ineq& c);
|
||||
bool should_compile(ineq& c);
|
||||
unsigned get_compilation_threshold(ineq& c);
|
||||
public:
|
||||
theory_pb(ast_manager& m);
|
||||
|
||||
virtual ~theory_pb();
|
||||
|
||||
virtual theory * mk_fresh(context * new_ctx);
|
||||
virtual bool internalize_atom(app * atom, bool gate_ctx);
|
||||
virtual bool internalize_term(app * term) { UNREACHABLE(); return false; }
|
||||
virtual void new_eq_eh(theory_var v1, theory_var v2) { }
|
||||
virtual void new_diseq_eh(theory_var v1, theory_var v2) { }
|
||||
virtual bool use_diseqs() const { return false; }
|
||||
virtual bool build_models() const { return false; }
|
||||
virtual final_check_status final_check_eh() { return FC_DONE; }
|
||||
|
||||
virtual void reset_eh();
|
||||
virtual void assign_eh(bool_var v, bool is_true);
|
||||
virtual void init_search_eh();
|
||||
virtual void push_scope_eh();
|
||||
virtual void pop_scope_eh(unsigned num_scopes);
|
||||
virtual void collect_statistics(::statistics & st) const;
|
||||
|
||||
};
|
||||
};
|
|
@ -40,6 +40,7 @@ class tactic2solver : public solver_na2as {
|
|||
bool m_produce_models;
|
||||
bool m_produce_proofs;
|
||||
bool m_produce_unsat_cores;
|
||||
statistics m_stats;
|
||||
public:
|
||||
tactic2solver(ast_manager & m, tactic * t, params_ref const & p, bool produce_proofs, bool produce_models, bool produce_unsat_cores, symbol const & logic);
|
||||
virtual ~tactic2solver();
|
||||
|
@ -161,6 +162,7 @@ lbool tactic2solver::check_sat_core(unsigned num_assumptions, expr * const * ass
|
|||
m_result->m_unknown = ex.msg();
|
||||
}
|
||||
m_tactic->collect_statistics(m_result->m_stats);
|
||||
m_tactic->collect_statistics(m_stats);
|
||||
m_result->m_model = md;
|
||||
m_result->m_proof = pr;
|
||||
if (m_produce_unsat_cores) {
|
||||
|
@ -177,9 +179,9 @@ void tactic2solver::set_cancel(bool f) {
|
|||
m_tactic->set_cancel(f);
|
||||
}
|
||||
|
||||
void tactic2solver::collect_statistics(statistics & st) const {
|
||||
if (m_result.get())
|
||||
m_result->collect_statistics(st);
|
||||
void tactic2solver::collect_statistics(statistics & st) const {
|
||||
st.copy(m_stats);
|
||||
SASSERT(m_stats.size() > 0);
|
||||
}
|
||||
|
||||
void tactic2solver::get_unsat_core(ptr_vector<expr> & r) {
|
||||
|
|
|
@ -31,15 +31,6 @@ Notes:
|
|||
|
||||
#define MEMLIMIT 300
|
||||
|
||||
tactic * mk_new_sat_tactic(ast_manager & m) {
|
||||
IF_VERBOSE(0, verbose_stream() << "Try to use the new SAT solver." << std::endl;);
|
||||
tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()),
|
||||
and_then(mk_simplify_tactic(m),
|
||||
mk_smt_tactic()),
|
||||
mk_sat_tactic(m));
|
||||
return new_sat;
|
||||
}
|
||||
|
||||
tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
|
||||
params_ref main_p;
|
||||
main_p.set_bool("elim_and", true);
|
||||
|
@ -94,7 +85,10 @@ tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) {
|
|||
tactic * new_sat = and_then(mk_simplify_tactic(m),
|
||||
mk_smt_tactic());
|
||||
#else
|
||||
tactic * new_sat = mk_new_sat_tactic(m);
|
||||
tactic * new_sat = cond(mk_or(mk_produce_proofs_probe(), mk_produce_unsat_cores_probe()),
|
||||
and_then(mk_simplify_tactic(m),
|
||||
mk_smt_tactic()),
|
||||
mk_sat_tactic(m));
|
||||
#endif
|
||||
|
||||
tactic * st = using_params(and_then(preamble_st,
|
||||
|
|
Loading…
Reference in a new issue