diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-01 09:18:27 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-01 16:18:27 +0000 |
| commit | afaf4413775ff7d6054a5893f1397ad908e0773c (patch) | |
| tree | 2b0af7821b910a325f80f41246e3a4a6a4f363b1 /src | |
| parent | 8b71d28d4c63b4147429125fae7de3d75fb55bd8 (diff) | |
kinds: Remove non-existent properties. (#6253)
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/bags/kinds | 4 | ||||
| -rwxr-xr-x | src/theory/mktheorytraits | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds index cd53484eb..dd8eacfb5 100644 --- a/src/theory/bags/kinds +++ b/src/theory/bags/kinds @@ -12,7 +12,7 @@ rewriter ::CVC5::theory::bags::BagsRewriter \ "theory/bags/bags_rewriter.h" properties parametric -properties check propagate presolve +properties check presolve # constants constant EMPTYBAG \ @@ -90,4 +90,4 @@ typerule BAG_TO_SET ::CVC5::theory::bags::ToSetTypeRule construle UNION_DISJOINT ::CVC5::theory::bags::BinaryOperatorTypeRule construle MK_BAG ::CVC5::theory::bags::MkBagTypeRule -endtheory
\ No newline at end of file +endtheory diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 81e551a10..b2c6e1ef2 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -172,7 +172,7 @@ struct TheoryTraits<${theory_id}> { # warnings about theory content and properties dir="$(dirname "$kf")/../../" if [ -e "$dir/$theory_header" ]; then - for function in check propagate ppStaticLearn notifyRestart presolve postsolve; do + for function in propagate ppStaticLearn notifyRestart presolve postsolve; do if eval "\$theory_has_$function"; then grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' || echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2 |