Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add alternative Picosat Project #872

Merged
merged 11 commits into from
Feb 20, 2024
Merged

Add alternative Picosat Project #872

Changes from 7 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
e1ed49f
- Added class for adapted picosat project
Jan 30, 2024
d03d059
- Adapted project name for picosat fork
Jan 30, 2024
6c26801
Merge branch 'vara-dev' into f-PicoSat-vara
vulder Jan 30, 2024
0d281f6
- Updated project name for Picosat load time version
Feb 6, 2024
e689393
Merge branch 'vara-dev' into f-PicoSat-vara
Feb 6, 2024
0f5158d
- Updated workloads for Picosat LT and added recompile
Feb 7, 2024
ca52b10
Merge branch 'vara-dev' into f-PicoSat-vara
LuAbelt Feb 12, 2024
6088be8
- Updated workloads for Picosat LT
Feb 13, 2024
8d67747
- Updated project name for alternative PicoSAT project as suggested i…
Feb 19, 2024
45d111b
Update varats/varats/experiments/vara/feature_perf_precision.py
LuAbelt Feb 19, 2024
c697975
Merge branch 'vara-dev' into f-PicoSat-vara
vulder Feb 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
154 changes: 147 additions & 7 deletions varats/varats/projects/c_projects/picosat.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
import typing as tp

