// chains must be in order of pb and be subsets of its literals
func (pb *Threshold) TranslateByMDDChain(chains Chains) {
	glob.A(!pb.Empty(), pb.Id, "works only for non-empty mdds")
	glob.A(pb.Positive(), pb.Id, "Weights need to be positive")
	glob.A(pb.Typ == LE, pb.Id, "works only on LE, but is", pb.Typ, pb.String())

	if len(chains) == 0 {
		pb.TransTyp = CMDD
	} else {
		pb.TransTyp = CMDDC
	}

	store := mdd.InitIntervalMdd(len(pb.Entries))
	topId, _, _, err := CreateMDDChain(&store, pb.K, pb.Entries, chains)
	store.Top = topId
	//store.Debug(true)

	if err != nil {
		pb.Err = err
		return
	}

	if *glob.MDD_redundant_flag {
		store.RemoveRedundants()
		//glob.D("remove redundant nodes in MDD", removed)
	}

	pb.Clauses.AddClauseSet(convertMDD2Clauses(store, pb))
}

// 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
}

// finds the subexpression of chain1 in e and
// returns the entries of chain1 existing in e.
func CleanChain(entries []Entry, chain1 Chain) (chain2 Chain) {
	glob.A(len(chain1) > 0, "no non-empty chains")

	chain2 = make(Chain, len(chain1))

	e := 0
	// find start of chain
	for i, x := range entries {
		if x.Literal == chain1[0] {
			e = i
			break
		}
		glob.A(i <= len(entries)-1, "chain must exist within entries")
	}

	j2 := 0
	for j1, l := range chain1 {
		//fmt.Println("e", e, "j1", j1, "j2", j2)
		if e+j2 == len(entries) {
			break
		}
		if l == entries[e+j2].Literal {
			chain2[j2] = chain1[j1]
			j2++
		}
	}

	return chain2[:j2]
}

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
}

func (pb *Threshold) TranslateBySN() {
	pb.TransTyp = CSN
	pb.Normalize(LE, true)
	glob.A(pb.Typ == LE, "does not work on OPT or ==, but we have", pb.Typ)
	pb.SortDescending()
	sn := NewSortingNetwork(*pb)
	sn.CreateSorter()

	//glob.D("size of comparators", len(sn.Sorter.Comparators))

	//PrintThresholdTikZ("sn.tex", []SortingNetwork{sn})

	wh := 1
	var which [8]bool

	switch wh {
	case 1:
		which = [8]bool{false, false, false, true, true, true, false, false}
	case 2:
		which = [8]bool{false, false, false, true, true, true, false, true}
	case 3:
		which = [8]bool{false, true, true, true, true, true, true, false}
	case 4:
		which = [8]bool{false, true, true, true, true, true, true, true}
	}

	pred := sat.Pred("auxSN_" + strconv.Itoa(pb.Id))
	pb.Clauses.AddClauseSet(CreateEncoding(sn.LitIn, which, []sat.Literal{}, "BnB", pred, sn.Sorter))
}

// returns if preprocessing was successful
// Uses the translation of pb2 (count translation)
func PreprocessPBwithAMO(pb *Threshold, amo CardTranslation) bool {

	//assumptions:
	//check for correct property of pb2
	//check for overlap of literals
	//both pb1 and amo are in the same ordering

	glob.A(amo.PB != nil, "amo PB pointer is not set correctly!")
	b, es := CommonSlice(pb.Entries, amo.PB.Entries)
	//fmt.Println(amo.PB.Entries, es)

	if !b {
		panic("Check if amo fits  with the pb1")
	}

	last := int64(0)
	for i, e := range es {
		es[i].Weight = e.Weight - last
		es[i].Literal = amo.Aux[i]
		last = e.Weight
	}

	pb.RemoveZeros()

	return true
}

// all weights are the same; performs rounding
// if this is true, then all weights are 1, and K is the cardinality
func (t *Threshold) Cardinality() (allSame bool, literals []sat.Literal) {
	glob.A(len(t.Chains) == 0, "cant reorder Entries with chains")

	t.NormalizePositiveCoefficients()
	allSame = true

	coeff := t.Entries[0].Weight
	for _, x := range t.Entries {
		if x.Weight != coeff {
			allSame = false
			break
		}
	}

	if allSame {
		literals = make([]sat.Literal, len(t.Entries))
		/// was ceil before, what happened here?
		t.K = int64(math.Floor(float64(t.K) / float64(coeff)))
		for i, x := range t.Entries {
			t.Entries[i].Weight = 1
			literals[i] = x.Literal
		}

	}

	return allSame, literals
}

