mirror of
https://github.com/mudler/luet.git
synced 2025-09-06 17:50:34 +00:00
🎨 Port package to types
This refactors DefaultPackage into types.Package and gets rid of the interface. This is a preceeding for a follow up where accessors will be removed from the code. It also does several cleanup, so we get rid also of some unneeded dependencies.
This commit is contained in:
135
pkg/solver/explainer.go
Normal file
135
pkg/solver/explainer.go
Normal file
@@ -0,0 +1,135 @@
|
||||
// Copyright © 2021-2022 Ettore Di Giacinto <mudler@mocaccino.org>
|
||||
//
|
||||
// This program is free software; you can redistribute it and/or modify
|
||||
// it under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 2 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// This program is distributed in the hope that it will be useful,
|
||||
// but WITHOUT ANY WARRANTY; without even the implied warranty of
|
||||
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
||||
// GNU General Public License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License along
|
||||
// with this program; if not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
package solver
|
||||
|
||||
import (
|
||||
"bufio"
|
||||
"bytes"
|
||||
"fmt"
|
||||
"io"
|
||||
"strings"
|
||||
|
||||
"github.com/crillab/gophersat/bf"
|
||||
"github.com/crillab/gophersat/explain"
|
||||
types "github.com/mudler/luet/pkg/api/core/types"
|
||||
"github.com/pkg/errors"
|
||||
)
|
||||
|
||||
type Explainer struct{}
|
||||
|
||||
func decodeDimacs(vars map[string]string, dimacs string) (string, error) {
|
||||
res := ""
|
||||
sc := bufio.NewScanner(bytes.NewBufferString(dimacs))
|
||||
lines := strings.Split(dimacs, "\n")
|
||||
linenum := 1
|
||||
SCAN:
|
||||
for sc.Scan() {
|
||||
|
||||
line := sc.Text()
|
||||
fields := strings.Fields(line)
|
||||
if len(fields) == 0 {
|
||||
continue
|
||||
}
|
||||
switch fields[0] {
|
||||
case "p":
|
||||
continue SCAN
|
||||
default:
|
||||
for i := 0; i < len(fields)-1; i++ {
|
||||
v := fields[i]
|
||||
negative := false
|
||||
if strings.HasPrefix(fields[i], "-") {
|
||||
v = strings.TrimLeft(fields[i], "-")
|
||||
negative = true
|
||||
}
|
||||
variable := vars[v]
|
||||
if negative {
|
||||
res += fmt.Sprintf("!(%s)", variable)
|
||||
} else {
|
||||
res += variable
|
||||
}
|
||||
|
||||
if i != len(fields)-2 {
|
||||
res += fmt.Sprintf(" or ")
|
||||
}
|
||||
}
|
||||
if linenum != len(lines)-1 {
|
||||
res += fmt.Sprintf(" and \n")
|
||||
}
|
||||
}
|
||||
linenum++
|
||||
}
|
||||
if err := sc.Err(); err != nil {
|
||||
return res, fmt.Errorf("could not parse problem: %v", err)
|
||||
}
|
||||
return res, nil
|
||||
}
|
||||
|
||||
func parseVars(r io.Reader) (map[string]string, error) {
|
||||
sc := bufio.NewScanner(r)
|
||||
res := map[string]string{}
|
||||
for sc.Scan() {
|
||||
line := sc.Text()
|
||||
fields := strings.Fields(line)
|
||||
if len(fields) == 0 {
|
||||
continue
|
||||
}
|
||||
switch fields[0] {
|
||||
case "c":
|
||||
data := strings.Split(fields[1], "=")
|
||||
res[data[1]] = data[0]
|
||||
|
||||
default:
|
||||
continue
|
||||
|
||||
}
|
||||
}
|
||||
if err := sc.Err(); err != nil {
|
||||
return nil, fmt.Errorf("could not parse problem: %v", err)
|
||||
}
|
||||
return res, nil
|
||||
}
|
||||
|
||||
// Solve tries to find the MUS (minimum unsat) formula from the original problem.
|
||||
// it returns an error with the decoded dimacs
|
||||
func (*Explainer) Solve(f bf.Formula, s types.PackageSolver) (types.PackagesAssertions, error) {
|
||||
buf := bytes.NewBufferString("")
|
||||
if err := bf.Dimacs(f, buf); err != nil {
|
||||
return nil, errors.Wrap(err, "cannot extract dimacs from formula")
|
||||
}
|
||||
|
||||
copy := *buf
|
||||
|
||||
pb, err := explain.ParseCNF(©)
|
||||
if err != nil {
|
||||
return nil, errors.Wrap(err, "could not parse problem")
|
||||
}
|
||||
pb2, err := pb.MUS()
|
||||
if err != nil {
|
||||
return nil, errors.Wrap(err, "could not extract subset")
|
||||
}
|
||||
|
||||
variables, err := parseVars(buf)
|
||||
if err != nil {
|
||||
return nil, errors.Wrap(err, "could not parse variables")
|
||||
}
|
||||
|
||||
res, err := decodeDimacs(variables, pb2.CNF())
|
||||
if err != nil {
|
||||
return nil, errors.Wrap(err, "could not parse dimacs")
|
||||
}
|
||||
|
||||
return nil, fmt.Errorf("could not satisfy the constraints: \n%s", res)
|
||||
}
|
Reference in New Issue
Block a user