<commit_before>// Copyright <NAME> 2014. See the LICENSE file for more information.

package pigosat

import (
	"fmt"
	"reflect"
	"testing"
)

func TestLitArrayToSlice(t *testing.T) {
	// null pointers
	assertPanics(t, "null pointer", "litArrayToSlice",
		func() { litArrayToSlice(nil, 0) })
	assertPanics(t, "null pointer", "litArrayToSlice",
		func() { litArrayToSlice(nil, 1) })
	// not zero terminated
	badPtr := &cArray123[0]
	assertPanics(t, "not zero terminated - 1", "litArrayToSlice",
		func() { litArrayToSlice(badPtr, 1) })
	assertPanics(t, "not zero terminated - 2", "litArrayToSlice",
		func() { litArrayToSlice(badPtr, 2) })
	// zero length
	for maxLen := 0; maxLen <= 2; maxLen++ {
		if ls := litArrayToSlice(&cZero, 0); len(ls) != 0 {
			t.Errorf("Test 0-length litArrayToSlice, maxLen==%d: return value has length %d",
				maxLen, len(ls))
		}
	}
	// works correctly
	ptr := &cArray1230[0]
	expected := []Literal{1, 2, 3}
	for maxLen := 3; maxLen <= 10; maxLen++ {
		if ls := litArrayToSlice(ptr, maxLen); !reflect.DeepEqual(ls, expected) {
			t.Errorf("Test litArrayToSlice correct, maxLen==%d: expected %v but got %v",
				maxLen, expected, ls)
		}
	}
}

func TestAssumptionsSucceeding(t *testing.T) {
	successTests := []struct {
		assumpts  []Literal // The literals which should be assumed true/false
		solutions int       // The number of solutions that we expect to produce
	}{
		{[]Literal{1}, 10}, // We use formulaTests[0].formula below
		{[]Literal{2}, 9},
		{[]Literal{3}, 6},
		{[]Literal{4, 5}, 4},
	}

	for i, at := range successTests {
		p, _ := New(nil)
		p.AddClauses(formulaTests[0].formula)

		count := 0
		for ; ; count++ {
			for _, lit := range at.assumpts {
				p.Assume(lit)
			}
			status, sol := p.Solve()
			if status != Satisfiable {
				break
			}

			// All the UNSAT methods should give zero answers.
			if p.FailedAssumption(at.assumpts[0]) {
				t.Errorf("Test %d: FailedAssumption: expected %v not to be failed", i, at.assumpts[0])
			}
			if r := p.FailedAssumptions(); !reflect.DeepEqual(r, []Literal{}) {
				t.Errorf("Test %d: FailedAssumptions: expected [], got %v", i, r)
			}

			p.BlockSolution(sol)
		}
		if count != at.solutions {
			t.Errorf("Test %d: Expected %d solution(s) for assumptions %v; got %d",
				i, at.solutions, at.assumpts, count)
		}
	}
}

func TestAssumptionsFailing(t *testing.T) {
	p, _ := New(nil)
	p.AddClauses(formulaTests[0].formula)
	p.Assume(3)
	p.Assume(4)
	p.Assume(5)
	p.Solve()

	failed := []Literal{3, 4}
	if actual := p.FailedAssumptions(); !reflect.DeepEqual(failed, actual) {
		t.Errorf("Expected failed assumptions %v != %v actual", failed, actual)
	}
	for _, f := range failed {
		if !p.FailedAssumption(f) {
			t.Errorf("Expected literal %v to be a failed assumption", f)
		}
	}

	i, wanted := 0, [][]Literal{{3, 5}, {3, 5}, {5, 4}, {}}
	for a := p.MaxSatisfiableAssumptions(); len(a) > 0; i++ {
		if !reflect.DeepEqual(a, wanted[i]) {
			t.Errorf("(Next)MaxSat'Assumpt's: Got %v wanted %v", a, wanted[i])
		}
		a = p.NextMaxSatisfiableAssumptions()
	}
	if a := p.MaxSatisfiableAssumptions(); !reflect.DeepEqual(a, []Literal{}) {
		t.Errorf("MaxSatisfiableAssumptions: CNF inconsistent, so wanted []Literal{}, but got %v", a)
	}
}

