Skip to content

Commit

Permalink
Add alternative Picosat Project (#872)
Browse files Browse the repository at this point in the history 
Additional fork for Picosat that does not rely on field sensitivity as much
  • Loading branch information
@LuAbelt
LuAbelt authored Feb 20, 2024
1 parent 27a6eae commit 954882a
Show file tree
Hide file tree
Showing 2 changed files with 157 additions and 9 deletions.
4 changes: 2 additions & 2 deletions varats/varats/experiments/vara/feature_perf_precision.py
View file
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
View file
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)]

0 comments on commit 954882a

Please sign in to comment.