func (t *Threshold) NormalizePositiveLiterals() {
	glob.A(len(t.Chains) == 0, "cant reorder Entries with chains")

	for i, e := range t.Entries {
		if t.Entries[i].Literal.Sign == false {
			t.Entries[i].Literal = sat.Neg(e.Literal)
			t.K -= t.Entries[i].Weight
			t.Entries[i].Weight = -t.Entries[i].Weight
		}
	}
}

func nextOptIterative(lb int64, result *Result) (bool, int64) {
	if lb == result.Value {
		result.M = "OPTIMUM"
		return true, result.Value
	} else if lb < result.Value {
		return false, result.Value - 1
	} else {
		glob.A(false, "lb <= ub")
		return false, 0
	}
}

func nextOptValue(lb int64, result *Result) (finished bool, nextOpt int64) {
	switch *glob.Search_strategy_flag {
	case "iterative":
		finished, nextOpt = nextOptIterative(lb, result)
	case "binary":
		finished, nextOpt = nextOptBinary(lb, result)
	default:
		glob.A(false, "Search strategy not implemented", *glob.Search_strategy_flag)
	}
	return
}

func (pb *Threshold) PosAfterChains() int {
	current := 0

	for _, chain := range pb.Chains {
		for _, lit := range chain {
			glob.A(pb.Entries[current].Literal == lit, "chain is not aligned with PB", chain, pb)
			current++
		}
	}
	return current
}

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 nextOptBinary(lb int64, result *Result) (bool, int64) {

	if lb == result.Value {
		result.M = "OPTIMUM"
		return true, result.Value
	} else if lb < result.Value {
		return false, (lb + result.Value) / 2
	} else {
		glob.A(false, "lb <= ub")
		return false, 0
	}
}

// normalizes the threshold
// Change EquationType in case of LE/GE
// in case of EQ and OPT, positive weights
func (t *Threshold) Normalize(typ EquationType, posWeights bool) {
	glob.A(len(t.Chains) == 0, "cant reorder Entries with chains")

	if (typ == LE && t.Typ == GE) || (typ == GE && t.Typ == LE) {
		t.Multiply(-1)
	}

	if posWeights {
		t.NormalizePositiveCoefficients()
	} else {
		t.NormalizePositiveLiterals()
	}

	return
}

func (mddStore *IntervalMddStore) Insert(n IntervalNode) (id int) {

	//check code start TODO: remove for performance
	if a := mddStore.storage.Get(n); a != nil {
		fmt.Println("FAIL")
		printNode(a.(IntervalNode))
		panic("node should not exist")
	}
	//check code end

	n.Id = mddStore.NextId
	mddStore.Nodes = append(mddStore.Nodes, &n)
	mddStore.NextId++

	glob.A(mddStore.NextId == len(mddStore.Nodes), "nextId calculation and length of Nodes list is wrong")

	mddStore.storage.Insert(n)

	return n.Id
}

func printStats(stats []int) {

	glob.A(len(stats) == int(constraints.TranslationTypes), "Stats for translation errornous")

	trans := constraints.Facts
	fmt.Print("Name;")
	for i := trans; i < constraints.TranslationTypes; i++ {
		if i > 0 {
			fmt.Printf("%v;", constraints.TranslationType(i))
		}
	}
	fmt.Println()
	fmt.Print(*glob.Filename_flag, ";")
	for i := trans; i < constraints.TranslationTypes; i++ {
		if i > 0 {
			fmt.Printf("%v;", stats[i])
		}
	}
	fmt.Println()
}

func (g *Gen) putAtom(a Atom) {
	if _, b := g.mapping[a.Id()]; !b {
		succ := false
		if *glob.Infer_var_ids {
			id, err := strconv.Atoi(strings.TrimLeft(a.Id(), "v"))
			v := strings.TrimRight(a.Id(), "0123456789")
			if v == "v" && err == nil {
				glob.A(*glob.First_aux_id_flag > id, "Inferred number ID if higher than First_aux_id. Use values for first_aux  that a larger than id in all variables v<id>.")
				succ = true
				g.mapping[a.Id()] = id
				g.idMap[id] = a
			}
		}
		if !succ {
			g.nextId++
			g.mapping[a.Id()] = g.nextId
			g.idMap = append(g.idMap, a)
		}

	}
}