import benchbuild as bb
from benchbuild.command import WorkloadSet, Command, SourceRoot
from benchbuild.command import WorkloadSet, SourceRoot
from benchbuild.source import HTTP
from benchbuild.source.http import HTTPUntar
from benchbuild.utils.cmd import make
Expand All @@ -21,6 +21,7 @@
verify_binaries,
)
from varats.project.sources import FeatureSource
from varats.project.varats_command import VCommand
from varats.project.varats_project import VProject
from varats.provider.release.release_provider import (
ReleaseProviderHook,
Expand Down Expand Up @@ -98,39 +99,39 @@ class PicoSAT(VProject, ReleaseProviderHook):

WORKLOADS = {
WorkloadSet(WorkloadCategory.EXAMPLE): [
Command(
VCommand(
SourceRoot("picosat") / RSBinary("picosat"),
"example.cnf",
label="example.cnf",
)
],
WorkloadSet(WorkloadCategory.SMALL): [
Command(
VCommand(
SourceRoot("picosat") / RSBinary("picosat"),
"aim-100-1_6-no-1.cnf",
label="aim-100-1-6-no-1.cnf",
)
],
WorkloadSet(WorkloadCategory.MEDIUM): [
Command(
VCommand(
SourceRoot("picosat") / RSBinary("picosat"),
"traffic_kkb_unknown.cnf/traffic_kkb_unknown.cnf",
label="traffic-kkb-unknow.cnf",
),
Command(
VCommand(
SourceRoot("picosat") / RSBinary("picosat"),
"abw-N-bcsstk07.mtx-w44.cnf/abw-N-bcsstk07.mtx-w44.cnf",
label="abw-N-bcsstk07.mtx-w44.cnf",
),
],
WorkloadSet(WorkloadCategory.LARGE): [
Command(
VCommand(
SourceRoot("picosat") / RSBinary("picosat"),
"UNSAT_H_instances_childsnack_p11.hddl_1.cnf/"
"UNSAT_H_instances_childsnack_p11.hddl_1.cnf",
label="UNSAT-H-instances-childsnack-p11.hddl-1.cnf",
),
Command(
VCommand(
SourceRoot("picosat") / RSBinary("picosat"),
"UNSAT_H_instances_childsnack_p12.hddl_1.cnf/"
"UNSAT_H_instances_childsnack_p12.hddl_1.cnf",
Expand Down Expand Up @@ -189,3 +190,142 @@ def get_release_revisions(
return [(FullCommitHash(h), tag)
for h, tag in tagged_commits
if re.match(release_regex, tag)]


class PicoSATLT(VProject, ReleaseProviderHook):
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

For what does the LT stand?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

My initial thought was Load Time - I wanted to pick a more speaking addition to the normal Picosat for distinction that just VaRA, but in hindsight the LT itself is also not really more helpful.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The idea is good, maybe just call it that PicoSATLoadTime

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

Branch should be ready for a merge into vara-dev now

"""Adapted version of picoSAT that has been refactored, such that it does
not require a field-sensitive analysis."""

NAME = 'PicosatLT'
GROUP = 'c_projects'
DOMAIN = ProjectDomains.SOLVER

SOURCE = [
PaperConfigSpecificGit(
project_name="PicosatLT",
remote="https://github.com/se-sic/picoSAT-vara",
local="PicosatLT",
refspec="origin/HEAD",
limit=None,
shallow=False
),
FeatureSource(),
HTTP(
local="example.cnf",
remote={
"1.0":
"https://github.com/se-sic/picoSAT-mirror/releases/"
"download/picoSAT-965/example.cnf"
}
),
HTTPUntar(
local="abw-N-bcsstk07.mtx-w44.cnf",
remote={
"1.0":
"https://github.com/se-sic/picoSAT-mirror/releases/"
"download/picoSAT-965/abw-N-bcsstk07.mtx-w44.cnf.tar.gz"
}
),
HTTPUntar(
local="traffic_kkb_unknown.cnf",
remote={
"1.0":
"https://github.com/se-sic/picoSAT-mirror/releases/"
"download/picoSAT-965/traffic_kkb_unknown.cnf.tar.gz"
}
),
HTTPUntar(
local="UNSAT_H_instances_childsnack_p11.hddl_1.cnf",
remote={
"1.0":
"https://github.com/se-sic/picoSAT-mirror/releases/"
"download/picoSAT-965/"
"UNSAT_H_instances_childsnack_p11.hddl_1.cnf.tar.gz"
}
),
HTTPUntar(
local="UNSAT_H_instances_childsnack_p12.hddl_1.cnf",
remote={
"1.0":
"https://github.com/se-sic/picoSAT-mirror/releases/"
"download/picoSAT-965/"
"UNSAT_H_instances_childsnack_p12.hddl_1.cnf.tar.gz"
}
),
]

WORKLOADS = {
WorkloadSet(WorkloadCategory.MEDIUM): [
VCommand(
SourceRoot("PicosatLT") / RSBinary("picosat"),
"abw-N-bcsstk07.mtx-w44.cnf/abw-N-bcsstk07.mtx-w44.cnf",
label="abw-N-bcsstk07.mtx-w44.cnf",
),
],
}

@staticmethod
def binaries_for_revision(
revision: ShortCommitHash
) -> tp.List[ProjectBinaryWrapper]:
binary_map = RevisionBinaryMap(
get_local_project_git_path(PicoSATLT.NAME)
)
binary_map.specify_binary(
'picosat', BinaryType.EXECUTABLE, valid_exit_codes=[0, 10, 20]
)

return binary_map[revision]

def run_tests(self) -> None:
pass

def compile(self) -> None:
"""Compile the project."""
picosat_source = local.path(self.source_of(self.primary_source))

c_compiler = bb.compiler.cc(self)
cxx_compiler = bb.compiler.cxx(self)

with local.cwd(picosat_source):
revisions_with_new_config_name = get_all_revisions_between(
"33c685e82213228726364980814f0183e435de78", "", ShortCommitHash
)
picosat_version = ShortCommitHash(self.version_of_primary)
if picosat_version in revisions_with_new_config_name:
config_script_name = "./configure.sh"
else:
config_script_name = "./configure"

with local.cwd(picosat_source):
with local.env(CC=str(c_compiler), CXX=str(cxx_compiler)):
bb.watch(local[config_script_name])(["--trace", "--stats"])
bb.watch(make)("-j", get_number_of_jobs(bb_cfg()))

with local.cwd(picosat_source):
verify_binaries(self)

def recompile(self) -> None:
"""Re-Compile the project."""
picosat_source = local.path(self.source_of(self.primary_source))
c_compiler = bb.compiler.cc(self)
cxx_compiler = bb.compiler.cxx(self)

with local.cwd(picosat_source):
with local.env(CC=str(c_compiler), CXX=str(cxx_compiler)):
bb.watch(make)("-j", get_number_of_jobs(bb_cfg()))

with local.cwd(picosat_source):
verify_binaries(self)

@classmethod
def get_release_revisions(
cls, release_type: ReleaseType
) -> tp.List[tp.Tuple[FullCommitHash, str]]:
release_regex = "^picoSAT-[0-9]+$"

tagged_commits = get_tagged_commits(cls.NAME)

return [(FullCommitHash(h), tag)
for h, tag in tagged_commits
if re.match(release_regex, tag)]
Loading