diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-20 14:48:22 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-20 14:48:22 +0000 |
commit | a426d4b7795a173d6a50418a38a3b41bbfaf880d (patch) | |
tree | 0687d074dd73c5b474538814e1c5f29207f48ab1 /src/theory/mktheorytraits | |
parent | 96240c3cbc2a25e2d9ab14d1048ffda82a83ded2 (diff) |
Added Theory::postsolve() infrastructure as Clark requested.
(Though currently unused.)
For theories that request presolve and postsolve (in their kinds file),
they will get a presolve() notification before the first check(). After
the final check during the current search, they get a postsolve().
presolve() and postsolve() notifications always come in pairs, bracketing
all check()/propagate()/getValue() calls related to a single query. In
the case of incremental benchmarks, theories may get additional
presolve()/postsolve() pairs, but again, they always come in pairs.
Expected performance impact: none (for theories that don't use it)
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3598&reference_id=3581&p=5
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 |