diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-30 11:57:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-30 11:57:58 -0500 |
commit | bc0c0b8b9ea77e8e4e328dbe66a4582fa7883eda (patch) | |
tree | 4f43e20e294ade551676847668ceb424d44bab4f /test/regress/regress1/strings/policy_variable.smt2 | |
parent | 3eac9d04c5d4bfba81142d4a5fe91b86590b32ae (diff) |
Add regular expression elimination module (#2400)
Diffstat (limited to 'test/regress/regress1/strings/policy_variable.smt2')
-rw-r--r-- | test/regress/regress1/strings/policy_variable.smt2 | 40 |
1 files changed, 40 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/policy_variable.smt2 b/test/regress/regress1/strings/policy_variable.smt2 new file mode 100644 index 000000000..4d14e95d5 --- /dev/null +++ b/test/regress/regress1/strings/policy_variable.smt2 @@ -0,0 +1,40 @@ +(set-info :smt-lib-version 2.5) +(set-logic ALL) +(set-info :status unsat) +(set-option :strings-exp true) +(set-option :re-elim true) +(declare-const actionName String) +(declare-const actionNamespace String) +(declare-const example_key String) + +; Action: p0.0 +(declare-const p0.0.action Bool) +(assert (= p0.0.action (and (= "foobar" actionNamespace) (and (str.prefixof "ab" actionName) (str.contains (str.substr actionName 2 (- (str.len actionName) 3)) "b") (str.suffixof "b" actionName) (not (= actionName "abb")) (not (= actionName "ab")))))) + +; Policy: 0 +(declare-const p0.denies Bool) +(assert (not p0.denies)) +(declare-const p0.allows Bool) +(assert (= p0.allows (and (not p0.denies) p0.0.action))) +(declare-const p0.neutral Bool) +(assert (= p0.neutral (and (not p0.allows) (not p0.denies)))) + +; Action: p1.0 +(declare-const p1.0.action Bool) +(assert (= p1.0.action (and (= "foobar" actionNamespace) (and (str.prefixof "a" actionName) (str.prefixof example_key (str.substr actionName 1 (- (str.len actionName) 1))) (str.contains (str.substr actionName (+ 1 (str.len example_key)) (- (str.len actionName) 1 (str.len example_key))) "b") (str.suffixof "b" actionName))))) + +(declare-const p1.0.condition Bool) +(assert (= p1.0.condition (str.prefixof "bb" example_key))) + +; Policy: 1 +(declare-const p1.denies Bool) +(assert (not p1.denies)) +(declare-const p1.allows Bool) +(assert (= p1.allows (and (not p1.denies) p1.0.action p1.0.condition))) +(declare-const p1.neutral Bool) +(assert (= p1.neutral (and (not p1.allows) (not p1.denies)))) + +; Goals +(assert (or p0.neutral p0.denies)) +(assert p1.allows) +(check-sat) |