// CreateCardinality takes set of literals and creates a sorting network
func (pb *Threshold) CreateCardinality() {

	for _, x := range pb.Entries {
		glob.A(x.Weight == 1, "Prerequisite for this translation")
	}

	literals := pb.Literals()
	sx := strconv.Itoa(int(pb.K)) + "\\" + strconv.Itoa(len(literals))
	var s string
	var sorterEqTyp sorters.EquationType
	var w int // which type of clauses

	switch pb.Typ {
	case LE:
		w = 0
		sorterEqTyp = sorters.AtMost
		s = pb.IdS() + "pb<SN" + sx
	case GE:
		w = 3
		sorterEqTyp = sorters.AtLeast
		s = pb.IdS() + "pb>SN" + sx
	case EQ:
		w = 3
		s = pb.IdS() + "pb=SN" + sx
		sorterEqTyp = sorters.Equal
	default:
		panic("Not supported")
	}

	sorter := sorters.CreateCardinalityNetwork(len(literals), int(pb.K), sorterEqTyp, sorters.Pairwise)
	sorter.RemoveOutput()
	pred := sat.Pred("SN-" + pb.IdS())
	output := make([]sat.Literal, 0)
	pb.Clauses.AddClauseSet(CreateEncoding(literals, sorters.WhichCls(w), output, s, pred, sorter))

}

