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.

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
4 changes: 2 additions & 2 deletions varats/varats/experiments/vara/feature_perf_precision.py
Original file line number Diff line number Diff line change
Expand Up @@ -99,9 +99,9 @@ def get_threshold(project: VProject) -> int:
if project.DOMAIN is ProjectDomains.TEST:
if project.name in [
"SynthSAFieldSensitivity", "SynthIPRuntime", "SynthIPTemplate",
"SynthIPTemplate2", "SynthIPCombined"
"SynthIPTemplate2", "SynthIPCombined", "PicoSATLoadTime"
]:
# Don't instrument everything for these synthtic projects
# Don't instrument everything for these synthetic projects
return 10

return 0
Expand Down
162 changes: 155 additions & 7 deletions varats/varats/projects/c_projects/picosat.py
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,150 @@ def get_release_revisions(
return [(FullCommitHash(h), tag)
for h, tag in tagged_commits
if re.match(release_regex, tag)]


class PicoSATLoadTime(VProject, ReleaseProviderHook):
"""Adapted version of picoSAT that has been refactored, such that it does
not require a field-sensitive analysis."""

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

SOURCE = [
PaperConfigSpecificGit(
project_name="PicoSATLoadTime",
remote="https://github.com/se-sic/picoSAT-vara",
local="PicoSATLoadTime",
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"
}
),
HTTP(
local="ibm-2004-03-k70.cnf",
remote={
"1.0":
"https://github.com/se-sic/picoSAT-vara/releases/"
"download/workloads-sat-race-2006/ibm-2004-03-k70.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.SMALL): [
VCommand(
SourceRoot("PicoSATLoadTime") / RSBinary("picosat"),
"ibm-2004-03-k70.cnf",
label="ibm-2004-03-k70.cnf",
),
],
}

@staticmethod
def binaries_for_revision(
revision: ShortCommitHash
) -> tp.List[ProjectBinaryWrapper]:
binary_map = RevisionBinaryMap(
get_local_project_git_path(PicoSATLoadTime.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