func (pb *Threshold) TranslateComplexThreshold() {

	glob.A(!pb.Empty(), "No Empty at this point.")
	glob.A(len(pb.Chains) == 0, "should not contain a chain")

	pb.Normalize(LE, true)
	pb.SortDescending()

	var err error
	switch *glob.Complex_flag {
	case "mdd":
		pb.Print10()
		pb.TranslateByMDD()
		if pb.Err != nil {
			panic(err.Error())
		}
		glob.D(pb.Id, " mdd:", pb.Clauses.Size())
	case "sn":
		pb.TranslateBySN()
		if pb.Err != nil {
			panic(err.Error())
		}
		glob.D(pb.Id, " Complex, SN:", pb.Clauses.Size())
	case "hybrid":
		tSN := pb.Copy()
		tMDD := pb.Copy()
		tSN.TranslateBySN()
		tMDD.TranslateByMDD()

		if tSN.Err != nil {
			panic(tSN.Err.Error())
		}

		glob.D(pb.Id, "Complex, SN:", tSN.Clauses.Size(), " mdd:", tMDD.Clauses.Size())

		if tMDD.Err == nil && tMDD.Clauses.Size() < tSN.Clauses.Size() {
			pb.Clauses.AddClauseSet(tMDD.Clauses)
			pb.TransTyp = CMDD
		} else {
			pb.Clauses.AddClauseSet(tSN.Clauses)
			pb.TransTyp = CSN
		}
	default:
		panic("Complex_flag option not available: " + *glob.Complex_flag)
	}

	glob.A(pb.Clauses.Size() > 0, pb.Id, " non-trivial pb should produce some clauses...")

	return
}

// finds trivially implied facts, returns set of facts
// removes such entries from the pb
// threshold can become empty!
func (pb *Threshold) Simplify() {

	if pb.Typ == OPT {
		glob.D(pb.IdS(), " is not simplyfied because is OPT")
		return
	}

	pb.Normalize(LE, true)

	entries := make([]Entry, 0, len(pb.Entries))

	for _, x := range pb.Entries {
		if x.Weight > pb.K {
			pb.Clauses.AddTaggedClause(pb.IdS()+"-simpl", sat.Neg(x.Literal))
		} else {
			entries = append(entries, x)
		}
	}

	pb.Entries = entries
	pb.Normalize(GE, true)

	if pb.SumWeights() == pb.K {
		for _, x := range pb.Entries {
			pb.Clauses.AddTaggedClause("Fact", x.Literal)
		}
		pb.Entries = []Entry{}
	}

	if pb.SumWeights() < pb.K {
		glob.D("c PB", pb.Id, "is UNSAT")
		pb.Entries = []Entry{}
		pb.K = -1
		// is unsatisfied: how to do that?
	}

	pb.Normalize(LE, true)
	if pb.SumWeights() <= pb.K {
		glob.D("c PB", pb.Id, "is redundant")
		pb.Entries = []Entry{}
	}

	if pb.Empty() {
		pb.Translated = true
	}

	return
}

// returns the encoding of this PB
func (pb *Threshold) Translate(K_lessOffset int64) sat.ClauseSet {
	glob.A(pb.Positive(), "no negative coefficients beyond this point")

	K := K_lessOffset + pb.Offset
	if pb.SumWeights() <= K {
		glob.D("opt init ignored")
		return sat.ClauseSet{}
	}

	pb_K := pb.Copy() //removes all clauses !
	pb_K.K = K
	pb_K.Typ = LE
	if len(pb_K.Chains) > 0 {
		pb_K.TranslateByMDDChain(pb_K.Chains)
	} else {
		pb_K.CategorizeTranslate1()
	}

	if pb_K.Err != nil { // case MDD construction did go wrong!
		glob.A(false, "Capacity of MDD reached, try to solve by not taking chains into account")
		pb_K := pb.Copy() //removes all clauses !
		pb_K.K = K
		pb_K.Typ = LE
		pb_K.CategorizeTranslate1()
	}
	return pb_K.Clauses
}

