diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-16 21:30:41 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-16 21:30:41 +0000 |
commit | dd30200795d4b37398c29f0d20998c9bd63a7fe7 (patch) | |
tree | 494e235520553c0f20654bb991e8359e6b0f1b9e /src/theory/mktheorytraits | |
parent | d260caa58d462f7e1eb0d94f73789f844f5f5596 (diff) |
Replace propagateAsDecision() with Theory::getNextDecisionRequest():
* arrays now uses the new approach by using a CDQueue<>
* uf strong solver has had the feature disabled, pending a merge from Andy
* theory kinds files now have a getNextDecisionRequest property (if you want to take part in such decision requests you have to list that property)
* the staticLearning property has been renamed ppStaticLearn to match the function name
* theory kinds files are now checked again for correctly-declared properties (this had been disabled)
* minor documentation and other fixups
Diffstat (limited to 'src/theory/mktheorytraits')
-rwxr-xr-x | src/theory/mktheorytraits | 41 |
1 files changed, 22 insertions, 19 deletions
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 60ff05d35..c8ef23a78 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -47,10 +47,11 @@ mk_type_enumerator_cases= theory_has_check="false" theory_has_propagate="false" -theory_has_staticLearning="false" +theory_has_ppStaticLearn="false" theory_has_notifyRestart="false" theory_has_presolve="false" theory_has_postsolve="false" +theory_has_getNextDecisionRequest="false" theory_stable_infinite="false" theory_finite="false" @@ -143,36 +144,37 @@ struct TheoryTraits<${theory_id}> { static const bool hasCheck = ${theory_has_check}; static const bool hasPropagate = ${theory_has_propagate}; - static const bool hasStaticLearning = ${theory_has_staticLearning}; + static const bool hasPpStaticLearn = ${theory_has_ppStaticLearn}; static const bool hasNotifyRestart = ${theory_has_notifyRestart}; static const bool hasPresolve = ${theory_has_presolve}; static const bool hasPostsolve = ${theory_has_postsolve}; + static const bool hasGetNextDecisionRequest = ${theory_has_getNextDecisionRequest}; };/* struct TheoryTraits<${theory_id}> */ " # warnings about theory content and properties - # TODO: fix, not corresponding to staticLearning anymore - # dir="$(dirname "$kf")/../../" - # if [ -e "$dir/$theory_header" ]; then - # 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 - # else - # grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' && - # echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2 - # fi - # done - # else - # echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2 - # fi + dir="$(dirname "$kf")/../../" + if [ -e "$dir/$theory_header" ]; then + for function in check propagate ppStaticLearn notifyRestart presolve postsolve getNextDecisionRequest; 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 + else + grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' && + echo "$kf: warning: $theory_class does not have property \"$function\" in its kinds file but appears to declare the function" >&2 + fi + done + else + echo "$me: warning: theory header \"$theory_header\" does not exist or is unreadable" >&2 + fi theory_has_check="false" theory_has_propagate="false" - theory_has_staticLearning="false" + theory_has_ppStaticLearn="false" theory_has_notifyRestart="false" theory_has_presolve="false" theory_has_postsolve="false" + theory_has_getNextDecisionRequest="false" theory_stable_infinite="false" theory_finite="false" @@ -264,9 +266,10 @@ function properties { polite) theory_polite="true";; check) theory_has_check="true";; propagate) theory_has_propagate="true";; - staticLearning) theory_has_staticLearning="true";; + ppStaticLearn) theory_has_ppStaticLearn="true";; presolve) theory_has_presolve="true";; postsolve) theory_has_postsolve="true";; + getNextDecisionRequest) theory_has_getNextDecisionRequest="true";; notifyRestart) theory_has_notifyRestart="true";; *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;; esac |