Commit 0f542be7 authored by Nikolai Käfer's avatar Nikolai Käfer 🏠
Browse files

version 0.7.0

parent d1fbba56
# Default ignored files
/shelf/
/workspace.xml
<?xml version="1.0" encoding="UTF-8"?>
<module type="PYTHON_MODULE" version="4">
<component name="NewModuleRootManager">
<content url="file://$MODULE_DIR$">
<excludeFolder url="file://$MODULE_DIR$/venv" />
</content>
<orderEntry type="inheritedJdk" />
<orderEntry type="sourceFolder" forTests="false" />
</component>
</module>
\ No newline at end of file
<component name="InspectionProjectProfileManager">
<settings>
<option name="USE_PROJECT_PROFILE" value="false" />
<version value="1.0" />
</settings>
</component>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<project version="4">
<component name="ProjectRootManager" version="2" project-jdk-name="Python 3.7 (venv)" project-jdk-type="Python SDK" />
</project>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<project version="4">
<component name="ProjectModuleManager">
<modules>
<module fileurl="file://$PROJECT_DIR$/.idea/code.iml" filepath="$PROJECT_DIR$/.idea/code.iml" />
</modules>
</component>
</project>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<project version="4">
<component name="VcsDirectoryMappings">
<mapping directory="$PROJECT_DIR$" vcs="Git" />
</component>
</project>
\ No newline at end of file
; P(cr⇒r) = 2 ∗ P(cr⇒m)
(declare-fun p_CR-R () Real)
(declare-fun p_CR-M () Real)
(assert (= p_CR-R (* 2 p_CR-M)))
; P(cr⇒r ∨ cr⇒m | cr) ≥ 0.98
; P((cr⇒r ∨ cr⇒m) ∧ cr) ≥ 0.98 ∗ P(cr)
; P(cr⇒r ∧ cr) + P(cr⇒m ∧ cr) ≥ 0.98 ∗ P(cr)
(declare-fun p_CR_CR-R () Real)
(declare-fun p_CR_CR-M () Real)
(declare-fun p_CR () Real)
(assert (>= (+ p_CR_CR-R p_CR_CR-M) (* 0.98 p_CR)))
; bicycle AF
CT ; continue
ST ; stop
; lidar
LD
LD-M
NLD
NLD-NM
; camera left
CL
CL-L
CL-M
NCL
NCL-NL
NCL-NM
; camera right
CR
CR-R
CR-M
NCR
NCR-NR
NCR-NM
# ; attacks
CT ST
LD NLD
LD NLD-NM
NLD LD
NLD LD-M
LD-M NLD-NM
LD-M NCL-NM
LD-M NCR-NM
LD-M CT
NLD-NM LD-M
NLD-NM CL-M
NLD-NM CR-M
CL NCL
CL NCL-NL
CL NCL-NM
NCL CL
NCL CL-L
NCL CL-M
CL-M NLD-NM
CL-M NCL-NM
CL-M NCR-NM
CL-M CT
NCL-NM LD-M
NCL-NM CL-M
NCL-NM CR-M
CL-L NCL-NL
NCL-NL CL-L
CR NCR
CR NCR-NR
CR NCR-NM
NCR CR
NCR CR-R
NCR CR-M
CR-M NLD-NM
CR-M NCL-NM
CR-M NCR-NM
CR-M CT
NCR-NM LD-M
NCR-NM CL-M
NCR-NM CR-M
CR-R NCR-NR
NCR-NR CR-R
\ No newline at end of file
; bicycle AF
CT ; continue
ST ; stop
; lidar
;LD
;LD-M
;NLD
;NLD-NM
; camera left
CL
CL-L
CL-M
NCL
NCL-NL
NCL-NM
; camera right
CR
CR-R
CR-M
NCR
NCR-NR
NCR-NM
# ; attacks
CT ST
;LD NLD
;LD NLD-NM
;NLD LD
;NLD LD-M
;LD-M NLD-NM
;LD-M NCL-NM
;LD-M NCR-NM
;LD-M CT
;NLD-NM LD-M
;NLD-NM CL-M
;NLD-NM CR-M
CL NCL
CL NCL-NL
CL NCL-NM
NCL CL
NCL CL-L
NCL CL-M
;CL-M NLD-NM
CL-M NCL-NM
CL-M NCR-NM
CL-M CT
;NCL-NM LD-M
NCL-NM CL-M
NCL-NM CR-M
CL-L NCL-NL
NCL-NL CL-L
CR NCR
CR NCR-NR
CR NCR-NM
NCR CR
NCR CR-R
NCR CR-M
;CR-M NLD-NM
CR-M NCL-NM
CR-M NCR-NM
CR-M CT
;NCR-NM LD-M
NCR-NM CL-M
NCR-NM CR-M
CR-R NCR-NR
NCR-NR CR-R
\ No newline at end of file
(declare-fun p_A1_nA2_B () Real)
(declare-fun p_A1_B () Real)
(assert (= p_A1_B 1))
\ No newline at end of file
A1
A2
B
C
#
A1 B
A1 A2
A2 B
A2 A1
B C
\ No newline at end of file
A
B
C
D
#
A B
B C
B D
D A
\ No newline at end of file
A
B
C
D
#
A B
;A D
B C
B D
C A
D B
\ No newline at end of file
A 0.5
B
C
D
#
A B
B C
C A
C D
D C
\ No newline at end of file
......@@ -36,7 +36,31 @@ Basic usage usually requires at least three flags:
* `--semantics` (or `-s`) followed by the names of one or more semantics
* the task to perform, e.g. `--one_distribution` to compute one distribution which satisfies the constraints of all specified semantics
cpraa --file AFs/example.tgf --semantics MinCmp --one_distribution
**Example:**
$ cpraa --file AFs/example.tgf --semantics MinCmp --one_distribution
Computing one distribution satisfying the following semantics: MinCmp
Support:
P( A,-B, C) = 1
The result shows a distribution in _support format_, that is, only the assignments with non-zero probabilities are shown.
In this case, `P( A,-B, C) = 1` means that the assignment where `A` and `C` hold while `B` does not hold has a probability of one under this distribution.
To get the full distribution, the flag `--distribution_output_format` (or just `-o` for short) can be used with parameter `F`.
Likewise, the parameter `M` can be passed with the same flag to display the marginal probabilities of all arguments, and it is possible to pass multiple format options at once:
$ cpraa --file AFs/example.tgf --semantics MinCmp --one_distribution --distribution_output_format FM
Computing one distribution satisfying the following semantics: MinCmp
P(-A,-B,-C) = 0
P(-A,-B, C) = 0
P(-A, B,-C) = 0
P(-A, B, C) = 0
P( A,-B,-C) = 0
P( A,-B, C) = 1
P( A, B,-C) = 0
P( A, B, C) = 0
P(A) = 1
P(B) = 0
P(C) = 1
## Input format
......@@ -81,7 +105,7 @@ There is also the option to specify that certain semantics should _not_ hold wit
A list of all available semantics can be viewed with `--list_semantics` or `-ls`:
$ cpraa --list_semantics
Available semantics: DiracStl, DiracSStl, DiracPrf, DiracGrn, DiracCmp, DiracAdm, DiracCF, StrengthSupportCF, StrengthCF, CFs, NNor, NNorAF, AF, SNor, Nor, WNor, SNorS, NorS, WNorS, ElmStl, ElmSStl, ElmPrf, ElmGrn, ElmCmp, ElmAdm, ElmCF, JntCmp, MinCmp, PrCmp, WCmp, JntAdm, MinAdm, PrAdm, WAdm, CF, Jus, SOpt, Opt, Coh, Rat, Inv, SFou, Fou, Ter, Dirac, Max, Neu, Min
Available semantics: Min, Neu, Max, Dirac, Ter, Fou, SFou, Inv, Rat, Coh, Opt, SOpt, Jus, CF, WAdm, PrAdm, MinAdm, JntAdm, WCmp, PrCmp, MinCmp, JntCmp, ElmCF, ElmAdm, ElmCmp, ElmGrn, ElmPrf, ElmSStl, ElmStl, WNorS, NorS, SNorS, WNor, Nor, SNor, AF, NNorAF, NNor, CFs, StrengthCF, StrengthSupportCF, DiracCF, DiracAdm, DiracCmp, DiracGrn, DiracPrf, DiracSStl, DiracStl
Tip: With `--documentation` or `-d` followed by the names of one or more semantics a short description of most semantics is available:
......@@ -150,7 +174,7 @@ As expected, the resulting distributions are the Dirac distributions of the assi
`-MIN`, `--minimize_probability`, or `-MAX`, `--maximize_probability`
This task requires linear constraints and one or more arguments from the AF (passed with `--arguments` or `-a`).
If the constraints are satisfiable, the resulting distribution minimises (or maximises) the marginal probability of the given argument, or, if multiple arguments are given, the probability of any argument holding.
If the constraints are satisfiable, the resulting distribution minimises (or respectively maximises) the marginal probability of the given argument, or, if multiple arguments are given, the probability of any argument holding.
**Example:** (TODO)
......@@ -184,6 +208,8 @@ If the constraints are satisfiable, the resulting distribution minimises (or max
## Further options
`-smt`, `--smt_file`
`-b`, `--backend_solver`
`-t`, `--time`
......
__version__ = '0.2.0'
__version__ = '0.7.0'
......@@ -12,15 +12,21 @@ import assignments as asg
from distribution import Distribution
from timer import Timer
Constraint = Tuple[np.array, float]
DEFAULT_SOLVER = "glpk"
# TODO:
# - also handle equalities as constraints
# - sparse matrix representation of constraints?
Constraint = Tuple[np.array, float]
DEFAULT_SOLVER = "glpk"
class LinearConstraintError(Exception):
pass
def config_solver(solver: str):
if solver is None:
return config_solver(DEFAULT_SOLVER)
......
......@@ -4,7 +4,8 @@ from typing import List
import af_parser
import labeling_scheme as lab
from labeling import Labeling
from linear_solver import LinearSolver
from linear_solver import LinearSolver, LinearConstraintError
from DPGM import DPGM
import semantics as sem
import tasks
from solver_instance import SolverInstance
......@@ -20,7 +21,7 @@ from timer import Timer
# - flag to generate unsat core; this needs named assertions, see assert_and_track() in z3.py
# - credulous and skeptical acceptance wrt. a labeling scheme
__version__ = "0.6.1"
__version__ = "0.7.0"
# Solvers
Z3_LEGACY = "z3-legacy"
......@@ -61,6 +62,7 @@ def main():
+ ", ".join(pysmt_solvers) + "), linear solvers via CVXOPT ("
+ ", ".join(linear_solvers) + "), and a direct integration of Z3 ("
+ Z3_LEGACY + ")")
base_group.add_argument("-smt", "--smt_file", help="add additional constraints from a file in SMT-LIB format")
lp_group = arg_parser.add_argument_group("optimization")
lp_group.add_argument("-MIN", "--minimize_probability", action="store_true",
......@@ -138,10 +140,10 @@ def main():
sem.CONSTRAINT_LOGGING = args.display_constraints
if args.list_semantics:
print("Available semantics:", ", ".join(sem.all_semantics_names()))
print("Available semantics:", ", ".join(reversed(sem.all_semantics_names())))
if args.list_labeling_schemes:
print("Available labeling schemes:", ", ".join(lab.get_all_labeling_scheme_names()))
print("Available labeling schemes:", ", ".join(reversed(lab.get_all_labeling_scheme_names())))
if args.documentation:
for name in args.documentation:
......@@ -227,7 +229,20 @@ def main():
if args.arguments:
if not af:
arg_parser.error("no AF provided")
arguments = [af.get_node_by_name(argument_name) for argument_name in args.arguments]
try:
arguments = [af.get_node_by_name(argument_name) for argument_name in args.arguments]
except ValueError as e:
arg_parser.error(str(e))
if args.smt_file:
if not af:
arg_parser.error("no AF provided")
if solver == Z3_LEGACY or solver in linear_solvers:
arg_parser.error("smt constraints only available via pysmt solvers")
# solver in pysmt_solvers or solver is None
si = get_smt_solver(si, af, solver)
with open(args.smt_file, "r") as smt_file:
si.add_constraints_from_smt(smt_file)
########
# tasks
......@@ -262,6 +277,9 @@ def main():
if args.corner_distributions:
if not af:
arg_parser.error("an AF must be provided to compute the corner distribution")
if args.smt_file:
arg_parser.error("task not available with additional SMT constraints")
assert_linear_semantics_availability(semantics, arg_parser)
if solver in linear_solvers:
ls = get_linear_solver(ls, af, solver)
else:
......@@ -287,13 +305,16 @@ def main():
arg_parser.error("no AF given, use -f to load one from a TGF file")
if not arguments:
arg_parser.error("no arguments from the AF given, provide one or more with -a")
if args.smt_file:
arg_parser.error("task not available with additional SMT constraints")
assert_linear_semantics_availability(semantics, arg_parser)
if solver in linear_solvers:
ls = get_linear_solver(ls, af, solver)
else:
ls = get_linear_solver(ls, af, None)
timer = Timer(output_string="Computing optimal distribution took")
print("Computing optimal distribution minimizing the marginal probabilities of", repr_list(args.arguments),
"while satisfying the following semantics:", repr_list(semantics))
print("Computing optimal distribution minimizing the probability of argument" + plural(args.arguments),
repr_list_i(args.arguments), "while satisfying the following semantics:", repr_list(semantics))
distribution = tasks.minimize_marginal_probabilities(ls, arguments, semantics)
if distribution:
distribution.print_formatted(args.distribution_output_format)
......@@ -306,13 +327,16 @@ def main():
arg_parser.error("no AF given, use -f to load one from a TGF file")
if not arguments:
arg_parser.error("no arguments from the AF given, provide one or more with -a")
if args.smt_file:
arg_parser.error("task not available with additional SMT constraints")
assert_linear_semantics_availability(semantics, arg_parser)
if solver in linear_solvers:
ls = get_linear_solver(ls, af, solver)
else:
ls = get_linear_solver(ls, af, None)
timer = Timer(output_string="Computing optimal distribution took")
print("Computing optimal distribution maximizing the marginal probabilities of", repr_list(args.arguments),
"while satisfying the following semantics:", repr_list(semantics))
print("Computing optimal distribution maximizing the probability of argument" + plural(args.arguments),
repr_list_i(args.arguments), "while satisfying the following semantics:", repr_list(semantics))
distribution = tasks.maximize_marginal_probabilities(ls, arguments, semantics)
if distribution:
distribution.print_formatted(args.distribution_output_format)
......@@ -335,6 +359,7 @@ def main():
ol_timer.start()
distribution = tasks.get_one_distribution_z3(z3i, semantics)
elif solver in linear_solvers:
assert_linear_semantics_availability(semantics, arg_parser)
ls = get_linear_solver(ls, af, solver)
ol_timer.start()
distribution = tasks.get_one_distribution_linear(ls, semantics)
......@@ -521,6 +546,20 @@ def main():
# print(af.name + ";" + timings)
def assert_linear_semantics_availability(semantics: List[sem.Semantics], arg_parser):
"""
Test availability of linear constraints for given semantics without constructing potentially expensive constraints.
"""
dummy_af = DPGM()
dummy_ls = LinearSolver(dummy_af)
for s in semantics:
dummy_s = s.__class__(dummy_af, complemented=s.complemented)
try:
dummy_s.get_linear_constraints(dummy_ls)
except NotImplementedError:
arg_parser.error("No linear constraints available (or implemented) for semantics '" + str(dummy_s) + "'")
def get_linear_solver(ls, af, solver_name) -> LinearSolver:
if ls is None:
ls_setup_timer = Timer(output_string="linear solver setup took")
......@@ -552,24 +591,20 @@ def repr_list(s: List[str]):
return "(none)"
if __name__ == "__main__":
main()
# ---------------------------------------------------------
def repr_list_i(s: List[str]):
assert len(s) > 0
if len(s) == 1:
return str(s[0])
else:
return ", ".join(map(str, s[:-1])) + " and " + str(s[-1])
def test_all_semantics():
# path = "AFs/af01.tgf"
path = "AFs/af_references_noisy.tgf"
af = af_parser.parse_tgf(path)
z3i = Z3Instance(af)
for semantics_class in tasks.Semantics.__subclasses__():
try:
semantics = semantics_class(af)
print(semantics_class.__name__, semantics.get_z3_constraints(z3i))
except NotImplementedError:
print(semantics_class.__name__, "(not implemented)")
def plural(s: List[str]):
if len(s) > 1:
return "s"
else:
return ""
# test_all_semantics()
if __name__ == "__main__":
main()
......@@ -1036,70 +1036,70 @@ class ElmStl(ElmClassicalSemantics):
# Experimental semantics generalizing labelings
################################################
class LabAdm(Semantics):
def generate_z3_constraints(self, z3i: Z3Instance):
sCF = CF(self.af)
self.constraints_z3.extend(sCF.get_z3_constraints(z3i))
for node in self.all_nodes:
node_prob = z3i.get_node_prob_var(node)
or_list = []
for parent_node in node.get_parents():
parent_node_prob = z3i.get_node_prob_var(parent_node)
or_list.append(parent_node_prob == 1)
self.add_z3_constraint(z3.Implies(node_prob == 0, z3.Or(or_list, z3i.context), z3i.context), node=node)
class SLabAdm(Semantics):
def generate_z3_constraints(self, z3i: Z3Instance):
sCF = CF(self.af)
self.constraints_z3.extend(sCF.get_z3_constraints(z3i))
for node in self.all_nodes:
node_prob = z3i.get_node_prob_var(node)
if node.is_initial():
continue
or_list = []
for parent_node in node.get_parents():
parent_node_prob = z3i.get_node_prob_var(parent_node)
or_list.append(parent_node_prob == 1)
self.add_z3_constraint(z3.Implies(node_prob == 0, z3.Or(or_list, z3i.context), z3i.context), node=node)
def open_interval_constraint(prob_var, context, low=0, high=1):
return z3.And(prob_var > low, prob_var < high, context)
class LabCmp(Semantics):
def generate_z3_constraints(self, z3i: Z3Instance):
labAdm = LabAdm(self.af)
self.constraints_z3.extend(labAdm.get_z3_constraints(z3i))
for node in self.all_nodes:
node_prob = z3i.get_node_prob_var(node)
node_undec = open_interval_constraint(node_prob, z3i.context)
or_list = []
for parent_node in node.get_parents():
parent_node_prob = z3i.get_node_prob_var(parent_node)
self.add_z3_constraint(z3.Implies(node_undec, parent_node_prob < 1, z3i.context), node=node)
parent_undec = open_interval_constraint(parent_node_prob, z3i.context)
or_list.append(parent_undec)
self.add_z3_constraint(z3.Implies(node_undec, z3.Or(or_list, z3i.context), z3i.context), node=node)
class SLabCmp(Semantics):
def generate_z3_constraints(self, z3i: Z3Instance):
sLabAdm = SLabAdm(self.af)
self.constraints_z3.extend(sLabAdm.get_z3_constraints(z3i))
for node in self.all_nodes:
node_prob = z3i.get_node_prob_var(node)
if node.is_initial():
continue
node_undec = open_interval_constraint(node_prob, z3i.context)
or_list = []
for parent_node in node.get_parents():
parent_node_prob = z3i.get_node_prob_var(parent_node)
self.add_z3_constraint(z3.Implies(node_undec, parent_node_prob < 1, z3i.context), node=node)
parent_undec = open_interval_constraint(parent_node_prob, z3i.context)
or_list.append(parent_undec)
self.add_z3_constraint(z3.Implies(node_undec, z3.Or(or_list, z3i.context), z3i.context), node=node)
# class LabAdm(Semantics):
# def generate_z3_constraints(self, z3i: Z3Instance):
# sCF = CF(self.af)
# self.constraints_z3.extend(sCF.get_z3_constraints(z3i))
# for node in self.all_nodes:
# node_prob = z3i.get_node_prob_var(node)
# or_list = []
# for parent_node in node.get_parents():
# parent_node_prob = z3i.get_node_prob_var(parent_node)
# or_list.append(parent_node_prob == 1)
# self.add_z3_constraint(z3.Implies(node_prob == 0, z3.Or(or_list, z3i.context), z3i.context), node=node)
#