func TestTranslateAMO2(test *testing.T) {
	glob.D("TestTranslateAMO2")
	*glob.MDD_max_flag = 300000
	*glob.MDD_redundant_flag = false

	results := []int{40, 33, 29}

	for i := 0; i < 3; i++ {

		//fmt.Println()
		pb1 := CreatePB([]int64{2, 2, 3, 4, 4, 5, 2, 1}, 8)
		pb2 := CreatePBOffset(i, []int64{1, 1, 1, 1}, 1)

		//pb1.Print10()
		//pb2.Print10()

		b, literals := pb2.Cardinality()
		amo := TranslateAtMostOne(Count, "c", literals)
		amo.PB = &pb2

		TranslatePBwithAMO(&pb1, amo)
		//t.Clauses.PrintDebug()

		if !b || pb1.Clauses.Size() != results[i] {
			fmt.Println("translation size incorrect", pb1.Clauses.Size(), " should be", results[i])
			//t.Clauses.PrintDebug()
			test.Fail()
		}
	}

}

func TestTranslate(test *testing.T) {
	glob.D("TestTranslate")

	pb1 := CreatePB([]int64{1, 1, 1}, 1)
	pb1.CategorizeTranslate1()
	if pb1.TransTyp != AMO {
		pb1.Print10()
		test.Errorf("1: Does not classify atmostOne")
	}

	pb2 := CreatePB([]int64{1, 1, 1}, 1)
	pb2.Typ = GE
	pb2.CategorizeTranslate1()
	if pb2.TransTyp != Clause {
		pb2.Print10()
		test.Errorf("2: Does not classify a clause")
	}

	pb3 := CreatePB([]int64{1, 1, 1}, 1)
	pb3.Typ = EQ
	pb3.CategorizeTranslate1()

	if pb3.TransTyp != EX1 {
		pb3.Print10()
		test.Errorf("3: Does not classify ExactlyOne")
	}

	pb4 := CreatePB([]int64{1, 1, -1}, 0)
	pb4.Typ = EQ
	pb4.CategorizeTranslate1()

	if pb4.TransTyp != EX1 {
		pb4.Print10()
		test.Errorf("4: Does not classify ExactlyOne")
	}

	pb5 := CreatePB([]int64{-3, 3, -3}, 0)
	pb5.Typ = LE
	pb5.CategorizeTranslate1()

	if pb5.TransTyp != Clause { // should be different
		pb5.Print10()
		test.Errorf("5: Does not classify clause", pb5)
	}

	pb6 := CreatePB([]int64{1, 1, 1, 1, 1}, 4)
	pb6.Typ = EQ
	pb6.CategorizeTranslate1()

	if pb6.TransTyp != EX1 {
		test.Errorf("6: Does not classify ExactlyOne", pb6)
	}

}

func TestRemoveZeros(test *testing.T) {
	glob.D("TestRemoveZeros")

	pb1 := CreatePB([]int64{1, 2, 3, 0, 321, 0, 0, -123, 0}, 1347)
	c := len(pb1.Entries)
	pb1.RemoveZeros()

	if len(pb1.Entries) != c-4 {
		test.Fail()
	}
}

