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

Debug output, variable initialization

parent 412dba7a
......@@ -25,6 +25,7 @@ SUBool::UPSCCBinary::Encode(unsigned max_level, std::vector<unsigned> *inputs,
max_level = max_level_bound;
}
#if 0
if (logs.CheckLevel(3))
{
logs.TLog(3) << "[UPSCCUnary::Encode] Using implication system:"
......@@ -54,6 +55,7 @@ SUBool::UPSCCBinary::Encode(unsigned max_level, std::vector<unsigned> *inputs,
logs.Log(3) << std::endl;
}
}
#endif
Context ctx{max_level, VarInfoList(2 * mCnf.MaxVariable()),
mVarStore.VarArray(mCnf.MaxVariable(), true, ":in(", ")"),
......
......@@ -20,8 +20,8 @@ namespace SUBool
public:
struct VarInfo
{
std::vector<unsigned> level_vars;
std::vector<std::vector<Literal>> level_clauses;
std::vector<unsigned> level_vars{};
std::vector<std::vector<Literal>> level_clauses{};
};
using VarInfoList = std::vector<VarInfo>;
struct Context
......@@ -44,49 +44,44 @@ namespace SUBool
const LitISGraph &mSCCGraph;
VarInfoList InitVarInfo(unsigned max_level) const;
FireVariables InitFireVariables(Context &ctx, const LitImpl &impl,
unsigned impl_index) const;
FireVariables InitFireVariables(
Context &ctx, const LitImpl &impl, unsigned impl_index) const;
FireVariables NewFireVariables(unsigned impl_index, unsigned main_scc,
bool cons_out_of_main_scc,
unsigned max_level) const;
bool cons_out_of_main_scc, unsigned max_level) const;
FireVariables UnifiedFireVariables(Context &ctx, const LitImpl &impl,
unsigned main_scc,
bool cons_out_of_main_scc) const;
unsigned main_scc, bool cons_out_of_main_scc) const;
void InitLevelClauses(Context &ctx) const;
void AddClauses(Context &ctx, std::vector<Clause> &clauses) const;
std::pair<unsigned, bool> InspectImplSCC(Context &ctx,
const LitImpl &impl) const;
std::pair<unsigned, bool> InspectImplSCC(
Context &ctx, const LitImpl &impl) const;
void FireClauses(Context &ctx, const LitImpl &impl, unsigned impl_index,
std::vector<Clause> &clauses) const;
std::vector<Clause> &clauses) const;
void SimpleFireVarDefinition(Context &ctx, const LitImpl &impl,
unsigned fire_var,
std::vector<Clause> &clauses) const;
unsigned fire_var, std::vector<Clause> &clauses) const;
void LevelFireVarDefinition(Context &ctx, const LitImpl &impl,
unsigned fire_var, unsigned level,
unsigned main_scc,
std::vector<Clause> &clauses) const;
unsigned fire_var, unsigned level, unsigned main_scc,
std::vector<Clause> &clauses) const;
void FireVarDefinition(Context &ctx, const LitImpl &impl,
const FireVariables &fv,
std::vector<Clause> &clauses) const;
void AddFireVarsToLevelClauses(Context &ctx, const LitImpl &impl,
const FireVariables &fv) const;
const FireVariables &fv, std::vector<Clause> &clauses) const;
void AddFireVarsToLevelClauses(
Context &ctx, const LitImpl &impl, const FireVariables &fv) const;
void MoveLevelClauses(Context &ctx, std::vector<Clause> &clauses) const;
void AddOutImplications(const Context &ctx,
std::vector<Clause> &clauses) const;
void AddOutImplications(
const Context &ctx, std::vector<Clause> &clauses) const;
public:
UPSCCUnary(const CNF &cnf, const ClausesToLiterals &cl2lit,
VarStore &var_store, const LitImplSystem &is,
const LitISGraph &scc_graph)
VarStore &var_store, const LitImplSystem &is,
const LitISGraph &scc_graph)
: UPEncoder(cnf, cl2lit, var_store), mImplSystem(is),
mSCCGraph(scc_graph)
{
}
virtual void Encode(unsigned max_level, std::vector<unsigned> *inputs,
std::vector<unsigned> *outputs,
std::vector<Clause> *clauses) const override;
std::vector<unsigned> *outputs,
std::vector<Clause> *clauses) const override;
virtual NFSize EstimateSize(unsigned max_level) const override;
virtual unsigned MaxLevelBound() const override;
virtual unsigned NextLevelBound(unsigned level) const override;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment