aig_encoder.hpp
No OneTemporary
Actions

Authored By

Unknown

Size

71 KB

Referenced Files

None

Subscribers

None

aig_encoder.hpp
View Options

	#pragma once

	#include <vector>
	#include <kitty/kitty.hpp>
	#include "encoder.hpp"

	namespace percy
	{
	class aig_encoder
	{
	private:
	int level_dist[32]; // How many steps are below a certain level
	int nr_levels; // The number of levels in the Boolean fence
	int nr_sel_vars;
	int nr_res_vars;
	int nr_sim_vars;
	int total_nr_vars;
	int sel_offset;
	int res_offset;
	int sim_offset;
	bool dirty = false;
	pabc::lit pLits[2048];
	solver_wrapper* solver;

	static const int NR_SIM_TTS = 32;
	std::vector<kitty::dynamic_truth_table> sim_tts { NR_SIM_TTS };

	int get_sim_var(const spec& spec, int step_idx, int t) const
	{
	return sim_offset + spec.tt_size * step_idx + t;
	}

	bool fix_output_sim_vars(const spec& spec, int t)
	{
	const auto ilast_step = spec.nr_steps - 1;
	auto outbit = kitty::get_bit(
	spec[spec.synth_func(0)], t + 1);
	if ((spec.out_inv >> spec.synth_func(0)) & 1) {
	outbit = 1 - outbit;
	}
	const auto sim_var = get_sim_var(spec, ilast_step, t);
	pabc::lit sim_lit = pabc::Abc_Var2Lit(sim_var, 1 - outbit);
	return solver->add_clause(&sim_lit, &sim_lit + 1);
	}

	int get_sel_var(
	const spec& spec,
	const int i,
	const int j,
	const int k,
	const int l) const
	{
	assert(i < spec.nr_steps);

	int offset = 0;
	for (int ip = 0; ip < i; ip++) {
	const auto n = spec.nr_in + ip;
	offset += (n * (n - 1) * (n - 2)) / 6;
	}

	int svar_ctr = 0;
	for (int lp = 2; lp < spec.nr_in + i; lp++) {
	for (int kp = 1; kp < lp; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if (l == lp && k == kp && j == jp) {
	return sel_offset + offset + svar_ctr;
	}
	svar_ctr++;
	}
	}
	}

	assert(false);
	return -1;
	}

	int get_sel_var(const spec& spec, int idx, int var_idx) const
	{
	assert(idx < spec.nr_steps);
	const auto nr_svars_for_idx = nr_svars_for_step(spec, idx);
	assert(var_idx < nr_svars_for_idx);
	auto offset = 0;
	for (int i = 0; i < idx; i++) {
	offset += nr_svars_for_step(spec, i);
	}
	return sel_offset + offset + var_idx;
	}

	int get_res_var(const spec& spec, int step_idx, int res_var_idx) const
	{
	auto offset = 0;
	for (int i = 0; i < step_idx; i++) {
	offset += (nr_svars_for_step(spec, i) + 1) * (1 + 2);
	}

	return res_offset + offset + res_var_idx;
	}

	public:
	aig_encoder(solver_wrapper& solver)
	{
	this->solver = &solver;
	}

	~aig_encoder()
	{
	}

	void create_variables(const spec& spec)
	{
	nr_sim_vars = spec.nr_steps * spec.tt_size;

	nr_sel_vars = 0;
	for (int i = 0; i < spec.nr_steps; i++) {
	const auto n = spec.nr_in + i;
	nr_sel_vars += (n * (n - 1)) / 2;
	}

	sel_offset = 0;
	sim_offset = nr_sel_vars;
	total_nr_vars = nr_sel_vars + nr_sim_vars;

	if (spec.verbosity) {
	printf("Creating variables (AIG)\n");
	printf("nr steps = %d\n", spec.nr_steps);
	printf("nr_sel_vars=%d\n", nr_sel_vars);
	printf("nr_sim_vars = %d\n", nr_sim_vars);
	printf("creating %d total variables\n", total_nr_vars);
	}

	solver->set_nr_vars(total_nr_vars);
	}

	void create_variables(const spec& spec, const partial_dag& dag)
	{
	nr_sim_vars = spec.nr_steps * spec.tt_size;

	nr_sel_vars = 0;
	for (int i = 0; i < spec.nr_steps; i++) {
	const auto nr_svars_for_i = nr_svars_for_step(spec, dag, i);
	nr_sel_vars += nr_svars_for_i;
	}

	sel_offset = 0;
	sim_offset = nr_sel_vars;
	total_nr_vars = nr_sel_vars + nr_sim_vars;

	if (spec.verbosity) {
	printf("Creating variables (PD-%d)\n", spec.fanin);
	printf("nr steps = %d\n", spec.nr_steps);
	printf("nr_sel_vars=%d\n", nr_sel_vars);
	printf("nr_sim_vars = %d\n", nr_sim_vars);
	printf("creating %d total variables\n", total_nr_vars);
	}

	solver->set_nr_vars(total_nr_vars);
	}

	int first_step_on_level(int level) const
	{
	if (level == 0) { return 0; }
	return level_dist[level-1];
	}

	int nr_svars_for_step(const spec& spec, int i) const
	{
	// Determine the level of this step.
	const auto level = get_level(spec, i + spec.nr_in);
	auto nr_svars_for_i = 0;
	assert(level > 0);
	for (auto l = first_step_on_level(level - 1);
	l < first_step_on_level(level); l++) {
	// We select l as fanin 3, so have (l choose 2) options
	// (j,k in {0,...,(l-1)}) left for fanin 1 and 2.
	nr_svars_for_i += (l * (l - 1)) / 2;
	}

	return nr_svars_for_i;
	}

	int nr_pi_fanins_for_step(const partial_dag& dag, int i) const
	{
	const auto& vertex = dag.get_vertex(i);
	auto nr_pi_fanins = 0;
	if (vertex[2] == FANIN_PI) {
	nr_pi_fanins = 3;
	} else if (vertex[1] == FANIN_PI) {
	nr_pi_fanins = 2;
	} else if (vertex[0] == FANIN_PI) {
	nr_pi_fanins = 1;
	}

	return nr_pi_fanins;
	}

	int nr_svars_for_step(
	const spec& spec,
	const partial_dag& dag,
	int i) const
	{
	const auto& vertex = dag.get_vertex(i);
	const auto nr_pi_fanins = nr_pi_fanins_for_step(dag, i);
	switch (nr_pi_fanins) {
	case 1:
	return spec.nr_in;
	case 2:
	return (spec.nr_in * (spec.nr_in - 1)) / 2;
	case 3:
	return (spec.nr_in * (spec.nr_in - 1) * (spec.nr_in - 2)) / 6;
	default: // No fanin flexibility
	return 0;
	}
	}

	int get_sel_var(
	const spec& spec,
	const partial_dag& dag,
	int step_idx,
	int var_idx) const
	{
	auto offset = 0;
	for (int i = 0; i < step_idx; i++) {
	offset += nr_svars_for_step(spec, dag, i);
	}
	return sel_offset + offset + var_idx;
	}

	void fence_create_variables(const spec& spec)
	{
	nr_sim_vars = spec.nr_steps * spec.tt_size;

	nr_sel_vars = 0;
	for (int i = 0; i < spec.nr_steps; i++) {
	nr_sel_vars += nr_svars_for_step(spec, i);
	}

	sel_offset = 0;
	sim_offset = nr_sel_vars;
	total_nr_vars = nr_sel_vars + nr_sim_vars;

	if (spec.verbosity) {
	printf("Creating variables (AIG)\n");
	printf("nr steps = %d\n", spec.nr_steps);
	printf("nr_sel_vars=%d\n", nr_sel_vars);
	printf("nr_sim_vars = %d\n", nr_sim_vars);
	printf("creating %d total variables\n", total_nr_vars);
	}

	solver->set_nr_vars(total_nr_vars);
	}

	void cegar_fence_create_variables(const spec& spec)
	{
	nr_sim_vars = spec.nr_steps * spec.tt_size;

	nr_sel_vars = 0;
	nr_res_vars = 0;
	for (int i = 0; i < spec.nr_steps; i++) {
	const auto nr_svars_for_i = nr_svars_for_step(spec, i);
	nr_sel_vars += nr_svars_for_i;
	nr_res_vars += (nr_svars_for_i + 1) * (1 + 2);
	}

	sel_offset = 0;
	res_offset = nr_sel_vars;
	sim_offset = nr_sel_vars + nr_res_vars;
	total_nr_vars = nr_sel_vars + nr_res_vars + nr_sim_vars;

	if (spec.verbosity) {
	printf("Creating variables (AIG)\n");
	printf("nr steps = %d\n", spec.nr_steps);
	printf("nr_sel_vars=%d\n", nr_sel_vars);
	printf("nr_sel_vars=%d\n", nr_res_vars);
	printf("nr_sim_vars = %d\n", nr_sim_vars);
	printf("creating %d total variables\n", total_nr_vars);
	}

	solver->set_nr_vars(total_nr_vars);
	}

	/// Ensures that each gate has the proper number of fanins.
	bool create_fanin_clauses(const spec& spec)
	{
	auto status = true;

	if (spec.verbosity > 2) {
	printf("Creating fanin clauses (AIG)\n");
	printf("Nr. clauses = %d (PRE)\n", solver->nr_clauses());
	}

	for (int i = 0; i < spec.nr_steps; i++) {
	auto ctr = 0;
	for (int l = 2; l < spec.nr_in + i; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto svar = get_sel_var(spec, i, j, k, l);
	pLits[ctr++] = pabc::Abc_Var2Lit(svar, 0);
	}
	}
	}
	status &= solver->add_clause(pLits, pLits + ctr);
	}

	if (spec.verbosity > 2) {
	printf("Nr. clauses = %d (POST)\n", solver->nr_clauses());
	}

	return status;
	}

	bool create_fanin_clauses(const spec& spec, const partial_dag& dag)
	{
	auto status = true;

	for (int i = 0; i < spec.nr_steps; i++) {
	const auto nr_svars_for_i = nr_svars_for_step(spec, dag, i);
	if (nr_svars_for_i == 0) {
	continue;
	}

	for (int j = 0; j < nr_svars_for_i; j++) {
	pLits[j] = pabc::Abc_Var2Lit(get_sel_var(spec, dag, i, j), 0);
	}

	status &= solver->add_clause(pLits, pLits + nr_svars_for_i);
	}

	return status;
	}


	bool add_simulation_clause(
	const spec& spec,
	const int t,
	const int i,
	const int j,
	const int k,
	const int l,
	const int c,
	const int b,
	const int a,
	const int sel_var
	)
	{
	int ctr = 0;
	//assert(j > 0);

	if (j < spec.nr_in) {
	if ((((t + 1) & (1 << j)) ? 1 : 0) != a) {
	return true;
	}
	} else {
	pLits[ctr++] = pabc::Abc_Var2Lit(
	get_sim_var(spec, j - spec.nr_in, t), a);
	}

	if (k < spec.nr_in) {
	if ((((t + 1) & (1 << k)) ? 1 : 0) != b) {
	return true;
	}
	} else {
	pLits[ctr++] = pabc::Abc_Var2Lit(
	get_sim_var(spec, k - spec.nr_in, t), b);
	}

	if (l < spec.nr_in) {
	if ((((t + 1) & (1 << l)) ? 1 : 0) != c) {
	return true;
	}
	} else {
	pLits[ctr++] = pabc::Abc_Var2Lit(
	get_sim_var(spec, l - spec.nr_in, t), c);
	}

	if (sel_var != -1) {
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_var, 1);
	}

	if (maj3(a, b, c)) {
	pLits[ctr++] = pabc::Abc_Var2Lit(get_sim_var(spec, i, t), 0);
	} else {
	pLits[ctr++] = pabc::Abc_Var2Lit(get_sim_var(spec, i, t), 1);
	}

	const auto ret = solver->add_clause(pLits, pLits + ctr);
	assert(ret);
	return ret;
	}

	bool create_tt_clauses(const spec& spec, const int t)
	{
	bool ret = true;
	for (int i = 0; i < spec.nr_steps; i++) {
	for (int l = 2; l < spec.nr_in + i; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, i, j, k);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 1, sel_var);
	}
	}
	}
	assert(ret);
	}

	ret &= fix_output_sim_vars(spec, t);

	return ret;
	}

	bool create_tt_clauses(const spec& spec, const partial_dag& dag, const int t)
	{
	auto ret = true;

	for (int i = 0; i < spec.nr_steps; i++) {
	const auto& vertex = dag.get_vertex(i);
	const auto nr_pi_fanins = nr_pi_fanins_for_step(dag, i);
	if (nr_pi_fanins == 0) {
	// The fanins for this step are fixed
	const auto j = vertex[0] + spec.nr_in - 1;
	const auto k = vertex[1] + spec.nr_in - 1;
	const auto l = vertex[1] + spec.nr_in - 1;
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 0, -1);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 1, -1);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 0, -1);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 1, -1);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 0, -1);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 1, -1);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 0, -1);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 1, -1);
	} else if (nr_pi_fanins == 1) {
	// The first fanin is flexible
	const auto k = vertex[1] + spec.nr_in - 1;
	const auto l = vertex[2] + spec.nr_in - 1;
	for (int j = 0; j < spec.nr_in; j++) {
	const auto sel_var = get_sel_var(spec, dag, i, j);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 1, sel_var);
	}
	} else if (nr_pi_fanins == 2) {
	const auto l = vertex[2] + spec.nr_in - 1;
	int ctr = 0;
	for (int k = 1; k < spec.nr_in; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, dag, i, ctr++);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 1, sel_var);
	}
	}
	} else {
	assert(nr_pi_fanins == 3);
	int ctr = 0;
	for (int l = 2; l < spec.nr_in; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, dag, i, ctr++);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 1, sel_var);
	}
	}
	}
	}
	}

	ret &= fix_output_sim_vars(spec, t);

	return ret;
	}

	bool fence_create_tt_clauses(const spec& spec, const int t)
	{
	bool ret = true;
	for (int i = 0; i < spec.nr_steps; i++) {
	const auto level = get_level(spec, i + spec.nr_in);
	int ctr = 0;
	for (int l = first_step_on_level(level - 1);
	l < first_step_on_level(level); l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, i, ctr++);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 0, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 0, 1, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 0, 1, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 0, sel_var);
	ret &= add_simulation_clause(spec, t, i, j, k, l, 1, 1, 1, sel_var);
	}
	}
	}
	assert(ret);
	}

	ret &= fix_output_sim_vars(spec, t);

	return ret;
	}

	void create_main_clauses(const spec& spec)
	{
	for (int t = 0; t < spec.tt_size; t++) {
	(void)create_tt_clauses(spec, t);
	}
	}

	void create_main_clauses(const spec& spec, const partial_dag& dag)
	{
	for (int t = 0; t < spec.tt_size; t++) {
	(void)create_tt_clauses(spec, dag, t);
	}
	}

	bool fence_create_main_clauses(const spec& spec)
	{
	bool ret = true;
	for (int t = 0; t < spec.tt_size; t++) {
	ret &= fence_create_tt_clauses(spec, t);
	}
	return ret;
	}

	void create_alonce_clauses(const spec& spec)
	{
	for (int i = 0; i < spec.nr_steps - 1; i++) {
	int ctr = 0;
	const auto idx = spec.nr_in + i;
	for (int ip = i + 1; ip < spec.nr_steps; ip++) {
	for (int l = spec.nr_in + i; l < spec.nr_in + ip; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	if (j == idx \|\| k == idx \|\| l == idx) {
	const auto sel_var = get_sel_var(spec, ip, j, k, l);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_var, 0);
	}
	}
	}
	}
	}
	const auto res = solver->add_clause(pLits, pLits + ctr);
	assert(res);
	}
	}

	void fence_create_alonce_clauses(const spec& spec)
	{
	for (int i = 0; i < spec.nr_steps - 1; i++) {
	auto ctr = 0;
	const auto idx = spec.nr_in + i;
	const auto level = get_level(spec, idx);
	for (int ip = i + 1; ip < spec.nr_steps; ip++) {
	auto levelp = get_level(spec, ip + spec.nr_in);
	assert(levelp >= level);
	if (levelp == level) {
	continue;
	}
	auto svctr = 0;
	for (int l = first_step_on_level(levelp - 1);
	l < first_step_on_level(levelp); l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	if (j == idx \|\| k == idx \|\| l == idx) {
	const auto sel_var = get_sel_var(spec, ip, svctr);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_var, 0);
	}
	svctr++;
	}
	}
	}
	assert(svctr == nr_svars_for_step(spec, ip));
	}
	solver->add_clause(pLits, pLits + ctr);
	}
	}

	void create_noreapply_clauses(const spec& spec)
	{
	for (int i = 0; i < spec.nr_steps - 1; i++) {
	for (int l = 2; l < spec.nr_in + i; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, i, j, k, l);
	pLits[0] = pabc::Abc_Var2Lit(sel_var, 1);
	for (int ip = i + 1; ip < spec.nr_steps; ip++) {
	for (int kp = 1; kp < spec.nr_steps + i; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if ((kp == l && jp == k) \|\|
	(kp == k && jp == j) \|\|
	(kp == l && jp == k)) {
	const auto sel_varp = get_sel_var(spec, ip, jp, kp, spec.nr_in + i);
	pLits[1] = pabc::Abc_Var2Lit(sel_varp, 1);
	auto status = solver->add_clause(pLits, pLits + 2);
	assert(status);
	}
	}
	}
	}
	}
	}
	}
	}
	}

	bool reapply_helper(
	const spec& spec,
	const partial_dag& dag,
	int *svars,
	int depth,
	int i,
	int j,
	int k,
	int l,
	int ip,
	int jp,
	int kp,
	int lp)
	{
	int pLits[3];
	if (depth == 2) {
	if (lp == (spec.nr_in + i) &&
	((kp == l && jp == k) \|\|
	(kp == k && jp == j) \|\|
	(kp == l && jp == k))) {
	const auto sel_var = svars[0];
	const auto sel_varp = svars[1];
	auto ctr = 0;
	if (sel_var != -1) {
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_var, 1);
	}
	if (sel_varp != -1) {
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 1);
	}
	if (ctr > 1) {
	return solver->add_clause(pLits, pLits + ctr);
	}
	}
	} else if (depth == 1) {
	for (ip = i + 1; ip < spec.nr_steps; ip++) {
	const auto& vertex = dag.get_vertex(ip);
	const auto nr_pi_fanins = nr_pi_fanins_for_step(dag, ip);
	if (nr_pi_fanins == 0) {
	svars[1] = -1;
	jp = spec.nr_in + vertex[0] - 1;
	kp = spec.nr_in + vertex[1] - 1;
	lp = spec.nr_in + vertex[2] - 1;
	reapply_helper(spec, dag, svars, 2, i, j, k, l, ip, jp, kp, lp);
	} else if (nr_pi_fanins == 1) {
	kp = spec.nr_in + vertex[1] - 1;
	lp = spec.nr_in + vertex[2] - 1;
	for (jp = 0; jp < spec.nr_in; jp++) {
	svars[1] = get_sel_var(spec, dag, ip, jp);
	reapply_helper(spec, dag, svars, 2, i, j, k, l, ip, jp, kp, lp);
	}
	} else if (nr_pi_fanins == 2) {
	auto svar_ctr = 0;
	lp = spec.nr_in + vertex[2] - 1;
	for (kp = 1; kp < spec.nr_in; kp++) {
	for (jp = 0; jp < kp; jp++) {
	const auto sel_var = get_sel_var(spec, dag, ip, svar_ctr++);
	svars[1] = sel_var;
	reapply_helper(spec, dag, svars, 2, i, j, k, l, ip, jp, kp, lp);
	}
	}
	} else {
	auto svar_ctr = 0;
	for (lp = 2; lp < spec.nr_in; lp++) {
	for (kp = 1; kp < lp; kp++) {
	for (jp = 0; jp < kp; jp++) {
	const auto sel_var = get_sel_var(spec, dag, ip, svar_ctr++);
	svars[1] = sel_var;
	reapply_helper(spec, dag, svars, 2, i, j, k, l, ip, jp, kp, lp);
	}
	}
	}
	}
	}
	} else {
	for (i = 0; i < spec.nr_steps; i++) {
	const auto& vertex = dag.get_vertex(i);
	const auto nr_pi_fanins = nr_pi_fanins_for_step(dag, i);
	if (nr_pi_fanins == 0) {
	svars[0] = -1;
	j = spec.nr_in + vertex[0] - 1;
	k = spec.nr_in + vertex[1] - 1;
	l = spec.nr_in + vertex[2] - 1;
	reapply_helper(spec, dag, svars, 1, i, j, k, l, 0, 0, 0, 0);
	} else if (nr_pi_fanins == 1) {
	k = spec.nr_in + vertex[1] - 1;
	l = spec.nr_in + vertex[2] - 1;
	for (j = 0; j < spec.nr_in; j++) {
	svars[0] = get_sel_var(spec, dag, i, j);
	reapply_helper(spec, dag, svars, 1, i, j, k, l, 0, 0, 0, 0);
	}
	} else if (nr_pi_fanins == 2) {
	auto svar_ctr = 0;
	l = spec.nr_in + vertex[2] - 1;
	for (k = 1; k < spec.nr_in; k++) {
	for (j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, dag, i, svar_ctr++);
	svars[0] = sel_var;
	reapply_helper(spec, dag, svars, 1, i, j, k, l, 0, 0, 0, 0);
	}
	}
	} else {
	auto svar_ctr = 0;
	for (l = 2; l < spec.nr_in; l++) {
	for (k = 1; k < l; k++) {
	for (j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, dag, i, svar_ctr++);
	svars[0] = sel_var;
	reapply_helper(spec, dag, svars, 1, i, j, k, l, 0, 0, 0, 0);
	}
	}
	}
	}
	}
	}

	return true;
	}

	bool create_noreapply_clauses(const spec& spec, const partial_dag& dag)
	{
	int svars[2];

	return reapply_helper(spec, dag, svars, 0, 0, 0, 0, 0, 0, 0, 0, 0);
	}


	void fence_create_noreapply_clauses(const spec& spec)
	{
	for (int i = 0; i < spec.nr_steps - 1; i++) {
	const auto level = get_level(spec, spec.nr_in + i);
	int svar_ctr = 0;
	for (int l = first_step_on_level(level - 1);
	l < first_step_on_level(level); l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, i, svar_ctr);
	pLits[0] = pabc::Abc_Var2Lit(sel_var, 1);
	for (int ip = i + 1; ip < spec.nr_steps; ip++) {
	const auto levelp = get_level(spec, spec.nr_in + ip);
	if (level == levelp) {
	continue;
	}
	int svar_ctrp = 0;
	for (int lp = first_step_on_level(levelp - 1);
	lp < first_step_on_level(levelp); lp++) {
	for (int kp = 1; kp < l; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if ((lp == spec.nr_in + i) &&
	((kp == l && jp == k) \|\|
	(kp == k && jp == j) \|\|
	(kp == l && jp == k))) {
	const auto sel_varp = get_sel_var(spec, ip, svar_ctrp);
	pLits[1] = pabc::Abc_Var2Lit(sel_varp, 1);
	auto status = solver->add_clause(pLits, pLits + 2);
	assert(status);
	}
	svar_ctrp++;
	}
	}
	}
	}
	svar_ctr++;
	}
	}
	}
	}
	}

	/// Ensure that all steps are in strict co-lexicographic
	/// order. Unlike the general Boolean chain case, here we
	/// don't want two steps pointing to the same inputs since
	/// they cannot implement different functions.
	void create_colex_clauses(const spec& spec)
	{
	for (int i = 0; i < spec.nr_steps - 1; i++) {
	for (int l = 2; l < spec.nr_in + i; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	pLits[0] = pabc::Abc_Var2Lit(get_sel_var(spec, i, j, k, l), 1);

	// Cannot have lp <= l
	for (int lp = 2; lp <= l; lp++) {
	for (int kp = 1; kp < lp; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	pLits[1] = pabc::Abc_Var2Lit(get_sel_var(spec, i + 1, jp, kp, lp), 1);
	const auto res = solver->add_clause(pLits, pLits + 2);
	assert(res);
	}
	}
	}

	// May have lp == l and kp > k
	for (int kp = 1; kp <= k; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	pLits[1] = pabc::Abc_Var2Lit(get_sel_var(spec, i + 1, jp, kp, l), 1);
	const auto res = solver->add_clause(pLits, pLits + 2);
	assert(res);
	}
	}
	// OR lp == l and kp == k
	for (int jp = 0; jp <= j; jp++) {
	pLits[1] = pabc::Abc_Var2Lit(get_sel_var(spec, i + 1, jp, k, l), 1);
	const auto res = solver->add_clause(pLits, pLits + 2);
	assert(res);
	}
	}
	}
	}
	}
	}

	void colex_helper(
	const spec& spec,
	const partial_dag& dag,
	int i,
	int j,
	int k,
	int l,
	int sel_var)
	{
	int pLits[2];

	const auto& vertex = dag.get_vertex(i + 1);
	const auto nr_pi_fanins = nr_pi_fanins_for_step(dag, i);
	if (nr_pi_fanins == 1) {
	const auto kp = spec.nr_in + vertex[1] - 1;
	const auto lp = spec.nr_in + vertex[2] - 1;
	for (int jp = 0; jp < spec.nr_in; jp++) {
	if ((kp == k && jp <= j && lp == l) \|\| (kp < k && lp == l) \|\| (lp < l)) {
	const auto sel_varp = get_sel_var(spec, dag, i + 1, jp);
	int ctr = 0;
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_var, 1);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 1);
	(void)solver->add_clause(pLits, pLits + ctr);
	}
	}
	} else if (nr_pi_fanins == 2) {
	auto svar_ctr = 0;
	const auto lp = spec.nr_in + vertex[2] - 1;
	for (int kp = 1; kp < spec.nr_in; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if ((kp == k && jp <= j && lp == l) \|\| (kp < k && lp == l) \|\| (lp < l)) {
	const auto sel_varp = get_sel_var(spec, dag, i + 1, svar_ctr);
	int ctr = 0;
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_var, 1);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 1);
	(void)solver->add_clause(pLits, pLits + ctr);
	}
	svar_ctr++;
	}
	}
	} else if (nr_pi_fanins == 3) {
	auto svar_ctr = 0;
	for (int lp = 2; lp < spec.nr_in; lp++) {
	for (int kp = 1; kp < lp; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if ((kp == k && jp <= j && lp == l) \|\| (kp < k && lp == l) \|\| (lp < l)) {
	const auto sel_varp = get_sel_var(spec, dag, i + 1, svar_ctr);
	int ctr = 0;
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_var, 1);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 1);
	(void)solver->add_clause(pLits, pLits + ctr);
	}
	svar_ctr++;
	}
	}
	}
	}
	}

	void create_colex_clauses(const spec& spec, const partial_dag& dag)
	{
	for (int i = 0; i < spec.nr_steps - 1; i++) {
	const auto& vertex = dag.get_vertex(i);
	const auto nr_pi_fanins = nr_pi_fanins_for_step(dag, i);
	if (nr_pi_fanins == 0) {
	continue;
	} else if (nr_pi_fanins == 1) {
	const auto k = spec.nr_in + vertex[1] - 1;
	const auto l = spec.nr_in + vertex[2] - 1;
	for (int j = 0; j < spec.nr_in; j++) {
	const auto sel_var = get_sel_var(spec, dag, i, j);
	colex_helper(spec, dag, i, j, k, l, sel_var);
	}
	} else if (nr_pi_fanins == 2) {
	auto svar_ctr = 0;
	const auto l = spec.nr_in + vertex[2] - 1;
	for (int k = 1; k < spec.nr_in; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, dag, i, svar_ctr++);
	colex_helper(spec, dag, i, j, k, l, sel_var);
	}
	}
	} else {
	auto svar_ctr = 0;
	for (int l = 2; l < spec.nr_in; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, dag, i, svar_ctr++);
	colex_helper(spec, dag, i, j, k, l, sel_var);
	}
	}
	}
	}
	}
	}

	void fence_create_colex_clauses(const spec& spec)
	{
	for (int i = 0; i < spec.nr_steps - 1; i++) {
	const auto level = get_level(spec, i + spec.nr_in);
	const auto levelp = get_level(spec, i + 1 + spec.nr_in);
	int svar_ctr = 0;
	for (int l = first_step_on_level(level-1);
	l < first_step_on_level(level); l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	if (l < 3) {
	svar_ctr++;
	continue;
	}
	const auto sel_var = get_sel_var(spec, i, svar_ctr);
	pLits[0] = pabc::Abc_Var2Lit(sel_var, 1);
	int svar_ctrp = 0;
	for (int lp = first_step_on_level(levelp - 1);
	lp < first_step_on_level(levelp); lp++) {
	for (int kp = 1; kp < lp; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if ((lp == l && kp == k && jp <= j) \|\|
	(lp == l && kp <= k) \|\| (lp <= l)) {
	const auto sel_varp = get_sel_var(spec, i + 1, svar_ctrp);
	pLits[1] = pabc::Abc_Var2Lit(sel_varp, 1);
	(void)solver->add_clause(pLits, pLits + 2);
	}
	svar_ctrp++;
	}
	}
	}
	svar_ctr++;
	}
	}
	}
	}
	}

	bool create_symvar_clauses(const spec& spec)
	{
	for (int q = 1; q < spec.nr_in; q++) {
	for (int p = 0; p < q; p++) {
	auto symm = true;
	for (int i = 0; i < spec.nr_nontriv; i++) {
	auto f = spec[spec.synth_func(i)];
	if (!(swap(f, p, q) == f)) {
	symm = false;
	break;
	}
	}
	if (!symm) {
	continue;
	}

	for (int i = 1; i < spec.nr_steps; i++) {
	for (int l = 2; l < spec.nr_in + i; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	if (!(j == q \|\| k == q \|\| l == q) \|\| (j == p \|\| k == p)) {
	continue;
	}
	pLits[0] = pabc::Abc_Var2Lit(get_sel_var(spec, i, j, k, l), 1);
	auto ctr = 1;
	for (int ip = 0; ip < i; ip++) {
	for (int lp = 2; lp < spec.nr_in + ip; lp++) {
	for (int kp = 1; kp < lp; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if (jp == p \|\| kp == p \|\| lp == p) {
	pLits[ctr++] = pabc::Abc_Var2Lit(get_sel_var(spec, ip, jp, kp, lp), 0);
	}
	}
	}
	}
	}
	if (!solver->add_clause(pLits, pLits + ctr)) {
	return false;
	}
	}
	}
	}
	}
	}
	}
	return true;
	}

	bool create_symvar_clauses(const spec& spec, const partial_dag& dag)
	{
	for (int q = 1; q < spec.nr_in; q++) {
	for (int p = 0; p < q; p++) {
	auto symm = true;
	for (int i = 0; i < spec.nr_nontriv; i++) {
	auto f = spec[spec.synth_func(i)];
	if (!(swap(f, p, q) == f)) {
	symm = false;
	break;
	}
	}
	if (!symm) {
	continue;
	}

	for (int i = 1; i < spec.nr_steps; i++) {
	const auto vertex = dag.get_vertex(i);
	const auto nr_pi_fanins = nr_pi_fanins_for_step(dag, i);

	if (nr_pi_fanins == 0) {
	continue;
	} else if (nr_pi_fanins == 1) {
	const auto sel_var = get_sel_var(spec, dag, i, q);
	pLits[0] = pabc::Abc_Var2Lit(sel_var, 1);
	auto ctr = 1;
	for (int ip = 0; ip < i; ip++) {
	const auto vertex2 = dag.get_vertex(ip);
	auto nr_pi_fanins2 = nr_pi_fanins_for_step(dag, ip);
	if (nr_pi_fanins2 == 0) {
	continue;
	} else if (nr_pi_fanins2 == 1) {
	const auto sel_varp = get_sel_var(spec, dag, ip, p);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 0);
	} else if (nr_pi_fanins2 == 2) {
	auto svar_ctr = 0;
	for (int k = 1; k < spec.nr_in; k++) {
	for (int j = 0; j < k; j++) {
	if (j == p \|\| k == p) {
	const auto sel_varp = get_sel_var(spec, dag, ip, svar_ctr);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 0);
	}
	svar_ctr++;
	}
	}
	} else {
	auto svar_ctr = 0;
	for (int l = 2; l < spec.nr_in; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	if (j == p \|\| k == p \|\| l == p) {
	const auto sel_varp = get_sel_var(spec, dag, ip, svar_ctr);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 0);
	}
	svar_ctr++;
	}
	}
	}
	}
	}
	if (!solver->add_clause(pLits, pLits + ctr)) {
	return false;
	}
	} else if (nr_pi_fanins == 2) {
	auto svar_ctr = 0;
	for (int k = 1; k < spec.nr_in; k++) {
	for (int j = 0; j < k; j++) {
	if (!(j == q \|\| k == q) \|\| j == p) {
	svar_ctr++;
	continue;
	}
	const auto sel_var = get_sel_var(spec, dag, i, svar_ctr);
	pLits[0] = pabc::Abc_Var2Lit(sel_var, 1);
	auto ctr = 1;
	for (int ip = 0; ip < i; ip++) {
	const auto vertex2 = dag.get_vertex(ip);
	const auto nr_pi_fanins2 = nr_pi_fanins_for_step(dag, ip);
	if (nr_pi_fanins2 == 0) {
	continue;
	} else if (nr_pi_fanins2 == 1) {
	const auto sel_varp = get_sel_var(spec, dag, ip, p);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 0);
	} else if (nr_pi_fanins2 == 2) {
	auto svar_ctrp = 0;
	for (int kp = 1; kp < spec.nr_in; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if (jp == p \|\| kp == p) {
	const auto sel_varp = get_sel_var(spec, dag, ip, svar_ctrp);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 0);
	}
	svar_ctrp++;
	}
	}
	} else {
	auto svar_ctrp = 0;
	for (int lp = 2; lp < spec.nr_in; lp++) {
	for (int kp = 1; kp < lp; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if (jp == p \|\| kp == p \|\| lp == p) {
	const auto sel_varp = get_sel_var(spec, dag, ip, svar_ctrp);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 0);
	}
	svar_ctrp++;
	}
	}
	}
	}
	}
	if (!solver->add_clause(pLits, pLits + ctr)) {
	return false;
	}
	svar_ctr++;
	}
	}
	} else {
	auto svar_ctr = 0;
	for (int l = 2; l < spec.nr_in; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	if (!(j == q \|\| k == q \|\| l == q) \|\| (j == p \|\| k == p)) {
	svar_ctr++;
	continue;
	}
	const auto sel_var = get_sel_var(spec, dag, i, svar_ctr);
	pLits[0] = pabc::Abc_Var2Lit(sel_var, 1);
	auto ctr = 1;
	for (int ip = 0; ip < i; ip++) {
	const auto vertex2 = dag.get_vertex(ip);
	auto nr_pi_fanins2 = nr_pi_fanins_for_step(dag, ip);
	if (nr_pi_fanins2 == 0) {
	continue;
	} else if (nr_pi_fanins2 == 1) {
	const auto sel_varp = get_sel_var(spec, dag, ip, p);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 0);
	} else if (nr_pi_fanins2 == 2) {
	auto svar_ctrp = 0;
	for (int kp = 1; kp < spec.nr_in; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if (jp == p \|\| kp == p) {
	const auto sel_varp = get_sel_var(spec, dag, ip, svar_ctrp);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 0);
	}
	svar_ctrp++;
	}
	}
	} else {
	auto svar_ctrp = 0;
	for (int lp = 2; lp < spec.nr_in; lp++) {
	for (int kp = 1; kp < lp; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if (jp == p \|\| kp == p \|\| lp == p) {
	const auto sel_varp = get_sel_var(spec, dag, ip, svar_ctrp);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 0);
	}
	svar_ctrp++;
	}
	}
	}
	}
	}
	if (!solver->add_clause(pLits, pLits + ctr)) {
	return false;
	}
	svar_ctr++;
	}
	}
	}
	}
	}
	}
	}
	return true;
	}

	void fence_create_symvar_clauses(const spec& spec)
	{
	for (int q = 1; q < spec.nr_in; q++) {
	for (int p = 0; p < q; p++) {
	auto symm = true;
	for (int i = 0; i < spec.nr_nontriv; i++) {
	auto& f = spec[spec.synth_func(i)];
	if (!(swap(f, p, q) == f)) {
	symm = false;
	break;
	}
	}
	if (!symm) {
	continue;
	}
	for (int i = 1; i < spec.nr_steps; i++) {
	const auto level = get_level(spec, i + spec.nr_in);
	int svar_ctr = 0;
	for (int l = first_step_on_level(level - 1);
	l < first_step_on_level(level); l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	if (!(j == q \|\| k == q \|\| l == q) \|\| (j == p \|\| k == p)) {
	svar_ctr++;
	continue;
	}
	const auto sel_var = get_sel_var(spec, i, svar_ctr);
	pLits[0] = pabc::Abc_Var2Lit(sel_var, 1);
	auto ctr = 1;
	for (int ip = 0; ip < i; ip++) {
	const auto levelp = get_level(spec, spec.nr_in + ip);
	auto svar_ctrp = 0;
	for (int lp = first_step_on_level(levelp - 1);
	lp < first_step_on_level(levelp); lp++) {
	for (int kp = 1; kp < lp; kp++) {
	for (int jp = 0; jp < kp; jp++) {
	if (jp == p \|\| kp == p \|\| lp == p) {
	const auto sel_varp = get_sel_var(spec, ip, svar_ctrp);
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_varp, 0);
	}
	svar_ctrp++;
	}
	}
	}
	}
	(void)solver->add_clause(pLits, pLits + ctr);
	svar_ctr++;
	}
	}
	}
	}
	}
	}
	}

	void create_cardinality_constraints(const spec& spec)
	{
	std::vector<int> svars;
	std::vector<int> rvars;

	for (int i = 0; i < spec.nr_steps; i++) {
	svars.clear();
	rvars.clear();
	const auto level = get_level(spec, spec.nr_in + i);
	auto svar_ctr = 0;
	for (int l = first_step_on_level(level - 1);
	l < first_step_on_level(level); l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, i, svar_ctr++);
	svars.push_back(sel_var);
	}
	}
	}
	assert(svars.size() == nr_svars_for_step(spec, i));
	const auto nr_res_vars = (1 + 2) * (svars.size() + 1);
	for (int j = 0; j < nr_res_vars; j++) {
	rvars.push_back(get_res_var(spec, i, j));
	}
	create_cardinality_circuit(solver, svars, rvars, 1);

	// Ensure that the fanin cardinality for each step i
	// is exactly FI.
	const auto fi_var =
	get_res_var(spec, i, svars.size() * (1 + 2) + 1);
	auto fi_lit = pabc::Abc_Var2Lit(fi_var, 0);
	(void)solver->add_clause(&fi_lit, &fi_lit + 1);
	}
	}

	void reset_sim_tts(int nr_in)
	{
	for (int i = 0; i < NR_SIM_TTS; i++) {
	sim_tts[i] = kitty::dynamic_truth_table(nr_in);
	if (i < nr_in) {
	kitty::create_nth_var(sim_tts[i], i);
	}
	}
	}

	bool encode(const spec& spec)
	{
	assert(spec.nr_in >= 3);

	create_variables(spec);
	create_main_clauses(spec);

	if (!create_fanin_clauses(spec)) {
	return false;
	}

	if (spec.add_alonce_clauses) {
	create_alonce_clauses(spec);
	}

	if (spec.add_colex_clauses) {
	create_colex_clauses(spec);
	}

	if (spec.add_noreapply_clauses) {
	create_noreapply_clauses(spec);
	}

	if (spec.add_symvar_clauses && !create_symvar_clauses(spec)) {
	return false;
	}

	return true;
	}

	bool encode(const spec& spec, const partial_dag& dag)
	{
	create_variables(spec, dag);
	create_main_clauses(spec, dag);

	if (!create_fanin_clauses(spec, dag)) {
	return false;
	}

	if (spec.add_noreapply_clauses && !create_noreapply_clauses(spec, dag)) {
	return false;
	}

	if (spec.add_colex_clauses) {
	create_colex_clauses(spec, dag);
	}

	if (spec.add_symvar_clauses && !create_symvar_clauses(spec, dag)) {
	return false;
	}

	return true;
	}

	void update_level_map(const spec& spec, const fence& f)
	{
	nr_levels = f.nr_levels();
	level_dist[0] = spec.nr_in;
	for (int i = 1; i <= nr_levels; i++) {
	level_dist[i] = level_dist[i-1] + f.at(i-1);
	}
	}

	int get_level(const spec& spec, int step_idx) const
	{
	// PIs are considered to be on level zero.
	if (step_idx < spec.nr_in) {
	return 0;
	} else if (step_idx == spec.nr_in) {
	// First step is always on level one
	return 1;
	}
	for (int i = 0; i <= nr_levels; i++) {
	if (level_dist[i] > step_idx) {
	return i;
	}
	}
	return -1;
	}

	bool fence_create_fanin_clauses(const spec& spec)
	{
	bool res = true;

	for (int i = 0; i < spec.nr_steps; i++) {
	const auto nr_svars_for_i = nr_svars_for_step(spec, i);
	for (int j = 0; j < nr_svars_for_i; j++) {
	const auto sel_var = get_sel_var(spec, i, j);
	pLits[j] = pabc::Abc_Var2Lit(sel_var, 0);
	}

	res &= solver->add_clause(pLits, pLits + nr_svars_for_i);
	}

	return res;
	}

	bool
	encode(const spec& spec, const fence& f)
	{
	assert(spec.nr_in >= 3);
	assert(spec.nr_steps == f.nr_nodes());

	update_level_map(spec, f);
	fence_create_variables(spec);
	if (!fence_create_main_clauses(spec)) {
	return false;
	}

	if (!fence_create_fanin_clauses(spec)) {
	return false;
	}

	if (spec.add_alonce_clauses) {
	fence_create_alonce_clauses(spec);
	}

	if (spec.add_colex_clauses) {
	fence_create_colex_clauses(spec);
	}

	if (spec.add_noreapply_clauses) {
	fence_create_noreapply_clauses(spec);
	}

	if (spec.add_symvar_clauses) {
	fence_create_symvar_clauses(spec);
	}

	return true;
	}

	bool
	cegar_encode(const spec& spec, const fence& f)
	{
	update_level_map(spec, f);
	cegar_fence_create_variables(spec);
	for (int i = 0; i < spec.nr_rand_tt_assigns; i++) {
	const auto t = rand() % spec.get_tt_size();
	(void)fence_create_tt_clauses(spec, t);
	}

	if (!fence_create_fanin_clauses(spec)) {
	return false;
	}
	create_cardinality_constraints(spec);

	if (spec.add_alonce_clauses) {
	fence_create_alonce_clauses(spec);
	}

	if (spec.add_colex_clauses) {
	fence_create_colex_clauses(spec);
	}

	if (spec.add_noreapply_clauses) {
	fence_create_noreapply_clauses(spec);
	}

	if (spec.add_symvar_clauses) {
	fence_create_symvar_clauses(spec);
	}

	return true;

	assert(false);
	return false;
	}

	void extract_chain(const spec& spec, chain& chain)
	{
	int op_inputs[3] = { 0, 0 };

	chain.reset(spec.nr_in, 1, spec.nr_steps);

	for (int i = 0; i < spec.nr_steps; i++) {
	const int op = 0;

	for (int l = 2; l < spec.nr_in + i; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, i, j, k, l);
	if (solver->var_value(sel_var)) {
	op_inputs[0] = j;
	op_inputs[1] = k;
	op_inputs[2] = l;
	break;
	}
	}
	}
	}
	chain.set_step(i, op_inputs[0], op_inputs[1], op_inputs[2], op);
	}

	// TODO: support multiple outputs
	chain.set_output(0,
	((spec.nr_steps + spec.nr_in) << 1) +
	((spec.out_inv) & 1));
	}

	void fence_extract_chain(const spec& spec, chain& chain)
	{
	int op_inputs[3] = { 0, 0, 0 };

	chain.reset(spec.nr_in, 1, spec.nr_steps);

	for (int i = 0; i < spec.nr_steps; i++) {
	const int op = 0;

	int ctr = 0;
	const auto level = get_level(spec, spec.nr_in + i);
	for (int l = first_step_on_level(level - 1);
	l < first_step_on_level(level); l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, i, ctr++);
	if (solver->var_value(sel_var)) {
	op_inputs[0] = j;
	op_inputs[1] = k;
	op_inputs[2] = l;
	break;
	}
	}
	}
	}
	chain.set_step(i, op_inputs[0], op_inputs[1], op_inputs[2], op);
	}

	// TODO: support multiple outputs
	chain.set_output(0,
	((spec.nr_steps + spec.nr_in) << 1) +
	((spec.out_inv) & 1));
	}

	void print_solver_state(spec& spec)
	{
	for (auto i = 0; i < spec.nr_steps; i++) {
	for (int l = 2; l < spec.nr_in + i; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, i, j, k, l);
	if (solver->var_value(sel_var)) {
	printf("s[%d][%d][%d][%d]=1\n", i, j, k, l);
	} else {
	printf("s[%d][%d][%d][%d]=0\n", i, j, k, l);
	}
	}
	}
	}
	}

	for (auto i = 0; i < spec.nr_steps; i++) {
	printf("tt_%d_0=0\n", i);
	for (int t = 0; t < spec.tt_size; t++) {
	const auto sim_var = get_sim_var(spec, i, t);
	if (solver->var_value(sim_var)) {
	printf("tt_%d_%d=1\n", i, t + 1);
	} else {
	printf("tt_%d_%d=0\n", i, t + 1);
	}
	}
	}
	}

	void print_solver_state(spec& spec, const partial_dag& dag)
	{
	for (auto i = 0; i < spec.nr_steps; i++) {
	const auto& vertex = dag.get_vertex(i);
	const auto nr_pi_fanins = nr_pi_fanins_for_step(dag, i);
	if (nr_pi_fanins == 0) {
	continue;
	} else if (nr_pi_fanins == 1) {
	const auto l = vertex[2] + spec.nr_in - 1;
	const auto k = vertex[1] + spec.nr_in - 1;
	for (int j = 0; j < spec.nr_in; j++) {
	const auto sel_var = get_sel_var(spec, dag, i, j);
	if (solver->var_value(sel_var)) {
	printf("s[%d][%d][%d][%d]=1\n", i, j, k, l);
	} else {
	printf("s[%d][%d][%d][%d]=0\n", i, j, k, l);
	}
	}
	} else if (nr_pi_fanins == 2) {
	int ctr = 0;
	const auto l = vertex[2] + spec.nr_in - 1;
	for (int k = 1; k < spec.nr_in; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, dag, i, ctr++);
	if (solver->var_value(sel_var)) {
	printf("s[%d][%d][%d][%d]=1\n", i, j, k, l);
	} else {
	printf("s[%d][%d][%d][%d]=0\n", i, j, k, l);
	}
	}
	}
	} else if (nr_pi_fanins == 3) {
	int ctr = 0;
	for (int l = 2; l < spec.nr_in; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, dag, i, ctr++);
	if (solver->var_value(sel_var)) {
	printf("s[%d][%d][%d][%d]=1\n", i, j, k, l);
	} else {
	printf("s[%d][%d][%d][%d]=0\n", i, j, k, l);
	}
	}
	}
	}
	}

	for (auto i = 0; i < spec.nr_steps; i++) {
	printf("tt_%d_0=0\n", i);
	for (int t = 0; t < spec.tt_size; t++) {
	const auto sim_var = get_sim_var(spec, i, t);
	if (solver->var_value(sim_var)) {
	printf("tt_%d_%d=1\n", i, t + 1);
	} else {
	printf("tt_%d_%d=0\n", i, t + 1);
	}
	}
	}
	}
	}

	void fence_print_solver_state(spec& spec)
	{
	for (auto i = 0; i < spec.nr_steps; i++) {
	const auto level = get_level(spec, i);
	for (int l = first_step_on_level(level - 1);
	l < first_step_on_level(level); l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, i, j, k, l);
	if (solver->var_value(sel_var)) {
	printf("s[%d][%d][%d][%d]=1\n", i, j, k, l);
	} else {
	printf("s[%d][%d][%d][%d]=0\n", i, j, k, l);
	}
	}
	}
	}
	}

	for (auto i = 0; i < spec.nr_steps; i++) {
	printf("tt_%d_0=0\n", i);
	for (int t = 0; t < spec.tt_size; t++) {
	const auto sim_var = get_sim_var(spec, i, t);
	if (solver->var_value(sim_var)) {
	printf("tt_%d_%d=1\n", i, t + 1);
	} else {
	printf("tt_%d_%d=0\n", i, t + 1);
	}
	}
	}
	}

	bool cegar_encode(const spec& spec)
	{
	// TODO: implement
	assert(false);
	return false;
	}

	bool block_solution(const spec& spec)
	{
	int ctr = 0;
	for (int i = 0; i < spec.nr_steps; i++) {
	for (int l = 2; l < spec.nr_in + i; l++) {
	for (int k = 1; k < l; k++) {
	for (int j = 0; j < k; j++) {
	const auto sel_var = get_sel_var(spec, i, j, k, l);
	if (solver->var_value(sel_var)) {
	pLits[ctr++] = pabc::Abc_Var2Lit(sel_var, 1);
	break;
	}
	}
	}
	}
	}
	assert(ctr == spec.nr_steps);

	return solver->add_clause(pLits, pLits + ctr);
	}

	bool block_struct_solution(const spec& spec)
	{
	return block_solution(spec);
	}

	bool is_dirty()
	{
	return dirty;
	}

	void set_dirty(bool _dirty)
	{
	dirty = _dirty;
	}

	};
	}

File Metadata

Mime Type: text/x-c++
Expires: Tue, Oct 27, 8:47 PM (7 h, 5 m)
Storage Engine: blob
Storage Format: Raw Data
Storage Handle: 411491
Default Alt Text: aig_encoder.hpp (71 KB)

aig_encoder.hppNo OneTemporaryActions

aig_encoder.hppView Options

File Metadata

Event Timeline

aig_encoder.hpp
No OneTemporary
Actions

aig_encoder.hpp
View Options