func doChaining(pbs []*Threshold, complOcc map[sat.Literal][]int, simplOcc map[sat.Literal][]int,
	lit2id map[sat.Literal]int, litSets []intsets.Sparse) {

	//2) Prepare Matchings

	checked := make(map[Match]bool, 0)

	//ex_matchings := make(map[int][]Matching, 0)  // simpl_id -> []Matchings
	//currently ex and amo matchings are treated equivalently, the only
	//difference is that ex adds the unit clause of the ladder encoding, thus
	//the rewrite is correct and after UP the first value in the Ex is propagated.
	// TODO: explicitly rewrite and remove smallest value

	amo_matchings := make(map[int][]Matching, 0) // compl_id -> []Matchings

	for lit, list := range complOcc {
		//id2lit[lit2id[lit]] = lit
		for _, c := range list {
			for _, s := range simplOcc[lit] {
				if !checked[Match{c, s}] {
					// of comp c and simpl s there is at least
					checked[Match{c, s}] = true
					// 0 means it has not been checked,
					// as there is at least one intersection
					var inter intsets.Sparse
					inter.Intersection(&litSets[c], &litSets[s])
					if pbs[s].Typ == LE {
						if inter.Len() >= *glob.Len_rewrite_amo_flag {
							amo_matchings[c] = append(amo_matchings[c], Matching{s, &inter})
						}
					} else if pbs[s].Typ == EQ {
						if inter.Len() >= *glob.Len_rewrite_ex_flag {
							amo_matchings[c] = append(amo_matchings[c], Matching{s, &inter})
							//ex_matchings[c] = append(amo_matchings[c], Matching{s, &inter})
						}
					} else {
						glob.A(false, "case not treated")
					}
				}
			}
		}
	}

	glob.D("amo/ex_matchings:", len(amo_matchings))

	//3) amo/ex matchings

	for comp, _ := range pbs {
		if matchings, b := amo_matchings[comp]; b {
			workOnMatching(pbs, comp, matchings, lit2id, litSets)
		}
	}
}

func TestSNTranslation(test *testing.T) {
	glob.D("TestSortingNetworkTranslation")

	pb := createIgnasi2()

	pb.TranslateBySN()

	//filename := "test"
	//typ := sorters.Bubble
	//typ := sorters.Pairwise
	//typ := sorters.Bitonic
	//typ := sorters.OddEven

	//Example 1
	//t := createCardinality(4, 15, 5)
	//t := createCardinality(2, 1, 1)
	//t := createCardinality(9, 1, 1)

	//Example 2
	//t := createCardinality(8, 4, 1)
	//t := createCardinality(8,8,2)
	//t := createCardinality(8,16,4)
	//filename := "cardinality_8_16_4"

	//Example 3
	//t := createCardinality(8,12,3)
	//filename := "cardinality_8_12_3"

	//Example 4
	//t := createExample1()
	//filename := "example1"

	//Example 5
	//t := createJapan1(80)
	//filename := "japan1_10"

	//Example 6
	//t := createJapan2(3)
	//filename := "japan2_3"

	//t1 := createIgnasi1()
	//t2 := createIgnasi2()

	//s1 := NewSortingNetwork(t1)
	//s2 := NewSortingNetwork(t2)

	//fmt.Println(t)

	//PrintThresholdTikZ(filename+".tex", []SortingNetwork{s1, s2})

}

func (g *Gen) generateIds(cs ClauseSet, inferPrimeVars bool) { // recalculates new sat ids for each atom:
	// assuming full regeneration of Ids
	// might change existing mappings

	g.refresh()

	glob.D("c auxiliary Ids start with", g.nextId)

	for _, c := range cs.list {
		for _, l := range c.Literals {
			g.putAtom(l.A)
		}
	}
}

func (pb *Threshold) Evaluate(a sat.Assignment) (r int64) {

	for _, e := range pb.Entries {
		v, b := a[e.Literal.A.Id()]
		glob.DT(!b, "Literal not found in assignment: ", e.Literal.ToTxt())
		if e.Literal.Sign {
			r += int64(v) * e.Weight
		} else {
			r += (1 - int64(v)) * e.Weight
		}
	}
	glob.D("evaluate", r, pb.Offset)

	return r - pb.Offset
}

func TestRewriteExactly4(test *testing.T) {
	glob.D("TestExactly3")

	pb1 := CreatePB([]int64{2, 2, 3, 4, 1, 1}, 6)
	pb1.Typ = LE

	pb2 := CreatePB([]int64{1, 1, 1, 1}, 2)
	pb2.Typ = EQ
	pb2.Entries[2].Literal = sat.Neg(pb2.Entries[2].Literal)

	b := PreprocessPBwithExactly(&pb1, &pb2)

	if b {
		test.Fail()
	}

}

func TestMDDChains1(test *testing.T) {
	//glob.Debug_flag = true

	glob.D("TestMDDChains1")

	*glob.MDD_max_flag = 300000
	*glob.MDD_redundant_flag = false

	var t Threshold
	t.Entries = createEntries([]int64{1, 2, 1, 1, 3, 1})
	t.Typ = LE
	t.K = 5
	//t.Print10()

	{ // check
		store := mdd.InitIntervalMdd(len(t.Entries))
		_, _, _, s1 := CreateMDD(&store, t.K, t.Entries)
		//store.Debug(true)
		if s1 != nil {
			test.Fail()
		}
	}

	chain := Chain(t.Literals()) //createLiterals(i, 3)

	//fmt.Println("\n\n Chain on index", i, i+3)

	chains := Chains{chain[0:3], chain[3:6]}
	//chains[0].Print()

	store := mdd.InitIntervalMdd(len(t.Entries))
	_, _, _, s1 := CreateMDDChain(&store, t.K, t.Entries, chains)

	if s1 != nil {
		test.Fail()
	}
	if len(store.Nodes) != 6 {
		store.Debug(true)
		test.Fail()
	}
	//glob.Debug_flag = false
}

func TestCleanChain(test *testing.T) {
	glob.D("TestCleanChain")

	pb := CreatePB([]int64{1, 2, 3, 0, 321, 0, 1, -123, 0}, 1347)
	results := []int{3, 3, 2, 0, 3, 0}

	chain := pb.Literals()

	pb.RemoveZeros()

	for i := 0; i < len(chain)-4; i++ {
		c1 := chain[i : i+4]
		c2 := CleanChain(pb.Entries, c1)
		if results[i] != len(c2) {
			fmt.Println(results[i], len(c2))
			test.Fail()
		}
	}

}

func TestMDDRedundant(test *testing.T) {
	//glob.Debug_flag = true
	//glob.Debug_flag = false

	glob.D("TestMDDRedundant")
	*glob.MDD_max_flag = 300000
	*glob.MDD_redundant_flag = false

	var t Threshold
	t.Entries = createEntries([]int64{1, 2, 1, 1, 3, 1})
	t.Typ = LE
	t.K = 5

	store := mdd.InitIntervalMdd(len(t.Entries))
	CreateMDD(&store, t.K, t.Entries)

	if store.RemoveRedundants() != 5 {
		test.Fail()
	}
}

func TestMDDChains2(test *testing.T) {
	//glob.Debug_flag = true

	glob.D("TestMDDChains")

	*glob.MDD_max_flag = 300000
	*glob.MDD_redundant_flag = false

	var t Threshold
	t.Entries = createEntries([]int64{1, 2, 1, 1, 3, 1, 3, 2, 1, 1, 1})
	t.Typ = LE
	t.K = 10
	//t.Print10()

	{ // check
		store := mdd.InitIntervalMdd(len(t.Entries))
		_, _, _, s1 := CreateMDD(&store, t.K, t.Entries)
		//store.Debug(true)
		if s1 != nil {
			test.Fail()
		}
	}

	chain := Chain(t.Literals()) //createLiterals(i, 3)

	chains := Chains{chain[1:3], chain[5:9]}

	store := mdd.InitIntervalMdd(len(t.Entries))
	_, _, _, s1 := CreateMDDChain(&store, t.K, t.Entries, chains)

	if s1 != nil {
		test.Fail()
	}
	if len(store.Nodes) != 31 {
		store.Debug(true)
		test.Fail()
	}
	//glob.Debug_flag = false
}

func TestRewriteExactly3(test *testing.T) {
	glob.D("TestExactly3")

	pb1 := CreatePB([]int64{2, 2, 3, 4, 1, 1}, 6)
	pb1.Typ = LE
	pb1.SortDescending()

	pb2 := CreatePB([]int64{1, 1, 1, 1}, 2)
	pb2.Typ = EQ

	//pb1.Print10()
	//pb2.Print10()

	b := PreprocessPBwithExactly(&pb1, &pb2)

	//pb1.Print10()
	//pb1.SortVar()
	//pb1.Print10()
	if !b && len(pb1.Entries) != 4 {
		test.Fail()
	}

}

