Commit c30ca425 authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

Merge branch 'dnnf'

parents 73ffcbae ee60282d
-I ./lib/
-I ../lib/
-I /usr/local/include
......@@ -2,7 +2,9 @@ cmake_minimum_required (VERSION 3.0.2)
project (SUBool)
set (CMAKE_EXPORT_COMPILE_COMMANDS ON)
set (CMAKE_CXX_STANDARD 11)
set (CMAKE_CXX_STANDARD 14)
set (CMAKE_CXX_STANDARD_REQUIRED ON)
set (CMAKE_CXX_EXTENSIONS OFF)
set (CMAKE_BUILD_TYPE Release)
enable_testing()
......@@ -23,6 +25,8 @@ find_library(GLUCOSE_LIB _release ${GLUCOSE_HOME}/simp)
include_directories (${SUBool_SOURCE_DIR}/lib)
include_directories (${GLUCOSE_HOME})
include_directories (/usr/local/include/)
# include_directories (/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/include/)
# include_directories (/Applications/Xcode.app/Contents/Developer/Toolchains/XcodeDefault.xctoolchain/usr/include/c++/v1/)
add_subdirectory (lib)
add_subdirectory (test)
......
......@@ -32,5 +32,8 @@ target_link_libraries (nnfsmooth subool ${GLUCOSE_LIB})
add_executable (rhbdmc_compile rhbdmc_compile.cpp)
target_link_libraries (rhbdmc_compile subool ${GLUCOSE_LIB})
add_executable (triple_cnf triple_cnf.cpp)
target_link_libraries (triple_cnf subool)
# add_executable (horn_uniform_pcgen horn_uniform_pcgen.cpp)
# target_link_libraries (horn_uniform_pcgen subool ${GLUCOSE_LIB})
/*
* Project SUBool
* Straslivy Uragan, 2018
*/
/**@file triple_cnf.cpp
* Generates special CNF with 3n variables and all prime implicates having n
* positive, n negative and n missing literals.
*/
#include <csignal>
#include <cxxopts.hpp>
#include <iostream>
#include "assign.h"
#include "logstream.h"
#include "normalform.h"
#include "prgutil.h"
const std::string prg_name = "triple_cnf";
const std::string prg_desc =
"Generates special CNF with 3n variables and all prime implicates having n "
"positive, n negative and n missing literals.";
struct config_t
{
std::string output_file;
unsigned verbosity; // 0 means no output
unsigned n;
};
auto &logs = SUBool::default_logstream;
void
dump_config(const config_t &conf, unsigned level)
{
logs.TLog(level) << "Configuration:" << std::endl;
logs.TLog(level) << "\toutput_file: " << conf.output_file << std::endl;
logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
logs.TLog(level) << "\tn: " << conf.n << std::endl;
}
int
parse_arguments(int argc, char *argv[], config_t &conf)
{
try
{
cxxopts::Options options(prg_name, prg_desc);
options.positional_help("[input [output]]");
options.add_options()("h,help", "Print help")("v,version",
"Print version info")(
"b,verbosity",
"Verbosity level of the log which is written to standard output."
" 0 means no log is written, however messages of glucose can still "
"appear.",
cxxopts::value<unsigned>(conf.verbosity)
->default_value(SUBool::LogStream::kMaxLogLevels))(
"o,output", "Output file with the encoding CNF in DIMACS format",
cxxopts::value<std::string>(conf.output_file))(
"n", "The number of variables is 3n",
cxxopts::value<unsigned>(conf.n)->default_value("2"));
options.parse_positional({"output", "positional"});
auto result = options.parse(argc, argv);
if (result.count("help"))
{
std::cout << options.help() << std::endl;
return 1;
}
if (result.count("version"))
{
SUBool::print_version(prg_name, prg_desc);
return 1;
}
if (result.count("positional"))
{
logs.TLog(0) << "Multiple files passed as parameters, ";
logs.TLog(0) << "only output file is allowed" << std::endl;
logs.TLog(0) << options.help() << std::endl;
return 1;
}
}
catch (const cxxopts::OptionException &e)
{
std::cerr << "Error parsing options: " << e.what() << std::endl;
return 1;
}
return 0;
}
void
term_func(int signal)
{
logs.TLog(0) << "Terminated by signal " << signal << std::endl;
_Exit(signal);
}
SUBool::CNF
generate(unsigned n)
{
SUBool::PartialAssignment alpha(3 * n);
std::vector<SUBool::Clause> clauses;
do
{
unsigned c_true = 0;
unsigned c_false = 0;
unsigned c_undef = 0;
for (const auto &val : alpha)
{
switch (val)
{
case SUBool::PartialValue::UNDEF:
++c_undef;
break;
case SUBool::PartialValue::TRUE:
++c_true;
break;
case SUBool::PartialValue::FALSE:
++c_false;
break;
}
}
if (c_undef == c_true && c_undef == c_false)
{
clauses.emplace_back(alpha);
}
} while (alpha.Inc());
return SUBool::CNF(std::move(clauses));
}
int
main(int argc, char *argv[])
{
config_t conf;
int r = parse_arguments(argc, argv, conf);
if (r != 0)
{
return r;
}
logs.mVerbLevel = conf.verbosity;
std::signal(SIGTERM, term_func);
std::signal(SIGQUIT, term_func);
std::signal(SIGINT, term_func);
dump_config(conf, 0);
SUBool::output(conf.output_file, generate(conf.n));
return 0;
}
......@@ -76,6 +76,22 @@ SUBool::PartialAssignment::PartialAssignment(const Assignment &alpha)
}
}
SUBool::PartialAssignment::PartialAssignment(size_t n_values,
std::vector<Literal> literals)
: PartialAssignment(n_values, PartialValue::UNDEF)
{
for (const auto &lit : literals)
{
SetLiteral(lit);
}
}
void
SUBool::PartialAssignment::SetLiteral(const Literal &lit)
{
(*this)[lit.Variable()] = partial_value_of_bool(lit.Positive());
}
std::ostream &
SUBool::operator<<(std::ostream &out, const PartialValue &v)
{
......@@ -156,17 +172,3 @@ SUBool::next_value(PartialValue val)
"TRUE cannot be increased");
}
}
bool
SUBool::bool_of_partial_value(PartialValue v, bool default_value)
{
if (v == PartialValue::TRUE)
{
return true;
}
else if (v == PartialValue::FALSE)
{
return false;
}
return default_value;
}
......@@ -12,6 +12,8 @@
#include <iostream>
#include <vector>
#include "literal.h"
namespace SUBool
{
/**@brief Assignment is basically a vector of values, but indexed
......@@ -192,6 +194,9 @@ namespace SUBool
PartialAssignment(size_t n_values, double probability_false,
double probability_true);
PartialAssignment(const std::string &s);
PartialAssignment(size_t n_values, std::vector<Literal> literals);
void SetLiteral(const Literal &lit);
};
std::ostream &operator<<(std::ostream &out, const PartialValue &v);
......@@ -206,7 +211,19 @@ namespace SUBool
return (v ? PartialValue::TRUE : PartialValue::FALSE);
}
bool bool_of_partial_value(PartialValue v, bool default_value = false);
constexpr bool
bool_of_partial_value(PartialValue v, bool default_value = false)
{
if (v == PartialValue::TRUE)
{
return true;
}
else if (v == PartialValue::FALSE)
{
return false;
}
return default_value;
}
} // namespace SUBool
// Implementation
......
......@@ -12,9 +12,9 @@
bool
SUBool::cnf_implies(const CNF &a, const CNF &b)
{
for(const auto &clause : b)
for (const auto &clause : b)
{
if(!is_implicate(a, clause))
if (!is_implicate(a, clause))
{
return false;
}
......@@ -26,9 +26,9 @@ bool
SUBool::cnf_implies_up(const CNF &a, const CNF &b)
{
OneProve op(a);
for(const auto &clause : b)
for (const auto &clause : b)
{
if(!op.IsOneProvable(clause))
if (!op.IsOneProvable(clause))
{
return false;
}
......@@ -39,12 +39,10 @@ SUBool::cnf_implies_up(const CNF &a, const CNF &b)
SUBool::CompareResult
SUBool::cmp_result_of_bool(bool leq, bool geq)
{
return (leq
? (geq ? CompareResult::EQUAL : CompareResult::LESS)
: (geq ? CompareResult::GREATER : CompareResult::INCOMPARABLE));
return (leq ? (geq ? CompareResult::EQUAL : CompareResult::LESS)
: (geq ? CompareResult::GREATER : CompareResult::INCOMPARABLE));
}
SUBool::CompareResult
SUBool::cnf_compare(const CNF &a, const CNF &b)
{
......@@ -57,4 +55,14 @@ SUBool::cnf_compare_up(const CNF &a, const CNF &b)
return cmp_result_of_bool(cnf_implies_up(a, b), cnf_implies_up(b, a));
}
bool
SUBool::cnf_equal(const CNF &a, const CNF &b)
{
return cnf_implies(a, b) && cnf_implies(b, a);
}
bool
SUBool::cnf_equal_up(const CNF &a, const CNF &b)
{
return cnf_implies_up(a, b) && cnf_implies_up(b, a);
}
......@@ -13,15 +13,23 @@
namespace SUBool
{
enum class CompareResult { INCOMPARABLE, LESS, GREATER, EQUAL };
enum class CompareResult
{
INCOMPARABLE,
LESS,
GREATER,
EQUAL
};
bool cnf_implies(const CNF &a, const CNF &b);
bool cnf_implies_up(const CNF &a, const CNF &b);
bool cnf_equal(const CNF &a, const CNF &b);
bool cnf_equal_up(const CNF &a, const CNF &b);
CompareResult cnf_compare(const CNF &a, const CNF &b);
CompareResult cnf_compare_up(const CNF &a, const CNF &b);
CompareResult cmp_result_of_bool(bool leq, bool geq);
};
}; // namespace SUBool
#endif
......@@ -81,6 +81,14 @@ namespace SUBool
using GraphType = boost::adjacency_list<boost::vecS, boost::vecS,
Directionality, VertexProperty>;
struct Components
{
unsigned count;
// indexed from 0, var 1 is at index 0
std::vector<unsigned> comp_variables;
std::vector<unsigned> comp_clauses;
};
private:
GraphType mGraph;
unsigned mMaxVariable;
......@@ -104,6 +112,8 @@ namespace SUBool
const std::string &var_color,
const std::string &clause_prefix,
const std::string &clause_color);
Components ConnectedComponents() const;
};
using IncidenceGraph = IncidenceGraphT<boost::undirectedS>;
......
......@@ -6,69 +6,68 @@
* CNF graphs.
*/
#include <boost/graph/connected_components.hpp>
#include <boost/graph/graphml.hpp>
#include <boost/graph/graphviz.hpp>
template<class Directionality>
template <class Directionality>
const typename SUBool::IncidenceGraphT<Directionality>::GraphType &
SUBool::IncidenceGraphT<Directionality>::Graph() const
{
return mGraph;
}
template<class Directionality>
template <class Directionality>
void
SUBool::IncidenceGraphT<Directionality>::WriteGraphML(std::ostream &out,
const std::string &var_prefix,
const std::string &var_color,
const std::string &clause_prefix,
const std::string &clause_color)
SUBool::IncidenceGraphT<Directionality>::WriteGraphML(
std::ostream &out, const std::string &var_prefix,
const std::string &var_color, const std::string &clause_prefix,
const std::string &clause_color)
{
auto dp=DynamicProperties(var_prefix, var_color, clause_prefix,
clause_color);
auto dp =
DynamicProperties(var_prefix, var_color, clause_prefix, clause_color);
boost::write_graphml(out, Graph(), dp.first, true);
}
template<class Directionality>
void
SUBool::IncidenceGraphT<Directionality>::WriteGraphViz(std::ostream &out,
const std::string &var_prefix,
const std::string &var_color,
const std::string &clause_prefix,
const std::string &clause_color)
template <class Directionality>
void
SUBool::IncidenceGraphT<Directionality>::WriteGraphViz(
std::ostream &out, const std::string &var_prefix,
const std::string &var_color, const std::string &clause_prefix,
const std::string &clause_color)
{
auto dp=DynamicProperties(var_prefix, var_color, clause_prefix,
clause_color);
auto dp =
DynamicProperties(var_prefix, var_color, clause_prefix, clause_color);
boost::write_graphviz_dp(out, Graph(), dp.first, dp.second);
}
template<class Directionality>
template <class Directionality>
SUBool::IncidenceGraphT<Directionality>::IncidenceGraphT(const CNF &cnf)
: mMaxVariable(cnf.MaxVariable())
: mMaxVariable(cnf.MaxVariable())
{
std::vector<std::pair<unsigned, unsigned> > edges;
for(unsigned i=0; i<cnf.Size(); ++i)
std::vector<std::pair<unsigned, unsigned>> edges;
for (unsigned i = 0; i < cnf.Size(); ++i)
{
for(const auto &lit : cnf[i])
for (const auto &lit : cnf[i])
{
if(lit.Positive())
if (lit.Positive())
{
edges.emplace_back(cnf.MaxVariable()+i, lit.Variable()-1);
edges.emplace_back(cnf.MaxVariable() + i, lit.Variable() - 1);
}
else
{
edges.emplace_back(lit.Variable()-1, cnf.MaxVariable()+i);
edges.emplace_back(lit.Variable() - 1, cnf.MaxVariable() + i);
}
}
}
mGraph=GraphType(edges.begin(), edges.end(), cnf.MaxVariable()+cnf.Size());
mGraph =
GraphType(edges.begin(), edges.end(), cnf.MaxVariable() + cnf.Size());
typename boost::graph_traits<GraphType>::vertex_iterator v, v_end;
auto index=boost::get(boost::vertex_index, mGraph);
for(boost::tie(v, v_end)=boost::vertices(mGraph);
v!=v_end; ++v)
auto index = boost::get(boost::vertex_index, mGraph);
for (boost::tie(v, v_end) = boost::vertices(mGraph); v != v_end; ++v)
{
std::stringstream ss;
if(index[*v]<cnf.MaxVariable())
if (index[*v] < cnf.MaxVariable())
{
boost::put(boost::vertex_color_t(), mGraph, *v, VERTEX_TYPE::VARIABLE);
}
......@@ -79,28 +78,40 @@ SUBool::IncidenceGraphT<Directionality>::IncidenceGraphT(const CNF &cnf)
}
}
template<class Directionality>
template <class Directionality>
std::pair<boost::dynamic_properties, std::string>
SUBool::IncidenceGraphT<Directionality>::DynamicProperties(
const std::string &var_prefix,
const std::string &var_color,
const std::string &clause_prefix,
const std::string &clause_color)
const std::string &var_prefix, const std::string &var_color,
const std::string &clause_prefix, const std::string &clause_color)
{
boost::dynamic_properties dp;
auto index=boost::get(boost::vertex_index, mGraph);
auto index2name=[&](unsigned i)
{
return (i<mMaxVariable
? var_prefix+std::to_string(i+1)
: clause_prefix+std::to_string(i-mMaxVariable));
auto index = boost::get(boost::vertex_index, mGraph);
auto index2name = [&](unsigned i) {
return (i < mMaxVariable
? var_prefix + std::to_string(i + 1)
: clause_prefix + std::to_string(i - mMaxVariable));
};
dp.property("name", boost::make_transform_value_property_map(index2name, index));
auto vertex_type=boost::get(boost::vertex_color, mGraph);
auto func=[&](const VERTEX_TYPE &vt)->std::string
{
return (vt==VERTEX_TYPE::VARIABLE ? var_color : clause_color);
dp.property("name",
boost::make_transform_value_property_map(index2name, index));
auto vertex_type = boost::get(boost::vertex_color, mGraph);
auto func = [&](const VERTEX_TYPE &vt) -> std::string {
return (vt == VERTEX_TYPE::VARIABLE ? var_color : clause_color);
};
dp.property("color", boost::make_transform_value_property_map(func, vertex_type));
dp.property("color",
boost::make_transform_value_property_map(func, vertex_type));
return std::make_pair(dp, "name");
}
template <class Directionality>
typename SUBool::IncidenceGraphT<Directionality>::Components
SUBool::IncidenceGraphT<Directionality>::ConnectedComponents() const
{
std::vector<unsigned> comp(boost::num_vertices(mGraph));
Components components;
components.count = boost::connected_components(mGraph, &comp[0]);
components.comp_variables.assign(comp.begin(), comp.begin() + mMaxVariable);
std::transform(comp.begin() + mMaxVariable, comp.end(),
std::back_inserter(components.comp_clauses),
[mv = this->mMaxVariable](auto cl) { return cl - mv; });
return components;
}
......@@ -9,6 +9,7 @@
#include <sstream>
#include <string>
#include "assign.h"
#include "literal.h"
#include "sbexception.h"
......
......@@ -12,10 +12,12 @@
#include <iostream>
#include <vector>
#include "assign.h"
namespace SUBool
{
class Assignment;
enum class PartialValue;
class PartialAssignment;
struct Literal
{
unsigned mVariable;
......
......@@ -60,6 +60,13 @@ namespace SUBool
{
++mNodeCount;
}
virtual void
PostVisitLeafCNF(const CnfPtr &node) override
{
++mNodeCount;
mMaxVariable = std::max(mMaxVariable, node->MaxVariable());
}
};
void nnf_header(std::istream &input, unsigned *max_var, size_t *edge_count,
......@@ -141,6 +148,12 @@ namespace SUBool
node->CacheMovedValue(mNodeCopy, NnfNode::MakeFalse());
}
virtual void
PostVisitLeafCNF(const CnfPtr &node) override
{
node->CacheMovedValue(mNodeCopy, NnfNode::MakeLeafCNF(node->Cnf()));
}
static NnfNode::tPointer
MakeRootCopy(const Nnf &nnf)
{
......
......@@ -264,3 +264,14 @@ SUBool::NnfLeafCNF::MaxVariable() const
{
return mCnf.MaxVariable();
}
const std::vector<unsigned> &
SUBool::NnfLeafCNF::Variables() const
{
if (!mVariables)
{
auto vars = mCnf.Variables();
mVariables = std::vector<unsigned>(vars.begin(), vars.end());
}
return *mVariables;
}
......@@ -158,6 +158,7 @@ namespace SUBool
class NnfLeafCNF : public NnfLeaf
{
CNF mCnf;
mutable boost::optional<std::vector<unsigned>> mVariables;
protected:
virtual bool Eval(const Assignment &assignment) const override;
......@@ -177,11 +178,7 @@ namespace SUBool
}
virtual ~NnfLeafCNF() = default;
virtual unsigned MaxVariable() const override;
std::set<unsigned>
Variables() const
{
return mCnf.Variables();
}
const std::vector<unsigned> &Variables() const;
virtual Type
NodeType() const override
......
......@@ -86,6 +86,7 @@ namespace SUBool
bool AddWithoutSubsumptions(ElementType element);
void RemoveDuplicities();
void RemoveSubsumptions();