// TestAssumptionsNoCrash tests that if you call Assume with a satisfiable
// assumption after Solve returns UNSAT then FailedAssumption(s) does not crash.
func TestCrashOnAssumeSatAfterUnsatThenCallFailedAssumptions(t *testing.T) {
	p, _ := New(nil)
	p.AddClauses(formulaTests[0].formula)
	p.Assume(3)
	p.Assume(4)
	p.Assume(5)
	p.Solve()

	if r := p.Res(); r != Unsatisfiable {
		t.Fatalf("Expected %v, got %v", Unsatisfiable, r)
	}
	if !p.FailedAssumption(3) {
		t.Fatalf("Expected literal 3 to be a failed assumption")
	}
	if r := p.Res(); r != Unsatisfiable {
		t.Fatalf("Expected %v, got %v", Unsatisfiable, r)
	}

	p.Assume(3)
	if r := p.Res(); r != Unsatisfiable {
		t.Fatalf("Expected %v, got %v", Unsatisfiable, r)
	}

	// Either the next two assertions work or they crash with this message:
	//   *** picosat: API usage: expected to be in UNSAT state
	//   SIGABRT: abort
	if p.FailedAssumption(3) {
		t.Errorf("FailedAssumption: Expected false, got true")
	}
	if r := p.FailedAssumptions(); len(r) != 0 {
		t.Errorf("FailedAssumptions: Expected []Literal{}, got %v", r)
	}
}