func workOnMatching(pbs []*Threshold, comp int, matchings []Matching,
	lit2id map[sat.Literal]int, litSets []intsets.Sparse) {
	glob.A(!pbs[comp].Translated, "comp", comp, "should not have been translated yet")

	var chains Chains
	//inter := &intsets.Sparse{}
	var comp_offset int // the  new first position of Entries in comp

	if !*glob.Amo_reuse_flag {
		//fmt.Println("before remove translated matches: len", len(matchings))
		// remove translated ones...
		p := len(matchings)
		for i := 0; i < p; i++ { // find the next non-translated one
			if pbs[matchings[i].simp].Translated {
				p--
				matchings[i] = matchings[p]
				i--
			}
		}
		matchings = matchings[:p]
		//fmt.Println("after removing translated matches: len", len(matchings))
	}

	for len(matchings) > 0 {

		//fmt.Println("len(matchings", len(matchings))
		sort.Sort(MatchingsBySize(matchings))
		matching := matchings[0]
		//glob.D(comp, matching.simp, matching.inter.Len())
		// choose longest matching, that is not translated yet
		//fmt.Println("check matching: simp", matching.simp, "inter", matching.inter.String())
		//matching.inter.IntersectionWith(&litSets[comp]) //update matching
		if matching.inter.Len() < *glob.Len_rewrite_amo_flag {
			break
		}
		inter := matching.inter
		simp := matching.simp

		//pbs[comp].Print10()
		//pbs[simp].Print10()
		//glob.D("entries", comp, litSets[comp].String(), simp, litSets[simp].String(), inter.String())

		ind_entries := make(IndEntries, inter.Len())
		comp_rest := make([]*Entry, len(pbs[comp].Entries)-inter.Len()-comp_offset)
		simp_rest := make([]*Entry, len(pbs[simp].Entries)-inter.Len())
		simp_offset := len(simp_rest)

		ind_pos := 0
		rest_pos := 0
		for i := comp_offset; i < len(pbs[comp].Entries); i++ {
			if inter.Has(lit2id[pbs[comp].Entries[i].Literal]) {
				ind_entries[ind_pos].c = &pbs[comp].Entries[i]
				ind_pos++
			} else {
				comp_rest[rest_pos] = &pbs[comp].Entries[i]
				rest_pos++
			}
		}

		ind_pos = 0
		rest_pos = 0
		for i, x := range pbs[simp].Entries {
			if inter.Has(lit2id[x.Literal]) {
				ind_entries[ind_pos].s = &pbs[simp].Entries[i]
				ind_pos++
			} else {
				simp_rest[rest_pos] = &pbs[simp].Entries[i]
				rest_pos++
			}
		}

		//fmt.Println("intersection of", litSets[comp].String(), litSets[simp].String())
		//fmt.Println("intersection", inter.String(), " len:", inter.Len())
		litSets[comp].DifferenceWith(inter)

		{ // remove intersecting matchings
			//fmt.Println("before remove intersecting matches: len", len(matchings))
			p := len(matchings)
			for i := 1; i < p; i++ { // find the next non-translated one
				//var tmp intsets.Sparse
				//			glob.D("before", matchings[i].inter.String())
				//				glob.D("inter", inter.String())
				matchings[i].inter.DifferenceWith(inter)
				//			glob.D("after ", matchings[i].inter.String())
				//if tmp.Intersection(inter, matchings[i].inter); !tmp.IsEmpty() {
				if matchings[i].inter.IsEmpty() {
					//			fmt.Println("remove", matchings[i].inter.String())
					p--
					matchings[i] = matchings[p]
					i--
				}
			}
			matchings = matchings[1:p]
			//fmt.Println("after removing intersecting matches: len", len(matchings))
		}

		sort.Sort(ind_entries)

		compEntries := make([]Entry, len(pbs[comp].Entries))
		simpEntries := make([]Entry, len(pbs[simp].Entries))
//.........这里部分代码省略.........

func (t *SortingNetwork) CreateSorter() {

	glob.A(!t.pb.Empty(), "No empty at this point.")

	t.CreateBags()

	layers := make([]sorters.Sorter, len(t.Bags))

	for i, bag := range t.Bags {

		layers[i] = sorters.CreateSortingNetwork(len(bag), -1, t.typ)

		t.LitIn = append(t.LitIn, bag...)
	}

	t.Sorter.In = make([]int, 0, len(t.LitIn))
	t.Sorter.Out = make([]int, 0, len(t.LitIn))

	offset := 2

	// determine the constant and what to add on both sides
	layerPow2 := int64(1 << uint(len(t.Bags)))

	tare := layerPow2 - ((t.pb.K + 1) % layerPow2)
	tare = tare % layerPow2
	t.Tare = tare
	bTare := Binary(tare)

	// output of sorter in layer $i-1$
	bIn := make([]int, 0)

	finalMapping := make(map[int]int, len(t.Sorter.In))

	for i, layer := range layers {

		offset = layer.Normalize(offset, []int{})
		t.Sorter.Comparators = append(t.Sorter.Comparators, layer.Comparators...)

		t.Sorter.In = append(t.Sorter.In, layer.In...)

		size := len(bIn) + len(layers[i].In)

		mergeIn := make([]int, 0, size)
		mergeIn = append(mergeIn, bIn...)
		mergeIn = append(mergeIn, layer.Out...)

		merger := sorters.CreateSortingNetwork(size, len(bIn), t.typ)
		offset = merger.Normalize(offset, mergeIn)

		// halving circuit:

		odd := 1

		if i < len(bTare) && bTare[i] == 1 {
			odd = 0
			bIn = make([]int, (len(merger.Out)+1)/2)
		} else {
			bIn = make([]int, len(merger.Out)/2)
		}

		// Alternate depending on bTare
		for j, x := range merger.Out {
			if j%2 == odd {
				bIn[j/2] = x
			} else if i < len(layers)-1 { // not in last layer, but else
				finalMapping[x] = -1
			}
		}

		t.Sorter.Comparators = append(t.Sorter.Comparators, merger.Comparators...)

	}

	// outLastLayer identifies the nth output in the last layer
	outLastLayer := ((t.pb.K + 1 + tare) / int64(layerPow2)) - 1

	// debug stuff:
	//glob.D("len last layer:", len(bIn), "kth output in last layer: ", outLastLayer)
	//glob.D("K+1+tar", t.pb.K+1+tare, "n layers", layerPow2)

	idSetToZero := bIn[outLastLayer]

	// and propagate the rest backwards
	setTo := -1 // dont care
	for _, id := range t.Sorter.ComputeOut() {
		if id == idSetToZero {
			setTo = 0
		}
		if _, ok := finalMapping[id]; !ok {
			finalMapping[id] = setTo
		}
	}

	t.Sorter.PropagateBackwards(finalMapping)
	t.Sorter.Normalize(2, []int{})

	//fmt.Println("LitIn", t.LitIn)
	//fmt.Println("final debug: tSorter", t.Sorter)

}