func TestRewriteExactly1(test *testing.T) {
	glob.D("TestExactly1")

	//+2 x1 +2 x2 +3 x3 +4 x4 +1 x5 +1 x6 <= 6 ;
	//+1 x1 +1 x2 +1 x3 +1 x4 = 1 ;

	pb1 := CreatePB([]int64{2, 2, 3, 4, 1, 1}, 6)
	pb1.Typ = LE

	pb2 := CreatePB([]int64{1, 1, 1, 1}, 1)
	pb2.Typ = EQ

	//pb1.Print10()
	//pb2.Print10()

	b := PreprocessPBwithExactly(&pb1, &pb2)
	if !b && len(pb1.Entries) != 4 {
		test.Fail()
	}

	//pb1.Print10()

}

func TestTranslateAMO1(test *testing.T) {
	glob.D("TestTranslateAMO1")
	*glob.MDD_max_flag = 300000
	*glob.MDD_redundant_flag = false

	pb1 := CreatePB([]int64{2, 2, 3, 4, 2, 3}, 6)
	pb2 := CreatePB([]int64{1, 1, 1, 1}, 1)

	//pb1.Print10()
	//pb2.Print10()

	//translate AMO, i.e. pb2
	b, literals := pb2.Cardinality()
	amo := TranslateAtMostOne(Count, "c", literals)
	amo.PB = &pb2

	TranslatePBwithAMO(&pb1, amo)

	if !b || pb1.Clauses.Size() != 13 {
		fmt.Println("translation size incorrect", pb1.Clauses.Size(), "should be:", 13)
		pb1.Clauses.PrintDebug()
		test.Fail()
	}
}

func TestRewriteAMO(test *testing.T) {
	glob.D("TestRewriteAMO1")

	pb1 := CreatePB([]int64{2, 2, 3, 4, 1, 1}, 6)
	pb2 := CreatePB([]int64{1, 1, 1, 1}, 1)

	//pb1.Print10()
	//pb2.Print10()

	//translate AMO, i.e. pb2
	b, literals := pb2.Cardinality()
	amo := TranslateAtMostOne(Count, "count", literals)
	amo.PB = &pb2

	b = PreprocessPBwithAMO(&pb1, amo)

	if !b || len(pb1.Entries) != 5 {
		test.Fail()
	}

	if sumE(pb1) != 6 {
		test.Fail()
	}
}

func (pb *Threshold) CatSimpl() {

	glob.A(!pb.Empty(), "pb should not be empty")

	if pb.Typ == OPT {
		glob.D(pb.IdS(), " is not simplyfied because is OPT")
		pb.TransTyp = UNKNOWN
		return
	}

	pb.Simplify()

	if pb.Empty() {
		pb.TransTyp = Facts
		return
	} else {

		if b, literals := pb.Cardinality(); b {

			if pb.K == int64(len(pb.Entries)-1) {
				switch pb.Typ {
				case LE:
					pb.Normalize(GE, true)
					for i, x := range literals {
						literals[i] = sat.Neg(x)
					}
				case GE:
					for i, x := range literals {
						literals[i] = sat.Neg(x)
					}
					pb.Normalize(LE, true)
				case EQ:
					for i, x := range literals {
						literals[i] = sat.Neg(x)
					}
					pb.Multiply(-1)
					pb.NormalizePositiveCoefficients()
				}
			}

			if pb.K == 1 {
				switch pb.Typ {
				case LE: // check for binary, which is also a clause ( ~l1 \/ ~l2 )
					if len(pb.Entries) == 2 {
						pb.Clauses.AddTaggedClause("Cls", sat.Neg(pb.Entries[0].Literal), sat.Neg(pb.Entries[1].Literal))
						pb.TransTyp = Clause
					} else {
						pb.TransTyp = AMO
					}
				case GE: // its a clause!
					pb.Clauses.AddTaggedClause("Cls", literals...)
					pb.TransTyp = Clause
				case EQ:
					pb.TransTyp = EX1
				}
			} else { //cardinality
				switch pb.Typ {
				case LE, GE, EQ:
					pb.CreateCardinality()
					pb.TransTyp = CARD
				}
			}
		}
	}
	return
}