From 09018c15c6e55ceed4a39bb6c072dfbc98f99c71 Mon Sep 17 00:00:00 2001 From: "John [Pete] Peterson" Date: Tue, 20 Jul 2021 11:34:34 -0400 Subject: [PATCH 1/3] initial implementation of rddl tests for (in)equality atom-based appraoch for boolean interop --- tests/fol/test_sorts.py | 22 ++++++ tests/io/test_rddl_writer.py | 140 ++++++++++++++++++++++++++++++++++- 2 files changed, 161 insertions(+), 1 deletion(-) diff --git a/tests/fol/test_sorts.py b/tests/fol/test_sorts.py index 94d498ad..60a3767c 100644 --- a/tests/fol/test_sorts.py +++ b/tests/fol/test_sorts.py @@ -201,3 +201,25 @@ def test_sort_domain_retrieval(): with pytest.raises(err.TarskiError): lang.Integer.domain() # Domain too large to iterate over it + +def test_boolean_sort_no_arithmetic_theory(): + #todo: [Pete] should force Equality theory when Boolean attached? + lang = tarski.language(theories=[Theory.BOOLEAN, Theory.EQUALITY]) + assert lang.Boolean in lang.sorts, 'the Boolean sort should be attached' + assert lang.Object in lang.sorts, 'the object sort should be the only other sort' + assert len(lang.sorts) == 2, 'the Boolean and Object sorts should be the only sorts' + + assert isinstance(lang.Boolean, Interval), 'the Boolean sort is an interval' + assert lang.Boolean.cardinality() == 2, 'Boolean sort is of cardinality 2' + assert lang.Boolean.builtin == True + assert parent(lang.Boolean) == lang.Object, 'since there are no numeric sorts, the Boolean sort has parent Object' + +def test_boolean_sort_with_arithmetic_theory(): + lang = tarski.language(theories=[Theory.BOOLEAN, Theory.EQUALITY, Theory.ARITHMETIC]) + assert lang.Boolean in lang.sorts, 'the Boolean sort should always be attached' + assert len(lang.sorts) == 5, 'sorts Boolean, Integer, Naturals, Reals and Object attached' + + assert isinstance(lang.Boolean, Interval), 'the Boolean sort is an interval' + assert lang.Boolean.cardinality() == 2, 'Boolean sort is of cardinality 2' + assert lang.Boolean.builtin == True + assert parent(lang.Boolean) == lang.Natural, 'when there are numeric sorts, the parent of Boolean is Naturals' diff --git a/tests/io/test_rddl_writer.py b/tests/io/test_rddl_writer.py index 68f3cd20..862d8164 100644 --- a/tests/io/test_rddl_writer.py +++ b/tests/io/test_rddl_writer.py @@ -383,7 +383,7 @@ def test_parametrized_model_with_random_vars_and_waypoints_boolean(): uy = lang.function('uy', vehicle, lang.Real) t = lang.function('t', lang.Real) - wv = lang.predicate('visited', waypoint) + wv = lang.function('visited', waypoint, lang.Boolean) # objects v001 = lang.constant('v001', vehicle) @@ -472,3 +472,141 @@ def test_parametrized_model_with_random_vars_and_waypoints_boolean(): assert mr_reader.rddl_model.domain.name == 'lqg_nav_2d_multi_unit_bool_waypoints' mr_reader.translate_rddl_model() assert mr_reader.language is not None + + +def test_rddl_integration_with_boolean_patterns_academic_advising_example_write(): + lang = tarski.language('standard', [Theory.BOOLEAN, Theory.EQUALITY, Theory.ARITHMETIC, Theory.RANDOM]) + the_task = Task(lang, 'academic_advising', 'instance_001') + + the_task.requirements = [rddl.Requirements.REWARD_DET, rddl.Requirements.PRECONDITIONS] + + the_task.parameters.discount = 1.0 + the_task.parameters.horizon = 20 + the_task.parameters.max_nondef_actions = 1 + + #sorts + course = lang.sort('course') + + # variables + c = lang.variable('c', course) + c2 = lang.variable('c2', course) + + # non fluents + PREREQ = lang.function('PREREQ', course, course, lang.Boolean) + PRIOR_PROB_PASS_NO_PREREQ = lang.function('PRIOR_PROB_PASS_NO_PREREQ', course, lang.Real) + PRIOR_PROB_PASS = lang.function('PRIOR_PROB_PASS', course, lang.Real) + PROGRAM_REQUIREMENT = lang.function('PROGRAM_REQUIREMENT', course, lang.Boolean) + COURSE_COST = lang.function('COURSE_COST', lang.Real) + COURSE_RETAKE_COST = lang.function('COURSE_RETAKE_COST', lang.Real) + PROGRAM_INCOMPLETE_PENALTY = lang.function('PROGRAM_INCOMPLETE_PENALTY', lang.Real) + COURSES_PER_SEMESTER = lang.function('COURSES_PER_SEMESTER', lang.Real) + + # state fluents + passed = lang.function('passed', course, lang.Boolean) + taken = lang.function('taken', course, lang.Boolean) + + # action fluents + take_course = lang.function('take-course', course, lang.Boolean) + + one = lang.constant(1, lang.Real) + # cpfs + the_task.add_cpfs(passed(c), ite((take_course(c) == 1) & ~(sum(c2, PREREQ(c2, c)) > 0), + bernoulli(PRIOR_PROB_PASS_NO_PREREQ(c)), + ite((take_course(c) == 1), + bernoulli(PRIOR_PROB_PASS(c) + + ((one - PRIOR_PROB_PASS(c)) + * (sumterm(c2, (PREREQ(c2, c) & passed(c2)))) + / (one + sumterm(c2, (PREREQ(c2, c)))))), + passed(c)))) + + the_task.add_cpfs(taken(c), (taken(c) == 1) | (take_course(c) == 1)) + + # cost function + the_task.reward = ( sumterm(c, COURSE_COST() * (ite((take_course(c) == 1) & (taken(c) == 0), one, zero))) + + sumterm(c, COURSE_RETAKE_COST() * (ite((take_course(c) == 1) & (taken(c) == 1))) + + (PROGRAM_INCOMPLETE_PENALTY() * ite(~(forall(c, (PROGRAM_REQUIREMENT(c) == 1) > (passed(c) == 1)), 1, 0))))) + + # constraints + the_task.add_constraint(forall(c, ((take_course(c) == 1) > (passed(c) == 0)), rddl.ConstraintType.ACTION)) + the_task.add_constraint(sumterm(c, take_course(c)) <= COURSES_PER_SEMESTER(), rddl.ConstraintType.ACTION) + + # fluent metadata + the_task.declare_state_fluent(passed(c), 0) + the_task.declare_state_fluent(taken(c), 0) + the_task.declare_action_fluent(take_course(c), 0) + the_task.declare_non_fluent(PREREQ(c, c2), 0) + the_task.declare_non_fluent(PRIOR_PROB_PASS_NO_PREREQ(c), 0.8) + the_task.declare_non_fluent(PRIOR_PROB_PASS(c), 0.2) + the_task.declare_non_fluent(PROGRAM_REQUIREMENT(c), 0) + the_task.declare_non_fluent(COURSE_COST(), -1) + the_task.declare_non_fluent(COURSE_RETAKE_COST(), -2) + the_task.declare_non_fluent(PROGRAM_INCOMPLETE_PENALTY(), -5) + the_task.declare_non_fluent(COURSES_PER_SEMESTER(), 1) + + #constants + c0000 = lang.constant('c0000', course) + c0001 = lang.constant('c0001', course) + c0002 = lang.constant('c0002', course) + c0003 = lang.constant('c0003', course) + c0004 = lang.constant('c0004', course) + c0100 = lang.constant('c0100', course) + c0101 = lang.constant('c0101', course) + c0102 = lang.constant('c0102', course) + c0103 = lang.constant('c0103', course) + c0200 = lang.constant('c0200', course) + c0201 = lang.constant('c0201', course) + c0202 = lang.constant('c0202', course) + c0300 = lang.constant('c0300', course) + c0301 = lang.constant('c0301', course) + c0302 = lang.constant('c0302', course) + + the_task.x0.set(PRIOR_PROB_PASS_NO_PREREQ(c0000), 0.80) + the_task.x0.set(PRIOR_PROB_PASS_NO_PREREQ(c0001), 0.55) + the_task.x0.set(PRIOR_PROB_PASS_NO_PREREQ(c0002), 0.67) + the_task.x0.set(PRIOR_PROB_PASS_NO_PREREQ(c0003), 0.78) + the_task.x0.set(PRIOR_PROB_PASS_NO_PREREQ(c0004), 0.75) + the_task.x0.set(PRIOR_PROB_PASS(c0100), 0.22) + the_task.x0.set(PRIOR_PROB_PASS(c0101), 0.45) + the_task.x0.set(PRIOR_PROB_PASS(c0102), 0.41) + the_task.x0.set(PRIOR_PROB_PASS(c0103), 0.44) + the_task.x0.set(PRIOR_PROB_PASS(c0200), 0.14) + the_task.x0.set(PRIOR_PROB_PASS(c0201), 0.07) + the_task.x0.set(PRIOR_PROB_PASS(c0202), 0.24) + the_task.x0.set(PRIOR_PROB_PASS(c0300), 0.23) + the_task.x0.set(PRIOR_PROB_PASS(c0301), 0.08) + the_task.x0.set(PRIOR_PROB_PASS(c0302), 0.16) + + + the_task.x0.set(PREREQ(c0003, c0100), 1) + the_task.x0.set(PREREQ(c0000, c0100), 1) + the_task.x0.set(PREREQ(c0004, c0100), 1) + the_task.x0.set(PREREQ(c0001, c0101), 1) + the_task.x0.set(PREREQ(c0002, c0101), 1) + the_task.x0.set(PREREQ(c0000, c0102), 1) + the_task.x0.set(PREREQ(c0004, c0102), 1) + the_task.x0.set(PREREQ(c0001, c0103), 1) + the_task.x0.set(PREREQ(c0001, c0200), 1) + the_task.x0.set(PREREQ(c0101, c0200), 1) + the_task.x0.set(PREREQ(c0103, c0201), 1) + the_task.x0.set(PREREQ(c0002, c0202), 1) + the_task.x0.set(PREREQ(c0200, c0300), 1) + the_task.x0.set(PREREQ(c0201, c0301), 1) + the_task.x0.set(PREREQ(c0201, c0301), 1) + the_task.x0.set(PREREQ(c0200, c0302), 1) + + the_task.x0.set(PROGRAM_REQUIREMENT(c0300), 1) + the_task.x0.set(PROGRAM_REQUIREMENT(c0202), 1) + the_task.x0.set(PROGRAM_REQUIREMENT(c0101), 1) + the_task.x0.set(PROGRAM_REQUIREMENT(c0002), 1) + the_task.x0.set(PROGRAM_REQUIREMENT(c0001), 1) + + the_task.x0.set(passed(c0000), 0) + + the_writer = rddl.Writer(the_task) + rddl_filename = os.path.join(tempfile.gettempdir(), 'academic_advising_001.rddl') + the_writer.write_model(rddl_filename) + mr_reader = rddl.Reader(rddl_filename) + assert mr_reader.rddl_model is not None + assert mr_reader.rddl_model.domain.name == 'academic_advising' + mr_reader.translate_rddl_model() + assert mr_reader.language is not None From 6ad72e5c09346a437b8d56dab3cb627850742fb5 Mon Sep 17 00:00:00 2001 From: "John [Pete] Peterson" Date: Thu, 22 Jul 2021 11:12:44 -0400 Subject: [PATCH 2/3] implements tests and changes to Boolean sort & RDDL writer IO to support equality-atom based boolean interop development Tests are focused on supporting Boolean/numeric interoperability for RDDL as discussed in #91. Currently passing all relevent tests. Read-side IO is untested. Write-side IO does not test necessary simplifications from the equality-atom, if-then-else wrapper, and sumterm-based quantifier replacements to typical RDDL patterns. --- src/tarski/io/rddl.py | 97 ++++++++++++++++++++++---- src/tarski/syntax/arithmetic/random.py | 8 +++ src/tarski/syntax/builtins.py | 5 +- src/tarski/syntax/sorts.py | 29 ++++---- src/tarski/syntax/terms.py | 2 +- src/tarski/theories.py | 4 +- tests/fol/test_sorts.py | 9 ++- tests/io/test_rddl_writer.py | 21 +++--- 8 files changed, 127 insertions(+), 48 deletions(-) diff --git a/src/tarski/io/rddl.py b/src/tarski/io/rddl.py index d8190b04..895fd687 100644 --- a/src/tarski/io/rddl.py +++ b/src/tarski/io/rddl.py @@ -7,7 +7,7 @@ from .common import load_tpl from ..fol import FirstOrderLanguage from ..syntax import implies, land, lor, neg, Connective, Quantifier, CompoundTerm, Interval, Atom, IfThenElse, \ - Contradiction, Tautology, CompoundFormula, forall, ite, AggregateCompoundTerm, QuantifiedFormula, Term, Function, \ + Contradiction, Tautology, CompoundFormula, forall, exists, ite, AggregateCompoundTerm, QuantifiedFormula, Term, Function, \ Variable, Predicate, Constant, Formula, builtins from ..syntax import arithmetic as tm from ..syntax.temporal import ltl as tt @@ -25,6 +25,7 @@ class TranslationError(Exception): logic_rddl_to_tarski = { '=>': implies, '^': land, + '&': land, '|': lor, '~': neg} @@ -149,9 +150,15 @@ def translate_expression(lang, rddl_expr): prod_expr = ite(prod_expr, Constant(1, lang.Integer), Constant(0, lang.Integer)) return tm.product(var, prod_expr) elif expr_sym == 'forall': - var = translate_expression(lang, rddl_expr.args[0]) - forall_expr = translate_expression(lang, rddl_expr.args[1]) - return forall(var, forall_expr) + vars = [translate_expression(lang, a) for a in rddl_expr.args[:-1]] + #var = translate_expression(lang, rddl_expr.args[0]) + forall_expr = translate_expression(lang, rddl_expr.args[-1]) + return forall(*(vars + [forall_expr])) + elif expr_sym == 'exists': + vars = [translate_expression(lang, a) for a in rddl_expr.args[:-1]] + #var = translate_expression(lang, rddl_expr.args[0]) + exists_expr = translate_expression(lang, rddl_expr.args[-1]) + return exists(*(vars + [exists_expr])) elif expr_type == 'arithmetic': op = arithmetic_rddl_to_tarski[expr_sym] targs = [lang] + [translate_expression(lang, arg) for arg in rddl_expr.args] @@ -211,9 +218,12 @@ class Reader: that specify a RDDL task """ - def __init__(self, filename): + def __init__(self, domain_filename, inst_filename = None): self.language = None - self.rddl_model = self._load_rddl_model(filename) + if inst_filename is None: + self.rddl_model = self._load_rddl_model(domain_filename) + else: + self.rddl_model = self._load_rddl_model_ippc(domain_filename, inst_filename) self.parameters = Parameters() self.x0 = None @@ -226,6 +236,22 @@ def _load_rddl_model(filename): # parse RDDL return parser.parse(rddl) + @staticmethod + def _load_rddl_model_ippc(dom_filename, inst_filename): + with open(dom_filename, 'r') as input_file: + dom_text = input_file.read() + with open(inst_filename, 'r') as input_file: + inst_text = input_file.read() + full_text = '\n\n'.join([dom_text, inst_text]) + # MRJ: for debug purposes + #for k, l in enumerate(full_text.split('\n')): + # print(k, l) + parser = modules.import_pyrddl_parser()() + parser.debugging = True + parser.build() + # parse RDDL + return parser.parse(full_text) + def _translate_types(self): for typename, parent_type in self.rddl_model.domain.types: assert parent_type == 'object' @@ -262,9 +288,11 @@ def translate_rddl_model(self): # 3. acquire instance parameters self.parameters.horizon = self.rddl_model.instance.horizon self.parameters.discount = self.rddl_model.instance.discount - if self.rddl_model.instance.max_nondef_actions != 'pos-inf': - self.parameters.max_actions = self.rddl_model.instance.max_nondef_actions - + try: + if self.rddl_model.instance.max_nondef_actions != 'pos-inf': + self.parameters.max_actions = self.rddl_model.instance.max_nondef_actions + except AttributeError: + pass # 4. recover initial state, interpretation of fluents self.x0 = Model(self.language) self.x0.evaluator = evaluate @@ -317,6 +345,7 @@ class Requirements(Enum): CONTINUOUS = "continuous" MULTIVALUED = "multivalued" REWARD_DET = "reward-deterministic" + PRECONDITIONS = "preconditions" INTERMEDIATE_NODES = "intermediate-nodes" PARTIALLY_OBS = "partially-observed" CONCURRENT = "concurrent" @@ -415,7 +444,30 @@ def __init__(self, task): self.non_fluent_signatures = set() self.interm_signatures = set() - def write_model(self, filename): + def rddl_2018_format(self): + tpl = load_tpl("rddl_model_2018.tpl") + domain_content = tpl.format( + domain_name=self.task.domain_name, + req_list=self.get_requirements(), + type_list=self.get_types(), + pvar_list=self.get_pvars(), + cpfs_list=self.get_cpfs(), + reward_expr=self.get_reward(), + action_precondition_list=self.get_preconditions(), + state_invariant_list=self.get_state_invariants(), + domain_non_fluents='{}_non_fluents'.format(self.task.instance_name), + object_list=self.get_objects(), + non_fluent_expr=self.get_non_fluent_init(), + instance_name=self.task.instance_name, + init_state_fluent_expr=self.get_state_fluent_init(), + non_fluents_ref='{}_non_fluents'.format(self.task.instance_name), + max_nondef_actions=self.get_max_nondef_actions(), + horizon=self.get_horizon(), + discount=self.get_discount() + ) + return domain_content + + def rddl_pre_2018_format(self): tpl = load_tpl("rddl_model.tpl") content = tpl.format( domain_name=self.task.domain_name, @@ -436,8 +488,23 @@ def write_model(self, filename): horizon=self.get_horizon(), discount=self.get_discount() ) + return content + + + def write_model(self, filename, format_2018_style=False): with open(filename, 'w') as file: + if format_2018_style: + content = self.rddl_2018_format() + else: + content = self.rddl_pre_2018_format() file.write(content) + self.reset() + + def reset(self): + self.need_obj_decl = [] + self.need_constraints = {} + self.non_fluent_signatures = set() + self.interm_signatures = set() def get_requirements(self): return ', '.join([str(r) for r in self.task.requirements]) @@ -610,7 +677,9 @@ def rewrite(self, expr): if len(re_st) > 0: # MRJ: Random variables need parenthesis, other functions need # brackets... - if expr.symbol.symbol in builtins.get_random_binary_functions(): + relevant_functions = builtins.get_random_binary_functions() + relevant_functions += builtins.get_random_unary_functions() + if expr.symbol.symbol in relevant_functions: st_str = '({})'.format(','.join(re_st)) else: st_str = '[{}]'.format(','.join(re_st)) @@ -645,13 +714,13 @@ def rewrite(self, expr): re_sf = [self.rewrite(st) for st in expr.subformulas] re_sym = symbol_map[expr.connective] if len(re_sf) == 1: - return '{}{}'.format(re_sym, re_sf) + return '{}({})'.format(re_sym, re_sf[0]) return '({} {} {})'.format(re_sf[0], re_sym, re_sf[1]) elif isinstance(expr, QuantifiedFormula): re_f = self.rewrite(expr.formula) re_vars = ['?{} : {}'.format(x.symbol, x.sort.name) for x in expr.variables] re_sym = symbol_map[expr.quantifier] - return '{}_{{{}}} ({})'.format(re_sym, ','.join(re_vars), re_f) + return '{}_{{{}}} [{}]'.format(re_sym, ','.join(re_vars), re_f) elif isinstance(expr, AggregateCompoundTerm): re_expr = self.rewrite(expr.subterm) re_vars = ['?{} : {}'.format(x.symbol, x.sort.name) for x in expr.bound_vars] @@ -659,7 +728,7 @@ def rewrite(self, expr): re_sym = 'sum' elif expr.symbol == BFS.MUL: re_sym = 'prod' - return '{}_{{{}}} ({})'.format(re_sym, ','.join(re_vars), re_expr) + return '{}_{{{}}} [{}]'.format(re_sym, ','.join(re_vars), re_expr) raise RuntimeError(f"Unknown expression type for '{expr}'") @staticmethod diff --git a/src/tarski/syntax/arithmetic/random.py b/src/tarski/syntax/arithmetic/random.py index 6b508dae..b7a55e55 100644 --- a/src/tarski/syntax/arithmetic/random.py +++ b/src/tarski/syntax/arithmetic/random.py @@ -14,6 +14,14 @@ def normal(mu, sigma): return np.random.normal(mu, sigma) return normal_func(mu, sigma) +def bernoulli(p): + try: + bernoulli_func = p.language.get_function(bfs.BERNOULLI) + except AttributeError: + np = modules.import_numpy() + return np.random.random(p) + return bernoulli_func(p) + def gamma(shape, scale): try: diff --git a/src/tarski/syntax/builtins.py b/src/tarski/syntax/builtins.py index b2cd6828..f9711e28 100644 --- a/src/tarski/syntax/builtins.py +++ b/src/tarski/syntax/builtins.py @@ -111,9 +111,8 @@ def get_random_binary_functions(): def get_random_unary_functions(): - # BFS = BuiltinFunctionSymbol - return [] - + BFS = BuiltinFunctionSymbol + return [BFS.BERNOULLI] def get_predicate_from_symbol(symbol: str): return BuiltinPredicateSymbol(symbol) diff --git a/src/tarski/syntax/sorts.py b/src/tarski/syntax/sorts.py index e5deb540..9ea2cbff 100644 --- a/src/tarski/syntax/sorts.py +++ b/src/tarski/syntax/sorts.py @@ -29,7 +29,7 @@ def __hash__(self): return hash(self.name) def __eq__(self, other): - return self.name == other.name + return self.name == other.name and self.language == other.language def contains(self, x): """ Return true iff the current sort contains a constant with the given value """ @@ -155,7 +155,7 @@ def dump(self): return dict(name=self.name, domain=[self.lower_bound, self.upper_bound]) def domain(self): - if self.builtin or self.upper_bound - self.lower_bound > 9999: # Yes, very hacky + if self.upper_bound - self.lower_bound > 9999: # Yes, very hacky raise err.TarskiError(f'Cannot iterate over interval with range [{self.lower_bound}, {self.upper_bound}]') from . import Constant # pylint: disable=import-outside-toplevel # Avoiding circular references return (Constant(x, self) for x in range(self.lower_bound, self.upper_bound+1)) @@ -191,7 +191,7 @@ def children(s: Sort) -> Set[Sort]: def int_encode_fn(x): if isinstance(x, float) and not x.is_integer(): - raise ValueError(x) # We don't want 1.2 to get encoded as an int + raise ValueError() # We don't want 1.2 to get encoded as an int return int(x) @@ -199,17 +199,6 @@ def float_encode_fn(x): return float(x) -def build_the_bools(lang): - bools = lang.sort('Boolean') - # TODO: we really should be setting builtin to True, but at the moment this is undesirable, as in many places in - # the code we seem to assume that "builtin" sorts are kind of "numeric" sorts, which leads us to try to do - # things with the new Bool sort that cannot be done, e.g. to cast string object "True" to a value, etc. - # bools.builtin = True - lang.constant('True', bools) - lang.constant('False', bools) - return bools - - def build_the_naturals(lang): the_nats = Interval('Natural', lang, int_encode_fn, 0, 2 ** 32 - 1, builtin=True) the_nats.builtin = True @@ -227,12 +216,20 @@ def build_the_reals(lang): reals.builtin = True return reals +def build_the_bools(lang): + bools = Interval('Boolean', lang, int_encode_fn, 0, 1, builtin=True) + bools.builtin = True + return bools + +def attach_the_non_arithmetic_bools(lang): + _ = lang.attach_sort(build_the_bools(lang), lang.ns.object) def attach_arithmetic_sorts(lang): real_t = lang.attach_sort(build_the_reals(lang), lang.ns.object) int_t = lang.attach_sort(build_the_integers(lang), real_t) - _ = lang.attach_sort(build_the_naturals(lang), int_t) - + nat_t = lang.attach_sort(build_the_naturals(lang), int_t) + if not lang.has_sort("Boolean"): + _ = lang.attach_sort(build_the_bools(lang), nat_t) def compute_signature_bindings(signature): """ Return an exhaustive list of all possible bindings compatible with the given signature, i.e. diff --git a/src/tarski/syntax/terms.py b/src/tarski/syntax/terms.py index a508e799..068df914 100644 --- a/src/tarski/syntax/terms.py +++ b/src/tarski/syntax/terms.py @@ -110,7 +110,7 @@ def __divmod__(self, rhs): def __and__(self, rhs): return self.language.dispatch_operator('&', Term, Term, self, rhs) - + def __xor__(self, rhs): return self.language.dispatch_operator('^', Term, Term, self, rhs) diff --git a/src/tarski/theories.py b/src/tarski/theories.py index 0c53d95b..4506ac32 100644 --- a/src/tarski/theories.py +++ b/src/tarski/theories.py @@ -57,7 +57,7 @@ def load_theory(lang, theory: Union[Theory, str]): raise err.UnknownTheory(theory) theories_requiring_arithmetic_sorts = { - Theory.ARITHMETIC, Theory.SPECIAL, Theory.RANDOM + Theory.ARITHMETIC, Theory.SPECIAL, Theory.RANDOM, Theory.BOOLEAN } if th in theories_requiring_arithmetic_sorts and not lang.has_sort('Integer'): attach_arithmetic_sorts(lang) @@ -129,7 +129,7 @@ def load_random_theory(lang): f.builtin = True for fun in builtins.get_random_unary_functions(): lang.register_unary_operator_handler(fun, Term, create_casting_handler(lang, fun, create_arithmetic_term)) - f = lang.function(fun, lang.Real, lang.Real) + f = lang.function(fun, lang.Real, lang.Boolean) f.builtin = True diff --git a/tests/fol/test_sorts.py b/tests/fol/test_sorts.py index 60a3767c..4801fbfe 100644 --- a/tests/fol/test_sorts.py +++ b/tests/fol/test_sorts.py @@ -6,7 +6,7 @@ from tarski.benchmarks.counters import generate_fstrips_counters_problem from tarski.syntax import symref from tarski.syntax.ops import compute_sort_id_assignment -from tarski.syntax.sorts import parent, ancestors, compute_signature_bindings, compute_direct_sort_map +from tarski.syntax.sorts import parent, ancestors, compute_signature_bindings, compute_direct_sort_map, Interval from tarski.theories import Theory @@ -207,12 +207,15 @@ def test_boolean_sort_no_arithmetic_theory(): lang = tarski.language(theories=[Theory.BOOLEAN, Theory.EQUALITY]) assert lang.Boolean in lang.sorts, 'the Boolean sort should be attached' assert lang.Object in lang.sorts, 'the object sort should be the only other sort' - assert len(lang.sorts) == 2, 'the Boolean and Object sorts should be the only sorts' + assert lang.Integer in lang.sorts + assert lang.Real in lang.sorts + assert lang.Natural in lang.sorts + assert len(lang.sorts) == 5, 'the Boolean and Object sorts should be attached, in addition to numeric sorts (implicitly)' assert isinstance(lang.Boolean, Interval), 'the Boolean sort is an interval' assert lang.Boolean.cardinality() == 2, 'Boolean sort is of cardinality 2' assert lang.Boolean.builtin == True - assert parent(lang.Boolean) == lang.Object, 'since there are no numeric sorts, the Boolean sort has parent Object' + assert parent(lang.Boolean) == lang.Natural, 'Boolean sort always has the naturals as parent' def test_boolean_sort_with_arithmetic_theory(): lang = tarski.language(theories=[Theory.BOOLEAN, Theory.EQUALITY, Theory.ARITHMETIC]) diff --git a/tests/io/test_rddl_writer.py b/tests/io/test_rddl_writer.py index 862d8164..370d02c4 100644 --- a/tests/io/test_rddl_writer.py +++ b/tests/io/test_rddl_writer.py @@ -12,7 +12,7 @@ def test_simple_rddl_model(): - lang = tarski.language('lqr_nav_1d', [Theory.EQUALITY, Theory.ARITHMETIC, Theory.SPECIAL]) + lang = tarski.language('lqr_nav_1d', [Theory.BOOLEAN, Theory.EQUALITY, Theory.ARITHMETIC, Theory.SPECIAL]) the_task = Task(lang, 'lqr_nav_1d', 'instance_001') the_task.requirements = [rddl.Requirements.CONTINUOUS, rddl.Requirements.REWARD_DET] @@ -75,7 +75,7 @@ def test_simple_rddl_model(): def test_rddl_model_with_random_vars(): - lang = tarski.language('lqg_nav_1d', [Theory.EQUALITY, Theory.ARITHMETIC, Theory.SPECIAL, Theory.RANDOM]) + lang = tarski.language('lqg_nav_1d', [Theory.BOOLEAN, Theory.EQUALITY, Theory.ARITHMETIC, Theory.SPECIAL, Theory.RANDOM]) the_task = Task(lang, 'lqg_nav_1d', 'instance_001') the_task.requirements = [rddl.Requirements.CONTINUOUS, rddl.Requirements.REWARD_DET] @@ -405,7 +405,7 @@ def test_parametrized_model_with_random_vars_and_waypoints_boolean(): # cpfs the_task.add_cpfs(t(), t() + dt()) dist_vec_norm = ((x(v) - wx(wpt)) * (x(v) - wx(wpt))) + ((y(v) - wy(wpt)) * (y(v) - wy(wpt))) - the_task.add_cpfs(wv(wpt), (wv(wpt) | (sqrt(dist_vec_norm) <= wr()))) + the_task.add_cpfs(wv(wpt), ((wv(wpt) == lang.constant(1, lang.Boolean)) | (sqrt(dist_vec_norm) <= wr()))) the_task.add_cpfs(vx(v), vx(v) + dt() * ux(v) + normal(mu_w(), sigma_w())) the_task.add_cpfs(vy(v), vy(v) + dt() * uy(v) + normal(mu_w(), sigma_w())) the_task.add_cpfs(x(v), x(v) + dt() * vx(v)) @@ -509,25 +509,28 @@ def test_rddl_integration_with_boolean_patterns_academic_advising_example_write( take_course = lang.function('take-course', course, lang.Boolean) one = lang.constant(1, lang.Real) + true = lang.constant(1, lang.Boolean) + false = lang.constant(0, lang.Boolean) + # cpfs - the_task.add_cpfs(passed(c), ite((take_course(c) == 1) & ~(sum(c2, PREREQ(c2, c)) > 0), + the_task.add_cpfs(passed(c), ite((take_course(c) == 1) & ~(sumterm(c2, PREREQ(c2, c)) > 0), bernoulli(PRIOR_PROB_PASS_NO_PREREQ(c)), ite((take_course(c) == 1), bernoulli(PRIOR_PROB_PASS(c) + ((one - PRIOR_PROB_PASS(c)) - * (sumterm(c2, (PREREQ(c2, c) & passed(c2)))) + * (sumterm(c2, (ite((PREREQ(c2, c) == 1) & (passed(c2) == 1), true, false)))) / (one + sumterm(c2, (PREREQ(c2, c)))))), passed(c)))) the_task.add_cpfs(taken(c), (taken(c) == 1) | (take_course(c) == 1)) # cost function - the_task.reward = ( sumterm(c, COURSE_COST() * (ite((take_course(c) == 1) & (taken(c) == 0), one, zero))) - + sumterm(c, COURSE_RETAKE_COST() * (ite((take_course(c) == 1) & (taken(c) == 1))) - + (PROGRAM_INCOMPLETE_PENALTY() * ite(~(forall(c, (PROGRAM_REQUIREMENT(c) == 1) > (passed(c) == 1)), 1, 0))))) + the_task.reward = ( sumterm(c, COURSE_COST() * (ite((take_course(c) == 1) & (taken(c) == 0), true, false))) + + sumterm(c, COURSE_RETAKE_COST() * (ite((take_course(c) == 1) & (taken(c) == 1), true, false)) + + (PROGRAM_INCOMPLETE_PENALTY() * ite(~(forall(c, (PROGRAM_REQUIREMENT(c) == 1) > (passed(c) == 1))), true, false)))) # constraints - the_task.add_constraint(forall(c, ((take_course(c) == 1) > (passed(c) == 0)), rddl.ConstraintType.ACTION)) + the_task.add_constraint(forall(c, ((take_course(c) == 1) > (passed(c) == 0))), rddl.ConstraintType.ACTION) the_task.add_constraint(sumterm(c, take_course(c)) <= COURSES_PER_SEMESTER(), rddl.ConstraintType.ACTION) # fluent metadata From caad5e0c0d39fcc4c4ef1017e62a39e491ffafb0 Mon Sep 17 00:00:00 2001 From: "John [Pete] Peterson" Date: Fri, 23 Jul 2021 10:30:19 -0400 Subject: [PATCH 3/3] implements minor hacks in write-side rddl IO to get true/false literals rather than 1/0 in written files for bool vars --- src/tarski/io/rddl.py | 69 +++++++++++++++++++++++++++++------- tests/io/test_rddl_writer.py | 14 ++++---- 2 files changed, 64 insertions(+), 19 deletions(-) diff --git a/src/tarski/io/rddl.py b/src/tarski/io/rddl.py index 895fd687..ee7cd832 100644 --- a/src/tarski/io/rddl.py +++ b/src/tarski/io/rddl.py @@ -17,6 +17,11 @@ from ..errors import LanguageError from ..theories import Theory, language +def is_boolean_constant_equal_to_true(expr): + if isinstance(expr, Constant): + if Theory.BOOLEAN in expr.language.theories: + return expr.sort == expr.language.Boolean and expr.is_syntactically_equal(expr.language.constant(1, expr.language.Boolean)) + return False class TranslationError(Exception): pass @@ -311,8 +316,8 @@ def translate_rddl_model(self): self.x0.add(expr.predicate, *expr.subterms) -built_in_type_map = {'object': 'Object', 'real': 'Real', 'int': 'Integer'} -reverse_built_in_type_map = {'Object': 'object', 'Real': 'real', 'Integer': 'int'} +built_in_type_map = {'object': 'Object', 'real': 'Real', 'int': 'Integer', 'bool' : 'Boolean'} +reverse_built_in_type_map = {'Object': 'object', 'Real': 'real', 'Integer': 'int', 'Boolean': 'bool'} def translate_builtin_type(lang: FirstOrderLanguage, name): @@ -444,6 +449,9 @@ def __init__(self, task): self.non_fluent_signatures = set() self.interm_signatures = set() + self.bool_t = self.task.L.constant(1, self.task.L.Boolean) + self.bool_f = self.task.L.constant(0, self.task.L.Boolean) + def rddl_2018_format(self): tpl = load_tpl("rddl_model_2018.tpl") domain_content = tpl.format( @@ -490,7 +498,6 @@ def rddl_pre_2018_format(self): ) return content - def write_model(self, filename, format_2018_style=False): with open(filename, 'w') as file: if format_2018_style: @@ -547,12 +554,22 @@ def get_signature(fl): return '{}'.format(head) return '{}({})'.format(head, ','.join(domain)) + def get_valstring(self, fluent, value): + if self.get_type(fluent) == 'bool': + if value == 0: + return "false" + elif value == 1: + return "true" + else: + assert(False) + return str(value) + def get_pvars(self): pvar_decl_list = [] # state fluents for fl, v in self.task.state_fluents: rsig = self.get_signature(fl) - pvar_decl_list += ['\t{} : {{state-fluent, {}, default = {}}};'.format(rsig, self.get_type(fl), str(v))] + pvar_decl_list += ['\t{} : {{state-fluent, {}, default = {}}};'.format(rsig, self.get_type(fl), self.get_valstring(fl, v))] for fl, level in self.task.interm_fluents: rsig = self.get_signature(fl) try: @@ -562,14 +579,14 @@ def get_pvars(self): pvar_decl_list += ['\t{} : {{interm-fluent, {}, level = {}}};'.format(rsig, self.get_type(fl), str(level))] for fl, v in self.task.action_fluents: rsig = self.get_signature(fl) - pvar_decl_list += ['\t{} : {{action-fluent, {}, default = {}}};'.format(rsig, self.get_type(fl), str(v))] + pvar_decl_list += ['\t{} : {{action-fluent, {}, default = {}}};'.format(rsig, self.get_type(fl), self.get_valstring(fl,v))] for fl, v in self.task.non_fluents: rsig = self.get_signature(fl) try: self.non_fluent_signatures.add(fl.symbol.signature) except AttributeError: self.non_fluent_signatures.add(fl.predicate.signature) - pvar_decl_list += ['\t{} : {{non-fluent, {}, default = {}}};'.format(rsig, self.get_type(fl), str(v))] + pvar_decl_list += ['\t{} : {{non-fluent, {}, default = {}}};'.format(rsig, self.get_type(fl), self.get_valstring(fl,v))] return '\n'.join(pvar_decl_list) def get_cpfs(self): @@ -619,6 +636,11 @@ def get_non_fluent_init(self): term_str = signature[0] else: term_str = str(self.task.L.get(signature[0])(*subterms)) + if signature[-1] == "Boolean": + if value.is_syntactically_equal(self.bool_f): + value = "false" + elif value.is_syntactically_equal(self.bool_t): + value = "true" non_fluent_init_list += ['\t{} = {};'.format(term_str, value)] for signature, defs in self.task.x0.predicate_extensions.items(): if signature not in self.non_fluent_signatures: @@ -648,6 +670,11 @@ def get_state_fluent_init(self): term_str = signature[0] else: term_str = str(self.task.L.get(signature[0])(*subterms)) + if signature[-1] == "Boolean": + if value.is_syntactically_equal(self.bool_f): + value = "false" + elif value.is_syntactically_equal(self.bool_t): + value = "true" init_list += ['\t{} = {};'.format(term_str, value)] for signature, defs in self.task.x0.predicate_extensions.items(): if signature in self.non_fluent_signatures \ @@ -689,7 +716,14 @@ def rewrite(self, expr): return '{}{}'.format(expr.symbol.signature[0], st_str) elif isinstance(expr, Atom): re_st = [self.rewrite(st) for st in expr.subterms] + st = expr.subterms if expr.predicate.builtin: + #check to see if we have a equality atom wrapping a Boolean codomain function to a literal 1 constant + if expr.predicate.symbol == BPS.EQ: + if is_boolean_constant_equal_to_true(st[0]) and isinstance(st[1], CompoundTerm) and st[1].codomain == st[1].language.Boolean: + return re_st[1] + elif is_boolean_constant_equal_to_true(st[1]) and isinstance(st[0], CompoundTerm) and st[0].sort == st[0].language.Boolean: + return re_st[0] if expr.predicate.symbol in symbol_map.keys(): return '({} {} {})'.format(re_st[0], symbol_map[expr.predicate.symbol], re_st[1]) st_str = '' @@ -702,10 +736,21 @@ def rewrite(self, expr): elif isinstance(expr, Constant): return str(expr) elif isinstance(expr, IfThenElse): - cond = self.rewrite(expr.condition) - expr1 = self.rewrite(expr.subterms[0]) - expr2 = self.rewrite(expr.subterms[1]) - return 'if ({}) then ({}) else ({})'.format(cond, expr1, expr2) + #check to see if it is a conversion to a boolean type + isconversion = True + lang = expr.subterms[0].language + for index, val in [(0, 1),(1, 0)]: + st = expr.subterms[index] + if not (isinstance(st, Constant) and st.sort == lang.Boolean and st.is_syntactically_equal(lang.constant(val, lang.Boolean))): + isconversion = False + break + if isconversion: + return self.rewrite(expr.condition) + else: + cond = self.rewrite(expr.condition) + expr1 = self.rewrite(expr.subterms[0]) + expr2 = self.rewrite(expr.subterms[1]) + return 'if ({}) then ({}) else ({})'.format(cond, expr1, expr2) elif isinstance(expr, Tautology): return 'true' elif isinstance(expr, Contradiction): @@ -720,7 +765,7 @@ def rewrite(self, expr): re_f = self.rewrite(expr.formula) re_vars = ['?{} : {}'.format(x.symbol, x.sort.name) for x in expr.variables] re_sym = symbol_map[expr.quantifier] - return '{}_{{{}}} [{}]'.format(re_sym, ','.join(re_vars), re_f) + return '({}_{{{}}} [{}])'.format(re_sym, ','.join(re_vars), re_f) elif isinstance(expr, AggregateCompoundTerm): re_expr = self.rewrite(expr.subterm) re_vars = ['?{} : {}'.format(x.symbol, x.sort.name) for x in expr.bound_vars] @@ -728,7 +773,7 @@ def rewrite(self, expr): re_sym = 'sum' elif expr.symbol == BFS.MUL: re_sym = 'prod' - return '{}_{{{}}} [{}]'.format(re_sym, ','.join(re_vars), re_expr) + return '({}_{{{}}} [{}])'.format(re_sym, ','.join(re_vars), re_expr) raise RuntimeError(f"Unknown expression type for '{expr}'") @staticmethod diff --git a/tests/io/test_rddl_writer.py b/tests/io/test_rddl_writer.py index 370d02c4..f151f077 100644 --- a/tests/io/test_rddl_writer.py +++ b/tests/io/test_rddl_writer.py @@ -476,7 +476,7 @@ def test_parametrized_model_with_random_vars_and_waypoints_boolean(): def test_rddl_integration_with_boolean_patterns_academic_advising_example_write(): lang = tarski.language('standard', [Theory.BOOLEAN, Theory.EQUALITY, Theory.ARITHMETIC, Theory.RANDOM]) - the_task = Task(lang, 'academic_advising', 'instance_001') + the_task = Task(lang, 'academic_advising', 'academic_advising_001') the_task.requirements = [rddl.Requirements.REWARD_DET, rddl.Requirements.PRECONDITIONS] @@ -513,7 +513,7 @@ def test_rddl_integration_with_boolean_patterns_academic_advising_example_write( false = lang.constant(0, lang.Boolean) # cpfs - the_task.add_cpfs(passed(c), ite((take_course(c) == 1) & ~(sumterm(c2, PREREQ(c2, c)) > 0), + the_task.add_cpfs(passed(c), ite((take_course(c) == 1) & ~(exists(c2, PREREQ(c2, c) == 1)), bernoulli(PRIOR_PROB_PASS_NO_PREREQ(c)), ite((take_course(c) == 1), bernoulli(PRIOR_PROB_PASS(c) + @@ -525,12 +525,12 @@ def test_rddl_integration_with_boolean_patterns_academic_advising_example_write( the_task.add_cpfs(taken(c), (taken(c) == 1) | (take_course(c) == 1)) # cost function - the_task.reward = ( sumterm(c, COURSE_COST() * (ite((take_course(c) == 1) & (taken(c) == 0), true, false))) - + sumterm(c, COURSE_RETAKE_COST() * (ite((take_course(c) == 1) & (taken(c) == 1), true, false)) - + (PROGRAM_INCOMPLETE_PENALTY() * ite(~(forall(c, (PROGRAM_REQUIREMENT(c) == 1) > (passed(c) == 1))), true, false)))) + the_task.reward = ( sumterm(c, COURSE_COST() * (ite((take_course(c) == 1) & ~(taken(c) == 1), true, false))) + + sumterm(c, COURSE_RETAKE_COST() * (ite((take_course(c) == 1) & (taken(c) == 1), true, false))) + + (PROGRAM_INCOMPLETE_PENALTY() * ite(~(forall(c, (PROGRAM_REQUIREMENT(c) == 1) > (passed(c) == 1))), true, false))) # constraints - the_task.add_constraint(forall(c, ((take_course(c) == 1) > (passed(c) == 0))), rddl.ConstraintType.ACTION) + the_task.add_constraint(forall(c, ((take_course(c) == 1) > ~(passed(c) == 1))), rddl.ConstraintType.ACTION) the_task.add_constraint(sumterm(c, take_course(c)) <= COURSES_PER_SEMESTER(), rddl.ConstraintType.ACTION) # fluent metadata @@ -601,7 +601,7 @@ def test_rddl_integration_with_boolean_patterns_academic_advising_example_write( the_task.x0.set(PROGRAM_REQUIREMENT(c0202), 1) the_task.x0.set(PROGRAM_REQUIREMENT(c0101), 1) the_task.x0.set(PROGRAM_REQUIREMENT(c0002), 1) - the_task.x0.set(PROGRAM_REQUIREMENT(c0001), 1) + the_task.x0.set(PROGRAM_REQUIREMENT(c0001), 0) the_task.x0.set(passed(c0000), 0)