diff options
Diffstat (limited to 'src/theory/mktheorytraits')
| -rwxr-xr-x | src/theory/mktheorytraits | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 8e503f53e..bccd520f9 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -45,6 +45,7 @@ theory_has_propagate="false" theory_has_staticLearning="false" theory_has_notifyRestart="false" theory_has_presolve="false" +theory_has_postsolve="false" theory_stable_infinite="false" theory_finite="false" @@ -133,13 +134,14 @@ struct TheoryTraits<${theory_id}> { static const bool hasStaticLearning = ${theory_has_staticLearning}; static const bool hasNotifyRestart = ${theory_has_notifyRestart}; static const bool hasPresolve = ${theory_has_presolve}; + static const bool hasPostsolve = ${theory_has_postsolve}; };/* struct TheoryTraits<${theory_id}> */ " # warnings about theory content and properties dir="$(dirname "$kf")/../../" if [ -e "$dir/$theory_header" ]; then - for function in check propagate staticLearning notifyRestart presolve; do + for function in check propagate staticLearning 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 @@ -157,6 +159,7 @@ struct TheoryTraits<${theory_id}> { theory_has_staticLearning="false" theory_has_notifyRestart="false" theory_has_presolve="false" + theory_has_postsolve="false" theory_stable_infinite="false" theory_finite="false" @@ -200,6 +203,7 @@ function properties { propagate) theory_has_propagate="true";; staticLearning) theory_has_staticLearning="true";; presolve) theory_has_presolve="true";; + postsolve) theory_has_postsolve="true";; notifyRestart) theory_has_notifyRestart="true";; *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;; esac |