diff --git a/LICENSE.txt b/LICENSE.txt index 91c8070d0..cc90bed74 100644 --- a/LICENSE.txt +++ b/LICENSE.txt @@ -2,6 +2,9 @@ Z3 Copyright (c) Microsoft Corporation All rights reserved. MIT License -Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the ""Software""), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: + The above copyright notice and this permission notice shall be included in all copies or substantial portions of the Software. -THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + +THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. \ No newline at end of file diff --git a/contrib/cmake/src/test/CMakeLists.txt b/contrib/cmake/src/test/CMakeLists.txt index 6ea07e84c..46781b2cc 100644 --- a/contrib/cmake/src/test/CMakeLists.txt +++ b/contrib/cmake/src/test/CMakeLists.txt @@ -23,6 +23,7 @@ add_executable(test-z3 bv_simplifier_plugin.cpp chashtable.cpp check_assumptions.cpp + cnf_backbones.cpp datalog_parser.cpp ddnf.cpp diff_logic.cpp diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 568ffe9a2..b4cdf834b 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6194,7 +6194,7 @@ class Solver(Z3PPObject): >>> s.consequences([a],[b,c,d]) (sat, [Implies(a, b), Implies(a, c)]) >>> s.consequences([Not(c),d],[a,b,c,d]) - (sat, [Implies(Not(c), Not(c)), Implies(d, d), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))]) + (sat, [Implies(d, d), Implies(Not(c), Not(c)), Implies(Not(c), Not(b)), Implies(Not(c), Not(a))]) """ if isinstance(assumptions, list): _asms = AstVector(None, self.ctx) diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp index 11cb2f6a2..26ef7386c 100755 --- a/src/interp/iz3proof_itp.cpp +++ b/src/interp/iz3proof_itp.cpp @@ -541,6 +541,7 @@ class iz3proof_itp_impl : public iz3proof_itp { placeholder_arg |= is_placeholder(args[i]); } try { + TRACE("duality", print_expr(tout, e); tout << "\n";); opr f = op(e); if(f == Equal && args[0] == args[1]) res = mk_true(); else if(f == And) res = my_and(args); @@ -853,6 +854,7 @@ class iz3proof_itp_impl : public iz3proof_itp { ast simplify_rotate_eq2leq(const ast &pl, const ast &neg_equality, const ast &pf){ if(pl == arg(pf,1)){ + TRACE("duality", print_expr(tout, pl); print_expr(tout << "\n", neg_equality); print_expr(tout << "\n", pf); tout << "\n";); ast cond = mk_true(); ast equa = sep_cond(arg(pf,0),cond); if(is_equivrel_chain(equa)){ @@ -1870,10 +1872,13 @@ class iz3proof_itp_impl : public iz3proof_itp { ast chain_ineqs(opr comp_op, LitType t, const ast &chain, const ast &lhs, const ast &rhs){ if(is_true(chain)){ - if(lhs != rhs) + if (lhs != rhs) { + TRACE("duality", print_expr(tout, lhs); tout << " "; print_expr(tout, rhs); tout << "\n";); throw bad_ineq_inference(); + } return make(Leq,make_int(rational(0)),make_int(rational(0))); } + TRACE("duality", print_expr(tout, chain); print_expr(tout << "\n", lhs); tout << " "; print_expr(tout, rhs); tout << "\n";); ast last = chain_last(chain); ast rest = chain_rest(chain); ast mid = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last)); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index af3c57baa..1310727aa 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1235,7 +1235,7 @@ namespace opt { out << " ("; display_objective(out, obj); if (get_lower_as_num(i) != get_upper_as_num(i)) { - out << " (" << get_lower(i) << " " << get_upper(i) << ")"; + out << " (interval " << get_lower(i) << " " << get_upper(i) << ")"; } else { out << " " << get_lower(i); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 08c70fba5..739a591e7 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3284,13 +3284,17 @@ namespace sat { checkpoint(); literal_set::iterator it = unfixed_lits.begin(), end = unfixed_lits.end(); unsigned num_resolves = 0; + unsigned num_fixed = 0; + unsigned num_assigned = 0; lbool is_sat = l_true; for (; it != end; ++it) { - literal lit = *it; + literal lit = *it; if (value(lit) != l_undef) { + ++num_fixed; continue; } push(); + ++num_assigned; assign(~lit, justification()); propagate(false); while (inconsistent()) { @@ -3307,8 +3311,18 @@ namespace sat { break; } } + if (scope_lvl() == 1) { + it = unfixed_lits.begin(); + for (; it != end; ++it) { + literal lit = *it; + if (value(lit) == l_true) { + VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq)); + } + } + } if (is_sat == l_true) { if (scope_lvl() == 1 && num_resolves > 0) { + IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences backjump)\n";); is_sat = l_undef; } else { @@ -3325,12 +3339,14 @@ namespace sat { if (is_sat == l_true) { delete_unfixed(unfixed_lits, unfixed_vars); } - extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq); + extract_fixed_consequences(num_units, assumptions, unfixed_vars, conseq); update_unfixed_literals(unfixed_lits, unfixed_vars); IF_VERBOSE(1, verbose_stream() << "(sat.get-consequences" << " iterations: " << num_iterations << " variables: " << unfixed_lits.size() << " fixed: " << conseq.size() + << " status: " << is_sat + << " pre-assigned: " << num_fixed << " unfixed: " << lits.size() - conseq.size() - unfixed_lits.size() << ")\n";); diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index 42291609d..c7f472a60 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -247,6 +247,7 @@ namespace sat { unsigned num_clauses() const; unsigned num_restarts() const { return m_restarts; } bool is_external(bool_var v) const { return m_external[v] != 0; } + void set_external(bool_var v) { m_external[v] = true; } bool was_eliminated(bool_var v) const { return m_eliminated[v] != 0; } unsigned scope_lvl() const { return m_scope_lvl; } lbool value(literal l) const { return static_cast(m_assignment[l.index()]); } diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index 9558f6a3b..65272207e 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -30,6 +30,7 @@ namespace smt { index_set::iterator it = vars.begin(), end = vars.end(); for (; it != end; ++it) { expr* e = bool_var2expr(*it); + e = m_assumption2orig.find(e); premises.push_back(get_assignment(*it) != l_false ? e : m_manager.mk_not(e)); } return mk_and(premises); @@ -44,13 +45,14 @@ namespace smt { // - e is an equality between a variable and value that is to be fixed. // - e is a data-type recognizer of a variable that is to be fixed. // - void context::extract_fixed_consequences(literal lit, obj_map& vars, index_set const& assumptions, expr_ref_vector& conseq) { + void context::extract_fixed_consequences(literal lit, index_set const& assumptions, expr_ref_vector& conseq) { ast_manager& m = m_manager; datatype_util dt(m); expr* e1, *e2; expr_ref fml(m); if (lit == true_literal) return; expr* e = bool_var2expr(lit.var()); + TRACE("context", display(tout << mk_pp(e, m) << "\n");); index_set s; if (assumptions.contains(lit.var())) { s.insert(lit.var()); @@ -65,26 +67,32 @@ namespace smt { } tout << "\n";); bool found = false; - if (vars.contains(e)) { + if (m_var2val.contains(e)) { found = true; + m_var2val.erase(e); + e = m_var2orig.find(e); fml = lit.sign() ? m.mk_not(e) : e; - vars.erase(e); } else if (!lit.sign() && m.is_eq(e, e1, e2)) { - if (vars.contains(e2)) { - std::swap(e1, e2); - } - if (vars.contains(e1) && m.is_value(e2)) { + if (m_var2val.contains(e2) && m.is_value(e1)) { found = true; - fml = e; - vars.erase(e1); + m_var2val.erase(e2); + e2 = m_var2orig.find(e2); + std::swap(e1, e2); + fml = m.mk_eq(e1, e2); + } + else if (m_var2val.contains(e1) && m.is_value(e2)) { + found = true; + m_var2val.erase(e1); + e1 = m_var2orig.find(e1); + fml = m.mk_eq(e1, e2); } } else if (!lit.sign() && is_app(e) && dt.is_recognizer(to_app(e)->get_decl())) { - if (vars.contains(to_app(e)->get_arg(0))) { + if (m_var2val.contains(to_app(e)->get_arg(0))) { found = true; fml = m.mk_eq(to_app(e)->get_arg(0), m.mk_const(dt.get_recognizer_constructor(to_app(e)->get_decl()))); - vars.erase(to_app(e)->get_arg(0)); + m_var2val.erase(to_app(e)->get_arg(0)); } } if (found) { @@ -94,6 +102,7 @@ namespace smt { } void context::justify(literal lit, index_set& s) { + ast_manager& m = m_manager; b_justification js = get_justification(lit.var()); switch (js.get_kind()) { case b_justification::CLAUSE: { @@ -119,6 +128,9 @@ namespace smt { literal_vector literals; m_conflict_resolution->justification2literals(js.get_justification(), literals); for (unsigned j = 0; j < literals.size(); ++j) { + if (!m_antecedents.contains(literals[j].var())) { + TRACE("context", tout << literals[j] << " " << mk_pp(bool_var2expr(literals[j].var()), m) << "\n";); + } s |= m_antecedents.find(literals[j].var()); } break; @@ -126,13 +138,13 @@ namespace smt { } } - void context::extract_fixed_consequences(unsigned& start, obj_map& vars, index_set const& assumptions, expr_ref_vector& conseq) { + void context::extract_fixed_consequences(unsigned& start, index_set const& assumptions, expr_ref_vector& conseq) { pop_to_search_lvl(); SASSERT(!inconsistent()); literal_vector const& lits = assigned_literals(); unsigned sz = lits.size(); for (unsigned i = start; i < sz; ++i) { - extract_fixed_consequences(lits[i], vars, assumptions, conseq); + extract_fixed_consequences(lits[i], assumptions, conseq); } start = sz; SASSERT(!inconsistent()); @@ -150,10 +162,10 @@ namespace smt { // rules out as many non-fixed variables as possible. // - unsigned context::delete_unfixed(obj_map& var2val, expr_ref_vector& unfixed) { + unsigned context::delete_unfixed(expr_ref_vector& unfixed) { ast_manager& m = m_manager; ptr_vector to_delete; - obj_map::iterator it = var2val.begin(), end = var2val.end(); + obj_map::iterator it = m_var2val.begin(), end = m_var2val.end(); for (; it != end; ++it) { expr* k = it->m_key; expr* v = it->m_value; @@ -189,7 +201,7 @@ namespace smt { } } for (unsigned i = 0; i < to_delete.size(); ++i) { - var2val.remove(to_delete[i]); + m_var2val.remove(to_delete[i]); unfixed.push_back(to_delete[i]); } return to_delete.size(); @@ -202,12 +214,12 @@ namespace smt { // Add a clause to short-circuit the congruence justifications for // next rounds. // - unsigned context::extract_fixed_eqs(obj_map& var2val, expr_ref_vector& conseq) { + unsigned context::extract_fixed_eqs(expr_ref_vector& conseq) { TRACE("context", tout << "extract fixed consequences\n";); ast_manager& m = m_manager; ptr_vector to_delete; expr_ref fml(m), eq(m); - obj_map::iterator it = var2val.begin(), end = var2val.end(); + obj_map::iterator it = m_var2val.begin(), end = m_var2val.end(); for (; it != end; ++it) { expr* k = it->m_key; expr* v = it->m_value; @@ -220,7 +232,7 @@ namespace smt { s |= m_antecedents.find(literals[i].var()); } - fml = m.mk_eq(k, v); + fml = m.mk_eq(m_var2orig.find(k), v); fml = m.mk_implies(antecedent2fml(s), fml); conseq.push_back(fml); to_delete.push_back(k); @@ -235,16 +247,20 @@ namespace smt { } } for (unsigned i = 0; i < to_delete.size(); ++i) { - var2val.remove(to_delete[i]); + m_var2val.remove(to_delete[i]); } return to_delete.size(); } literal context::mk_diseq(expr* e, expr* val) { ast_manager& m = m_manager; - if (m.is_bool(e)) { + if (m.is_bool(e) && b_internalized(e)) { return literal(get_bool_var(e), m.is_true(val)); } + else if (m.is_bool(e)) { + internalize_formula(e, false); + return literal(get_bool_var(e), !m.is_true(val)); + } else { expr_ref eq(mk_eq_atom(e, val), m); internalize_formula(eq, false); @@ -252,43 +268,85 @@ namespace smt { } } - lbool context::get_consequences(expr_ref_vector const& assumptions, - expr_ref_vector const& vars, + lbool context::get_consequences(expr_ref_vector const& assumptions0, + expr_ref_vector const& vars0, expr_ref_vector& conseq, expr_ref_vector& unfixed) { m_antecedents.reset(); + m_antecedents.insert(true_literal.var(), index_set()); pop_to_base_lvl(); + ast_manager& m = m_manager; + expr_ref_vector vars(m), assumptions(m); + m_var2val.reset(); + m_var2orig.reset(); + m_assumption2orig.reset(); + bool pushed = false; + for (unsigned i = 0; i < vars0.size(); ++i) { + expr* v = vars0[i]; + if (is_uninterp_const(v)) { + vars.push_back(v); + m_var2orig.insert(v, v); + } + else { + if (!pushed) { + pushed = true; + push(); + } + expr_ref c(m.mk_fresh_const("v", m.get_sort(v)), m); + expr_ref eq(m.mk_eq(c, v), m); + assert_expr(eq); + vars.push_back(c); + m_var2orig.insert(c, v); + } + } + for (unsigned i = 0; i < assumptions0.size(); ++i) { + expr* a = assumptions0[i]; + if (is_uninterp_const(a)) { + assumptions.push_back(a); + m_assumption2orig.insert(a, a); + } + else { + if (!pushed) { + pushed = true; + push(); + } + expr_ref c(m.mk_fresh_const("a", m.get_sort(a)), m); + expr_ref eq(m.mk_eq(c, a), m); + assert_expr(eq); + assumptions.push_back(c); + m_assumption2orig.insert(c, a); + } + } lbool is_sat = check(assumptions.size(), assumptions.c_ptr()); if (is_sat != l_true) { TRACE("context", tout << is_sat << "\n";); + if (pushed) pop(1); return is_sat; } - obj_map var2val; index_set _assumptions; for (unsigned i = 0; i < assumptions.size(); ++i) { - _assumptions.insert(get_literal(assumptions[i]).var()); + _assumptions.insert(get_literal(assumptions[i].get()).var()); } model_ref mdl; get_model(mdl); - ast_manager& m = m_manager; expr_ref_vector trail(m); model_evaluator eval(*mdl.get()); expr_ref val(m); TRACE("context", model_pp(tout, *mdl);); for (unsigned i = 0; i < vars.size(); ++i) { - eval(vars[i], val); + eval(vars[i].get(), val); if (m.is_value(val)) { trail.push_back(val); - var2val.insert(vars[i], val); + m_var2val.insert(vars[i].get(), val); } else { - unfixed.push_back(vars[i]); + unfixed.push_back(vars[i].get()); } } unsigned num_units = 0; - extract_fixed_consequences(num_units, var2val, _assumptions, conseq); + extract_fixed_consequences(num_units, _assumptions, conseq); app_ref eq(m); TRACE("context", tout << "vars: " << vars.size() << "\n"; @@ -298,11 +356,12 @@ namespace smt { unsigned num_fixed_eqs = 0; unsigned chunk_size = 100; - while (!var2val.empty()) { - obj_map::iterator it = var2val.begin(), end = var2val.end(); + while (!m_var2val.empty()) { + obj_map::iterator it = m_var2val.begin(), end = m_var2val.end(); unsigned num_vars = 0; for (; it != end && num_vars < chunk_size; ++it) { if (get_cancel_flag()) { + if (pushed) pop(1); return l_undef; } expr* e = it->m_key; @@ -332,6 +391,7 @@ namespace smt { while (true) { is_sat = bounded_search(); if (is_sat != l_true && m_last_search_failure != OK) { + if (pushed) pop(1); return is_sat; } if (is_sat == l_undef) { @@ -347,18 +407,21 @@ namespace smt { m_not_l = null_literal; } if (is_sat == l_true) { - delete_unfixed(var2val, unfixed); + delete_unfixed(unfixed); } - extract_fixed_consequences(num_units, var2val, _assumptions, conseq); - num_fixed_eqs += extract_fixed_eqs(var2val, conseq); - IF_VERBOSE(1, display_consequence_progress(verbose_stream(), num_iterations, var2val.size(), conseq.size(), + extract_fixed_consequences(num_units, _assumptions, conseq); + num_fixed_eqs += extract_fixed_eqs(conseq); + IF_VERBOSE(1, display_consequence_progress(verbose_stream(), num_iterations, m_var2val.size(), conseq.size(), unfixed.size(), num_fixed_eqs);); - TRACE("context", display_consequence_progress(tout, num_iterations, var2val.size(), conseq.size(), + TRACE("context", display_consequence_progress(tout, num_iterations, m_var2val.size(), conseq.size(), unfixed.size(), num_fixed_eqs);); } end_search(); DEBUG_CODE(validate_consequences(assumptions, vars, conseq, unfixed);); + if (pushed) { + pop(1); + } return l_true; } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 1d7ce084e..3f8f9b1f1 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1411,14 +1411,17 @@ namespace smt { typedef hashtable index_set; //typedef uint_set index_set; u_map m_antecedents; - void extract_fixed_consequences(literal lit, obj_map& var2val, index_set const& assumptions, expr_ref_vector& conseq); - void extract_fixed_consequences(unsigned& idx, obj_map& var2val, index_set const& assumptions, expr_ref_vector& conseq); + obj_map m_var2orig; + obj_map m_assumption2orig; + obj_map m_var2val; + void extract_fixed_consequences(literal lit, index_set const& assumptions, expr_ref_vector& conseq); + void extract_fixed_consequences(unsigned& idx, index_set const& assumptions, expr_ref_vector& conseq); void display_consequence_progress(std::ostream& out, unsigned it, unsigned nv, unsigned fixed, unsigned unfixed, unsigned eq); - unsigned delete_unfixed(obj_map& var2val, expr_ref_vector& unfixed); + unsigned delete_unfixed(expr_ref_vector& unfixed); - unsigned extract_fixed_eqs(obj_map& var2val, expr_ref_vector& conseq); + unsigned extract_fixed_eqs(expr_ref_vector& conseq); expr_ref antecedent2fml(index_set const& ante); diff --git a/src/test/cnf_backbones.cpp b/src/test/cnf_backbones.cpp new file mode 100644 index 000000000..c562cfe58 --- /dev/null +++ b/src/test/cnf_backbones.cpp @@ -0,0 +1,106 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +--*/ +#include +#include +#include +#include"timeout.h" +#include"rlimit.h" +#include"dimacs.h" +#include"sat_solver.h" +#include"gparams.h" + +static sat::solver * g_solver = 0; +static clock_t g_start_time; + +static void display_statistics() { + clock_t end_time = clock(); + if (g_solver) { + std::cout.flush(); + std::cerr.flush(); + + statistics st; + g_solver->collect_statistics(st); + st.update("total time", ((static_cast(end_time) - static_cast(g_start_time)) / CLOCKS_PER_SEC)); + st.display_smt2(std::cout); + } +} + +static void on_timeout() { + display_statistics(); + exit(0); +} + +static void STD_CALL on_ctrl_c(int) { + signal (SIGINT, SIG_DFL); + display_statistics(); + raise(SIGINT); +} + +static void display_model(sat::solver const & s) { + sat::model const & m = s.get_model(); + for (unsigned i = 1; i < m.size(); i++) { + switch (m[i]) { + case l_false: std::cout << "-" << i << " "; break; + case l_undef: break; + case l_true: std::cout << i << " "; break; + } + } + std::cout << "\n"; +} + + +static void cnf_backbones(char const* file_name) { + g_start_time = clock(); + register_on_timeout_proc(on_timeout); + signal(SIGINT, on_ctrl_c); + params_ref p = gparams::get_module("sat"); + p.set_bool("produce_models", true); + reslimit limit; + sat::solver solver(p, limit, 0); + g_solver = &solver; + + if (file_name) { + std::ifstream in(file_name); + if (in.bad() || in.fail()) { + std::cerr << "(error \"failed to open file '" << file_name << "'\")" << std::endl; + exit(ERR_OPEN_FILE); + } + parse_dimacs(in, solver); + } + else { + parse_dimacs(std::cin, solver); + } + IF_VERBOSE(20, solver.display_status(verbose_stream());); + + vector conseq; + sat::bool_var_vector vars; + sat::literal_vector assumptions; + for (unsigned i = 1; i < solver.num_vars(); ++i) { + vars.push_back(i); + solver.set_external(i); + } + lbool r = solver.get_consequences(assumptions, vars, conseq); + + switch (r) { + case l_true: + std::cout << "sat\n"; + std::cout << vars.size() << " " << conseq.size() << "\n"; + break; + case l_undef: + std::cout << "unknown\n"; + break; + case l_false: + std::cout << "unsat\n"; + break; + } + display_statistics(); +} + +void tst_cnf_backbones(char ** argv, int argc, int& i) { + if (i + 1 < argc) { + cnf_backbones(argv[i + 1]); + ++i; + } +} diff --git a/src/test/ddnf.cpp b/src/test/ddnf.cpp index d2ca92557..31503842d 100644 --- a/src/test/ddnf.cpp +++ b/src/test/ddnf.cpp @@ -1,4 +1,3 @@ - /*++ Copyright (c) 2015 Microsoft Corporation diff --git a/src/test/main.cpp b/src/test/main.cpp index 9239d0119..4a54797ac 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -229,6 +229,7 @@ int main(int argc, char ** argv) { TST(model_evaluator); TST(get_consequences); TST(pb2bv); + TST_ARGV(cnf_backbones); //TST_ARGV(hs); }