Added tests, small bug fix

src/isla/evaluator.py

@@ -26,6 +26,7 @@
 from grammar_graph import gg
 from orderedset import OrderedSet
 
+import isla.isla_shortcuts as sc
 from isla import language
 from isla.derivation_tree import DerivationTree
 from isla.helpers import is_nonterminal, Maybe, chain_functions, is_prefix
@@ -77,7 +78,6 @@
     replace_in_z3_expr,
     z3_subst,
 )
-import isla.isla_shortcuts as sc
 
 logger = logging.getLogger("evaluator")
 
@@ -329,7 +329,7 @@ def well_formed(
         )
 
     def raise_not_implemented_error(
-        formula: Formula,
+        formula: Formula, _1, _2, _3, _4
     ) -> Maybe[Tuple[bool, str]]:
         raise NotImplementedError(f"Unsupported formula type {type(formula).__name__}")
 
@@ -350,7 +350,7 @@ def close(check_function: callable) -> callable:
                 wellformed_quantified_formula,
                 wellformed_smt_formula,
                 wellformed_propositional_formula,
-                wellformed_structural_predicate_formula,
+                wellformed_predicate_formula,
                 raise_not_implemented_error,
             ],
         ),
@@ -568,14 +568,16 @@ def wellformed_propositional_formula(
         return Maybe((True, ""))
 
 
-def wellformed_structural_predicate_formula(
+def wellformed_predicate_formula(
     formula: Formula,
     _1,
     bound_vars: OrderedSet[BoundVariable],
     _2,
     _3,
 ) -> Maybe[Tuple[bool, str]]:
-    if not isinstance(formula, StructuralPredicateFormula):
+    if not isinstance(formula, StructuralPredicateFormula) and not isinstance(
+        formula, SemanticPredicateFormula
+    ):
         return Maybe.nothing()
 
     unbound_variables = [

src/isla/language.py

@@ -3761,7 +3761,7 @@ def exitExistsInt(self, ctx: IslaLanguageParser.ExistsIntContext):
         if self.mgr.var_declared(var_id):
             raise SyntaxError(
                 f"Variable {var_id} already declared "
-                f"(line {ctx.varId.symbol.line}, column {ctx.varId.symbol.column})"
+                f"(line {ctx.ID().symbol.line}, column {ctx.ID().symbol.column})"
             )
 
         self.formulas[ctx] = ExistsIntFormula(

src/isla/three_valued_truth.py

@@ -90,7 +90,7 @@ def __neg__(self):
         if self.is_unknown():
             return self
 
-        return ThreeValuedTruth(bool(self))
+        return ThreeValuedTruth(not bool(self))
 
     def __and__(self, other: "ThreeValuedTruth") -> "ThreeValuedTruth":
         if self.is_unknown() or other.is_unknown():

tests/test_language.py

@@ -178,6 +178,50 @@ def test_wellformed(self):
 
         self.assertFalse(well_formed(bad_formula_7, LANG_GRAMMAR)[0])
 
+    def test_wellformed_exists_int(self):
+        formula = parse_isla(
+            'exists int i: count(<start>, "<assgn>", i)',
+            LANG_GRAMMAR,
+            semantic_predicates={COUNT_PREDICATE},
+        )
+
+        self.assertTrue(well_formed(formula, LANG_GRAMMAR)[0])
+
+        formula = language.ForallFormula(
+            BoundVariable("start", "<start>"),
+            Constant("start", "<start>"),
+            language.ExistsIntFormula(
+                BoundVariable("i", "NUM"),
+                language.ExistsIntFormula(
+                    BoundVariable("i", "NUM"),
+                    language.SemanticPredicateFormula(
+                        COUNT_PREDICATE,
+                        BoundVariable("start", "<start>"),
+                        "<assgn>",
+                        BoundVariable("i", "NUM"),
+                    ),
+                ),
+            ),
+        )
+
+        self.assertFalse(well_formed(formula, LANG_GRAMMAR)[0])
+
+        formula = language.ForallFormula(
+            BoundVariable("start", "<start>"),
+            Constant("start", "<start>"),
+            language.ExistsIntFormula(
+                BoundVariable("i", "NUM"),
+                language.SemanticPredicateFormula(
+                    COUNT_PREDICATE,
+                    BoundVariable("start", "<start>"),
+                    "<assgn>",
+                    BoundVariable("k", "NUM"),
+                ),
+            ),
+        )
+
+        self.assertFalse(well_formed(formula, LANG_GRAMMAR)[0])
+
     def test_free_variables(self):
         # TODO: Remove if not refined, trivial that way
         formula: ExistsFormula = parse_isla(

tests/test_three_valued_truth.py

@@ -0,0 +1,65 @@
+import itertools
+import unittest
+
+from isla.three_valued_truth import ThreeValuedTruth
+
+
+class TestThreeValuedTruth(unittest.TestCase):
+    def test_neg(self):
+        tval = ThreeValuedTruth.unknown()
+        try:
+            result = not tval
+            self.fail("AssertionError expected")
+        except AssertionError:
+            pass
+
+        tval = ThreeValuedTruth.true()
+        self.assertTrue((-tval).is_false())
+
+        tval = ThreeValuedTruth.false()
+        self.assertTrue((-tval).is_true())
+
+    def test_and(self):
+        values = [
+            ThreeValuedTruth.unknown(),
+            ThreeValuedTruth.true(),
+            ThreeValuedTruth.false(),
+        ]
+
+        for val_1, val_2 in itertools.combinations_with_replacement(values, 2):
+            result = val_1 & val_2
+            self.assertTrue(
+                not val_1.is_unknown() and not val_2.is_unknown() or result.is_unknown()
+            )
+            self.assertTrue(
+                val_1.is_unknown()
+                or val_2.is_unknown()
+                or bool(result) == (bool(val_1) and bool(val_2))
+            )
+
+    def test_or(self):
+        values = [
+            ThreeValuedTruth.unknown(),
+            ThreeValuedTruth.true(),
+            ThreeValuedTruth.false(),
+        ]
+
+        for val_1, val_2 in itertools.combinations_with_replacement(values, 2):
+            result = val_1 | val_2
+            self.assertTrue(
+                not val_1.is_unknown() and not val_2.is_unknown() or result.is_unknown()
+            )
+            self.assertTrue(
+                val_1.is_unknown()
+                or val_2.is_unknown()
+                or bool(result) == (bool(val_1) or bool(val_2))
+            )
+
+    def test_str(self):
+        self.assertEqual("TRUE", str(ThreeValuedTruth.true()))
+        self.assertEqual("FALSE", str(ThreeValuedTruth.false()))
+        self.assertEqual("UNKNOWN", str(ThreeValuedTruth.unknown()))
+
+
+if __name__ == "__main__":
+    unittest.main()