// ExamplePigosat_Assume demonstrates how to use Assume and related methods.
func ExamplePigosat_Assume() {
	var formula = Formula{{1, 2, 3}, {1, 2}, {2, 3}}
	p, _ := New(nil)
	p.AddClauses(formula)
	fmt.Println("Formula:", formula)<commit_msg>Add test to demonstrate issue #22: calling BlockSolution from inside Solve<commit_after>// Copyright <NAME> 2014. See the LICENSE file for more information.

package pigosat

import (
	"fmt"
	"reflect"
	"testing"
)

func TestLitArrayToSlice(t *testing.T) {
	// null pointers
	assertPanics(t, "null pointer", "litArrayToSlice",
		func() { litArrayToSlice(nil, 0) })
	assertPanics(t, "null pointer", "litArrayToSlice",
		func() { litArrayToSlice(nil, 1) })
	// not zero terminated
	badPtr := &cArray123[0]
	assertPanics(t, "not zero terminated - 1", "litArrayToSlice",
		func() { litArrayToSlice(badPtr, 1) })
	assertPanics(t, "not zero terminated - 2", "litArrayToSlice",
		func() { litArrayToSlice(badPtr, 2) })
	// zero length
	for maxLen := 0; maxLen <= 2; maxLen++ {
		if ls := litArrayToSlice(&cZero, 0); len(ls) != 0 {
			t.Errorf("Test 0-length litArrayToSlice, maxLen==%d: return value has length %d",
				maxLen, len(ls))
		}
	}
	// works correctly
	ptr := &cArray1230[0]
	expected := []Literal{1, 2, 3}
	for maxLen := 3; maxLen <= 10; maxLen++ {
		if ls := litArrayToSlice(ptr, maxLen); !reflect.DeepEqual(ls, expected) {
			t.Errorf("Test litArrayToSlice correct, maxLen==%d: expected %v but got %v",
				maxLen, expected, ls)
		}
	}
}

func TestAssumptionsSucceeding(t *testing.T) {
	successTests := []struct {
		assumpts  []Literal // The literals which should be assumed true/false
		solutions int       // The number of solutions that we expect to produce
	}{
		{[]Literal{1}, 10}, // We use formulaTests[0].formula below
		{[]Literal{2}, 9},
		{[]Literal{3}, 6},
		{[]Literal{4, 5}, 4},
	}

	for i, at := range successTests {
		p, _ := New(nil)
		p.AddClauses(formulaTests[0].formula)

		count := 0
		for ; ; count++ {
			for _, lit := range at.assumpts {
				p.Assume(lit)
			}
			status, sol := p.Solve()
			if status != Satisfiable {
				break
			}

			// All the UNSAT methods should give zero answers.
			if p.FailedAssumption(at.assumpts[0]) {
				t.Errorf("Test %d: FailedAssumption: expected %v not to be failed", i, at.assumpts[0])
			}
			if r := p.FailedAssumptions(); !reflect.DeepEqual(r, []Literal{}) {
				t.Errorf("Test %d: FailedAssumptions: expected [], got %v", i, r)
			}

			p.BlockSolution(sol)
		}
		if count != at.solutions {
			t.Errorf("Test %d: Expected %d solution(s) for assumptions %v; got %d",
				i, at.solutions, at.assumpts, count)
		}
	}
}

func TestAssumptionsFailing(t *testing.T) {
	p, _ := New(nil)
	p.AddClauses(formulaTests[0].formula)
	p.Assume(3)
	p.Assume(4)
	p.Assume(5)
	p.Solve()

	failed := []Literal{3, 4}
	if actual := p.FailedAssumptions(); !reflect.DeepEqual(failed, actual) {
		t.Errorf("Expected failed assumptions %v != %v actual", failed, actual)
	}
	for _, f := range failed {
		if !p.FailedAssumption(f) {
			t.Errorf("Expected literal %v to be a failed assumption", f)
		}
	}

	i, wanted := 0, [][]Literal{{3, 5}, {3, 5}, {5, 4}, {}}
	for a := p.MaxSatisfiableAssumptions(); len(a) > 0; i++ {
		if !reflect.DeepEqual(a, wanted[i]) {
			t.Errorf("(Next)MaxSat'Assumpt's: Got %v wanted %v", a, wanted[i])
		}
		a = p.NextMaxSatisfiableAssumptions()
	}
	if a := p.MaxSatisfiableAssumptions(); !reflect.DeepEqual(a, []Literal{}) {
		t.Errorf("MaxSatisfiableAssumptions: CNF inconsistent, so wanted []Literal{}, but got %v", a)
	}
}

// TestAssumptionsNoCrash tests that if you call Assume with a satisfiable
// assumption after Solve returns UNSAT then FailedAssumption(s) does not crash.
func TestCrashOnAssumeSatAfterUnsatThenCallFailedAssumptions(t *testing.T) {
	p, _ := New(nil)
	p.AddClauses(formulaTests[0].formula)
	p.Assume(3)
	p.Assume(4)
	p.Assume(5)
	p.Solve()

	if r := p.Res(); r != Unsatisfiable {
		t.Fatalf("Expected %v, got %v", Unsatisfiable, r)
	}
	if !p.FailedAssumption(3) {
		t.Fatalf("Expected literal 3 to be a failed assumption")
	}
	if r := p.Res(); r != Unsatisfiable {
		t.Fatalf("Expected %v, got %v", Unsatisfiable, r)
	}

	p.Assume(3)
	if r := p.Res(); r != Unsatisfiable {
		t.Fatalf("Expected %v, got %v", Unsatisfiable, r)
	}

	// Either the next two assertions work or they crash with this message:
	//   *** picosat: API usage: expected to be in UNSAT state
	//   SIGABRT: abort
	if p.FailedAssumption(3) {
		t.Errorf("FailedAssumption: Expected false, got true")
	}
	if r := p.FailedAssumptions(); len(r) != 0 {
		t.Errorf("FailedAssumptions: Expected []Literal{}, got %v", r)
	}
}

// TestNextMaxSatisfiableAssumptionsAsIterator tests that NextMaxSatisfiableAssumptions
// can be used as an iterator. In particular, this test panics if Solve calls
// BlockSolution when Solve returns Satisfiable.
func TestNextMaxSatisfiableAssumptionsAsIterator(t *testing.T) {
	var formula = Formula{{1, 2, 3}, {1, 2}, {2, 3}}
	p, _ := New(nil)
	p.AddClauses(formula)
	p.Assume(1)
	p.Assume(-2)
	p.Solve()
	p.Assume(-1)
	p.Assume(-2)
	ms := make([][]Literal, 0)
	for m := p.NextMaxSatisfiableAssumptions(); len(m) > 0; m = p.NextMaxSatisfiableAssumptions() {
		ms = append(ms, m)
	}
	expected := [][]Literal{{-1}, {-2}}
	if !reflect.DeepEqual(ms, expected) {
		t.Errorf("Expected %v. Got %v.", expected, ms)
	}
}

// ExamplePigosat_Assume demonstrates how to use Assume and related methods.
func ExamplePigosat_Assume() {
	var formula = Formula{{1, 2, 3}, {1, 2}, {2, 3}}
	p, _ := New(nil)
	p.AddClauses(formula)
	fmt.Println("Formula:", formula)
{'fraction_non_alphanumeric': 0.16340133306402746, 'fraction_numerical': 0.01686527974146637, 'mean_word_length': 3.966399197592778, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 8, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 5, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '7340339', 'n_tokens_mistral': 4049, 'n_tokens_neox': 3658, 'n_words': 983}